max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init): avoid calc at corelib

Browse source
This commit is contained in:
Leonardo de Moura 2018-08-27 12:17:15 -07:00
parent 4917ab0c65
commit 66adac6af6
4 changed files with 61 additions and 54 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
library/init/core.lean
View file

@ -1614,17 +1614,20 @@ def right_distributive := ∀ a b c, (a + b) * c = a * c + b * c
def right_commutative (h : β → α → β) := ∀ b a₁ a₂, h (h b a₁) a₂ = h (h b a₂) a₁
def left_commutative (h : α → β → β) := ∀ a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b)
local infix `◾`:50 := eq.trans
theorem left_comm : commutative f → associative f → left_commutative f :=
assume hcomm hassoc, assume a b c, calc
a*(b*c) = (a*b)*c : eq.symm (hassoc a b c)
... = (b*a)*c : hcomm a b ▸ rfl
... = b*(a*c) : hassoc b a c
assume hcomm hassoc, assume a b c,
eq.symm (hassoc a b c)
◾ (hcomm a b ▸ rfl : (a*b)*c = (b*a)*c)
◾ hassoc b a c
theorem right_comm : commutative f → associative f → right_commutative f :=
assume hcomm hassoc, assume a b c, calc
(a*b)*c = a*(b*c) : hassoc a b c
... = a*(c*b) : hcomm b c ▸ rfl
... = (a*c)*b : eq.symm (hassoc a c b)
assume hcomm hassoc, assume a b c,
hassoc a b c
◾ (hcomm b c ▸ rfl : a*(b*c) = a*(c*b))
◾ eq.symm (hassoc a c b)
end binary
/- Subtype -/
@ -1881,10 +1884,11 @@ quot.rec f (λ a b h, subsingleton.elim _ (f b)) q
@[reducible, elab_as_eliminator]
protected def hrec_on
(q : quot r) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : r a b), f a == f b) : β q :=
quot.rec_on q f
(λ a b p, eq_of_heq (calc
(eq.rec (f a) (sound p) : β ⟦b⟧) == f a : eq_rec_heq (sound p) (f a)
... == f b : c a b p))
quot.rec_on q f $
λ a b p, eq_of_heq $
have p₁ : (eq.rec (f a) (sound p) : β ⟦b⟧) == f a, from eq_rec_heq (sound p) (f a),
heq.trans p₁ (c a b p)
end
end quot

12
library/init/data/hashmap/basic.lean
View file

@ -13,8 +13,7 @@ def bucket_array (α : Type u) (β : α → Type v) :=
def bucket_array.uwrite {α : Type u} {β : α → Type v} (data : bucket_array α β) (i : usize) (d : list (Σ a, β a)) (h : i.to_nat < data.val.sz) : bucket_array α β :=
⟨ data.val.uwrite i d h,
calc (data.val.uwrite i d h).sz = data.val.sz : array.sz_write_eq _ _ _
... > 0 : data.property ⟩
trans_rel_right gt (array.sz_write_eq (data.val) ⟨usize.to_nat i, h⟩ d) data.property ⟩
structure hashmap_imp (α : Type u) (β : α → Type v) :=
(size : nat)
@ -25,12 +24,13 @@ let n := if nbuckets = 0 then 8 else nbuckets in
{ size := 0,
buckets :=
⟨ mk_array n [],
calc (mk_array n []).sz = n : sz_mk_array_eq _ _
... = if nbuckets = 0 then 8 else nbuckets : rfl
... > 0 :
have p₁ : (mk_array n []).sz = n, from sz_mk_array_eq _ _,
have p₂ : n = (if nbuckets = 0 then 8 else nbuckets), from rfl,
have p₃ : (if nbuckets = 0 then 8 else nbuckets) > 0, from
match nbuckets with
| 0 := nat.zero_lt_succ _
| (nat.succ x) := nat.zero_lt_succ _ ⟩ }
| (nat.succ x) := nat.zero_lt_succ _,
trans_rel_right gt (eq.trans p₁ p₂) p₃ ⟩ }
namespace hashmap_imp
variables {α : Type u} {β : α → Type v}

