Small touchups

Author: sgraf812

.vale/styles/config/ignore/terms.txt

@@ -119,6 +119,7 @@ monad's
 monoid
 monomorphic
 monomorphism
+morphism
 multipattern
 multipatterns
 multiset

Manual/VCGen.lean

@@ -55,12 +55,12 @@ open Std.Do
 
 ## Preconditions and Postconditions
 
-One style in which program specifications can be written is to provide a {deftech}_precondition_, which the program's caller is expected to ensure, and a {deftech}_postcondition_, which the program itself is expected to ensure.
-The program is correct if running it when the precondition holds always results in the postcondition holding.
+One style in which program specifications can be written is to provide a {deftech}_precondition_ $`P`, which the caller of a program `prog` is expected to ensure, and a {deftech}_postcondition_ $`Q`, which the `prog` is expected to ensure.
+The program `prog` satisfies the specification if running it when the precondition $`P` holds always results in the postcondition $`Q` holding.
 
 In general, many different preconditions might suffice for a program to ensure the postcondition.
-After all, new preconditions can be generated by replacing a precondition $`P` with $`P \wedge Q`.
-The {deftech}_weakest precondition_ is a precondition that is implied by all other preconditions.
+After all, new preconditions can be generated by replacing a precondition $`P₁` with $`P₁ \wedge P₂`.
+The {deftech}_weakest precondition_ $`\textbf{wp}⟦\texttt{prog}⟧(Q)` of a program `prog` and postcondition $`Q` is a precondition for which `prog` ensures the postcondition `Q` and is implied by all other such preconditions.
 
 One way to prove something about the result of a program is to find the weakest precondition that guarantees the desired result, and then to show that this weakest precondition is simply true.
 This means that the postcondition holds no matter what.
@@ -83,7 +83,7 @@ def mySum (l : Array Nat) : Nat := Id.run do
 If {name}`mySum` is correct, then it is equal to {name}`Array.sum`.
 In {name}`mySum`, the use of {keywordOf Lean.Parser.Term.do}`do` is an internal implementation detail—the function's signature makes no mention of any monad.
 Thus, the proof first manipulates the goal into a form that is amenable to the use of {tactic}`mvcgen`, using the lemma {name}`Id.of_wp_run_eq`.
-This lemma states that facts about the result of running a computation in the {name}`Id` monad that terminates normally (that is, does not use {ref "early-return"}[early return]) can be proved by showing that the {tech}[weakest precondition] that ensures the desired result is true.
+This lemma states that facts about the result of running a computation in the {name}`Id` monad that terminates normally (`Id` computations never throw exceptions) can be proved by showing that the {tech}[weakest precondition] that ensures the desired result is true.
 Next, the proof uses {tactic}`mvcgen` to replace the formulation in terms of weakest preconditions with a set of {tech}[verification conditions].
 
 While {tactic}`mvcgen` is mostly automatic, it does require an invariant for the loop.
@@ -130,7 +130,7 @@ For example:
 
 * `vc1.step` conveys that this {tech}[VC] proves the inductive step for the loop
 * `vc2.a.pre` is meant to prove that the hypotheses of a goal imply the precondition of a specification (of {name}`forIn`).
-* `vc3.a.post` is meant to prove that the postcondition of a specification (of {name}`forIn`) implies the desired property.
+* `vc3.a.post.success` is meant to prove that the postcondition of a specification (of {name}`forIn`) implies the desired property.
 :::
 
 :::paragraph
@@ -257,13 +257,21 @@ end
 ```
 :::
 
-:::TODO
-Note that the form `mvcgen invariants?` would hint that {name}`Invariant.withEarlyReturn` is a useful way to construct the invariant:
-```
+:::paragraph
+Note that the form `mvcgen invariants?` will suggest an initial invariant using {name}`Invariant.withEarlyReturn`, so there is no need to memorize the exact syntax for specifying invariants:
+```lean
+/--
+info: Try this:
+  [apply] invariants
+  ·
+    Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜l.Nodup ∧ (r = true ↔ l.Nodup)⌝) (onContinue :=
+      fun xs letMuts => ⌜xs.prefix = [] ∧ letMuts = ∅ ∨ xs.suffix = [] ∧ l.Nodup⌝)
+-/
+#guard_msgs (info) in
 example (l : List Int) : nodup l ↔ l.Nodup := by
   generalize h : nodup l = r
   apply Id.of_wp_run_eq h
-  mvcgen invariants?
+  mvcgen invariants? <;> sorry
 ```
 :::
 
@@ -417,7 +425,7 @@ mkFresh
 ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄
 ```
 When working in a state monad, preconditions may be parameterized over the value of the state prior to running the code.
-Here, the universally quantified {name}`Nat` is used to _relate_ the initial state to the final state; the precondition is used to connect it the initial state.
+Here, the universally quantified {name}`Nat` is used to _relate_ the initial state to the final state; the precondition is used to connect it to the initial state.
 Similarly, the postcondition may also accept the final state as a parameter.
 This Hoare triple states: