a semi-formal proof about peano numbers, for illustration purposes

peano-proof.txt

GIVEN
  data N = Z | S N;            -- call this N:0 (peano representation of natural numbers)
  add Z y = y                  -- call this add:1
  add x Z = x                  -- call this add:2
  add x (S y) = add (S x) y    -- call this add:3

PROVE
  add x (S y) = S add (x y)   -- for all x, y : N

BEGIN

  -- We will prove all 4 cases:
  -- 0. X = Z   , Y = Z
  -- 1. X = Z   , Y = S n
  -- 2. X = S n , Y = Z
  -- 3. X = S n , Y = S n

  LEMMA 0. PROOF THAT add x (S y) = S (add x y)  WHERE X = Z , Y = Z
    -- proof by construction
    add x (S y) = add (S x) y    -- add:3
                = add (S Z) Z    -- substitution
                = S Z            -- application of add:2
                = S (add Z Z)    -- substitution, allowed by lemma zz, below
                = S (add x y)    -- by substitution
  END.

  LEMMA zz. PROOF THAT Z = add Z Z
    add Z y = y                  -- add:1
    add Z Z = Z                  -- parameter subtitution
          Z = add ZZ             -- definition of =
  END

  LEMMA 1. PROOF THAT add x (S y) = S (add x y)  WHERE X = Z , Y = S n
    -- TODO
  END

  LEMMA 2. PROOF THAT add x (S y) = S (add x y)  WHERE X = S n , Y = Z
    -- TODO
  END

  LEMMA 3. PROOF THAT add x (S y) = S (add x y)  WHERE X = S n , Y = S n
    -- TODO
  END

QED