Two worlds and a vocabulary¶

Hold one idea in your head from the very start, because it explains most of Algae’s shape: there are two separate worlds, and their names live in two disjoint namespaces.

The term world — sorts, operators, variables, and the propositions built from them. This is the term namespace.
The proof world — axioms, rules, lemmas, and hypotheses: the things you apply to build a proof. This is the proof namespace.

A name in one world is invisible to the other. You can’t sneak a lemma into a proposition, and you can’t apply an operator as a proof step. It feels strict at first, but it’s exactly what keeps proofs honest — and we’ll make it delightfully concrete back in Induction and friends.

Running the checker¶

Everything below is a .alg file you feed to the CLI:

cargo run -p algae-cli -- verify file.alg      # elaborate + proof-check
cargo run -p algae-cli -- typecheck file.alg   # signatures only, skip proofs
cargo run -p algae-cli -- parse file.alg        # syntax only
cargo run -p algae-cli -- fmt file.alg          # normalize operator glyphs

verify is the one that runs the proof checker. A clean run prints … : checked N proof obligation(s) — the sound of success.

ASCII or Unicode, your call¶

Every operator has an ASCII and a Unicode spelling, and both lex to the same token. This tutorial uses the pretty Unicode forms; if you’d rather type ASCII, fmt converts it to Unicode for you (and fmt --ascii converts back).

ASCII	Unicode	meaning
`\|-`	`⊢`	turnstile (a sequent)
`->`	`→`	function type
`forall`	`∀`	universal
`exists`	`∃`	existential
`lambda`	`λ`	lambda
`=>`	`⇒`	implication
`/\` `\/` `~`	`∧` `∨` `¬`	and, or, not

The product type is always written * (as in Nat * Nat).

Sorts, operators, types¶

A sort is a base type. An operator is a total function symbol with a signature. Nothing here is a proof yet — this is the term world’s vocabulary. Here’s the opening of nat.alg:

sort Nat : Sort;            # a base sort

op 0 : → Nat;              # a nullary operator (a constant)
op s : Nat → Nat;          # successor
op + : Nat * Nat → Nat;    # a binary operator, written infix as x + y

Types are built from sorts with * (product), | (sum), and → (function). A proposition has the special type Prop; a predicate is therefore just an operator into Prop, e.g. op even : Nat → Prop. option.alg shows all three at once — its bind takes a product of an Option(A) and a function:

op bind : Option(A) * (A → Option(B)) → Option(B);

Propositions and sequents¶

A proposition is just a Prop-valued term: an equation a = b, a connective (∧, ∨, ⇒, ⇔, ¬), a quantifier (∀, ∃), or a predicate applied to arguments. Terms and propositions share one grammar.

A sequent is a proposition under a context of assumptions:

context ⊢ proposition

The context lists typed variables and named hypotheses. With an empty context you just write ⊢ proposition. These two read “x = x” and “under x and y, and a proof of x = y, conclude y = x”:

⊢ x = x
x : Nat, y : Nat, h := x = y ⊢ y = x

A lemma states a sequent and must supply a proof of it. That’s next.