From bdf0340404170809b25516177ab764f3d6b15f41 Mon Sep 17 00:00:00 2001
From: Martin Bodin <martin.bodin@inria.fr>
Date: Tue, 17 Nov 2020 16:41:59 +0100
Subject: [PATCH] Minor documentation changes about tactics.
---
README.md | 2 +-
doc/tactics.md | 14 +++++++++-----
util/ssrlia.v | 4 ++++
3 files changed, 14 insertions(+), 6 deletions(-)
diff --git a/README.md b/README.md
index 13f11fee4..e85a1cdac 100644
--- a/README.md
+++ b/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>
diff --git a/doc/tactics.md b/doc/tactics.md
index 56a6638db..3c46e4481 100644
--- a/doc/tactics.md
+++ b/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.
+
diff --git a/util/ssrlia.v b/util/ssrlia.v
index e24e726fc..469fed3d8 100644
--- a/util/ssrlia.v
+++ b/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 ssreflect's operations
+ to the corresponding operations in the Coq library, then calls [lia]. *)
+
Ltac ssrlia :=
repeat arith_hypo_ssrnat2coqnat;
arith_goal_ssrnat2coqnat; simpl;
--
GitLab