Backward Proof in C*

EN | 中文

In the previous section, we built proofs forward: starting from axioms and known theorems at the leaves, we applied inference rules until we obtained the desired conclusion. This direction is often unintuitive. It is more natural to start from the goal and decompose it into simpler subgoals until each can be proved directly, then assemble the theorem. This is backward, or goal-directed, proof.

Proving on the LCF Architecture introduced this idea through tactics, goalstacks, and validation functions in ML/HOL Light. This section explains its implementation in C*. Since C has no native closures, C* represents the proof tree as an explicit data structure that users can inspect and manipulate. We explain the design using R. Milner’s general goal-seeking theory, then write and compose tactics in C.

Forward vs. Backward: A First Example

A proof system provides a set of inference rules. Each rule constructs a theorem matching its conclusion from theorems matching its premises. C*‘s HOL interface includes the following three rules:

In the rule layout above, forward inference proceeds from the premises above the bar to the conclusion below it: given the premise theorems, apply the rule to obtain the conclusion theorem. Backward inference starts from the goal: find a rule whose conclusion matches the goal, and turn its premises into subgoals. Consider the goal |-? P ==> Q ==> P && Q|-? P ==> Q ==> P && Q (we write |-?|-? for a goal to be proved and |-|- for a theorem already proved).

Forward. A forward proof calls rules in dependency order, producing a sequence of theorems:


[[cst::proof]] {
  // two leaf theorems first, then combine bottom-up in dependency order
  thm p_th   = assume_rule(`P:bool`);        // P |- P
  thm q_th   = assume_rule(`Q:bool`);        // Q |- Q
  thm pq_th  = conj_rule(p_th, q_th);        // P,Q |- P && Q
  thm q_imp  = disch_rule(`Q:bool`, pq_th);  // P |- Q ==> P && Q
  thm result = disch_rule(`P:bool`, q_imp);  // |- P ==> Q ==> P && Q
}


[[cst::proof]] {
  // two leaf theorems first, then combine bottom-up in dependency order
  thm p_th   = assume_rule(`P:bool`);        // P |- P
  thm q_th   = assume_rule(`Q:bool`);        // Q |- Q
  thm pq_th  = conj_rule(p_th, q_th);        // P,Q |- P && Q
  thm q_imp  = disch_rule(`Q:bool`, pq_th);  // P |- Q ==> P && Q
  thm result = disch_rule(`P:bool`, q_imp);  // |- P ==> Q ==> P && Q
}

The derivation’s dependencies determine the call order: conj_ruleconj_rule needs p_thp_th and q_thq_th; the two calls to disch_ruledisch_rule then successively discharge assumptions from the conjunction theorem to produce resultresult.

Backward. A backward proof decomposes the goal according to the conclusion’s shape, constructing a proof tree (also called a goal tree). In the diagram below, the root goal is at the top and its subgoals are below it, so backward decomposition proceeds downward and forward theorem construction proceeds upward:

Blue arrows decompose the goal top-down; green arrows traverse the completed tree bottom-up, calling inference rules to assemble the theorem.

The outermost connective is an implication, matching disch_ruledisch_rule’s conclusion. We therefore move the antecedent into the context and use the consequent as the subgoal. Repeating this step with disch_ruledisch_rule leaves a conjunction, which matches conj_ruleconj_rule and splits into two subgoals. Each can be closed directly by assume_ruleassume_rule, so decomposition stops there.

Once decomposition is complete, we traverse the tree bottom-up. At each node, we call an inference rule to construct a theorem for that node’s goal, until we obtain the desired theorem at the root.

Milner’s Goal-Seeking Theory

Milner’s general goal-seeking theory describes the conditions under which this two-phase process is trustworthy. The theory applies beyond theorem proving and starts from two kinds of objects and a relation between them. Let

be a set of goals, ;
be a set of events, ;
be the achievement relation; means event achieves goal .

Definition 1 (Tactic and validation function). For a set , write for finite lists over and for a partial function. A validation function is a partial function from event lists to events; write for the set of validation functions.
A tactic is a partial function that maps a goal to a subgoal list and a validation function:
When is defined at , write its result as , where is the subgoal list. When each event achieves its corresponding subgoal , the validation function takes the event list and reconstructs a candidate parent event: .

A complete round of goal-directed reasoning has two phases: backward decomposition, then forward validation.

The two directions of a tactic: the goal produces subgoals (blue); the subgoals’ achieving events reconstruct the parent event (green).

