The Coq mailing list

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

... in particular, I can't do something like

Fixpoint permute_term : Permute Term

because then now the fixpoint does not have any arguments; similar attempts using Program Fixpoint don't work either. Of course, I can define this like

Instance permute_term : Permute Term := fix ... 

but still I cannot use permute in the body (it complains that no instance of Permute Term is known). The work around is the same as for the inductive definitions, I now have whole slews of lemmas of the form

permute p (pair t u) = pair (permute p t) (permute p u)

but it's tedious to write these and they make the proof script rather large.

Edsko

On Fri, Jan 6, 2012 at 1:37 PM, Edsko de Vries <edskodevries AT gmail.com> wrote:

In this particular case, where [LC] is a definitional type class, you can directly write:

Class LC T := 

  lc : T -> Prop .

Inductive term := pair (t u : term) | atom.

Inductive LC_term : LC term :=

  LC_term1 t u : lc t -> lc u -> lc (pair t u).

This is because [LC term] unfolds to the arity [term -> Prop] and 

constructors are typechecked in a context where [LC_term : LC term]

so you have your recursive instance available.

You get your induction principle for free:

About LC_term_ind.

(*

LC_term_ind :

∀ P : term → Prop,

(∀ t u : term, lc t → P t → lc u → P u → P (pair t u))

→ (∀ t : term, LC_term t → P t)

*)

You then just have to add: [Existing Instance LC_term] to register it,

Ah, that certainly makes it a lot cleaner, thanks! Is it possible to do something similar for recursive functions? Say,

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

and then use permute in recursive calls?

Edsko