Commit 97dd059a authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Add a few more tactics to documentation

parent ada2f267
......@@ -8,12 +8,27 @@ Each tactic should be named and briefly described (just a few sentences). Please
Tactics taken from the standard library of Viktor Vafeiadis.
- `ins`: combination of `intros`, `simpl` and `eauto`. Some trivial proofs follow from `by ins`.
- `des`: breaks all conjunctions in the local context, applies any simple substitutions via `subst`, and breaks any disjunctions in the local context into separate cases that are to be proved individually as subgoals.
- `desc`: same as `des`, but does not break disjunctions.
- `desf`: Combination of `des` with the evaluation of 'if-then-else' conditions. It performs a case analysis of every 'if-then-else' in the local context
or in the goal. If it becomes slow in large proofs, you can remove unnecessary assumptions (e.g., with `clear - ...`) before applying the tactic.
- `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.
- `specialize (H x1 x2 x3)`: instantiates hypothesis H in place with values x1, x2, 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.
*To be written… please feel free to start.*
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment