coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] setoid rewriting, partial application and relfexivity
Date: Thu, 16 Feb 2017 18:15:01 -0800
Authentication-results: mail3-smtp-sop.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-f49.google.com
Ironport-phdr: 9a23:ZZD+yh0Sc5Aa5LBAsmDT+DRfVm0co7zxezQtwd8ZseweLfad9pjvdHbS+e9qxAeQG96KtrQc1qGK7OjJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMhDexe69+IRW5oQjetMQdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LptRRT1iikIKiQ5/XnXhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YAAPAOMvtZr4n4ulABrgGxBQ2tBOPx0DBDm3j73bM70us7FQHG3RIgEMgVvXvIqdX1Kb0eXv6ow6nV1DjOae5d1zTl6IXQcB0sruuAUa9ufcfR00UiFB3Jgk+fpIHhOT6ey/4DvHKB7+V6UOKik24npB91ojio3sosj5PGhoMRylzd+yR5xZo5KcS2SEN0ZdOoCpRQtyadN4t5RsMtXXtktzo9yr0DoZK7fS4Kx4o7xxPHafGKfJKE7g/9WOuROzt1h2xpdKiwihu26USgz/fzVsiw0FZEtCpFldzMu2gT1xPJ98eHS/598l2g2DmV0wDT6/9ELlovmKvVNZEh2aIwmoAPvkTGAy/6glv5g7KLdkk84Oin9/znYqn6pp+bL4J7lgb+Mr03lsOjBeQ4LxMBUnOA+eW80b3j5Vf2TK9Ljv0wiKnZsYrVKd4Vpq6jUEdp1dMo7A/6BDO72vwZm2MGJRRLYkGplY/sbm/HLPH9RcW2h1WymX8/2eLPOrz/C73GK2WFnbv8K+Uuo3VAwRY+mIgMr6lfDasMdar+

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