Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • prepare_MC_PR
  • tutorial
  • classic-prosa protected
  • wip-hunspell
  • fset
  • embed_arr_seq_uniq
  • v0.5 protected
  • v0.4 protected
  • v0.3 protected
  • v0.2 protected
  • v0.1 protected
12 results
Blame Permalink
tactics.md 2.52 KiB

List of Tactics

In effort to make it easier for new users to get started with the Prosa project, the idea is to maintain a list of the tactics used in the project in this file.

Each tactic should be named and briefly described (just a few sentences). Please add links to additional documentation elsewhere (if available).

Tactics from VBase

Tactics taken from the standard library of Viktor Vafeiadis.

  • ins: combination of intros, simpl and eauto. Some trivial proofs follow from by ins.

  • 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_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, 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. It's usually easier to read than move: (f x1 x2 x3) => y.

To be continued… please help out.

Standard Coq Tactics

Generally speaking, in new code, prefer ssreflect tactics over standard Coq tactics whenever possible. While the current code base is a mix of classic Coq tactics and ssreflect tactics, that's only a historical accident not worth emulating.

  • lia: Solves arithmetic goals, including ones with ssreflect's definitions (thanks to the coq-mathcomp-zify dependency).

To be continued… please help out.

PROSA Tactics

  • move_neq_down H: moves inequality H : t1 <= t2 (or H : t1 < t2) from the context into goals as t1 > t2 (or t1 >= t2)
  • move_neq_up H: the reverse operation that moves inequality t1 <= t2 (or t1 < t2) from goals into the context as H : t1 > t2 (or H : t1 >= t2)
  • interval_to_duration t1 t2 k: any interval [t1, t2] can be represented as [t1, t1 + k] for some natural number k. This tactic searches for inequality t1 <= t2 (or t1 < t2) in the context and replaces t2 with t1 + k. Note: k is the name of a newly created natural number.
  • rt_auto: equivalent to auto with basic_rt_facts
  • rt_eauto: equivalent to eauto with basic_rt_facts