From 66adac6af6d73515bcbfbc2f5c6099682cd049c8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Aug 2018 12:17:15 -0700 Subject: [PATCH] chore(library/init): avoid `calc` at corelib --- library/init/core.lean | 28 +++++++----- library/init/data/hashmap/basic.lean | 12 ++--- library/init/data/nat/basic.lean | 66 ++++++++++++++-------------- library/init/function.lean | 9 ++-- 4 files changed, 61 insertions(+), 54 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index 90d13968e5..8420f92b10 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -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 diff --git a/library/init/data/hashmap/basic.lean b/library/init/data/hashmap/basic.lean index 77ebf004db..9e642b79c0 100644 --- a/library/init/data/hashmap/basic.lean +++ b/library/init/data/hashmap/basic.lean @@ -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} diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean index 49317cedc8..e642dd285f 100644 --- a/library/init/data/nat/basic.lean +++ b/library/init/data/nat/basic.lean @@ -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 _ diff --git a/library/init/function.lean b/library/init/function.lean index 590207d7f5..641c8e634b 100644 --- a/library/init/function.lean +++ b/library/init/function.lean @@ -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