The Coq mailing list

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