Setoid rewriting with implications

Using Coq
1

Hi!

I just encountered a limitation that I don’t quite understand the justification for, and would like to know more about it.

Boiled down, the problem is rewriting with an implication in a product:

From Coq Require Import Morphisms.
From Coq Require Import Program.

Goal forall (A B C : Prop) (H : A /\ B) (P : B -> C), A /\ C.
  intros.
  setoid_rewrite P in H. (* fails *)

After a bit of a head scratch, and having been able to do this manually by calling Morphisms_Prop.and_impl_morphism, I was wondering whether I could help by folding -> into impl, and indeed, it works:

From Coq Require Import Morphisms.
From Coq Require Import Program.

Goal forall (A B C : Prop) (H : A /\ B) (P : B -> C), A /\ C.
  intros.
  assert (impl B C) as P' by exact P.
  setoid_rewrite P' in H.

What is the reason for this limitation? Is there a known trick to force this rewrite to happen?
It is particularly annoying when P is not a local assumption, but some existing lemma you’d like to rewrite with.

2

That’s indeed unfortunate that setoid_rewrite expects a lemma of the form (forall ..., R x y) and attempts only to rewrite with R rather than the implication relation, but changing this would involve a lot of incompatibilities I suspect. You should be able to use a helper lemma of type to_impl: forall {A B}, (A -> B) -> impl A B to turn an existing lemma into an explicit impl version and rewrite with to_impl (lemma _ .. _) intead.

1 Like