Skip to content

Latest commit

 

History

History
51 lines (39 loc) · 2.26 KB

Tactics.md

File metadata and controls

51 lines (39 loc) · 2.26 KB
Raw

Brief documentation of the tactics in the Hahn library

Tactics to solve a goal

  • done solves trivial goals (adapted from SSReflect).
  • edone solves trivial goals with eassumption or done.
  • by tac is a shorthand for tac; done.
  • eby tac is a shorthand for tac; edone.
  • vauto tries to solve the goal by up to two nested econstructor calls.
  • basic_solver solves simple goals containing relational operators.

Generic simplification tactics

  • simpls is shorthand for simpl in *; try done.
  • ins is shorthand for intros; simpls.
  • clarify simplifies the goal by simple injections/rewrites.
  • clarsimp is similar, but also does a few further rewrites.
  • clarassoc does further rewrites with associativity lemmas.
  • desc destructs conjunctions and existentials in hypotheses.
  • des also destructs disjunctions.
  • desf also performs case splits on conditionals/matches.
  • des_eqrefl simplifies weird-looking dependent matches generated by Program.

Specialized simplification tactics

  • clarify_not simplifies negated hypotheses.
  • in_simp simplifies In x list assumptions.
  • rels simplifies goals with relational operators.
  • relsf also does case splits.

Forward reasoning

  • tertium_non_datur X [as Pattern] does a case split on X \/ ~X.
  • forward eapply H [with ...] as Name generates subgoals for all the premises of H; the final subgoal names the conclusion of H as Name.
  • exploit H is similar to forward eapply H (adapted from CompCert, deprecated).

Backward reasoning

  • splits repeatedly applies split to conjunctions.
  • hahn_frame/hahn_frame_l/hahn_frame_r try to apply the frame rule on goals with relational operators.

Rewriting support for relations

  • hahn_rewrite H rewrites with a relational inclusion/equivalence lemma
  • seq_rewrite H rewrites with an equivalence lemma up to associativity of seq
  • sin_rewrite H rewrites with an inclusion lemma up to associativity of seq
  • arewrite EQ generates a subgoal to prove EQ and seq/sin-rewrites with EQ
  • arewrite_false term is shorthand for arewrite (term ≡ ∅₂)
  • arewrite_id term is shorthand for arewrite (term ⊆ ⦗fun _ => True⦘)
  • case_union x y case splits on relations of the form _ ⨾ (x ∪ y) ⨾ _