The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hello,

It's possible that there might be a better way, but a few short tactics makes this more manageable:

Ltac unfold_let E :=
  let a := fresh "x" in let b := fresh "y" in let H := fresh "H" in
  case_eq E; intros a b H; try rewrite H in *.

Ltac unfold_all_lets :=
  repeat match goal with
           | [ |- context [ match ?X with
                              | (_,_) => _
                            end ] ] => unfold_let X
           | [ H : context [ match ?X with
                               | (_,_) => _
                             end ] |- _ ] => unfold_let X
         end.

Lemma compose_is_good :
 forall f g,
 good f -> good g -> good (compose f g).
Proof.
 unfold good, compose; intros.
 unfold_all_lets.

Produces:
  f : nat -> nat * nat
  g : nat -> nat * nat
  H : forall a : nat, let (x, y) := f a in x < y /\ a < x
  H0 : forall a : nat, let (x, y) := g a in x < y /\ a < x
  a : nat
  x : nat
  y : nat
  x0 : nat
  y0 : nat
  y1 : nat
  H1 : (x0, y1) = (x, y)
  H2 : f a = (x0, y0)
  x1 : nat
  H3 : g y0 = (x1, y1)
  ============================
   x < y /\ a < x

at which point specialization and intuition will solve it which is probably more what you could.
You could also automate this part:

 repeat match goal with 
          | [ H  : ?F ?A = _, H' : forall a, _ |- _ ] => 
            specialize (H' A); rewrite H in H'
          | [ H : (_,_) = (_,_) |- _ ] => inversion H; clear H; subst
        end.
 intuition.
Qed.


On Wed, Aug 5, 2009 at 10:22 PM, Benjamin Pierce <bcpierce AT cis.upenn.edu> wrote:
>
> 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
>
>
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
> Â  Â  Â  Â  http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club



--
gregory malecha