peano arithmetic

peano-demo.bpa

// Peano arithmetic: the living demo, and the exemplar for CONVENTIONS.md.
// Proves addZeroRight, addSuccRight, and addIsCommutative by induction.
//
// The induction schema is a stored FORM (comptime semantics): it is not
// checked until instantiated with a concrete, written-out predicate, at which
// point it is monomorphized into plain first-order logic.

// -- signature --------------------------------------------------------------

sort Nat
const ZERO: Nat
func succ(n: Nat): Nat
func add(a: Nat, b: Nat): Nat

// -- axioms: addition by recursion on the first argument --------------------

axiom addZeroLeft: forall b: Nat. add(ZERO, b) = b
axiom addSuccLeft: forall a, b: Nat. add(succ(a), b) = succ(add(a, b))

// -- schemas ----------------------------------------------------------------

schema induction(prop: Nat -> Prop):
  prop(ZERO) -> (forall k: Nat. prop(k) -> prop(succ(k))) -> forall n: Nat. prop(n)

// -- theorems ---------------------------------------------------------------

// Strategy: induction on n with prop(k) := add(k, ZERO) = k.
// (addZeroLeft reduces ZERO on the LEFT; this is the mirror-image fact.)
theorem addZeroRight: forall n: Nat. add(n, ZERO) = n
proof
  // base case: addZeroLeft specialized at b := ZERO
  add-zero-left| forall b: Nat. add(ZERO, b) = b
    [by axiom addZeroLeft]
  base| add(ZERO, ZERO) = ZERO
    [by forall_elim(ZERO) add-zero-left]

  // inductive step: unfold add on succ(k), then rewrite with the IH
  induction-step| fix k: Nat {
    given-ih| assume add(k, ZERO) = k {
      add-succ-left| forall a, b: Nat. add(succ(a), b) = succ(add(a, b))
        [by axiom addSuccLeft]
      add-succ-left-at-k| forall b: Nat. add(succ(k), b) = succ(add(k, b))
        [by forall_elim(k) add-succ-left]
      unfolded| add(succ(k), ZERO) = succ(add(k, ZERO))
        [by forall_elim(ZERO) add-succ-left-at-k]
      ih| add(k, ZERO) = k
        [by hypothesis given-ih]
      succ-case| add(succ(k), ZERO) = succ(k)
        [by rewrite ih unfolded]
    }
    step-at-k| add(k, ZERO) = k -> add(succ(k), ZERO) = succ(k)
      [by implies_intro given-ih]
  }
  step| forall k: Nat. add(k, ZERO) = k -> add(succ(k), ZERO) = succ(k)
    [by forall_intro induction-step]

  conclusion| forall n: Nat. add(n, ZERO) = n
    [by instantiate induction((fun k: Nat => add(k, ZERO) = k)) base step]
qed

// Strategy: fix b, then induct on the left argument with
// prop(k) := add(k, succ(b)) = succ(add(k, b)).
// Stated forall b, a (b outermost) because induction binds its variable
// innermost; use sites forall_elim twice anyway, so the order costs nothing.
theorem addSuccRight: forall b, a: Nat. add(a, succ(b)) = succ(add(a, b))
proof
  generalize-b| fix b: Nat {
    // base case: reduce both sides with addZeroLeft, then chain via symmetry
    add-zero-left| forall c: Nat. add(ZERO, c) = c
      [by axiom addZeroLeft]
    at-succ-b| add(ZERO, succ(b)) = succ(b)
      [by forall_elim(succ(b)) add-zero-left]
    at-b| add(ZERO, b) = b
      [by forall_elim(b) add-zero-left]
    at-b-refl| add(ZERO, b) = add(ZERO, b)
      [by reflexivity]
    at-b-sym| b = add(ZERO, b)
      [by rewrite at-b at-b-refl]
    base| add(ZERO, succ(b)) = succ(add(ZERO, b))
      [by rewrite at-b-sym at-succ-b]

    // inductive step: push succ through the left with addSuccLeft, rewrite the IH in,
    // then fold the right-hand side back up
    induction-step| fix k: Nat {
      given-ih| assume add(k, succ(b)) = succ(add(k, b)) {
        add-succ-left| forall a, c: Nat. add(succ(a), c) = succ(add(a, c))
          [by axiom addSuccLeft]
        add-succ-left-at-k| forall c: Nat. add(succ(k), c) = succ(add(k, c))
          [by forall_elim(k) add-succ-left]
        unfolded| add(succ(k), succ(b)) = succ(add(k, succ(b)))
          [by forall_elim(succ(b)) add-succ-left-at-k]
        ih| add(k, succ(b)) = succ(add(k, b))
          [by hypothesis given-ih]
        rewritten| add(succ(k), succ(b)) = succ(succ(add(k, b)))
          [by rewrite ih unfolded]
        fold-target| add(succ(k), b) = succ(add(k, b))
          [by forall_elim(b) add-succ-left-at-k]
        fold-refl| add(succ(k), b) = add(succ(k), b)
          [by reflexivity]
        fold-sym| succ(add(k, b)) = add(succ(k), b)
          [by rewrite fold-target fold-refl]
        succ-case| add(succ(k), succ(b)) = succ(add(succ(k), b))
          [by rewrite fold-sym rewritten]
      }
      step-at-k| add(k, succ(b)) = succ(add(k, b)) -> add(succ(k), succ(b)) = succ(add(succ(k), b))
        [by implies_intro given-ih]
    }
    step| forall k: Nat. add(k, succ(b)) = succ(add(k, b)) -> add(succ(k), succ(b)) = succ(add(succ(k), b))
      [by forall_intro induction-step]

    for-all-a| forall a: Nat. add(a, succ(b)) = succ(add(a, b))
      [by instantiate induction((fun k: Nat => add(k, succ(b)) = succ(add(k, b)))) base step]
  }
  conclusion| forall b, a: Nat. add(a, succ(b)) = succ(add(a, b))
    [by forall_intro generalize-b]
