The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

On 10/06/2016 04:18 PM, Klaus Ostermann wrote:
> Hi Dominque
> 
> thanks a lot! Your solution works like a charm. Very nice!
> 
> That said, I'm fascinated how much work is required to do something
> so basic.
> 
> In general, my impression as a Coq beginner is that is relatively easy to
> follow one of the numerous Coq tutorials and solve the exercises, but
> as soon as you try to do something yourself, you run into many complicated
> pitfalls that the exercise designers have carefully avoided.

This is very true.

I did not know that it was possible to parametrize the decide equality
tactic as Clément showed. Since obviously, decide equality cannot
rely on the Coq generated inductive principle ty_rec (ty_rec is too
weak), it must find one itself.

So I wonder why the nested induction required by the type of trees ty
is still not guessed when Coq generates induction principles.

Dominique