refactor(library/init/nat,library/): protect more nat theorems
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
7bb2ffb79a
commit
dc8858d764
11 changed files with 65 additions and 64 deletions
|
|
@ -54,6 +54,9 @@ section
|
|||
theorem lt.irrefl (a : A) : ¬ a < a := !strict_order.lt_irrefl
|
||||
theorem not_lt_self (a : A) : ¬ a < a := !lt.irrefl -- alternate syntax
|
||||
|
||||
theorem lt_self_iff_false [simp] (a : A) : a < a ↔ false :=
|
||||
iff_false_intro (lt.irrefl a)
|
||||
|
||||
theorem lt.trans [trans] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
|
||||
|
||||
theorem gt.trans [trans] {a b c : A} (H1 : a > b) (H2: b > c) : a > c := lt.trans H2 H1
|
||||
|
|
|
|||
|
|
@ -131,7 +131,7 @@ finset.induction_on s
|
|||
(assume Hnfa : f a ∉ image f s',
|
||||
have H2 : card (image f s') + 1 = card s' + 1,
|
||||
by rewrite [card_insert_of_not_mem Hnfa at H1]; assumption,
|
||||
have H3 : card (image f s') = card s', from add.cancel_right H2,
|
||||
have H3 : card (image f s') = card s', from add.right_cancel H2,
|
||||
have injf : inj_on f (ts s'), from IH H3,
|
||||
show inj_on f (set.insert a (ts s')), from
|
||||
take x1 x2,
|
||||
|
|
|
|||
|
|
@ -178,7 +178,7 @@ calc
|
|||
... = pr2 q + pr1 p : by rewrite add.comm
|
||||
|
||||
protected theorem equiv.trans [trans] {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q ≡ r) : p ≡ r :=
|
||||
add.cancel_right (calc
|
||||
add.right_cancel (calc
|
||||
pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : by rewrite add.right_comm
|
||||
... = pr2 p + pr1 q + pr2 r : {H1}
|
||||
... = pr2 p + (pr1 q + pr2 r) : by rewrite add.assoc
|
||||
|
|
@ -221,7 +221,7 @@ theorem abstr_repr : Π (a : ℤ), abstr (repr a) = a
|
|||
| -[1+ m] := rfl
|
||||
|
||||
theorem repr_sub_nat_nat (m n : ℕ) : repr (sub_nat_nat m n) ≡ (m, n) :=
|
||||
lt_ge_by_cases
|
||||
nat.lt_ge_by_cases
|
||||
(take H : m < n,
|
||||
have H1 : repr (sub_nat_nat m n) = (0, n - m), by
|
||||
rewrite [sub_nat_nat_of_lt H, -(succ_pred_of_pos (sub_pos_of_lt H))],
|
||||
|
|
@ -271,7 +271,7 @@ section
|
|||
local attribute abstr [reducible]
|
||||
local attribute dist [reducible]
|
||||
theorem nat_abs_abstr : Π (p : ℕ × ℕ), nat_abs (abstr p) = dist (pr1 p) (pr2 p)
|
||||
| (m, n) := lt_ge_by_cases
|
||||
| (m, n) := nat.lt_ge_by_cases
|
||||
(assume H : m < n,
|
||||
calc
|
||||
nat_abs (abstr (m, n)) = nat_abs (-[1+ pred (n - m)]) : int.abstr_of_lt H
|
||||
|
|
@ -462,7 +462,7 @@ theorem repr_mul : Π (a b : ℤ), repr (a * b) = pmul (repr a) (repr b)
|
|||
theorem equiv_mul_prep {xa ya xb yb xn yn xm ym : ℕ}
|
||||
(H1 : xa + yb = ya + xb) (H2 : xn + ym = yn + xm)
|
||||
: xa*xn+ya*yn+(xb*ym+yb*xm) = xa*yn+ya*xn+(xb*xm+yb*ym) :=
|
||||
nat.add.cancel_right (calc
|
||||
nat.add.right_cancel (calc
|
||||
xa*xn+ya*yn + (xb*ym+yb*xm) + (yb*xn+xb*yn + (xb*xn+yb*yn))
|
||||
= xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*ym+yb*xm + (xb*xn+yb*yn)) : by rewrite add.comm4
|
||||
... = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*ym+yb*xm)) : by rewrite {xb*ym+yb*xm +_}nat.add_comm
|
||||
|
|
|
|||
|
|
@ -151,7 +151,7 @@ left_comm nat.add_comm nat.add_assoc
|
|||
protected theorem add.right_comm : Π (n m k : ℕ), n + m + k = n + k + m :=
|
||||
right_comm nat.add_comm nat.add_assoc
|
||||
|
||||
theorem add.cancel_left {n m k : ℕ} : n + m = n + k → m = k :=
|
||||
protected theorem add.left_cancel {n m k : ℕ} : n + m = n + k → m = k :=
|
||||
nat.induction_on n
|
||||
(take H : 0 + m = 0 + k,
|
||||
!nat.zero_add⁻¹ ⬝ H ⬝ !nat.zero_add)
|
||||
|
|
@ -164,9 +164,9 @@ nat.induction_on n
|
|||
have n + m = n + k, from succ.inj this,
|
||||
IH this)
|
||||
|
||||
theorem add.cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k :=
|
||||
protected theorem add.right_cancel {n m k : ℕ} (H : n + m = k + m) : n = k :=
|
||||
have H2 : m + n = m + k, from !nat.add_comm ⬝ H ⬝ !nat.add_comm,
|
||||
add.cancel_left H2
|
||||
add.left_cancel H2
|
||||
|
||||
theorem eq_zero_of_add_eq_zero_right {n m : ℕ} : n + m = 0 → n = 0 :=
|
||||
nat.induction_on n
|
||||
|
|
|
|||
|
|
@ -54,7 +54,7 @@ namespace nat
|
|||
|
||||
theorem not_bex_succ {P : nat → Prop} {n : nat} (H₁ : ¬ bex n P) (H₂ : ¬ P n) : ¬ bex (succ n) P :=
|
||||
λ H, obtain (w : nat) (Hw : w < succ n ∧ P w), from H,
|
||||
and.rec_on Hw (λ hltsn hp, or.rec_on (eq_or_lt_of_le (le_of_succ_le_succ hltsn))
|
||||
and.rec_on Hw (λ hltsn hp, or.rec_on (nat.eq_or_lt_of_le (le_of_succ_le_succ hltsn))
|
||||
(λ heq : w = n, absurd (eq.rec_on heq hp) H₂)
|
||||
(λ hltn : w < n, absurd (exists.intro w (and.intro hltn hp)) H₁))
|
||||
|
||||
|
|
@ -68,7 +68,7 @@ namespace nat
|
|||
λ x Hlt, H x (lt.step Hlt)
|
||||
|
||||
theorem ball_succ_of_ball {n : nat} {P : nat → Prop} (H₁ : ball n P) (H₂ : P n) : ball (succ n) P :=
|
||||
λ (x : nat) (Hlt : x < succ n), or.elim (eq_or_lt_of_le (le_of_succ_le_succ Hlt))
|
||||
λ (x : nat) (Hlt : x < succ n), or.elim (nat.eq_or_lt_of_le (le_of_succ_le_succ Hlt))
|
||||
(λ heq : x = n, eq.rec_on (eq.rec_on heq rfl) H₂)
|
||||
(λ hlt : x < n, H₁ x hlt)
|
||||
|
||||
|
|
|
|||
|
|
@ -247,7 +247,7 @@ calc
|
|||
theorem eq_quotient {q1 r1 q2 r2 y : ℕ} (H1 : r1 < y) (H2 : r2 < y)
|
||||
(H3 : q1 * y + r1 = q2 * y + r2) : q1 = q2 :=
|
||||
have H4 : q1 * y + r2 = q2 * y + r2, from (eq_remainder H1 H2 H3) ▸ H3,
|
||||
have H5 : q1 * y = q2 * y, from add.cancel_right H4,
|
||||
have H5 : q1 * y = q2 * y, from add.right_cancel H4,
|
||||
have H6 : y > 0, from lt_of_le_of_lt !zero_le H1,
|
||||
show q1 = q2, from eq_of_mul_eq_mul_right H6 H5
|
||||
|
||||
|
|
|
|||
|
|
@ -13,20 +13,20 @@ namespace nat
|
|||
/- lt and le -/
|
||||
|
||||
protected theorem le_of_lt_or_eq {m n : ℕ} (H : m < n ∨ m = n) : m ≤ n :=
|
||||
le_of_eq_or_lt (or.swap H)
|
||||
nat.le_of_eq_or_lt (or.swap H)
|
||||
|
||||
protected theorem lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ∨ m = n :=
|
||||
or.swap (eq_or_lt_of_le H)
|
||||
or.swap (nat.eq_or_lt_of_le H)
|
||||
|
||||
protected theorem le_iff_lt_or_eq (m n : ℕ) : m ≤ n ↔ m < n ∨ m = n :=
|
||||
iff.intro nat.lt_or_eq_of_le nat.le_of_lt_or_eq
|
||||
|
||||
protected theorem lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) : m ≠ n → m < n :=
|
||||
or_resolve_right (eq_or_lt_of_le H1)
|
||||
or_resolve_right (nat.eq_or_lt_of_le H1)
|
||||
|
||||
protected theorem lt_iff_le_and_ne (m n : ℕ) : m < n ↔ m ≤ n ∧ m ≠ n :=
|
||||
iff.intro
|
||||
(take H, and.intro (le_of_lt H) (take H1, !lt.irrefl (H1 ▸ H)))
|
||||
(take H, and.intro (nat.le_of_lt H) (take H1, !lt.irrefl (H1 ▸ H)))
|
||||
(and.rec nat.lt_of_le_and_ne)
|
||||
|
||||
theorem le_add_right (n k : ℕ) : n ≤ n + k :=
|
||||
|
|
@ -43,7 +43,7 @@ le.rec (exists.intro 0 rfl) (λm h, Exists.rec
|
|||
(λ k H, exists.intro (succ k) (H ▸ rfl)))
|
||||
|
||||
protected theorem le.total {m n : ℕ} : m ≤ n ∨ n ≤ m :=
|
||||
or.imp_left le_of_lt !lt_or_ge
|
||||
or.imp_left nat.le_of_lt !nat.lt_or_ge
|
||||
|
||||
/- addition -/
|
||||
|
||||
|
|
@ -54,10 +54,10 @@ protected theorem add_le_add_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k
|
|||
!add.comm ▸ !add.comm ▸ nat.add_le_add_left H k
|
||||
|
||||
protected theorem le_of_add_le_add_left {k n m : ℕ} (H : k + n ≤ k + m) : n ≤ m :=
|
||||
obtain l Hl, from le.elim H, le.intro (add.cancel_left (!add.assoc⁻¹ ⬝ Hl))
|
||||
obtain l Hl, from le.elim H, le.intro (add.left_cancel (!add.assoc⁻¹ ⬝ Hl))
|
||||
|
||||
protected theorem lt_of_add_lt_add_left {k n m : ℕ} (H : k + n < k + m) : n < m :=
|
||||
let H' := le_of_lt H in
|
||||
let H' := nat.le_of_lt H in
|
||||
nat.lt_of_le_and_ne (nat.le_of_add_le_add_left H') (assume Heq, !lt.irrefl (Heq ▸ H))
|
||||
|
||||
protected theorem add_lt_add_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m :=
|
||||
|
|
@ -83,7 +83,7 @@ protected theorem mul_le_mul {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n *
|
|||
le.trans (!nat.mul_le_mul_right H1) (!nat.mul_le_mul_left H2)
|
||||
|
||||
protected theorem mul_lt_mul_of_pos_left {n m k : ℕ} (H : n < m) (Hk : k > 0) : k * n < k * m :=
|
||||
lt_of_lt_of_le (nat.lt_add_of_pos_right Hk) (!mul_succ ▸ nat.mul_le_mul_left k (succ_le_of_lt H))
|
||||
nat.lt_of_lt_of_le (nat.lt_add_of_pos_right Hk) (!mul_succ ▸ nat.mul_le_mul_left k (succ_le_of_lt H))
|
||||
|
||||
protected theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k :=
|
||||
!mul.comm ▸ !mul.comm ▸ nat.mul_lt_mul_of_pos_left H Hk
|
||||
|
|
@ -95,19 +95,19 @@ open algebra
|
|||
protected definition decidable_linear_ordered_semiring [reducible] [trans_instance] :
|
||||
algebra.decidable_linear_ordered_semiring nat :=
|
||||
⦃ algebra.decidable_linear_ordered_semiring, nat.comm_semiring,
|
||||
add_left_cancel := @add.cancel_left,
|
||||
add_right_cancel := @add.cancel_right,
|
||||
add_left_cancel := @nat.add.left_cancel,
|
||||
add_right_cancel := @nat.add.right_cancel,
|
||||
lt := nat.lt,
|
||||
le := nat.le,
|
||||
le_refl := le.refl,
|
||||
le_trans := @le.trans,
|
||||
le_antisymm := @le.antisymm,
|
||||
le_total := @le.total,
|
||||
le_refl := nat.le.refl,
|
||||
le_trans := @nat.le.trans,
|
||||
le_antisymm := @nat.le.antisymm,
|
||||
le_total := @nat.le.total,
|
||||
le_iff_lt_or_eq := @nat.le_iff_lt_or_eq,
|
||||
le_of_lt := @le_of_lt,
|
||||
lt_irrefl := @lt.irrefl,
|
||||
lt_of_lt_of_le := @lt_of_lt_of_le,
|
||||
lt_of_le_of_lt := @lt_of_le_of_lt,
|
||||
le_of_lt := @nat.le_of_lt,
|
||||
lt_irrefl := @nat.lt.irrefl,
|
||||
lt_of_lt_of_le := @nat.lt_of_lt_of_le,
|
||||
lt_of_le_of_lt := @nat.lt_of_le_of_lt,
|
||||
lt_of_add_lt_add_left := @nat.lt_of_add_lt_add_left,
|
||||
add_lt_add_left := @nat.add_lt_add_left,
|
||||
add_le_add_left := @nat.add_le_add_left,
|
||||
|
|
|
|||
|
|
@ -251,7 +251,7 @@ have H2 : k - n + n = m + n, from
|
|||
k - n + n = k : sub_add_cancel (le.intro H)
|
||||
... = n + m : H⁻¹
|
||||
... = m + n : !add.comm,
|
||||
add.cancel_right H2
|
||||
add.right_cancel H2
|
||||
|
||||
theorem eq_sub_of_add_eq {a b c : ℕ} (H : a + c = b) : a = b - c :=
|
||||
(sub_eq_of_add_eq (!add.comm ▸ H))⁻¹
|
||||
|
|
@ -287,7 +287,7 @@ sub.cases
|
|||
... = m + m' : Hl
|
||||
... = k : Hm
|
||||
... = k - n + n : sub_add_cancel H3,
|
||||
le.intro (add.cancel_right H4))
|
||||
le.intro (add.right_cancel H4))
|
||||
|
||||
open algebra
|
||||
|
||||
|
|
|
|||
|
|
@ -88,7 +88,7 @@ theorem max_eq_left {a b : ℕ+} (H : ¬ a < b) : max a b = a :=
|
|||
begin rewrite lt.def at H, exact pnat.eq (max_eq_left (le_of_not_gt H)) end
|
||||
|
||||
theorem le_of_lt {a b : ℕ+} : a < b → a ≤ b :=
|
||||
begin rewrite [lt.def, le.def], apply le_of_lt end
|
||||
begin rewrite [lt.def, le.def], apply nat.le_of_lt end
|
||||
|
||||
theorem not_lt_of_ge {a b : ℕ+} : a ≤ b → ¬ (b < a) :=
|
||||
begin rewrite [lt.def, le.def], apply not_lt_of_ge end
|
||||
|
|
|
|||
|
|
@ -40,13 +40,13 @@ namespace nat
|
|||
|
||||
/- basic definitions on natural numbers -/
|
||||
inductive le (a : ℕ) : ℕ → Prop :=
|
||||
| refl : le a a
|
||||
| refl' : le a a -- use refl' to avoid overloading le.refl
|
||||
| step : Π {b}, le a b → le a (succ b)
|
||||
|
||||
definition nat_has_le [instance] [reducible] [priority nat.prio]: has_le nat := has_le.mk nat.le
|
||||
|
||||
lemma le_refl [refl] : ∀ a : nat, a ≤ a :=
|
||||
le.refl
|
||||
protected lemma le.refl [refl] : ∀ a : nat, a ≤ a :=
|
||||
le.refl'
|
||||
|
||||
protected definition lt [reducible] (n m : ℕ) := succ n ≤ m
|
||||
definition nat_has_lt [instance] [reducible] [priority nat.prio] : has_lt nat := has_lt.mk nat.lt
|
||||
|
|
@ -85,7 +85,7 @@ namespace nat
|
|||
|
||||
/- properties of inequality -/
|
||||
|
||||
theorem le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ !le.refl
|
||||
protected theorem le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ !le.refl
|
||||
|
||||
theorem le_succ (n : ℕ) : n ≤ succ n := le.step !le.refl
|
||||
|
||||
|
|
@ -97,14 +97,14 @@ namespace nat
|
|||
theorem pred_le_iff_true [simp] (n : ℕ) : pred n ≤ n ↔ true :=
|
||||
iff_true_intro (pred_le n)
|
||||
|
||||
theorem le.trans {n m k : ℕ} (H1 : n ≤ m) : m ≤ k → n ≤ k :=
|
||||
protected theorem le.trans {n m k : ℕ} (H1 : n ≤ m) : m ≤ k → n ≤ k :=
|
||||
le.rec H1 (λp H2, le.step)
|
||||
|
||||
theorem le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := le.trans H !le_succ
|
||||
|
||||
theorem le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := le.trans !le_succ H
|
||||
|
||||
theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H
|
||||
protected theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H
|
||||
|
||||
theorem succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m :=
|
||||
le.rec !le.refl (λa b, le.step)
|
||||
|
|
@ -144,18 +144,15 @@ namespace nat
|
|||
theorem zero_lt_succ_iff_true [simp] (n : ℕ) : 0 < succ n ↔ true :=
|
||||
iff_true_intro (zero_lt_succ n)
|
||||
|
||||
theorem lt.trans {n m k : ℕ} (H1 : n < m) : m < k → n < k :=
|
||||
protected theorem lt.trans {n m k : ℕ} (H1 : n < m) : m < k → n < k :=
|
||||
le.trans (le.step H1)
|
||||
|
||||
theorem lt_of_le_of_lt {n m k : ℕ} (H1 : n ≤ m) : m < k → n < k :=
|
||||
protected theorem lt_of_le_of_lt {n m k : ℕ} (H1 : n ≤ m) : m < k → n < k :=
|
||||
le.trans (succ_le_succ H1)
|
||||
|
||||
theorem lt_of_lt_of_le {n m k : ℕ} : n < m → m ≤ k → n < k := le.trans
|
||||
protected theorem lt_of_lt_of_le {n m k : ℕ} : n < m → m ≤ k → n < k := le.trans
|
||||
|
||||
theorem lt.irrefl (n : ℕ) : ¬n < n := not_succ_le_self
|
||||
|
||||
theorem lt_self_iff_false [simp] (n : ℕ) : n < n ↔ false :=
|
||||
iff_false_intro (lt.irrefl n)
|
||||
protected theorem lt.irrefl (n : ℕ) : ¬n < n := not_succ_le_self
|
||||
|
||||
theorem self_lt_succ (n : ℕ) : n < succ n := !le.refl
|
||||
|
||||
|
|
@ -165,34 +162,34 @@ namespace nat
|
|||
theorem lt.base (n : ℕ) : n < succ n := !le.refl
|
||||
|
||||
theorem le_lt_antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m < n) : false :=
|
||||
!lt.irrefl (lt_of_le_of_lt H1 H2)
|
||||
!lt.irrefl (nat.lt_of_le_of_lt H1 H2)
|
||||
|
||||
theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) : m ≤ n → n = m :=
|
||||
le.cases_on H1 (λa, rfl) (λa b c, absurd (lt_of_le_of_lt b c) !lt.irrefl)
|
||||
protected theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) : m ≤ n → n = m :=
|
||||
le.cases_on H1 (λa, rfl) (λa b c, absurd (nat.lt_of_le_of_lt b c) !lt.irrefl)
|
||||
|
||||
theorem lt_le_antisymm {n m : ℕ} (H1 : n < m) (H2 : m ≤ n) : false :=
|
||||
le_lt_antisymm H2 H1
|
||||
|
||||
theorem lt.asymm {n m : ℕ} (H1 : n < m) : ¬ m < n :=
|
||||
le_lt_antisymm (le_of_lt H1)
|
||||
protected theorem lt.asymm {n m : ℕ} (H1 : n < m) : ¬ m < n :=
|
||||
le_lt_antisymm (nat.le_of_lt H1)
|
||||
|
||||
theorem not_lt_zero (a : ℕ) : ¬ a < 0 := !not_succ_le_zero
|
||||
|
||||
theorem lt_zero_iff_false [simp] (a : ℕ) : a < 0 ↔ false :=
|
||||
iff_false_intro (not_lt_zero a)
|
||||
|
||||
theorem eq_or_lt_of_le {a b : ℕ} (H : a ≤ b) : a = b ∨ a < b :=
|
||||
protected theorem eq_or_lt_of_le {a b : ℕ} (H : a ≤ b) : a = b ∨ a < b :=
|
||||
le.cases_on H (inl rfl) (λn h, inr (succ_le_succ h))
|
||||
|
||||
theorem le_of_eq_or_lt {a b : ℕ} (H : a = b ∨ a < b) : a ≤ b :=
|
||||
or.elim H !le_of_eq !le_of_lt
|
||||
protected theorem le_of_eq_or_lt {a b : ℕ} (H : a = b ∨ a < b) : a ≤ b :=
|
||||
or.elim H !nat.le_of_eq !nat.le_of_lt
|
||||
|
||||
-- less-than is well-founded
|
||||
definition lt.wf [instance] : well_founded lt :=
|
||||
well_founded.intro (nat.rec
|
||||
(!acc.intro (λn H, absurd H (not_lt_zero n)))
|
||||
(λn IH, !acc.intro (λm H,
|
||||
elim (eq_or_lt_of_le (le_of_succ_le_succ H))
|
||||
elim (nat.eq_or_lt_of_le (le_of_succ_le_succ H))
|
||||
(λe, eq.substr e IH) (acc.inv IH))))
|
||||
|
||||
definition measure {A : Type} : (A → ℕ) → A → A → Prop :=
|
||||
|
|
@ -219,22 +216,23 @@ namespace nat
|
|||
definition decidable_lt [instance] [priority nat.prio] : ∀ a b : nat, decidable (a < b) :=
|
||||
λ a b, decidable_le (succ a) b
|
||||
|
||||
theorem lt_or_ge (a b : ℕ) : a < b ∨ a ≥ b :=
|
||||
protected theorem lt_or_ge (a b : ℕ) : a < b ∨ a ≥ b :=
|
||||
nat.rec (inr !zero_le) (λn, or.rec
|
||||
(λh, inl (le_succ_of_le h))
|
||||
(λh, elim (eq_or_lt_of_le h) (λe, inl (eq.subst e !le.refl)) inr)) b
|
||||
(λh, elim (nat.eq_or_lt_of_le h) (λe, inl (eq.subst e !le.refl)) inr)) b
|
||||
|
||||
definition lt_ge_by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a ≥ b → P) : P :=
|
||||
by_cases H1 (λh, H2 (elim !lt_or_ge (λa, absurd a h) (λa, a)))
|
||||
protected definition lt_ge_by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a ≥ b → P) : P :=
|
||||
by_cases H1 (λh, H2 (elim !nat.lt_or_ge (λa, absurd a h) (λa, a)))
|
||||
|
||||
definition lt.by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
|
||||
lt_ge_by_cases H1 (λh₁,
|
||||
lt_ge_by_cases H3 (λh₂, H2 (le.antisymm h₂ h₁)))
|
||||
protected definition lt.by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P)
|
||||
(H3 : b < a → P) : P :=
|
||||
nat.lt_ge_by_cases H1 (λh₁,
|
||||
nat.lt_ge_by_cases H3 (λh₂, H2 (le.antisymm h₂ h₁)))
|
||||
|
||||
theorem lt.trichotomy (a b : ℕ) : a < b ∨ a = b ∨ b < a :=
|
||||
protected theorem lt.trichotomy (a b : ℕ) : a < b ∨ a = b ∨ b < a :=
|
||||
lt.by_cases (λH, inl H) (λH, inr (inl H)) (λH, inr (inr H))
|
||||
|
||||
theorem eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬ a < b) : a = b ∨ b < a :=
|
||||
protected theorem eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬ a < b) : a = b ∨ b < a :=
|
||||
or.rec_on (lt.trichotomy a b)
|
||||
(λ hlt, absurd hlt hnlt)
|
||||
(λ h, h)
|
||||
|
|
|
|||
|
|
@ -50,7 +50,7 @@ private lemma Y_unique : ∀ {P l₁ l₂}, length l₁ = length l₂ → Y P l
|
|||
| P [] (a₂::l₂) h₁ h₂ h₃ := by contradiction
|
||||
| P (a₁::l₁) [] h₁ h₂ h₃ := by contradiction
|
||||
| P (a₁::l₁) (a₂::l₂) h₁ h₂ h₃ :=
|
||||
have n₁ : length l₁ = length l₂, by rewrite [*length_cons at h₁]; apply add.cancel_right h₁,
|
||||
have n₁ : length l₁ = length l₂, by rewrite [*length_cons at h₁]; apply add.right_cancel h₁,
|
||||
have n₂ : Y P l₁, from and.elim_left h₂,
|
||||
have n₃ : Y P l₂, from and.elim_left h₃,
|
||||
assert ih : l₁ = l₂, from Y_unique n₁ n₂ n₃,
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue