From 39431e210dc35b188c59025a6eb266f11431c7f6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 21 Oct 2016 18:13:27 -0400 Subject: Add Bool lemmas about if statements --- src/Util/Bool.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Util/Bool.v') diff --git a/src/Util/Bool.v b/src/Util/Bool.v index 5293268df..7b94c503e 100644 --- a/src/Util/Bool.v +++ b/src/Util/Bool.v @@ -41,3 +41,13 @@ Hint Rewrite Bool.orb_andb_distrib_r Bool.orb_andb_distrib_l : push_orb. Hint Rewrite <- Bool.andb_orb_distrib_r Bool.andb_orb_distrib_l : push_orb. Hint Rewrite <- Bool.orb_andb_distrib_r Bool.orb_andb_distrib_l : pull_orb. Hint Rewrite Bool.andb_orb_distrib_r Bool.andb_orb_distrib_l : pull_orb. + +Definition pull_bool_if_dep {A B} (f : forall b : bool, A b -> B b) (b : bool) (x : A true) (y : A false) + : (if b return B b then f _ x else f _ y) = f b (if b return A b then x else y) + := if b return ((if b return B b then f _ x else f _ y) = f b (if b return A b then x else y)) + then eq_refl + else eq_refl. + +Definition pull_bool_if {A B} (f : A -> B) (b : bool) (x : A) (y : A) + : (if b then f x else f y) = f (if b then x else y) + := @pull_bool_if_dep (fun _ => A) (fun _ => B) (fun _ => f) b x y. -- cgit v1.2.3