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.

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.

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.

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.

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