Backward construction produces an achievement plan: it identifies the subgoals needed to achieve and records the validation function to use later. Once events achieving the subgoals are available, we invoke to construct the parent event.

An everyday example. Consider a travel plan. The top goal is . A tactic splits it into subgoals and saves a validation function :

where is “Alice is downstairs with her luggage at 7:30” and is “Bob arrives by car at 7:30.” Another tactic splits further, , with = “Bob wakes at 7” and = “the car starts.” So far, we have only specified subgoals and validation functions; none of these events has occurred.

When the forward phase begins, let events achieve . The validation functions run in dependency order:

Here is “Bob drives off and reaches Alice’s building by 7:30” and is “Bob picks Alice up and drives to the airport.” If both tactic applications are valid, then , and hence . The backward phase specifies what remains to be achieved and how the resulting events will be combined. The forward phase combines the events that occur to construct an event achieving the top goal.

Validity

Definition 2 (Valid tactic). Let . The tactic is valid at , written , iff
Here means the validation function is defined on that event list. Validity requires the function to produce a result for every legal list of events achieving the corresponding subgoals, and requires that result to achieve the parent goal.
If this holds at every goal in ‘s domain, is a valid tactic, written .

Why Backward Tactics Need No Extra Trust

In LCF-style theorem proving, an event is a theorem and a goal is a goal sequent. Their achievement relation is:

Definition 3 (When a theorem achieves a goal). A theorem achieves a goal , written , iff and are equal up to -equivalence, and every assumption in has an -equivalent counterpart in .

In a functional metalanguage (ML, Haskell, …), a validation function takes a list of subgoal theorems and combines them into a theorem. The classic tactic type is:


type tactic     = goal -> goal list * validation
type validation = thm list -> thm


type tactic     = goal -> goal list * validation
type validation = thm list -> thm

Each tactic application returns subgoals and a validation closure. Tacticals such as THENTHEN and THENLTHENL combine both the tactics and their validation closures, so nested higher-order functions implicitly represent the entire achievement plan.

This preserves the guarantee of the trusted kernel discussed earlier. A backward proof ultimately calls its validation functions, which can only combine existing theorems through inference rules. An error in decomposition or validation may prevent the construction of a theorem for the parent goal, but it cannot prove a goal that does not hold.

Explicit Goal Trees in C*

Classic tacticals compose validation closures that implicitly represent the proof tree. C has no native closures, so C* represents the tree explicitly as a user-visible data structure called a goal tree:


typedef thm (*valid_fun)(thm_list, gnode);
typedef struct goal_node {
  goal       g;
  thm        solved;
  gnode_list children;
  valid_fun  valid;
  void      *env;
} *gnode;


typedef thm (*valid_fun)(thm_list, gnode);
typedef struct goal_node {
  goal       g;
  thm        solved;
  gnode_list children;
  valid_fun  valid;
  void      *env;
} *gnode;

The correspondence with Milner’s framework is direct:

Milner’s framework	*C goal tree**
goal	`goalgoal`
event	`thmthm`
subgoals	`gnode->childrengnode->children`
validation function	`gnode->validgnode->valid` with `envenv`
achievement relation	the check in `gnode_acceptgnode_accept`
executing the plan	`gnode_provegnode_prove`

Goal trees provide a small primitive interface:

Interface	Role in the achievement plan
`gnode_new_with_ccl(ccl)gnode_new_with_ccl(ccl)`	create an open root goal with conclusion `cclccl`
`gnode_expand(g, subgoals, valid, env)gnode_expand(g, subgoals, valid, env)`	expand `gg` into a subgoal list and install a validation function
`gnode_leaves(root)gnode_leaves(root)`	return the open goals, depth-first and left-to-right
`gnode_accept(g, th)gnode_accept(g, th)`	supply a theorem directly and immediately check that it achieves the goal
`gnode_prove(root)gnode_prove(root)`	run the validation functions of the expanded nodes bottom-up

A node can be in one of three states:

A tactic expands a node into children; once their goals are achieved, the validation function solves the expanded node.

an open leaf has a goal, but no theorem, children, or validation function;
an expanded node holds the children, validation function, and environment the tactic created;
a solved node holds a theorem that achieves the node’s goal.

A tactic that expands the tree: `DISCH_TACDISCH_TAC`

Its logical reduction is:


        Gamma, HP:p ?- q
