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

refactor(library): mark absurd_elim argument as implicit

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-26 18:27:39 -07:00
parent dd99e60a00
commit a8d58fdd33
14 changed files with 61 additions and 59 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
doc/lean/tutorial.org
View file

@ -528,10 +528,12 @@ the Lean standard library.
=not_intro H= produces a proof for =¬ a= from =H : a → false=. That is, =not_intro H= produces a proof for =¬ a= from =H : a → false=. That is,
we obtain =¬ a= if we can derive =false= from =a=. The expression we obtain =¬ a= if we can derive =false= from =a=. The expression
=absurd_elim b Ha Hna= produces a proof for =b= from =Ha : a= and =Hna : ¬ a=. =absurd_elim Ha Hna= produces a proof for some =b= from =Ha : a= and =Hna : ¬ a=.
That is, we can deduce anything if we have =a= and =¬ a=. That is, we can deduce anything if we have =a= and =¬ a=.
We now use =not_intro= and =absurd_elim= to produce a proof term for We now use =not_intro= and =absurd_elim= to produce a proof term for
=(a → b) → ¬b → ¬a=. =absurd Ha Hna= is just =absurd_elim false Ha Hna=. =(a → b) → ¬b → ¬a=. =absurd Ha Hna= is just a special case of
=absurd_elim= where =b=
is false.
#+BEGIN_SRC lean #+BEGIN_SRC lean
import logic import logic
@ -560,7 +562,7 @@ Now, here is the proof term for =¬a → b → (b → a) → c=
import logic import logic
variables a b c : Prop variables a b c : Prop
check fun (Hna : ¬ a) (Hb : b) (Hba : b → a), check fun (Hna : ¬ a) (Hb : b) (Hba : b → a),
absurd_elim c (Hba Hb) Hna absurd_elim (Hba Hb) Hna
#+END_SRC #+END_SRC
*** Iff (if-and-only-if) *** Iff (if-and-only-if)

2
library/data/bool.lean
View file

