From ecdfd03c636ab63e167fbe4fc4d7ab0ed5d9db74 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 22 Apr 2019 21:17:05 -0400 Subject: Add some move/transport eq lemmas --- src/Util/Equality.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'src/Util/Equality.v') 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. -- cgit v1.2.3