The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-labs.fr>]

Hi Edsko,

Edsko de Vries a écrit :
> Hi,
>
> If I have an *inductively* defined property, such as
>
> Inductive typeof : Env -> Expr -> AttrType -> FreeVars -> Prop := ...
>
> does that mean that all proofs of "typeof" are finite? Or could there be
> infinite proofs of "typeof", even though typeof is an inductive property?

Yes, all the elements (proofs) of an inductive type are finite objects.


> What I don't know is (a) if there can be infinite proofs of typeof, even
> though typeof is inductive, and (b) if there cannot, how I can express
> that after having applied T_Exchange a number of times, another rule
> must have been applied. 

(a): There are no infinite proofs of the type typeof.
(b) Use the inductive principle on this type, which states exactly that. This 
correspond to the "elim" tactic. The induction principle is the constant called 
typeof_ind. Coq automatically derives this constant for you from the definition 
of the inductive predicate. You may take a look to it by typing "Print typeof_ind".

Cheers,
Eduardo Gimenez.


> If there can be infinite proofs of an inductive property, can I use a
> coinductive proof? (noting that I have very little experience with
> coinduction, so if I'm not making sense here, please excuse me :)
>
> Thanks very much!
>
> Edsko
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
> __________ Information NOD32 2267 (20070515) __________
>
> Ce message a ete verifie par NOD32 Antivirus System.
> http://www.nod32.com