Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade
Created January 17, 2023 18:34
Show Gist options
  • Save Blaisorblade/f8928e791dfd19c8df18c10679e51bd1 to your computer and use it in GitHub Desktop.
Save Blaisorblade/f8928e791dfd19c8df18c10679e51bd1 to your computer and use it in GitHub Desktop.
(*
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment