michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/bool): add auxiliary theorems for bool

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-30 04:55:28 -07:00
parent 42fe87d7cc
commit 299cbe4b25
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/data/bool.lean
View file

@ -68,6 +68,12 @@ namespace bool
or.inr Hb)
(assume H, or.inl rfl)
theorem bor_inl {a b : bool} (H : a = tt) : a || b = tt :=
by rewrite H
theorem bor_inr {a b : bool} (H : b = tt) : a || b = tt :=
bool.rec_on a (by rewrite H) (by rewrite H)
theorem ff_band (a : bool) : ff && a = ff :=
rfl
@ -104,6 +110,9 @@ namespace bool
ff_ne_tt)
(assume H1 : a = tt, H1)
theorem band_intro {a b : bool} (H₁ : a = tt) (H₂ : b = tt) : a && b = tt :=
by rewrite [H₁, H₂]
theorem band_elim_right {a b : bool} (H : a && b = tt) : b = tt :=
band_elim_left (!band.comm ⬝ H)