aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-04-22 21:17:05 -0400
committerGravatar Jason Gross <jgross@mit.edu>2019-04-22 21:17:05 -0400
commitecdfd03c636ab63e167fbe4fc4d7ab0ed5d9db74 (patch)
tree8a9d443ec84d11fae082ca9f1cac4a2db2f5cdb2
parentc9ed485e5521c4ebead81d48d66a782b3a46ca4f (diff)
Add some move/transport eq lemmas
-rw-r--r--src/Util/Equality.v14
1 files changed, 14 insertions, 0 deletions
diff --git a/src/Util/Equality.v b/src/Util/Equality.v
index 693cc5d7d..f65d73338 100644
--- a/src/Util/Equality.v
+++ b/src/Util/Equality.v
@@ -162,3 +162,17 @@ Proof. cbv [pointwise_relation]; intros; subst; trivial. Qed.
Lemma push_rew_fun_dep A P Q a b (pf : a = b) f x
: (rew [fun x : A => P x -> Q x] pf in f) x = (rew [Q] pf in (f (rew <- [P] pf in x))).
Proof. subst; reflexivity. Defined.
+
+Lemma rew_r_moveL A P x y (pf : x = y :> A) a b
+ : (rew [P] pf in a) = b -> a = (rew <- [P] pf in b).
+Proof. subst; exact id. Defined.
+Lemma rew_moveL A P x y (pf : x = y :> A) a b
+ : (rew <- [P] pf in a) = b -> a = (rew [P] pf in b).
+Proof. subst; exact id. Defined.
+
+Lemma rew_moveR A P x y (pf : x = y :> A) a b
+ : a = (rew <- [P] pf in b) -> (rew [P] pf in a) = b.
+Proof. subst; exact id. Defined.
+Lemma rew_r_moveR A P x y (pf : x = y :> A) a b
+ : a = (rew [P] pf in b) -> (rew <- [P] pf in a) = b.
+Proof. subst; exact id. Defined.