From 7ba9a5012a51a4e949ce6d438351ca3ac03ab927 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 2 Jul 2019 16:46:51 -0700 Subject: [PATCH] chore(frontends/lean/builtin_exprs): make sure `have`-expression is consistent with `let`-expression --- library/init/core.lean | 30 +++--- library/init/data/dlist.lean | 4 +- library/init/data/fin/basic.lean | 2 +- library/init/data/hashmap/basic.lean | 10 +- library/init/data/list/basic.lean | 8 +- library/init/data/nat/basic.lean | 132 ++++++++++++++------------- library/init/data/nat/div.lean | 16 ++-- library/init/wf.lean | 20 ++-- src/frontends/lean/builtin_exprs.cpp | 2 +- 9 files changed, 113 insertions(+), 111 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index 4be339480c..9f1c8c5f84 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -266,8 +266,8 @@ infix ≅ := Heq @[matchPattern] def Heq.rfl {α : Sort u} {a : α} : a ≅ a := Heq.refl a theorem eqOfHeq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' := -have ∀ (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') (h₂ : α = α'), (Eq.recOn h₂ a : α') = a', from - fun (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') => Heq.recOn h₁ (fun h₂ : α = α => rfl), +have ∀ (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') (h₂ : α = α'), (Eq.recOn h₂ a : α') = a' := + fun (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') => Heq.recOn h₁ (fun h₂ : α = α => rfl); show (Eq.ndrecOn (Eq.refl α) a : α) = a', from this α a' h (Eq.refl α) @@ -825,7 +825,7 @@ Eq.recOn h Iff.rfl theorem neqOfNotIff {a b : Prop} : ¬(a ↔ b) → a ≠ b := fun h₁ h₂ => -have a ↔ b, from Eq.subst h₂ (Iff.refl a), +have a ↔ b, from Eq.subst h₂ (Iff.refl a); absurd this h₁ theorem notIffNotOfIff (h₁ : a ↔ b) : ¬a ↔ ¬b := @@ -1437,7 +1437,7 @@ protected def hrecOn (q : Quot r) (f : Π a, β (Quot.mk r a)) (c : ∀ (a b : α) (p : r a b), f a ≅ f b) : β q := Quot.recOn q f $ fun a b p => eqOfHeq $ - have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a, from eqRecHeq (sound p) (f a), + have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a := eqRecHeq (sound p) (f a); Heq.trans p₁ (c a b p) end @@ -1705,34 +1705,34 @@ theorem chooseSpec {α : Sort u} {p : α → Prop} (h : Exists (fun x => p x)) : theorem em (p : Prop) : p ∨ ¬p := let U (x : Prop) : Prop := x = True ∨ p; let V (x : Prop) : Prop := x = False ∨ p; -have exU : Exists (fun x => U x), from ⟨True, Or.inl rfl⟩, -have exV : Exists (fun x => V x), from ⟨False, Or.inl rfl⟩, +have exU : Exists (fun x => U x), from ⟨True, Or.inl rfl⟩; +have exV : Exists (fun x => V x), from ⟨False, Or.inl rfl⟩; let u : Prop := choose exU; let v : Prop := choose exV; -have uDef : U u, from chooseSpec exU, -have vDef : V v, from chooseSpec exV, +have uDef : U u, from chooseSpec exU; +have vDef : V v, from chooseSpec exV; have notUvOrP : u ≠ v ∨ p, from Or.elim uDef (fun hut : u = True => Or.elim vDef (fun hvf : v = False => - have hne : u ≠ v, from hvf.symm ▸ hut.symm ▸ trueNeFalse, + have hne : u ≠ v, from hvf.symm ▸ hut.symm ▸ trueNeFalse; Or.inl hne) Or.inr) - Or.inr, + Or.inr; have pImpliesUv : p → u = v, from fun hp : p => have hpred : U = V, from funext $ fun x : Prop => have hl : (x = True ∨ p) → (x = False ∨ p), from - fun a => Or.inr hp, + fun a => Or.inr hp; have hr : (x = False ∨ p) → (x = True ∨ p), from - fun a => Or.inr hp, + fun a => Or.inr hp; show (x = True ∨ p) = (x = False ∨ p), from - propext (Iff.intro hl hr), + propext (Iff.intro hl hr); have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV, from - hpred ▸ fun exU exV => rfl, - show u = v, from h₀ _ _, + hpred ▸ fun exU exV => rfl; + show u = v, from h₀ _ _; Or.elim notUvOrP (fun (hne : u ≠ v) => Or.inr (mt pImpliesUv hne)) Or.inl diff --git a/library/init/data/dlist.lean b/library/init/data/dlist.lean index 65b8b3e228..81268fc0b7 100644 --- a/library/init/data/dlist.lean +++ b/library/init/data/dlist.lean @@ -40,8 +40,8 @@ def cons : α → DList α → DList α | a ⟨f, h⟩ := ⟨fun t => a :: f t, fun t => show a :: f t = a :: f [] ++ t, from - have h₁ : a :: f t = a :: (f nil ++ t), from h t ▸ rfl, - have h₂ : a :: (f nil ++ t) = a :: f nil ++ t, from (consAppend _ _ _).symm, + have h₁ : a :: f t = a :: (f nil ++ t) := h t ▸ rfl; + have h₂ : a :: (f nil ++ t) = a :: f nil ++ t := (consAppend _ _ _).symm; Eq.trans h₁ h₂⟩ def append : DList α → DList α → DList α diff --git a/library/init/data/fin/basic.lean b/library/init/data/fin/basic.lean index 5c2e569c7a..1480c9bedb 100644 --- a/library/init/data/fin/basic.lean +++ b/library/init/data/fin/basic.lean @@ -36,7 +36,7 @@ def ofNat {n : Nat} (a : Nat) : Fin (succ n) := private theorem mlt {n b : Nat} : ∀ {a}, n > a → b % n < n | 0 h := Nat.modLt _ h | (a+1) h := - have n > 0, from Nat.ltTrans (Nat.zeroLtSucc _) h, + have n > 0, from Nat.ltTrans (Nat.zeroLtSucc _) h; Nat.modLt _ this protected def add : Fin n → Fin n → Fin n diff --git a/library/init/data/hashmap/basic.lean b/library/init/data/hashmap/basic.lean index 8fb94e0e40..6fac41a4b7 100644 --- a/library/init/data/hashmap/basic.lean +++ b/library/init/data/hashmap/basic.lean @@ -24,12 +24,12 @@ let n := if nbuckets = 0 then 8 else nbuckets; { size := 0, buckets := ⟨ mkArray n AssocList.nil, - have p₁ : (mkArray n (@AssocList.nil α β)).size = n, from Array.szMkArrayEq _ _, - have p₂ : n = (if nbuckets = 0 then 8 else nbuckets), from rfl, + have p₁ : (mkArray n (@AssocList.nil α β)).size = n, from Array.szMkArrayEq _ _; + 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.zeroLtSucc _ - | (Nat.succ x) := Nat.zeroLtSucc _, + | (Nat.succ x) := Nat.zeroLtSucc _; transRelRight Greater (Eq.trans p₁ p₂) p₃ ⟩ } namespace HashMapImp @@ -80,8 +80,8 @@ partial def moveEntries [Hashable α] : Nat → Array (AssocList α β) → Hash def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β := let nbuckets := buckets.val.size * 2; -have aux₁ : nbuckets > 0, from Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero), -have aux₂ : (mkArray nbuckets (@AssocList.nil α β)).size = nbuckets, from Array.szMkArrayEq _ _, +have aux₁ : nbuckets > 0, from Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero); +have aux₂ : (mkArray nbuckets (@AssocList.nil α β)).size = nbuckets, from Array.szMkArrayEq _ _; let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, aux₂.symm ▸ aux₁⟩; { size := size, buckets := moveEntries 0 buckets.val new_buckets } diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index d737d221e4..9c935934be 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -71,10 +71,10 @@ theorem appendAssoc : ∀ (as bs cs : List α), (as ++ bs) ++ cs = as ++ (bs ++ | [] bs cs := rfl | (a::as) bs cs := show ((a::as) ++ bs) ++ cs = (a::as) ++ (bs ++ cs), from - have h₁ : ((a::as) ++ bs) ++ cs = a::(as++bs) ++ cs, from congrArg (fun ds => ds ++ cs) (consAppend a as bs), - have h₂ : a::(as++bs) ++ cs = a::((as++bs) ++ cs), from consAppend a (as++bs) cs, - have h₃ : a::((as++bs) ++ cs) = a::(as ++ (bs ++ cs)), from congrArg (fun as => a::as) (appendAssoc as bs cs), - have h₄ : a::(as ++ (bs ++ cs)) = (a::as ++ (bs ++ cs)), from (consAppend a as (bs++cs)).symm, + have h₁ : ((a::as) ++ bs) ++ cs = a::(as++bs) ++ cs, from congrArg (fun ds => ds ++ cs) (consAppend a as bs); + have h₂ : a::(as++bs) ++ cs = a::((as++bs) ++ cs), from consAppend a (as++bs) cs; + have h₃ : a::((as++bs) ++ cs) = a::(as ++ (bs ++ cs)), from congrArg (fun as => a::as) (appendAssoc as bs cs); + have h₄ : a::(as ++ (bs ++ cs)) = (a::as ++ (bs ++ cs)), from (consAppend a as (bs++cs)).symm; Eq.trans (Eq.trans (Eq.trans h₁ h₂) h₃) h₄ inductive Mem : α → List α → Prop diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean index 628f84b519..084dd89101 100644 --- a/library/init/data/nat/basic.lean +++ b/library/init/data/nat/basic.lean @@ -21,8 +21,8 @@ theorem eqOfBeqEqTt : ∀ {n m : Nat}, beq n m = true → n = m | zero (succ m) h := Bool.noConfusion h | (succ n) zero h := Bool.noConfusion h | (succ n) (succ m) h := - have beq n m = true, from h, - have n = m, from eqOfBeqEqTt this, + have beq n m = true, from h; + have n = m, from eqOfBeqEqTt this; congrArg succ this theorem neOfBeqEqFf : ∀ {n m : Nat}, beq n m = false → n ≠ m @@ -30,8 +30,8 @@ theorem neOfBeqEqFf : ∀ {n m : Nat}, beq n m = false → n ≠ m | zero (succ m) h₁ h₂ := Nat.noConfusion h₂ | (succ n) zero h₁ h₂ := Nat.noConfusion h₂ | (succ n) (succ m) h₁ h₂ := - have beq n m = false, from h₁, - have n ≠ m, from neOfBeqEqFf this, + have beq n m = false, from h₁; + have n ≠ m, from neOfBeqEqFf this; Nat.noConfusion h₂ (fun h₂ => absurd h₂ this) @[extern cpp "lean::nat_dec_eq"] @@ -157,12 +157,12 @@ protected theorem addLeftCancel : ∀ {n m k : Nat}, n + m = n + k → m = k | 0 m k h := Nat.zeroAdd m ▸ Nat.zeroAdd k ▸ h | (succ n) m k h := have n+m = n+k, from - have succ (n + m) = succ (n + k), from succAdd n m ▸ succAdd n k ▸ h, - Nat.noConfusion this id, + have succ (n + m) = succ (n + k), from succAdd n m ▸ succAdd n k ▸ h; + Nat.noConfusion this id; addLeftCancel this protected theorem addRightCancel {n m k : Nat} (h : n + m = k + m) : n = k := -have m + n = m + k, from Nat.addComm n m ▸ Nat.addComm k m ▸ h, +have m + n = m + k, from Nat.addComm n m ▸ Nat.addComm k m ▸ h; Nat.addLeftCancel this /- Nat.mul theorems -/ @@ -181,7 +181,7 @@ theorem succMul : ∀ (n m : Nat), (succ n) * m = (n * m) + m | n 0 := rfl | n (succ m) := have succ (n * m + m + n) = succ (n * m + n + m), from - congrArg succ (Nat.addRightComm _ _ _), + congrArg succ (Nat.addRightComm _ _ _); (mulSucc n m).symm ▸ (mulSucc (succ n) m).symm ▸ (succMul n m).symm ▸ this protected theorem mulComm : ∀ (n m : Nat), n * m = m * n @@ -197,31 +197,31 @@ Nat.mulComm n 1 ▸ Nat.mulOne n protected theorem leftDistrib : ∀ (n m k : Nat), n * (m + k) = n * m + n * k | 0 m k := (Nat.zeroMul (m + k)).symm ▸ (Nat.zeroMul m).symm ▸ (Nat.zeroMul k).symm ▸ rfl | (succ n) m k := - have h₁ : succ n * (m + k) = n * (m + k) + (m + k), from succMul _ _, - have h₂ : n * (m + k) + (m + k) = (n * m + n * k) + (m + k), from leftDistrib n m k ▸ rfl, - have h₃ : (n * m + n * k) + (m + k) = n * m + (n * k + (m + k)), from Nat.addAssoc _ _ _, - have h₄ : n * m + (n * k + (m + k)) = n * m + (m + (n * k + k)), from congrArg (fun x => n*m + x) (Nat.addLeftComm _ _ _), - have h₅ : n * m + (m + (n * k + k)) = (n * m + m) + (n * k + k), from (Nat.addAssoc _ _ _).symm, - have h₆ : (n * m + m) + (n * k + k) = (n * m + m) + succ n * k, from succMul n k ▸ rfl, - have h₇ : (n * m + m) + succ n * k = succ n * m + succ n * k, from succMul n m ▸ rfl, + have h₁ : succ n * (m + k) = n * (m + k) + (m + k), from succMul _ _; + have h₂ : n * (m + k) + (m + k) = (n * m + n * k) + (m + k), from leftDistrib n m k ▸ rfl; + have h₃ : (n * m + n * k) + (m + k) = n * m + (n * k + (m + k)), from Nat.addAssoc _ _ _; + have h₄ : n * m + (n * k + (m + k)) = n * m + (m + (n * k + k)), from congrArg (fun x => n*m + x) (Nat.addLeftComm _ _ _); + have h₅ : n * m + (m + (n * k + k)) = (n * m + m) + (n * k + k), from (Nat.addAssoc _ _ _).symm; + have h₆ : (n * m + m) + (n * k + k) = (n * m + m) + succ n * k, from succMul n k ▸ rfl; + have h₇ : (n * m + m) + succ n * k = succ n * m + succ n * k, from succMul n m ▸ rfl; (((((h₁.trans h₂).trans h₃).trans h₄).trans h₅).trans h₆).trans h₇ protected theorem rightDistrib (n m k : Nat) : (n + m) * k = n * k + m * k := -have h₁ : (n + m) * k = k * (n + m), from Nat.mulComm _ _, -have h₂ : k * (n + m) = k * n + k * m, from Nat.leftDistrib _ _ _, -have h₃ : k * n + k * m = n * k + k * m, from Nat.mulComm n k ▸ rfl, -have h₄ : n * k + k * m = n * k + m * k, from Nat.mulComm m k ▸ rfl, +have h₁ : (n + m) * k = k * (n + m), from Nat.mulComm _ _; +have h₂ : k * (n + m) = k * n + k * m, from Nat.leftDistrib _ _ _; +have h₃ : k * n + k * m = n * k + k * m, from Nat.mulComm n k ▸ rfl; +have h₄ : n * k + k * m = n * k + m * k, from Nat.mulComm m k ▸ rfl; ((h₁.trans h₂).trans h₃).trans h₄ protected theorem mulAssoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k) | n m 0 := 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.leftDistrib _ _ _, - have h₃ : (n * m * k) + n * m * 1 = (n * m * k) + n * m, from (Nat.mulOne (n*m)).symm ▸ rfl, - have h₄ : (n * m * k) + n * m = (n * (m * k)) + n * m, from (mulAssoc n m k).symm ▸ rfl, - have h₅ : (n * (m * k)) + n * m = n * (m * k + m), from (Nat.leftDistrib n (m*k) m).symm, - have h₆ : n * (m * k + m) = n * (m * succ k), from Nat.mulSucc m k ▸ rfl, + 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.leftDistrib _ _ _; + have h₃ : (n * m * k) + n * m * 1 = (n * m * k) + n * m, from (Nat.mulOne (n*m)).symm ▸ rfl; + have h₄ : (n * m * k) + n * m = (n * (m * k)) + n * m, from (mulAssoc n m k).symm ▸ rfl; + have h₅ : (n * (m * k)) + n * m = n * (m * k + m), from (Nat.leftDistrib n (m*k) m).symm; + have h₆ : n * (m * k + m) = n * (m * succ k), from Nat.mulSucc m k ▸ rfl; ((((h₁.trans h₂).trans h₃).trans h₄).trans h₅).trans h₆ /- Inequalities -/ @@ -245,8 +245,8 @@ theorem leStep : ∀ {n m : Nat}, n ≤ m → n ≤ succ m | zero (succ n) h := rfl | (succ n) zero h := Bool.noConfusion h | (succ n) (succ m) h := - have n ≤ m, from h, - have n ≤ succ m, from leStep this, + have n ≤ m, from h; + have n ≤ succ m, from leStep this; succLeSucc this theorem zeroLe : ∀ (n : Nat), 0 ≤ n @@ -286,8 +286,8 @@ protected theorem eqOrLtOfLe : ∀ {n m: Nat}, n ≤ m → n = m ∨ n < m | zero (succ n) h := Or.inr $ zeroLe n | (succ n) zero h := Bool.noConfusion h | (succ n) (succ m) h := - have n ≤ m, from h, - have n = m ∨ n < m, from eqOrLtOfLe this, + have n ≤ m, from h; + have n = m ∨ n < m, from eqOrLtOfLe this; Or.elim this (fun h => Or.inl $ congrArg succ h) (fun h => Or.inr $ succLtSucc h) @@ -314,9 +314,9 @@ protected theorem leTrans : ∀ {n m k : Nat}, n ≤ m → m ≤ k → n ≤ k | (succ n) zero k h₁ h₂ := Bool.noConfusion h₁ | (succ n) (succ m) zero h₁ h₂ := Bool.noConfusion h₂ | (succ n) (succ m) (succ k) h₁ h₂ := - have h₁' : n ≤ m, from h₁, - have h₂' : m ≤ k, from h₂, - have n ≤ k, from leTrans h₁' h₂', + have h₁' : n ≤ m, from h₁; + have h₂' : m ≤ k, from h₂; + have n ≤ k, from leTrans h₁' h₂'; succLeSucc this theorem predLe : ∀ (n : Nat), pred n ≤ n @@ -374,9 +374,9 @@ protected theorem leAntisymm : ∀ {n m : Nat}, n ≤ m → m ≤ n → n = m | (succ n) zero h₁ h₂ := Bool.noConfusion h₁ | zero (succ m) h₁ h₂ := Bool.noConfusion h₂ | (succ n) (succ m) h₁ h₂ := - have h₁' : n ≤ m, from h₁, - have h₂' : m ≤ n, from h₂, - have n = m, from leAntisymm h₁' h₂', + have h₁' : n ≤ m, from h₁; + have h₂' : m ≤ n, from h₂; + have n = m, from leAntisymm h₁' h₂'; congrArg succ this protected theorem ltOrGe : ∀ (n m : Nat), n < m ∨ n ≥ m @@ -416,8 +416,8 @@ theorem ltOrEqOrLeSucc {m n : Nat} (h : m ≤ succ n) : m ≤ n ∨ m = succ n : Decidable.byCases (fun (h' : m = succ n) => Or.inr h') (fun (h' : m ≠ succ n) => - have m < succ n, from Nat.ltOfLeAndNe h h', - have succ m ≤ succ n, from succLeOfLt this, + have m < succ n, from Nat.ltOfLeAndNe h h'; + have succ m ≤ succ n, from succLeOfLt this; Or.inl (leOfSuccLeSucc this)) theorem leAddRight : ∀ (n k : Nat), n ≤ n + k @@ -432,8 +432,8 @@ theorem le.dest : ∀ {n m : Nat}, n ≤ m → Exists (fun k => n + k = m) | zero (succ n) h := ⟨succ n, show 0 + succ n = succ n, from (Nat.addComm 0 (succ n)).symm ▸ rfl⟩ | (succ n) zero h := Bool.noConfusion h | (succ n) (succ m) h := - have n ≤ m, from h, - have Exists (fun k => n + k = m), from le.dest this, + have n ≤ m, from h; + have Exists (fun k => n + k = m), from le.dest this; match this with | ⟨k, h⟩ := ⟨k, show succ n + k = succ m, from ((succAdd n k).symm ▸ h ▸ rfl)⟩ @@ -443,7 +443,9 @@ h ▸ leAddRight n k protected theorem notLeOfGt {n m : Nat} (h : n > m) : ¬ n ≤ m := fun h₁ => Or.elim (Nat.ltOrGe n m) (fun h₂ => absurd (Nat.ltTrans h h₂) (Nat.ltIrrefl _)) - (fun h₂ => have Heq : n = m, from Nat.leAntisymm h₁ h₂, absurd (@Eq.subst _ _ _ _ Heq h) (Nat.ltIrrefl m)) + (fun h₂ => + have Heq : n = m, from Nat.leAntisymm h₁ h₂; + absurd (@Eq.subst _ _ _ _ Heq h) (Nat.ltIrrefl m)) theorem gtOfNotLe {n m : Nat} (h : ¬ n ≤ m) : n > m := Or.elim (Nat.ltOrGe m n) @@ -458,14 +460,14 @@ Or.elim (Nat.ltOrGe n m) protected theorem addLeAddLeft {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k + m := match le.dest h with | ⟨w, hw⟩ := - have h₁ : k + n + w = k + (n + w), from Nat.addAssoc _ _ _, - have h₂ : k + (n + w) = k + m, from congrArg _ hw, + have h₁ : k + n + w = k + (n + w), from Nat.addAssoc _ _ _; + have h₂ : k + (n + w) = k + m, from congrArg _ hw; le.intro $ h₁.trans h₂ protected theorem addLeAddRight {n m : Nat} (h : n ≤ m) (k : Nat) : n + k ≤ m + k := -have h₁ : n + k = k + n, from Nat.addComm _ _, -have h₂ : k + n ≤ k + m, from Nat.addLeAddLeft h k, -have h₃ : k + m = m + k, from Nat.addComm _ _, +have h₁ : n + k = k + n, from Nat.addComm _ _; +have h₂ : k + n ≤ k + m, from Nat.addLeAddLeft h k; +have h₃ : k + m = m + k, from Nat.addComm _ _; transRelLeft (fun a b => a ≤ b) (transRelRight (fun a b => a ≤ b) h₁ h₂) h₃ protected theorem addLtAddLeft {n m : Nat} (h : n < m) (k : Nat) : k + n < k + m := @@ -507,8 +509,8 @@ congrArg succ (succAdd n n) protected theorem zeroLtBit0 : ∀ {n : Nat}, n ≠ 0 → 0 < bit0 n | 0 h := absurd rfl h | (succ n) h := - have h₁ : 0 < succ (succ (bit0 n)), from zeroLtSucc _, - have h₂ : succ (succ (bit0 n)) = bit0 (succ n), from (Nat.bit0SuccEq n).symm, + have h₁ : 0 < succ (succ (bit0 n)), from zeroLtSucc _; + have h₂ : succ (succ (bit0 n)) = bit0 (succ n), from (Nat.bit0SuccEq n).symm; transRelLeft (fun a b => a < b) h₁ h₂ protected theorem zeroLtBit1 (n : Nat) : 0 < bit1 n := @@ -538,26 +540,26 @@ protected theorem bit1NeOne : ∀ {n : Nat}, n ≠ 0 → bit1 n ≠ 1 protected theorem bit0NeOne : ∀ n : Nat, bit0 n ≠ 1 | 0 h := absurd h (Ne.symm Nat.oneNeZero) | (n+1) h := - have h1 : succ (succ (n + n)) = 1, from succAdd n n ▸ h, + have h1 : succ (succ (n + n)) = 1, from succAdd n n ▸ h; Nat.noConfusion h1 (fun h2 => absurd h2 (succNeZero (n + n))) protected theorem addSelfNeOne : ∀ (n : Nat), n + n ≠ 1 | 0 h := Nat.noConfusion h | (n+1) h := - have h1 : succ (succ (n + n)) = 1, from succAdd n n ▸ h, + have h1 : succ (succ (n + n)) = 1, from succAdd n n ▸ h; Nat.noConfusion h1 (fun h2 => absurd h2 (Nat.succNeZero (n + n))) protected theorem bit1NeBit0 : ∀ (n m : Nat), bit1 n ≠ bit0 m | 0 m h := absurd h (Ne.symm (Nat.addSelfNeOne m)) | (n+1) 0 h := - have h1 : succ (bit0 (succ n)) = 0, from h, + have h1 : succ (bit0 (succ n)) = 0, from h; absurd h1 (Nat.succNeZero _) | (n+1) (m+1) h := have h1 : succ (succ (bit1 n)) = succ (succ (bit0 m)), from - Nat.bit0SuccEq m ▸ Nat.bit1SuccEq n ▸ h, + Nat.bit0SuccEq m ▸ Nat.bit1SuccEq n ▸ h; have h2 : bit1 n = bit0 m, from - Nat.noConfusion h1 (fun h2' => Nat.noConfusion h2' (fun h2'' => h2'')), + Nat.noConfusion h1 (fun h2' => Nat.noConfusion h2' (fun h2'' => h2'')); absurd h2 (bit1NeBit0 n m) protected theorem bit0NeBit1 : ∀ (n m : Nat), bit0 n ≠ bit1 m := @@ -568,17 +570,17 @@ protected theorem bit0Inj : ∀ {n m : Nat}, bit0 n = bit0 m → n = m | 0 (m+1) h := absurd h.symm (succNeZero _) | (n+1) 0 h := absurd h (succNeZero _) | (n+1) (m+1) h := - have (n+1) + n = (m+1) + m, from Nat.noConfusion h id, - have n + (n+1) = m + (m+1), from Nat.addComm (m+1) m ▸ Nat.addComm (n+1) n ▸ this, - have succ (n + n) = succ (m + m), from this, - have n + n = m + m, from Nat.noConfusion this id, - have n = m, from bit0Inj this, + have (n+1) + n = (m+1) + m, from Nat.noConfusion h id; + have n + (n+1) = m + (m+1), from Nat.addComm (m+1) m ▸ Nat.addComm (n+1) n ▸ this; + have succ (n + n) = succ (m + m), from this; + have n + n = m + m, from Nat.noConfusion this id; + have n = m, from bit0Inj this; congrArg (fun a => a + 1) this protected theorem bit1Inj : ∀ {n m : Nat}, bit1 n = bit1 m → n = m := fun n m h => -have succ (bit0 n) = succ (bit0 m), from Nat.bit1EqSuccBit0 n ▸ Nat.bit1EqSuccBit0 m ▸ h, -have bit0 n = bit0 m, from Nat.noConfusion this id, +have succ (bit0 n) = succ (bit0 m), from Nat.bit1EqSuccBit0 n ▸ Nat.bit1EqSuccBit0 m ▸ h; +have bit0 n = bit0 m, from Nat.noConfusion this id; Nat.bit0Inj this protected theorem bit0Ne {n m : Nat} : n ≠ m → bit0 n ≠ bit0 m := @@ -625,9 +627,9 @@ ltSuccOfLe (Nat.addLeAdd h h) protected theorem bit1LtBit0 : ∀ {n m : Nat}, n < m → bit1 n < bit0 m | n 0 h := absurd h (notLtZero _) | n (succ m) h := - have n ≤ m, from leOfLtSucc h, - have succ (n + n) ≤ succ (m + m), from succLeSucc (addLeAdd this this), - have succ (n + n) ≤ succ m + m, from (succAdd m m).symm ▸ this, + have n ≤ m, from leOfLtSucc h; + have succ (n + n) ≤ succ (m + m), from succLeSucc (addLeAdd this this); + have succ (n + n) ≤ succ m + m, from (succAdd m m).symm ▸ this; show succ (n + n) < succ (succ m + m), from ltSuccOfLe this protected theorem oneLeBit1 (n : Nat) : 1 ≤ bit1 n := @@ -646,7 +648,7 @@ protected theorem oneLeBit0 : ∀ (n : Nat), n ≠ 0 → 1 ≤ bit0 n theorem mulLeMulLeft {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m := match le.dest h with | ⟨l, hl⟩ := - have k * n + k * l = k * m, from Nat.leftDistrib k n l ▸ hl.symm ▸ rfl, + have k * n + k * l = k * m, from Nat.leftDistrib k n l ▸ hl.symm ▸ rfl; le.intro this theorem mulLeMulRight {n m : Nat} (k : Nat) (h : n ≤ m) : n * k ≤ m * k := @@ -662,7 +664,7 @@ protected theorem mulLtMulOfPosRight {n m k : Nat} (h : n < m) (hk : k > 0) : n Nat.mulComm k m ▸ Nat.mulComm k n ▸ Nat.mulLtMulOfPosLeft h hk protected theorem mulPos {n m : Nat} (ha : n > 0) (hb : m > 0) : n * m > 0 := -have h : 0 * m < n * m, from Nat.mulLtMulOfPosRight ha hb, +have h : 0 * m < n * m, from Nat.mulLtMulOfPosRight ha hb; Nat.zeroMul m ▸ h /- power -/ @@ -678,7 +680,7 @@ theorem powLePowOfLeLeft {n m : Nat} (h : n ≤ m) : ∀ i : Nat, n^i ≤ m^i theorem powLePowOfLeRight {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j | 0 h := - have i = 0, from eqZeroOfLeZero h, + have i = 0, from eqZeroOfLeZero h; this.symm ▸ Nat.leRefl _ | (succ j) h := Or.elim (ltOrEqOrLeSucc h) diff --git a/library/init/data/nat/div.lean b/library/init/data/nat/div.lean index ddea771616..bf12ee9916 100644 --- a/library/init/data/nat/div.lean +++ b/library/init/data/nat/div.lean @@ -69,12 +69,12 @@ div.inductionOn x y h₁ h₂ theorem modZero (a : Nat) : a % 0 = a := suffices (if 0 < 0 ∧ 0 ≤ a then (a - 0) % 0 else a) = a, from (modDef a 0).symm ▸ this, -have h : ¬ (0 < 0 ∧ 0 ≤ a), from fun ⟨h₁, _⟩ => absurd h₁ (Nat.ltIrrefl _), +have h : ¬ (0 < 0 ∧ 0 ≤ a), from fun ⟨h₁, _⟩ => absurd h₁ (Nat.ltIrrefl _); ifNeg h theorem modEqOfLt {a b : Nat} (h : a < b) : a % b = a := suffices (if 0 < b ∧ b ≤ a then (a - b) % b else a) = a, from (modDef a b).symm ▸ this, -have h' : ¬(0 < b ∧ b ≤ a), from fun ⟨_, h₁⟩ => absurd h₁ (Nat.notLeOfGt h), +have h' : ¬(0 < b ∧ b ≤ a), from fun ⟨_, h₁⟩ => absurd h₁ (Nat.notLeOfGt h); ifNeg h' theorem modEqSubMod {a b : Nat} (h : a ≥ b) : a % b = (a - b) % b := @@ -85,17 +85,17 @@ Or.elim (eqZeroOrPos b) theorem modLt (x : Nat) {y : Nat} : y > 0 → x % y < y := mod.inductionOn x y (fun (x y) ⟨_, h₁⟩ (h₂ h₃) => - have ih : (x - y) % y < y, from h₂ h₃, - have Heq : x % y = (x - y) % y, from modEqSubMod h₁, + have ih : (x - y) % y < y, from h₂ h₃; + have Heq : x % y = (x - y) % y, from modEqSubMod h₁; Heq.symm ▸ ih) (fun x y h₁ h₂ => - have h₁ : ¬ 0 < y ∨ ¬ y ≤ x, from Iff.mp (Decidable.notAndIffOrNot _ _) h₁, + have h₁ : ¬ 0 < y ∨ ¬ y ≤ x, from Iff.mp (Decidable.notAndIffOrNot _ _) h₁; Or.elim h₁ (fun h₁ => absurd h₂ h₁) (fun h₁ => - have hgt : y > x, from gtOfNotLe h₁, - have Heq : x % y = x, from modEqOfLt hgt, - Heq.symm ▸ hgt)) + have hgt : y > x, from gtOfNotLe h₁; + have Heq : x % y = x, from modEqOfLt hgt; + Heq.symm ▸ hgt)) theorem modLe (x y : Nat) : x % y ≤ x := Or.elim (Nat.ltOrGe x y) diff --git a/library/init/wf.lean b/library/init/wf.lean index 5b7d17961c..8e2dd56bc8 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -180,7 +180,7 @@ Acc.ndrecOn aca $ fun xa aca iha b => @Prod.Lex.recOn α β ra rb (fun p₁ p₂ _ => fst p₂ = xa → snd p₂ = xb → Acc (Lex ra rb) p₁) p (xa, xb) lt (fun (a₁ b₁ a₂ b₂ h) (Eq₂ : a₂ = xa) (Eq₃ : b₂ = xb) => iha a₁ (Eq.recOn Eq₂ h) b₁) - (fun (a b₁ b₂ h) (Eq₂ : a = xa) (Eq₃ : b₂ = xb) => Eq.recOn Eq₂.symm (ihb b₁ (Eq.recOn Eq₃ h))), + (fun (a b₁ b₂ h) (Eq₂ : a = xa) (Eq₃ : b₂ = xb) => Eq.recOn Eq₂.symm (ihb b₁ (Eq.recOn Eq₃ h))); aux rfl rfl -- The lexicographical order of well founded relations is well-founded @@ -227,19 +227,19 @@ Acc.ndrecOn aca $ fun (xa aca) (iha : ∀ y, r y xa → ∀ b : β y, Acc (Lex r (fun (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂) (h : r a₁ a₂) (Eq₂ : a₂ = xa) (Eq₃ : b₂ ≅ xb) => have aux : (∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩) → r a₁ a₂ → ∀ (b₁ : β a₁), Acc (Lex r s) ⟨a₁, b₁⟩, - from Eq.subst Eq₂ (fun iha h b₁ => iha a₁ h b₁), + from Eq.subst Eq₂ (fun iha h b₁ => iha a₁ h b₁); aux iha h b₁) (fun (a : α) (b₁ b₂ : β a) (h : s a b₁ b₂) (Eq₂ : a = xa) (Eq₃ : b₂ ≅ xb) => have aux : ∀ (xb : β xa), (∀ (y : β xa), s xa y xb → Acc (s xa) y) → (∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩) → Lex r s p ⟨xa, xb⟩ → ∀ (b₁ : β a), s a b₁ b₂ → b₂ ≅ xb → Acc (Lex r s) ⟨a, b₁⟩, from Eq.subst Eq₂ $ fun xb acb ihb lt b₁ h Eq₃ => - have newEq₃ : b₂ = xb, from eqOfHeq Eq₃, + have newEq₃ : b₂ = xb, from eqOfHeq Eq₃; have aux : (∀ (y : β a), s a y xb → Acc (Lex r s) ⟨a, y⟩) → ∀ (b₁ : β a), s a b₁ b₂ → Acc (Lex r s) ⟨a, b₁⟩, - from Eq.subst newEq₃ (fun ihb b₁ h => ihb b₁ h), - aux ihb b₁ h, - aux xb acb ihb lt b₁ h Eq₃), + from Eq.subst newEq₃ (fun ihb b₁ h => ihb b₁ h); + aux ihb b₁ h; + aux xb acb ihb lt b₁ h Eq₃); aux rfl (Heq.refl xb) -- The lexicographical order of well founded relations is well-founded @@ -281,13 +281,13 @@ Acc.recOn acb $ fun (xb acb) (ihb : ∀ y, s y xb → ∀ a, Acc (RevLex r s) p ⟨xa, xb⟩ lt (fun (a₁ a₂ b) (h : r a₁ a₂) (Eq₂ : a₂ = xa) (Eq₃ : b = xb) => show Acc (RevLex r s) ⟨a₁, b⟩, from - have r₁ : r a₁ xa, from Eq.recOn Eq₂ h, - have aux : Acc (RevLex r s) ⟨a₁, xb⟩, from iha a₁ r₁, + have r₁ : r a₁ xa, from Eq.recOn Eq₂ h; + have aux : Acc (RevLex r s) ⟨a₁, xb⟩, from iha a₁ r₁; Eq.recOn (Eq.symm Eq₃) aux) (fun (a₁ b₁ a₂ b₂) (h : s b₁ b₂) (Eq₂ : a₂ = xa) (Eq₃ : b₂ = xb) => show Acc (RevLex r s) (mk a₁ b₁), from - have s₁ : s b₁ xb, from Eq.recOn Eq₃ h, - ihb b₁ s₁ a₁), + have s₁ : s b₁ xb, from Eq.recOn Eq₃ h; + ihb b₁ s₁ a₁); aux rfl rfl def revLexWf (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) := diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 18c98c33fc..34545a7c13 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -417,7 +417,7 @@ static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos) p.check_token_next(get_comma_tk(), "invalid 'have' declaration, ',' expected"); proof = parse_proof(p); } - p.check_token_next(get_comma_tk(), "invalid 'have' declaration, ',' expected"); + p.check_token_next(get_semicolon_tk(), "invalid 'have' declaration, ';' expected"); parser::local_scope scope(p); expr l = p.save_pos(mk_local(id, prop), pos); p.add_local(l);