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

refactor(library/init/nat): rename constants

Browse source 
closes #387
This commit is contained in:
Leonardo de Moura 2015-01-07 18:26:51 -08:00
parent 42c328e781
commit 1fab144aa7
9 changed files with 62 additions and 71 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/data/fin.lean
View file

@ -54,13 +54,13 @@ namespace fin
of_nat 0 0 h := absurd h (not_lt_zero zero),
of_nat 0 (n+1) h := fz n,
of_nat (p+1) 0 h := absurd h (not_lt_zero (succ p)),
of_nat (p+1) (n+1) h := fs (of_nat p n (lt.of_succ_lt_succ h))
of_nat (p+1) (n+1) h := fs (of_nat p n (lt_of_succ_lt_succ h))
theorem of_nat_zero_succ (n : nat) (h : 0 < n+1) : of_nat 0 (n+1) h = fz n :=
rfl
theorem of_nat_succ_succ (p n : nat) (h : p+1 < n+1) :
of_nat (p+1) (n+1) h = fs (of_nat p n (lt.of_succ_lt_succ h)) :=
of_nat (p+1) (n+1) h = fs (of_nat p n (lt_of_succ_lt_succ h)) :=
rfl
theorem to_nat_of_nat : ∀ (p : nat) (n : nat) (h : p < n), to_nat (of_nat p n h) = p,

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

@ -222,7 +222,7 @@ or.elim (@le_or_gt n m)
H1⁻¹ ▸
(calc
0 + n = n : zero_add
... = n - m + m : add_sub_ge_left (le.of_lt H)
... = n - m + m : add_sub_ge_left (le_of_lt H)
... = succ (pred (n - m)) + m : (succ_pred_of_pos (sub_pos_of_gt H))⁻¹))
theorem repr_abstr (p : ℕ × ℕ) : repr (abstr p) ≡ p :=
@ -251,7 +251,7 @@ or.elim (equiv_cases Hequiv)
calc
pr2 p = pr2 p + pr1 q - pr1 q : sub_add_left
... = pr1 p + pr2 q - pr1 q : Hequiv
... = pr1 p + (pr2 q - pr1 q) : add_sub_assoc (le.of_lt H4)
... = pr1 p + (pr2 q - pr1 q) : add_sub_assoc (le_of_lt H4)
... = pr2 q - pr1 q + pr1 p : add.comm,
have H6 : pr2 p - pr1 p = pr2 q - pr1 q, from
calc
@ -290,7 +290,7 @@ or.elim (@le_or_gt n m)
nat_abs (abstr (m, n)) = nat_abs (neg_succ_of_nat (pred (n - m))) : int.abstr_of_lt H
... = succ (pred (n - m)) : rfl
... = n - m : succ_pred_of_pos (sub_pos_of_gt H)
... = dist m n : dist_le (le.of_lt H))
... = dist m n : dist_le (le_of_lt H))
theorem cases_of_nat (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - of_nat n) :=
cases_on a

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

@ -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.of_lt_of_le 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 :=
if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y + 1 else zero
@ -40,7 +40,7 @@ theorem div_less {a b : ℕ} (h : a < b) : a div b = 0 :=
divide_def a b ⬝ if_neg (!not_and_of_not_right (not_le_of_lt h))
theorem zero_div (b : ℕ) : 0 div b = 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)))
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 (!not_and_of_not_right (not_le_of_lt h))
theorem zero_mod (b : ℕ) : 0 mod b = 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)))
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 lt.of_le_of_lt !zero_le H1,
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
theorem div_mul_mul {z x y : ℕ} (zpos : z > 0) : (z * x) div (z * y) = x div y :=
@ -351,7 +351,7 @@ by_cases
have H4 : n1 = n1 - n2 + n2, from (add_sub_ge_left H3)⁻¹,
show m | n1 - n2, from dvd_add_cancel_right (H4 ▸ H1) H2)
(assume H3 : ¬ (n1 ≥ n2),
have H4 : n1 - n2 = 0, from le_imp_sub_eq_zero (le.of_lt (lt_of_not_le H3)),
have H4 : n1 - n2 = 0, from le_imp_sub_eq_zero (le_of_lt (lt_of_not_le H3)),
show m | n1 - n2, from H4⁻¹ ▸ dvd_zero _)
-- Gcd and lcm

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

