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

refactor(library/standard): rename rec to rec_on

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-24 17:01:51 -07:00
parent 5529ef1056
commit bfdf187ce7
2 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
library/standard/decidable.lean
View file

@ -14,7 +14,7 @@ theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2
theorem em (p : Prop) (H : decidable p) : p ∨ ¬p theorem em (p : Prop) (H : decidable p) : p ∨ ¬p
:= induction_on H (λ Hp, or_intro_left _ Hp) (λ Hnp, or_intro_right _ Hnp) := induction_on H (λ Hp, or_intro_left _ Hp) (λ Hnp, or_intro_right _ Hnp)
definition rec [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C definition rec_on [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C
:= decidable_rec H1 H2 H := decidable_rec H1 H2 H
theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2 theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2
@ -36,36 +36,36 @@ theorem decidable_false [instance] : decidable false
:= inr not_false_trivial := inr not_false_trivial
theorem decidable_and [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∧ b) theorem decidable_and [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∧ b)
:= rec Ha := rec_on Ha
(assume Ha : a, rec Hb (assume Ha : a, rec_on Hb
(assume Hb : b, inl (and_intro Ha Hb)) (assume Hb : b, inl (and_intro Ha Hb))
(assume Hnb : ¬b, inr (and_not_right a Hnb))) (assume Hnb : ¬b, inr (and_not_right a Hnb)))
(assume Hna : ¬a, inr (and_not_left b Hna)) (assume Hna : ¬a, inr (and_not_left b Hna))
theorem decidable_or [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∨ b) theorem decidable_or [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∨ b)
:= rec Ha := rec_on Ha
(assume Ha : a, inl (or_intro_left b Ha)) (assume Ha : a, inl (or_intro_left b Ha))
(assume Hna : ¬a, rec Hb (assume Hna : ¬a, rec_on Hb
(assume Hb : b, inl (or_intro_right a Hb)) (assume Hb : b, inl (or_intro_right a Hb))
(assume Hnb : ¬b, inr (or_not_intro Hna Hnb))) (assume Hnb : ¬b, inr (or_not_intro Hna Hnb)))
theorem decidable_not [instance] {a : Prop} (Ha : decidable a) : decidable (¬a) theorem decidable_not [instance] {a : Prop} (Ha : decidable a) : decidable (¬a)
:= rec Ha := rec_on Ha
(assume Ha, inr (not_not_intro Ha)) (assume Ha, inr (not_not_intro Ha))
(assume Hna, inl Hna) (assume Hna, inl Hna)
theorem decidable_iff [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ↔ b) theorem decidable_iff [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ↔ b)
:= rec Ha := rec_on Ha
(assume Ha, rec Hb (assume Ha, rec_on Hb
(assume Hb : b, inl (iff_intro (assume H, Hb) (assume H, Ha))) (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 Hnb : ¬b, inr (not_intro (assume H : a ↔ b, absurd (iff_mp_left H Ha) Hnb))))
(assume Hna, rec Hb (assume Hna, rec_on Hb
(assume Hb : b, inr (not_intro (assume H : a ↔ b, absurd (iff_mp_right H Hb) Hna))) (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)))) (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 : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a → b) theorem decidable_implies [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a → b)
:= rec Ha := rec_on Ha
(assume Ha : a, rec Hb (assume Ha : a, rec_on Hb
(assume Hb : b, inl (assume H, Hb)) (assume Hb : b, inl (assume H, Hb))
(assume Hnb : ¬b, inr (not_intro (assume H : a → b, (assume Hnb : ¬b, inr (not_intro (assume H : a → b,
absurd (H Ha) Hnb)))) absurd (H Ha) Hnb))))

2
library/standard/if.lean
View file

@ -5,7 +5,7 @@ import decidable tactic
using decidable tactic using decidable tactic
definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A
:= rec H (assume Hc, t) (assume Hnc, e) := rec_on H (assume Hc, t) (assume Hnc, e)
notation `if` c `then` t `else` e:45 := ite c t e notation `if` c `then` t `else` e:45 := ite c t e