qed

// Strategy: induction on b with prop(k) := forall a. add(a, k) = add(k, a);
// each case handles all a at once (an inner fix).
theorem addIsCommutative: forall b, a: Nat. add(a, b) = add(b, a)
proof
  // base case: add(a, ZERO) = a = add(ZERO, a), chaining the two ZERO facts
  base-case| fix a: Nat {
    add-zero-right| forall n: Nat. add(n, ZERO) = n
      [by theorem addZeroRight]
    right-zero| add(a, ZERO) = a
      [by forall_elim(a) add-zero-right]
    add-zero-left| forall c: Nat. add(ZERO, c) = c
      [by axiom addZeroLeft]
    left-zero| add(ZERO, a) = a
      [by forall_elim(a) add-zero-left]
    left-zero-refl| add(ZERO, a) = add(ZERO, a)
      [by reflexivity]
    left-zero-sym| a = add(ZERO, a)
      [by rewrite left-zero left-zero-refl]
    chained| add(a, ZERO) = add(ZERO, a)
      [by rewrite left-zero-sym right-zero]
  }
  base| forall a: Nat. add(a, ZERO) = add(ZERO, a)
    [by forall_intro base-case]

  // inductive step: unfold via addSuccRight, swap with the IH, fold via addSuccLeft
  induction-step| fix k: Nat {
    given-ih| assume forall a: Nat. add(a, k) = add(k, a) {
      pointwise| fix a2: Nat {
        add-succ-right| forall b, a: Nat. add(a, succ(b)) = succ(add(a, b))
          [by theorem addSuccRight]
        add-succ-right-at-k| forall a: Nat. add(a, succ(k)) = succ(add(a, k))
          [by forall_elim(k) add-succ-right]
        left-unfold| add(a2, succ(k)) = succ(add(a2, k))
          [by forall_elim(a2) add-succ-right-at-k]
        ih| forall a: Nat. add(a, k) = add(k, a)
          [by hypothesis given-ih]
        ih-at-a2| add(a2, k) = add(k, a2)
          [by forall_elim(a2) ih]
        swapped| add(a2, succ(k)) = succ(add(k, a2))
          [by rewrite ih-at-a2 left-unfold]
        add-succ-left| forall a, b: Nat. add(succ(a), b) = succ(add(a, b))
          [by axiom addSuccLeft]
        add-succ-left-at-k| forall b: Nat. add(succ(k), b) = succ(add(k, b))
          [by forall_elim(k) add-succ-left]
        right-unfold| add(succ(k), a2) = succ(add(k, a2))
          [by forall_elim(a2) add-succ-left-at-k]
        right-refl| add(succ(k), a2) = add(succ(k), a2)
          [by reflexivity]
        right-sym| succ(add(k, a2)) = add(succ(k), a2)
          [by rewrite right-unfold right-refl]
        succ-case| add(a2, succ(k)) = add(succ(k), a2)
          [by rewrite right-sym swapped]
      }
      for-all-a| forall a: Nat. add(a, succ(k)) = add(succ(k), a)
        [by forall_intro pointwise]
    }
    step-at-k| (forall a: Nat. add(a, k) = add(k, a)) -> forall a: Nat. add(a, succ(k)) = add(succ(k), a)
      [by implies_intro given-ih]
  }
  step| forall k: Nat. (forall a: Nat. add(a, k) = add(k, a)) -> forall a: Nat. add(a, succ(k)) = add(succ(k), a)
    [by forall_intro induction-step]

  conclusion| forall b, a: Nat. add(a, b) = add(b, a)
    [by instantiate induction((fun k: Nat => forall a: Nat. add(a, k) = add(k, a))) base step]
qed