Skip to content

Commit

Permalink
doc(library/init/*): document some definitions and theorems (#463)
Browse files Browse the repository at this point in the history
A docstring PR adding some docstrings to various mathematically important ideas.
  • Loading branch information
kbuzzard committed Sep 9, 2020
1 parent 1604446 commit 227492e
Show file tree
Hide file tree
Showing 4 changed files with 28 additions and 3 deletions.
15 changes: 15 additions & 0 deletions library/init/algebra/classes.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down
2 changes: 2 additions & 0 deletions library/init/algebra/order.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
8 changes: 7 additions & 1 deletion library/init/core.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 -/
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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)

Expand Down Expand Up @@ -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
Expand Down
6 changes: 4 additions & 2 deletions library/init/logic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand All @@ -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 -/
Expand Down Expand Up @@ -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)

Expand Down

0 comments on commit 227492e

Please sign in to comment.