The Coq mailing list

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

Adam and Guillaume,

  thanks a lot for your comprehensive and helpful answers!


To my problems with definining IsSome_extract for
 >>
 >>  Inductive IsSome {T : Type} : option T ->  Prop :=
 >>  |  isSome : forall (r : T), IsSome (Some r).
 >>
, Adam Chlipala wrote:

 > OK, so here's my second attempt at a full answer: The phenomenon above
 > is indeed what's going wrong in your example, though it (I now see) does
 > not rule out writing a nice computational definition of
 > [IsSome_extract].  You just need to express your contradiction solely
 > within [Prop], and then you can do case analysis on a proof of [False],
 > which is allowed because the universe restriction on [match] is waived
 > for inductive types with at most one constructor, satisfying certain
 > constraints.  (This is how [False_rect] is defined, and I think that
 > writing the [match] directly is clearer.)
 > 
 > (**)
 > Lemma IsSome_None : forall {T}, IsSome (T := T) None -> False.
 >   inversion 1.
 > Qed.
 > 
 > Definition IsSome_extract {A : Type} {x : option A} : IsSome x -> A :=
 >   match x with
 >     | Some x => fun _ => x
 >     | None => fun H => match IsSome_None H with end
 >   end.
 > (**)

So the empty match works for False, but not for IsSome None
(which does have at most one constructor...) ---
are there useful cases besides False where it works,
or do the ``certain constraints'' effectively force us
to normally go via False?

``gallais'' wrote:

 > Lemma IsSome_extract : forall A (x : option A), IsSome x -> { r | x = Some 
 > r }.
 > Proof.
 > intros A x Hx ; destruct x.
 >  exists a ; reflexivity.
 >  apply False_rect.
 >   inversion Hx.
 > Qed.

(That additional equation is indeed essential, and I also had produced
 it for the other definition in the meantime.)
I found it surprising that ``inversion Hx'' works here,
while in my attempt (without the False_rect of gallais),
it produces a sort error:

(**)
 Lemma IsSome0_extract0 : forall {A : Type} {x : option A} (xS : IsSome0 x) , 
A.
 Proof.
  intros A x Hx.
  induction x.
  (* Case 1 *)
  exact a.
  (* Case 2 *)  
  inversion Hx.
(**)

 | Toplevel input, characters 0-12:
 | Error: Inversion would require case analysis on sort 
 | Type which is not allowed for inductive definition IsSome0.

I guess this is connected to the fact that in gallais' version,
inversion is used in a backwards-reasoning way, establishing the
current goal --- is there a way to use inversion (or something like it)
in a forwards-reasoning way in the proof state like the one here?

  A : Type
  Hx : IsSome None
  ============================
   A



Thanks a lot again!


Wolfram