@ -120,7 +120,7 @@ cases_on a
theorem band_eq_tt_elim_left {a b : bool} (H : a && b = tt) : a = tt := theorem band_eq_tt_elim_left {a b : bool} (H : a && b = tt) : a = tt :=
or_elim (dichotomy a) or_elim (dichotomy a)
(assume H0 : a = ff, (assume H0 : a = ff,
absurd_elim (a = tt) absurd_elim
(calc ff = ff && b : (band_ff_left _)⁻¹ (calc ff = ff && b : (band_ff_left _)⁻¹
... = a && b : {H0⁻¹} ... = a && b : {H0⁻¹}
... = tt : H) ... = tt : H)

6
library/data/int/order.lean
View file

@ -522,7 +522,7 @@ theorem mul_lt_cancel_left_nonneg {a b c : ℤ} (Hc : c ≥ 0) (H : c * a < c *
or_elim (le_or_gt b a) or_elim (le_or_gt b a)
(assume H2 : b ≤ a, (assume H2 : b ≤ a,
have H3 : c * b ≤ c * a, from mul_le_left_nonneg Hc H2, have H3 : c * b ≤ c * a, from mul_le_left_nonneg Hc H2,
absurd_elim _ H3 (lt_imp_not_ge H)) absurd_elim H3 (lt_imp_not_ge H))
(assume H2 : a < b, H2) (assume H2 : a < b, H2)
theorem mul_lt_cancel_right_nonneg {a b c : ℤ} (Hc : c ≥ 0) (H : a * c < b * c) : a < b := theorem mul_lt_cancel_right_nonneg {a b c : ℤ} (Hc : c ≥ 0) (H : a * c < b * c) : a < b :=
@ -543,7 +543,7 @@ or_elim (le_or_gt a b)
(assume H2 : a ≤ b, H2) (assume H2 : a ≤ b, H2)
(assume H2 : a > b, (assume H2 : a > b,
have H3 : c * a > c * b, from mul_lt_left_pos Hc H2, have H3 : c * a > c * b, from mul_lt_left_pos Hc H2,
absurd_elim _ H3 (le_imp_not_gt H)) absurd_elim H3 (le_imp_not_gt H))
theorem mul_le_cancel_right_pos {a b c : ℤ} (Hc : c > 0) (H : a * c ≤ b * c) : a ≤ b := theorem mul_le_cancel_right_pos {a b c : ℤ} (Hc : c > 0) (H : a * c ≤ b * c) : a ≤ b :=
mul_le_cancel_left_pos Hc (subst (mul_comm b c) (subst (mul_comm a c) H)) mul_le_cancel_left_pos Hc (subst (mul_comm b c) (subst (mul_comm a c) H))
@ -647,7 +647,7 @@ or_elim3 (trichotomy a 0) sorry sorry sorry
theorem to_nat_sign_ne_zero {a : ℤ} (H : a ≠ 0) : (to_nat (sign a)) = 1 := theorem to_nat_sign_ne_zero {a : ℤ} (H : a ≠ 0) : (to_nat (sign a)) = 1 :=
or_elim3 (trichotomy a 0) sorry or_elim3 (trichotomy a 0) sorry
-- (by simp) -- (by simp)
(assume H2 : a = 0, absurd_elim _ H2 H) (assume H2 : a = 0, absurd_elim H2 H)
sorry sorry
-- (by simp) -- (by simp)

4
library/data/list/basic.lean
View file

@ -164,7 +164,7 @@ theorem head_cons (x : T) (x0 : T) (t : list T) : head x0 (x :: t) = x := refl _
theorem head_concat (s t : list T) (x0 : T) : s ≠ nil → (head x0 (s ++ t) = head x0 s) := theorem head_concat (s t : list T) (x0 : T) : s ≠ nil → (head x0 (s ++ t) = head x0 s) :=
list_cases_on s list_cases_on s
(take H : nil ≠ nil, absurd_elim (head x0 (concat nil t) = head x0 nil) (refl nil) H) (take H : nil ≠ nil, absurd_elim (refl nil) H)
(take x s, (take x s,
take H : cons x s ≠ nil, take H : cons x s ≠ nil,
calc calc
@ -180,7 +180,7 @@ theorem tail_cons (x : T) (l : list T) : tail (cons x l) = l := refl _
theorem cons_head_tail (x0 : T) (l : list T) : l ≠ nil → (head x0 l) :: (tail l) = l := theorem cons_head_tail (x0 : T) (l : list T) : l ≠ nil → (head x0 l) :: (tail l) = l :=
list_cases_on l list_cases_on l
(assume H : nil ≠ nil, absurd_elim _ (refl _) H) (assume H : nil ≠ nil, absurd_elim (refl _) H)
(take x l, assume H : cons x l ≠ nil, refl _) (take x l, assume H : cons x l ≠ nil, refl _)

4
library/data/nat/basic.lean
View file

@ -255,7 +255,7 @@ induction_on n
(take (H : 0 + m = 0), refl 0) (take (H : 0 + m = 0), refl 0)
(take k IH, (take k IH,
assume (H : succ k + m = 0), assume (H : succ k + m = 0),
absurd_elim (succ k = 0) absurd_elim
(show succ (k + m) = 0, from (show succ (k + m) = 0, from
calc calc
succ (k + m) = succ k + m : symm (add_succ_left k m) succ (k + m) = succ k + m : symm (add_succ_left k m)
@ -402,7 +402,7 @@ discriminate
... = succ k * succ l : {Hk} ... = succ k * succ l : {Hk}
... = k * succ l + succ l : mul_succ_left _ _ ... = k * succ l + succ l : mul_succ_left _ _
... = succ (k * succ l + l) : add_succ_right _ _), ... = succ (k * succ l + l) : add_succ_right _ _),
absurd_elim _ (trans Heq H) (succ_ne_zero _))) absurd_elim (trans Heq H) (succ_ne_zero _)))
---other inversion theorems appear below ---other inversion theorems appear below

12
library/data/nat/order.lean
View file

@ -297,7 +297,7 @@ not_succ_zero_le n
theorem lt_imp_eq_succ {n m : ℕ} (H : n < m) : exists k, m = succ k := theorem lt_imp_eq_succ {n m : ℕ} (H : n < m) : exists k, m = succ k :=
discriminate discriminate
(take (Hm : m = 0), absurd_elim _ (subst Hm H) (not_lt_zero n)) (take (Hm : m = 0), absurd_elim (subst Hm H) (not_lt_zero n))
(take (l : ℕ) (Hm : m = succ l), exists_intro l Hm) (take (l : ℕ) (Hm : m = succ l), exists_intro l Hm)
-- ### interaction with le -- ### interaction with le
@ -437,7 +437,7 @@ theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n
have H1 : ∀n, ∀m, m < n → P m, from have H1 : ∀n, ∀m, m < n → P m, from
take n, take n,
induction_on n induction_on n
(show ∀m, m < 0 → P m, from take m H, absurd_elim _ H (not_lt_zero _)) (show ∀m, m < 0 → P m, from take m H, absurd_elim H (not_lt_zero _))
(take n', (take n',
assume IH : ∀m, m < n' → P m, assume IH : ∀m, m < n' → P m,
have H2: P n', from H n' IH, have H2: P n', from H n' IH,
@ -479,7 +479,7 @@ theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0 :=
H⁻¹ ▸ (succ_pos m) H⁻¹ ▸ (succ_pos m)
theorem ne_zero_imp_pos {n : ℕ} (H : n ≠ 0) : n > 0 := theorem ne_zero_imp_pos {n : ℕ} (H : n ≠ 0) : n > 0 :=
or_elim (zero_or_pos n) (take H2 : n = 0, absurd_elim _ H2 H) (take H2 : n > 0, H2) or_elim (zero_or_pos n) (take H2 : n = 0, absurd_elim H2 H) (take H2 : n > 0, H2)
theorem pos_imp_ne_zero {n : ℕ} (H : n > 0) : n ≠ 0 := theorem pos_imp_ne_zero {n : ℕ} (H : n > 0) : n ≠ 0 :=
ne_symm (lt_imp_ne H) ne_symm (lt_imp_ne H)
@ -512,7 +512,7 @@ discriminate
n * m = 0 * m : {H2} n * m = 0 * m : {H2}
... = 0 : mul_zero_left m, ... = 0 : mul_zero_left m,
have H4 : 0 > 0, from H3 ▸ H, have H4 : 0 > 0, from H3 ▸ H,
absurd_elim _ H4 (lt_irrefl 0)) absurd_elim H4 (lt_irrefl 0))
(take l : nat, (take l : nat,
assume Hl : n = succ l, assume Hl : n = succ l,
Hl⁻¹ ▸ (succ_pos l)) Hl⁻¹ ▸ (succ_pos l))
@ -545,7 +545,7 @@ theorem mul_lt_cancel_left {n m k : ℕ} (H : k * n < k * m) : n < m :=
or_elim (le_or_gt m n) or_elim (le_or_gt m n)
(assume H2 : m ≤ n, (assume H2 : m ≤ n,
have H3 : k * m ≤ k * n, from mul_le_left H2 k, have H3 : k * m ≤ k * n, from mul_le_left H2 k,
absurd_elim _ H3 (lt_imp_not_ge H)) absurd_elim H3 (lt_imp_not_ge H))
(assume H2 : n < m, H2) (assume H2 : n < m, H2)
theorem mul_lt_cancel_right {n m k : ℕ} (H : n * k < m * k) : n < m := theorem mul_lt_cancel_right {n m k : ℕ} (H : n * k < m * k) : n < m :=
@ -587,7 +587,7 @@ or_elim (le_or_gt n 1)
(assume H5 : n > 1, (assume H5 : n > 1,
have H6 : n * m ≥ 2 * 1, from mul_le H5 H4, have H6 : n * m ≥ 2 * 1, from mul_le H5 H4,
have H7 : 1 ≥ 2, from mul_one_right 2 ▸ H ▸ H6, have H7 : 1 ≥ 2, from mul_one_right 2 ▸ H ▸ H6,
absurd_elim _ (self_lt_succ 1) (le_imp_not_gt H7)) absurd_elim (self_lt_succ 1) (le_imp_not_gt H7))
theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 := theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 :=
mul_eq_one_left ((mul_comm n m) ▸ H) mul_eq_one_left ((mul_comm n m) ▸ H)

6
library/data/nat/sub.lean
View file

@ -196,7 +196,7 @@ sub_induction n m
... = succ (k - 0) : {symm (sub_zero_right k)}) ... = succ (k - 0) : {symm (sub_zero_right k)})
(take k, (take k,
assume H : succ k ≤ 0, assume H : succ k ≤ 0,
absurd_elim _ H (not_succ_zero_le k)) absurd_elim H (not_succ_zero_le k))
(take k l, (take k l,
assume IH : k ≤ l → succ l - k = succ (l - k), assume IH : k ≤ l → succ l - k = succ (l - k),
take H : succ k ≤ succ l, take H : succ k ≤ succ l,
@ -215,7 +215,7 @@ sub_induction n m
calc calc
0 + (k - 0) = k - 0 : add_zero_left (k - 0) 0 + (k - 0) = k - 0 : add_zero_left (k - 0)
... = k : sub_zero_right k) ... = k : sub_zero_right k)
(take k, assume H : succ k ≤ 0, absurd_elim _ H (not_succ_zero_le k)) (take k, assume H : succ k ≤ 0, absurd_elim H (not_succ_zero_le k))
(take k l, (take k l,
assume IH : k ≤ l → k + (l - k) = l, assume IH : k ≤ l → k + (l - k) = l,
take H : succ k ≤ succ l, take H : succ k ≤ succ l,
@ -271,7 +271,7 @@ have l1 : k ≤ m → n + m - k = n + (m - k), from
calc calc
n + m - 0 = n + m : sub_zero_right (n + m) n + m - 0 = n + m : sub_zero_right (n + m)
... = n + (m - 0) : {symm (sub_zero_right m)}) ... = n + (m - 0) : {symm (sub_zero_right m)})
(take k : ℕ, assume H : succ k ≤ 0, absurd_elim _ H (not_succ_zero_le k)) (take k : ℕ, assume H : succ k ≤ 0, absurd_elim H (not_succ_zero_le k))
(take k m, (take k m,
assume IH : k ≤ m → n + m - k = n + (m - k), assume IH : k ≤ m → n + m - k = n + (m - k),
take H : succ k ≤ succ m, take H : succ k ≤ succ m,

8
library/logic/axioms/classical.lean
View file

@ -98,9 +98,9 @@ eqt_intro (hrefl a)
theorem not_or (a b : Prop) : (¬(a ∨ b)) = (¬a ∧ ¬b) := theorem not_or (a b : Prop) : (¬(a ∨ b)) = (¬a ∧ ¬b) :=
propext propext
(assume H, or_elim (em a) (assume H, or_elim (em a)
(assume Ha, absurd_elim (¬a ∧ ¬b) (or_inl Ha) H) (assume Ha, absurd_elim (or_inl Ha) H)
(assume Hna, or_elim (em b) (assume Hna, or_elim (em b)
(assume Hb, absurd_elim (¬a ∧ ¬b) (or_inr Hb) H) (assume Hb, absurd_elim (or_inr Hb) H)
(assume Hnb, and_intro Hna Hnb))) (assume Hnb, and_intro Hna Hnb)))
(assume (H : ¬a ∧ ¬b) (N : a ∨ b), (assume (H : ¬a ∧ ¬b) (N : a ∨ b),
or_elim N or_elim N
@ -111,7 +111,7 @@ theorem not_and (a b : Prop) : (¬(a ∧ b)) = (¬a ∨ ¬b) :=
propext propext
(assume H, or_elim (em a) (assume H, or_elim (em a)
(assume Ha, or_elim (em b) (assume Ha, or_elim (em b)
(assume Hb, absurd_elim (¬a ∨ ¬b) (and_intro Ha Hb) H) (assume Hb, absurd_elim (and_intro Ha Hb) H)
(assume Hnb, or_inr Hnb)) (assume Hnb, or_inr Hnb))
(assume Hna, or_inl Hna)) (assume Hna, or_inl Hna))
(assume (H : ¬a ∨ ¬b) (N : a ∧ b), (assume (H : ¬a ∨ ¬b) (N : a ∧ b),
@ -153,7 +153,7 @@ propext (assume H, eqf_elim H) (assume H, eqf_intro H)
theorem not_exists_forall {A : Type} {P : A → Prop} (H : ¬∃x, P x) : ∀x, ¬P x := theorem not_exists_forall {A : Type} {P : A → Prop} (H : ¬∃x, P x) : ∀x, ¬P x :=
take x, or_elim (em (P x)) take x, or_elim (em (P x))
(assume Hp : P x, absurd_elim (¬P x) (exists_intro x Hp) H) (assume Hp : P x, absurd_elim (exists_intro x Hp) H)
(assume Hn : ¬P x, Hn) (assume Hn : ¬P x, Hn)
theorem not_forall_exists {A : Type} {P : A → Prop} (H : ¬∀x, P x) : ∃x, ¬P x := theorem not_forall_exists {A : Type} {P : A → Prop} (H : ¬∀x, P x) : ∃x, ¬P x :=

8
library/logic/classes/decidable.lean
View file

@ -27,10 +27,10 @@ theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2 :=
decidable_rec decidable_rec
(assume Hp1 : p, decidable_rec (assume Hp1 : p, decidable_rec
(assume Hp2 : p, congr_arg inl (refl Hp1)) -- using proof irrelevance for Prop (assume Hp2 : p, congr_arg inl (refl Hp1)) -- using proof irrelevance for Prop
(assume Hnp2 : ¬p, absurd_elim (inl Hp1 = inr Hnp2) Hp1 Hnp2) (assume Hnp2 : ¬p, absurd_elim Hp1 Hnp2)
d2) d2)
(assume Hnp1 : ¬p, decidable_rec (assume Hnp1 : ¬p, decidable_rec
(assume Hp2 : p, absurd_elim (inr Hnp1 = inl Hp2) Hp2 Hnp1) (assume Hp2 : p, absurd_elim Hp2 Hnp1)
(assume Hnp2 : ¬p, congr_arg inr (refl Hnp1)) -- using proof irrelevance for Prop (assume Hnp2 : ¬p, congr_arg inr (refl Hnp1)) -- using proof irrelevance for Prop
d2) d2)
d1 d1
@ -76,7 +76,7 @@ rec_on Ha
(assume Hna, rec_on Hb (assume Hna, rec_on Hb
(assume Hb : b, inr (assume H : a ↔ b, absurd (iff_elim_right H Hb) Hna)) (assume Hb : b, inr (assume H : a ↔ b, absurd (iff_elim_right H Hb) Hna))
(assume Hnb : ¬b, inl (assume Hnb : ¬b, inl
(iff_intro (assume Ha, absurd_elim b Ha Hna) (assume Hb, absurd_elim a Hb Hnb)))) (iff_intro (assume Ha, absurd_elim Ha Hna) (assume Hb, absurd_elim Hb Hnb))))
theorem implies_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : theorem implies_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
decidable (a → b) := decidable (a → b) :=
@ -84,7 +84,7 @@ rec_on Ha
(assume Ha : a, rec_on 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 (assume H : a → b, absurd (H Ha) Hnb))) (assume Hnb : ¬b, inr (assume H : a → b, absurd (H Ha) Hnb)))
(assume Hna : ¬a, inl (assume Ha, absurd_elim b Ha Hna)) (assume Hna : ¬a, inl (assume Ha, absurd_elim Ha Hna))
theorem decidable_iff_equiv {a b : Prop} (Ha : decidable a) (H : a ↔ b) : decidable b := theorem decidable_iff_equiv {a b : Prop} (Ha : decidable a) (H : a ↔ b) : decidable b :=
rec_on Ha rec_on Ha

12
library/logic/connectives/basic.lean
View file

@ -40,7 +40,7 @@ assume Hna : ¬a, absurd Ha Hna
theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a := theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a :=
assume Ha : a, absurd (H1 Ha) H2 assume Ha : a, absurd (H1 Ha) H2
theorem absurd_elim {a : Prop} (b : Prop) (H1 : a) (H2 : ¬a) : b := theorem absurd_elim {a : Prop} {b : Prop} (H1 : a) (H2 : ¬a) : b :=
false_elim b (absurd H1 H2) false_elim b (absurd H1 H2)
theorem absurd_not_true (H : ¬true) : false := theorem absurd_not_true (H : ¬true) : false :=
@ -50,7 +50,7 @@ theorem not_false_trivial : ¬false :=
assume H : false, H assume H : false, H
theorem not_implies_left {a b : Prop} (H : ¬(a → b)) : ¬¬a := theorem not_implies_left {a b : Prop} (H : ¬(a → b)) : ¬¬a :=
assume Hna : ¬a, absurd (assume Ha : a, absurd_elim b Ha Hna) H assume Hna : ¬a, absurd (assume Ha : a, absurd_elim Ha Hna) H
theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b := theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b :=
assume Hb : b, absurd (assume Ha : a, Hb) H assume Hb : b, absurd (assume Ha : a, Hb) H
@ -113,18 +113,18 @@ theorem or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
or_rec H2 H3 H1 or_rec H2 H3 H1
theorem resolve_right {a b : Prop} (H1 : a ∨ b) (H2 : ¬a) : b := theorem resolve_right {a b : Prop} (H1 : a ∨ b) (H2 : ¬a) : b :=
or_elim H1 (assume Ha, absurd_elim b Ha H2) (assume Hb, Hb) or_elim H1 (assume Ha, absurd_elim Ha H2) (assume Hb, Hb)
theorem resolve_left {a b : Prop} (H1 : a ∨ b) (H2 : ¬b) : a := 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) or_elim H1 (assume Ha, Ha) (assume Hb, absurd_elim Hb H2)
theorem or_swap {a b : Prop} (H : a ∨ b) : b ∨ a := theorem or_swap {a b : Prop} (H : a ∨ b) : b ∨ a :=
or_elim H (assume Ha, or_inr Ha) (assume Hb, or_inl 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) := theorem or_not_intro {a b : Prop} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) :=
assume H : a ∨ b, or_elim H assume H : a ∨ b, or_elim H
(assume Ha, absurd_elim _ Ha Hna) (assume Ha, absurd_elim Ha Hna)
(assume Hb, absurd_elim _ Hb Hnb) (assume Hb, absurd_elim Hb Hnb)
theorem or_imp_or {a b c d : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → d) : c ∨ d := theorem or_imp_or {a b c d : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → d) : c ∨ d :=
or_elim H1 or_elim H1

8
library/logic/connectives/if.lean
View file

@ -15,12 +15,12 @@ notation `if` c `then` t `else` e:45 := ite c t e
theorem if_pos {c : Prop} {H : decidable c} (Hc : c) {A : Type} (t e : A) : (if c then t else e) = t := theorem if_pos {c : Prop} {H : decidable c} (Hc : c) {A : Type} (t e : A) : (if c then t else e) = t :=
decidable_rec decidable_rec
(assume Hc : c, refl (@ite c (inl Hc) A t e)) (assume Hc : c, refl (@ite c (inl Hc) A t e))
(assume Hnc : ¬c, absurd_elim (@ite c (inr Hnc) A t e = t) Hc Hnc) (assume Hnc : ¬c, absurd_elim Hc Hnc)
H H
theorem if_neg {c : Prop} {H : decidable c} (Hnc : ¬c) {A : Type} (t e : A) : (if c then t else e) = e := theorem if_neg {c : Prop} {H : decidable c} (Hnc : ¬c) {A : Type} (t e : A) : (if c then t else e) = e :=
decidable_rec decidable_rec
(assume Hc : c, absurd_elim (@ite c (inl Hc) A t e = e) Hc Hnc) (assume Hc : c, absurd_elim Hc Hnc)
(assume Hnc : ¬c, refl (@ite c (inr Hnc) A t e)) (assume Hnc : ¬c, refl (@ite c (inr Hnc) A t e))
H H
@ -41,9 +41,9 @@ theorem if_cond_congr {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidab
rec_on H₁ rec_on H₁
(assume Hc₁ : c₁, rec_on H₂ (assume Hc₁ : c₁, rec_on H₂
(assume Hc₂ : c₂, (if_pos Hc₁ t e) ⬝ (if_pos Hc₂ t e)⁻¹) (assume Hc₂ : c₂, (if_pos Hc₁ t e) ⬝ (if_pos Hc₂ t e)⁻¹)
(assume Hnc₂ : ¬c₂, absurd_elim _ (iff_elim_left Heq Hc₁) Hnc₂)) (assume Hnc₂ : ¬c₂, absurd_elim (iff_elim_left Heq Hc₁) Hnc₂))
(assume Hnc₁ : ¬c₁, rec_on H₂ (assume Hnc₁ : ¬c₁, rec_on H₂
(assume Hc₂ : c₂, absurd_elim _ (iff_elim_right Heq Hc₂) Hnc₁) (assume Hc₂ : c₂, absurd_elim (iff_elim_right Heq Hc₂) Hnc₁)
(assume Hnc₂ : ¬c₂, (if_neg Hnc₁ t e) ⬝ (if_neg Hnc₂ t e)⁻¹)) (assume Hnc₂ : ¬c₂, (if_neg Hnc₁ t e) ⬝ (if_neg Hnc₂ t e)⁻¹))
theorem if_congr_aux {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidable c₂} {A : Type} {t₁ t₂ e₁ e₂ : A} theorem if_congr_aux {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidable c₂} {A : Type} {t₁ t₂ e₁ e₂ : A}

12
library/logic/examples/nuprl_examples.lean
View file

@ -18,7 +18,7 @@ assume Hab Hbc Ha,
-- 3. False Propositions and Negation -- 3. False Propositions and Negation
theorem thm4 {P Q : Prop} : ¬P → P → Q := theorem thm4 {P Q : Prop} : ¬P → P → Q :=
assume Hnp Hp, assume Hnp Hp,
absurd_elim Q Hp Hnp absurd_elim Hp Hnp
theorem thm5 {P : Prop} : P → ¬¬P := theorem thm5 {P : Prop} : P → ¬¬P :=
assume (Hp : P) (HnP : ¬P), assume (Hp : P) (HnP : ¬P),
@ -31,7 +31,7 @@ assume (Hpq : P → Q) (Hnq : ¬Q) (Hp : P),
theorem thm7 {P Q : Prop} : (P → ¬P) → (P → Q) := theorem thm7 {P Q : Prop} : (P → ¬P) → (P → Q) :=
assume Hpnp Hp, assume Hpnp Hp,
absurd_elim Q Hp (Hpnp Hp) absurd_elim Hp (Hpnp Hp)
theorem thm8 {P Q : Prop} : ¬(P → Q) → (P → ¬Q) := theorem thm8 {P Q : Prop} : ¬(P → Q) → (P → ¬Q) :=
assume (Hn : ¬(P → Q)) (Hp : P) (Hq : Q), assume (Hn : ¬(P → Q)) (Hp : P) (Hq : Q),
@ -44,7 +44,7 @@ theorem thm9 {P : Prop} : (P ∨ ¬P) → (¬¬P → P) :=
assume (em : P ∨ ¬P) (Hnn : ¬¬P), assume (em : P ∨ ¬P) (Hnn : ¬¬P),
or_elim em or_elim em
(assume Hp, Hp) (assume Hp, Hp)
(assume Hn, absurd_elim P Hn Hnn) (assume Hn, absurd_elim Hn Hnn)
theorem thm10 {P : Prop} : ¬¬(P ∨ ¬P) := theorem thm10 {P : Prop} : ¬¬(P ∨ ¬P) :=
assume Hnem : ¬(P ∨ ¬P), assume Hnem : ¬(P ∨ ¬P),
@ -76,7 +76,7 @@ assume (H : ¬P ∧ ¬Q) (Hn : P ∨ Q),
theorem thm14 {P Q : Prop} : ¬P ∨ Q → P → Q := theorem thm14 {P Q : Prop} : ¬P ∨ Q → P → Q :=
assume (Hor : ¬P ∨ Q) (Hp : P), assume (Hor : ¬P ∨ Q) (Hp : P),
or_elim Hor or_elim Hor
(assume Hnp : ¬P, absurd_elim Q Hp Hnp) (assume Hnp : ¬P, absurd_elim Hp Hnp)
(assume Hq : Q, Hq) (assume Hq : Q, Hq)
theorem thm15 {P Q : Prop} : (P → Q) → ¬¬(¬P ∨ Q) := theorem thm15 {P Q : Prop} : (P → Q) → ¬¬(¬P ∨ Q) :=
@ -129,7 +129,7 @@ assume (Hem : C ∨ ¬C) (Hin : ∃x : T, true) (H1 : C → ∃x, P x),
exists_intro w Hr) exists_intro w Hr)
(assume Hnc : ¬C, (assume Hnc : ¬C,
obtain (w : T) (Hw : true), from Hin, obtain (w : T) (Hw : true), from Hin,
have Hr : C → P w, from assume Hc, absurd_elim (P w) Hc Hnc, have Hr : C → P w, from assume Hc, absurd_elim Hc Hnc,
exists_intro w Hr) exists_intro w Hr)
theorem thm19b : (∃x, C → P x) → C → (∃x, P x) := theorem thm19b : (∃x, C → P x) → C → (∃x, P x) :=
@ -147,7 +147,7 @@ assume Hem Hin Hnf H,
have H1 : ¬(∀x, P x), from mt H Hnc, have H1 : ¬(∀x, P x), from mt H Hnc,
have H2 : ∃x, ¬P x, from Hnf H1, have H2 : ∃x, ¬P x, from Hnf H1,
obtain (w : T) (Hw : ¬P w), from H2, obtain (w : T) (Hw : ¬P w), from H2,
exists_intro w (assume H : P w, absurd_elim C H Hw)) exists_intro w (assume H : P w, absurd_elim H Hw))
theorem thm20b : (∃x, P x → C) → (∀ x, P x) → C := theorem thm20b : (∃x, P x → C) → (∀ x, P x) → C :=
assume Hex Hall, assume Hex Hall,

