safe_per_rewriting.v

(*
 An answer to https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/rewriting.20with.20PERs.
 Instances PER_valid_l and PER_valid_r are optimized to be safest.
  *)

From Coq Require Import Relations RelationClasses Setoid Morphisms.

Class ByEassumption (P : Prop) := {
  by_eassumption : P
}.
#[global] Arguments by_eassumption : clear implicits.

#[global] Hint Extern 1 (ByEassumption ?P) =>
  constructor;
  (* Other solvers are acceptable here. *)
  eassumption
  : typeclass_instances.

#[export] Instance PER_valid_l {A} {R : relation A} `{!PER R} x y (H : ByEassumption (R x y)) : Proper R x.
Proof.
  apply by_eassumption in H; hnf; etransitivity; eassumption || symmetry; eassumption.
Qed.
#[export] Instance PER_valid_r {A} {R : relation A} `{!PER R} x y (H : ByEassumption (R x y)) : Proper R y.
Proof.
  apply by_eassumption in H; hnf; etransitivity; eassumption || symmetry; eassumption.
Qed.

Lemma test:
   forall (T : Set)  (eqv strict_eqv : relation T)
   (g: T -> T -> bool)  (x x' y : T)
   (H: Equivalence eqv)
   (H0: RelationClasses.PER strict_eqv)
   (H1: RewriteRelation eqv)
   (H2: RewriteRelation strict_eqv)
   (H3:  Proper (eqv ==> strict_eqv ==> @eq bool) g)
   (H4:  strict_eqv y y)
   (H5: eqv x x')
   (H6:  g x y = false),
    g x' y = false.
Proof.
intros.
(* Set Typeclasses Debug. *)
Succeed rewrite H5 in H6.
Abort.