The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

Hi Stéphane,

The proof I wanted to complete was actually the property you called
"eq_dec" from (a slight generalization of) your version of the EqDec
class.  I didn't realize that, for record types with n fields, there
would be a proof of size O(n) of this property instead of a proof of
size O(n^2).  One only needs to break down the proof in the proper way
(rather than the more naive way) as your example shows.  This helps
tremendously and is convincing me even more that your overall approach
is correct.

 - Aaron

2010/10/22 Stéphane Lescuyer 
<stephane.lescuyer AT inria.fr>:
> Hi Aaron,
>
> Do not think I am obsessed with sumbool ;-) but you actually do not
> need any inversion lemma at all for the relation [r_equiv] if you
> separate computation and proofs  properly when proving decidability.
>
> There is no magic but simply the fact that if you can characterize
> computationally when you are in the left branch and when you are in
> the right, it allows you to completely factorize the reasoning
> required in these branches. In particular, you only use inversion in
> the right branch but you do the same inversion a great number of
> times.
>
> To illustrate my point, consider you have a function [is_requiv : r ->
> r -> bool] which decides [r_equiv]. The lemma [is_equiv x x' = true ->
> r_equiv x x'] is straightforward by analysis and discrimination, and
> the converse can be proved with "destruct" once instead of inversion:
>
> Lemma is_equiv_false : forall x x', is_equiv x x' = false -> r_equiv x
> x' -> False.
> Proof.
>  intros x x' H E; destruct E; simpl in H.
>  ... (* direct proof by subst/conversion *)
> Qed.
>
> You are actually reasoning by case analysis on the fact that the
> elements are equal instead of case analysis by the elements itself,
> and therefore the proof is super short (smaller than the other lemma
> actually).
>
> I attached a .v file which shows different possibilities and where I
> measured the corresponding proofs sizes. In the file, the number of
> elements in the record are parameterized by a natural integer (in a
> fashion similar to Int31 in the standard library) in order to be able
> to test how  the method scales. Here are some comparisons I obtain in
> this file:
>
> Using sumbool, no abstract, no special inversion lemma:
>  n   Total time    Total size (# of nodes in the AST)
> 8         1.1s          39k
> 16        9s           263k
> 32      141s         1940k
>
> Using sumbool and the special inversion lemma:
>  n   Total time    Total size (# of nodes in the AST)
> 8         0.2s          14k
> 16       1.3s          71k
> 32        12s          410k
>
> Using bool and no inversion lemma:
>  n   Total time    Total size (# of nodes in the AST)
> 8          ~0s         3600
> 16        ~0s         11k
> 32        ~0.1s       38k
>
> I hope this helps, and thank you for giving me that many opportunities
> to criticize sumbool :)
> --
> Stéphane
>
> On Fri, Oct 22, 2010 at 3:35 PM, Aaron Bohannon 
>Â <bohannon AT cis.upenn.edu>
>  wrote:
>> Hi, I didn't realize this message didn't go to the whole list.  In
>> case people are interested, my precise scenario is explained below.
>>
>>  - Aaron
>>
>> ---------- Forwarded message ----------
>> From: Aaron Bohannon 
>>Â <bohannon AT cis.upenn.edu>
>> Date: Thu, Oct 21, 2010 at 12:06 PM
>> Subject: Re: [Coq-Club] running out of memory with big proof objects
>> To: Jean-Francois Monin 
>>Â <jean-francois.monin AT imag.fr>
>> Cc: Jim Apple 
>>Â <coq-club AT jbapple.com>
>>
>>
>> Hi,
>>
>> I began reading your paper, but didn't get far enough to understand
>> how much your technique could help me.  In case you're curious, I'll
>> tell you the general situation.  Consider the following:
>>
>> Record r: Type := build_r { r1: A1; ...; rn: An }.
>>
>> Inductive r_equiv: r -> r -> Prop :=
>>  r_equiv_: forall a1 a1' ... an an',
>>    a1_equiv a1 a1' ->
>>    ...
>>    an_equiv an an' ->
>>    r_equiv r1 r1'.
>>
>> Lemma r_equiv_inv: forall a1 a1' ... an an',
>>  r_equiv_ (build_r a1 ... an) (build_r a1' ... an') ->
>>  (a1_equiv a1 a1') /\ ... /\ (an_equiv an an').
>>
>> Now I want to (roughly speaking) prove another lemma stating that
>> r_equiv is decidable, which requires a n^2 case analysis.  I can
>> either
>> 1) write an Ltac that uses "inversion" at the leaves, without the
>> "abstract" tactical
>> 2) write an Ltac that uses "inversion" at the leaves, using the
>> "abstract" tactical
>> 3) write an Ltac that applies r_equiv_inv instead of using "inversion"
>>
>> My sense of time was off in my first post.  Actually (1) takes about
>> 60s to run the Ltac and another 60s to check the proof term at Qed.
>> (2) takes about 60s to run the Ltac, but just a couple seconds at Qed.
>>  And (3) takes about 20s to run the Ltac and a couple seconds at Qed.
>>
>> I was a little disappointed to find I needed to write out and prove
>> r_equiv_inv simply for performance reasons (but the reason for the
>> performance gain is clear).  I am not sure that constructing a small
>> inversion proof will help me further here, but I am very interested in
>> the paper and would like to look at it more closely.
>>
>>  - Aaron
>>
>> On Wed, Oct 20, 2010 at 11:13 PM, Jean-Francois Monin
>>Â <jean-francois.monin AT imag.fr>
>>  wrote:
>>> Hello,
>>>
>>> Thanks for the advertisement. The technique explained there may
>>> require fine tuning, and I sometimes wonder how it could be useful on
>>> large examples, preferably not my own. This one seems to be a good
>>> candidate. So I would be delighted to know more about it and maybe to
>>> help, if possible.
>>>
>>> Regards,
>>> Jean-Francois
>>>
>>> On Tue, Oct 19, 2010 at 06:15:17PM -0400, Jim Apple wrote:
>>>> You might try "Proof Trick: Small Inversions"
>>>>
>>>> http://hal.inria.fr/inria-00489412/en/
>>>> http://www-verimag.imag.fr/~monin/Proof/SmallInversion/small_inversions.v
>>>>
>>>> On Tue, Oct 19, 2010 at 6:10 PM, Aaron Bohannon 
>>>>Â <bohannon AT cis.upenn.edu>
>>>>  wrote:
>>>> > It seems like something must be wrong here.  Is there something I
>>>> > should be using instead of "inversion H; congruence"?
>>>>
>>>>
>>>>
>>>
>>> --
>>> Jean-Francois Monin
>>> CNRS-LIAMA, Project FORMES  &  Universite de Grenoble 1
>>>
>>> Office 3-605, FIT, Tsinghua University
>>> Haidian District, Beijing 100084, CHINA
>>> Tel: +86 10 62 79 69 79 ext 605
>>> Fax@LIAMA:
>>>  +86 10 6264 7458
>>>
>>
>>
>
>
>
> --
> I'm the kind of guy that until it happens, I won't worry about it. -
> R.H. RoY05, MVP06
>