The Coq mailing list

[Wolfram Kahl <kahl AT cas.mcmaster.ca>]

Dear Coq users,

  not really knowing Coq, and being spoilt by Agda myself,
I am still trying to help somebody here with their Coq developments.
For practical purposes, the immediate problem seems to be solved
by using a different definition of IsSome:

 Definition IsSome {T : Type} (x : option T) : Prop :=
   match x with
    | None => False
    | Some _ => True
   end.

However, I am still puzzled why I wasn't able to define IsSome_extract
starting from the inductive definition:

 Inductive IsSome {T : Type} : option T -> Prop :=
 |  isSome : forall (r : T), IsSome (Some r).

This definition is used throughout in the remainder of this message.
I want to have IsSome_extract, and try:

 Definition IsSome_extract : forall {A : Type} {x : option A} (xS : IsSome x) 
, A :=
  fun {A : Type} {x : option A} (xS : IsSome x) => match x with
     | None => match xS return A with
               end
     | Some a => a
   end.

Coq says:

 | Error: Found a matching with no clauses on a term unknown to have an empty
 | inductive type.

(Agda would know that IsSome None is an empty type...)

So I try a tactical ``proof'' instead of a term:

 Lemma IsSome_extract : forall {A : Type} {x : option A} (xS : IsSome x) , A.
 Proof.
  intros.
  induction x.
  (* Case 1 *)
  exact a.
  (* Case 2 *)

Now I am in the 1-goal proof state:

  A : Type
  xS : IsSome None
  ============================
   A

and cannot find anything to continue --- at least
destruct, induction, inversion all complain about a sort issue,
and I didn't find anything else that looked possibly useful.
But ``obviously'', there can be no such xS!
How do I make Coq see this?


I found False_rect in CoqArt, and tried:

 Definition IsSome_None_rect : forall T : Type , IsSome None -> T :=
   fun (T : Type) (x : IsSome None) => match x return T with
                                       end.

This also gets:

 | Error: Found a matching with no clauses on a term unknown to have an empty
 | inductive type.


Is there a way out?


Puzzled,

  Wolfram