4
tests/lean/run/class4.lean
View file

@ -35,12 +35,12 @@ theorem is_zero_to_eq (x : nat) (H : is_zero x) : x = zero
(assume Hz : x = zero, Hz) (assume Hz : x = zero, Hz)
(assume Hs : (∃ n, x = succ n), (assume Hs : (∃ n, x = succ n),
exists_elim Hs (λ (w : nat) (Hw : x = succ w), exists_elim Hs (λ (w : nat) (Hw : x = succ w),
absurd_elim _ H (subst (symm Hw) (not_is_zero_succ w)))) absurd_elim H (subst (symm Hw) (not_is_zero_succ w))))
theorem is_not_zero_to_eq {x : nat} (H : ¬ is_zero x) : ∃ n, x = succ n theorem is_not_zero_to_eq {x : nat} (H : ¬ is_zero x) : ∃ n, x = succ n
:= or_elim (dichotomy x) := or_elim (dichotomy x)
(assume Hz : x = zero, (assume Hz : x = zero,
absurd_elim _ (subst (symm Hz) is_zero_zero) H) absurd_elim (subst (symm Hz) is_zero_zero) H)
(assume Hs, Hs) (assume Hs, Hs)
theorem not_zero_add (x y : nat) (H : ¬ is_zero y) : ¬ is_zero (x + y) theorem not_zero_add (x y : nat) (H : ¬ is_zero y) : ¬ is_zero (x + y)

