coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Aaron B." <aaron678 AT gmail.com>
- To: AUGER Cedric <Cedric.Auger AT lri.fr>
- Cc: Adam Megacz <megacz AT cs.berkeley.edu>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Re: running out of memory with big proof objects
- Date: Fri, 22 Oct 2010 09:37:53 -0400
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=Dl6zSU5/iDE4CMUzJe1735ARFMUhnLQjEfPZE/9RMFkpp6Vao3OWAP0fX84yYy4sI8 x23QIaKBJZYHxkzNZEj6ff8j1/noLf/W9IAJ4xxXw5YOkrZFk7I3IEY05bmdI2j0N5ri d2oWJRzgbnmhH2hSRK0aAarPc4AUlIhUd8S6s=
Thanks. I find the point in your last comment especially interesting.
- Aaron
On Fri, Oct 22, 2010 at 9:20 AM, AUGER Cedric
<Cedric.Auger AT lri.fr>
wrote:
> Le Thu, 21 Oct 2010 21:40:06 +0000,
> Adam Megacz
>Â <megacz AT cs.berkeley.edu>
> a écrit :
>
>>
>> Aaron Bohannon
>>Â <bohannon AT cis.upenn.edu>
>> writes:
>> > It seems like something must be wrong here. Is there something I
>> > should be using instead of "inversion H; congruence"?
>>
>> If "destruct H" gives you the hypotheses you need (it doesn't always),
>> you might try using it instead of inversion. At least for me it
>> speeds things up dramatically.
>>
>> - a
>>
>
> In my experience, "destruct H." is always better as "inversion H."
> when the dependent parameters of H are all simple variables.
>
>>>>>
> (* first simple comparison between destruct and inversion *)
> Lemma false_is_not_true_1: false = true -> False.
> Proof.
> intro H; inversion H.
> (* I know "discriminate." works, but it simply
> do what I wrote and is almost as long as
> what I have written *)
> Qed.
> Print false_is_not_true_1.
> (*
> false_is_not_true_1 =
> fun H : false = true =>
> let H0 :=
> match H in (_ = y) return (y = true -> False) with
> | refl_equal =>
> fun H0 : false = true =>
> let H1 :=
> eq_ind false (fun e : bool => if e then False else True) I true
> H0 in False_ind False H1
> end in
> H0 (refl_equal true)
> : false = true -> False
> *)
> (* honestly, it is really painfull for me to read it *)
>
> Lemma false_is_not_true_2: false = true -> False.
> Proof.
> assert (CorruptedTrue := I: if true then True else False).
> intro H; destruct H.
> (* now all occurences of "true" are replaced by "false",
> 'corrupting' "CorruptedTrue" *)
> exact CorruptedTrue.
> Qed.
> Print false_is_not_true_2.
> (*
> false_is_not_true_2 =
> let CorruptedTrue := I in
> fun H : false = true =>
> let b := true in
> match H in (_ = y) return ((if y then True else False) -> False) with
> | refl_equal => fun CorruptedTrue0 : False => CorruptedTrue0
> end CorruptedTrue
> : false = true -> False
> *)
> (* I do not pretend it is easy to read, but at least the term
> has not so much pollution in it *)
>
> (* Of course, we need to manually assert a
> "match [destructed dependent parameters] with
> | [possible cases for the destructed dependent parameters] => True
> | [impossible cases for the destructed dependent parameters] =>
> False end",
> that is mainly what the inversion tactic automatically does with
> "fun e : bool => if e then False else True",
> and after having used our pattern matching, eliminate manually
> absurd cases using our assertion;
> once again, inversion does it automatically *)
>
> (* Here is another example *)
>
> (* some dummy inductive for our examples *)
> Inductive Eq_bool: bool -> bool -> Prop :=
> | Eq_true: Eq_bool true true
> | Eq_false: Eq_bool false false.
>
> (* a not very interesting lemma *)
> Lemma X: forall b, Eq_bool b true -> ~false = b.
> Proof.
> intros.
> (*inversion seems smart as only the 1st case of the inductive is
> considered*) inversion H.
> exact false_is_not_true_2.
> Qed.
>
> Print X.
> (*
> X =
> fun (b : bool) (H : Eq_bool b true) =>
> let H0 :=
> match H in (Eq_bool b0 b1) return (b0 = b -> b1 = true -> false <> b)
> with | Eq_true =>
> fun (H0 : true = b) (H1 : true = true) =>
> eq_ind true (fun b0 : bool => true = true -> false <> b0)
> (fun _ : true = true => false_is_not_true_2) b H0 H1
> | Eq_false =>
> fun (H0 : false = b) (H1 : false = true) =>
> eq_ind false (fun b0 : bool => false = true -> false <> b0)
> (fun H2 : false = true =>
> let H3 :=
> eq_ind false (fun e : bool => if e then False else True) I
> true H2 in False_ind (false <> false) H3) b H0 H1
> end in
> H0 (refl_equal b) (refl_equal true)
> : forall b : bool, Eq_bool b true -> false <> b
> *)
> (* the proof is all but readable *)
>
> Lemma Y: forall b, Eq_bool b true -> ~false = b.
> Proof.
> intros.
> (*this example runs using destruct,
> for that, we need to have only variables as dependent parameters *)
> remember true as c.
> (*as "destruct H" will replace all occurences of "b" and "c" with
> first "true" (we'll have to prove "false<>true")
> then "false" (we'll have "Heqc: false=true"),
> that will be OK*)
> destruct H.
> exact false_is_not_true_2.
> now intros _; exact (false_is_not_true_2 Heqc).
> (* we also could have used "destruct (false_is_not_true2 Heqc).",
> but the proof term would have been less readable,
> because of a need to perform type-casting from False with
> "match H return false<>false with end" *)
> Qed.
>
> Print Y.
> (*
> Y =
> fun (b : bool) (H : Eq_bool b true) =>
> let c := true in
> let Heqc := refl_equal c in
> match H in (Eq_bool b0 b1) return (b1 = true -> false <> b0) with
> | Eq_true => fun _ : true = true => false_is_not_true_2
> | Eq_false =>
> fun (Heqc0 : false = true) (_ : false = false) =>
> false_is_not_true_2 Heqc0
> end Heqc
> : forall b : bool, Eq_bool b true -> false <> b
> *)
>
> (* like above, we need an assertion "c = true" to keep trace
> of modification of the value of "c" in the inductive type
> *)
> Goal forall b, Eq_bool b true -> ~false = b.
> intros.
> destruct H.
> intro; discriminate.
> intro.
> (* hard to prove now... *)
> Abort.
>
> (* so, as long as dependent parameters of inductives are simple
> variables, we don't have to keep trace of their value, and
> we can use "destruct" directly instead of "inversion",
> without making proof scripts longer.
>
> That is a reason why I prefer to have
> "f a = b" in my hypothesis than "b = f a";
> in the first case, the dependent parameter is "b", which is
> a simple variable and can be harmlessly replaced everywhere by
> "f a" with a destruct;
> in the second case, the dependent parameter is "f a",
> "destruct" will replace all occurences of "f a" with "b",
> losing the link between "f a" and "b";
> so if somewhere you have an occurence of "g a", or simply "a",
> then you can lose the possibility to prove your lemma.
> Of course I know the "rewrite" tactic, but this tactic is
> mainly an "inversion", so it produces unnecessarily big and
> hardly readable terms; the worst being "rewrite <- H.", which
> can always be directly replaced by "destruct H.", as far as I know.
> (I belive "rewrite <- H." performs a "symmetry in H; rewrite H.")
> *)
>
>
- Re: [Coq-Club] running out of memory with big proof objects, (continued)
- Re: [Coq-Club] running out of memory with big proof objects, Aaron Bohannon
- Re: [Coq-Club] running out of memory with big proof objects,
Jim Apple
- Message not available
- Message not available
- Fwd: [Coq-Club] running out of memory with big proof objects,
Aaron Bohannon
- Re: [Coq-Club] running out of memory with big proof objects,
Stéphane Lescuyer
- Re: [Coq-Club] running out of memory with big proof objects,
Aaron Bohannon
- Re: [Coq-Club] running out of memory with big proof objects, Aaron Bohannon
- Message not available
- Re: [Coq-Club] running out of memory with big proof objects, Stéphane Lescuyer
- Re: [Coq-Club] running out of memory with big proof objects,
Aaron Bohannon
- Re: [Coq-Club] running out of memory with big proof objects,
Stéphane Lescuyer
- Fwd: [Coq-Club] running out of memory with big proof objects,
Aaron Bohannon
- Message not available
- Message not available
- Re: [Coq-Club] running out of memory with big proof objects, Stéphane Lescuyer
- [Coq-Club] Re: running out of memory with big proof objects,
Adam Megacz
- Re: [Coq-Club] Re: running out of memory with big proof objects,
AUGER Cedric
- Re: [Coq-Club] Re: running out of memory with big proof objects, Aaron B.
- Re: [Coq-Club] Re: running out of memory with big proof objects,
AUGER Cedric
Archive powered by MhonArc 2.6.16.