66
library/init/data/nat/basic.lean
View file

@ -164,35 +164,37 @@ nat.zero_add
protected theorem one_mul (n : nat) : 1 * n = n :=
nat.mul_comm n 1 ▸ nat.mul_one n
local infix `◾`:50 := eq.trans
protected theorem left_distrib : ∀ (n m k : nat), n * (m + k) = n * m + n * k
| 0 m k := (nat.zero_mul (m + k)).symm ▸ (nat.zero_mul m).symm ▸ (nat.zero_mul k).symm ▸ rfl
| (succ n) m k := calc
succ n * (m + k)
= n * (m + k) + (m + k) : succ_mul _ _
... = (n * m + n * k) + (m + k) : left_distrib n m k ▸ rfl
... = n * m + (n * k + (m + k)) : nat.add_assoc _ _ _
... = n * m + (m + (n * k + k)) : congr_arg (λ x, n*m + x) (nat.add_left_comm _ _ _)
... = (n * m + m) + (n * k + k) : (nat.add_assoc _ _ _).symm
... = (n * m + m) + succ n * k : succ_mul n k ▸ rfl
... = succ n * m + succ n * k : succ_mul n m ▸ rfl
| (succ n) m k :=
have h₁ : succ n * (m + k) = n * (m + k) + (m + k), from succ_mul _ _,
have h₂ : n * (m + k) + (m + k) = (n * m + n * k) + (m + k), from left_distrib n m k ▸ rfl,
have h₃ : (n * m + n * k) + (m + k) = n * m + (n * k + (m + k)), from nat.add_assoc _ _ _,
have h₄ : n * m + (n * k + (m + k)) = n * m + (m + (n * k + k)), from congr_arg (λ x, n*m + x) (nat.add_left_comm _ _ _),
have h₅ : n * m + (m + (n * k + k)) = (n * m + m) + (n * k + k), from (nat.add_assoc _ _ _).symm,
have h₆ : (n * m + m) + (n * k + k) = (n * m + m) + succ n * k, from succ_mul n k ▸ rfl,
have h₇ : (n * m + m) + succ n * k = succ n * m + succ n * k, from succ_mul n m ▸ rfl,
h₁ ◾ h₂ ◾ h₃ ◾ h₄ ◾ h₅ ◾ h₆ ◾ h₇
protected theorem right_distrib (n m k : nat) : (n + m) * k = n * k + m * k :=
calc (n + m) * k
= k * (n + m) : nat.mul_comm _ _
... = k * n + k * m : nat.left_distrib _ _ _
... = n * k + k * m : nat.mul_comm n k ▸ rfl
... = n * k + m * k : nat.mul_comm m k ▸ rfl
have h₁ : (n + m) * k = k * (n + m), from nat.mul_comm _ _,
have h₂ : k * (n + m) = k * n + k * m, from nat.left_distrib _ _ _,
have h₃ : k * n + k * m = n * k + k * m, from nat.mul_comm n k ▸ rfl,
have h₄ : n * k + k * m = n * k + m * k, from nat.mul_comm m k ▸ rfl,
h₁ ◾ h₂ ◾ h₃ ◾ h₄
protected theorem mul_assoc : ∀ (n m k : nat), (n * m) * k = n * (m * k)
| n m 0 := rfl
| n m (succ k) := calc
n * m * succ k
= n * m * (k + 1) : rfl
... = (n * m * k) + n * m * 1 : nat.left_distrib _ _ _
... = (n * m * k) + n * m : (nat.mul_one (n*m)).symm ▸ rfl
... = (n * (m * k)) + n * m : (mul_assoc n m k).symm ▸ rfl
... = n * (m * k + m) : (nat.left_distrib n (m*k) m).symm
... = n * (m * succ k) : nat.mul_succ m k ▸ rfl
| n m (succ k) :=
have h₁ : n * m * succ k = n * m * (k + 1), from rfl,
have h₂ : n * m * (k + 1) = (n * m * k) + n * m * 1, from nat.left_distrib _ _ _,
have h₃ : (n * m * k) + n * m * 1 = (n * m * k) + n * m, from (nat.mul_one (n*m)).symm ▸ rfl,
have h₄ : (n * m * k) + n * m = (n * (m * k)) + n * m, from (mul_assoc n m k).symm ▸ rfl,
have h₅ : (n * (m * k)) + n * m = n * (m * k + m), from (nat.left_distrib n (m*k) m).symm,
have h₆ : n * (m * k + m) = n * (m * succ k), from nat.mul_succ m k ▸ rfl,
h₁ ◾ h₂ ◾ h₃ ◾ h₄ ◾ h₅ ◾ h₆
/- Inequalities -/
@ -426,16 +428,15 @@ or.elim (nat.lt_or_ge n m)
protected theorem add_le_add_left {n m : nat} (h : n ≤ m) (k : nat) : k + n ≤ k + m :=
match le.dest h with
| ⟨w, hw⟩ :=
have k + n + w = k + m, from
calc k + n + w = k + (n + w) : nat.add_assoc _ _ _
... = k + m : congr_arg _ hw,
le.intro this
have h₁ : k + n + w = k + (n + w), from nat.add_assoc _ _ _,
have h₂ : k + (n + w) = k + m, from congr_arg _ hw,
le.intro $ h₁ ◾ h₂
protected theorem add_le_add_right {n m : nat} (h : n ≤ m) (k : nat) : n + k ≤ m + k :=
calc
n + k = k + n : nat.add_comm _ _
... ≤ k + m : nat.add_le_add_left h k
... = m + k : nat.add_comm _ _
have h₁ : n + k = k + n, from nat.add_comm _ _,
have h₂ : k + n ≤ k + m, from nat.add_le_add_left h k,
have h₃ : k + m = m + k, from nat.add_comm _ _,
trans_rel_left (≤) (trans_rel_right (≤) h₁ h₂) h₃
protected theorem add_lt_add_left {n m : nat} (h : n < m) (k : nat) : k + n < k + m :=
lt_of_succ_le (add_succ k n ▸ nat.add_le_add_left (succ_le_of_lt h) k)
@ -476,8 +477,9 @@ congr_arg succ (succ_add n n)
protected theorem zero_lt_bit0 : ∀ {n : nat}, n ≠ 0 → 0 < bit0 n
| 0 h := absurd rfl h
| (succ n) h :=
calc 0 < succ (succ (bit0 n)) : zero_lt_succ _
... = bit0 (succ n) : (nat.bit0_succ_eq n).symm
have h₁ : 0 < succ (succ (bit0 n)), from zero_lt_succ _,
have h₂ : succ (succ (bit0 n)) = bit0 (succ n), from (nat.bit0_succ_eq n).symm,
trans_rel_left (<) h₁ h₂
protected theorem zero_lt_bit1 (n : nat) : 0 < bit1 n :=
zero_lt_succ _

9
library/init/function.lean
View file

@ -110,10 +110,11 @@ lemma surjective_of_has_right_inverse {f : α → β} : has_right_inverse f →
lemma left_inverse_of_surjective_of_right_inverse {f : α → β} {g : β → α}
(surjf : surjective f) (rfg : right_inverse f g) :
left_inverse f g :=
assume y, exists.elim (surjf y) (λ x hx, calc
f (g y) = f (g (f x)) : hx ▸ rfl
... = f x : eq.symm (rfg x) ▸ rfl
... = y : hx)
assume y, exists.elim (surjf y) $ λ x hx,
have h₁ : f (g y) = f (g (f x)), from hx ▸ rfl,
have h₂ : f (g (f x)) = f x, from eq.symm (rfg x) ▸ rfl,
have h₃ : f x = y, from hx,
eq.trans h₁ $ eq.trans h₂ h₃
lemma injective_id : injective (@id α) := assume a₁ a₂ h, h