The Coq mailing list

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

Hah, very clever! That seems to do the trick, at least based on some simple tests. Let me see if I can simplify my proof now..

Thanks!

Edsko

On Tue, Jan 10, 2012 at 5:03 PM, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

On 01/10/2012 04:26 PM, Edsko de Vries wrote:

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

Does the following help you out?

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

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

Definition permute_list {A} : Permute A  (list A) :=
 fix aux (p : Permutation A) (l : list A) :=

   match l with
     | nil => nil

     | cons a l => cons (p a) (@permute _ _ aux p l)
   end.
Existing Instance permute_list.

Here I give the Permute instance by hand.