Proof Basics

The first proof examples stay close to computation. You write a HOAS proposition, give refl as evidence, and let the kernel normalize both sides. When the normal forms match, the checker accepts the proof.

Later sections use the same checker with dependent pairs and eliminators. The full source lives at examples/proof-basics.nix.

Computational equality

Addition, boolean negation, list length, and append are defined with eliminators. The equality proof is still refl; the work happens in normalization.

add = m: n:
  ind 0 (lam "_" nat (_: nat)) n
    (lam "k" nat (_: lam "ih" nat (ih: succ ih)))
    m;

addThreeFive =
  (checkHoas (eq nat (add (natLit 3) (natLit 5)) (natLit 8)) refl)
    .tag == "desc-con";

doubleNegTrue =
  (checkHoas (eq bool (not_ (not_ true_)) true_) refl).tag == "desc-con";

Dependent witnesses

A sigma value packages a witness with proof that the witness has the requested property. These examples use concrete witnesses whose proof component reduces to reflexivity.

witnessAddResult =
  let
    ty = sigma "x" nat (x: eq nat (add (natLit 3) (natLit 5)) x);
    tm = pair (natLit 8) refl;
  in
  (checkHoas ty tm).tag == "pair";

Eliminators as programs

Natural, boolean, list, and sum eliminators let the proof examples define small programs inside HOAS. Each checked assertion ties the computed result back to an equality.

listSum =
  let
    sumList = xs: listElim 0 nat (lam "_" (listOf nat) (_: nat)) zero
      (lam "h" nat (h: lam "t" (listOf nat) (_:
        lam "ih" nat (ih: add h ih))))
      xs;
  in
  (checkHoas (eq nat (sumList list123) (natLit 6)) refl).tag == "desc-con";

Polymorphism and impossibility

The final examples leave concrete computation and check reusable functions: a universe-polymorphic identity and the eliminator from Void.

polyId =
  let
    ty = forall "A" (u 0) (a: forall "x" a (_: a));
    tm = lam "A" (u 0) (a: lam "x" a (x: x));
  in
  (checkHoas ty tm).tag == "lam";

exFalso =
  let
    ty = forall "A" (u 0) (a: forall "x" void (_: a));
    tm = lam "A" (u 0) (a: lam "x" void (x: absurd a x));
  in
  (checkHoas ty tm).tag == "lam";