The Coq mailing list

[Pierre Néron <pierre.neron AT polytechnique.org>]

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.