doc: docstring review for Std.Do

src/Std/Do/PostCond.lean

@@ -10,6 +10,8 @@ public import Std.Do.SPred
 
 @[expose] public section
 
+set_option linter.missingDocs true
+
 /-!
 # Pre and postconditions
 
@@ -44,51 +46,86 @@ namespace Std.Do
 
 universe u
 
+/--
+The “shape” of the postconditions that are used to reason about a monad.
+
+A postcondition shape is an abstraction of many possible monadic effects, based on the structure of pure functions that can simulate them. The postcondition shape of a monad is given by its `WP` instance. This shape is used to determine both its `Assertion`s and its `PostCond`s.
+-/
 inductive PostShape : Type (u+1) where
+  /-- The assertions and postconditions in this monad use neither state nor exceptions. -/
   | pure : PostShape
+  /--
+  The assertions in this monad may mention the current value of a state of type `σ`, and
+  postconditions may mention the state's final value.
+  -/
   | arg : (σ : Type u) → PostShape → PostShape
+  /--
+  The postconditions in this monad include assertions about exceptional values of type `ε` that
+  result from premature termination.
+  -/
   | except : (ε : Type u) → PostShape → PostShape
 
 variable {ps : PostShape.{u}} {α σ ε : Type u}
 
+/--
+Extracts the list of state types under `PostShape.arg` constructors, discarding exception types.
+
+The state types determine the shape of assertions in the monad.
+-/
 abbrev PostShape.args : PostShape.{u} → List (Type u)
   | .pure => []
   | .arg σ s => σ :: PostShape.args s
   | .except _ s => PostShape.args s
 
 /--
-  An assertion on the `.arg`s in the given predicate shape.
-  ```
-  example : Assertion (.arg ρ .pure) = (ρ → ULift Prop) := rfl
-  example : Assertion (.except ε .pure) = ULift Prop := rfl
-  example : Assertion (.arg σ (.except ε .pure)) = (σ → ULift Prop) := rfl
-  example : Assertion (.except ε (.arg σ .pure)) = (σ → ULift Prop) := rfl
-  ```
-  This is an abbreviation for `SPred` under the hood, so all theorems about `SPred` apply.
+An assertion about the state fields for a monad whose postcondition shape is `ps`.
+
+Concretely, this is an abbreviation for `SPred` applied to the `.arg`s in the given predicate shape, so all theorems about `SPred` apply.
+
+Examples:
+```lean example
+example : Assertion (.arg ρ .pure) = (ρ → ULift Prop) := rfl
+example : Assertion (.except ε .pure) = ULift Prop := rfl
+example : Assertion (.arg σ (.except ε .pure)) = (σ → ULift Prop) := rfl
+example : Assertion (.except ε (.arg σ .pure)) = (σ → ULift Prop) := rfl
+```
 -/
 abbrev Assertion (ps : PostShape.{u}) : Type u :=
   SPred (PostShape.args ps)
 
 /--
-  Encodes one continuation barrel for each `PostShape.except` in the given predicate shape.
-  ```
-  example : ExceptConds (.pure) = Unit := rfl
-  example : ExceptConds (.except ε .pure) = ((ε → ULift Prop) × Unit) := rfl
-  example : ExceptConds (.arg σ (.except ε .pure)) = ((ε → ULift Prop) × Unit) := rfl
-  example : ExceptConds (.except ε (.arg σ .pure)) = ((ε → σ → ULift Prop) × Unit) := rfl
-  ```
+An assertion about each potential exception that's declared in a postcondition shape.
+
+Examples:
+```lean example
+example : ExceptConds (.pure) = Unit := rfl
+example : ExceptConds (.except ε .pure) = ((ε → ULift Prop) × Unit) := rfl
+example : ExceptConds (.arg σ (.except ε .pure)) = ((ε → ULift Prop) × Unit) := rfl
+example : ExceptConds (.except ε (.arg σ .pure)) = ((ε → σ → ULift Prop) × Unit) := rfl
+```
 -/
 def ExceptConds : PostShape.{u} → Type u
   | .pure => PUnit
   | .arg _ ps => ExceptConds ps
   | .except ε ps => (ε → Assertion ps) × ExceptConds ps
 
+/--
+Lifts a proposition `p` to a set of assertions about the possible exceptions in `ps`. Each
+exception's postcondition holds when `p` is true.
+-/
 def ExceptConds.const {ps : PostShape.{u}} (p : Prop) : ExceptConds ps := match ps with
   | .pure => ⟨⟩
   | .arg _ ps => @ExceptConds.const ps p
   | .except _ ps => (fun _ε => spred(⌜p⌝), @ExceptConds.const ps p)
 
