From 08299eab49eef6b3e1d9bf70e46f092bb6ddea68 Mon Sep 17 00:00:00 2001 From: Cameron Low Date: Fri, 28 Feb 2025 16:07:44 +0000 Subject: [PATCH] Document existing intro patterns --- tactics/intro-patterns.md | 95 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 95 insertions(+) create mode 100644 tactics/intro-patterns.md diff --git a/tactics/intro-patterns.md b/tactics/intro-patterns.md new file mode 100644 index 0000000..48f0eef --- /dev/null +++ b/tactics/intro-patterns.md @@ -0,0 +1,95 @@ +Intro patterns are shorthands, based on Small-Scale Reflection in Coq, that enable quick manipulation of goals resulting from tactic calls. +They can be used after any tactic with the following syntax: `tactic => ip1 ip2 ...` where `ip` is some intro pattern. + +## Introducing Hypotheses + +Given a goal of the form: `a1 => a2 ... => an => c`, we can use the following patterns to introduce assumption `a` as a hypothesis: + +- `name` : Introduce the top assumption as a hypothesis called 'name'. +- `?` : Introduce the top assumption but generate a name for the hypothesis. +- `n?` : Introduce the first `n` assumptions, generating a name for each new hypothesis. +- `*` : Introduce all assumptions, generating a name for each new hypothesis. + +## Clearing Hypotheses + +- `_` : Clear the top assumption. +- `{name1, name2, ...}` : Clear hypotheses with the given names, same as `clear name1 name2 ...`. + +## Substitution + +Given a goal of the form: `x = y => c`, we can use the following patterns to perform substitution on `c` using the top assumption. + +- `->` : Substitute the top assumption from left-to-right in the conclusion. +- `<-` : Substitute the top assumption from right-to-left in the conclusion. +- `->>` : Substitute the top assumption from left-to-right in the conclusion and in all the hypotheses. +- `<<-` : Substitute the top assumption from right-to-left in the conclusion and in all the hypotheses. +- `<*>`, `<*>>` : try to substitute as many assumptions as possible with a preference for left-to-right substitution. +- `<<*>` : try to substitute as many assumptions as possible with a preference for right-to-left substitution. +- `@/op`, `@/(op args)`, `@{x}/(op args)` : Unfold operator `op` in the goal. For more specific unfolding, arguments and/or an occurrence can be provided. +- `@-/op`, `@-/(op args)`, `@-{x}/(op args)` : Refold operator `op` in the goal. Often you'll need to be specific about the arguments to help the matching. + +## Destructuring Assumptions + +For goals of the forms: `forall (x : t), a => c`, `a /\ b => c`, `a \/ b => c`, `(exists (x : t), a) => c`. A common desire is to break-down assumptions into their smaller component parts. + +There are three main variants: +- `[]` : Perform a `case` on the top most assumption. +- `[m#]` : Destruct all conjuncts in a goal using the mode `m` +- `[m#|]` : Destruct all conjuncts and disjuncts in the goal using the mode `m`. This will create new goals for each disjunct encountered. + +The destruction mode has a few options that must be enabled in the following order: +- `!`, `x!` : Apply destruction to all assumptions or the top `x` assumptions. +- `~` : Destruct inductives as if they were disjuncts/conjuncts. +- `/` : Unfold operators to check if they can be destructed. + +If `m` is left empty, the default behaviour is: only destruct the top assumption without destructing inductives or unfolding operators. + +It is also possible to sequence further intro patterns on the generated goals with the following syntax: + +- `[v ip1 ip2 ... ]` : Apply intro patterns `ip1`, `ip2`, ... to the goal generated using the variant `v` (one of ``, `m#`, `m#`). Fails if multiple goals are generated. +- `[v ip11 ip12 ... | ... | ... ]`: Apply intro patterns `ipx1`, `ipx2`, ... to the x'th goal generated using the variant `v` (one of ``, `m#`, `m#`). Fails if an incorrect number of `|` are used. + +## Views + +Often it is desirable to apply existing lemmas to an assumption, or pass arguments to the top assumption. + +- `/lemma` : Apply a lemma in the forwards direction to the top assumption. E.G. If `lemma : P => Q` and the goal is `P => R`, then `/lemma` produces `Q => R`. +- `/(_ args)` : Apply the args to the top assumption. E.G. If the goal is `(forall x, P x) => Q` then `/(_ v)` produces `P v => Q`. + +## Manipulating assumptions + +When chaining intro patterns it is useful to be able to manipulate the assumptions in-between patterns. + +- `^` : Duplicate the top assumption. E.G. If the goal is `P => Q` then `^` produces `P => P => Q`. +- `+` : Temporarily introduce the top assumption but do not give it a name. After a full intro pattern chain has finished, all temporary introductions are reverted. E.G. If the goal is `P => Q => R => S`, then the chain `+ + x` produces `P => Q => S` as a goal and a new hypothesis `x : R`. +- `-` : Revert all temporary introductions. E.G. If the goal is `P => Q => R => S`, then the chain `+ + x - y` produces `Q => S` as a goal and new hypotheses `x : R`, and `y : P`. + +## Simplifying The Goal + +There are a variety of methods for automatically simplifying the goal. + +- `/=` : Simplify the current goal via beta-reduction. +- `/~=` : Same as `/=` but do not simplify `P => Q`, `P <=> Q`, `forall (x : t), P`, and `exists (x : t), P`. + +## Trivial +`//` +`//=` +`//~=` + +## SMT + +`/#` +`//#` - Checks if can be killed by `done` before going to SMT. + +## Crush + +`|>` rewrite as much as possible then +`||>` above + trivial + +same as above but unfold ops +`/>` +`//>` + +## Examples + +todo