The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

True, a bug I will report.

P.

2016-06-16 11:11 GMT+02:00 Pierre Casteran <pierre.casteran AT labri.fr>:

Le 16/06/2016 11:04, Pierre Courtieu a écrit :

Hi,

2016-06-16 8:41 GMT+02:00 Pierre Casteran <pierre.casteran AT labri.fr
<mailto:pierre.casteran AT labri.fr>>:


    Then, using the automatically generated induction principle
    compose'_ind, you get a rewriting lemma.

      Lemma compose'_rw :


Actually this lemma is also automatically generated by Function, it is
called compose'_equation.

Hi, Pierre.

 That's right, but (at least in Coq 8.5pl1) compose'_equation is generated, but doesn't appear in the list of automatically generated
lemmas:

compose'_tcc is defined

compose'_terminate is defined

compose'_ind is defined

compose'_rec is defined

compose'_rect is defined

R_compose'_correct is defined

R_compose'_complete is defined

This why I proved it by hand :-)

Pierre

Note that:

1) "Function" does not support dependent types or higher order functions,
2) "Program Fixpoint" does support those but provides less automatically
generated stuff (_ind _equation etc).

P.