The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Washington,

  you need to use rewriting with the equiv_rec_equation lemma that is generated I think.

Best,

-- Matthieu

On Fri, Sep 4, 2015 at 10:08 PM Washington Ribeiro <wtonribeiro AT gmail.com> wrote:

Dears,

I've defined a function with a specific measure by the "Function" style:

Function equiv_rec (T :  Context * (term * term ))
 {measure size_term_triple} : Prop :=

 match T with
...
 end.

I get a proof of the measure decreasing and so equiv_rec was defined as the adjacent lemmas:

equiv_rec_tcc is defined
equiv_rec_terminate is defined
equiv_rec_ind is defined
equiv_rec_rec is defined
equiv_rec_rect is defined
R_equiv_rec_correct is defined
R_equiv_rec_complete is defined
equiv_rec is defined
equiv_rec_equation is defined

But when I try do apply in the future lemmas some simple tactics like "simpl" or "compute" it doesn't work.

Someone can help me?

Best,

Washington Segundo