-------------------------------- DISCH_TAC "HP"
        Gamma ?- p ==> q


        Gamma, HP:p ?- q
-------------------------------- DISCH_TAC "HP"
        Gamma ?- p ==> q

Read bottom-up, this rule adds the implication’s antecedent to the assumptions and uses its consequent as the subgoal:


static thm disch_valid(thm_list ths, gnode gn) {
  term p = ((disch_env *)gn->env)->antecedent;
  return disch_rule(p, ths[0]);
}
gnode DISCH_TAC(gnode gn, const char *label) {
  term p = dest_imp(goal_ccl(gn->g)).tm1;
  term q = dest_imp(goal_ccl(gn->g)).tm2;
  goal child = general_goal_new(append_assumption(gn, label, p), q);
  return gnode_expand(gn, LIST_GOAL(child), disch_valid,
                      make_disch_env(p))[0];
}


static thm disch_valid(thm_list ths, gnode gn) {
  term p = ((disch_env *)gn->env)->antecedent;
  return disch_rule(p, ths[0]);
}
gnode DISCH_TAC(gnode gn, const char *label) {
  term p = dest_imp(goal_ccl(gn->g)).tm1;
  term q = dest_imp(goal_ccl(gn->g)).tm2;
  goal child = general_goal_new(append_assumption(gn, label, p), q);
  return gnode_expand(gn, LIST_GOAL(child), disch_valid,
                      make_disch_env(p))[0];
}

The code performs four steps: extract the implication’s antecedent and consequent; add the antecedent as a labeled assumption of the subgoal; save the antecedent in envenv for the validation function; and use gnode_expandgnode_expand to install the child, validation function, and environment. The backward phase constructs the subgoal for the consequent. The forward phase receives a theorem achieving that subgoal and calls disch_ruledisch_rule to reconstruct the parent’s implication.

`gnode_provegnode_prove` runs the validation functions

The core recursion is:


thm gnode_prove_internal(gnode gn) {
  if (gn->solved != empty_theorem) return gn->solved;
  thm_list child_ths = THM_LIST();
  for (size_t i = 0; i < vector_size(gn->children); ++i)
    vector_add(&child_ths, gnode_prove_internal(gn->children[i]));
  thm result = gn->valid(child_ths, gn);
  gnode_accept(gn, result);
  return result;
}


thm gnode_prove_internal(gnode gn) {
  if (gn->solved != empty_theorem) return gn->solved;
  thm_list child_ths = THM_LIST();
  for (size_t i = 0; i < vector_size(gn->children); ++i)
    vector_add(&child_ths, gnode_prove_internal(gn->children[i]));
  thm result = gn->valid(child_ths, gn);
  gnode_accept(gn, result);
  return result;
}

gnode_provegnode_prove traverses the existing tree, collecting child theorems from left to right and running validation functions bottom-up. It does not search for a proof or apply tactics. An already-solved node immediately returns its theorem. An open leaf or any other unsolved node without a validation function causes failure. Before returning, the outermost call also aligns the bound-variable names with those in the root goal, making the final conclusion identical to the root goal, rather than merely -equivalent.

Using and Writing Tactics

First, pick a tactic by the goal’s shape

Current focus	Common tactics
outer structure of the conclusion	`GEN_TACGEN_TAC`, `EXISTS_TACEXISTS_TAC`, `DISCH_TACDISCH_TAC`, `CONJ_TACCONJ_TAC`, `EQ_TACEQ_TAC`
structure of an ordinary assumption	`ASMP_CONJ_TACASMP_CONJ_TAC`, `ASMP_DISJ_TACASMP_DISJ_TAC`, `ASMP_EXISTS_TACASMP_EXISTS_TAC`
using an existing theorem	`MATCH_MP_TACMATCH_MP_TAC`, `MATCH_ACCEPT_TACMATCH_ACCEPT_TAC`, `ASSUME_TACASSUME_TAC`
cases and induction	`BOOL_CASES_TACBOOL_CASES_TAC`, `CASES_TACCASES_TAC`, `INDUCT_TACINDUCT_TAC`
closing a leaf	`CONV_TACCONV_TAC`, `CONV_WITH_ASMP_TACCONV_WITH_ASMP_TAC`, `RULE_TACRULE_TAC`
moving and matching	`REVERT_TACREVERT_TAC`, `SPEC_TACSPEC_TAC`, `INTRO_TACINTRO_TAC`, `INTROS_TACINTROS_TAC`

