From 40c7ffa60a077040ad741bc1a68bb4679efe4475 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 23 Jan 2017 20:42:54 -0500 Subject: Add match commutation lemmas --- src/Util/Equality.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'src/Util') 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. -- cgit v1.2.3