diff options
Diffstat (limited to 'src/Util/Relations.v')
-rw-r--r-- | src/Util/Relations.v | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/src/Util/Relations.v b/src/Util/Relations.v new file mode 100644 index 000000000..aa280db26 --- /dev/null +++ b/src/Util/Relations.v @@ -0,0 +1,29 @@ +Require Import Crypto.Util.FixCoqMistakes. +Require Import Crypto.Util.Logic. +Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. + +Lemma symmetry_iff {T} {R} {Rsym:@Symmetric T R} x y: R x y <-> R y x. + intuition eauto using symmetry. +Qed. + +Lemma and_rewrite_l {A B} {RA RB} {Equivalence_RA:Equivalence RA} {Equivalence_RB:Equivalence RB} + (f:A->B) ref P {Proper_P: Proper (RA==>RB==>iff) P} a + : (RB (f a) ref /\ P a (f a)) <-> (RB (f a) ref /\ P a ref). +Proof. + logic; match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end. +Qed. + +Lemma and_rewriteleft_l {A B} {RA RB} {Equivalence_RA:Equivalence RA} {Equivalence_RB:Equivalence RB} + (f:A->B) ref P {Proper_P: Proper (RA==>RB==>iff) P} a + : (RB ref (f a) /\ P a (f a)) <-> (RB ref (f a) /\ P a ref). +Proof. + logic; match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end. +Qed. + +Lemma exists_and_equiv_r {A} {RA} {Equivalence_RA:Equivalence RA} + P {Proper_P: Proper (RA==>iff) P} (ref:A) + : (exists a, P a /\ RA a ref) <-> P ref. +Proof. + logic; try match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end. + repeat (assumption||reflexivity||econstructor); assumption. (* WHY the last [assumption]?*) +Qed. |