max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library): add to_bool lemmas

Browse source
This commit is contained in:
Leonardo de Moura 2017-12-03 13:27:12 -08:00
parent 8032d2eefd
commit b6c8551753
2 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/data/bool/lemmas.lean
View file

@ -101,7 +101,7 @@ show (ff = tt) = false, by simp
@[simp] lemma coe_tt : ↑tt = true :=
show (tt = tt) = true, by simp
theorem to_bool_iff (p : Prop) [d : decidable p] : to_bool p ↔ p :=
@[simp] theorem to_bool_iff (p : Prop) [d : decidable p] : (to_bool p = tt) ↔ p :=
match d with
| is_true hp := ⟨λh, hp, λ_, rfl⟩
| is_false hnp := ⟨λh, bool.no_confusion h, λhp, absurd hp hnp⟩
@ -117,7 +117,7 @@ theorem bool_iff_false {b : bool} : ¬ b ↔ b = ff := by cases b; exact dec_tri
theorem bool_eq_false {b : bool} : ¬ b → b = ff := bool_iff_false.1
theorem to_bool_ff_iff (p : Prop) [decidable p] : to_bool p = ff ↔ ¬p :=
@[simp] theorem to_bool_ff_iff (p : Prop) [decidable p] : to_bool p = ff ↔ ¬p :=
bool_iff_false.symm.trans (not_congr (to_bool_iff _))
theorem to_bool_ff {p : Prop} [decidable p] : ¬p → to_bool p = ff := (to_bool_ff_iff p).2

6
library/init/logic.lean
View file

@ -589,6 +589,12 @@ decidable.cases_on h (λ h₁, bool.ff) (λ h₂, bool.tt)
export decidable (is_true is_false to_bool)
@[simp] lemma to_bool_true_eq_tt (h : decidable true) : @to_bool true h = tt :=
decidable.cases_on h (λ h, false.elim (iff.mp not_true h)) (λ _, rfl)
@[simp] lemma to_bool_false_eq_ff (h : decidable false) : @to_bool false h = ff :=
decidable.cases_on h (λ h, rfl) (λ h, false.elim h)
instance decidable.true : decidable true :=
is_true trivial