Tactic (beluga.Harpoon.Tactic)

module Command = Beluga_syntax.Ext.Harpoon

module Total = Beluga.Total

type t = Theorem.t -> Beluga_syntax.Synint.Comp.proof_state -> unit

Tactics operate on an incomplete proof in a tactic context. They may choose to solve the goal by removing it or add new subgoals, or both.

val solve : ?action_name:string -> Beluga_syntax.Synint.Comp.proof -> t

Solves the subgoal with the given proof.

val intros : string list option -> t

Introduces the arguments to a function type, with the given names, if any.

type intros'_failure =

| DuplicateName of Beluga_syntax.Synint.LF.mctx * Beluga_syntax.Synint.Comp.gctx * Beluga_syntax.Synint.Comp.ctyp_decl
| NothingToIntro

val intros' : 
  Theorem.t ->
  string list option ->
  Beluga_syntax.Syncom.Name.t list ->
  Beluga_syntax.Synint.LF.mctx ->
  Beluga_syntax.Synint.Comp.gctx ->
  Beluga_syntax.Synint.Comp.typ ->
  (intros'_failure,
    Beluga_syntax.Synint.LF.mctx
    * Beluga_syntax.Synint.Comp.gctx
    * Beluga_syntax.Synint.Comp.typ)
    Support.Either.t

Introduces the arguments to a function type, with the given names, if any.

val split : 
  [ `split | `invert | `impossible ] ->
  Beluga_syntax.Synint.Comp.exp ->
  Beluga_syntax.Synint.Comp.typ ->
  Beluga_syntax.Synint.Comp.total_dec list ->
  t

Performs a case analysis on the given synthesizable expression of the given type. The split_kind is used to perform an additional check on the split, regarding the number of branches. In particular, this is used to implement variants of splitting, e.g. inversion and impossible.

val unbox : 
  Beluga_syntax.Synint.Comp.exp ->
  Beluga_syntax.Synint.Comp.typ ->
  Beluga_syntax.Syncom.Name.t ->
  Beluga_syntax.Synint.Comp.unbox_modifier option ->
  t

Performs unboxing of the given synthesizable expression of the given type. The tactic will itself verify that the type is a box-type.

val invoke : 
  Beluga_syntax.Synint.Comp.exp ->
  Beluga_syntax.Synint.Comp.typ ->
  Beluga_syntax.Syncom.Name.t ->
  t

It is verified that the given expression is an application. The result of the invocation is assigned to the variable of the given name, in cG, in case the given boxity is (the default) `boxed. Otherwise, with `unboxed, the name is a new variable declaration in cD.

val suffices : 
  Beluga_syntax.Synint.Comp.exp ->
  Beluga_syntax.Synint.Comp.suffices_typ list ->
  Beluga_syntax.Synint.Comp.typ ->
  t

Solves the current goal with an implication whose conclusion is compatible with the goal type. Subgoals are generated for each premise of the implication.

The user needs to decide upfront what the types of all the premises are, and these given types must unify with the corresponding premise types. Furthermore, this unification must pin down all universally quantified variables, as there is no way to construct them using Harpoon. (Harpoon can only construct computational objects, not LF objects.)

Another restriction is that *all* universally quantified variables must appear at the beginning. That is, the type `tau` must be of the form

tau = Pi X_1:U_1. ... Pi X_n:U_n. tau_1 -> ... -> tau_k -> tau'

(This is most common form of type for a Beluga function.)

Subject to the following requirements:

cD; cG |- i ==> tau
tau' unifies with the current goal type.
each tau_i unifies with the corresponding type in the args list.

After all these unifications, there must be no remaining universally quantified variables. (Such a type would be very strange, so this requirement is quite weak.)

The concrete syntax of this command piggybacks off the syntax of `by` is

by <lemma/ih> i suffices tau_1, ..., tau_k