The Coq mailing list

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

Well, on second thought, I'm not positive whether the proof is
literally size O(n) or whether the n^2 factor in the proof size is
just immensely smaller...either way, it works great for me.

 - Aaron

2010/10/22 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
>>
>