From 227492eaa53f6d868bfe90687249f06de939abe6 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Wed, 9 Sep 2020 20:55:22 +0000 Subject: [PATCH] doc(library/init/*): document some definitions and theorems (#463) A docstring PR adding some docstrings to various mathematically important ideas. --- library/init/algebra/classes.lean | 15 +++++++++++++++ library/init/algebra/order.lean | 2 ++ library/init/core.lean | 8 +++++++- library/init/logic.lean | 6 ++++-- 4 files changed, 28 insertions(+), 3 deletions(-) diff --git a/library/init/algebra/classes.lean b/library/init/algebra/classes.lean index 93e14146b3..378cca49f3 100644 --- a/library/init/algebra/classes.lean +++ b/library/init/algebra/classes.lean @@ -71,34 +71,49 @@ class is_idempotent (α : Type u) (f : α → α) : Prop := (idempotent : ∀ a, f (f a) = f a) -/ +/-- `is_irrefl X r` means the binary relation `r` on `X` is irreflexive (that is, `r x x` never +holds). -/ @[algebra] class is_irrefl (α : Type u) (r : α → α → Prop) : Prop := (irrefl : ∀ a, ¬ r a a) +/-- `is_refl X r` means the binary relation `r` on `X` is reflexive. -/ @[algebra] class is_refl (α : Type u) (r : α → α → Prop) : Prop := (refl : ∀ a, r a a) +/-- `is_symm X r` means the binary relation `r` on `X` is symmetric. -/ @[algebra] class is_symm (α : Type u) (r : α → α → Prop) : Prop := (symm : ∀ a b, r a b → r b a) +/-- The opposite of a symmetric relation is symmetric. -/ instance is_symm_op_of_is_symm (α : Type u) (r : α → α → Prop) [is_symm α r] : is_symm_op α Prop r := {symm_op := λ a b, propext $ iff.intro (is_symm.symm a b) (is_symm.symm b a)} +/-- `is_asymm X r` means that the binary relation `r` on `X` is asymmetric, that is, +`r a b → ¬ r b a`. -/ @[algebra] class is_asymm (α : Type u) (r : α → α → Prop) : Prop := (asymm : ∀ a b, r a b → ¬ r b a) +/-- `is_antisymm X r` means the binary relation `r` on `X` is antisymmetric. -/ @[algebra] class is_antisymm (α : Type u) (r : α → α → Prop) : Prop := (antisymm : ∀ a b, r a b → r b a → a = b) +/-- `is_trans X r` means the binary relation `r` on `X` is transitive. -/ @[algebra] class is_trans (α : Type u) (r : α → α → Prop) : Prop := (trans : ∀ a b c, r a b → r b c → r a c) +/-- `is_total X r` means that the binary relation `r` on `X` is total, that is, that for any +`x y : X` we have `r x y` or `r y x`.-/ @[algebra] class is_total (α : Type u) (r : α → α → Prop) : Prop := (total : ∀ a b, r a b ∨ r b a) +/-- `is_preorder X r` means that the binary relation `r` on `X` is a pre-order, that is, reflexive +and transitive. -/ @[algebra] class is_preorder (α : Type u) (r : α → α → Prop) extends is_refl α r, is_trans α r : Prop. +/-- `is_total_preorder X r` means that the binary relation `r` on `X` is total and a preorder. -/ @[algebra] class is_total_preorder (α : Type u) (r : α → α → Prop) extends is_trans α r, is_total α r : Prop. +/-- Every total pre-order is a pre-order. -/ instance is_total_preorder_is_preorder (α : Type u) (r : α → α → Prop) [s : is_total_preorder α r] : is_preorder α r := {trans := s.trans, refl := λ a, or.elim (@is_total.total _ r _ a a) id id} diff --git a/library/init/algebra/order.lean b/library/init/algebra/order.lean index 3d96241fba..7637130967 100644 --- a/library/init/algebra/order.lean +++ b/library/init/algebra/order.lean @@ -30,9 +30,11 @@ class partial_order (α : Type u) extends preorder α := class linear_order (α : Type u) extends partial_order α := (le_total : ∀ a b : α, a ≤ b ∨ b ≤ a) +/-- The relation `≤` on a preorder is reflexive. -/ @[refl] lemma le_refl [preorder α] : ∀ a : α, a ≤ a := preorder.le_refl +/-- The relation `≤` on a preorder is transitive. -/ @[trans] lemma le_trans [preorder α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c := preorder.le_trans diff --git a/library/init/core.lean b/library/init/core.lean index d976742f6b..6722205484 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -10,7 +10,7 @@ prelude notation `Prop` := Sort 0 notation f ` $ `:1 a:0 := f a -/- Reserving notation. We do this sot that the precedence of all of the operators +/- Reserving notation. We do this so that the precedence of all of the operators can be seen in one place and to prevent core notation being accidentally overloaded later. -/ /- Notation for logical operations and relations -/ @@ -142,6 +142,8 @@ inductive false : Prop inductive empty : Type +/-- `not P`, with notation `¬ P`, is the `Prop` which is true if and only if `P` is false. It is +internally represented as `P → false`. -/ def not (a : Prop) := a → false prefix `¬` := not @@ -183,6 +185,8 @@ structure prod (α : Type u) (β : Type v) := structure pprod (α : Sort u) (β : Sort v) := (fst : α) (snd : β) +/-- `and P Q`, with notation `P ∧ Q`, is the `Prop` which is true precisely when `P` and `Q` are +both true. -/ structure and (a b : Prop) : Prop := intro :: (left : a) (right : b) @@ -246,6 +250,8 @@ inductive psum (α : Sort u) (β : Sort v) | inl (val : α) : psum | inr (val : β) : psum +/-- `or P Q`, with notation `P ∨ Q`, is the proposition which is true if and only if `P` or `Q` is +true. -/ inductive or (a b : Prop) : Prop | inl (h : a) : or | inr (h : b) : or diff --git a/library/init/logic.lean b/library/init/logic.lean index 556e9fd340..32d6957684 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -20,6 +20,7 @@ def flip {α : Sort u} {β : Sort v} {φ : Sort w} (f : α → β → φ) : β def implies (a b : Prop) := a → b +/-- Implication `→` is transitive. If `P → Q` and `Q → R` then `P → R`. -/ @[trans] lemma implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r := assume hp, h₂ (h₁ hp) @@ -32,7 +33,7 @@ false.rec b (h₂ h₁) lemma not.intro {a : Prop} (h : a → false) : ¬ a := h -/-- Modus tollens.-/ +/-- Modus tollens. If an implication is true, then so is its contrapositive. -/ lemma mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a := assume ha : a, h₂ (h₁ ha) /- not -/ @@ -221,7 +222,8 @@ def or.symm := @or.swap def xor (a b : Prop) := (a ∧ ¬ b) ∨ (b ∧ ¬ a) /- iff -/ - +/-- `iff P Q`, with notation `P ↔ Q`, is the proposition asserting that `P` and `Q` are equivalent, +that is, have the same truth value. -/ structure iff (a b : Prop) : Prop := intro :: (mp : a → b) (mpr : b → a)