From 7615c9f92fe5ebb71087bf258b7c4e23e732999d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 21 Mar 2019 17:03:47 +0100 Subject: [PATCH] chore(library/init/core): style review of the first half --- library/init/core.lean | 59 +++++++++++++++---------------- library/init/data/list/basic.lean | 4 +-- library/init/data/nat/basic.lean | 2 +- library/init/function.lean | 8 ++--- 4 files changed, 35 insertions(+), 38 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index 0b02f37f0a..ecb0ae6bac 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -590,11 +590,11 @@ theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rf Later, we define a coercion from `BinTree` into `List`. -/ inductive BinTree (α : Type u) -| Empty {} : BinTree +| empty {} : BinTree | leaf (val : α) : BinTree -| Node (left right : BinTree) : BinTree +| node (left right : BinTree) : BinTree -attribute [elabSimple] BinTree.Node BinTree.leaf +attribute [elabSimple] BinTree.node BinTree.leaf /-- Like `by applyInstance`, but not dependent on the tactic framework. -/ @[reducible] def inferInstance {α : Type u} [i : α] : α := i @@ -721,11 +721,11 @@ theorem trueNeFalse : ¬True = False := neFalseOfSelf trivial end Ne -theorem eqFfOfNeTt : ∀ {b : Bool}, b ≠ true → b = false +theorem eqFalseOfNeTrue : ∀ {b : Bool}, b ≠ true → b = false | true h := False.elim (h rfl) | false h := rfl -theorem eqTtOfNeFf : ∀ {b : Bool}, b ≠ false → b = true +theorem eqTrueOfNeFalse : ∀ {b : Bool}, b ≠ false → b = true | true h := rfl | false h := False.elim (h rfl) @@ -784,13 +784,13 @@ 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 := +theorem And.elim (h₁ : a ∧ b) (h₂ : a → b → c) : c := And.rec h₂ h₁ -theorem and.swap : a ∧ b → b ∧ a := +theorem And.swap : a ∧ b → b ∧ a := assume ⟨ha, hb⟩, ⟨hb, ha⟩ -def and.symm := @and.swap +def And.symm := @And.swap theorem Or.elim (h₁ : a ∨ b) (h₂ : a → c) (h₃ : b → c) : c := Or.rec h₂ h₃ h₁ @@ -809,7 +809,7 @@ Or.elim h Or.inr Or.inl def Or.symm := @Or.swap /- xor -/ -def xor (a b : Prop) := (a ∧ ¬ b) ∨ (b ∧ ¬ a) +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 := @@ -948,7 +948,7 @@ theorem andCongr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∧ b) ↔ (c ∧ d) := Iff.intro (and.imp (Iff.mp h₁) (Iff.mp h₂)) (and.imp (Iff.mpr h₁) (Iff.mpr h₂)) theorem andComm : a ∧ b ↔ b ∧ a := -Iff.intro and.swap and.swap +Iff.intro And.swap And.swap theorem andAssoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) := Iff.intro @@ -971,7 +971,7 @@ theorem falseAnd (a : Prop) : False ∧ a ↔ False := iffFalseIntro And.left theorem notAndSelf (a : Prop) : (¬a ∧ a) ↔ False := -iffFalseIntro (λ h, and.elim h (λ h₁ h₂, absurd h₂ h₁)) +iffFalseIntro (λ h, And.elim h (λ h₁ h₂, absurd h₂ h₁)) theorem andNotSelf (a : Prop) : (a ∧ ¬a) ↔ False := iffFalseIntro (assume ⟨h₁, h₂⟩, absurd h₁ h₂) @@ -1059,12 +1059,9 @@ Iff.intro (λ h, trivial) (λ ha h, False.elim h) theorem trueImpliesIff (α : Prop) : (True → α) ↔ α := Iff.intro (λ h, h trivial) (λ h h', h) -/- exists -/ +/- Exists -/ -@[pattern] -def exists.intro := @Exists.intro - -theorem exists.elim {α : Sort u} {p : α → Prop} {b : Prop} +theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop} (h₁ : ∃ x, p x) (h₂ : ∀ (a : α), p a → b) : b := Exists.rec h₂ h₁ @@ -1073,7 +1070,7 @@ theorem forallCongr {α : Sort u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) Iff.intro (λ p a, Iff.mp (h a) (p a)) (λ q a, Iff.mpr (h a) (q a)) theorem existsImpExists {α : Sort u} {p q : α → Prop} (h : ∀ a, (p a → q a)) (p : ∃ a, p a) : ∃ a, q a := -exists.elim p (λ a hp, ⟨a, h a hp⟩) +Exists.elim p (λ a hp, ⟨a, h a hp⟩) theorem existsCongr {α : Sort u} {p q : α → Prop} (h : ∀ a, (p a ↔ q a)) : (Exists p) ↔ ∃ a, q a := Iff.intro @@ -1090,10 +1087,10 @@ Decidable.casesOn h (λ h₁, false) (λ h₂, true) export Decidable (isTrue isFalse toBool) -theorem toBoolTrueEqTt (h : Decidable True) : @toBool True h = true := +theorem toBoolTrueEqTrue (h : Decidable True) : @toBool True h = true := Decidable.casesOn h (λ h, False.elim (Iff.mp notTrue h)) (λ _, rfl) -theorem toBoolFalseEqFf (h : Decidable False) : @toBool False h = false := +theorem toBoolFalseEqFalse (h : Decidable False) : @toBool False h = false := Decidable.casesOn h (λ h, rfl) (λ h, False.elim h) instance : Decidable True := @@ -1207,7 +1204,7 @@ else if hq : q then isFalse $ λh, hp (h.2 hq) else isTrue $ ⟨λh, absurd h hp, λh, absurd h hq⟩ -instance [Decidable p] [Decidable q] : Decidable (xor p q) := +instance [Decidable p] [Decidable q] : Decidable (Xor p q) := if hp : p then if hq : q then isFalse (λ h, Or.elim h (λ ⟨_, h⟩, h hq : ¬(p ∧ ¬ q)) (λ ⟨_, h⟩, h hp : ¬(q ∧ ¬ p))) else isTrue $ Or.inl ⟨hp, hq⟩ @@ -1367,28 +1364,28 @@ match h₁, h₂ with | (isFalse hC), h₂ := False.elim h₂ /-- Universe lifting operation -/ -structure {r s} Ulift (α : Type s) : Type (max s r) := +structure {r s} ULift (α : Type s) : Type (max s r) := up :: (down : α) -namespace Ulift -/- Bijection between α and Ulift.{v} α -/ -theorem upDown {α : Type u} : ∀ (b : Ulift.{v} α), up (down b) = b +namespace ULift +/- Bijection between α and ULift.{v} α -/ +theorem upDown {α : Type u} : ∀ (b : ULift.{v} α), up (down b) = b | (up a) := rfl theorem downUp {α : Type u} (a : α) : down (up.{v} a) = a := rfl -end Ulift +end ULift /-- Universe lifting operation from Sort to Type -/ -structure Plift (α : Sort u) : Type u := +structure PLift (α : Sort u) : Type u := up :: (down : α) -namespace Plift -/- Bijection between α and Plift α -/ -theorem upDown {α : Sort u} : ∀ (b : Plift α), up (down b) = b +namespace PLift +/- Bijection between α and PLift α -/ +theorem upDown {α : Sort u} : ∀ (b : PLift α), up (down b) = b | (up a) := rfl theorem downUp {α : Sort u} (a : α) : down (up a) = a := rfl -end Plift +end PLift /- pointed types -/ structure PointedType := @@ -2131,7 +2128,7 @@ noncomputable def inhabitedOfNonempty {α : Sort u} (h : nonempty α) : Inhabite noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : Inhabited α := -inhabitedOfNonempty (exists.elim h (λ w hw, ⟨w⟩)) +inhabitedOfNonempty (Exists.elim h (λ w hw, ⟨w⟩)) /- all propositions are Decidable -/ noncomputable def propDecidable (a : Prop) : Decidable a := diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index a13908760e..bf6ce525f1 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -369,9 +369,9 @@ end List namespace BinTree private def toListAux : BinTree α → List α → List α -| Empty as := as +| empty as := as | (leaf a) as := a::as -| (Node l r) as := toListAux l (toListAux r as) +| (node l r) as := toListAux l (toListAux r as) def toList (t : BinTree α) : List α := toListAux t [] diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean index 28f145529c..bfbf1da3e5 100644 --- a/library/init/data/nat/basic.lean +++ b/library/init/data/nat/basic.lean @@ -39,7 +39,7 @@ theorem neOfBeqEqFf : ∀ {n m : Nat}, beq n m = false → n ≠ m @[extern cpp "lean::nat_dec_eq"] protected def decEq (n m : @& Nat) : Decidable (n = m) := if h : beq n m = true then isTrue (eqOfBeqEqTt h) -else isFalse (neOfBeqEqFf (eqFfOfNeTt h)) +else isFalse (neOfBeqEqFf (eqFalseOfNeTrue h)) @[inline] instance : DecidableEq Nat := {decEq := Nat.decEq} diff --git a/library/init/function.lean b/library/init/function.lean index eaac2abf7c..fc91442eee 100644 --- a/library/init/function.lean +++ b/library/init/function.lean @@ -69,8 +69,8 @@ assume a₁ a₂, assume h, hf (hg h) @[reducible] def surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b lemma surjectiveComp {g : β → φ} {f : α → β} (hg : surjective g) (hf : surjective f) : surjective (g ∘ f) := -λ (c : φ), exists.elim (hg c) (λ b hb, exists.elim (hf b) (λ a ha, - exists.intro a (show g (f a) = c, from (Eq.trans (congrArg g ha) hb)))) +λ (c : φ), Exists.elim (hg c) (λ b hb, Exists.elim (hf b) (λ a ha, + Exists.intro a (show g (f a) = c, from (Eq.trans (congrArg g ha) hb)))) def bijective (f : α → β) := injective f ∧ surjective f @@ -95,7 +95,7 @@ have h₃ : g (f a) = g (f b), from congrArg g faeqfb, Eq.trans h₁ (Eq.trans h₃ h₂) lemma injectiveOfHasLeftInverse {f : α → β} : hasLeftInverse f → injective f := -assume h, exists.elim h (λ finv inv, injectiveOfLeftInverse inv) +assume h, Exists.elim h (λ finv inv, injectiveOfLeftInverse inv) lemma rightInverseOfInjectiveOfLeftInverse {f : α → β} {g : β → α} (injf : injective f) (lfg : leftInverse f g) : @@ -110,7 +110,7 @@ lemma surjectiveOfHasRightInverse {f : α → β} : hasRightInverse f → surjec lemma leftInverseOfSurjectiveOfRightInverse {f : α → β} {g : β → α} (surjf : surjective f) (rfg : rightInverse f g) : leftInverse f g := -assume y, exists.elim (surjf y) $ λ x 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,