The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Marco Servetto wrote:
> I have another problem with  match-returns.
> This time I can provide a very minimal working example.
> Can someone help me in the proof of the last theorem? (nat and bool
> are the standard ones)
>    

Oo, my chance to make up for my confused answer last time! :D

> Definition f (x:nat):= true. (*some complex calculation I do not want
> to unfold ever*)
> Record R:= r{
> data:nat;
> cond: true=f data
> }.
> Definition rK (n:nat):=
> let res:=f n in
> (match res as x return x=res->_ with
>    | true =>  fun p=>  Some (r n p)
>    | false =>fun p=>  None
>   end)(refl_equal res).
> Theorem rKFix:
> forall(n: nat)(myR:R),
> Some myR=rK n->data myR=n.
> Proof.
> ?????
>    

Here's the code, which will probably deserve some stepping-through and 
pondering.  The [pattern] tactic is key to abstracting some uses of [f 
n] but not others, in a way that preserves well-typedness of the goal.

Theorem rKFix: forall (n : nat) (myR : R),
  Some myR = rK n -> data myR=n.
Proof.
  unfold rK; intros n myR.
  generalize (refl_equal (f n)).
  pattern (f n) at -2 -4 -5 -6.
  destruct (f n); simpl; intuition.
  injection H; intros; subst.
  reflexivity.
Qed.