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

feat(library/init/logic): add is_true and is_false

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-11 18:14:03 -08:00
parent 91ce99d921
commit b01cf73a91
2 changed files with 26 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
library/init/logic.lean
View file

@ -605,3 +605,21 @@ decidable.rec
-- Remark: dite and ite are "definitionally equal" when we ignore the proofs.
theorem dite_ite_eq (c : Prop) [H : decidable c] {A : Type} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e :=
rfl
definition is_true (c : Prop) [H : decidable c] : Prop :=
if c then true else false
definition is_false (c : Prop) [H : decidable c] : Prop :=
if c then false else true
theorem of_is_true {c : Prop} [H₁ : decidable c] (H₂ : is_true c) : c :=
decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, false_elim (if_neg Hnc ▸ H₂))
theorem not_of_not_is_true {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_true c) : ¬ c :=
decidable.rec_on H₁ (λ Hc, absurd true.intro (if_pos Hc ▸ H₂)) (λ Hnc, Hnc)
theorem not_of_is_false {c : Prop} [H₁ : decidable c] (H₂ : is_false c) : ¬ c :=
decidable.rec_on H₁ (λ Hc, false_elim (if_pos Hc ▸ H₂)) (λ Hnc, Hnc)
theorem of_not_is_false {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_false c) : c :=
decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, absurd true.intro (if_neg Hnc ▸ H₂))

8
tests/lean/run/is_true.lean Normal file
View file

@ -0,0 +1,8 @@
import data.nat
open nat
example : is_true (2 = 2) := trivial
example : is_false (3 = 2) := trivial
example : is_true (2 < 3) := trivial
example : is_true (3 | 9) := trivial
example : is_false (3 | 7) := trivial