Proof Language and Elaboration

The grammar adds proof namespaces to implementation and interface declarations under proof-preview. The foundation, not the source notation, determines derivability. Examples in this document are future conformance inputs and do not run on the current compiler.

C3-SYNTAX-001 — Names, declarations, and profiles

public proof namespace Math { ... } introduces logical declarations, not a runtime object. universe u; binds a namespace-scoped universe parameter; each declaration lists its own parameters in <u,...> and may use only those parameters in its type and body. Names resolve lexically, then through exact module imports under the inherited package closure. There are no ambient imports, implicit propositions, inferred axioms, or model-dependent name lookup. Imported kernel environments must be independently checked or loaded from a revalidated local checker cache bound to the exact environment and kernel.

define is transparent; opaque has a checked but non-reducing body; theorem requires a proposition as its type and is opaque. All declare an explicit type, body, and using (...) profile allowlist. using () selects the constructive default. axiom declares a typed constant assigned to a named profile. Acceptance of its type is not admission of its assumption. Package profiles bind exact qualified axiom names and identities; standard profile names cannot be shadowed or rebound.

C3-SYNTAX-002 — Explicit terms and elaboration

Prop, Sort(level), and Type(level) have the foundation meanings. forall (x:A) -> B elaborates to a dependent product; fun (x:A) => t to an abstraction; let (x:A) = a in t to a typed let. Repeated binders nest left-to-right. f(a,b) elaborates to App(App(f,a),b); A -> B is not an additional implicit-binder notation in this initial grammar. Names with universe arguments, such as Eq<1>, explicitly instantiate all level parameters. There are no inferred implicit term arguments or coercions in this baseline.

All propositions use ordinary declared types and functions. Equality is Eq<u>(A,a,b), not host-language equality; conjunction and existence are declared inductives. Numerals in proof data positions require a library constructor expression; integer literals in the grammar denote levels only. Pattern-matching tactics and recursive syntax are not kernel extensions: external elaborators may generate recursor applications, but serialized terms must use only the explicit core and preserve the claimed type.

C3-SYNTAX-003 — Minimal logical library

Each environment supplies checked definitions, not trusted evaluator hooks, for the following names before examples referring to them can be admitted:

Name	Definition shape
False	Empty inductive in Prop
True	Prop with one fieldless constructor True.intro
And(P,Q)	Prop with constructor taking p:P, q:Q
Or(P,Q)	Prop with separate constructors taking P or Q
Not(P)	Definition forall (p:P) -> False
Eq<u>(A,a,b)	Parameters A:Sort(u), a:A; index b:A; sole constructor Eq.refl<u>(A,a):Eq<u>(A,a,a)
Exists<u>(A,pred)	Prop with constructor taking a:A, h:pred(a)
Nonempty<u>(A)	Prop with constructor taking a:A
Sigma<u,v>(A,B)	Data family with constructor taking a:A, b:B(a); sort determined by field universes
Nat	Data family in Type(0), with Nat.zero and Nat.succ(n)

These are schemata with explicit universe parameters where necessary; constructor argument order is parameter order followed by field order. Their source definitions and hashes are part of the environment, not assumed from spelling. In particular, replacing Eq with a differently defined type cannot satisfy an obligation pinned to the original equality environment.

Example without any library imports:

public proof namespace Logic {
  theorem identity : forall (P : Prop) -> forall (p : P) -> P
    using () = fun (P : Prop) (p : P) => p;
  theorem compose : forall (P : Prop) (Q : Prop) (R : Prop) ->
    forall (f : forall (p : P) -> Q) (g : forall (q : Q) -> R) ->
    forall (p : P) -> R
    using () = fun (P : Prop) (Q : Prop) (R : Prop)
      (f : forall (p : P) -> Q) (g : forall (q : Q) -> R)
      (p : P) => g(f(p));
}

Composition is justified by checked application and its premises. Merely combining two accepted strings or runtime types does not establish a theorem.

C3-SYNTAX-004 — Verification and extraction declarations

verify name : P subject S model M mode partial using (...) by p; requests a check against the formal obligation P derived for the exact subject and model. mode total additionally requires the bridge’s termination or progress obligations. S and M resolve to checked, identity-bound records; a source name alone is insufficient. A user-supplied P must match the derived obligation under the same environment, not replace it. Matching may use checked definitional equality; the receipt retains the original expected statement identity. A bridge-specific unresolved requirement prevents a full verification claim.

extract name from f contract theorem_name; requests the extraction judgment in extraction. It does not declare every theorem executable. The result is a checked Algorithm artifact with its own identity and retained link to f, its contract, and the chosen extraction profile.

C3-SYNTAX-005 — Interfaces and source authority

Public proof interfaces expose qualified names, universes, declared types, kernel/profile identities, theorem statement IDs, and derived axiom footprints. Private proof bodies and model inputs are not included automatically. An interface-only theorem is an outstanding proof dependency, not an axiom and not an independently checked theorem. Verification requires its full proof closure or an explicit named trust assumption permitted by policy.

The textual .zli grammar carries signatures; statement IDs and assumption summaries belong to the corresponding logical public projection, not additional unchecked syntax in a signature. A redacted projection is a view, not a partial Proof record accepted by the logical-record loader.

An interface declaration uses the same header ending in ; instead of = t;; the grammar distinguishes interface items from implementation items. Axioms remain explicitly marked as axioms in either representation. Public bodies of transparent definitions needed for downstream conversion must be supplied by the checked environment; a hidden body cannot secretly reduce during checking. Changes to authoritative prose require the interpretation rules in Intent authority, not a new mathematical proof by fiat.