Std.Proof

View source →

Genuine propositional-equality proofs over the inductive Std.Nat (spec 2026-07-04-identity-type-as-inductive).

These are NOT runtime tokens. Each law is checked by the dependent kernel: the proofs proceed by induction (match on the Nat index) and close each case with reflexive or rewrite, exactly the technique Agda's Data.Nat.Properties uses. plus is Std.Nat.plus, whose definition the kernel unfolds during conversion, so plus(Z, Z) reduces to Z and the reflexive cases type-check.

The previous version of this module returned the :cure_refl atom from Equivalent(...)-shaped signatures whose propositions were either vacuous (Equivalent(Int, n, n)) or unstated (a "commutativity" law with return type Equivalent(Int, a, a)). Those tokens carried no propositional content; the laws below actually prove what they claim.

Examples

cure
use Std.Proof

plus_zero_right(n)        # : Equivalent(Nat, plus(n, Z), n)
plus_comm(m, n)          # : Equivalent(Nat, plus(m, n), plus(n, m))

Group tag consumed by Cure.Stdlib.Preload. n + 0 = n. Induction on n: the Z case is reflexive, and the S case rewrites by the inductive hypothesis before closing on reflexive(S(k)).

Functions

  • # fn plus_comm(m: Nat, n: Nat) -> Equivalent(Nat, plus(m, n), plus(n, m))

    Commutativity of addition, m + n = n + m. Induction on m, using plus_zero_right for the base case and plus_succ_right together with the inductive hypothesis for the successor case.

  • # fn plus_succ_right(m: Nat, n: Nat) -> Equivalent(Nat, plus(m, S(n)), S(plus(m, n)))

    m + S(n) = S(m + n). Induction on m; the successor case pushes the S outward via the inductive hypothesis.

  • # fn plus_zero_right(n: Nat) -> Equivalent(Nat, plus(n, Z), n)