Backward Proof in C*

EN | 中文

In the previous section we built proofs forward: start from the leaves — axioms and known theorems — and apply inference rules until the goal falls out. That direction is often unintuitive. People would rather start from the goal they want and decompose it into simpler subgoals, until each subgoal is trivial; only then do they assemble the actual theorem. This is backward, or goal-directed, proof.

Proving on the LCF Architecture already introduced the idea — the tactic, the goalstack, the validation function — in ML/HOL Light terms. This section shows C*‘s concrete realization: because C has no closures to hide a proof tree inside, C* makes the tree an explicit data structure you can see and manipulate. We ground the whole design in R. Milner’s general goal-seeking theory, and end by writing and composing tactics in C.

Forward vs. Backward: A First Example

A proof system gives a set of inference rules; each says that once the theorems matching its premises are in hand, one may construct the theorem matching its conclusion. C*‘s HOL interface includes, among others, these three:

Forward inference runs down the bar: given the premise theorems, apply the rule to get the conclusion theorem. Backward inference instead starts from the goal: find a rule whose conclusion matches the goal, and turn that rule’s premises into new goals. Take the goal |-? P ==> Q ==> P && Q|-? P ==> Q ==> P && Q (we write |-?|-? for a goal still 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 call order is forced by the derivation’s dependencies: conj_ruleconj_rule must wait for p_thp_th and q_thq_th; each disch_ruledisch_rule must wait for the conjunction; only then does resultresult appear.

Backward. A backward proof starts from the conclusion’s shape and decomposes it, growing a proof tree (also called a goal tree):

Blue arrows decompose the goal top-down; green arrows run back up the finished tree, calling inference rules to assemble the theorem.

The outermost connective is an implication, matching disch_ruledisch_rule’s conclusion, so the subgoal moves the antecedent into the context and keeps the consequent as the new goal; a second disch_ruledisch_rule does the same again; the conjunction then matches conj_ruleconj_rule and splits into two subgoals, each closed directly by assume_ruleassume_rule. Decomposition stops there.

Once the decomposition is complete, we walk the tree bottom-up, calling an inference rule at each node to build the theorem for that node’s goal, until the root’s theorem — the one we wanted — is produced.

Milner’s Goal-Seeking Theory

To say when this two-phase process is trustworthy, Milner gave a general goal-seeking theory that is not specific to theorem proving. It starts from two kinds of object 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 all of them.
A tactic is a partial function from a goal to a “subgoal list together with a validation function”:
When is defined at , write its result as , where is the subgoal list. When events each achieve , the validation function takes the event list and reconstructs a candidate parent event: .

A full round of goal-directed reasoning thus 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 only draws up an achievement plan: it answers “to achieve , which goals must I achieve first?” and records the validation function to use later. Only when the subgoals’ events actually arrive is invoked, forward-constructing the parent event.

A everyday example. Instantiate the objects with a travel plan. The top goal is . A tactic splits it 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 there are only subgoals and validation functions — nothing has happened yet.

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 fixes what still must be achieved and how to combine it later; the forward phase uses the events that actually occur to build, layer by layer, 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. So validity requires not only that the result achieve the parent goal, but that any legal list of subgoal-achieving events actually makes the validation function produce a result.
If this holds at every goal in ‘s domain, is a valid tactic, written .

Why Backward Tactics Need No Extra Trust

For LCF-style theorem proving, the abstract objects become concrete: 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 is just a higher-order function taking a list of theorems and returning a theorem, so the classic tactic type reads:


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 not only subgoals but a validation closure; tacticals such as THENTHEN and THENLTHENL combine tactics and their validation closures at once, so the whole achievement plan sits implicitly inside nested higher-order functions.

The payoff is the previous chapter’s point about the trusted kernel. Since a backward proof ultimately calls its validation functions, and a validation function can only combine existing theorems with inference rules, a buggy decomposition or validation may fail to construct a theorem for the parent goal — but it can never prove a goal that does not hold.

Explicit Goal Trees in C*

Classic tacticals combine several validation closures, and the proof tree is hidden inside their nesting. C has no native closures, so C* represents the tree directly, 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`

The primitive interface over goal trees is small:

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 it achieves the goal
`gnode_prove(root)gnode_prove(root)`	run the validation functions of the expanded nodes bottom-up

Each node passes through three states:

A tactic expands a node’s children; once the children are achieved, the validation function closes 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, it lifts the antecedent of an implicative conclusion into the assumptions and keeps the 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 does four things in order: split out the implication’s antecedent and consequent; add the antecedent as a labeled assumption of the subgoal; save, in envenv, the antecedent the validation function will later need; and finally use gnode_expandgnode_expand to install the child, the validation function, and the environment. The backward phase only builds the consequent subgoal; the forward phase receives its achieving theorem 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 does not search for a proof and does not apply tactics for you. It only walks the already-built tree, collecting child theorems left to right and running the validation functions bottom-up. If it meets an open leaf or a node with no validation function, it must fail. The outermost call also aligns the root goal’s bound-variable names before returning, so the final conclusion is not merely -equivalent to the root goal you wrote but identical to it.

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`

Roughly, an implicative goal calls for introducing its antecedent, a conjunctive goal splits in two, a universal goal introduces a fresh variable, and an existential goal asks for a witness. Every step has a definite output shape, which is exactly what makes backward reasoning feel directed.

A condensed view of the conclusion-driven tactics and the rules their validations 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 DISCH_TACDISCH_TAC showed, a new C* tactic follows four steps:

spell out the accepted goal shape and the 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 achieving theorems in child order and call only HOL inference rules to rebuild the parent theorem.

Example 1: a first small goal

Proving |- P ==> Q ==> P && Q|- P ==> Q ==> P && Q — the same theorem as above, now built by 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 DISCH_TACDISCH_TACs introduce the antecedents, CONJ_TACCONJ_TAC splits the conjunction, ACCEPT_TACACCEPT_TAC closes each leaf with a theorem, and gnode_provegnode_prove runs the tree back up to the root theorem.

Example 2: a branching proof

Proving |- (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

Proving |- ((!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 take the assumption Hall: !x:A. man(x) ==> mortal(x)Hall: !x:A. man(x) ==> mortal(x), then let MATCH_MP_TACMATCH_MP_TAC match its consequent against the current goal mortal(Socrates)mortal(Socrates) and turn the goal into the instantiated antecedent man(Socrates)man(Socrates), which ACCEPT_TACACCEPT_TAC closes with 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 had the user build the base case and the step, then instantiate the induction theorem by hand to the predicate \l. app l nil = l\l. app l nil = l with spec_rulespec_rule and a -reduction; the goal played no part in choosing those arguments. Backward, 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 step introduces hh, tt, IHIH and rewrites with app_defapp_def and IHIH. Because the goal fixed the output shape of the match, the user never writes spec_rulespec_rule.

Summary

Milner’s tactics return both subgoals and a validation function: the backward phase draws up an achievement plan, the forward phase runs the validation functions. Validity is a universal semantic specification over all legal subgoal-achieving events.
A tactic program does not enter the trusted kernel; the final theorem is still built by HOL inference rules and accepted at each goal node — so a buggy tactic can fail, but never prove a false goal.
Classic LCF hides the proof tree inside higher-order functions and closures; C*, lacking closures, makes the same structure explicit 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: the goal’s shape picks the tactic and even recovers instantiations (as in MATCH_MP_TACMATCH_MP_TAC against an induction theorem) that a forward proof must supply by hand.

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