coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] setoid rewriting, partial application and relfexivity

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: Vadim Zaliva <vzaliva AT cmu.edu>, coq-club AT inria.fr
Subject: Re: [Coq-Club] setoid rewriting, partial application and relfexivity
Date: Fri, 17 Feb 2017 15:24:32 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wr0-f173.google.com
Ironport-phdr: 9a23:Yq48kxeMWv5o+jc7zntNp5DalGMj4u6mDksu8pMizoh2WeGdxc2zbB7h7PlgxGXEQZ/co6odzbGH7ua4BidZuN7B6ClEK8McEUddyI0/pE8JPo2sMQXDNvnkbig3ToxpdWRO2DWFC3VTA9v0fFbIo3e/vnY4ExT7MhdpdKyuQtaBx5f/6+fnxZTfYgAAtjO5YK17ZEGovwzVt9cfqYBnN+A8xgaf5jNDfP0Tzmd1L3qSmQz974G+5s1N6SNV7swo+89FGZfze6UmRPQMEiYvN2Er7eXgsASFQAeSsChPGl4KmwZFVlCWpCrxWY3853P3

But it does not need to be transitive:

Example ex1 (a b c: Foo):

R a b -> R (bar c a) (bar c b).

Proof.

intros H.

apply bar_proper.

reflexivity.

apply H.

Qed.

Sounds like an unnecessary constraint.

CMU ECE PhD candidate

Mobile: +1(510)220-1060

On Thu, Feb 16, 2017 at 11:05 PM, John Wiegley <johnw AT newartisans.com> wrote:

>>>>> "VZ" == Vadim Zaliva <vzaliva AT cmu.edu> writes:

VZ> Of course, R must be reflexive. But adding:

VZ> Instance R_reflexive: Reflexive R. Admitted.

VZ> Does not help either.

Turns out you need Transitive also.

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

[Coq-Club] setoid rewriting, partial application and relfexivity, Vadim Zaliva, 02/17/2017
- Re: [Coq-Club] setoid rewriting, partial application and relfexivity, Vadim Zaliva, 02/17/2017
  - Re: [Coq-Club] setoid rewriting, partial application and relfexivity, John Wiegley, 02/17/2017
    - Re: [Coq-Club] setoid rewriting, partial application and relfexivity, Vadim Zaliva, 02/18/2017
      - [Coq-Club] Question about maximum operation for universe levels in Coq, Erik Palmgren, 02/21/2017
        
        Re: [Coq-Club] Question about maximum operation for universe levels in Coq, Bas Spitters, 02/22/2017