As a general guide, an implication calls for introducing its antecedent, a conjunction splits into two subgoals, a universal goal introduces a fresh variable, and an existential goal requires a witness. In each case, the goal’s structure determines the form of the next step.

The following table summarizes conclusion-driven tactics and the rules their validation functions call:

Tactic	Backward reduction	Validation
`GEN_TAC(g,"x")GEN_TAC(g,"x")`	`!u. P u!u. P u` → `P xP x`	`gen_rulegen_rule`
`EXISTS_TAC(g,w)EXISTS_TAC(g,w)`	`?u. P u?u. P u` → `P wP w`	`exists_ruleexists_rule`
`DISCH_TAC(g,"H")DISCH_TAC(g,"H")`	`p ==> qp ==> q` → `H:p ?- qH:p ?- q`	`disch_ruledisch_rule`
`CONJ_TAC(g)CONJ_TAC(g)`	`p && qp && q` → two subgoals `pp`, `qq`	`conj_ruleconj_rule`
`DISJ1_TAC(g)DISJ1_TAC(g)` / `DISJ2_TAC(g)DISJ2_TAC(g)`	`p \|\| qp \|\| q` → `pp` / → `qq`	`disj1_ruledisj1_rule` / `disj2_ruledisj2_rule`
`EQ_TAC(g)EQ_TAC(g)`	`p <=> qp <=> q` → both implications	`undisch_ruleundisch_rule` + `deduct_antisym_rulededuct_antisym_rule`
`MATCH_MP_TAC(g,th)MATCH_MP_TAC(g,th)`	match `thth`’s consequent; instantiated antecedent becomes the subgoal	`mp_rulemp_rule` + instantiation
`CONV_TAC(g,cv)CONV_TAC(g,cv)`	rewrite goal `pp` to `qq` via `p = qp = q`	`sym_rulesym_rule` + `eq_mp_ruleeq_mp_rule`

A recipe for writing a tactic

As with DISCH_TACDISCH_TAC, writing a C* tactic involves four steps:

specify the accepted goal shape and backward transformation, including the number and fixed order of subgoals;
extract from the parent goal the terms or theorems the validation function will need, and save them in envenv;
create the child nodes and use gnode_expandgnode_expand to install the children, validation function, and envenv on the parent;
in the validation function, receive the theorems achieving the subgoals in child order and call only HOL inference rules to reconstruct the parent theorem.

Example 1: a first small goal

We now prove |- P ==> Q ==> P && Q|- P ==> Q ==> P && Q, the same theorem as above, using tactics:


gnode root = gnode_new_with_ccl(
    `(P:bool) ==> (Q:bool) ==> P && Q`);
gnode intro_p = DISCH_TAC(root, "HP");
gnode intro_q = DISCH_TAC(intro_p, "HQ");
gnode_list leaves = CONJ_TAC(intro_q);
ACCEPT_TAC(leaves[0], assume_rule(`P:bool`));
ACCEPT_TAC(leaves[1], assume_rule(`Q:bool`));
thm result = gnode_prove(root);


gnode root = gnode_new_with_ccl(
    `(P:bool) ==> (Q:bool) ==> P && Q`);
gnode intro_p = DISCH_TAC(root, "HP");
gnode intro_q = DISCH_TAC(intro_p, "HQ");
gnode_list leaves = CONJ_TAC(intro_q);
ACCEPT_TAC(leaves[0], assume_rule(`P:bool`));
ACCEPT_TAC(leaves[1], assume_rule(`Q:bool`));
thm result = gnode_prove(root);

Two calls to DISCH_TACDISCH_TAC introduce the antecedents, CONJ_TACCONJ_TAC splits the conjunction, and ACCEPT_TACACCEPT_TAC closes each leaf with a theorem. Finally, gnode_provegnode_prove traverses the tree bottom-up to construct the root theorem.

Example 2: a branching proof

We next prove |- (p && (q || r)) ==> ((p && q) || (p && r))|- (p && (q || r)) ==> ((p && q) || (p && r)):


