The Coq mailing list

[Nicolas Oury <Nicolas.Oury AT ed.ac.uk>]

Dear all,


Le 22 juin 09 à 13:08, Lionel Elie Mamane a écrit :

> > I believe they are added as axioms every time an inductive data type
> > is declared.
>
> That is not correct. They are just automatically generated
> definitions. They are as much axioms as proofs generated with "auto."
> :)
I am not sure I agree.  I am not really a specialist of this point so  
I may be completly wrong.
But it seems to me that the generated proofs relie on a fixpoint  
construct that is
somehow specialised to the inductive family it works on.

These constructs are equiped with typing rules and elimination  
behaviour that depends on
the inductive family.
The justification of these new rules is somehow made at a meta level  
and uses some
exterior criterias: strict positivity and structural guardedness.

CIC includes a family of such typing/reduction rules for any  
acceptable inductive definitions.
In the link you sent, the typing rule for match is given
"[...] provided I is an inductive type in a declaration Ind(Δ)[r] 
(ΓI:=ΓC ) with
ΓC = [c1:C1;…;cn:Cn] and cp1…cpl are the only constructors of I."

This is not really different from adding new eliminators and reduction  
rules for eliminators.

To try to answer Neil's questions:

1. I think the functors has to be strictly positive.
2. The fact that it is correct to add new typing/reduction rules for  
each defined strictly positive inductive family is justified
in at least two places:
- Benjamin Werner's PhD.
- Bruno Barras's Phd proves properties CIC in Coq itself.

Best regards,

Nicolas


--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.