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

feat(library/standard): add or_inl and or_inr as short-hands for the commonly used 'or_intro_left _' and 'or_intro_right _'

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-27 17:25:57 -07:00
parent d1fe1286c0
commit 5555d620cf
6 changed files with 55 additions and 52 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/standard/bool.lean
View file

@ -21,7 +21,7 @@ definition cond {A : Type} (b : bool) (t e : A)
:= bool_rec e t b
theorem dichotomy (b : bool) : b = '0 ∨ b = '1
:= induction_on b (or_intro_left _ (refl '0)) (or_intro_right _ (refl '1))
:= induction_on b (or_inl (refl '0)) (or_inr (refl '1))
theorem cond_b0 {A : Type} (t e : A) : cond '0 t e = e
:= refl (cond '0 t e)
@ -79,8 +79,8 @@ theorem bor_to_or {a b : bool} : a || b = '1 → a = '1 ∨ b = '1
:= bool_rec
(assume H : '0 || b = '1,
have Hb : b = '1, from (bor_b0_left b) ▸ H,
or_intro_right _ Hb)
(assume H, or_intro_left _ (refl '1))
or_inr Hb)
(assume H, or_inl (refl '1))
a
definition band (a b : bool)

20
library/standard/classical.lean
View file

@ -13,13 +13,13 @@ theorem case (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a
theorem em (a : Prop) : a ∨ ¬a
:= or_elim (prop_complete a)
(assume Ht : a = true, or_intro_left (¬a) (eqt_elim Ht))
(assume Hf : a = false, or_intro_right a (eqf_elim Hf))
(assume Ht : a = true, or_inl (eqt_elim Ht))
(assume Hf : a = false, or_inr (eqf_elim Hf))
theorem prop_complete_swapped (a : Prop) : a = false ∨ a = true
:= case (λ x, x = false ∨ x = true)
(or_intro_right (true = false) (refl true))
(or_intro_left (false = true) (refl false))
(or_inr (refl true))
(or_inl (refl false))
a
theorem not_true : (¬true) = false
@ -86,9 +86,9 @@ theorem heq_id {A : Type} (a : A) : (a == a) = true
theorem not_or (a b : Prop) : (¬(a ∨ b)) = (¬a ∧ ¬b)
:= propext
(assume H, or_elim (em a)
(assume Ha, absurd_elim (¬a ∧ ¬b) (or_intro_left b Ha) H)
(assume Ha, absurd_elim (¬a ∧ ¬b) (or_inl Ha) H)
(assume Hna, or_elim (em b)
(assume Hb, absurd_elim (¬a ∧ ¬b) (or_intro_right a Hb) H)
(assume Hb, absurd_elim (¬a ∧ ¬b) (or_inr Hb) H)
(assume Hnb, and_intro Hna Hnb)))
(assume (H : ¬a ∧ ¬b) (N : a ∨ b),
or_elim N
@ -100,8 +100,8 @@ theorem not_and (a b : Prop) : (¬(a ∧ b)) = (¬a ∨ ¬b)
(assume H, or_elim (em a)
(assume Ha, or_elim (em b)
(assume Hb, absurd_elim (¬a ∨ ¬b) (and_intro Ha Hb) H)
(assume Hnb, or_intro_right (¬a) Hnb))
(assume Hna, or_intro_left (¬b) Hna))
(assume Hnb, or_inr Hnb))
(assume Hna, or_inl Hna))
(assume (H : ¬a ∨ ¬b) (N : a ∧ b),
or_elim H
(assume Hna, absurd (and_elim_left N) Hna)
@ -110,8 +110,8 @@ theorem not_and (a b : Prop) : (¬(a ∧ b)) = (¬a ∨ ¬b)
theorem imp_or (a b : Prop) : (a → b) = (¬a ∨ b)
:= propext
(assume H : a → b, (or_elim (em a)
(assume Ha : a, or_intro_right (¬a) (H Ha))
(assume Hna : ¬a, or_intro_left b Hna)))
(assume Ha : a, or_inr (H Ha))
(assume Hna : ¬a, or_inl Hna)))
(assume (H : ¬a ∨ b) (Ha : a),
resolve_right H ((not_not_eq a)⁻¹ ◂ Ha))

6
library/standard/decidable.lean
View file

@ -12,7 +12,7 @@ theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2
:= decidable_rec H1 H2 H
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_inl Hp) (λ Hnp, or_inr Hnp)
definition rec_on [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C
:= decidable_rec H1 H2 H
@ -44,9 +44,9 @@ theorem decidable_and [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable
theorem decidable_or [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∨ b)
:= rec_on Ha
(assume Ha : a, inl (or_intro_left b Ha))
(assume Ha : a, inl (or_inl Ha))
(assume Hna : ¬a, rec_on Hb
(assume Hb : b, inl (or_intro_right a Hb))
(assume Hb : b, inl (or_inr Hb))
(assume Hnb : ¬b, inr (or_not_intro Hna Hnb)))
theorem decidable_not [instance] {a : Prop} (Ha : decidable a) : decidable (¬a)

18
library/standard/diaconescu.lean
View file

@ -17,28 +17,28 @@ definition u [private] := epsilon (λ x, x = true ∨ p)
definition v [private] := epsilon (λ x, x = false ∨ p)
lemma u_def [private] : u = true ∨ p
:= epsilon_ax (exists_intro true (or_intro_left p (refl true)))
:= epsilon_ax (exists_intro true (or_inl (refl true)))
lemma v_def [private] : v = false ∨ p
:= epsilon_ax (exists_intro false (or_intro_left p (refl false)))
:= epsilon_ax (exists_intro false (or_inl (refl false)))
lemma uv_implies_p [private] : ¬(u = v) ∨ p
:= or_elim u_def
(assume Hut : u = true, or_elim v_def
(assume Hvf : v = false,
have Hne : ¬(u = v), from Hvf⁻¹ ▸ Hut⁻¹ ▸ true_ne_false,
or_intro_left p Hne)
(assume Hp : p, or_intro_right (¬u = v) Hp))
(assume Hp : p, or_intro_right (¬u = v) Hp)
or_inl Hne)
(assume Hp : p, or_inr Hp))
(assume Hp : p, or_inr Hp)
lemma p_implies_uv [private] : p → u = v
:= assume Hp : p,
have Hpred : (λ x, x = true ∨ p) = (λ x, x = false ∨ p), from
funext (take x : Prop,
have Hl : (x = true ∨ p) → (x = false ∨ p), from
assume A, or_intro_right (x = false) Hp,
assume A, or_inr Hp,
have Hr : (x = false ∨ p) → (x = true ∨ p), from
assume A, or_intro_right (x = true) Hp,
assume A, or_inr Hp,
show (x = true ∨ p) = (x = false ∨ p), from
propext Hl Hr),
show u = v, from
@ -47,6 +47,6 @@ lemma p_implies_uv [private] : p → u = v
theorem em : p ∨ ¬p
:= have H : ¬(u = v) → ¬p, from contrapos p_implies_uv,
or_elim uv_implies_p
(assume Hne : ¬(u = v), or_intro_right p (H Hne))
(assume Hp : p, or_intro_left (¬p) Hp)
(assume Hne : ¬(u = v), or_inr (H Hne))
(assume Hp : p, or_inl Hp)
end

29
library/standard/logic.lean
View file

@ -81,6 +81,9 @@ inductive or (a b : Prop) : Prop :=
infixr `\/`:30 := or
infixr `∨`:30 := or
theorem or_inl {a b : Prop} (Ha : a) : a ∨ b := or_intro_left b Ha
theorem or_inr {a b : Prop} (Hb : b) : a ∨ b := or_intro_right a Hb
theorem or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
:= or_rec H2 H3 H1
@ -91,7 +94,7 @@ theorem resolve_left {a b : Prop} (H1 : a ∨ b) (H2 : ¬b) : a
:= or_elim H1 (assume Ha, Ha) (assume Hb, absurd_elim a Hb H2)
theorem or_swap {a b : Prop} (H : a ∨ b) : b ∨ a
:= or_elim H (assume Ha, or_intro_right b Ha) (assume Hb, or_intro_left a Hb)
:= or_elim H (assume Ha, or_inr Ha) (assume Hb, or_inl Hb)
theorem or_not_intro {a b : Prop} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b)
:= assume H : a ∨ b, or_elim H
@ -100,18 +103,18 @@ theorem or_not_intro {a b : Prop} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b)
theorem or_imp_or {a b c d : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → d) : c ∨ d
:= or_elim H1
(assume Ha : a, or_intro_left _ (H2 Ha))
(assume Hb : b, or_intro_right _ (H3 Hb))
(assume Ha : a, or_inl (H2 Ha))
(assume Hb : b, or_inr (H3 Hb))
theorem imp_or_left {a b c : Prop} (H1 : a ∨ c) (H : a → b) : b ∨ c
:= or_elim H1
(assume H2 : a, or_intro_left _ (H H2))
(assume H2 : c, or_intro_right _ H2)
(assume H2 : a, or_inl (H H2))
(assume H2 : c, or_inr H2)
theorem imp_or_right {a b c : Prop} (H1 : c ∨ a) (H : a → b) : c ∨ b
:= or_elim H1
(assume H2 : c, or_intro_left _ H2)
(assume H2 : a, or_intro_right _ (H H2))
(assume H2 : c, or_inl H2)
(assume H2 : a, or_inr (H H2))
inductive eq {A : Type} (a : A) : A → Prop :=
| refl : eq a a
@ -271,14 +274,14 @@ theorem or_assoc (a b c : Prop) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c)
:= iff_intro
(assume H, or_elim H
(assume H1, or_elim H1
(assume Ha, or_intro_left _ Ha)
(assume Hb, or_intro_right a (or_intro_left c Hb)))
(assume Hc, or_intro_right a (or_intro_right b Hc)))
(assume Ha, or_inl Ha)
(assume Hb, or_inr (or_inl Hb)))
(assume Hc, or_inr (or_inr Hc)))
(assume H, or_elim H
(assume Ha, (or_intro_left c (or_intro_left b Ha)))
(assume Ha, (or_inl (or_inl Ha)))
(assume H1, or_elim H1
(assume Hb, or_intro_left c (or_intro_right a Hb))
(assume Hc, or_intro_right _ Hc)))
(assume Hb, or_inl (or_inr Hb))
(assume Hc, or_inr Hc)))
inductive Exists {A : Type} (P : A → Prop) : Prop :=
| exists_intro : ∀ (a : A), P a → Exists P

