Minor documentation changes about tactics.

README.md

@@ -6,7 +6,7 @@ This repository contains the main Coq specification & proof development of the [
 
 ## Documentation
 
-Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homeage:
+Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homepage:
 
 - <https://prosa.mpi-sws.org/branches>
 

doc/guidelines.md

@@ -31,7 +31,7 @@ This project targets Coq *non*-experts. Accordingly, great emphasis is placed on
 ```
 - When commenting, be careful not to leave any misspelled words: Prosa's CI system comprises a spell-checker that will signal errors.
 - When comments have to contain variable names or mathematical notation, use square brackets (e.g. `[job_cost j]`). You can nest square brackets _only if they are balanced_: `[[t1,t2)]` will not work. In this case, use `<<[t1,t2)>>`.
-- The vocabulary of the spell-checker is extended with the words contained in `scripts/wordlist.pws`. Add new words only if strictly necessary.
+- The vocabulary of the spell-checker is extended with the words contained in [`scripts/wordlist.pws`](../scripts/wordlist.pws). Add new words only if strictly necessary.
 - Document the sources of lemmas and theorems in the comments. For example, say something like "Theorem XXX in (Foo & Bar, 2007)", and document at the beginning of the file what "(Foo & Bar, 2007)" refers to.
 
 

doc/tactics.md

@@ -19,19 +19,19 @@ Tactics taken from the standard library of Viktor Vafeiadis.
 
 - `desf_asm`: same as `desf`, but only applied to the assumptions in the local context.
 
-- `exploit H`: When applied to a hypothesis/lemma H, converts pre-conditions into goals in order to infer the post-condition of H, which is then added to the local context.
+- `exploit H`: When applied to a hypothesis/lemma `H`, converts pre-conditions into goals in order to infer the post-condition of `H`, which is then added to the local context.
 
-- `feed H`: Same as exploit, but only generates a goal for the first pre-condition. That is, applying exploit to (H: P1 -> P2 -> P3) produces (H: P2 -> P3) and converts P1 into a goal. This is useful for cleaning up induction hypotheses.
+- `feed H`: Same as exploit, but only generates a goal for the first pre-condition. That is, applying exploit to `H: P1 -> P2 -> P3` produces `H: P2 -> P3` and converts `P1` into a goal. This is useful for cleaning up induction hypotheses.
 
-- `feed_n k H`: Same as feed, but generates goals up to the k-th pre-condition.
+- `feed_n k H`: Same as feed, but generates goals up to the `k`-th pre-condition.
 
-- `specialize (H x1 x2 x3)`: instantiates hypothesis H in place with values x1, x2, x3.
+- `specialize (H x1 x2 x3)`: instantiates hypothesis `H` in place with values `x1`, `x2`, and `x3`.
 
 *To be continued… please help out.*
 
 ## Tactics from `ssreflect`
 
-- `have y := f x1 x2 x3`: Creates an alias to (f x1 x2 x3) called y (in the local context). Note that f can be a function or a proposition/lemma.
+- `have y := f x1 x2 x3`: Creates an alias to `f x1 x2 x3` called `y` (in the local context). Note that `f` can be a function or a proposition/lemma. It's usually easier to read than `move: (f x1 x2 x3) => y`.
 
 *To be written… please feel free to start.*
 
@@ -40,3 +40,7 @@ Tactics taken from the standard library of Viktor Vafeiadis.
 
 *To be written… please feel free to start.*
 
+## Miscellaneous
+
+- `ssrlia`: Solves arithmetic goals, including ones with `ssreflect`'s definitions.
+

util/ssrlia.v

@@ -24,6 +24,10 @@ Ltac arith_goal_ssrnat2coqnat :=
     | |- is_true (_ < _) => try apply/ltP
   end.
 
+(** Solve arithmetic goals.
+  This tactic first rewrites the context to replace operations from ssreflect
+  to the corresponding operations in the Coq library, then calls [lia]. *)
+
 Ltac ssrlia :=
   repeat arith_hypo_ssrnat2coqnat;
   arith_goal_ssrnat2coqnat; simpl;