The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

Ok, I have updated the rest of my proofs, and your suggestion works beautifully. You sir are a genius :)

So to wrap up: given a class

Class LC (T : Type) := 
  lc : T -> Prop.

I follow Matthieu's suggestion and define instances this way:

Inductive lc_SrcTerm : LC SrcTerm :=
  | lc_S_Nil   : lc S_Nil
  | lc_S_Pre   : forall n P, lc n -> lc P -> lc (S_Pre n P)
  | lc_S_Par   : forall P Q, lc P -> lc Q -> lc (S_Par P Q)
  | lc_S_Res   : forall L P, (forall x, x \notin L -> lc (P ^^ x)) -> lc (S_Res P)
  | lc_S_Trans : forall L P Q, (forall x, x \notin L -> lc (P ^^ x)) -> lc Q -> lc (S_Trans P Q)
  | lc_S_Co    : forall n, lc n -> lc (S_Co n)
  | lc_S_Rec   : forall L P, (forall x, x \notin L -> lc (P ^^ x)) -> lc (S_Rec P)
  | lc_S_PVar  : forall n, lc n -> lc (S_PVar n).
Existing Instance lc_SrcTerm.

where we can use lc in the recursive hypothesis (directly); and given a 

Class Permute T := 
  permute : Permutation -> T -> T.

I follow Robbert's suggestion and define instances like

Instance permute_SrcTerm : Permute SrcTerm := fix permute_SrcTerm p t := 
  let rec := @permute _ permute_SrcTerm in
  match t with
  | S_Nil       => S_Nil
  | S_Pre n P   => S_Pre (permute p n) (rec p P)
  | S_Par P Q   => S_Par (rec p P) (rec p Q)
  | S_Res P     => S_Res (rec p P)
  | S_Trans P Q => S_Trans (rec p P) (rec p Q)
  | S_Co n      => S_Co (permute p n)
  | S_Rec P     => S_Rec (rec p P)
  | S_PVar n    => S_PVar (permute p n)
  end.

This means that all recursive occurrences are in terms of the type classes, rather than their instances, which greatly improves proof automation. Nice :)

Thanks!

Edsko