Commits (2)
......@@ -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>
......
......@@ -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.
......@@ -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;
......