The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi Adam,

My first guess would have been to follow closely
the function's definition with something like:

[pose (res := f n) ; destruct res ; simpl]

and it turns out to work:

====================
Theorem rKFix:
forall(n: nat)(myR:R),
Some myR=rK n->data myR=n.
Proof.
intros n myR ; unfold rK ;
pose (res := f n) ; destruct res ;
simpl ; intro H ; inversion H ; reflexivity.
Qed.
====================

Is your approach more robust if we end up changing
rK's definition or is it more or less equivalent (I'm guessing
that pattern & pose do the same job here).

--
gallais



On 17 July 2011 15:20, Adam Chlipala 
<adam AT chlipala.net>
 wrote:
> 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.
>
>