gnode root = gnode_new_with_ccl(`
  ((p:bool) && (q || r)) ==>
  ((p && q) || (p && r))
`);
gnode body = DISCH_TAC(root, "H");
body = ASMP_CONJ_TAC(body, "H", "HP", "HQR");
gnode_list branches = ASMP_DISJ_TAC(body, "HQR", "HQ", "HR");
gnode left = DISJ1_TAC(branches[0]);
gnode_list lp = CONJ_TAC(left);
ACCEPT_TAC(lp[0], assume_rule(`p:bool`));
ACCEPT_TAC(lp[1], assume_rule(`q:bool`));
gnode right = DISJ2_TAC(branches[1]);
gnode_list rp = CONJ_TAC(right);
ACCEPT_TAC(rp[0], assume_rule(`p:bool`));
ACCEPT_TAC(rp[1], assume_rule(`r:bool`));
thm result = gnode_prove(root);


gnode root = gnode_new_with_ccl(`
  ((p:bool) && (q || r)) ==>
  ((p && q) || (p && r))
`);
gnode body = DISCH_TAC(root, "H");
body = ASMP_CONJ_TAC(body, "H", "HP", "HQR");
gnode_list branches = ASMP_DISJ_TAC(body, "HQR", "HQ", "HR");
gnode left = DISJ1_TAC(branches[0]);
gnode_list lp = CONJ_TAC(left);
ACCEPT_TAC(lp[0], assume_rule(`p:bool`));
ACCEPT_TAC(lp[1], assume_rule(`q:bool`));
gnode right = DISJ2_TAC(branches[1]);
gnode_list rp = CONJ_TAC(right);
ACCEPT_TAC(rp[0], assume_rule(`p:bool`));
ACCEPT_TAC(rp[1], assume_rule(`r:bool`));
thm result = gnode_prove(root);

ASMP_DISJ_TACASMP_DISJ_TAC produces two independent subgoals, one per disjunct:


#0  HP:p, HQ:q |-? (p && q) || (p && r)
#1  HP:p, HR:r |-? (p && q) || (p && r)


#0  HP:p, HQ:q |-? (p && q) || (p && r)
#1  HP:p, HR:r |-? (p && q) || (p && r)

Starting from a fresh root, the three lines that introduce and destructure the assumption can be abbreviated to one step with INTRO_TACINTRO_TAC’s introduction pattern:


gnode root2 = gnode_new_with_ccl(goal_ccl(root->g));
gnode_list branches2 = INTRO_TAC(root2, "HP & (HQ | HR)");


gnode root2 = gnode_new_with_ccl(goal_ccl(root->g));
gnode_list branches2 = INTRO_TAC(root2, "HP & (HQ | HR)");

Example 3: Socratic reasoning

We now prove |- ((!x:A. man(x) ==> mortal(x)) /\ man(Socrates)) ==> mortal(Socrates)|- ((!x:A. man(x) ==> mortal(x)) /\ man(Socrates)) ==> mortal(Socrates):


gnode root = gnode_new_with_ccl(`
  (((!x:A. man(x) ==> mortal(x)) /\ man(Socrates)) ==>
    mortal(Socrates))
`);
gnode body = INTRO_TAC(root, "Hall & Hman")[0];
thm socrates_rule =
    assume_rule(gnode_get_asmps(body, CONST_STRING_LIST("Hall"))[0]);
body = MATCH_MP_TAC(body, socrates_rule);
thm man_socrates =
    assume_rule(gnode_get_asmps(body, CONST_STRING_LIST("Hman"))[0]);
ACCEPT_TAC(body, man_socrates);
thm result = gnode_prove(root);


gnode root = gnode_new_with_ccl(`
  (((!x:A. man(x) ==> mortal(x)) /\ man(Socrates)) ==>
    mortal(Socrates))
`);
gnode body = INTRO_TAC(root, "Hall & Hman")[0];
thm socrates_rule =
    assume_rule(gnode_get_asmps(body, CONST_STRING_LIST("Hall"))[0]);
body = MATCH_MP_TAC(body, socrates_rule);
thm man_socrates =
    assume_rule(gnode_get_asmps(body, CONST_STRING_LIST("Hman"))[0]);
ACCEPT_TAC(body, man_socrates);
thm result = gnode_prove(root);

We retrieve the assumption Hall: !x:A. man(x) ==> mortal(x)Hall: !x:A. man(x) ==> mortal(x). Then MATCH_MP_TACMATCH_MP_TAC matches its consequent against the current goal mortal(Socrates)mortal(Socrates), replacing the goal with the instantiated antecedent man(Socrates)man(Socrates). Finally, ACCEPT_TACACCEPT_TAC closes this goal using the HmanHman assumption.