@ -16,7 +16,7 @@ namespace nat
/- lt and le -/
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)
or.elim H (take H1, le_of_lt H1) (take H1, H1 ▸ !le.refl)
theorem lt.by_cases {a b : ℕ} {P : Prop}
(H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
@ -28,7 +28,7 @@ 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)
(assume H1 : m > n, absurd (lt.of_le_of_lt H H1) !lt.irrefl)
(assume H1 : m > n, absurd (lt_of_le_of_lt H H1) !lt.irrefl)
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
@ -40,12 +40,9 @@ or.elim (lt_or_eq_of_le H1)
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 (le_of_lt H) (take H1, lt.irrefl _ (H1 ▸ H)))
(take H, lt_of_le_and_ne (and.elim_left H) (and.elim_right H))
theorem le_succ_of_le {n m : ℕ} (h : n ≤ m) : n ≤ succ m :=
lt.step h
theorem le_add_right (n k : ℕ) : n ≤ n + k :=
induction_on k
(calc n ≤ n : le.refl n
@ -73,9 +70,9 @@ le.rec_on h
theorem le.total {m n : ℕ} : m ≤ n ∨ n ≤ m :=
lt.by_cases
(assume H : m < n, or.inl (le.of_lt H))
(assume H : m < n, or.inl (le_of_lt H))
(assume H : m = n, or.inl (H ▸ !le.refl))
(assume H : m > n, or.inr (le.of_lt H))
(assume H : m > n, or.inr (le_of_lt H))
/- addition -/
@ -124,7 +121,7 @@ le.trans (mul_le_mul_right H1 m) (mul_le_mul_left H2 k)
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
lt_of_lt_of_le H2 H3
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
@ -337,9 +334,6 @@ lt.base n
theorem le_of_lt_succ {n m : ℕ} (H : n < succ m) : n ≤ m :=
le_of_succ_le_succ (succ_le_of_lt H)
theorem succ_lt_succ {n m : ℕ} (H : n < m) : succ n < succ m :=
!add_one ▸ !add_one ▸ add_lt_add_right H 1
/- other forms of induction -/
protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) :
@ -394,16 +388,16 @@ exists_eq_succ_of_lt H
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)
lt_of_le_of_lt (mul_le_mul_right H1 m) (mul_lt_mul_of_pos_left H2 Hk)
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)
lt_of_le_of_lt (mul_le_mul_left H2 n) (mul_lt_mul_of_pos_right H1 Hl)
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
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
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,

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

@ -273,9 +273,6 @@ have H2 : k - n + n = m + n, from
... = m + n : !add.comm,
add.cancel_right H2
theorem sub_lt {x y : ℕ} (xpos : x > 0) (ypos : y > 0) : x - y < x :=
sub.lt xpos ypos
theorem sub_le_right {n m : ℕ} (H : n ≤ m) (k : nat) : n - k ≤ m - k :=
obtain (l : ℕ) (Hl : n + l = m), from le.elim H,
or.elim !le.total
@ -307,7 +304,7 @@ sub_split
le.intro (add.cancel_right H4))
theorem sub_pos_of_gt {m n : ℕ} (H : n > m) : n - m > 0 :=
have H1 : n = n - m + m, from (add_sub_ge_left (le.of_lt H))⁻¹,
have H1 : n = n - m + m, from (add_sub_ge_left (le_of_lt H))⁻¹,
have H2 : 0 + m < n - m + m, from (zero_add m)⁻¹ ▸ H1 ▸ H,
!lt_of_add_lt_add_right H2

72
library/init/nat.lean
View file

