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: coq-club AT inria.fr
Subject: Re: [Coq-Club] setoid rewriting, partial application and relfexivity
Date: Thu, 16 Feb 2017 18:25:46 -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-wm0-f47.google.com
Ironport-phdr: 9a23:gbumUhDCmPwiWXKuShC6UyQJP3N1i/DPJgcQr6AfoPdwSP39ocbcNUDSrc9gkEXOFd2CrakV1qyO7uu9ACRAuc/H6y9SNsQUFlcssoY/oU8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUt2as8Pi3OervpbXfg9ghTynYLo0Ig/lgx/Ws5woiIdjL+4Dwx/IvHIAL/pEzGdpO1u7lBPhoMq84cgwoGxrp/s9+psYAu3BdKMiQOkAAQ==

Of course, R must be reflexive. But adding:

Instance R_reflexive: Reflexive R. Admitted.

Does not help either.

Vadim

CMU ECE PhD candidate

Mobile: +1(510)220-1060

On Thu, Feb 16, 2017 at 6:15 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

If there is any reason the example below shouldn't work?
I was thinking that `partial_application_tactic` and
`eq_proper_proxy` applied by setoid_rewrite should do the trick.

Require Import Relations Setoid Morphisms.

Parameter Foo: Type.
Parameter R: relation Foo.
Parameter bar: Foo -> Foo -> Foo.

Instance bar_proper: Proper ((R) ==> (R) ==> (R)) (bar). Admitted.

Example ex1 (a b c: Foo):
R a b -> R (bar c a) (bar c b).
Proof.
intros H.
setoid_rewrite H.
Qed.

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060

[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