Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to simplify / compute with a recursive "Function" definition

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to simplify / compute with a recursive "Function" definition


Chronological Thread 
  • From: Washington Ribeiro <wtonribeiro AT gmail.com>
  • To: coq-club AT inria.fr, pierre.courtieu AT gmail.com, mattam AT mattam.org
  • Subject: Re: [Coq-Club] How to simplify / compute with a recursive "Function" definition
  • Date: Mon, 7 Sep 2015 14:48:42 -0300
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=wtonribeiro AT gmail.com; spf=Pass smtp.mailfrom=wtonribeiro AT gmail.com; spf=None smtp.helo=postmaster AT mail-yk0-f170.google.com
  • Ironport-phdr: 9a23:fyGoLRMr+tmKdSebNQ8l6mtUPXoX/o7sNwtQ0KIMzox0KPX6rarrMEGX3/hxlliBBdydsKIYzbOO+Pm5BiQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTrkbnqsMSKPE1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOHBROO62EGXyMdlQdSHwnI8Tn1W57wtm3xse85kCyTIdH/SJgxUCi+5qItTwXn2wkdMDtsz2jMis12g75cplqbphZywpTTKNWKKP14ZKLXcNIAQkJOW89QU2pKBYbqPNhHNPYIIesN99q1nFAJtxbrXQQ=

Dears,

The rewrite just have worked! Thank you so much!

Best,
Washington

2015-09-07 13:00 GMT-03:00 Pierre Courtieu <pierre.courtieu AT gmail.com>:
Indeed this is generally the way to do things with well founded
recursive functions defined with Function.

Can you give the complete code of your problem please?

Best regards,
Pierre

2015-09-07 17:37 GMT+02:00 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




Archive powered by MHonArc 2.6.18.

Top of Page