From 379af8a04e347c8e734c75c8296f644621bcb001 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 9 May 2015 12:15:30 -0700 Subject: [PATCH] feat(library): avoid 'definition' hack for theorems --- hott/types/nat/order.hlean | 158 +++++++++++++++++------------------ library/data/encodable.lean | 2 +- library/data/fintype.lean | 8 +- library/data/nat/choose.lean | 16 ++-- library/data/nat/order.lean | 10 +-- library/init/logic.lean | 48 +++++------ library/init/nat.lean | 74 ++++++++-------- 7 files changed, 157 insertions(+), 159 deletions(-) diff --git a/hott/types/nat/order.hlean b/hott/types/nat/order.hlean index 674f82d6d..bfba715fd 100644 --- a/hott/types/nat/order.hlean +++ b/hott/types/nat/order.hlean @@ -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, diff --git a/library/data/encodable.lean b/library/data/encodable.lean index 882cb360d..706bdd40b 100644 --- a/library/data/encodable.lean +++ b/library/data/encodable.lean @@ -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], diff --git a/library/data/fintype.lean b/library/data/fintype.lean index 9de60c187..714e512b2 100644 --- a/library/data/fintype.lean +++ b/library/data/fintype.lean @@ -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, diff --git a/library/data/nat/choose.lean b/library/data/nat/choose.lean index a4bb7a6f7..6244b0117 100644 --- a/library/data/nat/choose.lean +++ b/library/data/nat/choose.lean @@ -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} := diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 848ebc2e9..ea9bb3377 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -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) diff --git a/library/init/logic.lean b/library/init/logic.lean index 20c5a2b64..d74d6e050 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -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)) diff --git a/library/init/nat.lean b/library/init/nat.lean index d4c0cf6a6..7a37e4a1f 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -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)