The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

Many thanks for all the answers to our question yesterday!

Now we have another.  :-)

Suppose we start a development like this...

> Definition good (f : nat->(nat*nat)) :=
>   forall a,
>     let (x,y) := f a in
>     x < y /\ a < x.
>
> Definition compose (f g : nat->(nat*nat)) :=
>   fun a =>
>     let (x,y) := f a in
>     let (u,v) := g y in
>     (x,v).
>
> Lemma compose_is_good :
>   forall f g,
>   good f -> good g -> good (compose f g).
> Proof.
>   (* ??? *)

Our attempted proof of the lemma quickly gets tangled up in reasoning  
about the lets, and we are not sure what to do to get through it in a  
nice way.  We found an exchange between Ewen Denney and Yves Bertot  
that addresses this question

   http://logical.saclay.inria.fr/coq-puma/messages/256b3dc43cf87d3b

but we do not see how to use it in a nice way -- all our attempts  
involve quite a bit of cutting and pasting snippets of code at  
multiple places in the proof script.

Can someone steer us in the right direction?

Thanks!!

   - Benjamin and Martin