Example 4: recovering an induction instance from the goal

Define a list type and append:


indtype nlist = new_datatype_definition(
    "nlist = nil"
    "      | cons num nlist");
thm app_def = new_rec_definition(
    nlist.rec,
    `app nil l = l &&
     app (cons h t) l = cons h (app t l)`);


indtype nlist = new_datatype_definition(
    "nlist = nil"
    "      | cons num nlist");
thm app_def = new_rec_definition(
    nlist.rec,
    `app nil l = l &&
     app (cons h t) l = cons h (app t l)`);

and prove |- !l:nlist. app l nil = l|- !l:nlist. app l nil = l.

The forward version of this right-identity proof required the user to construct the base case and induction step, then manually instantiate the induction theorem to the predicate \l. app l nil = l\l. app l nil = l using spec_rulespec_rule and a -reduction. The goal played no part in choosing those arguments. In a backward proof, the goal supplies them:


gnode root = gnode_new_with_ccl(
    `!l:nlist. app l nil = l`);
gnode_list cases =
    CONJ_TAC(MATCH_MP_TAC(root, nlist.ind));
CONV_TAC(cases[0], rewrite_conv(THM_LIST(app_def)));
gnode step = INTROS_TAC(
    cases[1], CONST_STRING_LIST("h", "t", "IH"))[0];
CONV_WITH_ASMP_TAC(step, rewrite_conv, THM_LIST(app_def));
thm result = gnode_prove(root);


gnode root = gnode_new_with_ccl(
    `!l:nlist. app l nil = l`);
gnode_list cases =
    CONJ_TAC(MATCH_MP_TAC(root, nlist.ind));
CONV_TAC(cases[0], rewrite_conv(THM_LIST(app_def)));
gnode step = INTROS_TAC(
    cases[1], CONST_STRING_LIST("h", "t", "IH"))[0];
CONV_WITH_ASMP_TAC(step, rewrite_conv, THM_LIST(app_def));
thm result = gnode_prove(root);

MATCH_MP_TACMATCH_MP_TAC matches the induction theorem’s consequent !l. P(l)!l. P(l) against the current goal, automatically recovering P := \l. app l nil = lP := \l. app l nil = l. Splitting the resulting conjunction gives the open goals:


#0  ?- app nil nil = nil
#1  ?- !h t. app t nil = t ==>
        app (cons h t) nil = cons h t


#0  ?- app nil nil = nil
#1  ?- !h t. app t nil = t ==>
        app (cons h t) nil = cons h t

The base case is closed by rewriting with app_defapp_def. The induction step introduces hh, tt, IHIH and rewrites with app_defapp_def and IHIH. Since the goal determines the output shape of the match, the user does not need to call spec_rulespec_rule.

Summary

Milner’s tactics return subgoals and a validation function: the backward phase constructs an achievement plan, and the forward phase runs the validation functions. Validity is a universal semantic specification over all legal events achieving the subgoals.
A tactic program does not enter the trusted kernel. The final theorem is built by HOL inference rules and accepted at each goal node, so an error in a tactic can cause failure but cannot prove a false goal.
Classic LCF represents the proof tree implicitly through higher-order functions and closures. C*, which lacks closures, represents the same structure explicitly as a goal_nodegoal_node, with a small primitive interface (gnode_new_with_cclgnode_new_with_ccl, gnode_expandgnode_expand, gnode_leavesgnode_leaves, gnode_acceptgnode_accept, gnode_provegnode_prove) and tactics such as DISCH_TACDISCH_TAC that expand it.
Backward proof is directed by the goal: its shape guides tactic selection and can determine instantiations that a forward proof must supply by hand, as shown by applying MATCH_MP_TACMATCH_MP_TAC to an induction theorem.

Backward Proof in C*

Forward vs. Backward: A First Example

Milner’s Goal-Seeking Theory

Validity

Why Backward Tactics Need No Extra Trust

Explicit Goal Trees in C*

A tactic that expands the tree: DISCH_TACDISCH_TAC

gnode_provegnode_prove runs the validation functions

Using and Writing Tactics

First, pick a tactic by the goal’s shape

A recipe for writing a tactic

Example 1: a first small goal

Example 2: a branching proof

Example 3: Socratic reasoning

Example 4: recovering an induction instance from the goal

Summary

A tactic that expands the tree: `DISCH_TACDISCH_TAC`

`gnode_provegnode_prove` runs the validation functions