How to compose setoid_rewrite?

Using Coq
1

Hi,
How can I do the equivalent of

rewrite ?H, ?H2 in *.

but with setoid_rewrite?

1 Like
2

This might be too naive of an answer, but since rewrite falls back to setoid_rewrite if the relation is not equality, the equivalent is the exact same code.

See:

Require Import Setoid.

Goal forall P Q R, (P <-> Q) -> (Q <-> R) -> (Q <-> Q) -> P -> R.
Proof.
  intros P Q R H H0 H1 H2.
  rewrite ?H0, ?H1 in *.
  apply H, H2.
Qed.

Or are you in a situation where the relation has equality deep down and rewrite does not fall back to setoid_rewrite automatically?

3

Thanks for your answer.
Yes due to type classes mismatches I am in a situation where only setoid_rewrite works.