The Coq mailing list

[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

Attachment: AaronTime.v
Description: Binary data