coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Help with a proof
Date: Thu, 16 Jun 2016 11:04:01 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f43.google.com
Ironport-phdr: 9a23:ukp5vxPAOMNV+/IWlsYl6mtUPXoX/o7sNwtQ0KIMzox0KPv8rarrMEGX3/hxlliBBdydsKIVzbqG+Pi8EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35Xxh7D5o8GbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoJvvRNWqTifqk+UacQTHF/azh0t4XXskzoShLHzX8BWC1CmR1RRgPB8RvSX5HrsyK8uPAriweAOsijdbE5Qy6vp4xsVQX0iSoaf2oh8WzNkME2h6VGug6gqgFXzIvdYYXTP/17KPCONegGTHZMC54CHxdKBZmxOs5WV7IM

Hi,

2016-06-16 8:41 GMT+02:00 Pierre Casteran <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.

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

[Coq-Club] Help with a proof, Vincent Archambault-Bouffard, 06/16/2016
- Re: [Coq-Club] Help with a proof, Pierre Casteran, 06/16/2016
  - Re: [Coq-Club] Help with a proof, Pierre Courtieu, 06/16/2016
    - Re: [Coq-Club] Help with a proof, Pierre Casteran, 06/16/2016
      - Re: [Coq-Club] Help with a proof, Pierre Courtieu, 06/16/2016
  - Re: [Coq-Club] Help with a proof, Vincent Archambault-Bouffard, 06/16/2016