# Equality Proofs


The J eliminator is the primitive way to reason from equality. These
examples build the familiar combinators by checking generic theorem
terms, then apply the same shapes to concrete values that reduce by
computation.

## Congruence

Congruence says that equal inputs stay equal after applying the same
function. The generic term is checked for arbitrary `A`, `B`, `f`,
`x`, and `y`; the concrete term exercises the same pattern after
normalizing arithmetic.

```nix
congType =
  let
    ty = forall "A" (u 0) (a:
      forall "B" (u 0) (b:
        forall "f" (forall "_" a (_: b)) (f:
          forall "x" a (x:
            forall "y" a (y:
              forall "_" (eq a x y) (_:
                eq b (app f x) (app f y)))))));
    tm = lam "A" (u 0) (a:
      lam "B" (u 0) (b:
        lam "f" (forall "_" a (_: b)) (f:
          lam "x" a (x:
            lam "y" a (y:
              lam "p" (eq a x y) (p:
                j a x
                  (lam "y'" a (y':
                    lam "_" (eq a x y') (_: eq b (app f x) (app f y'))))
                  refl
                  y
                  p))))));
  in
  (checkHoas ty tm).tag == "lam";
```

## Symmetry and transitivity

Symmetry flips an equality. Transitivity composes two equalities by
eliminating over the second proof and carrying the first proof as the
base case.

```nix
symType =
  let
    ty = forall "A" (u 0) (a:
      forall "x" a (x:
        forall "y" a (y:
          forall "_" (eq a x y) (_:
            eq a y x))));
    tm = lam "A" (u 0) (a:
      lam "x" a (x:
        lam "y" a (y:
          lam "p" (eq a x y) (p:
            j a x
              (lam "y'" a (y': lam "_" (eq a x y') (_: eq a y' x)))
              refl
              y
              p))));
  in
  (checkHoas ty tm).tag == "lam";
```

## Transport

Transport moves evidence through an equality in a dependent family.
The concrete example uses a boolean-indexed family that chooses
between `Nat` and `Bool`.

```nix
transportConcrete =
  let
    motiveP = b: boolElim 1 (lam "_" bool (_: u 0)) nat bool b;
    proofTm = j bool true_
      (lam "y" bool (y: lam "_" (eq bool true_ y) (_: motiveP y)))
      zero
      true_
      refl;
  in
  (checkHoas nat proofTm).tag == "app";
```

## Combining proof steps

The final example feeds a congruence proof into symmetry. It is a
small proof pipeline, and the useful invariant is that both
intermediate proof terms are still checked by the same kernel.

```nix
combinedProof =
  let
    add21 = add (natLit 2) (succ zero);
    three = natLit 3;
    sadd21 = succ add21;
    sthree = succ three;
    congStep = j nat add21
      (lam "y" nat (y: lam "_" (eq nat add21 y) (_: eq nat sadd21 (succ y))))
      refl
      three
      refl;
    proofTy = eq nat sthree sadd21;
    proofTm = j nat sadd21
      (lam "y" nat (y: lam "_" (eq nat sadd21 y) (_: eq nat y sadd21)))
      refl
      sthree
      congStep;
  in
  (checkHoas proofTy proofTm).tag == "app";
```