Skip to content

Discrepancy between f_equal and f_equiv on R x x

From stdpp Require Import tactics.

Lemma test_f_equal_refl {A} (x : A) :
  x = x.
Proof. f_equal. Qed.

Lemma test_f_equiv_refl {A} (R : relation A) `{!Equivalence R} x :
  R x x.
Proof.
  Fail f_equiv.
Abort.

Lemma test {A} (R : relation A) `{!Equivalence R} x :
  Proper (R ==> R) (λ _, x).
Proof.
  Fail solve_proper.
  solve_proper_prepare.
  Fail f_equiv. (* R x x, fails similar to above *)
Abort.

The last problem came up in iris!791 (diffs)