Tactics

Christine.Tactics implements a minimal Coq-style tactical proof engine in Elixir. Every tactic is a pure function on the proof state structure. It either returns new state or error reason with state. The engine builds the final CIC proof term via explicit reconstructor closures — no evars, no unification variables, no backtracking.

defmodule Christine.Tactics.ProofState do
  defstruct [
    :name,          # theorem name (String)
    :target,        # original goal type
    :env,           # typechecker environment
    :goals,         # list({context, goal_type})
    :proof_term,    # completed term when goals == []
    :reconstructor  # fn([subproofs]) -> term
  ]
end

The reconstructor is updated by every tactic to wrap the sub-proof into the correct constructor.

Use bullets (-, +, *) to organize sub-goals within recursive proofs or case analysis. In the current Christine prototype, these are purely decorative but encouraged for parity with standard Coq proof scripts.

Theorem beq_nat_refl : ∀ n : nat, beq_nat n n = true.
Proof.
  induction n.
  - reflexivity.
  - simpl. rewrite IHn. reflexivity.
Qed.

Tactic intro x works only when the current goal normalizes to a Pi type ∀ x : A, B. It adds the binding x : A to the context, replaces the goal with B, and updates the reconstructor to wrap the sub-proof in Lam x A body.

Theorem plus_O_n : ∀ n : Nat, plus O n = n.
Proof.
  intro n.
  reflexivity.
Qed.

Tactic intros x y z repeats intro for each name. It chains the reconstructor updates so the final term has nested Lam binders.

Theorem app_nil : ∀ A (l : List A), app l nil = l.
Proof.
  intros A l.
  induction l.
  - simpl. reflexivity.
  - simpl. rewrite IHl_0. reflexivity.
Qed.

Tactic exact t parses the expression t in the current context, infers its type, and checks that it equals the goal (or is Any). If successful, it closes the goal and updates the reconstructor to insert the term directly.

Theorem plus_O_n : ∀ n : Nat, plus O n = n.
Proof.
  intro n.
  exact (Refl Nat n).
Qed.

Tactic simpl replaces the current goal with its βι-normal form using Typechecker.normalize. It does not change the proof term — only the goal presentation.

Theorem plus_O_n : ∀ n : Nat, plus O n = n.
Proof.
  intro n.
  simpl.
  reflexivity.
Qed.

Tactic reflexivity normalizes the goal. If it is an equality a = a, it closes the goal with Refl and updates the reconstructor accordingly. The equality check uses syntactic Typechecker.equal? after normalization.

Theorem plus_O_n : ∀ n : Nat, plus O n = n.
Proof.
  intro n.
  reflexivity.
Qed.

Tactic ring normalizes the goal to an equality, converts both sides to polynomials via to_poly and poly_normalize, and solves if the polynomials are identical. It closes the goal with a placeholder term ring_solved.

Theorem ring_example : (x + 2*y) + (3*x + y) = 4*x + 3*y.
Proof.
  ring.
Qed.

Tactic apply H or apply H with x:=t looks up hypothesis H, matches its type against the goal using match_goal, generates subgoals for missing arguments, and builds an App node in the reconstructor. Named with bindings are evaluated and substituted.

Theorem plus_comm : ∀ n m : Nat, plus n m = plus m n.
Proof.
  intros n m.
  apply plus_comm_helper.
Qed.

Tactic split works when the current goal normalizes to an inductive type with exactly one constructor (e.g. conjunction A ∧ B with constructor conj). It applies that constructor, generating subgoals for each of its arguments and updating the reconstructor with the appropriate constructor application.

Theorem and_intro : ∀ A B : Prop, A → B → A ∧ B.
Proof.
  intros A B Ha Hb.
  split.
  - exact Ha.
  - exact Hb.
Qed.

Tactic left (resp. right) works when the goal normalizes to a disjunction A ∨ B. It replaces the goal with the left (resp. right) disjunct and updates the reconstructor with or_introl (resp. or_intror).

Theorem left_example : ∀ A B : Prop, A → A ∨ B.
Proof.
  intros A B Ha.
  left.
  exact Ha.
Qed.

Tactic exists t works when the current goal normalizes to an existential ∃ x : A, P x (or ex). It provides witness t, replaces the goal with P t, and updates the reconstructor to build the ex_intro constructor.

Theorem exists_plus : ∃ n : Nat, plus n O = n.
Proof.
  exists O.
  reflexivity.
Qed.

Tactic assumption scans the current context for a hypothesis whose type exactly matches the goal (after normalization) and closes the goal with that hypothesis variable if found.

Theorem assumption_example : ∀ A : Prop, A → A.
Proof.
  intro A.
  assumption.
Qed.

Tactic assert (H : T) (or assert H : T) creates a new subgoal to prove T, then adds H : T to the context of the original goal (implemented via a let-binding in the proof term).

Theorem assert_example : ∀ n : Nat, n = n.
Proof.
  intro n.
  assert (H : n = n).
  - reflexivity.
  - exact H.
Qed.

Tactic rewrite H or rewrite <- H (where H has type l = r) matches l (or r if backward) in the goal and replaces it with r (or l), keeping the original goal type unchanged otherwise. The reconstructor wraps the sub-proof with a rewrite placeholder.

Theorem rewrite_demo : ∀ n : Nat, plus (plus O n) O = n.
Proof.
  intro n.
  rewrite plus_O_n.
  reflexivity.
Qed.

Tactic induction x (or induction x as [c1_names | …]) performs case analysis + induction on inductive variable x, generating one subgoal per constructor with induction hypotheses (IH) for recursive arguments. destruct x does the same but without generating IHs. The reconstructor builds a full Ind (match) node.

Theorem plus_O_n : ∀ n : Nat, plus O n = n.
Proof.
  intro n.
  induction n.
  - reflexivity.
  - simpl. rewrite IHn_0. reflexivity.
Qed.

Tactic discriminate H (or without argument on an equality goal) solves the goal with a contradiction term when H (or the goal) equates terms built from different constructors of the same inductive type.

Theorem no_confusion : ∀ n : Nat, O = S n → False.
Proof.
  intros n H.
  discriminate H.
Qed.

Tactic intuition attempts to solve the current goal using basic logical tautologies and rules (in this prototype it closes the goal with an intuition_placeholder term).

Theorem intuition_example : ∀ P : Prop, P ∨ ¬P.
Proof.
  intuition.
Qed.

All tactics are defined in tactics.ex. The dispatcher is the apply_tactic function with pattern matching on the parsed tactic tuple. New tactics are added by extending parse_tactic and the main case clause.