Proofs and tactics

Ligare uses the Curry–Howard view: a proposition is a constraint, and a proof is a term checked against that constraint. The current implementation has two root universes:

• data contains values retained by the generated program.
• prop contains propositions and evidence erased after checking.

There are no separate theorem or proof universes. theorem is a top-level command for naming a checked proposition inhabitant.

Proof blocks

The by form builds a term interactively:

theorem identity : int -> int := by
  intro value
  exact value

Proofs can also discharge a refinement at an expression:

def NonNegative : prop := int where (value => value >= 0)

#check 0 by
  exact auto : NonNegative

Core tactics

The current prover includes:

Tactic	Role
exact term	Close the goal with a term.
intro	Introduce Pi-type parameters or hypotheses.
apply term	Use a function to reduce the current goal.
have name := term	Add a local lemma.
constructor	Build conjunctions and structs.
cases term	Split Boolean or enum cases.
induction term	Generate structural enum branches.
assumption	Use a matching local theorem.
rfl	Close a reflexive equality.
rw and simp	Rewrite with equality evidence.
solve, decide, norm_num, omega, linarith	Request bounded, kernel-checked automation.

Automation is fail-closed: an unknown proposition is not treated as proven. The kernel checks the generated evidence after tactic elaboration. Custom #[tactic] functions can extend the tactic surface, but their result still passes through normal checking.

Erasure

Evidence for a prop constraint is removed before C code generation. A refinement can therefore make an interface safer without adding a proof object or proof parameter to the runtime representation.