28
library/standard/nat.lean
View file

@ -55,8 +55,8 @@ theorem pred_succ (n : ℕ) : pred (succ n) = n
theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n)
:= induction_on n
(or_intro_left _ (refl 0))
(take m IH, or_intro_right _
(or_inl (refl 0))
(take m IH, or_inr
(show succ m = succ (pred (succ m)), from congr2 succ (pred_succ m⁻¹)))
theorem zero_or_succ2 (n : ℕ) : n = 0 ∨ ∃k, n = succ k
@ -366,11 +366,11 @@ theorem mul_one_left (n : ℕ) : 1 * n = n
theorem mul_eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0
:=
discriminate
(take Hn : n = 0, or_intro_left _ Hn)
(take Hn : n = 0, or_inl Hn)
(take (k : ℕ),
assume (Hk : n = succ k),
discriminate
(take (Hm : m = 0), or_intro_right _ Hm)
(take (Hm : m = 0), or_inr Hm)
(take (l : ℕ),
assume (Hl : m = succ l),
have Heq : succ (k * succ l + l) = n * m, from
@ -495,7 +495,7 @@ theorem succ_le_left_or {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
n = n + 0 : (add_zero_right n)⁻¹
... = n + k : {H3⁻¹}
... = m : Hk,
or_intro_right _ Heq)
or_inr Heq)
(take l:ℕ,
assume H3 : k = succ l,
have Hlt : succ n ≤ m, from
@ -504,7 +504,7 @@ theorem succ_le_left_or {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
succ n + l = n + succ l : add_move_succ n l
... = n + k : {H3⁻¹}
... = m : Hk)),
or_intro_left _ Hlt)
or_inl Hlt)
theorem succ_le_left {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m
:= resolve_left (succ_le_left_or H1) H2
@ -556,7 +556,7 @@ theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m
theorem pred_le_left_inv {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = succ m
:= discriminate
(take Hn : n = 0,
or_intro_left _ (subst (symm Hn) (zero_le m)))
or_inl (subst (symm Hn) (zero_le m)))
(take k : ℕ,
assume Hn : n = succ k,
have H2 : pred n = k,
@ -582,7 +582,7 @@ theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
n = n + 0 : symm (add_zero_right n)
... = n + k : {symm H3}
... = m : Hk,
or_intro_right _ Heq)
or_inr Heq)
(take l : nat,
assume H3 : k = succ l,
have Hlt : succ n ≤ m, from
@ -591,7 +591,7 @@ theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
succ n + l = n + succ l : add_move_succ n l
... = n + k : {symm H3}
... = m : Hk)),
or_intro_left _ Hlt)
or_inl Hlt)
theorem le_ne_imp_succ_le {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m
:= resolve_left (le_imp_succ_le_or_eq H1) H2
@ -619,7 +619,7 @@ theorem pred_le_imp_le_or_eq {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = su
:=
discriminate
(take Hn : n = 0,
or_intro_left _ (subst (symm Hn) (zero_le m)))
or_inl (subst (symm Hn) (zero_le m)))
(take k : nat,
assume Hn : n = succ k,
have H2 : pred n = k,
@ -789,7 +789,7 @@ theorem succ_lt_right {n m : ℕ} (H : n < m) : n < succ m
theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n
:= induction_on n
(or_intro_left _ (zero_le m))
(or_inl (zero_le m))
(take (k : ℕ),
assume IH : k ≤ m ∨ m < k,
or_elim IH
@ -803,7 +803,7 @@ theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n
... = k + 0 : {H2}
... = k : add_zero_right k,
have H4 : m < succ k, from subst H3 (lt_self_succ m),
or_intro_right _ H4)
or_inr H4)
(take l2 : ℕ,
assume H2 : l = succ l2,
have H3 : succ k + l2 = m,
@ -811,8 +811,8 @@ theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n
succ k + l2 = k + succ l2 : add_move_succ k l2
... = k + l : {symm H2}
... = m : Hl,
or_intro_left _ (le_intro H3)))
(assume H : m < k, or_intro_right _ (succ_lt_right H)))
or_inl (le_intro H3)))
(assume H : m < k, or_inr (succ_lt_right H)))
theorem trichotomy_alt (n m : ℕ) : (n < m ∨ n = m) ∨ m < n
:= or_imp_or (le_or_lt n m) (assume H : n ≤ m, le_imp_lt_or_eq H) (assume H : m < n, H)