From c665d5e20a22d0e9957d03ddc62deb552a69f6bf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Nov 2020 15:21:57 -0800 Subject: [PATCH] chore: cleanup --- src/Init/Classical.lean | 8 +- src/Init/Core.lean | 140 +++------------------------------ src/Init/Data/Array/Basic.lean | 2 +- src/Init/Data/Nat/Basic.lean | 19 ++--- src/Std/Data/HashMap.lean | 14 +--- src/Std/Data/HashSet.lean | 14 +--- 6 files changed, 30 insertions(+), 167 deletions(-) diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index 3051aa4775..e658a639d0 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -113,10 +113,10 @@ theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : ∀ x, β x → Pr theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : (∀ x, Exists (fun y => p x y)) ↔ Exists (fun (f : ∀ x, b x) => ∀ x, p x (f x)) := ⟨axiomOfChoice, fun ⟨f, hw⟩ (x) => ⟨f x, hw x⟩⟩ -theorem propComplete (a : Prop) : a = True ∨ a = False := - match em a with - | Or.inl t => Or.inl (eqTrueIntro t) - | Or.inr f => Or.inr (eqFalseIntro f) +theorem propComplete (a : Prop) : a = True ∨ a = False := by + cases em a + | inl _ => apply Or.inl; apply propext; apply Iff.intro; { intros; apply True.intro }; { intro; assumption } + | inr hn => apply Or.inr; apply propext; apply Iff.intro; { intro h; exact hn h }; { intro h; apply False.elim h } -- this supercedes byCases in Decidable theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q := diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 096b13cc34..c609dd0713 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -322,13 +322,6 @@ protected def Nat.prio := std.priority.default + 100 def std.prec.max : Nat := 1024 -- the strength of application, identifiers, (, [, etc. def std.prec.arrow : Nat := 25 -/- -The next def is "max + 10". It can be used e.g. for postfix operations that should -be stronger than application. --/ - -def std.prec.maxPlus : Nat := std.prec.max + 10 - /- Remark: tasks have an efficient implementation in the runtime. -/ structure Task (α : Type u) : Type u := pure :: (get : α) @@ -449,21 +442,6 @@ theorem congrFun {α : Sort u} {β : α → Sort v} {f g : ∀ x, β x} (h : f = theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂ := congr rfl h -theorem transRelLeft {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c := - h₂ ▸ h₁ - -theorem transRelRight {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c := - h₁ ▸ h₂ - -theorem ofEqTrue {p : Prop} (h : p = True) : p := - h ▸ trivial - -theorem notOfEqFalse {p : Prop} (h : p = False) : ¬p := - fun hp => h ▸ hp - -theorem castProofIrrel {α β : Sort u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a := - rfl - theorem castEq {α : Sort u} (h : α = α) (a : α) : cast h a = a := rfl @@ -552,9 +530,6 @@ end theorem eqRecHEq {α : Sort u} {φ : α → Sort v} : {a a' : α} → (h : a = a') → (p : φ a) → (Eq.recOn (motive := fun x _ => φ x) h p) ≅ p | a, _, rfl, p => HEq.refl p -theorem ofHEqTrue {a : Prop} (h : a ≅ True) : a := - ofEqTrue (eqOfHEq h) - theorem heqOfEqRecEq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) : a ≅ b := by subst h₁ apply heqOfEq @@ -566,16 +541,6 @@ theorem castHEq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a variables {a b c d : Prop} -/- xor -/ -def Xor (a b : Prop) : Prop := - (a ∧ ¬ b) ∨ (b ∧ ¬ a) - -theorem Iff.left : (a ↔ b) → a → b := - Iff.mp - -theorem Iff.right : (a ↔ b) → b → a := - Iff.mpr - theorem iffIffImpliesAndImplies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) := Iff.intro (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right) @@ -591,44 +556,11 @@ theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c := (fun hc => Iff.mpr h₁ (Iff.mpr h₂ hc)) theorem Iff.symm (h : a ↔ b) : b ↔ a := - Iff.intro (Iff.right h) (Iff.left h) + Iff.intro (Iff.mpr h) (Iff.mp h) theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm -theorem Eq.toIff {a b : Prop} (h : a = b) : a ↔ b := - 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); - absurd this h₁ - -theorem notIffNotOfIff (h₁ : a ↔ b) : ¬a ↔ ¬b := - Iff.intro - (fun (hna : ¬ a) (hb : b) => hna (Iff.right h₁ hb)) - (fun (hnb : ¬ b) (ha : a) => hnb (Iff.left h₁ ha)) - -theorem ofIffTrue (h : a ↔ True) : a := - Iff.mp (Iff.symm h) trivial - -theorem notOfIffFalse : (a ↔ False) → ¬a := - Iff.mp - -theorem iffTrueIntro (h : a) : a ↔ True := - Iff.intro - (fun hl => trivial) - (fun hr => h) - -theorem iffFalseIntro (h : ¬a) : a ↔ False := - Iff.intro h (False.rec (fun _ => a)) - -theorem notNotIntro (ha : a) : ¬¬a := - fun hna => hna ha - -theorem notTrue : (¬ True) ↔ False := - iffFalseIntro (notNotIntro trivial) - /- Exists -/ theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop} @@ -648,7 +580,7 @@ instance {α : Type u} [DecidableEq α] : BEq α := theorem decideTrueEqTrue (h : Decidable True) : @decide True h = true := match h with | isTrue h => rfl - | isFalse h => False.elim (Iff.mp notTrue h) + | isFalse h => False.elim $ h ⟨⟩ theorem decideFalseEqFalse (h : Decidable False) : @decide False h = false := match h with @@ -719,9 +651,6 @@ theorem byContradiction [dec : Decidable p] (h : ¬p → False) : p := theorem ofNotNot [Decidable p] : ¬ ¬ p → p := fun hnn => byContradiction (fun hn => absurd hn hnn) -theorem notNotIff (p) [Decidable p] : (¬ ¬ p) ↔ p := - Iff.intro ofNotNot notNotIntro - theorem notAndIffOrNot (p q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∧ q) ↔ ¬ p ∨ ¬ q := Iff.intro (fun h => match d₁, d₂ with @@ -737,11 +666,13 @@ end Decidable section variables {p q : Prop} @[inline] def decidableOfDecidableOfIff (hp : Decidable p) (h : p ↔ q) : Decidable q := - if hp : p then isTrue (Iff.mp h hp) - else isFalse (Iff.mp (notIffNotOfIff h) hp) + if hp : p then + isTrue (Iff.mp h hp) + else + isFalse fun hq => absurd (Iff.mpr h hq) hp @[inline] def decidableOfDecidableOfEq (hp : Decidable p) (h : p = q) : Decidable q := - decidableOfDecidableOfIff hp h.toIff + h ▸ hp end section @@ -783,21 +714,6 @@ instance [Decidable p] [Decidable q] : Decidable (p ↔ q) := isFalse fun h => hp (h.2 hq) else isTrue ⟨fun h => absurd h hp, fun h => absurd h hq⟩ - -instance [Decidable p] [Decidable q] : Decidable (Xor p q) := - if hp : p then - if hq : q then - isFalse fun h => match h with - | Or.inl ⟨_, h⟩ => h hq - | Or.inr ⟨_, h⟩ => h hp - else - isTrue $ Or.inl ⟨hp, hq⟩ - else if hq : q then - isTrue $ Or.inr ⟨hq, hp⟩ - else - isFalse fun h => match h with - | Or.inl ⟨h, _⟩ => hp h - | Or.inr ⟨h, _⟩ => hq h end @[inline] instance {α : Sort u} [DecidableEq α] (a b : α) : Decidable (a ≠ b) := @@ -805,14 +721,11 @@ end | isTrue h => isFalse $ fun h' => absurd h h' | isFalse h => isTrue h -theorem Bool.falseNeTrue (h : false = true) : False := - Bool.noConfusion h - @[inline] instance : DecidableEq Bool := fun a b => match a, b with | false, false => isTrue rfl - | false, true => isFalse Bool.falseNeTrue - | true, false => isFalse (Ne.symm Bool.falseNeTrue) + | false, true => isFalse fun h => Bool.noConfusion h + | true, false => isFalse fun h => Bool.noConfusion h | true, true => isTrue rfl /- if-then-else expression theorems -/ @@ -996,32 +909,6 @@ inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop | base : ∀ a b, r a b → TC r a b | trans : ∀ a b c, TC r a b → TC r b c → TC r a c -section Binary -variables {α : Type u} {β : Type v} -variable (f : α → α → α) - -def Commutative := - ∀ a b, f a b = f b a - -def Associative := - ∀ a b c, f (f a b) c = f a (f b c) - -def RightCommutative (h : β → α → β) := - ∀ b a₁ a₂, h (h b a₁) a₂ = h (h b a₂) a₁ - -def LeftCommutative (h : α → β → β) := - ∀ a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b) - -theorem leftComm : Commutative f → Associative f → LeftCommutative f := - fun hcomm hassoc a b c => - ((Eq.symm (hassoc a b c)).trans (hcomm a b ▸ rfl : f (f a b) c = f (f b a) c)).trans (hassoc b a c) - -theorem rightComm : Commutative f → Associative f → RightCommutative f := - fun hcomm hassoc a b c => - ((hassoc a b c).trans (hcomm b c ▸ rfl : f a (f b c) = f a (f c b))).trans (Eq.symm (hassoc a c b)) - -end Binary - /- Subtype -/ namespace Subtype @@ -1030,9 +917,6 @@ def existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (f variables {α : Type u} {p : α → Prop} -theorem tagIrrelevant {a : α} (h1 h2 : p a) : mk a h1 = mk a h2 := - rfl - protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2 | ⟨x, h1⟩, ⟨_, _⟩, rfl => rfl @@ -1175,12 +1059,6 @@ end Setoid axiom propext {a b : Prop} : (a ↔ b) → a = b -theorem eqTrueIntro {a : Prop} (h : a) : a = True := - propext (iffTrueIntro h) - -theorem eqFalseIntro {a : Prop} (h : ¬a) : a = False := - propext (iffFalseIntro h) - /- Quotients -/ -- Iff can now be used to do substitutions in a calculation diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index d7f1cda12b..8b9421b494 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -55,7 +55,7 @@ def mkArray {α : Type u} (n : Nat) (v : α) : Array α := { data := fun _ => v } -theorem szMkArrayEq (n : Nat) (v : α) : (mkArray n v).sz = n := +theorem sizeMkArrayEq (n : Nat) (v : α) : (mkArray n v).size = n := rfl def empty : Array α := diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index bb20bad74f..9ee6e5c3d3 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -152,11 +152,13 @@ protected theorem addAssoc : ∀ (n m k : Nat), (n + m) + k = n + (m + k) | n, m, 0 => rfl | n, m, succ k => congrArg succ (Nat.addAssoc n m k) -protected theorem addLeftComm : ∀ (n m k : Nat), n + (m + k) = m + (n + k) := - leftComm Nat.add Nat.addComm Nat.addAssoc +protected theorem addLeftComm (n m k : Nat) : n + (m + k) = m + (n + k) := by + rw [← Nat.addAssoc, Nat.addComm n m, Nat.addAssoc] + exact rfl -protected theorem addRightComm : ∀ (n m k : Nat), (n + m) + k = (n + k) + m := - rightComm Nat.add Nat.addComm Nat.addAssoc +protected theorem addRightComm (n m k : Nat) : (n + m) + k = (n + k) + m := by + rw [Nat.addAssoc, Nat.addComm m k, ← Nat.addAssoc] + exact rfl protected theorem addLeftCancel : ∀ {n m k : Nat}, n + m = n + k → m = k | 0, m, k, h => Nat.zeroAdd m ▸ Nat.zeroAdd k ▸ h @@ -481,11 +483,10 @@ protected theorem addLeAddLeft {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k 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 _ _ - transRelLeft (fun a b => a ≤ b) (transRelRight (fun a b => a ≤ b) h₁ h₂) h₃ +protected theorem addLeAddRight {n m : Nat} (h : n ≤ m) (k : Nat) : n + k ≤ m + k := by + rw [Nat.addComm n k, Nat.addComm m k] + apply Nat.addLeAddLeft + assumption protected theorem addLtAddLeft {n m : Nat} (h : n < m) (k : Nat) : k + n < k + m := ltOfSuccLe (addSucc k n ▸ Nat.addLeAddLeft (succLeOfLt h) k) diff --git a/src/Std/Data/HashMap.lean b/src/Std/Data/HashMap.lean index 09b410ad2b..f2f981a5b7 100644 --- a/src/Std/Data/HashMap.lean +++ b/src/Std/Data/HashMap.lean @@ -12,7 +12,7 @@ def HashMapBucket (α : Type u) (β : Type v) := def HashMapBucket.update {α : Type u} {β : Type v} (data : HashMapBucket α β) (i : USize) (d : AssocList α β) (h : i.toNat < data.val.size) : HashMapBucket α β := ⟨ data.val.uset i d h, - transRelRight Greater (Array.szFSetEq (data.val) ⟨USize.toNat i, h⟩ d) data.property ⟩ + by rw [Array.szFSetEq]; exact data.property ⟩ structure HashMapImp (α : Type u) (β : Type v) := (size : Nat) @@ -23,13 +23,7 @@ def mkHashMapImp {α : Type u} {β : Type v} (nbuckets := 8) : HashMapImp α β { 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₃ : (if nbuckets = 0 then 8 else nbuckets) > 0 from - match nbuckets with - | 0 => Nat.zeroLtSucc _ - | (Nat.succ x) => Nat.zeroLtSucc _ - transRelRight Greater (Eq.trans p₁ p₂) p₃ ⟩ } + by rw [Array.sizeMkArrayEq]; cases nbuckets; decide!; apply Nat.zeroLtSucc; done ⟩ } namespace HashMapImp variables {α : Type u} {β : Type v} @@ -85,9 +79,7 @@ partial def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β := let nbuckets := buckets.val.size * 2 have nbuckets > 0 from Nat.mulPos buckets.property (decide! : 2 > 0) - have (mkArray nbuckets (@AssocList.nil α β)).size = nbuckets from Array.szMkArrayEq _ _ - have Array.size (mkArray nbuckets AssocList.nil) > 0 by rw this; assumption - let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, this⟩ + let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, by rw [Array.sizeMkArrayEq]; assumption⟩ { size := size, buckets := moveEntries 0 buckets.val new_buckets } diff --git a/src/Std/Data/HashSet.lean b/src/Std/Data/HashSet.lean index e522e36253..b8482cd1a3 100644 --- a/src/Std/Data/HashSet.lean +++ b/src/Std/Data/HashSet.lean @@ -11,7 +11,7 @@ def HashSetBucket (α : Type u) := def HashSetBucket.update {α : Type u} (data : HashSetBucket α) (i : USize) (d : List α) (h : i.toNat < data.val.size) : HashSetBucket α := ⟨ data.val.uset i d h, - transRelRight Greater (Array.szFSetEq (data.val) ⟨USize.toNat i, h⟩ d) data.property ⟩ + by rw [Array.szFSetEq]; exact data.property ⟩ structure HashSetImp (α : Type u) := (size : Nat) @@ -22,13 +22,7 @@ def mkHashSetImp {α : Type u} (nbuckets := 8) : HashSetImp α := { size := 0, buckets := ⟨ mkArray n [], - have p₁ : (mkArray n ([] : List α)).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 _ - transRelRight Greater (Eq.trans p₁ p₂) p₃ ⟩ } + by rw [Array.sizeMkArrayEq]; cases nbuckets; decide!; apply Nat.zeroLtSucc ⟩ } namespace HashSetImp variables {α : Type u} @@ -78,9 +72,7 @@ partial def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (targ def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α := let nbuckets := buckets.val.size * 2 have nbuckets > 0 from Nat.mulPos buckets.property (decide! : 2 > 0) - have (mkArray nbuckets ([] : List α)).size = nbuckets from Array.szMkArrayEq _ _ - have Array.size (mkArray nbuckets List.nil) > 0 by rw this; assumption - let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], this⟩; + let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], by rw [Array.sizeMkArrayEq]; assumption⟩ { size := size, buckets := moveEntries 0 buckets.val new_buckets }