The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sat, 15 Dec 2012 00:41:56 +0100,
AUGER Cédric 
<sedrikov AT gmail.com>
 a écrit :

Sorry, it seems my file exceeded the size limit.
See www.sedrikov.fr/hered_subst.v to retrieve the file.

> Le Fri, 14 Dec 2012 11:57:35 -0600,
> "Harley D. Eades III" 
> <harley.eades AT gmail.com>
>  a écrit :
> 
> > Hi, Adam.
> > 
> > On Dec 14, 2012, at 10:41 AM, Adam Chlipala 
> > <adamc AT csail.mit.edu>
> > wrote:
> > 
> > > On 12/14/2012 10:33 AM, Harley D. Eades III wrote:
> > >> A while ago I formalized some of my research on the hereditary
> > >> substitution function in Coq.  At first I tried to define the
> > >> function in Set using Program Fixpoint and the wf annotation.  I
> > >> was able to define the function and satisfy all the obligations.
> > >> However, I can't compute with it.  Even worse the subgoals
> > >> generated are huge.  They are over 1000 lines long. 
> > > 
> > > Chapter 7 of CPDT <http://adam.chlipala.net/cpdt/> may be of
> > > interest.  It surveys a variety of techniques for general
> > > recursion in Coq (not including Program, which I've never gotten
> > > into, partly because of the issues you mention).
> > Thanks for a lot for your feedback.
> > 
> > I take a look at Chap. 7.
> > 
> > Harley
> > 
> > 
> 
> I rewrote some parts of your file here. I won't enumerata all
> differences, use a tool like 'diff' to get them all.
> 
> Some of my modifications may simplify parts of your proofs, I did not
> inspect all.
> 
> Some general points:
> 
> → when defining an inductive, take care of indices vs parameters.
>   You can always make all indices, but that will make proofs harder to
>   do.
> 
>   Inductive eq : ∀ (A : Type), A → A → Prop :=
>   | eq_refl : ∀ A x, eq A x x.
> 
>   and
> 
>   Inductive eq (A : Type) (x : A) : A → Prop :=
>   | eq_refl : eq A x x.
> 
>   Are "almost" the same stuff (in fact you can show that these
>   definitions are equivalent). First definition uses indices only and
>   is harder to use than second definition. It is not too much annoying
>   when there is no recursion, but when recursion is involved, it can
> be really painful, as you need to generalize correctly all variables.
> 
> → When using induction with "Acc" predicate, you need a proof of
>   "∀ x, Acc R x" (in your case, your "lex_wf" lemma). But to correctly
>   reduce it, you need parts of this proof to be transparent. That is
>   why your application didn't reduced. The part involving the proofs
>   themselves and not the recursion can (should) be abstracted to avoid
>   pollution.