26
tests/lean/slow/nat_wo_hints.lean
View file

@ -228,7 +228,7 @@ theorem add_eq_zero_left {n m : ℕ} : n + m = 0 → n = 0
(take (H : 0 + m = 0), refl 0) (take (H : 0 + m = 0), refl 0)
(take k IH, (take k IH,
assume (H : succ k + m = 0), assume (H : succ k + m = 0),
absurd_elim (succ k = 0) absurd_elim
(show succ (k + m) = 0, from (show succ (k + m) = 0, from
calc calc
succ (k + m) = succ k + m : symm (add_succ_left k m) succ (k + m) = succ k + m : symm (add_succ_left k m)
@ -376,7 +376,7 @@ theorem mul_eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0
... = succ k * succ l : { Hk } ... = succ k * succ l : { Hk }
... = k * succ l + succ l : mul_succ_left _ _ ... = k * succ l + succ l : mul_succ_left _ _
... = succ (k * succ l + l) : add_succ_right _ _), ... = succ (k * succ l + l) : add_succ_right _ _),
absurd_elim _ (trans Heq H) (succ_ne_zero _))) absurd_elim (trans Heq H) (succ_ne_zero _)))
-- see more under "positivity" below -- see more under "positivity" below
-------------------------------------------------- le -------------------------------------------------- le
@ -694,7 +694,7 @@ theorem lt_zero_inv (n : ℕ) : ¬ n < 0
theorem lt_positive {n m : ℕ} (H : n < m) : ∃k, m = succ k theorem lt_positive {n m : ℕ} (H : n < m) : ∃k, m = succ k
:= discriminate := discriminate
(take (Hm : m = 0), absurd_elim _ (subst Hm H) (lt_zero_inv n)) (take (Hm : m = 0), absurd_elim (subst Hm H) (lt_zero_inv n))
(take (l : ℕ) (Hm : m = succ l), exists_intro l Hm) (take (l : ℕ) (Hm : m = succ l), exists_intro l Hm)
---------- interaction with le ---------- interaction with le
@ -830,7 +830,7 @@ theorem strong_induction_on {P : ℕ → Prop} (n : ℕ) (IH : ∀n, (∀m, m <
(take m : ℕ, (take m : ℕ,
assume H4 : m < k, assume H4 : m < k,
have H5 : m < 0, from subst H2 H4, have H5 : m < 0, from subst H2 H4,
absurd_elim _ H5 (lt_zero_inv m)), absurd_elim H5 (lt_zero_inv m)),
show P k, from IH k H3) show P k, from IH k H3)
(take l : ℕ, (take l : ℕ,
assume IHl : ∀k, k ≤ l → P k, assume IHl : ∀k, k ≤ l → P k,
@ -866,7 +866,7 @@ theorem add_eq_self {n m : ℕ} (H : n + m = n) : m = 0
... = n : H, ... = n : H,
have H3 : n < n, from lt_intro H2, have H3 : n < n, from lt_intro H2,
have H4 : n ≠ n, from lt_ne H3, have H4 : n ≠ n, from lt_ne H3,
absurd_elim _ (refl n) H4) absurd_elim (refl n) H4)
-------------------------------------------------- positivity -------------------------------------------------- positivity
@ -881,11 +881,11 @@ theorem succ_positive {n m : ℕ} (H : n = succ m) : n > 0
:= subst (symm H) (lt_zero m) := subst (symm H) (lt_zero m)
theorem ne_zero_positive {n : ℕ} (H : n ≠ 0) : n > 0 theorem ne_zero_positive {n : ℕ} (H : n ≠ 0) : n > 0
:= or_elim (zero_or_positive n) (take H2 : n = 0, absurd_elim _ H2 H) (take H2 : n > 0, H2) := or_elim (zero_or_positive n) (take H2 : n = 0, absurd_elim H2 H) (take H2 : n > 0, H2)
theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : ∃l, n = succ l theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : ∃l, n = succ l
:= discriminate := discriminate
(take H2, absurd_elim _ (subst H2 H) (lt_irrefl 0)) (take H2, absurd_elim (subst H2 H) (lt_irrefl 0))
(take l Hl, exists_intro l Hl) (take l Hl, exists_intro l Hl)
theorem add_positive_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n theorem add_positive_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n
@ -918,7 +918,7 @@ theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0
:= subst (symm H) (succ_pos m) := subst (symm H) (succ_pos m)
theorem ne_zero_pos {n : ℕ} (H : n ≠ 0) : n > 0 theorem ne_zero_pos {n : ℕ} (H : n ≠ 0) : n > 0
:= or_elim (zero_or_pos n) (take H2 : n = 0, absurd_elim _ H2 H) (take H2 : n > 0, H2) := or_elim (zero_or_pos n) (take H2 : n = 0, absurd_elim H2 H) (take H2 : n > 0, H2)
theorem add_pos_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n theorem add_pos_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n
:= subst (add_zero_right n) (add_lt_left H n) := subst (add_zero_right n) (add_lt_left H n)
@ -945,7 +945,7 @@ theorem mul_positive_inv_left {n m : ℕ} (H : n * m > 0) : n > 0
n * m = 0 * m : {H2} n * m = 0 * m : {H2}
... = 0 : mul_zero_left m, ... = 0 : mul_zero_left m,
have H4 : 0 > 0, from subst H3 H, have H4 : 0 > 0, from subst H3 H,
absurd_elim _ H4 (lt_irrefl 0)) absurd_elim H4 (lt_irrefl 0))
(take l : ℕ, (take l : ℕ,
assume Hl : n = succ l, assume Hl : n = succ l,
subst (symm Hl) (lt_zero l)) subst (symm Hl) (lt_zero l))
@ -1061,7 +1061,7 @@ theorem mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1
(assume H5 : n > 1, (assume H5 : n > 1,
have H6 : n * m ≥ 2 * 1, from mul_le H5 H4, have H6 : n * m ≥ 2 * 1, from mul_le H5 H4,
have H7 : 1 ≥ 2, from subst (mul_one_right 2) (subst H H6), have H7 : 1 ≥ 2, from subst (mul_one_right 2) (subst H H6),
absurd_elim _ (self_lt_succ 1) (le_imp_not_gt H7)) absurd_elim (self_lt_succ 1) (le_imp_not_gt H7))
theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1
:= mul_eq_one_left (subst (mul_comm n m) H) := mul_eq_one_left (subst (mul_comm n m) H)
@ -1222,7 +1222,7 @@ theorem succ_sub {m n : ℕ} : m ≥ n → succ m - n = succ (m - n)
... = succ (k - 0) : {symm (sub_zero_right k)}) ... = succ (k - 0) : {symm (sub_zero_right k)})
(take k, (take k,
assume H : succ k ≤ 0, assume H : succ k ≤ 0,
absurd_elim _ H (not_succ_zero_le k)) absurd_elim H (not_succ_zero_le k))
(take k l, (take k l,
assume IH : k ≤ l → succ l - k = succ (l - k), assume IH : k ≤ l → succ l - k = succ (l - k),
take H : succ k ≤ succ l, take H : succ k ≤ succ l,
@ -1241,7 +1241,7 @@ theorem add_sub_le {n m : ℕ} : n ≤ m → n + (m - n) = m
calc calc
0 + (k - 0) = k - 0 : add_zero_left (k - 0) 0 + (k - 0) = k - 0 : add_zero_left (k - 0)
... = k : sub_zero_right k) ... = k : sub_zero_right k)
(take k, assume H : succ k ≤ 0, absurd_elim _ H (not_succ_zero_le k)) (take k, assume H : succ k ≤ 0, absurd_elim H (not_succ_zero_le k))
(take k l, (take k l,
assume IH : k ≤ l → k + (l - k) = l, assume IH : k ≤ l → k + (l - k) = l,
take H : succ k ≤ succ l, take H : succ k ≤ succ l,
@ -1299,7 +1299,7 @@ theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m -
calc calc
n + m - 0 = n + m : sub_zero_right (n + m) n + m - 0 = n + m : sub_zero_right (n + m)
... = n + (m - 0) : {symm (sub_zero_right m)}) ... = n + (m - 0) : {symm (sub_zero_right m)})
(take k : ℕ, assume H : succ k ≤ 0, absurd_elim _ H (not_succ_zero_le k)) (take k : ℕ, assume H : succ k ≤ 0, absurd_elim H (not_succ_zero_le k))
(take k m, (take k m,
assume IH : k ≤ m → n + m - k = n + (m - k), assume IH : k ≤ m → n + m - k = n + (m - k),
take H : succ k ≤ succ m, take H : succ k ≤ succ m,