@ -93,25 +93,25 @@ namespace nat
(λ b hl ih h₁ h₂, lt.step (ih h₁ h₂))),
aux H₂ rfl H₁
definition lt.succ_of_lt {a b : nat} (H : a < b) : succ a < succ b :=
definition 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 :=
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.of_succ_lt_succ {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.of_succ_lt hlt),
lt_of_succ_lt hlt),
aux
definition lt.is_decidable_rel [instance] : decidable_rel lt :=
@ -120,17 +120,17 @@ 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.succ_of_lt h_pos))
(λ h_pos : a < b₁, inl (succ_lt_succ h_pos))
(λ h_neg : ¬ a < b₁,
have aux : ¬ succ a < succ b₁, from
λ h : succ a < succ b₁, h_neg (lt.of_succ_lt_succ h),
λ h : succ a < succ b₁, h_neg (lt_of_succ_lt_succ h),
inr aux)))
a
definition le.refl (a : nat) : a ≤ a :=
lt.base a
definition le.of_lt {a b : nat} (H : 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 :=
@ -140,13 +140,13 @@ namespace nat
apply (or.inr hlt)
end
definition le.of_eq_or_lt {a b : nat} (H : a = b ∨ a < b) : a ≤ b :=
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)
(λ hr, le_of_lt hr)
definition le.is_decidable_rel [instance] : decidable_rel le :=
λ a b, decidable_of_decidable_of_iff _ (iff.intro le.of_eq_or_lt eq_or_lt_of_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 :=
begin
@ -159,12 +159,12 @@ namespace nat
rec_on a
!not_lt_zero
(λ (a : nat) (ih : ¬ a < a) (h : succ a < succ a),
ih (lt.of_succ_lt_succ 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.of_succ_lt h))
(λ b hlt (ih : ¬ b < a) (h : succ b < a), ih (lt.of_succ_lt 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
@ -174,10 +174,10 @@ 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.succ_of_lt h))
(λ h : a < b₁, or.inl (succ_lt_succ 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.succ_of_lt h))))))
(λ 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 :=
@ -189,13 +189,13 @@ namespace nat
h
definition lt_of_succ_le {a b : nat} (h : succ a ≤ b) : a < b :=
lt.of_succ_lt_succ h
lt_of_succ_lt_succ h
definition le.step {a b : nat} (h : a ≤ b) : a ≤ succ b :=
definition 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 :=
lt.succ_of_lt h
succ_lt_succ h
definition le.trans {a b c : nat} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
begin
@ -204,40 +204,40 @@ namespace nat
apply (lt.trans hlt h₂)
end
definition lt.of_le_of_lt {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
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.of_lt_of_le {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
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₂))
apply (lt_of_succ_lt_succ h₂),
apply (lt.trans hlt (lt_of_succ_lt_succ h₂))
end
definition lt.of_lt_of_eq {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.of_le_of_eq {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 lt.of_eq_of_lt {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 le.of_eq_of_le {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 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.of_le_of_eq
calc_trans le.of_eq_of_le
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
@ -262,7 +262,7 @@ namespace nat
definition max.left (a b : nat) : a ≤ max a b :=
by_cases
(λ h : a < b, le.of_lt (eq.rec_on (max.right_eq 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 :=
@ -272,7 +272,7 @@ namespace nat
(λ 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.left_eq (lt.asymm h),
eq.rec_on aux (le.of_lt h)))
eq.rec_on aux (le_of_lt h)))
definition gt a b := lt b a
@ -315,7 +315,7 @@ namespace nat
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 :=
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
λa h₁, lt.rec_on h₁
(λb h₂, lt.cases_on h₂
@ -333,7 +333,7 @@ namespace nat
definition pred_le (a : nat) : pred a ≤ a :=
cases_on a
(le.refl zero)
(λ a₁, le.of_lt (lt.base a₁))
(λ a₁, le_of_lt (lt.base a₁))
definition sub_le (a b : nat) : a - b ≤ a :=
induction_on b

2
tests/lean/run/div2.lean
View file

@ -80,7 +80,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.of_lt_of_le Hzx (le_of_lt_succ H1))
... = f z : !restrict_lt_eq (lt_of_lt_of_le Hzx (le_of_lt_succ H1))
∎,
have H2 : f' (succ m) x = rec_val x f,
proof

2
tests/lean/run/div_wf.lean
View file

@ -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.of_lt_of_le 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 :=
if H : 0 < y ∧ y ≤ x then f (x - y) (lt_aux H) y + 1 else zero

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

@ -9,9 +9,9 @@ nat.cases_on x
(λ x₁ (f : Π y, y < succ x₁ → Σ r : nat, r ≤ y),
let p₁ := f x₁ (lt.base x₁) in
let gx₁ := pr₁ p₁ in
let p₂ := f gx₁ (lt.of_le_of_lt (pr₂ p₁) (lt.base x₁)) in
let p₂ := f gx₁ (lt_of_le_of_lt (pr₂ p₁) (lt.base x₁)) in
let ggx₁ := pr₁ p₂ in
⟨ggx₁, le.step (le.trans (pr₂ p₂) (pr₂ p₁))⟩)
⟨ggx₁, le_succ_of_le (le.trans (pr₂ p₂) (pr₂ p₁))⟩)
definition g (x : nat) : nat :=
pr₁ (well_founded.fix g.F x)