Theories, laws, and models¶

Single facts are nice, but real structure comes from theories and the models that satisfy them. A theory is a parameterized interface plus a list of laws (propositions its implementers must prove). group.alg builds the classic algebra hierarchy, each theory include-ing the previous one and piling on laws:

theory Monoid(
  S : Sort,
  mul : S * S → S,
  e : S
) laws
  include Semigroup(S, mul);            # associativity, inherited

  law left_identity(x : S)   ⊢ mul(e, x) = x;
  law right_identity(x : S)  ⊢ mul(x, e) = x;
end;

A model claims specific operators satisfy a theory, and must prove every law as an obligation. Here’s the Monad interface from monad.alg:

theory Monad(
  M : Sort → Sort,
  return : forall (X : Sort) st X → M(X),
  bind : forall (X Y : Sort) st M(X) * (X → M(Y)) → M(Y)
) laws
  law left_identity(A B : Sort, x : A, f : A → M(B))  ⊢ bind(A, B, return(A, x), f) = f(x);
  law right_identity(A : Sort, m : M(A))              ⊢ bind(A, A, m, λ (x : A) st return(A, x)) = m;
  law associativity(A B C : Sort, m : M(A), f : A → M(B), g : B → M(C))
    ⊢ bind(B, C, bind(A, B, m, f), g) = bind(A, C, m, λ (x : A) st bind(B, C, f(x), g));
end;

option.alg, list.alg, and result.alg each ship a verified model proving their type satisfies Monad. Let’s build a smaller one, end to end, that you can actually run.

Remember the stack from Algebraic specification? Those two axioms are really an interface — any type with push / pop / top obeying them is a stack. So make that a theory, then prove our concrete stack is a model of it:

import core;

sort Stack : Sort → Sort;
op empty : forall (A : Sort) st → Stack(A);
op push  : forall (A : Sort) st A * Stack(A) → Stack(A);
op pop   : forall (A : Sort) st Stack(A) → Stack(A);
op top   : forall (A : Sort) st Stack(A) → A;

axiom top_ax(A : Sort, x : A, s : Stack(A))  ⊢ top(A, push(A, x, s)) = x;
axiom pop_ax(A : Sort, x : A, s : Stack(A))  ⊢ pop(A, push(A, x, s)) = s;

# the interface: any S with these operations obeying these laws is a stack
theory StackSpec(
  S : Sort → Sort,
  e : forall (X : Sort) st S(X),
  psh : forall (X : Sort) st X * S(X) → S(X),
  pp : forall (X : Sort) st S(X) → S(X),
  tp : forall (X : Sort) st S(X) → X
) laws
  law top_law(A : Sort, x : A, s : S(A))  ⊢ tp(A, psh(A, x, s)) = x;
  law pop_law(A : Sort, x : A, s : S(A))  ⊢ pp(A, psh(A, x, s)) = s;
end;

# the claim: our concrete operations are a stack
model ConcreteStack satisfies StackSpec(Stack, empty, push, pop, top) iff laws
  law top_law;
  proof
    by top_ax(A, x, s);
  qed;

  law pop_law;
  proof
    by pop_ax(A, x, s);
  qed;
qed;

Read the model header as binding each theory parameter to something concrete: the constructor S becomes Stack, psh becomes push, and so on. Then iff laws opens the obligations — one law <name>; proof … qed; per law in the theory — and each is proved just like a lemma. Here every proof is a one-liner, because StackSpec’s laws are exactly our two axioms. Press Check ▶: two obligations discharged, and ConcreteStack is certified a stack.

Every model has this shape, however big. option.alg’s OptionMonad is the same skeleton with three richer proofs — each threading backward to reach its equality, the defeq discipline from Algebraic specification at scale.

Imports and the standard library¶

import module; brings in everything a module declares — its sorts, operators, axioms, and rules. import module(name, …) selects specific names, and import module(name as alias) renames. Either way the module’s operators come along (which is why import nat; let us write 0 and +).

The standard library lives in algae/stdlib/v1/:

module	what it provides
`core`	equality (`refl`, `symmetry`, `backward` / `forward`), logic, quantifiers
`nat`	`Nat`, `+`, `*`, and `induction`
`option`, `result`, `list`	data types with their `Monad` models
`monad`	the `Functor` / `Applicative` / `Monad` theories
`group`	the `Magma` → … → `AbelianGroup` hierarchy
`adt`	algebraic-datatype scaffolding

Verify the whole library in one go:

cargo run -p algae-cli -- verify algae/stdlib/v1/

Where to go next¶

algae/stdlib/v1/ — worked, verified modules to read and imitate.
lang-specs/spec.md (in the repository) — the precise grammar and static semantics, when you want the letter of the law.
tests/accept/ — one minimal proof per inference rule, if you like your examples bite-sized.

Now go break some proofs. The kernel is waiting.