From b9edaf888f98c378fe228bcffc4dd7ffb6df3ea8 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 21 Mar 2019 12:55:18 +0100 Subject: [PATCH] chore(library/init/core): ne -> Ne, not -> Not --- library/init/core.lean | 34 +++++++++++++++---------------- library/init/data/list/basic.lean | 2 +- library/init/data/nat/basic.lean | 14 ++++++------- src/library/constants.cpp | 2 +- src/library/constants.txt | 2 +- 5 files changed, 27 insertions(+), 27 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index 53baec0795..6a398a1122 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -182,8 +182,8 @@ inductive False : Prop inductive Empty : Type -def not (a : Prop) : Prop := a → False -prefix `¬` := not +def Not (a : Prop) : Prop := a → False +prefix `¬` := Not inductive Eq {α : Sort u} (a : α) : α → Prop | refl : Eq a @@ -691,25 +691,25 @@ theorem castProofIrrel {α β : Sort u} (h₁ h₂ : α = β) (a : α) : cast h theorem castEq {α : Sort u} (h : α = α) (a : α) : cast h a = a := rfl -@[reducible] def ne {α : Sort u} (a b : α) := ¬(a = b) -infix ≠ := ne +@[reducible] def Ne {α : Sort u} (a b : α) := ¬(a = b) +infix ≠ := Ne -theorem ne.def {α : Sort u} (a b : α) : a ≠ b = ¬ (a = b) := rfl +theorem Ne.def {α : Sort u} (a b : α) : a ≠ b = ¬ (a = b) := rfl -section ne +section Ne variable {α : Sort u} variables {a b : α} {p : Prop} -theorem ne.intro (h : a = b → False) : a ≠ b := h +theorem Ne.intro (h : a = b → False) : a ≠ b := h -theorem ne.elim (h : a ≠ b) : a = b → False := h +theorem Ne.elim (h : a ≠ b) : a = b → False := h -theorem ne.irrefl (h : a ≠ a) : False := h rfl +theorem Ne.irrefl (h : a ≠ a) : False := h rfl -theorem ne.symm (h : a ≠ b) : b ≠ a := +theorem Ne.symm (h : a ≠ b) : b ≠ a := assume (h₁ : b = a), h (h₁.symm) -theorem falseOfNe : a ≠ a → False := ne.irrefl +theorem falseOfNe : a ≠ a → False := Ne.irrefl theorem neFalseOfSelf : p → p ≠ False := assume (hp : p) (Heq : p = False), Heq ▸ hp @@ -719,7 +719,7 @@ assume (hnp : ¬p) (Heq : p = True), (Heq ▸ hnp) trivial theorem trueNeFalse : ¬True = False := neFalseOfSelf trivial -end ne +end Ne theorem eqFfOfNeTt : ∀ {b : Bool}, b ≠ true → b = false | true h := False.elim (h rfl) @@ -901,7 +901,7 @@ iffTrueIntro notFalse theorem notCongr (h : a ↔ b) : ¬a ↔ ¬b := Iff.intro (λ h₁ h₂, h₁ (Iff.mpr h h₂)) (λ h₁ h₂, h₁ (Iff.mp h h₂)) -theorem neSelfIffFalse {α : Sort u} (a : α) : (not (a = a)) ↔ False := +theorem neSelfIffFalse {α : Sort u} (a : α) : (Not (a = a)) ↔ False := Iff.intro falseOfNe False.elim theorem eqSelfIffTrue {α : Sort u} (a : α) : (a = a) ↔ True := @@ -1240,7 +1240,7 @@ instance : DecidableEq Bool := {decEq := λ a b, match a, b with | false, false := isTrue rfl | false, true := isFalse Bool.falseNeTrue - | true, false := isFalse (ne.symm Bool.falseNeTrue) + | true, false := isFalse (Ne.symm Bool.falseNeTrue) | true, true := isTrue rfl} @[inline] @@ -2147,10 +2147,10 @@ local attribute [instance] decidableInhabited noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α := {decEq := λ x y, propDecidable (x = y)} -noncomputable def typeDecidable (α : Sort u) : Psum α (α → False) := +noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) := match (propDecidable (nonempty α)) with -| (isTrue hp) := Psum.inl (@Inhabited.default _ (inhabitedOfNonempty hp)) -| (isFalse hn) := Psum.inr (λ a, absurd (nonempty.intro a) hn) +| (isTrue hp) := PSum.inl (@Inhabited.default _ (inhabitedOfNonempty hp)) +| (isFalse hn) := PSum.inr (λ a, absurd (nonempty.intro a) hn) noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h : nonempty α) : {x : α // (∃ y : α, p y) → p x} := diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index 78944e81b2..a13908760e 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -345,7 +345,7 @@ instance [HasLt α] : HasLe (List α) := ⟨List.le⟩ instance hasDecidableLe [HasLt α] [h : DecidableRel ((<) : α → α → Prop)] : Π l₁ l₂ : List α, Decidable (l₁ ≤ l₂) := -λ a b, not.Decidable +λ a b, Not.Decidable lemma leEqNotGt [HasLt α] : ∀ l₁ l₂ : List α, (l₁ ≤ l₂) = ¬ (l₂ < l₁) := λ l₁ l₂, rfl diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean index 87018cc77c..28f145529c 100644 --- a/library/init/data/nat/basic.lean +++ b/library/init/data/nat/basic.lean @@ -522,7 +522,7 @@ protected theorem bit1NeOne : ∀ {n : Nat}, n ≠ 0 → bit1 n ≠ 1 | (n+1) h h1 := Nat.noConfusion h1 (λ h2, absurd h2 (succNeZero _)) protected theorem bit0NeOne : ∀ n : Nat, bit0 n ≠ 1 -| 0 h := absurd h (ne.symm Nat.oneNeZero) +| 0 h := absurd h (Ne.symm Nat.oneNeZero) | (n+1) h := have h1 : succ (succ (n + n)) = 1, from succAdd n n ▸ h, Nat.noConfusion h1 @@ -535,7 +535,7 @@ protected theorem addSelfNeOne : ∀ (n : Nat), n + n ≠ 1 Nat.noConfusion h1 (λ 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)) +| 0 m h := absurd h (Ne.symm (Nat.addSelfNeOne m)) | (n+1) 0 h := have h1 : succ (bit0 (succ n)) = 0, from h, absurd h1 (Nat.succNeZero _) @@ -547,7 +547,7 @@ protected theorem bit1NeBit0 : ∀ (n m : Nat), bit1 n ≠ bit0 m absurd h2 (bit1NeBit0 n m) protected theorem bit0NeBit1 : ∀ (n m : Nat), bit0 n ≠ bit1 m := -λ n m : Nat, ne.symm (Nat.bit1NeBit0 m n) +λ n m : Nat, Ne.symm (Nat.bit1NeBit0 m n) protected theorem bit0Inj : ∀ {n m : Nat}, bit0 n = bit0 m → n = m | 0 0 h := rfl @@ -574,16 +574,16 @@ protected theorem bit1Ne {n m : Nat} : n ≠ m → bit1 n ≠ bit1 m := λ h₁ h₂, absurd (Nat.bit1Inj h₂) h₁ protected theorem zeroNeBit0 {n : Nat} : n ≠ 0 → 0 ≠ bit0 n := -λ h, ne.symm (Nat.bit0NeZero h) +λ h, Ne.symm (Nat.bit0NeZero h) protected theorem zeroNeBit1 (n : Nat) : 0 ≠ bit1 n := -ne.symm (Nat.bit1NeZero n) +Ne.symm (Nat.bit1NeZero n) protected theorem oneNeBit0 (n : Nat) : 1 ≠ bit0 n := -ne.symm (Nat.bit0NeOne n) +Ne.symm (Nat.bit0NeOne n) protected theorem oneNeBit1 {n : Nat} : n ≠ 0 → 1 ≠ bit1 n := -λ h, ne.symm (Nat.bit1NeOne h) +λ h, Ne.symm (Nat.bit1NeOne h) protected theorem oneLtBit1 : ∀ {n : Nat}, n ≠ 0 → 1 < bit1 n | 0 h := absurd rfl h diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 2e7d55a703..32e036a136 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -485,7 +485,7 @@ void initialize_constants() { g_nat_ble = new name{"Nat", "ble"}; g_ne = new name{"ne"}; g_neq_of_not_iff = new name{"neqOfNotIff"}; - g_not = new name{"not"}; + g_not = new name{"Not"}; g_not_of_iff_false = new name{"notOfIffFalse"}; g_not_of_eq_false = new name{"notOfEqFalse"}; g_of_eq_true = new name{"ofEqTrue"}; diff --git a/src/library/constants.txt b/src/library/constants.txt index 17f4ce2373..9eb81aea87 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -196,7 +196,7 @@ Nat.beq Nat.ble ne neqOfNotIff -not +Not notOfIffFalse notOfEqFalse ofEqTrue