The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

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?

The reason I ask is that one of my rules for typeof is

  | T_Exchange : forall (G G':Env) (e:Expr) (T:AttrType) (fv fv':FreeVars),
        typeof (G ++ G') e T (fv ++ fv') -> typeof (G' ++ G) e T (fv' ++ fv)

(This rule allows you to swap the hypotheses in the typing environment;
I need explicitly encode this rule, as I am working with a substructural
type system). 

Now, when I try to prove that some term "t" does *not* have a particular
type "T" (that there does not exist a proof that term "t" has type "T"),
I need to consider all possible proofs that term "t" has type "T". So, I
assume that there is such a proof, and basically apply the inversion
rule as many times as I need until I get a contradiction (which will
then be discharged by one final application of inversion). 

The problem is that T_Exchange does not reduce the size of any of the
arguments to typeof in any way, and can thus be applied as often as one
likes. I know that in all *finite* proofs, at *some* point after having
applied T_Exchange a number of times another rule must be applied, which
will lead to contradiction. 

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. 

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