The Coq mailing list

["Harley D. Eades III" <harley.eades AT gmail.com>]

Hi, Auger.

Thanks a lot for your detailed response.

You explanations have helped a lot!

Thanks,
Harley

On Dec 15, 2012, at 4:50 AM, AUGER Cédric 
<sedrikov AT gmail.com>
 wrote:

> 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.
>