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

refactor(library/data/nat): declare lt and le asap using inductive definitions, and make key theorems transparent for definitional package

Browse source 
We also define key theorems that will be used to generate the
automatically generated a well-founded subterm relation for inductive
datatypes.
We also prove decidability and wf theorems asap.
This commit is contained in:
Leonardo de Moura 2014-11-22 00:15:51 -08:00
parent 7c54dbce10
commit 064ecd3e3d
15 changed files with 426 additions and 350 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/data/fin.lean
View file

@ -74,8 +74,8 @@ namespace fin
to_nat (of_nat_core (succ p₁)) = succ (to_nat (of_nat_core p₁)) : rfl
... = succ p₁ : ih)
private lemma of_nat_eq {p : nat} {n : nat} (H : p < n) : n - succ p + succ p = n :=
add_sub_ge_left (eq.subst (lt_def p n) H)
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)
definition of_nat (p : nat) (n : nat) : p < n → fin n :=
λ H : p < n,

2
library/data/int/order.lean
View file

@ -235,7 +235,7 @@ theorem lt_of_nat (n m : ℕ) : (of_nat n < of_nat m) ↔ (n < m) :=
calc
(of_nat n + 1 ≤ of_nat m) ↔ (of_nat (succ n) ≤ of_nat m) : by simp
... ↔ (succ n ≤ m) : le_of_nat (succ n) m
... ↔ (n < m) : iff.symm (eq_to_iff (nat.lt_def n m))
... ↔ (n < m) : iff.symm (nat.lt_def n m)
theorem gt_of_nat (n m : ℕ) : (of_nat n > of_nat m) ↔ (n > m) :=
lt_of_nat m n

94
library/data/nat/basic.lean
View file

