The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

> Salut,
> 
> What is the general way of going about `unfolding lets'? The folowing
> example shows the kind of thing:
> 
> Variable f : nat -> nat*nat.
> Hypothesis H : (n:nat) ((Fst (f n)) = O).
> 
> Goal  let (n,_) = (f O) in (n=O).
> 
> The example I actually have is where f is some complicated thing defined
> elsewhere and I want to move the binding n = Fst (f O) up into the
> assumptions somehow, so that I can work on the body.
> 
> 
> Ewen
> 

Here you have to be aware that "let" is simply a shorthand for Case.
Now, the problem is that doing "Case (f O)" will introduce an
arbirtrary couple, for which hypothesis H is useless.  One method to
make sure one remembers that Fst always returns O on this couple is
to make sure a suitable instance of H is in the scope of the "Case"
command:

Variable f : nat -> nat*nat.
Hypothesis H : (n:nat) ((Fst (f n)) = O).

Goal  let (n,_) = (f O) in (n=O).
Generalize (H O);Case (f O);Simpl;Auto.


Another method, easier to generalize, is to keep the relation between
(f O) and the couple as an equality.  Here is the technique:

Goal  let (n,_) = (f O) in (n=O).
Cut (f O)=(f O);[Pattern -1 (f O);Case (f O);Intros n1 n2 H1|Auto].

Then you get to the following goal, which is quite handy for
all kinds of purposes...

  n1 : nat
  n2 : nat
  H1 : (f O)=(n1,n2)
  ============================
   n1=O

For instance, you can now do:
Rewrite <- H with n:= O;Rewrite H1;Simpl;Auto.


This second method is the one I consider general.

Best regards

Yves