aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-01-23 20:42:54 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-01-23 20:42:54 -0500
commit40c7ffa60a077040ad741bc1a68bb4679efe4475 (patch)
tree7f7c6de7544fca6a8a8084e241d58e51c094bdc6 /src/Util
parent9f4e0d61abb3dd65943cc8242a4c7b0556d42757 (diff)
Add match commutation lemmas
Diffstat (limited to 'src/Util')
-rw-r--r--src/Util/Equality.v16
1 files changed, 16 insertions, 0 deletions
diff --git a/src/Util/Equality.v b/src/Util/Equality.v
index b7bce062d..81c94d871 100644
--- a/src/Util/Equality.v
+++ b/src/Util/Equality.v
@@ -122,3 +122,19 @@ Lemma commute_eq_rect {A} (P Q : A -> Type) (f : forall a, P a -> Q a) a b (H :
: f b (eq_rect _ P v _ H)
= eq_rect _ Q (f a v) _ H.
Proof. destruct H; reflexivity. Defined.
+
+Lemma commute_eq_match {A} (P Q : A -> Type) (f : forall a, P a -> Q a) a b (H : a = b :> A)
+ (v : P a)
+ : f b (match H in _ = y return P y with eq_refl => v end)
+ = (match H in _ = y return Q y with eq_refl => f a v end).
+Proof. destruct H; reflexivity. Defined.
+Lemma commute_eq_match2 {A} (P1 P2 Q : A -> Type) (f : forall a, P1 a -> P2 a -> Q a) a b (H : a = b :> A)
+ (v1 : P1 a) (v2 : P2 a)
+ : f b
+ (match H in _ = y return P1 y with eq_refl => v1 end)
+ (match H in _ = y return P2 y with eq_refl => v2 end)
+ = (match H in _ = y return Q y with eq_refl => f a v1 v2 end).
+Proof. destruct H; reflexivity. Defined.
+Lemma eq_match_const {A P x y} (p : x = y :> A) k
+ : match p return P with eq_refl => k end = k.
+Proof. case p; reflexivity. Defined.