From bb99fc400a005470b13122daf5c38da088011f1a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Nov 2020 19:16:23 -0800 Subject: [PATCH] chore: remove old crap --- src/Init/Core.lean | 116 ++++++++++++++--------------------- src/Init/Data/Nat/Basic.lean | 6 +- src/Init/Data/Nat/Div.lean | 6 +- 3 files changed, 54 insertions(+), 74 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 059b0001f0..eb0b783a80 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -646,33 +646,10 @@ theorem castHEq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a variables {a b c d : Prop} -theorem And.elim (h₁ : a ∧ b) (h₂ : a → b → c) : c := - h₂ h₁.1 h₁.2 - -theorem And.swap : a ∧ b → b ∧ a := - fun ⟨ha, hb⟩ => ⟨hb, ha⟩ - -def And.symm := @And.swap - -theorem Or.elim (h₁ : a ∨ b) (h₂ : a → c) (h₃ : b → c) : c := - match h₁ with - | Or.inl h => h₂ h - | Or.inr h => h₃ h - -theorem Or.swap (h : a ∨ b) : b ∨ a := - Or.elim h Or.inr Or.inl - -def Or.symm := - @Or.swap - /- xor -/ def Xor (a b : Prop) : Prop := (a ∧ ¬ b) ∨ (b ∧ ¬ a) -@[recursor 5] -theorem Iff.elim (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c := - h₁ h₂.1 h₂.2 - theorem Iff.left : (a ↔ b) → a → b := Iff.mp @@ -732,20 +709,6 @@ theorem notNotIntro (ha : a) : ¬¬a := theorem notTrue : (¬ True) ↔ False := iffFalseIntro (notNotIntro trivial) -/- or resolution rulses -/ - -theorem resolveLeft {a b : Prop} (h : a ∨ b) (na : ¬ a) : b := - Or.elim h (fun ha => absurd ha na) id - -theorem negResolveLeft {a b : Prop} (h : ¬ a ∨ b) (ha : a) : b := - Or.elim h (fun na => absurd ha na) id - -theorem resolveRight {a b : Prop} (h : a ∨ b) (nb : ¬ b) : a := - Or.elim h id (fun hb => absurd hb nb) - -theorem negResolveRight {a b : Prop} (h : a ∨ ¬ b) (hb : b) : a := - Or.elim h id (fun nb => absurd hb nb) - /- Exists -/ theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop} @@ -845,7 +808,9 @@ theorem notAndIffOrNot (p q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : | isTrue h₁, isTrue h₂ => absurd (And.intro h₁ h₂) h | _, isFalse h₂ => Or.inr h₂ | isFalse h₁, _ => Or.inl h₁) - (fun (h) ⟨hp, hq⟩ => Or.elim h (fun h => h hp) (fun h => h hq)) + (fun (h) ⟨hp, hq⟩ => match h with + | Or.inl h => h hp + | Or.inr h => h hq) end Decidable @@ -869,9 +834,14 @@ variables {p q : Prop} else isFalse (fun h => hp (And.left h)) @[macroInline] instance [Decidable p] [Decidable q] : Decidable (p ∨ q) := - if hp : p then isTrue (Or.inl hp) else - if hq : q then isTrue (Or.inr hq) else - isFalse (fun h => Or.elim h hp hq) + if hp : p then + isTrue (Or.inl hp) + else if hq : q then + isTrue (Or.inr hq) + else + isFalse fun h => match h with + | Or.inl h => hp h + | Or.inr h => hq h instance [Decidable p] : Decidable (¬p) := if hp : p then isFalse (absurd hp) else isTrue hp @@ -884,20 +854,30 @@ instance [Decidable p] : Decidable (¬p) := instance [Decidable p] [Decidable q] : Decidable (p ↔ q) := if hp : p then - if hq : q then isTrue ⟨fun _ => hq, fun _ => hp⟩ - else isFalse $ fun h => hq (h.1 hp) + if hq : q then + isTrue ⟨fun _ => hq, fun _ => hp⟩ + else + isFalse fun h => hq (h.1 hp) else - if hq : q then isFalse $ fun h => hp (h.2 hq) - else isTrue $ ⟨fun h => absurd h hp, fun h => absurd h hq⟩ + if hq : q then + 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 => Or.elim h (fun ⟨_, h⟩ => h hq : ¬(p ∧ ¬ q)) (fun ⟨_, h⟩ => h hp : ¬(q ∧ ¬ p))) - else isTrue $ Or.inl ⟨hp, hq⟩ + 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 - if hq : q then isTrue $ Or.inr ⟨hq, hp⟩ - else isFalse (fun h => Or.elim h (fun ⟨h, _⟩ => hp h : ¬(p ∧ ¬ q)) (fun ⟨h, _⟩ => hq h : ¬(q ∧ ¬ p))) - + 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) := @@ -1743,18 +1723,16 @@ theorem em (p : Prop) : p ∨ ¬p := 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 => - Or.elim vDef - (fun hvf => - have hne : u ≠ v from hvf.symm ▸ hut.symm ▸ trueNeFalse; - Or.inl hne) - Or.inr) - Or.inr; + match uDef, vDef with + | Or.inr h, _ => Or.inr h + | _, Or.inr h => Or.inr h + | Or.inl hut, Or.inl hvf => + have hne : u ≠ v from hvf.symm ▸ hut.symm ▸ trueNeFalse + Or.inl hne have pImpliesUv : p → u = v from fun hp => have hpred : U = V from - funext $ fun x => + funext fun x => have hl : (x = True ∨ p) → (x = False ∨ p) from fun a => Or.inr hp; have hr : (x = False ∨ p) → (x = True ∨ p) from @@ -1763,10 +1741,10 @@ theorem em (p : Prop) : p ∨ ¬p := 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₀ _ _; - Or.elim notUvOrP - (fun (hne : u ≠ v) => Or.inr (mt pImpliesUv hne)) - Or.inl + show u = v from h₀ ..; + match notUvOrP with + | Or.inl hne => Or.inr (mt pImpliesUv hne) + | Or.inr h => Or.inl h theorem existsTrueOfNonempty {α : Sort u} : Nonempty α → Exists (fun (x : α) => True) | ⟨x⟩ => ⟨x, trivial⟩ @@ -1779,9 +1757,9 @@ noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : Exists /- all propositions are Decidable -/ noncomputable def propDecidable (a : Prop) : Decidable a := - choice $ Or.elim (em a) - (fun ha => ⟨isTrue ha⟩) - (fun hna => ⟨isFalse hna⟩) + choice $ match em a with + | Or.inl h => ⟨isTrue h⟩ + | Or.inr h => ⟨isFalse h⟩ noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) := ⟨propDecidable a⟩ @@ -1825,9 +1803,9 @@ theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : ( ⟨axiomOfChoice, fun ⟨f, hw⟩ (x) => ⟨f x, hw x⟩⟩ theorem propComplete (a : Prop) : a = True ∨ a = False := - Or.elim (em a) - (fun t => Or.inl (eqTrueIntro t)) - (fun f => Or.inr (eqFalseIntro f)) + match em a with + | Or.inl t => Or.inl (eqTrueIntro t) + | Or.inr f => Or.inr (eqFalseIntro f) -- this supercedes byCases in Decidable theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q := diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 48f4df30bd..602fd52d2c 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -409,8 +409,10 @@ protected theorem leTotal (m n : Nat) : m ≤ n ∨ n ≤ m := | Or.inl h => Or.inl (Nat.leOfLt h) | Or.inr h => Or.inr h -protected theorem ltOfLeAndNe {m n : Nat} (h1 : m ≤ n) : m ≠ n → m < n := - resolveRight (Or.swap (Nat.eqOrLtOfLe h1)) +protected theorem ltOfLeAndNe {m n : Nat} (h₁ : m ≤ n) (h₂ : m ≠ n) : m < n := + match Nat.eqOrLtOfLe h₁ with + | Or.inl h => absurd h h₂ + | Or.inr h => h theorem eqZeroOfLeZero {n : Nat} (h : n ≤ 0) : n = 0 := Nat.leAntisymm h (zeroLe _) diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean index 02287e11ca..fddea61b0f 100644 --- a/src/Init/Data/Nat/Div.lean +++ b/src/Init/Data/Nat/Div.lean @@ -77,9 +77,9 @@ theorem modEqOfLt {a b : Nat} (h : a < b) : a % b = a := (modDef a b).symm ▸ this theorem modEqSubMod {a b : Nat} (h : a ≥ b) : a % b = (a - b) % b := - Or.elim (eqZeroOrPos b) - (fun h₁ => h₁.symm ▸ (Nat.subZero a).symm ▸ rfl) - (fun h₁ => (modDef a b).symm ▸ ifPos ⟨h₁, h⟩) + match eqZeroOrPos b with + | Or.inl h₁ => h₁.symm ▸ (Nat.subZero a).symm ▸ rfl + | Or.inr h₁ => (modDef a b).symm ▸ ifPos ⟨h₁, h⟩ theorem modLt (x : Nat) {y : Nat} : y > 0 → x % y < y := by refine mod.inductionOn (motive := fun x y => y > 0 → x % y < y) x y ?k1 ?k2