The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 10 janv. 2012 à 16:26, Edsko de Vries a écrit :

... 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.

Hi Edsko,

  the only way I see is to add a local alias for the instance, but I'm not sure it 

makes things more workable in the end:

(* Example, makes no computational sense *)

Definition Permutation T := (T -> T).

Class Permute A T := 

  permute : Permutation A -> T -> T.

Fixpoint permute_list {A} (p : Permutation A) (l : list A) : list A := 

  let permute_inst : Permute A (list A) := permute_list in

    match l with

      | nil => nil

      | cons a l => cons (p a) (permute p l)

    end.

Instance plist A : Permute A (list A) := permute_list.

-- Matthieu