The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Hello Pierre,

Your code seems to work under 8.4 (if we replace Variant with Inductive):

Require Import Program.

Inductive Is_Some {A} : option A -> Prop :=

| Is_some a : Is_Some (Some a).

Program Definition from_Some A (x : option A | Is_Some x) : A :=

   match x with

     | (Some a) => a

     | None => _

   end.

Next Obligation.

   apply False_rect. inversion H.

Qed.

From your error message, it seems that you're having some issue with universe levels. What's interesting is that, in 8.5, if we write the term that Coq is complaining about by hand, no error message appears:

Variant Is_Some {A} : option A -> Prop :=

| Is_some a : Is_Some (Some a).

Check (fun A (x : { x : option A | Is_Some x })  => proj1_sig x).

Em sex, 18 de mar de 2016 às 09:41, Pierre Néron <pierre.neron AT polytechnique.org> escreveu:

Hi,

I'm trying to use Program to define some kind of non-exhaustive pattern
matching.
For example I want to define a function from_Some : (x : option A |
"is_some x" ) -> A

Require Import Program.

Variant Is_Some {A} : option A -> Prop :=

| Is_some a : Is_Some (Some a).

Program Definition from_Some A (x : option A | Is_Some x) : A :=

   match x with

     | (Some a) => a

     | None => _

   end.

Next Obligation.

   apply False_rect. inversion H.

Fail Qed.

I can't understand why coq fails here with the following message:

The command has indeed failed with message:

Illegal application:

The term "proj1_sig" of type

  "forall (A : Type) (P : A -> Prop), {x : A | P x} -> A"

cannot be applied to the terms

  "option A" : "Type"

  "fun x : option A => Is_Some x" : "option A -> Prop"

  "x" : "{x : option A | Is_Some x}"

The 1st term has type "Type@{max(Set, Top.25)}" which should be coercible to

  "Type@{Coq.Init.Specif.16}".

  I managed to get around this problem by defining the following function:

Program Definition from_Some1 A (x : option A | Is_Some x) : A :=

   (match x as o return Is_Some o -> A with

     | (Some a) => fun _ => a

     | None => fun _ => !

   end) _.

Next Obligation of from_Some1.

   inversion H.

Qed.

but I would like to understand why the first definition fails.

Thanks in advance

--
Pierre.