chore(library): capitalize more Props

library/init/core.lean

@@ -1230,8 +1230,8 @@ match decEq a b with
 theorem Bool.falseNeTrue (h : false = true) : False :=
 Bool.noConfusion h
 
-def isDecEq {α : Sort u} (p : α → α → Bool) : Prop   := ∀ ⦃x y : α⦄, p x y = true → x = y
-def isDecRefl {α : Sort u} (p : α → α → Bool) : Prop := ∀ x, p x x = true
+def IsDecEq {α : Sort u} (p : α → α → Bool) : Prop   := ∀ ⦃x y : α⦄, p x y = true → x = y
+def IsDecRefl {α : Sort u} (p : α → α → Bool) : Prop := ∀ x, p x x = true
 
 instance : DecidableEq Bool :=
 {decEq := λ a b, match a, b with
@@ -1241,7 +1241,7 @@ instance : DecidableEq Bool :=
  | true, true   := isTrue rfl}
 
 @[inline]
-def decidableEqOfBoolPred {α : Sort u} {p : α → α → Bool} (h₁ : isDecEq p) (h₂ : isDecRefl p) : DecidableEq α :=
+def decidableEqOfBoolPred {α : Sort u} {p : α → α → Bool} (h₁ : IsDecEq p) (h₂ : IsDecRefl p) : DecidableEq α :=
 {decEq := λ x y : α,
  if hp : p x y = true then isTrue (h₁ hp)
  else isFalse (assume hxy : x = y, absurd (h₂ y) (@Eq.recOn _ _ (λ z _, ¬p z y = true) _ hxy hp))}
@@ -1546,27 +1546,27 @@ local postfix `⁻¹`:max := inv
 variable g : α → α → α
 local infix + := g
 
-def commutative        := ∀ a b, a * b = b * a
-def associative        := ∀ a b c, (a * b) * c = a * (b * c)
-def leftIdentity      := ∀ a, one * a = a
-def rightIdentity     := ∀ a, a * one = a
-def rightInverse      := ∀ a, a * a⁻¹ = one
-def leftCancelative   := ∀ a b c, a * b = a * c → b = c
-def rightCancelative  := ∀ a b c, a * b = c * b → a = c
-def leftDistributive  := ∀ a b c, a * (b + c) = a * b + a * c
-def rightDistributive := ∀ a b c, (a + b) * c = a * c + 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)
+def Commutative        := ∀ a b, a * b = b * a
+def Associative        := ∀ a b c, (a * b) * c = a * (b * c)
+def LeftIdentity      := ∀ a, one * a = a
+def RightIdentity     := ∀ a, a * one = a
+def RightInverse      := ∀ a, a * a⁻¹ = one
+def LeftCancelative   := ∀ a b c, a * b = a * c → b = c
+def RightCancelative  := ∀ a b c, a * b = c * b → a = c
+def LeftDistributive  := ∀ a b c, a * (b + c) = a * b + a * c
+def RightDistributive := ∀ a b c, (a + b) * c = a * c + 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)
 
 local infix `◾`:50 := Eq.trans
 
-theorem leftComm : commutative f → associative f → leftCommutative f :=
+theorem leftComm : Commutative f → Associative f → LeftCommutative f :=
 assume hcomm hassoc, assume a b c,
   Eq.symm (hassoc a b c)
 ◾ (hcomm a b ▸ rfl : (a*b)*c = (b*a)*c)
 ◾ hassoc b a c
 
-theorem rightComm : commutative f → associative f → rightCommutative f :=
+theorem rightComm : Commutative f → Associative f → RightCommutative f :=
 assume hcomm hassoc, assume a b c,
   hassoc a b c
 ◾ (hcomm b c ▸ rfl : a*(b*c) = a*(c*b))
@@ -2023,20 +2023,20 @@ instance {α : Sort u} {s : Setoid α} [d : ∀ a b : α, Decidable (a ≈ b)] :
 namespace Function
 variables {α : Sort u} {β : α → Sort v}
 
