refactor(data/nat/decl): use new naming convention at data/nat/decl.lean
This commit is contained in:
Leonardo de Moura
parent
079bf7f633
commit
dad94eafbe
14 changed files with 138 additions and 128 deletions
|
|
@ -61,7 +61,7 @@ namespace fin
|
|||
... = succ p₁ : ih)
|
||||
|
||||
private lemma of_nat_eq {p n : nat} (H : p < n) : n - succ p + succ p = n :=
|
||||
add_sub_ge_left (lt_imp_le_succ H)
|
||||
add_sub_ge_left (succ_le_of_lt H)
|
||||
|
||||
definition of_nat (p : nat) (n : nat) : p < n → fin n :=
|
||||
λ H : p < n,
|
||||
|
|
|
|||
|
|
@ -18,9 +18,7 @@ namespace nat
|
|||
|
||||
notation a < b := lt a b
|
||||
|
||||
inductive le (a : nat) : nat → Prop :=
|
||||
refl : le a a,
|
||||
of_lt : ∀ {b}, lt a b → le a b
|
||||
definition le (a b : nat) : Prop := a < succ b
|
||||
|
||||
notation a ≤ b := le a b
|
||||
|
||||
|
|
@ -94,25 +92,25 @@ namespace nat
|
|||
(λ b hl ih h₁ h₂, lt.step (ih h₁ h₂))),
|
||||
aux H₂ rfl H₁
|
||||
|
||||
definition lt.imp_succ {a b : nat} (H : a < b) : succ a < succ b :=
|
||||
definition lt.succ_of_lt {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.cancel_succ_left {a b : nat} (H : succ a < b) : a < b :=
|
||||
definition lt.of_succ_lt {a b : nat} (H : succ a < b) : a < b :=
|
||||
have aux : ∀ {a₁}, a₁ < b → succ a = a₁ → a < b, from
|
||||
λ a₁ H, lt.rec_on H
|
||||
(λ e₁, eq.rec_on e₁ (lt.step (lt.base a)))
|
||||
(λ d hlt ih e₁, lt.step (ih e₁)),
|
||||
aux H rfl
|
||||
|
||||
definition lt.cancel_succ_left_right {a b : nat} (H : succ a < succ b) : a < b :=
|
||||
definition 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)
|
||||
(λ (b : nat) (hlt : succ a < b) ih,
|
||||
show pred (succ a) < pred (succ b), from
|
||||
lt.cancel_succ_left hlt),
|
||||
lt.of_succ_lt hlt),
|
||||
aux
|
||||
|
||||
definition lt.is_decidable_rel [instance] : decidable_rel lt :=
|
||||
|
|
@ -121,36 +119,55 @@ namespace nat
|
|||
(λ (b₁ : nat) (ih : ∀ a, decidable (a < b₁)) (a : nat), cases_on a
|
||||
(inl !zero_lt_succ)
|
||||
(λ a, decidable.rec_on (ih a)
|
||||
(λ h_pos : a < b₁, inl (lt.imp_succ h_pos))
|
||||
(λ h_pos : a < b₁, inl (lt.succ_of_lt h_pos))
|
||||
(λ h_neg : ¬ a < b₁,
|
||||
have aux : ¬ succ a < succ b₁, from
|
||||
λ h : succ a < succ b₁, h_neg (lt.cancel_succ_left_right h),
|
||||
λ h : succ a < succ b₁, h_neg (lt.of_succ_lt_succ h),
|
||||
inr aux)))
|
||||
a
|
||||
|
||||
definition le_def_right {a b : nat} (H : a ≤ b) : a = b ∨ a < b :=
|
||||
le.cases_on H
|
||||
(or.inl rfl)
|
||||
(λ b hlt, or.inr hlt)
|
||||
definition le.refl (a : nat) : a ≤ a :=
|
||||
lt.base a
|
||||
|
||||
definition le_def_left {a b : nat} (H : a = b ∨ a < b) : a ≤ b :=
|
||||
definition 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 :=
|
||||
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 :=
|
||||
or.rec_on H
|
||||
(λ hl, eq.rec_on hl !le.refl)
|
||||
(λ hr, le.of_lt hr)
|
||||
|
||||
definition le.is_decidable_rel [instance] : decidable_rel le :=
|
||||
λ a b, decidable_iff_equiv _ (iff.intro le_def_left le_def_right)
|
||||
λ a b, decidable_iff_equiv _ (iff.intro le.of_eq_or_lt eq_or_lt_of_le)
|
||||
|
||||
inductive le2 (a : nat) : nat → Prop :=
|
||||
refl : le2 a a,
|
||||
of_lt : ∀ {b}, lt a b → le2 a b
|
||||
|
||||
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 :=
|
||||
begin
|
||||
cases H with (b', hlt),
|
||||
apply H₁,
|
||||
apply (H₂ b' hlt)
|
||||
end
|
||||
|
||||
definition lt.irrefl (a : nat) : ¬ a < a :=
|
||||
rec_on a
|
||||
!not_lt_zero
|
||||
(λ (a : nat) (ih : ¬ a < a) (h : succ a < succ a),
|
||||
ih (lt.cancel_succ_left_right h))
|
||||
ih (lt.of_succ_lt_succ h))
|
||||
|
||||
definition lt.asymm {a b : nat} (H : a < b) : ¬ b < a :=
|
||||
lt.rec_on H
|
||||
(λ h : succ a < a, !lt.irrefl (lt.cancel_succ_left h))
|
||||
(λ b hlt (ih : ¬ b < a) (h : succ b < a), ih (lt.cancel_succ_left 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 :=
|
||||
rec_on b
|
||||
|
|
@ -160,74 +177,70 @@ namespace nat
|
|||
(λ b₁ (ih : ∀a, a < b₁ ∨ a = b₁ ∨ b₁ < a) (a : nat), cases_on a
|
||||
(or.inl !zero_lt_succ)
|
||||
(λ a, or.rec_on (ih a)
|
||||
(λ h : a < b₁, or.inl (lt.imp_succ h))
|
||||
(λ h : a < b₁, or.inl (lt.succ_of_lt h))
|
||||
(λ h, or.rec_on h
|
||||
(λ h : a = b₁, or.inr (or.inl (eq.rec_on h rfl)))
|
||||
(λ h : b₁ < a, or.inr (or.inr (lt.imp_succ h))))))
|
||||
(λ h : b₁ < a, or.inr (or.inr (lt.succ_of_lt h))))))
|
||||
a
|
||||
|
||||
definition not_lt {a b : nat} (hnlt : ¬ a < b) : a = b ∨ b < a :=
|
||||
definition 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 le_imp_lt_succ {a b : nat} (h : a ≤ b) : a < succ b :=
|
||||
le.rec_on h
|
||||
(lt.base a)
|
||||
(λ b h, lt.step h)
|
||||
definition lt_succ_of_le {a b : nat} (h : a ≤ b) : a < succ b :=
|
||||
h
|
||||
|
||||
definition le_succ_imp_lt {a b : nat} (h : succ a ≤ b) : a < b :=
|
||||
le.rec_on h
|
||||
(lt.base a)
|
||||
(λ b (h : succ a < b), lt.cancel_succ_left_right (lt.step h))
|
||||
definition lt_of_succ_le {a b : nat} (h : succ a ≤ b) : a < b :=
|
||||
lt.of_succ_lt_succ h
|
||||
|
||||
definition le.step {a b : nat} (h : a ≤ b) : a ≤ succ b :=
|
||||
le.rec_on h
|
||||
(le.of_lt (lt.base a))
|
||||
(λ b (h : a < b), le.of_lt (lt.step h))
|
||||
lt.step h
|
||||
|
||||
definition lt_imp_le_succ {a b : nat} (h : a < b) : succ a ≤ b :=
|
||||
lt.rec_on h
|
||||
(le.refl (succ a))
|
||||
(λ b hlt (ih : succ a ≤ b), le.step ih)
|
||||
definition succ_le_of_lt {a b : nat} (h : a < b) : succ a ≤ b :=
|
||||
lt.succ_of_lt h
|
||||
|
||||
definition le.trans {a b c : nat} (h₁ : a ≤ b) : b ≤ c → a ≤ c :=
|
||||
le.rec_on h₁
|
||||
(λ h, h)
|
||||
(λ b (h₁ : a < b) (h₂ : b ≤ c), le.rec_on h₂
|
||||
(le.of_lt h₁)
|
||||
(λ c (h₂ : b < c), le.of_lt (lt.trans h₁ h₂)))
|
||||
definition le.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 le_lt.trans {a b c : nat} (h₁ : a ≤ b) : b < c → a < c :=
|
||||
le.rec_on h₁
|
||||
(λ h, h)
|
||||
(λ b (h₁ : a < b) (h₂ : b < c), lt.trans h₁ h₂)
|
||||
definition lt.of_le_of_lt {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_le.trans {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
|
||||
le.rec_on h₂
|
||||
h₁
|
||||
(λ c (h₂ : b < c), lt.trans h₁ h₂)
|
||||
definition lt.of_lt_of_le {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₂),
|
||||
apply (lt.trans hlt (lt.of_succ_lt_succ h₂))
|
||||
end
|
||||
|
||||
definition lt_eq.trans {a b c : nat} (h₁ : a < b) (h₂ : b = c) : a < c :=
|
||||
definition lt.of_lt_of_eq {a b c : nat} (h₁ : a < b) (h₂ : b = c) : a < c :=
|
||||
eq.rec_on h₂ h₁
|
||||
|
||||
definition le_eq.trans {a b c : nat} (h₁ : a ≤ b) (h₂ : b = c) : a ≤ c :=
|
||||
definition le.of_le_of_eq {a b c : nat} (h₁ : a ≤ b) (h₂ : b = c) : a ≤ c :=
|
||||
eq.rec_on h₂ h₁
|
||||
|
||||
definition eq_lt.trans {a b c : nat} (h₁ : a = b) (h₂ : b < c) : a < c :=
|
||||
definition lt.of_eq_of_lt {a b c : nat} (h₁ : a = b) (h₂ : b < c) : a < c :=
|
||||
eq.rec_on (eq.rec_on h₁ rfl) h₂
|
||||
|
||||
definition eq_le.trans {a b c : nat} (h₁ : a = b) (h₂ : b ≤ c) : a ≤ c :=
|
||||
definition le.of_eq_of_le {a b c : nat} (h₁ : a = b) (h₂ : b ≤ c) : a ≤ c :=
|
||||
eq.rec_on (eq.rec_on h₁ rfl) h₂
|
||||
|
||||
calc_trans lt.trans
|
||||
calc_trans lt.of_le_of_lt
|
||||
calc_trans lt.of_lt_of_le
|
||||
calc_trans lt.of_lt_of_eq
|
||||
calc_trans lt.of_eq_of_lt
|
||||
calc_trans le.trans
|
||||
calc_trans le_lt.trans
|
||||
calc_trans lt_le.trans
|
||||
calc_trans lt_eq.trans
|
||||
calc_trans le_eq.trans
|
||||
calc_trans eq_lt.trans
|
||||
calc_trans eq_le.trans
|
||||
calc_trans le.of_le_of_eq
|
||||
calc_trans le.of_eq_of_le
|
||||
|
||||
definition max (a b : nat) : nat :=
|
||||
if a < b then b else a
|
||||
|
|
@ -244,24 +257,24 @@ namespace nat
|
|||
definition max.eq_left {a b : nat} (H : ¬ a < b) : max a b = a :=
|
||||
if_neg H
|
||||
|
||||
definition max.eq_right_symm {a b : nat} (H : a < b) : b = max a b :=
|
||||
definition max.right_eq {a b : nat} (H : a < b) : b = max a b :=
|
||||
eq.rec_on (max.eq_right H) rfl
|
||||
|
||||
definition max.eq_left_symm {a b : nat} (H : ¬ a < b) : a = max a b :=
|
||||
definition max.left_eq {a b : nat} (H : ¬ a < b) : a = max a b :=
|
||||
eq.rec_on (max.eq_left H) rfl
|
||||
|
||||
definition max.left (a b : nat) : a ≤ max a b :=
|
||||
by_cases
|
||||
(λ h : a < b, le.of_lt (eq.rec_on (max.eq_right_symm h) h))
|
||||
(λ h : a < b, le.of_lt (eq.rec_on (max.right_eq h) h))
|
||||
(λ h : ¬ a < b, eq.rec_on (max.eq_left h) !le.refl)
|
||||
|
||||
definition max.right (a b : nat) : b ≤ max a b :=
|
||||
by_cases
|
||||
(λ h : a < b, eq.rec_on (max.eq_right h) !le.refl)
|
||||
(λ h : ¬ a < b, or.rec_on (not_lt h)
|
||||
(λ h : ¬ a < b, or.rec_on (eq_or_lt_of_not_lt h)
|
||||
(λ heq, eq.rec_on heq (eq.rec_on (max_a_a a) !le.refl))
|
||||
(λ h : b < a,
|
||||
have aux : a = max a b, from max.eq_left_symm (lt.asymm h),
|
||||
have aux : a = max a b, from max.left_eq (lt.asymm h),
|
||||
eq.rec_on aux (le.of_lt h)))
|
||||
|
||||
definition gt a b := lt b a
|
||||
|
|
@ -287,23 +300,23 @@ namespace nat
|
|||
|
||||
notation a * b := mul a b
|
||||
|
||||
definition sub.succ_succ (a b : nat) : succ a - succ b = a - b :=
|
||||
definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
|
||||
induction_on b
|
||||
rfl
|
||||
(λ b₁ (ih : succ a - succ b₁ = a - b₁),
|
||||
eq.rec_on ih (eq.refl (pred (succ a - succ b₁))))
|
||||
|
||||
definition sub.succ_succ_symm (a b : nat) : a - b = succ a - succ b :=
|
||||
eq.rec_on (sub.succ_succ a b) rfl
|
||||
definition 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 sub.zero_left (a : nat) : zero - a = zero :=
|
||||
definition zero_sub_eq_zero (a : nat) : zero - a = zero :=
|
||||
induction_on a
|
||||
rfl
|
||||
(λ a₁ (ih : zero - a₁ = zero),
|
||||
eq.rec_on ih (eq.refl (pred (zero - a₁))))
|
||||
|
||||
definition sub.zero_left_symm (a : nat) : zero = zero - a :=
|
||||
eq.rec_on (sub.zero_left a) rfl
|
||||
definition 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 :=
|
||||
have aux : Π {a}, zero < a → Π {b}, zero < b → a - b < a, from
|
||||
|
|
@ -311,23 +324,23 @@ namespace nat
|
|||
(λb h₂, lt.cases_on h₂
|
||||
(lt.base zero)
|
||||
(λ b₁ bpos,
|
||||
eq.rec_on (sub.succ_succ_symm zero b₁)
|
||||
(eq.rec_on (sub.zero_left_symm b₁) (lt.base zero))))
|
||||
eq.rec_on (sub_eq_succ_sub_succ zero b₁)
|
||||
(eq.rec_on (zero_eq_zero_sub b₁) (lt.base zero))))
|
||||
(λa₁ apos ih b h₂, lt.cases_on h₂
|
||||
(lt.base a₁)
|
||||
(λ b₁ bpos,
|
||||
eq.rec_on (sub.succ_succ_symm a₁ b₁)
|
||||
eq.rec_on (sub_eq_succ_sub_succ a₁ b₁)
|
||||
(lt.trans (@ih b₁ bpos) (lt.base a₁)))),
|
||||
λ h₁ h₂, aux h₁ h₂
|
||||
|
||||
definition sub_pred (a : nat) : pred a ≤ a :=
|
||||
definition pred_le (a : nat) : pred a ≤ a :=
|
||||
cases_on a
|
||||
(le.refl zero)
|
||||
(λ a₁, le.of_lt (lt.base a₁))
|
||||
|
||||
definition sub_le_self (a b : nat) : a - b ≤ a :=
|
||||
definition sub_le (a b : nat) : a - b ≤ a :=
|
||||
induction_on b
|
||||
(le.refl a)
|
||||
(λ b₁ ih, le.trans !sub_pred ih)
|
||||
(λ b₁ ih, le.trans !pred_le ih)
|
||||
|
||||
end nat
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ namespace nat
|
|||
-- Auxiliary lemma used to justify div
|
||||
private definition div_rec_lemma {x y : nat} (H : 0 < y ∧ y ≤ x) : x - y < x :=
|
||||
and.rec_on H (λ ypos ylex,
|
||||
sub.lt (lt_le.trans ypos ylex) ypos)
|
||||
sub.lt (lt.of_lt_of_le ypos ylex) ypos)
|
||||
|
||||
private definition div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
|
||||
dif 0 < y ∧ y ≤ x then (λ Hp, f (x - y) (div_rec_lemma Hp) y + 1) else (λ Hn, zero)
|
||||
|
|
@ -40,7 +40,7 @@ theorem div_less {a b : ℕ} (h : a < b) : a div b = 0 :=
|
|||
divide_def a b ⬝ if_neg (!and.not_right (lt_imp_not_ge h))
|
||||
|
||||
theorem zero_div (b : ℕ) : 0 div b = 0 :=
|
||||
divide_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_le.trans l r) (lt.irrefl 0)))
|
||||
divide_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt.of_lt_of_le l r) (lt.irrefl 0)))
|
||||
|
||||
theorem div_rec {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a div b = succ ((a - b) div b) :=
|
||||
divide_def a b ⬝ if_pos (and.intro h₁ h₂)
|
||||
|
|
@ -80,7 +80,7 @@ theorem mod_less {a b : ℕ} (h : a < b) : a mod b = a :=
|
|||
modulo_def a b ⬝ if_neg (!and.not_right (lt_imp_not_ge h))
|
||||
|
||||
theorem zero_mod (b : ℕ) : 0 mod b = 0 :=
|
||||
modulo_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt_le.trans l r) (lt.irrefl 0)))
|
||||
modulo_def 0 b ⬝ if_neg (λ h, and.rec_on h (λ l r, absurd (lt.of_lt_of_le l r) (lt.irrefl 0)))
|
||||
|
||||
theorem mod_rec {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a mod b = (a - b) mod b :=
|
||||
modulo_def a b ⬝ if_pos (and.intro h₁ h₂)
|
||||
|
|
@ -187,7 +187,7 @@ theorem quotient_unique {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y)
|
|||
(H3 : q1 * y + r1 = q2 * y + r2) : q1 = q2 :=
|
||||
have H4 : q1 * y + r2 = q2 * y + r2, from (remainder_unique H H1 H2 H3) ▸ H3,
|
||||
have H5 : q1 * y = q2 * y, from add.cancel_right H4,
|
||||
have H6 : y > 0, from le_lt.trans !zero_le H1,
|
||||
have H6 : y > 0, from lt.of_le_of_lt !zero_le H1,
|
||||
show q1 = q2, from mul_cancel_right H6 H5
|
||||
|
||||
theorem div_mul_mul {z x y : ℕ} (zpos : z > 0) : (z * x) div (z * y) = x div y :=
|
||||
|
|
@ -256,7 +256,7 @@ definition dvd (x y : ℕ) : Prop := y mod x = 0
|
|||
infix `|` := dvd
|
||||
|
||||
theorem dvd_iff_mod_eq_zero {x y : ℕ} : x | y ↔ y mod x = 0 :=
|
||||
eq_to_iff rfl
|
||||
iff.of_eq rfl
|
||||
|
||||
theorem dvd_imp_div_mul_eq {x y : ℕ} (H : y | x) : x div y * y = x :=
|
||||
(calc
|
||||
|
|
|
|||
|
|
@ -17,9 +17,7 @@ namespace nat
|
|||
-- ------------------
|
||||
|
||||
theorem le.succ_right {n m : ℕ} (h : n ≤ m) : n ≤ succ m :=
|
||||
le.rec_on h
|
||||
(le.of_lt (lt.base n))
|
||||
(λ b (h : n < b), le.of_lt (lt.step h))
|
||||
lt.step h
|
||||
|
||||
theorem le.add_right (n k : ℕ) : n ≤ n + k :=
|
||||
induction_on k
|
||||
|
|
@ -179,7 +177,7 @@ case n
|
|||
(pred.zero⁻¹ ▸ !le_refl)
|
||||
(take k : ℕ, !pred.succ⁻¹ ▸ !self_le_succ)
|
||||
|
||||
theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
|
||||
theorem pred_le_pre_of_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
|
||||
discriminate
|
||||
(take Hn : n = 0,
|
||||
have H2 : pred n = 0,
|
||||
|
|
@ -237,10 +235,10 @@ le_trans (mul_le_right H1 m) (mul_le_left H2 k)
|
|||
-- ----------------------------------------------
|
||||
|
||||
theorem lt_intro {n m k : ℕ} (H : succ n + k = m) : n < m :=
|
||||
le_succ_imp_lt (le_intro H)
|
||||
lt_of_succ_le (le_intro H)
|
||||
|
||||
theorem lt_elim {n m : ℕ} (H : n < m) : ∃ k, succ n + k = m :=
|
||||
le_elim (lt_imp_le_succ H)
|
||||
le_elim (succ_le_of_lt H)
|
||||
|
||||
theorem lt_add_succ (n m : ℕ) : n < n + succ m :=
|
||||
lt_intro !add.move_succ
|
||||
|
|
@ -255,8 +253,8 @@ not_intro (assume H : n < n, absurd rfl (lt_imp_ne H))
|
|||
|
||||
theorem lt_def (n m : ℕ) : n < m ↔ succ n ≤ m :=
|
||||
iff.intro
|
||||
(λ h, lt_imp_le_succ h)
|
||||
(λ h, le_succ_imp_lt h)
|
||||
(λ h, succ_le_of_lt h)
|
||||
(λ h, lt_of_succ_le h)
|
||||
|
||||
theorem succ_pos (n : ℕ) : 0 < succ n :=
|
||||
!zero_lt_succ
|
||||
|
|
@ -275,13 +273,13 @@ theorem lt_imp_le {n m : ℕ} (H : n < m) : n ≤ m :=
|
|||
le.of_lt H
|
||||
|
||||
theorem le_imp_lt_or_eq {n m : ℕ} (H : n ≤ m) : n < m ∨ n = m :=
|
||||
or.swap (le_def_right H)
|
||||
or.swap (eq_or_lt_of_le H)
|
||||
|
||||
theorem le_ne_imp_lt {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : n < m :=
|
||||
or.resolve_left (le_imp_lt_or_eq H1) H2
|
||||
|
||||
theorem lt_succ_imp_le {n m : ℕ} (H : n < succ m) : n ≤ m :=
|
||||
succ_le_cancel (lt_imp_le_succ H)
|
||||
succ_le_cancel (succ_le_of_lt H)
|
||||
|
||||
theorem le_imp_not_gt {n m : ℕ} (H : n ≤ m) : ¬ n > m :=
|
||||
le.rec_on H
|
||||
|
|
@ -289,7 +287,7 @@ le.rec_on H
|
|||
(λ m (h : n < m), lt.asymm h)
|
||||
|
||||
theorem lt_imp_not_ge {n m : ℕ} (H : n < m) : ¬ n ≥ m :=
|
||||
not_intro (assume H2 : m ≤ n, absurd (lt_le.trans H H2) !lt_irrefl)
|
||||
not_intro (assume H2 : m ≤ n, absurd (lt.of_lt_of_le H H2) !lt_irrefl)
|
||||
|
||||
theorem lt_antisym {n m : ℕ} (H : n < m) : ¬ m < n :=
|
||||
lt.asymm H
|
||||
|
|
@ -299,22 +297,22 @@ lt.asymm H
|
|||
-- ### interaction with addition
|
||||
|
||||
theorem add_lt_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m :=
|
||||
le_succ_imp_lt (!add.succ_right ▸ add_le_left (lt_imp_le_succ H) k)
|
||||
lt_of_succ_le (!add.succ_right ▸ add_le_left (succ_le_of_lt H) k)
|
||||
|
||||
theorem add_lt_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k :=
|
||||
!add.comm ▸ !add.comm ▸ add_lt_left H k
|
||||
|
||||
theorem add_le_lt {n m k l : ℕ} (H1 : n ≤ k) (H2 : m < l) : n + m < k + l :=
|
||||
le_lt.trans (add_le_right H1 m) (add_lt_left H2 k)
|
||||
lt.of_le_of_lt (add_le_right H1 m) (add_lt_left H2 k)
|
||||
|
||||
theorem add_lt_le {n m k l : ℕ} (H1 : n < k) (H2 : m ≤ l) : n + m < k + l :=
|
||||
lt_le.trans (add_lt_right H1 m) (add_le_left H2 k)
|
||||
lt.of_lt_of_le (add_lt_right H1 m) (add_le_left H2 k)
|
||||
|
||||
theorem add_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n + m < k + l :=
|
||||
add_lt_le H1 (lt_imp_le H2)
|
||||
|
||||
theorem add_lt_cancel_left {n m k : ℕ} (H : k + n < k + m) : n < m :=
|
||||
le_succ_imp_lt (add_le_cancel_left (!add.succ_right⁻¹ ▸ (lt_imp_le_succ H)))
|
||||
lt_of_succ_le (add_le_cancel_left (!add.succ_right⁻¹ ▸ (succ_le_of_lt H)))
|
||||
|
||||
theorem add_lt_cancel_right {n m k : ℕ} (H : n + k < m + k) : n < m :=
|
||||
add_lt_cancel_left (!add.comm ▸ !add.comm ▸ H)
|
||||
|
|
@ -386,7 +384,7 @@ strong_induction_on a (
|
|||
(take n,
|
||||
assume H : (∀m, m < succ n → P m),
|
||||
show P (succ n), from
|
||||
Hind n (take m, assume H1 : m ≤ n, H _ (le_imp_lt_succ H1))))
|
||||
Hind n (take m, assume H1 : m ≤ n, H _ (lt_succ_of_le H1))))
|
||||
|
||||
-- Positivity
|
||||
-- ---------
|
||||
|
|
@ -452,22 +450,22 @@ mul_pos_imp_pos_left (!mul.comm ▸ H)
|
|||
|
||||
theorem mul_lt_left {n m k : ℕ} (Hk : k > 0) (H : n < m) : k * n < k * m :=
|
||||
have H2 : k * n < k * n + k, from add_pos_right Hk,
|
||||
have H3 : k * n + k ≤ k * m, from !mul.succ_right ▸ mul_le_left (lt_imp_le_succ H) k,
|
||||
lt_le.trans H2 H3
|
||||
have H3 : k * n + k ≤ k * m, from !mul.succ_right ▸ mul_le_left (succ_le_of_lt H) k,
|
||||
lt.of_lt_of_le H2 H3
|
||||
|
||||
theorem mul_lt_right {n m k : ℕ} (Hk : k > 0) (H : n < m) : n * k < m * k :=
|
||||
!mul.comm ▸ !mul.comm ▸ mul_lt_left Hk H
|
||||
|
||||
theorem mul_le_lt {n m k l : ℕ} (Hk : k > 0) (H1 : n ≤ k) (H2 : m < l) : n * m < k * l :=
|
||||
le_lt.trans (mul_le_right H1 m) (mul_lt_left Hk H2)
|
||||
lt.of_le_of_lt (mul_le_right H1 m) (mul_lt_left Hk H2)
|
||||
|
||||
theorem mul_lt_le {n m k l : ℕ} (Hl : l > 0) (H1 : n < k) (H2 : m ≤ l) : n * m < k * l :=
|
||||
le_lt.trans (mul_le_left H2 n) (mul_lt_right Hl H1)
|
||||
lt.of_le_of_lt (mul_le_left H2 n) (mul_lt_right Hl H1)
|
||||
|
||||
theorem mul_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l :=
|
||||
have H3 : n * m ≤ k * m, from mul_le_right (lt_imp_le H1) m,
|
||||
have H4 : k * m < k * l, from mul_lt_left (le_lt.trans !zero_le H1) H2,
|
||||
le_lt.trans H3 H4
|
||||
have H4 : k * m < k * l, from mul_lt_left (lt.of_le_of_lt !zero_le H1) H2,
|
||||
lt.of_le_of_lt H3 H4
|
||||
|
||||
theorem mul_lt_cancel_left {n m k : ℕ} (H : k * n < k * m) : n < m :=
|
||||
or.elim le_or_gt
|
||||
|
|
@ -480,7 +478,7 @@ theorem mul_lt_cancel_right {n m k : ℕ} (H : n * k < m * k) : n < m :=
|
|||
mul_lt_cancel_left (!mul.comm ▸ !mul.comm ▸ H)
|
||||
|
||||
theorem mul_le_cancel_left {n m k : ℕ} (Hk : k > 0) (H : k * n ≤ k * m) : n ≤ m :=
|
||||
have H2 : k * n < k * m + k, from le_lt.trans H (add_pos_right Hk),
|
||||
have H2 : k * n < k * m + k, from lt.of_le_of_lt H (add_pos_right Hk),
|
||||
have H3 : k * n < k * succ m, from !mul.succ_right⁻¹ ▸ H2,
|
||||
have H4 : n < succ m, from mul_lt_cancel_left H3,
|
||||
show n ≤ m, from lt_succ_imp_le H4
|
||||
|
|
@ -511,9 +509,9 @@ have H3 : n > 0, from mul_pos_imp_pos_left H2,
|
|||
have H4 : m > 0, from mul_pos_imp_pos_right H2,
|
||||
or.elim le_or_gt
|
||||
(assume H5 : n ≤ 1,
|
||||
show n = 1, from le_antisym H5 (lt_imp_le_succ H3))
|
||||
show n = 1, from le_antisym H5 (succ_le_of_lt H3))
|
||||
(assume H5 : n > 1,
|
||||
have H6 : n * m ≥ 2 * 1, from mul_le (lt_imp_le_succ H5) (lt_imp_le_succ H4),
|
||||
have H6 : n * m ≥ 2 * 1, from mul_le (succ_le_of_lt H5) (succ_le_of_lt H4),
|
||||
have H7 : 1 ≥ 2, from !mul.one_right ▸ H ▸ H6,
|
||||
absurd !self_lt_succ (le_imp_not_gt H7))
|
||||
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@ induction_on n !sub_zero_right
|
|||
... = 0 : pred.zero)
|
||||
|
||||
theorem sub_succ_succ (n m : ℕ) : succ n - succ m = n - m :=
|
||||
sub.succ_succ n m
|
||||
succ_sub_succ_eq_sub n m
|
||||
|
||||
theorem sub_self (n : ℕ) : n - n = 0 :=
|
||||
induction_on n !sub_zero_right (take k IH, !sub_succ_succ ⬝ IH)
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ have H3 : ∀c, R a c ↔ R b c, from
|
|||
(assume H4 : R a c, transR (symmR H2) H4)
|
||||
(assume H4 : R b c, transR H2 H4),
|
||||
have H4 : (fun c, R a c) = (fun c, R b c), from
|
||||
funext (take c, iff_to_eq (H3 c)),
|
||||
funext (take c, eq.of_iff (H3 c)),
|
||||
have H5 [visible] : nonempty A, from
|
||||
nonempty.intro a,
|
||||
show epsilon (λc, R a c) = epsilon (λc, R b c), from
|
||||
|
|
|
|||
|
|
@ -41,17 +41,17 @@ or.elim (prop_complete a)
|
|||
(assume Hbt, false_elim (Haf ▸ (Hba (eq_true_elim Hbt))))
|
||||
(assume Hbf, Haf ⬝ Hbf⁻¹))
|
||||
|
||||
theorem iff_to_eq {a b : Prop} (H : a ↔ b) : a = b :=
|
||||
theorem eq.of_iff {a b : Prop} (H : a ↔ b) : a = b :=
|
||||
iff.elim (assume H1 H2, propext H1 H2) H
|
||||
|
||||
theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) :=
|
||||
propext
|
||||
(assume H, iff_to_eq H)
|
||||
(assume H, eq_to_iff H)
|
||||
(assume H, eq.of_iff H)
|
||||
(assume H, iff.of_eq H)
|
||||
|
||||
open relation
|
||||
theorem iff_congruence [instance] (P : Prop → Prop) : is_congruence iff iff P :=
|
||||
is_congruence.mk
|
||||
(take (a b : Prop),
|
||||
assume H : a ↔ b,
|
||||
show P a ↔ P b, from eq_to_iff (iff_to_eq H ▸ eq.refl (P a)))
|
||||
show P a ↔ P b, from iff.of_eq (eq.of_iff H ▸ eq.refl (P a)))
|
||||
|
|
|
|||
|
|
@ -152,16 +152,15 @@ namespace iff
|
|||
|
||||
theorem false_elim (H : a ↔ false) : ¬a :=
|
||||
assume Ha : a, mp H Ha
|
||||
|
||||
open eq.ops
|
||||
theorem of_eq {a b : Prop} (H : a = b) : a ↔ b :=
|
||||
iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
|
||||
end iff
|
||||
|
||||
calc_refl iff.refl
|
||||
calc_trans iff.trans
|
||||
|
||||
open eq.ops
|
||||
|
||||
theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b :=
|
||||
iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
|
||||
|
||||
-- comm and assoc for and / or
|
||||
-- ---------------------------
|
||||
namespace and
|
||||
|
|
|
|||
|
|
@ -83,7 +83,7 @@ namespace decidable
|
|||
(assume Hnp : ¬p, inr (iff.elim_left (iff.flip_sign H) Hnp))
|
||||
|
||||
definition decidable_eq_equiv (Hp : decidable p) (H : p = q) : decidable q :=
|
||||
decidable_iff_equiv Hp (eq_to_iff H)
|
||||
decidable_iff_equiv Hp (iff.of_eq H)
|
||||
|
||||
protected theorem rec_subsingleton [instance] [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type}
|
||||
(H3 : Π(h : p), subsingleton (H1 h)) (H4 : Π(h : ¬p), subsingleton (H2 h))
|
||||
|
|
|
|||
|
|
@ -78,7 +78,7 @@ case_strong_induction_on m
|
|||
assume Hzx : measure z < measure x,
|
||||
calc
|
||||
f' m z = restrict default measure f m z : IH m !le_refl z
|
||||
... = f z : !restrict_lt_eq (lt_le.trans Hzx (lt_succ_imp_le H1))
|
||||
... = f z : !restrict_lt_eq (lt.of_lt_of_le Hzx (lt_succ_imp_le H1))
|
||||
∎,
|
||||
have H2 : f' (succ m) x = rec_val x f,
|
||||
proof
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@ open nat well_founded decidable prod eq.ops
|
|||
-- Auxiliary lemma used to justify recursive call
|
||||
private definition lt_aux {x y : nat} (H : 0 < y ∧ y ≤ x) : x - y < x :=
|
||||
and.rec_on H (λ ypos ylex,
|
||||
sub.lt (lt_le.trans ypos ylex) ypos)
|
||||
sub.lt (lt.of_lt_of_le ypos ylex) ypos)
|
||||
|
||||
definition wdiv.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
|
||||
dif 0 < y ∧ y ≤ x then (λ Hp, f (x - y) (lt_aux Hp) y + 1) else (λ Hn, zero)
|
||||
|
|
|
|||
|
|
@ -42,12 +42,12 @@ aux
|
|||
|
||||
definition tree_forest.height_lt.cons₁ {A : Type} (t : tree A) (f : forest A) : sum.inl _ t ≺ sum.inr _ (forest.cons t f) :=
|
||||
have aux : tree.height t < forest.height (forest.cons t f), from
|
||||
le_imp_lt_succ (max.left _ _),
|
||||
lt_succ_of_le (max.left _ _),
|
||||
aux
|
||||
|
||||
definition tree_forest.height_lt.cons₂ {A : Type} (t : tree A) (f : forest A) : sum.inr _ f ≺ sum.inr _ (forest.cons t f) :=
|
||||
have aux : forest.height f < forest.height (forest.cons t f), from
|
||||
le_imp_lt_succ (max.right _ _),
|
||||
lt_succ_of_le (max.right _ _),
|
||||
aux
|
||||
|
||||
definition kind {A : Type} (t : tree_forest A) : bool :=
|
||||
|
|
|
|||
|
|
@ -11,11 +11,11 @@ infixl `≺`:50 := pair_nat.lt
|
|||
|
||||
-- Lemma for justifying recursive call
|
||||
private lemma lt₁ (x₁ y₁ : nat) : (x₁ - y₁, succ y₁) ≺ (succ x₁, succ y₁) :=
|
||||
!lex.left (le_imp_lt_succ (sub_le_self x₁ y₁))
|
||||
!lex.left (lt_succ_of_le (sub_le x₁ y₁))
|
||||
|
||||
-- Lemma for justifying recursive call
|
||||
private lemma lt₂ (x₁ y₁ : nat) : (succ x₁, y₁ - x₁) ≺ (succ x₁, succ y₁) :=
|
||||
!lex.right (le_imp_lt_succ (sub_le_self y₁ x₁))
|
||||
!lex.right (lt_succ_of_le (sub_le y₁ x₁))
|
||||
|
||||
definition gcd.F (p₁ : nat × nat) : (Π p₂ : nat × nat, p₂ ≺ p₁ → nat) → nat :=
|
||||
prod.cases_on p₁ (λ (x y : nat),
|
||||
|
|
|
|||
|
|
@ -19,10 +19,10 @@ definition height_lt.wf (A : Type) : well_founded (@height_lt A) :=
|
|||
inv_image.wf height lt.wf
|
||||
|
||||
theorem height_lt.node_left {A : Type} (t₁ t₂ : tree A) : height_lt t₁ (node t₁ t₂) :=
|
||||
le_imp_lt_succ (max.left (height t₁) (height t₂))
|
||||
lt_succ_of_le (max.left (height t₁) (height t₂))
|
||||
|
||||
theorem height_lt.node_right {A : Type} (t₁ t₂ : tree A) : height_lt t₂ (node t₁ t₂) :=
|
||||
le_imp_lt_succ (max.right (height t₁) (height t₂))
|
||||
lt_succ_of_le (max.right (height t₁) (height t₂))
|
||||
|
||||
theorem height_lt.trans {A : Type} : transitive (@height_lt A) :=
|
||||
inv_image.trans lt height @lt.trans
|
||||
|
|
|
|||
Loading…
Reference in a new issue