@ -1,44 +1,18 @@
--- Copyright (c) 2014 Floris van Doorn. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Floris van Doorn
--- Author: Floris van Doorn, Leonardo de Moura
-- data.nat.basic
-- ==============
--
-- Basic operations on the natural numbers.
import logic data.num tools.tactic algebra.binary tools.helper_tactics
import logic.inhabited
import .decl data.num algebra.binary
open tactic binary eq.ops
open decidable
open relation -- for subst_iff
open helper_tactics
-- Definition of the type
-- ----------------------
inductive nat : Type :=
zero : nat,
succ : nat → nat
open eq.ops binary
namespace nat
notation `ℕ` := nat
theorem rec_zero {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) : nat.rec x f zero = x
theorem rec_succ {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) (n : ℕ) :
nat.rec x f (succ n) = f n (nat.rec x f n)
protected definition is_inhabited [instance] : inhabited nat :=
inhabited.mk zero
-- Coercion from num
-- -----------------
definition add (x y : ℕ) : ℕ :=
nat.rec x (λ n r, succ r) y
notation a + b := add a b
definition of_num [coercion] [reducible] (n : num) : ℕ :=
num.rec zero
(λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
definition addl (x y : ℕ) : ℕ :=
nat.rec y (λ n r, succ r) x
@ -70,10 +44,6 @@ nat.induction_on x
... = succ (succ x₁ ⊕ y₁) : {ih₂}
... = succ x₁ ⊕ succ y₁ : addl.succ_right))
definition of_num [coercion] [reducible] (n : num) : ℕ :=
num.rec zero
(λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
-- Successor and predecessor
-- -------------------------
@ -82,11 +52,11 @@ assume H, no_confusion H
-- add_rewrite succ_ne_zero
definition pred (n : ℕ) := nat.rec 0 (fun m x, m) n
theorem pred.zero : pred 0 = 0 :=
rfl
theorem pred.zero : pred 0 = 0
theorem pred.succ (n : ℕ) : pred (succ n) = n
theorem pred.succ (n : ℕ) : pred (succ n) = n :=
rfl
irreducible pred
@ -103,11 +73,6 @@ or.imp_or (zero_or_succ_pred n) (assume H, H)
theorem case {P : ℕ → Prop} (n : ℕ) (H1: P 0) (H2 : ∀m, P (succ m)) : P n :=
induction_on n H1 (take m IH, H2 m)
theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B :=
or.elim (zero_or_succ_pred n)
(take H3 : n = 0, H1 H3)
(take H3 : n = succ (pred n), H2 (pred n) H3)
theorem succ.inj {n m : ℕ} (H : succ n = succ m) : n = m :=
no_confusion H (λe, e)
@ -118,25 +83,11 @@ induction_on n
absurd H ne)
(take k IH H, IH (succ.inj H))
protected definition has_decidable_eq [instance] : decidable_eq ℕ :=
take n m : ℕ,
have general : ∀n, decidable (n = m), from
rec_on m
(take n,
rec_on n
(inl rfl)
(λ m iH, inr !succ_ne_zero))
(λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')),
take n, rec_on n
(inr (ne.symm !succ_ne_zero))
(λ (n' : ℕ) (iH2 : decidable (n' = succ m')),
decidable.by_cases
(assume Heq : n' = m', inl (congr_arg succ Heq))
(assume Hne : n' ≠ m',
have H1 : succ n' ≠ succ m', from
assume Heq, absurd (succ.inj Heq) Hne,
inr H1))),
general n
theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B :=
or.elim (zero_or_succ_pred n)
(take H3 : n = 0, H1 H3)
(take H3 : n = succ (pred n), H2 (pred n) H3)
theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1)
(H3 : ∀ (n : ℕ) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a :=
@ -163,9 +114,11 @@ general m
-- Addition
-- --------
theorem add.zero_right (n : ℕ) : n + 0 = n
theorem add.zero_right (n : ℕ) : n + 0 = n :=
rfl
theorem add.succ_right (n m : ℕ) : n + succ m = succ (n + m)
theorem add.succ_right (n m : ℕ) : n + succ m = succ (n + m) :=
rfl
irreducible add
@ -267,12 +220,11 @@ nat.rec H1 (take n IH, !add.one ▸ (H2 n IH)) a
-- Multiplication
-- --------------
definition mul (n m : ℕ) := nat.rec 0 (fun m x, x + n) m
notation a * b := mul a b
theorem mul.zero_right (n : ℕ) : n * 0 = 0 :=
rfl
theorem mul.zero_right (n : ℕ) : n * 0 = 0
theorem mul.succ_right (n m : ℕ) : n * succ m = n * m + n
theorem mul.succ_right (n m : ℕ) : n * succ m = n * m + n :=
rfl
irreducible mul

277
library/data/nat/decl.lean Normal file
View file

@ -0,0 +1,277 @@
--- Copyright (c) 2014 Floris van Doorn. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Floris van Doorn, Leonardo de Moura
import logic.eq logic.heq logic.wf logic.decidable logic.if data.prod
open eq.ops decidable
inductive nat :=
zero : nat,
succ : nat → nat
namespace nat
notation `ℕ` := nat
inductive lt (a : nat) : nat → Prop :=
base : lt a (succ a),
step : Π {b}, lt a b → lt a (succ b)
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
notation a ≤ b := le a b
definition pred (a : nat) : nat :=
cases_on a zero (λ a₁, a₁)
protected definition is_inhabited [instance] : inhabited nat :=
inhabited.mk zero
protected definition has_decidable_eq [instance] : decidable_eq nat :=
λn m : nat,
have general : ∀n, decidable (n = m), from
rec_on m
(λ n, cases_on n
(inl rfl)
(λ m, inr (λ (e : succ m = zero), no_confusion e)))
(λ (m' : nat) (ih : ∀n, decidable (n = m')) (n : nat), cases_on n
(inr (λ h, no_confusion h))
(λ (n' : nat),
decidable.rec_on (ih n')
(assume Heq : n' = m', inl (eq.rec_on Heq rfl))
(assume Hne : n' ≠ m',
have H1 : succ n' ≠ succ m', from
assume Heq, no_confusion Heq (λ e : n' = m', Hne e),
inr H1))),
general n
-- less-than is well-founded
definition lt.wf [instance] : well_founded lt :=
well_founded.intro (λn, rec_on n
(acc.intro zero (λ (y : nat) (hlt : y < zero),
have aux : ∀ {n₁}, y < n₁ → zero = n₁ → acc lt y, from
λ n₁ hlt, lt.cases_on hlt
(λ heq, no_confusion heq)
(λ b hlt heq, no_confusion heq),
aux hlt rfl))
(λ (n : nat) (ih : acc lt n),
acc.intro (succ n) (λ (m : nat) (hlt : m < succ n),
have aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, from
λ n₁ hlt, lt.cases_on hlt
(λ (heq : succ n = succ m),
nat.no_confusion heq (λ (e : n = m),
eq.rec_on e ih))
(λ b (hlt : m < b) (heq : succ n = succ b),
nat.no_confusion heq (λ (e : n = b),
acc.inv (eq.rec_on e ih) hlt)),
aux hlt rfl)))
definition not_lt_zero (a : nat) : ¬ a < zero :=
have aux : ∀ {b}, a < b → b = zero → false, from
λ b H, lt.cases_on H
(λ heq, nat.no_confusion heq)
(λ b h₁ heq, nat.no_confusion heq),
λ H, aux H rfl
definition zero_lt_succ (a : nat) : zero < succ a :=
rec_on a
(lt.base zero)
(λ a (hlt : zero < succ a), lt.step hlt)
definition lt.trans {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c :=
have aux : ∀ {d}, d < c → b = d → a < b → a < c, from
(λ d H, lt.rec_on H
(λ h₁ h₂, lt.step (eq.rec_on h₁ h₂))
(λ 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 :=
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 :=
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 :=
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),
aux
definition lt.is_decidable_rel [instance] : decidable_rel lt :=
λ a b, rec_on b
(λ (a : nat), inr (not_lt_zero a))
(λ (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_neg : ¬ a < b₁,
have aux : ¬ succ a < succ b₁, from
λ h : succ a < succ b₁, h_neg (lt.cancel_succ_left_right 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_def_left {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)
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))
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))
definition lt.trichotomy (a b : nat) : a < b ∨ a = b ∨ b < a :=
rec_on b
(λa, cases_on a
(or.inr (or.inl rfl))
(λ a₁, or.inr (or.inr !zero_lt_succ)))
(λ 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, 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))))))
a
definition 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 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 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))
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 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_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_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_eq.trans {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 :=
eq.rec_on h₂ h₁
definition eq_lt.trans {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 :=
eq.rec_on (eq.rec_on h₁ rfl) h₂
calc_trans lt.trans
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
definition max (a b : nat) : nat :=
if a < b then b else a
definition min (a b : nat) : nat :=
if a < b then a else b
definition max_a_a (a : nat) : a = max a a :=
eq.rec_on !if_t_t rfl
definition max.eq_right {a b : nat} (H : a < b) : b = max a b :=
eq.rec_on (if_pos H) rfl
definition max.eq_left {a b : nat} (H : ¬ a < b) : a = max a b :=
eq.rec_on (if_neg 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 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)
(λ 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 (lt.asymm h),
eq.rec_on aux (le.of_lt h)))
definition gt a b := lt b a
notation a > b := gt a b
definition ge a b := le b a
notation a ≥ b := ge a b
definition add (a b : nat) : nat :=
rec_on b a (λ b₁ r, succ r)
notation a + b := add a b
definition sub (a b : nat) : nat :=
rec_on b a (λ b₁ r, pred r)
notation a - b := sub a b
definition mul (a b : nat) : nat :=
rec_on b zero (λ b₁ r, r + a)
notation a * b := mul a b
end nat

2
library/data/nat/default.lean
View file

@ -2,4 +2,4 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jeremy Avigad
import .basic .order .sub .div .wf
import .basic .order .sub .div

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

@ -11,7 +11,7 @@
import logic .sub algebra.relation data.prod
import tools.fake_simplifier
open nat relation relation.iff_ops prod
open relation relation.iff_ops prod
open fake_simplifier decidable
open eq.ops
@ -87,7 +87,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_le.trans Hzx (lt_succ_imp_le H1)),
have H2 : f' (succ m) x = rec_val x f, from
calc
f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl
@ -168,7 +168,7 @@ show lhs = rhs, from
have H2b : ¬ x < y, from assume H, H1 (or.inr H),
have ypos : y > 0, from ne_zero_imp_pos H2a,
have xgey : x ≥ y, from not_lt_imp_ge H2b,
have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos,
have H4 : x - y < x, from sub_lt (lt_le.trans ypos xgey) ypos,
calc
lhs = succ (g1 (x - y)) : if_neg H1
... = succ (g2 (x - y)) : {H _ H4}
@ -244,7 +244,7 @@ show lhs = rhs, from
have H2b : ¬ x < y, from assume H, H1 (or.inr H),
have ypos : y > 0, from ne_zero_imp_pos H2a,
have xgey : x ≥ y, from not_lt_imp_ge H2b,
have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos,
have H4 : x - y < x, from sub_lt (lt_le.trans ypos xgey) ypos,
calc
lhs = g1 (x - y) : if_neg H1
... = g2 (x - y) : H _ H4
@ -382,7 +382,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 le_lt.trans !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 :=

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

