Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Dealing with lets

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Dealing with lets


chronological Thread 
  • From: Benjamin Pierce <bcpierce AT cis.upenn.edu>
  • To: St�phane Lescuyer <stephane.lescuyer AT inria.fr>
  • Cc: Coq Club <coq-club AT pauillac.inria.fr>, Martin Hofmann <mhofmann AT tcs.ifi.lmu.de>
  • Subject: Re: [Coq-Club] Dealing with lets
  • Date: Mon, 10 Aug 2009 21:48:40 -0400
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Thanks to everybody for the suggestions! Gregory's variant worked well for us...

   - Benjamin


On Aug 6, 2009, at 12:18 AM, Stéphane Lescuyer wrote:

Hi Benjamin,

There's no magic trick unfortunately, and when you destruct something
other than a variable, you lose the information of what it was equal
to in the first place. There are only 2 ways to proceed which
correspond to Yves' two methods : you either make sure that you have
stated everything you needed to know about the term, say [t], before
you destroy it, or you prove an equality linking [t] to its destructed
form once and for all. The second method actually happens to be a
particular case of the first one. Now there are several ways you might
apply either method, and as often with Coq, it is rather a matter of
taste than good vs bad practice.

For the first method, assert whatever facts you need on [t] using
[cut], [assert] or [generalize], and then destruct accordingly.
[generalize] seems less verbose, but when you want to name your new
assertions, 1-line asserts are actually shorter and imo, somewhat more
elegant. In your case, you could end up with the following script,
which doesnt look too bad :

Lemma compose_is_good :
forall f g,
good f -> good g -> good (compose f g).
Proof.
intros f g Hf Hg a; unfold good, compose in *.
assert (Hfa := Hf a); clear Hf; destruct (f a) as [? y].
assert (Hgy := Hg y); clear Hg; destruct (g y).
intuition omega.
Qed.

As a side remark, these kind of purely administrative manipulations
(generalizations, destructions, naming, clears ...) are made less
painful by SSReflect.

For the second method, the complicated script give by Yves in his
reply has actually been made into a tactic in the meanwhile, so it's
easier to use now. [remember t as z] will replace all occurrences of
[t] by [z] in your context and also asser the equality [t = z]. Once
you have such an equality, you can destroy [z] and proceed safely. An
alternative is to use [case_eq t] which destructs [t] by giving you
the equation (but does not replace [t] in the hypotheses). The
following scripts follow in that order :

Lemma compose_is_good' :
 forall f g,
 good f -> good g -> good (compose f g).
Proof.
intros f g Hf Hg a; unfold good, compose in *.
remember (f a) as p; destruct p.
remember (g n0) as p'; destruct p'.
generalize (Hf a) (Hg n0); rewrite <- Heqp, <- Heqp'.
intuition omega.
Qed.

Lemma compose_is_good'' :
 forall f g,
 good f -> good g -> good (compose f g).
Proof.
 intros f g Hf Hg a; unfold good, compose in *.
 case_eq (f a); intros; case_eq (g n0); intros.
 generalize (Hf a) (Hg n0); rewrite H, H0.
 intuition omega.
Qed.

Note that in both cases, using the generated equation when
instantiating your hypothese is not particularly convenient, since
you're basically down to generalizing and rewriting (and [remember]
writes the equation the 'wrong way' for some reason !), so it's not
easier than the first method.

So far it's not really satisfactory, and it's not actually due to the
lets per se, but to the fact that the [good] states a property on
structured data (pair) by using its projections. Even if you write
[good] without lets, using [fst] and [snd] repeatedly instead, you
will end up with the same scripts as above, where rewriting steps are
replaced by conversion. Moreover, the problem does not lie with the
lets and destruction in compose, but in those you are using in your
specifications only. If you are not satisfied with that situation, you
can try changing your specification in such a way that it does not use
projections though, for instance by adding the destruction equality as
an hypothesis of [good] :

Definition good1 (f : nat->(nat*nat)) :=
forall a x y, f a = (x, y) -> x < y /\ a < x.

This may seem as an unnecessary tricky version of the first
specification, but it has the advantage that you can pass the
equations generated by [case_eq] directly to your [good] hypotheseses
which mean you dont need the generalization and rewriting at the end,
as with the 2nd method. Here is the script :

Lemma compose_is_good1 :
 forall f g,
 good1 f -> good1 g -> good1 (compose f g).
Proof.
 intros f g Hf Hg a x y; unfold good1, compose in *.
 case_eq (f a); intros ? v E'; destruct (Hf _ _ _ E').
 case_eq (g v); intros ? ? E''; destruct (Hg _ _ _ E'').
 intro I; inversion I; subst; intuition omega.
Qed.

The script is not much shorter, but the example is really easy and
this trick can be used in situations where it really makes a huge
difference. There remains two issues : one needs to manually destruct
using [case_eq] or [remember ...; destruct], and the inversion step at
the end is also an artifact of the equality in the specification. We
can still get rid of these by keeping the general idea but using
inductives, and this is a quite powerful method. We write an inductive
"view" of the specification involving the pair, in the following way :

Inductive good_aux : nat -> (nat * nat) -> Prop :=
| good_aux_1 : forall a x y, a < x -> x < y -> good_aux a (x,y).
Definition good2 f := forall a, good_aux a (f a).

The inductive [good_aux] is a convenient way of expressing what we did
above, because it makes the two projections [x] and [y] somewhat
implicit, and the equality as well. If you have an hypothesis [H :
good_aux a (f a)] in your context, destructing it will make Coq
introduce the two variables for you, replace [f a] by [(x, y)] in the
whole context, and will put the other hypotheses on the stack. This
makes it very easy to reason with, and here is the script :

Lemma compose_is_good2 :
 forall f g,
 good2 f -> good2 g -> good2 (compose f g).
Proof.
 intros f g Hf Hg a; unfold good2, compose in *.
 destruct (Hf a); destruct (Hg y); constructor; omega.
Qed.

which is by far the easiest and shortest of all. This comes at the
cost of the readability of the specification maybe, but it is
convenient enough that I really seldom use propositions for my
specifications and use inductives instead.

Thats it, sorry for the very longish response, but I tried to be as
exhaustive as possible since different cases may require different
solutions.
Hope this helps,

Stéphane

--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06

On Thu, Aug 6, 2009 at 4:22 AM, 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




--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06






Archive powered by MhonArc 2.6.16.

Top of Page