diff options
author | Jason Gross <jgross@mit.edu> | 2017-01-23 20:42:54 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-01-23 20:42:54 -0500 |
commit | 40c7ffa60a077040ad741bc1a68bb4679efe4475 (patch) | |
tree | 7f7c6de7544fca6a8a8084e241d58e51c094bdc6 /src/Util | |
parent | 9f4e0d61abb3dd65943cc8242a4c7b0556d42757 (diff) |
Add match commutation lemmas
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Equality.v | 16 |
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. |