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

feat(library): avoid 'definition' hack for theorems

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-09 12:15:30 -07:00
parent 9812cfe906
commit 379af8a04e
7 changed files with 157 additions and 159 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

158
hott/types/nat/order.hlean
View file

@ -17,35 +17,35 @@ namespace nat
/- lt and le -/
definition le_of_lt_or_eq {m n : ℕ} (H : m < n ⊎ m = n) : m ≤ n :=
theorem le_of_lt_or_eq {m n : ℕ} (H : m < n ⊎ m = n) : m ≤ n :=
sum.rec_on H (take H1, le_of_lt H1) (take H1, H1 ▸ !le.refl)
definition lt.by_cases {a b : ℕ} {P : Type}
theorem lt.by_cases {a b : ℕ} {P : Type}
(H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
sum.rec_on !lt.trichotomy
(assume H, H1 H)
(assume H, sum.rec_on H (assume H', H2 H') (assume H', H3 H'))
definition lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ⊎ m = n :=
theorem lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ⊎ m = n :=
lt.by_cases
(assume H1 : m < n, sum.inl H1)
(assume H1 : m = n, sum.inr H1)
(assume H1 : m > n, absurd (lt_of_le_of_lt H H1) !lt.irrefl)
definition le_iff_lt_or_eq (m n : ℕ) : m ≤ n ↔ m < n ⊎ m = n :=
theorem le_iff_lt_or_eq (m n : ℕ) : m ≤ n ↔ m < n ⊎ m = n :=
iff.intro lt_or_eq_of_le le_of_lt_or_eq
definition lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) (H2 : m ≠ n) : m < n :=
theorem lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) (H2 : m ≠ n) : m < n :=
sum.rec_on (lt_or_eq_of_le H1)
(take H3 : m < n, H3)
(take H3 : m = n, absurd H3 H2)
definition lt_iff_le_and_ne (m n : ℕ) : m < n ↔ m ≤ n × m ≠ n :=
theorem lt_iff_le_and_ne (m n : ℕ) : m < n ↔ m ≤ n × m ≠ n :=
iff.intro
(take H, pair (le_of_lt H) (take H1, lt.irrefl _ (H1 ▸ H)))
(take H, lt_of_le_and_ne (pr1 H) (pr2 H))
definition le_add_right (n k : ℕ) : n ≤ n + k :=
theorem le_add_right (n k : ℕ) : n ≤ n + k :=
nat.rec_on k
(calc n ≤ n : le.refl n
... = n + zero : add_zero)
@ -53,13 +53,13 @@ nat.rec_on k
n ≤ succ (n + k) : le_succ_of_le ih
... = n + succ k : add_succ)
definition le_add_left (n m : ℕ): n ≤ m + n :=
theorem le_add_left (n m : ℕ): n ≤ m + n :=
!add.comm ▸ !le_add_right
definition le.intro {n m k : ℕ} (h : n + k = m) : n ≤ m :=
theorem le.intro {n m k : ℕ} (h : n + k = m) : n ≤ m :=
h ▸ le_add_right n k
definition le.elim {n m : ℕ} (h : n ≤ m) : Σk, n + k = m :=
theorem le.elim {n m : ℕ} (h : n ≤ m) : Σk, n + k = m :=
le.rec_on h
(sigma.mk 0 rfl)
(λ m (h : n < m), lt.rec_on h
@ -70,7 +70,7 @@ le.rec_on h
n + succ k = succ (n + k) : add_succ
... = succ b : h))))
definition le.total {m n : ℕ} : m ≤ n ⊎ n ≤ m :=
theorem le.total {m n : ℕ} : m ≤ n ⊎ n ≤ m :=
lt.by_cases
(assume H : m < n, sum.inl (le_of_lt H))
(assume H : m = n, sum.inl (H ▸ !le.refl))
@ -78,54 +78,54 @@ lt.by_cases
/- addition -/
definition add_le_add_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m :=
theorem add_le_add_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m :=
sigma.rec_on (le.elim H) (λ(l : ℕ) (Hl : n + l = m),
le.intro
(calc
k + n + l = k + (n + l) : !add.assoc
... = k + m : {Hl}))
definition add_le_add_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k ≤ m + k :=
theorem add_le_add_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k ≤ m + k :=
!add.comm ▸ !add.comm ▸ add_le_add_left H k
definition le_of_add_le_add_left {k n m : ℕ} (H : k + n ≤ k + m) : n ≤ m :=
theorem le_of_add_le_add_left {k n m : ℕ} (H : k + n ≤ k + m) : n ≤ m :=
sigma.rec_on (le.elim H) (λ(l : ℕ) (Hl : k + n + l = k + m),
le.intro (add.cancel_left
(calc
k + (n + l) = k + n + l : (!add.assoc)⁻¹
... = k + m : Hl)))
definition add_lt_add_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m :=
theorem add_lt_add_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m :=
lt_of_succ_le (!add_succ ▸ add_le_add_left (succ_le_of_lt H) k)
definition add_lt_add_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k :=
theorem add_lt_add_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k :=
!add.comm ▸ !add.comm ▸ add_lt_add_left H k
definition lt_add_of_pos_right {n k : ℕ} (H : k > 0) : n < n + k :=
theorem lt_add_of_pos_right {n k : ℕ} (H : k > 0) : n < n + k :=
!add_zero ▸ add_lt_add_left H n
/- multiplication -/
definition mul_le_mul_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k * n ≤ k * m :=
theorem mul_le_mul_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k * n ≤ k * m :=
sigma.rec_on (le.elim H) (λ(l : ℕ) (Hl : n + l = m),
have H2 : k * n + k * l = k * m, by rewrite [-mul.left_distrib, Hl],
le.intro H2)
definition mul_le_mul_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n * k ≤ m * k :=
theorem mul_le_mul_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n * k ≤ m * k :=
!mul.comm ▸ !mul.comm ▸ (mul_le_mul_left H k)
definition mul_le_mul {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l :=
theorem mul_le_mul {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l :=
le.trans (mul_le_mul_right H1 m) (mul_le_mul_left H2 k)
definition mul_lt_mul_of_pos_left {n m k : ℕ} (H : n < m) (Hk : k > 0) : k * n < k * m :=
theorem mul_lt_mul_of_pos_left {n m k : ℕ} (H : n < m) (Hk : k > 0) : k * n < k * m :=
have H2 : k * n < k * n + k, from lt_add_of_pos_right Hk,
have H3 : k * n + k ≤ k * m, from !mul_succ ▸ mul_le_mul_left (succ_le_of_lt H) k,
lt_of_lt_of_le H2 H3
definition mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k :=
theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k :=
!mul.comm ▸ !mul.comm ▸ mul_lt_mul_of_pos_left H Hk
definition le.antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
sigma.rec_on (le.elim H1) (λ(k : ℕ) (Hk : n + k = m),
sigma.rec_on (le.elim H2) (λ(l : ℕ) (Hl : m + l = n),
have L1 : k + l = 0, from
@ -141,7 +141,7 @@ calc
... = n + k : {L2⁻¹}
... = m : Hk))
definition zero_le (n : ℕ) : 0 ≤ n :=
theorem zero_le (n : ℕ) : 0 ≤ n :=
le.intro !zero_add
/- nat is an instance of a linearly ordered semiring -/
@ -177,75 +177,75 @@ end
section port_algebra
open [classes] algebra
definition add_pos_left : Π{a : ℕ}, 0 < a → Πb : ℕ, 0 < a + b :=
theorem add_pos_left : Π{a : ℕ}, 0 < a → Πb : ℕ, 0 < a + b :=
take a H b, @algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le
definition add_pos_right : Π{a : ℕ}, 0 < a → Πb : ℕ, 0 < b + a :=
theorem add_pos_right : Π{a : ℕ}, 0 < a → Πb : ℕ, 0 < b + a :=
take a H b, !add.comm ▸ add_pos_left H b
definition add_eq_zero_iff_eq_zero_and_eq_zero : Π{a b : ℕ},
theorem add_eq_zero_iff_eq_zero_and_eq_zero : Π{a b : ℕ},
a + b = 0 ↔ a = 0 × b = 0 :=
take a b : ℕ,
@algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _ a b !zero_le !zero_le
definition le_add_of_le_left : Π{a b c : ℕ}, b ≤ c → b ≤ a + c :=
theorem le_add_of_le_left : Π{a b c : ℕ}, b ≤ c → b ≤ a + c :=
take a b c H, @algebra.le_add_of_nonneg_of_le _ _ a b c !zero_le H
definition le_add_of_le_right : Π{a b c : ℕ}, b ≤ c → b ≤ c + a :=
theorem le_add_of_le_right : Π{a b c : ℕ}, b ≤ c → b ≤ c + a :=
take a b c H, @algebra.le_add_of_le_of_nonneg _ _ a b c H !zero_le
definition lt_add_of_lt_left : Π{b c : ℕ}, b < c → Πa, b < a + c :=
theorem lt_add_of_lt_left : Π{b c : ℕ}, b < c → Πa, b < a + c :=
take b c H a, @algebra.lt_add_of_nonneg_of_lt _ _ a b c !zero_le H
definition lt_add_of_lt_right : Π{b c : ℕ}, b < c → Πa, b < c + a :=
theorem lt_add_of_lt_right : Π{b c : ℕ}, b < c → Πa, b < c + a :=
take b c H a, @algebra.lt_add_of_lt_of_nonneg _ _ a b c H !zero_le
definition lt_of_mul_lt_mul_left : Π{a b c : ℕ}, c * a < c * b → a < b :=
theorem lt_of_mul_lt_mul_left : Π{a b c : ℕ}, c * a < c * b → a < b :=
take a b c H, @algebra.lt_of_mul_lt_mul_left _ _ a b c H !zero_le
definition lt_of_mul_lt_mul_right : Π{a b c : ℕ}, a * c < b * c → a < b :=
theorem lt_of_mul_lt_mul_right : Π{a b c : ℕ}, a * c < b * c → a < b :=
take a b c H, @algebra.lt_of_mul_lt_mul_right _ _ a b c H !zero_le
definition pos_of_mul_pos_left : Π{a b : ℕ}, 0 < a * b → 0 < b :=
theorem pos_of_mul_pos_left : Π{a b : ℕ}, 0 < a * b → 0 < b :=
take a b H, @algebra.pos_of_mul_pos_left _ _ a b H !zero_le
definition pos_of_mul_pos_right : Π{a b : ℕ}, 0 < a * b → 0 < a :=
theorem pos_of_mul_pos_right : Π{a b : ℕ}, 0 < a * b → 0 < a :=
take a b H, @algebra.pos_of_mul_pos_right _ _ a b H !zero_le
end port_algebra
definition zero_le_one : 0 ≤ 1 := dec_trivial
definition zero_lt_one : 0 < 1 := dec_trivial
theorem zero_le_one : 0 ≤ 1 := dec_trivial
theorem zero_lt_one : 0 < 1 := dec_trivial
/- properties specific to nat -/
definition lt_intro {n m k : ℕ} (H : succ n + k = m) : n < m :=
theorem lt_intro {n m k : ℕ} (H : succ n + k = m) : n < m :=
lt_of_succ_le (le.intro H)
definition lt_elim {n m : ℕ} (H : n < m) : Σk, succ n + k = m :=
theorem lt_elim {n m : ℕ} (H : n < m) : Σk, succ n + k = m :=
le.elim (succ_le_of_lt H)
definition lt_add_succ (n m : ℕ) : n < n + succ m :=
theorem lt_add_succ (n m : ℕ) : n < n + succ m :=
lt_intro !succ_add_eq_succ_add
definition eq_zero_of_le_zero {n : ℕ} (H : n ≤ 0) : n = 0 :=
theorem eq_zero_of_le_zero {n : ℕ} (H : n ≤ 0) : n = 0 :=
obtain (k : ℕ) (Hk : n + k = 0), from le.elim H,
eq_zero_of_add_eq_zero_right Hk
/- succ and pred -/
definition lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n :=
theorem lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n :=
iff.intro succ_le_of_lt lt_of_succ_le
definition not_succ_le_zero (n : ℕ) : ¬ succ n ≤ 0 :=
theorem not_succ_le_zero (n : ℕ) : ¬ succ n ≤ 0 :=
(assume H : succ n ≤ 0,
have H2 : succ n = 0, from eq_zero_of_le_zero H,
absurd H2 !succ_ne_zero)
definition succ_le_succ {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
theorem succ_le_succ {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
!add_one ▸ !add_one ▸ add_le_add_right H 1
definition le_of_succ_le_succ {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
theorem le_of_succ_le_succ {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
le_of_add_le_add_right ((!add_one)⁻¹ ▸ (!add_one)⁻¹ ▸ H)
definition self_le_succ (n : ℕ) : n ≤ succ n :=
theorem self_le_succ (n : ℕ) : n ≤ succ n :=
le.intro !add_one
definition succ_le_or_eq_of_le {n m : ℕ} (H : n ≤ m) : succ n ≤ m ⊎ n = m :=
theorem succ_le_or_eq_of_le {n m : ℕ} (H : n ≤ m) : succ n ≤ m ⊎ n = m :=
sum.rec_on (lt_or_eq_of_le H)
(assume H1 : n < m, sum.inl (succ_le_of_lt H1))
(assume H1 : n = m, sum.inr H1)
definition le_succ_of_pred_le {n m : ℕ} : pred n ≤ m → n ≤ succ m :=
theorem le_succ_of_pred_le {n m : ℕ} : pred n ≤ m → n ≤ succ m :=
nat.cases_on n
(assume H : pred 0 ≤ m, !zero_le)
(take n',
@ -253,7 +253,7 @@ nat.cases_on n
have H1 : n' ≤ m, from pred_succ n' ▸ H,
succ_le_succ H1)
definition pred_le_of_le_succ {n m : ℕ} : n ≤ succ m → pred n ≤ m :=
theorem pred_le_of_le_succ {n m : ℕ} : n ≤ succ m → pred n ≤ m :=
nat.cases_on n
(assume H, !pred_zero⁻¹ ▸ zero_le m)
(take n',
@ -261,7 +261,7 @@ nat.cases_on n
have H1 : n' ≤ m, from le_of_succ_le_succ H,
!pred_succ⁻¹ ▸ H1)
definition succ_le_of_le_pred {n m : ℕ} : succ n ≤ m → n ≤ pred m :=
theorem succ_le_of_le_pred {n m : ℕ} : succ n ≤ m → n ≤ pred m :=
nat.cases_on m
(assume H, absurd H !not_succ_le_zero)
(take m',
@ -269,47 +269,47 @@ nat.cases_on m
have H1 : n ≤ m', from le_of_succ_le_succ H,
!pred_succ⁻¹ ▸ H1)
definition pred_le_pred_of_le {n m : ℕ} : n ≤ m → pred n ≤ pred m :=
theorem pred_le_pred_of_le {n m : ℕ} : n ≤ m → pred n ≤ pred m :=
nat.cases_on n
(assume H, pred_zero⁻¹ ▸ zero_le (pred m))
(take n',
assume H : succ n' ≤ m,
!pred_succ⁻¹ ▸ succ_le_of_le_pred H)
definition lt_of_pred_lt_pred {n m : ℕ} (H : pred n < pred m) : n < m :=
theorem lt_of_pred_lt_pred {n m : ℕ} (H : pred n < pred m) : n < m :=
lt_of_not_le
(take H1 : m ≤ n,
not_lt_of_le (pred_le_pred_of_le H1) H)
definition le_or_eq_succ_of_le_succ {n m : ℕ} (H : n ≤ succ m) : n ≤ m ⊎ n = succ m :=
theorem le_or_eq_succ_of_le_succ {n m : ℕ} (H : n ≤ succ m) : n ≤ m ⊎ n = succ m :=
sum_of_sum_of_imp_left (succ_le_or_eq_of_le H)
(take H2 : succ n ≤ succ m, show n ≤ m, from le_of_succ_le_succ H2)
definition le_pred_self (n : ℕ) : pred n ≤ n :=
theorem le_pred_self (n : ℕ) : pred n ≤ n :=
nat.cases_on n
(pred_zero⁻¹ ▸ !le.refl)
(take k : ℕ, (!pred_succ)⁻¹ ▸ !self_le_succ)
definition succ_pos (n : ℕ) : 0 < succ n :=
theorem succ_pos (n : ℕ) : 0 < succ n :=
!zero_lt_succ
definition succ_pred_of_pos {n : ℕ} (H : n > 0) : succ (pred n) = n :=
theorem succ_pred_of_pos {n : ℕ} (H : n > 0) : succ (pred n) = n :=
(sum_resolve_right (eq_zero_or_eq_succ_pred n) (ne.symm (ne_of_lt H)))⁻¹
definition exists_eq_succ_of_lt {n m : ℕ} (H : n < m) : Σk, m = succ k :=
theorem exists_eq_succ_of_lt {n m : ℕ} (H : n < m) : Σk, m = succ k :=
discriminate
(take (Hm : m = 0), absurd (Hm ▸ H) !not_lt_zero)
(take (l : ℕ) (Hm : m = succ l), sigma.mk l Hm)
definition lt_succ_self (n : ℕ) : n < succ n :=
theorem lt_succ_self (n : ℕ) : n < succ n :=
lt.base n
definition le_of_lt_succ {n m : ℕ} (H : n < succ m) : n ≤ m :=
theorem le_of_lt_succ {n m : ℕ} (H : n < succ m) : n ≤ m :=
le_of_succ_le_succ (succ_le_of_lt H)
/- other forms of rec -/
protected definition strong_induction_on {P : nat → Type} (n : ℕ) (H : Πn, (Πm, m < n → P m) → P n) :
protected theorem strong_induction_on {P : nat → Type} (n : ℕ) (H : Πn, (Πm, m < n → P m) → P n) :
P n :=
have H1 : Π {n m : nat}, m < n → P m, from
take n,
@ -326,7 +326,7 @@ have H1 : Π {n m : nat}, m < n → P m, from
(assume H4: m = n', H4⁻¹ ▸ H2)),
H1 !lt_succ_self
protected definition case_strong_induction_on {P : nat → Type} (a : nat) (H0 : P 0)
protected theorem case_strong_induction_on {P : nat → Type} (a : nat) (H0 : P 0)
(Hind : Π(n : nat), (Πm, m ≤ n → P m) → P (succ n)) : P a :=
strong_induction_on a (
take n,
@ -340,24 +340,24 @@ strong_induction_on a (
/- pos -/
definition by_cases_zero_pos {P : ℕ → Type} (y : ℕ) (H0 : P 0) (H1 : Π {y : nat}, y > 0 → P y) : P y :=
theorem by_cases_zero_pos {P : ℕ → Type} (y : ℕ) (H0 : P 0) (H1 : Π {y : nat}, y > 0 → P y) : P y :=
nat.cases_on y H0 (take y, H1 !succ_pos)
definition eq_zero_or_pos (n : ℕ) : n = 0 ⊎ n > 0 :=
theorem eq_zero_or_pos (n : ℕ) : n = 0 ⊎ n > 0 :=
sum_of_sum_of_imp_left
(sum.swap (lt_or_eq_of_le !zero_le))
(take H : 0 = n, H⁻¹)
definition pos_of_ne_zero {n : ℕ} (H : n ≠ 0) : n > 0 :=
theorem pos_of_ne_zero {n : ℕ} (H : n ≠ 0) : n > 0 :=
sum.rec_on !eq_zero_or_pos (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2)
definition ne_zero_of_pos {n : ℕ} (H : n > 0) : n ≠ 0 :=
theorem ne_zero_of_pos {n : ℕ} (H : n > 0) : n ≠ 0 :=
ne.symm (ne_of_lt H)
definition exists_eq_succ_of_pos {n : ℕ} (H : n > 0) : Σl, n = succ l :=
theorem exists_eq_succ_of_pos {n : ℕ} (H : n > 0) : Σl, n = succ l :=
exists_eq_succ_of_lt H
definition pos_of_dvd_of_pos {m n : ℕ} (H1 : m ∣ n) (H2 : n > 0) : m > 0 :=
theorem pos_of_dvd_of_pos {m n : ℕ} (H1 : m ∣ n) (H2 : n > 0) : m > 0 :=
pos_of_ne_zero
(assume H3 : m = 0,
have H4 : n = 0, from eq_zero_of_zero_dvd (H3 ▸ H1),
@ -365,37 +365,37 @@ pos_of_ne_zero
/- multiplication -/
definition mul_lt_mul_of_le_of_lt {n m k l : ℕ} (Hk : k > 0) (H1 : n ≤ k) (H2 : m < l) :
theorem mul_lt_mul_of_le_of_lt {n m k l : ℕ} (Hk : k > 0) (H1 : n ≤ k) (H2 : m < l) :
n * m < k * l :=
lt_of_le_of_lt (mul_le_mul_right H1 m) (mul_lt_mul_of_pos_left H2 Hk)
definition mul_lt_mul_of_lt_of_le {n m k l : ℕ} (Hl : l > 0) (H1 : n < k) (H2 : m ≤ l) :
theorem mul_lt_mul_of_lt_of_le {n m k l : ℕ} (Hl : l > 0) (H1 : n < k) (H2 : m ≤ l) :
n * m < k * l :=
lt_of_le_of_lt (mul_le_mul_left H2 n) (mul_lt_mul_of_pos_right H1 Hl)
definition mul_lt_mul_of_le_of_le {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l :=
theorem mul_lt_mul_of_le_of_le {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l :=
have H3 : n * m ≤ k * m, from mul_le_mul_right (le_of_lt H1) m,
have H4 : k * m < k * l, from mul_lt_mul_of_pos_left H2 (lt_of_le_of_lt !zero_le H1),
lt_of_le_of_lt H3 H4
definition eq_of_mul_eq_mul_left {m k n : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k :=
theorem eq_of_mul_eq_mul_left {m k n : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k :=
have H2 : n * m ≤ n * k, from H ▸ !le.refl,
have H3 : n * k ≤ n * m, from H ▸ !le.refl,
have H4 : m ≤ k, from le_of_mul_le_mul_left H2 Hn,
have H5 : k ≤ m, from le_of_mul_le_mul_left H3 Hn,
le.antisymm H4 H5
definition eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k :=
theorem eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k :=
eq_of_mul_eq_mul_left Hm (!mul.comm ▸ !mul.comm ▸ H)
definition eq_zero_or_eq_of_mul_eq_mul_left {n m k : ℕ} (H : n * m = n * k) : n = 0 ⊎ m = k :=
theorem eq_zero_or_eq_of_mul_eq_mul_left {n m k : ℕ} (H : n * m = n * k) : n = 0 ⊎ m = k :=
sum_of_sum_of_imp_right !eq_zero_or_pos
(assume Hn : n > 0, eq_of_mul_eq_mul_left Hn H)
definition eq_zero_or_eq_of_mul_eq_mul_right {n m k : ℕ} (H : n * m = k * m) : m = 0 ⊎ n = k :=
theorem eq_zero_or_eq_of_mul_eq_mul_right {n m k : ℕ} (H : n * m = k * m) : m = 0 ⊎ n = k :=
eq_zero_or_eq_of_mul_eq_mul_left (!mul.comm ▸ !mul.comm ▸ H)
definition eq_one_of_mul_eq_one_right {n m : ℕ} (H : n * m = 1) : n = 1 :=
theorem eq_one_of_mul_eq_one_right {n m : ℕ} (H : n * m = 1) : n = 1 :=
have H2 : n * m > 0, from H⁻¹ ▸ !succ_pos,
have H3 : n > 0, from pos_of_mul_pos_right H2,
have H4 : m > 0, from pos_of_mul_pos_left H2,
@ -407,16 +407,16 @@ sum.rec_on (le_or_gt n 1)
have H7 : 1 ≥ 2, from !mul_one ▸ H ▸ H6,
absurd !lt_succ_self (not_lt_of_le H7))
definition eq_one_of_mul_eq_one_left {n m : ℕ} (H : n * m = 1) : m = 1 :=
theorem eq_one_of_mul_eq_one_left {n m : ℕ} (H : n * m = 1) : m = 1 :=
eq_one_of_mul_eq_one_right (!mul.comm ▸ H)
definition eq_one_of_mul_eq_self_left {n m : ℕ} (Hpos : n > 0) (H : m * n = n) : m = 1 :=
theorem eq_one_of_mul_eq_self_left {n m : ℕ} (Hpos : n > 0) (H : m * n = n) : m = 1 :=
eq_of_mul_eq_mul_right Hpos (H ⬝ !one_mul⁻¹)
definition eq_one_of_mul_eq_self_right {n m : ℕ} (Hpos : m > 0) (H : m * n = m) : n = 1 :=
theorem eq_one_of_mul_eq_self_right {n m : ℕ} (Hpos : m > 0) (H : m * n = m) : n = 1 :=
eq_one_of_mul_eq_self_left Hpos (!mul.comm ▸ H)
definition eq_one_of_dvd_one {n : ℕ} (H : n ∣ 1) : n = 1 :=
theorem eq_one_of_dvd_one {n : ℕ} (H : n ∣ 1) : n = 1 :=
dvd.elim H
(take m,
assume H1 : 1 = n * m,

2
library/data/encodable.lean
View file

@ -273,7 +273,7 @@ exists.intro (encode w)
unfold pn, rewrite [encodek], esimp, exact pw
end
private definition decode_ne_none_of_pn {n : nat} : pn n → decode A n ≠ none :=
private lemma decode_ne_none_of_pn {n : nat} : pn n → decode A n ≠ none :=
assume pnn e,
begin
rewrite [▸ (match decode A n with | some a := p a | none := false end) at pnn],

8
library/data/fintype.lean
View file

@ -89,13 +89,13 @@ definition check_pred (p : A → Prop) [h : decidable_pred p] : list A → bool
| [] := tt
| (a::l) := if p a then check_pred l else ff
definition check_pred_cons_of_pos {p : A → Prop} [h : decidable_pred p] {a : A} (l : list A) : p a → check_pred p (a::l) = check_pred p l :=
theorem check_pred_cons_of_pos {p : A → Prop} [h : decidable_pred p] {a : A} (l : list A) : p a → check_pred p (a::l) = check_pred p l :=
assume pa, if_pos pa
definition check_pred_cons_of_neg {p : A → Prop} [h : decidable_pred p] {a : A} (l : list A) : ¬ p a → check_pred p (a::l) = ff :=
theorem check_pred_cons_of_neg {p : A → Prop} [h : decidable_pred p] {a : A} (l : list A) : ¬ p a → check_pred p (a::l) = ff :=
assume npa, if_neg npa
definition all_of_check_pred_eq_tt {p : A → Prop} [h : decidable_pred p] : ∀ {l : list A}, check_pred p l = tt → ∀ {a}, a ∈ l → p a
theorem all_of_check_pred_eq_tt {p : A → Prop} [h : decidable_pred p] : ∀ {l : list A}, check_pred p l = tt → ∀ {a}, a ∈ l → p a
| [] eqtt a ainl := absurd ainl !not_mem_nil
| (b::l) eqtt a ainbl := by_cases
(λ pb : p b, or.elim (eq_or_mem_of_mem_cons ainbl)
@ -106,7 +106,7 @@ definition all_of_check_pred_eq_tt {p : A → Prop} [h : decidable_pred p] : ∀
(λ npb : ¬ p b,
by rewrite [check_pred_cons_of_neg _ npb at eqtt]; exact (bool.no_confusion eqtt))
definition ex_of_check_pred_eq_ff {p : A → Prop} [h : decidable_pred p] : ∀ {l : list A}, check_pred p l = ff → ∃ w, ¬ p w
theorem ex_of_check_pred_eq_ff {p : A → Prop} [h : decidable_pred p] : ∀ {l : list A}, check_pred p l = ff → ∃ w, ¬ p w
| [] eqtt := bool.no_confusion eqtt
| (a::l) eqtt := by_cases
(λ pa : p a,

16
library/data/nat/choose.lean
View file

@ -21,10 +21,10 @@ parameter {p : nat → Prop}
private definition lbp (x : nat) : Prop := ∀ y, y < x → ¬ p y
private definition lbp_zero : lbp 0 :=
private lemma lbp_zero : lbp 0 :=
λ y h, absurd h (not_lt_zero y)
private definition lbp_succ {x : nat} : lbp x → ¬ p x → lbp (succ x) :=
private lemma lbp_succ {x : nat} : lbp x → ¬ p x → lbp (succ x) :=
λ lx npx y yltsx,
or.elim (eq_or_lt_of_le yltsx)
(λ yeqx, by rewrite [yeqx]; exact npx)
@ -35,14 +35,14 @@ a > b ∧ lbp a
local infix `≺`:50 := gtb
private definition acc_of_px {x : nat} : p x → acc gtb x :=
private lemma acc_of_px {x : nat} : p x → acc gtb x :=
assume h,
acc.intro x (λ (y : nat) (l : y ≺ x),
have h₁ : y > x, from and.elim_left l,
have h₂ : ∀ a, a < y → ¬ p a, from and.elim_right l,
absurd h (h₂ x h₁))
private definition acc_of_acc_succ {x : nat} : acc gtb (succ x) → acc gtb x :=
private lemma acc_of_acc_succ {x : nat} : acc gtb (succ x) → acc gtb x :=
assume h,
acc.intro x (λ (y : nat) (l : y ≺ x),
have ygtx : x < y, from and.elim_left l,
@ -52,14 +52,14 @@ acc.intro x (λ (y : nat) (l : y ≺ x),
have ygtsx : succ x < y, from lt_of_le_and_ne (succ_lt_succ ygtx) (ne.symm ynex),
acc.inv h (and.intro ygtsx (and.elim_right l))))
private definition acc_of_px_of_gt {x y : nat} : p x → y > x → acc gtb y :=
private lemma acc_of_px_of_gt {x y : nat} : p x → y > x → acc gtb y :=
assume px ygtx,
acc.intro y (λ (z : nat) (l : z ≺ y),
have zgty : z > y, from and.elim_left l,
have h : ∀ a, a < z → ¬ p a, from and.elim_right l,
absurd px (h x (lt.trans ygtx zgty)))
private definition acc_of_acc_of_lt : ∀ {x y : nat}, acc gtb x → y < x → acc gtb y
private lemma acc_of_acc_of_lt : ∀ {x y : nat}, acc gtb x → y < x → acc gtb y
| 0 y a0 ylt0 := absurd ylt0 !not_lt_zero
| (succ x) y asx yltsx :=
assert ax : acc gtb x, from acc_of_acc_succ asx,
@ -71,14 +71,14 @@ parameter (ex : ∃ a, p a)
parameter [dp : decidable_pred p]
include dp
private definition acc_of_ex (x : nat) : acc gtb x :=
private lemma acc_of_ex (x : nat) : acc gtb x :=
obtain (w : nat) (pw : p w), from ex,
lt.by_cases
(λ xltw : x < w, acc_of_acc_of_lt (acc_of_px pw) xltw)
(λ xeqw : x = w, by rewrite [xeqw]; exact (acc_of_px pw))
(λ xgtw : x > w, acc_of_px_of_gt pw xgtw)
private definition wf_gtb : well_founded gtb :=
private lemma wf_gtb : well_founded gtb :=
well_founded.intro acc_of_ex
private definition find.F (x : nat) : (Π x₁, x₁ ≺ x → lbp x₁ → {a : nat | p a}) → lbp x → {a : nat | p a} :=

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

@ -11,19 +11,17 @@ import data.nat.basic algebra.ordered_ring
open eq.ops
namespace nat
/- lt and le -/
definition le_of_lt_or_eq {m n : ℕ} (H : m < n ∨ m = n) : m ≤ n :=
theorem le_of_lt_or_eq {m n : ℕ} (H : m < n ∨ m = n) : m ≤ n :=
or.elim H (take H1, le_of_lt H1) (take H1, H1 ▸ !le.refl)
definition lt.by_cases {a b : ℕ} {P : Prop}
theorem lt.by_cases {a b : ℕ} {P : Prop}
(H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
or.elim !lt.trichotomy
(assume H, H1 H)
(assume H, or.elim H (assume H', H2 H') (assume H', H3 H'))
definition lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ∨ m = n :=
theorem lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ∨ m = n :=
lt.by_cases
(assume H1 : m < n, or.inl H1)
(assume H1 : m = n, or.inr H1)
@ -32,7 +30,7 @@ lt.by_cases
theorem le_iff_lt_or_eq (m n : ℕ) : m ≤ n ↔ m < n ∨ m = n :=
iff.intro lt_or_eq_of_le le_of_lt_or_eq
definition lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) (H2 : m ≠ n) : m < n :=
theorem lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) (H2 : m ≠ n) : m < n :=
or.elim (lt_or_eq_of_le H1)
(take H3 : m < n, H3)
(take H3 : m = n, absurd H3 H2)

48
library/init/logic.lean
View file

@ -20,12 +20,12 @@ definition trivial := true.intro
definition not (a : Prop) := a → false
prefix `¬` := not
definition absurd {a : Prop} {b : Type} (H1 : a) (H2 : ¬a) : b :=
theorem absurd {a : Prop} {b : Type} (H1 : a) (H2 : ¬a) : b :=
false.rec b (H2 H1)
/- not -/
definition not_false : ¬false :=
theorem not_false : ¬false :=
assume H : false, H
definition non_contradictory (a : Prop) : Prop := ¬¬a
@ -36,7 +36,7 @@ assume Hna : ¬a, absurd Ha Hna
/- eq -/
notation a = b := eq a b
definition rfl {A : Type} {a : A} := eq.refl a
theorem rfl {A : Type} {a : A} : a = a := eq.refl a
-- proof irrelevance is built in
theorem proof_irrel {a : Prop} (H₁ H₂ : a) : H₁ = H₂ :=
@ -52,7 +52,7 @@ namespace eq
theorem trans (H₁ : a = b) (H₂ : b = c) : a = c :=
subst H₂ H₁
definition symm (H : a = b) : b = a :=
theorem symm (H : a = b) : b = a :=
eq.rec (refl a) H
namespace ops
@ -61,7 +61,7 @@ namespace eq
notation H1 ▸ H2 := subst H1 H2
end ops
protected definition drec_on {B : Πa' : A, a = a' → Type} (H₁ : a = a') (H₂ : B a (refl a)) : B a' H₁ :=
protected theorem drec_on {B : Πa' : A, a = a' → Type} (H₁ : a = a') (H₂ : B a (refl a)) : B a' H₁ :=
eq.rec (λH₁ : a = a, show B a H₁, from H₂) H₁ H₁
end eq
@ -72,10 +72,10 @@ section
variables {A : Type} {a b c: A}
open eq.ops
definition trans_rel_left (R : A → A → Prop) (H₁ : R a b) (H₂ : b = c) : R a c :=
theorem trans_rel_left (R : A → A → Prop) (H₁ : R a b) (H₂ : b = c) : R a c :=
H₂ ▸ H₁
definition trans_rel_right (R : A → A → Prop) (H₁ : a = b) (H₂ : R b c) : R a c :=
theorem trans_rel_right (R : A → A → Prop) (H₁ : a = b) (H₂ : R b c) : R a c :=
H₁⁻¹ ▸ H₂
end
@ -132,12 +132,12 @@ namespace heq
universe variable u
variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C}
definition to_eq (H : a == a') : a = a' :=
theorem to_eq (H : a == a') : a = a' :=
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a, from
λ Ht, eq.refl (eq.rec_on Ht a),
heq.rec_on H H₁ (eq.refl A)
definition elim {A : Type} {a : A} {P : A → Type} {b : A} (H₁ : a == b) (H₂ : P a) : P b :=
theorem elim {A : Type} {a : A} {P : A → Type} {b : A} (H₁ : a == b) (H₂ : P a) : P b :=
eq.rec_on (to_eq H₁) H₂
theorem subst {P : ∀T : Type, T → Prop} (H₁ : a == b) (H₂ : P A a) : P B b :=
@ -187,7 +187,7 @@ notation a `\/` b := or a b
notation a ∨ b := or a b
namespace or
definition elim (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → c) : c :=
theorem elim (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → c) : c :=
or.rec H₂ H₃ H₁
end or
@ -205,26 +205,26 @@ notation a <-> b := iff a b
notation a ↔ b := iff a b
namespace iff
definition intro (H₁ : a → b) (H₂ : b → a) : a ↔ b :=
theorem intro (H₁ : a → b) (H₂ : b → a) : a ↔ b :=
and.intro H₁ H₂
definition elim (H₁ : (a → b) → (b → a) → c) (H₂ : a ↔ b) : c :=
theorem elim (H₁ : (a → b) → (b → a) → c) (H₂ : a ↔ b) : c :=
and.rec H₁ H₂
definition elim_left (H : a ↔ b) : a → b :=
theorem elim_left (H : a ↔ b) : a → b :=
elim (assume H₁ H₂, H₁) H
definition mp := @elim_left
definition elim_right (H : a ↔ b) : b → a :=
theorem elim_right (H : a ↔ b) : b → a :=
elim (assume H₁ H₂, H₂) H
definition mp' := @elim_right
definition refl (a : Prop) : a ↔ a :=
theorem refl (a : Prop) : a ↔ a :=
intro (assume H, H) (assume H, H)
definition rfl {a : Prop} : a ↔ a :=
theorem rfl {a : Prop} : a ↔ a :=
refl a
theorem trans (H₁ : a ↔ b) (H₂ : b ↔ c) : a ↔ c :=
@ -242,7 +242,7 @@ namespace iff
iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
end iff
definition not_iff_not_of_iff (H₁ : a ↔ b) : ¬a ↔ ¬b :=
theorem not_iff_not_of_iff (H₁ : a ↔ b) : ¬a ↔ ¬b :=
iff.intro
(assume (Hna : ¬ a) (Hb : b), absurd (iff.elim_right H₁ Hb) Hna)
(assume (Hnb : ¬ b) (Ha : a), absurd (iff.elim_left H₁ Ha) Hnb)
@ -282,7 +282,7 @@ definition exists.intro := @Exists.intro
notation `exists` binders `,` r:(scoped P, Exists P) := r
notation `∃` binders `,` r:(scoped P, Exists P) := r
definition exists.elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
theorem exists.elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
Exists.rec H2 H1
/- decidable -/
@ -374,7 +374,7 @@ definition decidable_ne [instance] {A : Type} [H : decidable_eq A] : Π (a b : A
show Π x y : A, decidable (x = y → false), from _
namespace bool
definition ff_ne_tt : ff = tt → false
theorem ff_ne_tt : ff = tt → false
| [none]
end bool
@ -484,19 +484,19 @@ decidable.rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent
definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A :=
decidable.rec_on H (λ Hc, t) (λ Hnc, e)
definition 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
(λ Hc : c, eq.refl (@ite c (decidable.inl Hc) A t e))
(λ Hnc : ¬c, absurd Hc Hnc)
H
definition 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
(λ Hc : c, absurd Hc Hnc)
(λ Hnc : ¬c, eq.refl (@ite c (decidable.inr Hnc) A t e))
H
definition if_t_t (c : Prop) [H : decidable c] {A : Type} (t : A) : (if c then t else t) = t :=
theorem if_t_t (c : Prop) [H : decidable c] {A : Type} (t : A) : (if c then t else t) = t :=
decidable.rec
(λ Hc : c, eq.refl (@ite c (decidable.inl Hc) A t t))
(λ Hnc : ¬c, eq.refl (@ite c (decidable.inr Hnc) A t t))
@ -507,13 +507,13 @@ decidable.rec
definition dite (c : Prop) [H : decidable c] {A : Type} (t : c → A) (e : ¬ c → A) : A :=
decidable.rec_on H (λ Hc, t Hc) (λ Hnc, e Hnc)
definition dif_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t : c → A} {e : ¬ c → A} : (if H : c then t H else e H) = t Hc :=
theorem dif_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t : c → A} {e : ¬ c → A} : (if H : c then t H else e H) = t Hc :=
decidable.rec
(λ Hc : c, eq.refl (@dite c (decidable.inl Hc) A t e))
(λ Hnc : ¬c, absurd Hc Hnc)
H
definition dif_neg {c : Prop} [H : decidable c] (Hnc : ¬c) {A : Type} {t : c → A} {e : ¬ c → A} : (if H : c then t H else e H) = e Hnc :=
theorem dif_neg {c : Prop} [H : decidable c] (Hnc : ¬c) {A : Type} {t : c → A} {e : ¬ c → A} : (if H : c then t H else e H) = e Hnc :=
decidable.rec
(λ Hc : c, absurd Hc Hnc)
(λ Hnc : ¬c, eq.refl (@dite c (decidable.inr Hnc) A t e))

74
library/init/nat.lean
View file

@ -40,7 +40,7 @@ namespace nat
end
-- less-than is well-founded
definition lt.wf [instance] : well_founded lt :=
theorem lt.wf [instance] : well_founded lt :=
well_founded.intro (λn, nat.rec_on n
(acc.intro zero (λ (y : nat) (hlt : y < zero),
have aux : ∀ {n₁}, y < n₁ → zero = n₁ → acc lt y, from
@ -64,36 +64,36 @@ namespace nat
definition measure.wf {A : Type} (f : A → nat) : well_founded (measure f) :=
inv_image.wf f lt.wf
definition not_lt_zero (a : nat) : ¬ a < zero :=
theorem not_lt_zero (a : nat) : ¬ a < zero :=
have aux : ∀ {b}, a < b → b = zero → false, from
λ b H, lt.cases_on H
(by contradiction)
(by contradiction),
λ H, aux H rfl
definition zero_lt_succ (a : nat) : zero < succ a :=
theorem zero_lt_succ (a : nat) : zero < succ a :=
nat.rec_on a
(lt.base zero)
(λ a (hlt : zero < succ a), lt.step hlt)
definition lt.trans [trans] {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c :=
theorem lt.trans [trans] {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c :=
have aux : a < b → a < c, from
lt.rec_on H₂
(λ h₁, lt.step h₁)
(λ b₁ bb₁ ih h₁, lt.step (ih h₁)),
aux H₁
definition succ_lt_succ {a b : nat} (H : a < b) : succ a < succ b :=
theorem succ_lt_succ {a b : nat} (H : a < b) : succ a < succ b :=
lt.rec_on H
(lt.base (succ a))
(λ b hlt ih, lt.trans ih (lt.base (succ b)))
definition lt_of_succ_lt {a b : nat} (H : succ a < b) : a < b :=
theorem lt_of_succ_lt {a b : nat} (H : succ a < b) : a < b :=
lt.rec_on H
(lt.step (lt.base a))
(λ b h ih, lt.step ih)
definition lt_of_succ_lt_succ {a b : nat} (H : succ a < succ b) : a < b :=
theorem lt_of_succ_lt_succ {a b : nat} (H : succ a < succ b) : a < b :=
have aux : pred (succ a) < pred (succ b), from
lt.rec_on H
(lt.base a)
@ -115,20 +115,20 @@ namespace nat
inr aux)))
a
definition le.refl (a : nat) : a ≤ a :=
theorem le.refl (a : nat) : a ≤ a :=
lt.base a
definition le_of_lt {a b : nat} (H : a < b) : a ≤ b :=
theorem le_of_lt {a b : nat} (H : a < b) : a ≤ b :=
lt.step H
definition eq_or_lt_of_le {a b : nat} (H : a ≤ b) : a = b ∨ a < b :=
theorem eq_or_lt_of_le {a b : nat} (H : a ≤ b) : a = b ∨ a < b :=
begin
cases H with b hlt,
apply or.inl rfl,
apply or.inr hlt
end
definition le_of_eq_or_lt {a b : nat} (H : a = b ∨ a < b) : a ≤ b :=
theorem le_of_eq_or_lt {a b : nat} (H : a = b ∨ a < b) : a ≤ b :=
or.rec_on H
(λ hl, eq.rec_on hl !le.refl)
(λ hr, le_of_lt hr)
@ -136,25 +136,25 @@ namespace nat
definition decidable_le [instance] : decidable_rel le :=
λ a b, decidable_of_decidable_of_iff _ (iff.intro le_of_eq_or_lt eq_or_lt_of_le)
definition le.rec_on {a : nat} {P : nat → Prop} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : ∀ b, a < b → P b) : P b :=
theorem le.rec_on {a : nat} {P : nat → Prop} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : ∀ b, a < b → P b) : P b :=
begin
cases H with b' hlt,
apply H₁,
apply H₂ b' hlt
end
definition lt.irrefl (a : nat) : ¬ a < a :=
theorem lt.irrefl (a : nat) : ¬ a < a :=
nat.rec_on a
!not_lt_zero
(λ (a : nat) (ih : ¬ a < a) (h : succ a < succ a),
ih (lt_of_succ_lt_succ h))
definition lt.asymm {a b : nat} (H : a < b) : ¬ b < a :=
theorem lt.asymm {a b : nat} (H : a < b) : ¬ b < a :=
lt.rec_on H
(λ h : succ a < a, !lt.irrefl (lt_of_succ_lt h))
(λ b hlt (ih : ¬ b < a) (h : succ b < a), ih (lt_of_succ_lt h))
definition lt.trichotomy (a b : nat) : a < b ∨ a = b ∨ b < a :=
theorem lt.trichotomy (a b : nat) : a < b ∨ a = b ∨ b < a :=
nat.rec_on b
(λa, nat.cases_on a
(or.inr (or.inl rfl))
@ -168,38 +168,38 @@ namespace nat
(λ h : b₁ < a, or.inr (or.inr (succ_lt_succ h))))))
a
definition eq_or_lt_of_not_lt {a b : nat} (hnlt : ¬ a < b) : a = b ∨ b < a :=
theorem eq_or_lt_of_not_lt {a b : nat} (hnlt : ¬ a < b) : a = b ∨ b < a :=
or.rec_on (lt.trichotomy a b)
(λ hlt, absurd hlt hnlt)
(λ h, h)
definition lt_succ_of_le {a b : nat} (h : a ≤ b) : a < succ b :=
theorem lt_succ_of_le {a b : nat} (h : a ≤ b) : a < succ b :=
h
definition lt_of_succ_le {a b : nat} (h : succ a ≤ b) : a < b :=
theorem lt_of_succ_le {a b : nat} (h : succ a ≤ b) : a < b :=
lt_of_succ_lt_succ h
definition le_succ_of_le {a b : nat} (h : a ≤ b) : a ≤ succ b :=
theorem le_succ_of_le {a b : nat} (h : a ≤ b) : a ≤ succ b :=
lt.step h
definition succ_le_of_lt {a b : nat} (h : a < b) : succ a ≤ b :=
theorem succ_le_of_lt {a b : nat} (h : a < b) : succ a ≤ b :=
succ_lt_succ h
definition le.trans [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
theorem le.trans [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
begin
cases h₁ with b' hlt,
apply h₂,
apply lt.trans hlt h₂
end
definition lt_of_le_of_lt [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
theorem lt_of_le_of_lt [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
begin
cases h₁ with b' hlt,
apply h₂,
apply lt.trans hlt h₂
end
definition lt_of_lt_of_le [trans] {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
theorem lt_of_lt_of_le [trans] {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
begin
cases h₁ with b' hlt,
apply lt_of_succ_lt_succ h₂,
@ -212,27 +212,27 @@ namespace nat
definition min (a b : nat) : nat :=
if a < b then a else b
definition max_self (a : nat) : max a a = a :=
theorem max_self (a : nat) : max a a = a :=
eq.rec_on !if_t_t rfl
definition max_eq_right {a b : nat} (H : a < b) : max a b = b :=
theorem max_eq_right {a b : nat} (H : a < b) : max a b = b :=
if_pos H
definition max_eq_left {a b : nat} (H : ¬ a < b) : max a b = a :=
theorem max_eq_left {a b : nat} (H : ¬ a < b) : max a b = a :=
if_neg H
definition eq_max_right {a b : nat} (H : a < b) : b = max a b :=
theorem eq_max_right {a b : nat} (H : a < b) : b = max a b :=
eq.rec_on (max_eq_right H) rfl
definition eq_max_left {a b : nat} (H : ¬ a < b) : a = max a b :=
theorem eq_max_left {a b : nat} (H : ¬ a < b) : a = max a b :=
eq.rec_on (max_eq_left H) rfl
definition le_max_left (a b : nat) : a ≤ max a b :=
theorem le_max_left (a b : nat) : a ≤ max a b :=
by_cases
(λ h : a < b, le_of_lt (eq.rec_on (eq_max_right h) h))
(λ h : ¬ a < b, eq.rec_on (eq_max_left h) !le.refl)
definition le_max_right (a b : nat) : b ≤ max a b :=
theorem le_max_right (a b : nat) : b ≤ max a b :=
by_cases
(λ h : a < b, eq.rec_on (eq_max_right h) !le.refl)
(λ h : ¬ a < b, or.rec_on (eq_or_lt_of_not_lt h)
@ -267,26 +267,26 @@ namespace nat
section
local attribute sub [reducible]
definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
theorem succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
nat.rec_on b
rfl
(λ b₁ (ih : succ a - succ b₁ = a - b₁),
eq.rec_on ih (eq.refl (pred (succ a - succ b₁))))
end
definition sub_eq_succ_sub_succ (a b : nat) : a - b = succ a - succ b :=
theorem sub_eq_succ_sub_succ (a b : nat) : a - b = succ a - succ b :=
eq.rec_on (succ_sub_succ_eq_sub a b) rfl
definition zero_sub_eq_zero (a : nat) : zero - a = zero :=
theorem zero_sub_eq_zero (a : nat) : zero - a = zero :=
nat.rec_on a
rfl
(λ a₁ (ih : zero - a₁ = zero),
eq.rec_on ih (eq.refl (pred (zero - a₁))))
definition zero_eq_zero_sub (a : nat) : zero = zero - a :=
theorem zero_eq_zero_sub (a : nat) : zero = zero - a :=
eq.rec_on (zero_sub_eq_zero a) rfl
definition sub_lt {a b : nat} : zero < a → zero < b → a - b < a :=
theorem sub_lt {a b : nat} : zero < a → zero < b → a - b < a :=
have aux : Π {a}, zero < a → Π {b}, zero < b → a - b < a, from
λa h₁, lt.rec_on h₁
(λb h₂, lt.cases_on h₂
@ -301,12 +301,12 @@ namespace nat
(lt.trans (@ih b₁ bpos) (lt.base a₁)))),
λ h₁ h₂, aux h₁ h₂
definition pred_le (a : nat) : pred a ≤ a :=
theorem pred_le (a : nat) : pred a ≤ a :=
nat.cases_on a
(le.refl zero)
(λ a₁, le_of_lt (lt.base a₁))
definition sub_le (a b : nat) : a - b ≤ a :=
theorem sub_le (a b : nat) : a - b ≤ a :=
nat.induction_on b
(le.refl a)
(λ b₁ ih, le.trans !pred_le ih)