@@ -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.

@@ -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.