@ -1,41 +1,52 @@
--- Copyright (c) 2014 Floris van Doorn. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Floris van Doorn
--- Author: Floris van Doorn, Leonardo de Moura
-- data.nat.order
-- ==============
--
-- The ordering on the natural numbers
import .basic logic.decidable
import tools.fake_simplifier
import .basic
open nat eq.ops tactic
open fake_simplifier
open eq.ops
namespace nat
-- Less than or equal
-- ------------------
definition le (n m : ℕ) : Prop := exists k : nat, n + k = m
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))
notation a <= b := le a b
notation a ≤ b := le a b
theorem le.add_right (n k : ℕ) : n ≤ n + k :=
induction_on k
(calc n ≤ n : le.refl n
... = n + zero : add.zero_right)
(λ k (ih : n ≤ n + k), calc
n ≤ succ (n + k) : le.succ_right ih
... = n + succ k : add.succ_right)
theorem le_intro {n m k : ℕ} (H : n + k = m) : n ≤ m :=
exists_intro k H
theorem le_intro {n m k : ℕ} (h : n + k = m) : n ≤ m :=
h ▸ le.add_right n k
theorem le_elim {n m : ℕ} (H : n ≤ m) : ∃k, n + k = m :=
H
irreducible le
theorem le_elim {n m : ℕ} (h : n ≤ m) : ∃k, n + k = m :=
le.rec_on h
(exists_intro 0 rfl)
(λ m (h : n < m), lt.rec_on h
(exists_intro 1 rfl)
(λ b hlt (ih : ∃ (k : ℕ), n + k = b),
obtain (k : ℕ) (h : n + k = b), from ih,
exists_intro (succ k) (calc
n + succ k = succ (n + k) : add.succ_right
... = succ b : h)))
-- ### partial order (totality is part of less than)
theorem le_refl (n : ℕ) : n ≤ n :=
le_intro !add.zero_right
le.refl n
theorem zero_le (n : ℕ) : 0 ≤ n :=
le_intro !add.zero_left
@ -51,13 +62,7 @@ not_intro
absurd H2 !succ_ne_zero)
theorem le_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k :=
obtain (l1 : ℕ) (Hl1 : n + l1 = m), from le_elim H1,
obtain (l2 : ℕ) (Hl2 : m + l2 = k), from le_elim H2,
le_intro
(calc
n + (l1 + l2) = n + l1 + l2 : !add.assoc⁻¹
... = m + l2 : {Hl1}
... = k : Hl2)
le.trans H1 H2
theorem le_antisym {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
obtain (k : ℕ) (Hk : n + k = m), from (le_elim H1),
@ -218,7 +223,7 @@ theorem mul_le_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k * n ≤ k * m :=
obtain (l : ℕ) (Hl : n + l = m), from (le_elim H),
have H2 : k * n + k * l = k * m, from
calc
k * n + k * l = k * (n + l) : by simp
k * n + k * l = k * (n + l) : mul.distr_left
... = k * m : {Hl},
le_intro H2
@ -228,52 +233,14 @@ theorem mul_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n * k ≤ m * k :=
theorem mul_le {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l :=
le_trans (mul_le_right H1 m) (mul_le_left H2 k)
-- mul_le_[left|right]_inv below
definition le_decidable [instance] (n m : ℕ) : decidable (n ≤ m) :=
have general : ∀n, decidable (n ≤ m), from
rec_on m
(take n,
rec_on n
(decidable.inl !le_refl)
(take m iH, decidable.inr !not_succ_zero_le))
(take (m' : ℕ) (iH1 : ∀n, decidable (n ≤ m')) (n : ℕ),
rec_on n
(decidable.inl !zero_le)
(take (n' : ℕ) (iH2 : decidable (n' ≤ succ m')),
decidable.by_cases
(assume Hp : n' ≤ m', decidable.inl (succ_le Hp))
(assume Hn : ¬ n' ≤ m',
have H : ¬ succ n' ≤ succ m', from
assume Hle : succ n' ≤ succ m',
absurd (succ_le_cancel Hle) Hn,
decidable.inr H))),
general n
-- Less than, Greater than, Greater than or equal
-- ----------------------------------------------
-- ge and gt will be transparent, so we don't need to reprove theorems for le and lt for them
definition lt (n m : ℕ) := succ n ≤ m
notation a < b := lt a b
definition ge (n m : ℕ) := m ≤ n
notation a >= b := ge a b
notation a ≥ b := ge a b
definition gt (n m : ℕ) := m < n
notation a > b := gt a b
theorem lt_def (n m : ℕ) : (n < m) = (succ n ≤ m) := rfl
-- add_rewrite gt_def ge_def --it might be possible to remove this in Lean 0.2
theorem lt_intro {n m k : ℕ} (H : succ n + k = m) : n < m :=
le_intro H
le_succ_imp_lt (le_intro H)
theorem lt_elim {n m : ℕ} (H : n < m) : ∃ k, succ n + k = m :=
le_elim H
le_elim (lt_imp_le_succ H)
theorem lt_add_succ (n m : ℕ) : n < n + succ m :=
lt_intro !add.move_succ
@ -281,16 +248,18 @@ lt_intro !add.move_succ
-- ### basic facts
theorem lt_imp_ne {n m : ℕ} (H : n < m) : n ≠ m :=
and.elim_right (succ_le_imp_le_and_ne H)
λ heq : n = m, absurd H (heq ▸ !lt.irrefl)
theorem lt_irrefl (n : ℕ) : ¬ n < n :=
not_intro (assume H : n < n, absurd rfl (lt_imp_ne H))
theorem succ_pos (n : ℕ) : 0 < succ n :=
succ_le !zero_le
theorem lt_def (n m : ℕ) : n < m ↔ succ n ≤ m :=
iff.intro
(λ h, lt_imp_le_succ h)
(λ h, le_succ_imp_lt h)
theorem not_lt_zero (n : ℕ) : ¬ n < 0 :=
!not_succ_zero_le
theorem succ_pos (n : ℕ) : 0 < succ n :=
!zero_lt_succ
theorem lt_imp_eq_succ {n m : ℕ} (H : n < m) : exists k, m = succ k :=
discriminate
@ -299,90 +268,53 @@ discriminate
-- ### interaction with le
theorem lt_imp_le_succ {n m : ℕ} (H : n < m) : succ n ≤ m :=
H
theorem le_succ_imp_lt {n m : ℕ} (H : succ n ≤ m) : n < m :=
H
theorem self_lt_succ (n : ℕ) : n < succ n :=
!le_refl
lt.base n
theorem lt_imp_le {n m : ℕ} (H : n < m) : n ≤ m :=
and.elim_left (succ_le_imp_le_and_ne H)
le.of_lt H
theorem le_imp_lt_or_eq {n m : ℕ} (H : n ≤ m) : n < m ∨ n = m :=
le_imp_succ_le_or_eq H
or.swap (le_def_right H)
theorem le_ne_imp_lt {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : n < m :=
le_ne_imp_succ_le H1 H2
theorem le_imp_lt_succ {n m : ℕ} (H : n ≤ m) : n < succ m :=
succ_le H
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 H
-- ### transitivity, antisymmmetry
theorem lt_le_trans {n m k : ℕ} (H1 : n < m) (H2 : m ≤ k) : n < k :=
le_trans H1 H2
theorem le_lt_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m < k) : n < k :=
le_trans (succ_le H1) H2
theorem lt_trans {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k :=
lt_le_trans H1 (lt_imp_le H2)
theorem eq_le_trans {n m k : ℕ} (H1 : n = m) (H2 : m ≤ k) : n ≤ k :=
H1⁻¹ ▸ H2
theorem eq_lt_trans {n m k : ℕ} (H1 : n = m) (H2 : m < k) : n < k :=
H1⁻¹ ▸ H2
theorem le_eq_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m = k) : n ≤ k :=
H2 ▸ H1
theorem lt_eq_trans {n m k : ℕ} (H1 : n < m) (H2 : m = k) : n < k :=
H2 ▸ H1
calc_trans le_trans
calc_trans lt_trans
calc_trans lt_le_trans
calc_trans le_lt_trans
calc_trans eq_le_trans
calc_trans eq_lt_trans
calc_trans le_eq_trans
calc_trans lt_eq_trans
succ_le_cancel (lt_imp_le_succ H)
theorem le_imp_not_gt {n m : ℕ} (H : n ≤ m) : ¬ n > m :=
not_intro (assume H2 : m < n, absurd (le_lt_trans H H2) !lt_irrefl)
le.rec_on H
!lt.irrefl
(λ 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_le.trans H H2) !lt_irrefl)
theorem lt_antisym {n m : ℕ} (H : n < m) : ¬ m < n :=
le_imp_not_gt (lt_imp_le H)
lt.asymm H
-- le_imp_not_gt (lt_imp_le H)
-- ### interaction with addition
theorem add_lt_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m :=
!add.succ_right ▸ add_le_left H k
le_succ_imp_lt (!add.succ_right ▸ add_le_left (lt_imp_le_succ 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)
le_lt.trans (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_le.trans (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 :=
add_le_cancel_left (!add.succ_right⁻¹ ▸ H)
le_succ_imp_lt (add_le_cancel_left (!add.succ_right⁻¹ ▸ (lt_imp_le_succ 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)
@ -395,43 +327,27 @@ theorem succ_lt {n m : ℕ} (H : n < m) : succ n < succ m :=
theorem succ_lt_cancel {n m : ℕ} (H : succ n < succ m) : n < m :=
add_lt_cancel_right (!add.one⁻¹ ▸ !add.one⁻¹ ▸ H)
theorem lt_imp_lt_succ {n m : ℕ} (H : n < m) : n < succ m
:= lt_trans H !self_lt_succ
theorem lt_imp_lt_succ {n m : ℕ} (H : n < m) : n < succ m :=
lt.step H
-- ### totality of lt and le
theorem le_or_gt {n m : ℕ} : n ≤ m ∨ n > m :=
induction_on n
(or.inl !zero_le)
(take (k : ℕ),
assume IH : k ≤ m ∨ m < k,
or.elim IH
(assume H : k ≤ m,
obtain (l : ℕ) (Hl : k + l = m), from le_elim H,
discriminate
(assume H2 : l = 0,
have H3 : m = k,
from calc
m = k + l : Hl⁻¹
... = k + 0 : {H2}
... = k : !add.zero_right,
have H4 : m < succ k, from H3 ▸ !self_lt_succ,
or.inr H4)
(take l2 : ℕ,
assume H2 : l = succ l2,
have H3 : succ k + l2 = m,
from calc
succ k + l2 = k + succ l2 : !add.move_succ
... = k + l : {H2⁻¹}
... = m : Hl,
or.inl (le_intro H3)))
(assume H : m < k, or.inr (lt_imp_lt_succ H)))
or.rec_on (lt.trichotomy n m)
(λ h : n < m, or.inl (le.of_lt h))
(λ h : n = m ∨ m < n, or.rec_on h
(λ h : n = m, eq.rec_on h (or.inl !le.refl))
(λ h : m < n, or.inr h))
theorem trichotomy_alt (n m : ℕ) : (n < m ∨ n = m) ∨ n > m :=
or.imp_or_left le_or_gt (assume H : n ≤ m, le_imp_lt_or_eq H)
or.rec_on (lt.trichotomy n m)
(λ h, or.inl (or.inl h))
(λ h, or.rec_on h
(λ h, or.inl (or.inr h))
(λ h, or.inr h))
theorem trichotomy (n m : ℕ) : n < m ∨ n = m ∨ n > m :=
iff.elim_left or.assoc !trichotomy_alt
lt.trichotomy n m
theorem le_total (n m : ℕ) : n ≤ m ∨ m ≤ n :=
or.imp_or_right le_or_gt (assume H : m < n, lt_imp_le H)
@ -442,13 +358,6 @@ or.resolve_left le_or_gt H
theorem not_le_imp_gt {n m : ℕ} (H : ¬ n ≤ m) : n > m :=
or.resolve_right le_or_gt H
-- The following three theorems are automatically proved using the instance le_decidable
definition lt_decidable [instance] (n m : ℕ) : decidable (n < m) := _
definition gt_decidable [instance] (n m : ℕ) : decidable (n > m) := _
definition ge_decidable [instance] (n m : ℕ) : decidable (n ≥ m) := _
-- Note: interaction with multiplication under "positivity"
-- ### misc
protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n :=
@ -543,22 +452,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 H k,
lt_le_trans H2 H3
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
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)
le_lt.trans (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)
le_lt.trans (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 (le_lt.trans !zero_le H1) H2,
le_lt.trans H3 H4
theorem mul_lt_cancel_left {n m k : ℕ} (H : k * n < k * m) : n < m :=
or.elim le_or_gt
@ -571,7 +480,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 le_lt.trans 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
@ -602,9 +511,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 H3)
show n = 1, from le_antisym H5 (lt_imp_le_succ H3))
(assume H5 : n > 1,
have H6 : n * m ≥ 2 * 1, from mul_le H5 H4,
have H6 : n * m ≥ 2 * 1, from mul_le (lt_imp_le_succ H5) (lt_imp_le_succ H4),
have H7 : 1 ≥ 2, from !mul.one_right ▸ H ▸ H6,
absurd !self_lt_succ (le_imp_not_gt H7))

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

@ -7,11 +7,10 @@
--
-- Subtraction on the natural numbers, as well as min, max, and distance.
import data.nat.order
import .order
import tools.fake_simplifier
open nat eq.ops tactic
open helper_tactics
open eq.ops
open fake_simplifier
namespace nat
@ -19,12 +18,11 @@ namespace nat
-- subtraction
-- -----------
definition sub (n m : ℕ) : nat := rec n (fun m x, pred x) m
notation a - b := sub a b
theorem sub_zero_right (n : ℕ) : n - 0 = n :=
rfl
theorem sub_zero_right (n : ℕ) : n - 0 = n
theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m)
theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m) :=
rfl
irreducible sub
@ -300,7 +298,7 @@ have xsuby_eq : x - y = x' - y', from calc
... = x' - y' : !sub_succ_succ,
have H1 : x' - y' ≤ x', from !sub_le_self,
have H2 : x' < succ x', from !self_lt_succ,
show x - y < x, from xeq⁻¹ ▸ xsuby_eq⁻¹ ▸ le_lt_trans H1 H2
show x - y < x, from xeq⁻¹ ▸ xsuby_eq⁻¹ ▸ le_lt.trans H1 H2
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,
@ -309,7 +307,7 @@ or.elim !le_total
(assume H2 : k ≤ n,
have H3 : n - k + l = m - k, from
calc
n - k + l = l + (n - k) : by simp
n - k + l = l + (n - k) : add.comm
... = l + n - k : (add_sub_assoc H2 l)⁻¹
... = n + l - k : {!add.comm}
... = m - k : {Hl},
@ -324,10 +322,12 @@ sub_split
have H3 : n ≤ k, from le_trans H (le_intro Hm),
have H4 : m' + l + n = k - n + n, from
calc
m' + l + n = n + l + m' : by simp
... = m + m' : {Hl}
... = k : Hm
... = k - n + n : (add_sub_ge_left H3)⁻¹,
m' + l + n = n + (m' + l) : add.comm
... = n + (l + m') : add.comm
... = n + l + m' : add.assoc
... = m + m' : {Hl}
... = k : Hm
... = k - n + n : (add_sub_ge_left H3)⁻¹,
le_intro (add.cancel_right H4))
-- theorem sub_lt_cancel_right {n m k : ℕ) (H : n - k < m - k) : n < m
@ -352,9 +352,10 @@ sub_split
assume Hkm : k + km = m,
have H : k + (mn + km) = n, from
calc
k + (mn + km) = k + km + mn : by simp
... = m + mn : {Hkm}
... = n : Hmn,
k + (mn + km) = k + (km + mn): add.comm
... = k + km + mn : add.assoc
... = m + mn : Hkm
... = n : Hmn,
have H2 : n - k = mn + km, from sub_intro H,
H2 ▸ !le_refl))
@ -362,24 +363,9 @@ sub_split
-- add_rewrite sub_self mul_sub_distr_left mul_sub_distr_right
-- Max, min, iteration, and absolute difference
-- absolute difference
-- --------------------------------------------
definition max (n m : ℕ) : ℕ := n + (m - n)
definition min (n m : ℕ) : ℕ := m - (m - n)
theorem max_le {n m : ℕ} (H : n ≤ m) : max n m = m :=
add_sub_le H
theorem max_ge {n m : ℕ} (H : n ≥ m) : max n m = n :=
add_sub_ge H
theorem left_le_max (n m : ℕ) : n ≤ max n m :=
!le_add_sub_left
theorem right_le_max (n m : ℕ) : m ≤ max n m :=
!le_add_sub_right
-- ### absolute difference
-- This section is still incomplete
@ -391,8 +377,9 @@ theorem dist_comm (n m : ℕ) : dist n m = dist m n :=
theorem dist_self (n : ℕ) : dist n n = 0 :=
calc
(n - n) + (n - n) = 0 + 0 : by simp
... = 0 : by simp
(n - n) + (n - n) = 0 + (n - n) : sub_self
... = 0 + 0 : sub_self
... = 0 : rfl
theorem dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m :=
have H2 : n - m = 0, from add.eq_zero_left H,
@ -445,9 +432,10 @@ calc
theorem dist_sub_move_add {n m : ℕ} (H : n ≥ m) (k : ℕ) : dist (n - m) k = dist n (k + m) :=
have H2 : n - m + (k + m) = k + n, from
calc
n - m + (k + m) = n - m + m + k : by simp
... = n + k : {add_sub_ge_left H}
... = k + n : by simp,
n - m + (k + m) = n - m + (m + k) : add.comm
... = n - m + m + k : add.assoc
... = n + k : {add_sub_ge_left H}
... = k + n : add.comm,
dist_eq_intro H2
theorem dist_sub_move_add' {k m : ℕ} (H : k ≥ m) (n : ℕ) : dist n (k - m) = dist (n + m) k :=

