coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to prove an inductive property on trees.

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to prove an inductive property on trees.
Date: Sun, 7 Feb 2016 16:56:31 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing.csail.mit.edu
Ironport-phdr: 9a23:/kRe5BQGAWHIiLYyVVtkHF59A9psv+yvbD5Q0YIujvd0So/mwa64ZxyN2/xhgRfzUJnB7Loc0qyN4/+mAzFLuMva+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8KVOVgD3WfmKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7uXqswPCRE2B/CgySGITxzNECg2NxxH+X4/4tiKy4uNx0SyRFcbtRLEwHzGj8+FmRAK+23RPDCIw7GyC0p84t6lcuh/0/xE=

I do think my one-line reference to a section of CPDT almost covers the same material, perhaps with a less fancy example. ;-)

On 02/07/2016 03:59 PM, Dominique Larchey-Wendling wrote:

Dear Benoit,

(* sorry for the duplicate but this is the complete answer, I did

send the first one too early ... *)

[Coq-Club] How to prove an inductive property on trees., Benoît Viguier, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Adam Chlipala, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Dominique Larchey-Wendling, 02/07/2016
  - Re: [Coq-Club] How to prove an inductive property on trees., Dominique Larchey-Wendling, 02/07/2016
    - Re: [Coq-Club] How to prove an inductive property on trees., Adam Chlipala, 02/07/2016
      - Re: [Coq-Club] How to prove an inductive property on trees., Dominique Larchey-Wendling, 02/07/2016
    - Re: [Coq-Club] How to prove an inductive property on trees., Frédéric Blanqui, 02/09/2016