# 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.

```nix
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.

```nix
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.

```nix
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`.

```nix
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";
```