52
library/data/nat/wf.lean
View file

@ -1,52 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import data.nat.order logic.wf
open nat eq.ops
namespace nat
inductive pred_rel : nat → nat → Prop :=
intro : Π (n : nat), pred_rel n (succ n)
definition not_pred_rel_zero (n : nat) : ¬ pred_rel n zero :=
have aux : ∀{m}, pred_rel n m → succ n = m, from
λm H, pred_rel.rec_on H (take n, rfl),
assume H : pred_rel n zero,
absurd (aux H) !succ_ne_zero
definition pred_rel_succ {a b : nat} (H : pred_rel a (succ b)) : b = a :=
have aux : pred (succ b) = a, from
pred_rel.rec_on H (λn, rfl),
aux
-- Predecessor relation is well-founded
definition pred_rel.wf : well_founded pred_rel :=
well_founded.intro
(λn, induction_on n
(acc.intro zero (λy (H : pred_rel y zero), absurd H (not_pred_rel_zero y)))
(λa (iH : acc pred_rel a),
acc.intro (succ a) (λy (H : pred_rel y (succ a)),
have aux : a = y, from pred_rel_succ H,
eq.rec_on aux iH)))
-- Less-than relation is well-founded
definition lt.wf [instance] : well_founded lt :=
well_founded.intro
(λn, induction_on n
(acc.intro zero (λ (y : nat) (H : y < 0),
absurd H !not_lt_zero))
(λ (n : nat) (iH : acc lt n),
acc.intro (succ n) (λ (m : nat) (H : m < succ n),
have H₁ : m < n ∨ m = n, from le_imp_lt_or_eq (succ_le_cancel (lt_imp_le_succ H)),
or.elim H₁
(assume Hlt : m < n, acc.inv iH Hlt)
(assume Heq : m = n, Heq⁻¹ ▸ iH))))
definition measure {A : Type} (f : A → nat) : A → A → Prop :=
inv_image lt f
definition measure.wf {A : Type} (f : A → nat) : well_founded (measure f) :=
inv_image.wf f lt.wf
end nat

