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

feat(library/standard): add more decidable instances

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-20 01:09:37 +01:00
parent c37b5afe93
commit 5e8c128b00
2 changed files with 28 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
library/standard/decidable.lean
View file

@ -41,3 +41,20 @@ theorem decidable_not [instance] {a : Bool} (Ha : decidable a) : decidable (¬a)
:= rec Ha
(assume Ha, inr (not_not_intro Ha))
(assume Hna, inl Hna)
theorem decidable_iff [instance] {a b : Bool} (Ha : decidable a) (Hb : decidable b) : decidable (a ↔ b)
:= rec Ha
(assume Ha, rec Hb
(assume Hb : b, inl (iff_intro (assume H, Hb) (assume H, Ha)))
(assume Hnb : ¬b, inr (not_intro (assume H : a ↔ b, absurd (iff_mp_left H Ha) Hnb))))
(assume Hna, rec Hb
(assume Hb : b, inr (not_intro (assume H : a ↔ b, absurd (iff_mp_right H Hb) Hna)))
(assume Hnb : ¬b, inl (iff_intro (assume Ha, absurd_elim b Ha Hna) (assume Hb, absurd_elim a Hb Hnb))))
theorem decidable_implies [instance] {a b : Bool} (Ha : decidable a) (Hb : decidable b) : decidable (a → b)
:= rec Ha
(assume Ha : a, rec Hb
(assume Hb : b, inl (assume H, Hb))
(assume Hnb : ¬b, inr (not_intro (assume H : a → b,
absurd (H Ha) Hnb))))
(assume Hna : ¬a, inl (assume Ha, absurd_elim b Ha Hna))

11
tests/lean/run/decidable.lean Normal file
View file

@ -0,0 +1,11 @@
import standard unit decidable
using bit unit decidable
variables a b c : bit
variables u v : unit
theorem tst : decidable ((a = b) ∧ (b = c) → ¬ (u = v) ∨ (a = c) → (a = c) ↔ a = '1 ↔ true)
(*
print(get_env():find("tst"):value())
*)