The Coq mailing list

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

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
>