-protected def equiv (f₁ f₂ : Π x : α, β x) : Prop := ∀ x, f₁ x = f₂ x
+protected def Equiv (f₁ f₂ : Π x : α, β x) : Prop := ∀ x, f₁ x = f₂ x
 
-local infix `~` := Function.equiv
+local infix `~` := Function.Equiv
 
-protected theorem equiv.refl (f : Π x : α, β x) : f ~ f := assume x, rfl
+protected theorem Equiv.refl (f : Π x : α, β x) : f ~ f := assume x, rfl
 
-protected theorem equiv.symm {f₁ f₂ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₁ :=
+protected theorem Equiv.symm {f₁ f₂ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₁ :=
 λ h x, Eq.symm (h x)
 
-protected theorem equiv.trans {f₁ f₂ f₃ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ :=
+protected theorem Equiv.trans {f₁ f₂ f₃ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ :=
 λ h₁ h₂ x, Eq.trans (h₁ x) (h₂ x)
 
-protected theorem equiv.isEquivalence (α : Sort u) (β : α → Sort v) : Equivalence (@Function.equiv α β) :=
-mkEquivalence (@Function.equiv α β) (@equiv.refl α β) (@equiv.symm α β) (@equiv.trans α β)
+protected theorem Equiv.isEquivalence (α : Sort u) (β : α → Sort v) : Equivalence (@Function.Equiv α β) :=
+mkEquivalence (@Function.Equiv α β) (@Equiv.refl α β) (@Equiv.symm α β) (@Equiv.trans α β)
 end Function
 
 section
@@ -2045,7 +2045,7 @@ variables {α : Sort u} {β : α → Sort v}
 
 @[instance]
 private def funSetoid (α : Sort u) (β : α → Sort v) : Setoid (Π x : α, β x) :=
-Setoid.mk (@Function.equiv α β) (Function.equiv.isEquivalence α β)
+Setoid.mk (@Function.Equiv α β) (Function.Equiv.isEquivalence α β)
 
 private def extfun (α : Sort u) (β : α → Sort v) : Sort (imax u v) :=
 Quotient (funSetoid α β)
@@ -2063,7 +2063,7 @@ show extfunApp ⟦f₁⟧ = extfunApp ⟦f₂⟧, from
 congrArg extfunApp (sound h)
 end
 
-local infix `~` := Function.equiv
+local infix `~` := Function.Equiv
 
 instance Pi.Subsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (Π a, β a) :=
 ⟨λ f₁ f₂, funext (λ a, Subsingleton.elim (f₁ a) (f₂ a))⟩

library/init/function.lean

@@ -61,66 +61,66 @@ lemma comp.rightId (f : α → β) : f ∘ id = f := rfl
 
 lemma compConstRight (f : β → φ) (b : β) : f ∘ (const α b) = const α (f b) := rfl
 
-@[reducible] def injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
+@[reducible] def Injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
 
-lemma injectiveComp {g : β → φ} {f : α → β} (hg : injective g) (hf : injective f) : injective (g ∘ f) :=
+lemma injectiveComp {g : β → φ} {f : α → β} (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) :=
 assume a₁ a₂, assume h, hf (hg h)
 
-@[reducible] def surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b
+@[reducible] def Surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b
 
-lemma surjectiveComp {g : β → φ} {f : α → β} (hg : surjective g) (hf : surjective f) : surjective (g ∘ f) :=
+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))))
 
-def bijective (f : α → β) := injective f ∧ surjective f
+def Bijective (f : α → β) := Injective f ∧ Surjective f
 
-lemma bijectiveComp {g : β → φ} {f : α → β} : bijective g → bijective f → bijective (g ∘ f)
+lemma bijectiveComp {g : β → φ} {f : α → β} : Bijective g → Bijective f → Bijective (g ∘ f)
 | ⟨hGinj, hGsurj⟩ ⟨hFinj, hFsurj⟩ := ⟨injectiveComp hGinj hFinj, surjectiveComp hGsurj hFsurj⟩
 
 -- g is a left inverse to f
-def leftInverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x
+def LeftInverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x
 
-def hasLeftInverse (f : α → β) : Prop := ∃ finv : β → α, leftInverse finv f
+def hasLeftInverse (f : α → β) : Prop := ∃ finv : β → α, LeftInverse finv f
 
 -- g is a right inverse to f
