Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Equality for inductive type containing list

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Equality for inductive type containing list


Chronological Thread 
  • From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Equality for inductive type containing list
  • Date: Thu, 06 Oct 2016 16:29:58 +0200
  • Organization: LORIA

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




Archive powered by MHonArc 2.6.18.

Top of Page