+/--
+An assertion about the possible exceptions in `ps` that always holds.
+-/
 def ExceptConds.true : ExceptConds ps := ExceptConds.const True
+
+/--
+An assertion about the possible exceptions in `ps` that never holds.
+-/
 def ExceptConds.false : ExceptConds ps := ExceptConds.const False
 
 @[simp, grind =]
@@ -118,12 +155,20 @@ theorem ExceptConds.snd_false {ps : PostShape.{u}} :
 instance : Inhabited (ExceptConds ps) where
   default := ExceptConds.true
 
+/--
+Entailment of exception assertions is defined as pointwise entailment of the assertions for each
+potential exception.
+
+While implication of exception conditions (`ExceptConds.imp`) is itself an exception condition,
+entailment is an ordinary proposition.
+-/
 def ExceptConds.entails {ps : PostShape.{u}} (x y : ExceptConds ps) : Prop :=
   match ps with
   | .pure => True
   | .arg _ ps => @entails ps x y
   | .except _ ps => (∀ e, x.1 e ⊢ₛ y.1 e) ∧ @entails ps x.2 y.2
 
+@[inherit_doc ExceptConds.entails]
 scoped infixr:25 " ⊢ₑ " => ExceptConds.entails
 
 @[refl, simp]
@@ -146,12 +191,17 @@ theorem ExceptConds.entails_false {x : ExceptConds ps} : ExceptConds.false ⊢
 theorem ExceptConds.entails_true {x : ExceptConds ps} : x ⊢ₑ ExceptConds.true := by
   induction ps <;> simp_all [true, const, entails]
 
+/--
+Conjunction of exception assertions is defined as pointwise conjunction of the assertions for each
+potential exception.
+-/
 def ExceptConds.and {ps : PostShape.{u}} (x : ExceptConds ps) (y : ExceptConds ps) : ExceptConds ps :=
   match ps with
   | .pure => ⟨⟩
   | .arg _ ps => @ExceptConds.and ps x y
   | .except _ _ => (fun e => SPred.and (x.1 e) (y.1 e), ExceptConds.and x.2 y.2)
 
+@[inherit_doc ExceptConds.and]
 infixr:35 " ∧ₑ " => ExceptConds.and
 
 @[simp]