2
tests/lean/notation.lean
View file

@ -1,4 +1,4 @@
import logic data.nat.basic
import logic data.num data.nat.basic
open num
constant b : num
check b + b + b

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

@ -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_le.trans Hzx (lt_succ_imp_le H1))
∎,
have H2 : f' (succ m) x = rec_val x f,
proof

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

@ -11,7 +11,7 @@ notation `dif` c `then` t:45 `else` e:45 := dite c t e
-- Auxiliary lemma used to justify recursive call
private lemma lt_aux {x y : nat} (H : 0 < y ∧ y ≤ x) : x - y < x :=
have y0 : 0 < y, from and.elim_left H,
have x0 : 0 < x, from lt_le_trans y0 (and.elim_right H),
have x0 : 0 < x, from lt_le.trans y0 (and.elim_right H),
sub_lt x0 y0
definition wdiv.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=

12
tests/lean/run/fib_wrec.lean
View file

@ -7,8 +7,8 @@ nat.cases_on n
(λ (n₁ : nat), nat.cases_on n₁
(λ (f : Π (m : nat), m < (succ zero) → nat), succ zero)
(λ (n₂ : nat) (f : Π (m : nat), m < (succ (succ n₂)) → nat),
have l₁ : succ n₂ < succ (succ n₂), from self_lt_succ (succ n₂),
have l₂ : n₂ < succ (succ n₂), from lt_trans (self_lt_succ n₂) l₁,
have l₁ : succ n₂ < succ (succ n₂), from lt.base (succ n₂),
have l₂ : n₂ < succ (succ n₂), from lt.trans (lt.base n₂) l₁,
f (succ n₂) l₁ + f n₂ l₂))
definition fib (n : nat) :=
@ -23,6 +23,8 @@ well_founded.fix_eq fib.F 1
theorem fib.succ_succ_eq (n : nat) : fib (succ (succ n)) = fib (succ n) + fib n :=
well_founded.fix_eq fib.F (succ (succ n))
eval fib 5 -- ignores opaque annotations
eval fib 6
eval [strict] fib 5 -- take opaque/irreducible annotations into account
example : fib 5 = 8 :=
rfl
example : fib 6 = 13 :=
rfl

6
tests/lean/run/tree_height.lean
View file

@ -19,13 +19,13 @@ 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 (left_le_max (height t₁) (height t₂))
le_imp_lt_succ (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 (right_le_max (height t₁) (height t₂))
le_imp_lt_succ (max.right (height t₁) (height t₂))
theorem height_lt.trans {A : Type} : transitive (@height_lt A) :=
inv_image.trans lt height @lt_trans
inv_image.trans lt height @lt.trans
example : height_lt (leaf 2) (node (leaf 1) (leaf 2)) :=
!height_lt.node_right

4
tests/lean/whnf.lean.expected.out
View file

@ -1,5 +1,5 @@
whnf.lean:2:0: warning: imported file uses 'sorry'
succ (nat.rec 2 (λ (n r : ℕ), succ r) zero)
succ (nat.rec 2 (λ (b₁ r : ℕ), succ r) zero)
succ (succ (succ zero))
succ (nat.rec a (λ (n r : ℕ), succ r) zero)
succ (nat.rec a (λ (b₁ r : ℕ), succ r) zero)
succ a