-def rightInverse (g : β → α) (f : α → β) : Prop := leftInverse f g
+def RightInverse (g : β → α) (f : α → β) : Prop := LeftInverse f g
 
-def hasRightInverse (f : α → β) : Prop := ∃ finv : β → α, rightInverse finv f
+def hasRightInverse (f : α → β) : Prop := ∃ finv : β → α, RightInverse finv f
 
-lemma injectiveOfLeftInverse {g : β → α} {f : α → β} : leftInverse g f → injective f :=
+lemma injectiveOfLeftInverse {g : β → α} {f : α → β} : LeftInverse g f → Injective f :=
 assume h, assume a b, assume faeqfb,
 have h₁ : a = g (f a),       from Eq.symm (h a),
 have h₂ : g (f b) = b,       from h b,
 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 :=
+lemma injectiveOfHasLeftInverse {f : α → β} : hasLeftInverse f → Injective f :=
 assume h, Exists.elim h (λ finv inv, injectiveOfLeftInverse inv)
 
 lemma rightInverseOfInjectiveOfLeftInverse {f : α → β} {g : β → α}
-    (injf : injective f) (lfg : leftInverse f g) :
-  rightInverse f g :=
+    (injf : Injective f) (lfg : LeftInverse f g) :
+  RightInverse f g :=
 assume x,
 have h : f (g (f x)) = f x, from lfg (f x),
 injf h
 
-lemma surjectiveOfHasRightInverse {f : α → β} : hasRightInverse f → surjective f
+lemma surjectiveOfHasRightInverse {f : α → β} : hasRightInverse f → Surjective f
 | ⟨finv, inv⟩ b := ⟨finv b, inv b⟩
 
 lemma leftInverseOfSurjectiveOfRightInverse {f : α → β} {g : β → α}
-    (surjf : surjective f) (rfg : rightInverse f g) :
-  leftInverse f g :=
+    (surjf : Surjective f) (rfg : RightInverse f g) :
+  LeftInverse f g :=
 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,
   Eq.trans h₁ $ Eq.trans h₂ h₃
 
-lemma injectiveId : injective (@id α) := assume a₁ a₂ h, h
+lemma injectiveId : Injective (@id α) := assume a₁ a₂ h, h
 
-lemma surjectiveId : surjective (@id α) := assume a, ⟨a, rfl⟩
+lemma surjectiveId : Surjective (@id α) := assume a, ⟨a, rfl⟩
 
-lemma bijectiveId : bijective (@id α) := ⟨injectiveId, surjectiveId⟩
+lemma bijectiveId : Bijective (@id α) := ⟨injectiveId, surjectiveId⟩
 
 end Function
 
@@ -139,10 +139,10 @@ rfl
 lemma uncurryCurry (f : α × β → φ) : uncurry (curry f) = f :=
 funext (λ ⟨a, b⟩, rfl)
 
-def idOfLeftInverse {g : β → α} {f : α → β} : leftInverse g f → g ∘ f = id :=
+def idOfLeftInverse {g : β → α} {f : α → β} : LeftInverse g f → g ∘ f = id :=
 assume h, funext h
 
-def idOfRightInverse {g : β → α} {f : α → β} : rightInverse g f → f ∘ g = id :=
+def idOfRightInverse {g : β → α} {f : α → β} : RightInverse g f → f ∘ g = id :=
 assume h, funext h
 
 end Function

script/find_uppers.py

@@ -3,7 +3,7 @@ import regex as re
 import os
 import sys
 
-upper = re.compile(r"^\s*(?:namespace|class|structure|inductive) ((?!inductive)[\w.]+)|(?:def|constant) ([\w.]+).*: Type$", re.MULTILINE)
+upper = re.compile(r"^\s*(?:namespace|class|structure|inductive) ((?!inductive)[\w.]+)|(?:def|constant) ([\w.]+).*(: (Type|Prop)$|:= ∀)", re.MULTILINE)
 fpath = sys.argv[1]
 with open(fpath) as f:
     s = f.read()