@@ -207,12 +257,20 @@ theorem ExceptConds.and_eq_left {ps : PostShape} {p q : ExceptConds ps} (h : p 
     · ext a; exact (SPred.and_eq_left.mp (h.1 a)).to_eq
     · exact ih h.2
 
+/--
+Implication of exception assertions is defined as pointwise implication of the assertion for each
+exception.
+
+Unlike entailment (`ExceptConds.entails`), which is an ordinary proposition of type `Prop`,
+implication of exception assertions is itself an exception assertion.
+-/
 def ExceptConds.imp {ps : PostShape.{u}} (x : ExceptConds ps) (y : ExceptConds ps) : ExceptConds ps :=
   match ps with
   | .pure => ⟨⟩
   | .arg _ ps => @ExceptConds.imp ps x y
   | .except _ _ => (fun e => SPred.imp (x.1 e) (y.1 e), ExceptConds.imp x.2 y.2)
 
+@[inherit_doc ExceptConds.imp]
 infixr:25 " →ₑ " => ExceptConds.imp
 
 @[simp]
@@ -304,10 +362,21 @@ scoped macro:max ppAllowUngrouped "⇓?" xs:term:max+ " => " e:term : term =>
 instance : Inhabited (PostCond α ps) where
   default := PostCond.noThrow fun _ => default
 
+/--
+Entailment of postconditions.
+
+This consists of:
+ * Entailment of the assertion about the return value, for all possible return values.
+ * Entailment of the exception conditions.
+
+While implication of postconditions (`PostCond.imp`) results in a new postcondition, entailment is
+an ordinary proposition.
+-/
 @[simp]
 def PostCond.entails (p q : PostCond α ps) : Prop :=
   (∀ a, SPred.entails (p.1 a) (q.1 a)) ∧ ExceptConds.entails p.2 q.2
 
+@[inherit_doc PostCond.entails]
 scoped infixr:25 " ⊢ₚ " => PostCond.entails
 
 @[refl, simp]
@@ -325,14 +394,31 @@ theorem PostCond.entails_noThrow (p : α → Assertion ps) (q : PostCond α ps)
 theorem PostCond.entails_mayThrow (p : PostCond α ps) (q : α → Assertion ps) : p ⊢ₚ PostCond.mayThrow q ↔ ∀ a, p.1 a ⊢ₛ q a := by
   simp only [entails, ExceptConds.entails_true, and_true]
 
+/--
+Conjunction of postconditions.
+
+This is defined pointwise, as the conjunction of the assertions about the return value and the
+conjunctions of the assertions about each potential exception.
+-/
 abbrev PostCond.and (p : PostCond α ps) (q : PostCond α ps) : PostCond α ps :=
   (fun a => SPred.and (p.1 a) (q.1 a), ExceptConds.and p.2 q.2)
 
+@[inherit_doc PostCond.and]
 scoped infixr:35 " ∧ₚ " => PostCond.and
 
+/--
+Implication of postconditions.
+
+This is defined pointwise, as the implication of the assertions about the return value and the
+implications of each of the assertions about each potential exception.
+
+While entailment of postconditions (`PostCond.entails`) is an ordinary proposition, implication of
+postconditions is itself a postcondition.
+-/
 abbrev PostCond.imp (p : PostCond α ps) (q : PostCond α ps) : PostCond α ps :=
   (fun a => SPred.imp (p.1 a) (q.1 a), ExceptConds.imp p.2 q.2)
 
+@[inherit_doc PostCond.imp]
 scoped infixr:25 " →ₚ " => PostCond.imp
 
 theorem PostCond.and_imp : P' ∧ₚ (P' →ₚ Q') ⊢ₚ P' ∧ₚ Q' := by

src/Std/Do/PredTrans.lean

@@ -11,6 +11,8 @@ public import Std.Do.PostCond
 
 @[expose] public section
 
+set_option linter.missingDocs true
+
 /-!
 # Predicate transformers for arbitrary postcondition shapes
 
@@ -54,9 +56,9 @@ def PredTrans.Conjunctive.mono (t : PostCond α ps → Assertion ps) (h : PredTr
   exact SPred.and_elim_r
 
 /--
-  The type of predicate transformers for a given `ps : PostShape` and return type `α : Type`.
-  A predicate transformer `x : PredTrans ps α` is a function that takes a postcondition
-  `Q : PostCond α ps` and returns a precondition `x.apply Q : Assertion ps`.
+The type of predicate transformers for a given `ps : PostShape` and return type `α : Type`. A
+predicate transformer `x : PredTrans ps α` is a function that takes a postcondition `Q : PostCond α
+ps` and returns a precondition `x.apply Q : Assertion ps`.
  -/
 @[ext]
 structure PredTrans (ps : PostShape) (α : Type u) : Type u where
@@ -72,16 +74,23 @@ theorem mono (t : PredTrans ps α) : Monotonic t.apply :=
   Conjunctive.mono t.apply t.conjunctive
 
 /--
-  Given a fixed postcondition, the *stronger* predicate transformer will yield a
-  *weaker* precondition.
+Given a fixed postcondition, the *stronger* predicate transformer will yield a *weaker*
+precondition.
 -/
 def le (x y : PredTrans ps α) : Prop :=
   ∀ Q, y.apply Q ⊢ₛ x.apply Q -- the weaker the precondition, the smaller the PredTrans
 instance : LE (PredTrans ps α) := ⟨le⟩
 
+/--
+The identity predicate transformer that transforms the postcondition's assertion about the return
+value into an assertion about `a`.
+-/
 def pure (a : α) : PredTrans ps α :=
   { apply := fun Q => Q.1 a, conjunctive := by intro _ _; simp }
 
+/--
+Sequences two predicate transformers by composing them.
+-/
 def bind (x : PredTrans ps α) (f : α → PredTrans ps β) : PredTrans ps β :=
   { apply := fun Q => x.apply (fun a => (f a).apply Q, Q.2),
     conjunctive := by
@@ -135,7 +144,14 @@ instance instLawfulMonad : LawfulMonad (PredTrans ps) :=
     (pure_bind := by simp +unfoldPartialApp [Bind.bind, bind, Pure.pure, pure])
     (bind_assoc := by simp +unfoldPartialApp [Bind.bind, bind])
 
--- The interpretation of `StateT σ (PredTrans ps) α` into `PredTrans (.arg σ ps) α`.
+/--
+Adds the ability to make assertions about a state of type `σ` to a predicate transformer with
+postcondition shape `ps`, resulting in postcondition shape `.arg σ ps`. This is done by
+interpreting `StateT σ (PredTrans ps) α` into `PredTrans (.arg σ ps) α`.
+
+This can be used to for all kinds of state-like effects, including reader effects or append-only
+states, by interpreting them as states.
+-/
 -- Think: modifyGetM
 def pushArg {σ : Type u} (x : StateT σ (PredTrans ps) α) : PredTrans (.arg σ ps) α where
   apply := fun Q s => (x s).apply (fun (a, s) => Q.1 a s, Q.2)
@@ -146,7 +162,14 @@ def pushArg {σ : Type u} (x : StateT σ (PredTrans ps) α) : PredTrans (.arg σ
     dsimp only [SPred.and_cons, ExceptConds.and]
     rw [← ((x s).conjunctive _ _).to_eq]
 
--- The interpretation of `ExceptT ε (PredTrans ps) α` into `PredTrans (.except ε ps) α`
+/--
+Adds the ability to make assertions about exceptions of type `ε` to a predicate transformer with
+postcondition shape `ps`, resulting in postcondition shape `.except ε ps`. This is done by
+interpreting `ExceptT ε (PredTrans ps) α` into `PredTrans (.except ε ps) α`.
+
+This can be used for all kinds of exception-like effects, such as early termination, by interpreting
+them as exceptions.
+-/
 def pushExcept {ps : PostShape} {α ε} (x : ExceptT ε (PredTrans ps) α) : PredTrans (.except ε ps) α where
   apply Q := x.apply (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2)
   conjunctive := by
@@ -158,6 +181,12 @@ def pushExcept {ps : PostShape} {α ε} (x : ExceptT ε (PredTrans ps) α) : Pre
     ext x
     cases x <;> simp
 
+/--
+Adds the ability to make assertions about early termination to a predicate transformer with
+postcondition shape `ps`, resulting in postcondition shape `.except PUnit ps`. This is done by
+interpreting `OptionT (PredTrans ps) α` into `PredTrans (.except PUnit ps) α`, which models the type
+`Option` as being equivalent to `Except PUnit`.
+-/
 def pushOption {ps : PostShape} {α} (x : OptionT (PredTrans ps) α) : PredTrans (.except PUnit ps) α where
   apply Q := x.apply (fun | .some a => Q.1 a | .none => Q.2.1 ⟨⟩, Q.2.2)
   conjunctive := by
@@ -170,19 +199,19 @@ def pushOption {ps : PostShape} {α} (x : OptionT (PredTrans ps) α) : PredTrans
     cases x <;> simp
 
 @[simp]
-def pushArg_apply {ps} {α σ : Type u} {Q : PostCond α (.arg σ ps)} (f : σ → PredTrans ps (α × σ)) :
+theorem pushArg_apply {ps} {α σ : Type u} {Q : PostCond α (.arg σ ps)} (f : σ → PredTrans ps (α × σ)) :
   (pushArg f).apply Q = fun s => (f s).apply (fun ⟨a, s⟩ => Q.1 a s, Q.2) := rfl
 
 @[simp]
-def pushExcept_apply {ps} {α ε : Type u} {Q : PostCond α (.except ε ps)} (x : PredTrans ps (Except ε α)) :
+theorem pushExcept_apply {ps} {α ε : Type u} {Q : PostCond α (.except ε ps)} (x : PredTrans ps (Except ε α)) :
   (pushExcept x).apply Q = x.apply (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := rfl
 
 @[simp]
-def pushOption_apply {ps} {α : Type u} {Q : PostCond α (.except PUnit ps)} (x : PredTrans ps (Option α)) :
+theorem pushOption_apply {ps} {α : Type u} {Q : PostCond α (.except PUnit ps)} (x : PredTrans ps (Option α)) :
   (pushOption x).apply Q = x.apply (fun | .some a => Q.1 a | .none => Q.2.1 ⟨⟩, Q.2.2) := rfl
 
-def dite_apply {ps} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : c → PredTrans ps α) (e : ¬ c → PredTrans ps α) :
+theorem dite_apply {ps} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : c → PredTrans ps α) (e : ¬ c → PredTrans ps α) :
   (if h : c then t h else e h).apply Q = if h : c then (t h).apply Q else (e h).apply Q := by split <;> rfl
 
-def ite_apply {ps} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : PredTrans ps α) (e : PredTrans ps α) :
+theorem ite_apply {ps} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : PredTrans ps α) (e : PredTrans ps α) :
   (if c then t else e).apply Q = if c then t.apply Q else e.apply Q := by split <;> rfl

src/Std/Do/SPred.lean

@@ -11,3 +11,5 @@ public import Std.Do.SPred.SPred
 public import Std.Do.SPred.Notation
 public import Std.Do.SPred.Laws
 public import Std.Do.SPred.DerivedLaws
+
+set_option linter.missingDocs true