coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Applying Lemma in fold_left

From: "John Wiegley" <johnw AT newartisans.com>
To: "Soegtrop\, Michael" <michael.soegtrop AT intel.com>
Cc: "coq-club\@inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Applying Lemma in fold_left
Date: Sun, 21 Aug 2016 12:52:53 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pa0-f53.google.com
Ironport-phdr: 9a23:7Df8eRXgbFJxQf48zwtRwC11ypbV8LGtZVwlr6E/grcLSJyIuqrYZxWEt8tkgFKBZ4jH8fUM07OQ6PG5HzZRqs/a4DhCKMUKDE5dz51O3kQJO42sMQXDNvnkbig3ToxpdWRO2DWFC3VTA9v0fFbIo3e/vnY4ExT7MhdpdKyuQtaBx/q+2+36wZDPeQIA3GP7OuIrak/n5lyK5oFW2dIkcfdpjEOR4zNhQKd//StQP1WdnhLxtI+b3aVI1GBugc8n7NNKSq7gfq41HvRyBTUiNH0ptoWw7UGQBSPG3HYXU30XnxxUGECFqUiiBtai+hf946BG3ySVIdfxVYRwERGj5KdiRRuiwHMCNjU5+WzTzNd3ga1HuhW5jx1534PQJoqSMawtULnaeIZQZ21BWI5uViFOBo6tJcNbDe0BO/lwqYTirkESrAC3AxLqD+TqnGwbzkTq1LE3hrxyWTrN2xYtSpdX6CzZ
Organization: New Artisans LLC

>>>>> "SM" == Soegtrop, Michael
>>>>> <michael.soegtrop AT intel.com>
>>>>> writes:

SM> I am myself still struggling with the concepts of this, so I took this as
SM> an exercise. Maybe one of the experts can review my comments /
SM> explanations of the required “Proper term”.

What you wrote is correct, but the relation doesn't need to be eq, or even an
Equivalence. You can build up a rewriting library on terms that only relate by
reflexivity and transitivity, for example.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] Applying Lemma in fold_left, Durjay Chowdhury, 08/15/2016
- Re: [Coq-Club] Applying Lemma in fold_left, Laurent Thery, 08/21/2016
- RE: [Coq-Club] Applying Lemma in fold_left, Soegtrop, Michael, 08/21/2016
  - Re: [Coq-Club] Applying Lemma in fold_left, John Wiegley, 08/21/2016