module Nat

import Base
import NatDefs

/*
  Theorems about Nat literals and addition.

  This file proves neutral-element, associativity, commutativity, and
  monotonicity facts for `+`, and registers the literal rewrites that
  make arithmetic on Nat literals evaluate smoothly.
*/

// ============================================================
// Properties of `lit`
// ============================================================

// `lit` is idempotent — wrapping a literal a second time is a no-op.
theorem lit_idem: all x:Nat.
  lit(lit(x)) = lit(x)
proof
  arbitrary x:Nat
  expand lit.
end

auto lit_idem

// `suc` distributes through `lit` so suc-of-literal evaluates to a literal.
theorem suc_lit: all n:Nat. suc(lit(n)) = lit(suc(n))
proof
  arbitrary n:Nat
  expand lit.
end

auto suc_lit

// ============================================================
// Properties of addition
// ============================================================

// Zero is the left identity for addition.
lemma zero_add: all n:Nat.
  zero + n = n
proof
  arbitrary n:Nat
  conclude zero + n = n by expand operator+.
end

auto zero_add

// Literal zero is also the left identity.
theorem nat_zero_add: all y:Nat.
  lit(zero) + y = y
proof
  arbitrary y:Nat
  expand lit.
end

auto nat_zero_add

// Zero is the right identity for addition.
lemma add_zero: all n:Nat.
  n + zero = n
proof
  induction Nat
  case zero {
    conclude zero + zero = zero   by .
  }
  case suc(n') suppose IH: n' + zero = n' {
    equations
      suc(n') + zero = suc(n' + zero)  by expand operator+.
              ... = suc(n')      by replace IH.
  }
end

auto add_zero

// Literal zero is also the right identity.
theorem nat_add_zero: all x:Nat.
  x + lit(zero) = x
proof
  arbitrary x:Nat
  expand lit.
end

auto nat_add_zero

// `suc` on the left of `+` factors out.
lemma suc_add: all m:Nat, n:Nat.
  suc(m) + n = suc(m + n)
proof
  arbitrary m:Nat, n:Nat
  expand operator+.
end

// Literal-friendly form of `suc_add` for arithmetic on Nat literals.
theorem lit_suc_add: all x:Nat, y:Nat.
  lit(suc(x)) + lit(y) = lit(suc(lit(x) + lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand lit
  suc_add
end

auto lit_suc_add

// `suc(n) = 1 + n` — the one-plus form of successor.
lemma suc_one_add: all n:Nat.
  suc(n) = suc(zero) + n
proof
  arbitrary n:Nat
  equations
    suc(n) =# suc(zero + n) #      by expand operator+.
       ... = suc(zero) + n         by symmetric suc_add[zero, n]
end

// Literal form of `suc_one_add`.
theorem nat_suc_one_add: all n:Nat.
  suc(n) = lit(suc(zero)) + n
proof
  arbitrary n:Nat
  expand lit
  suc_one_add
end

// Reverse direction of `suc_one_add` — `1 + n = suc(n)`.
lemma one_add_suc: all n:Nat.
  suc(zero) + n = suc(n)
proof
  arbitrary n:Nat
  symmetric suc_one_add[n]
end

// `1 + n` is never zero — a positivity fact used in many side conditions.
lemma not_one_add_zero: all n:Nat.
  not (suc(zero) + n = zero)
proof
  arbitrary n:Nat
  expand operator+.
end

// `suc` on the right of `+` factors out.
lemma add_suc: all m:Nat. all n:Nat.
  m + suc(n) = suc(m + n)
proof
  induction Nat
  case zero {
    arbitrary n : Nat
    conclude zero + suc(n) = suc(zero + n)  by evaluate
  }
  case suc(n') suppose IH {
    arbitrary n : Nat
    equations
      suc(n') + suc(n) = suc(n' + suc(n))  by evaluate
                   ... = suc(suc(n' + n))  by replace IH.
                   ... = suc(suc(n') + n)  by evaluate
  }
end

// Addition on Nat is commutative.
theorem add_commute: all n:Nat. all m:Nat.  n + m = m + n
proof
  induction Nat
  case zero {
    arbitrary m : Nat
    equations  zero + m = m      by evaluate
                    ... = m + zero  by .
  }
  case suc(n') suppose IH {
    arbitrary m : Nat
    equations suc(n') + m = suc(n' + m)     by evaluate
                      ... = suc(m + n')     by replace IH.
                      ... = # m + suc(n') # by replace add_suc.
  }
end

// `1 + m = suc(m)` — duplicate of `one_add_suc` with a one-step proof.
lemma one_add: all m:Nat.  suc(zero) + m = suc(m)
proof
  arbitrary m:Nat
  expand 1 * operator+.
end

// `m + 1 = suc(m)` — successor as right-addition by one.
lemma add_one: all m:Nat.  m + suc(zero) = suc(m)
proof
  arbitrary m:Nat
  equations
    m + suc(zero) = suc(zero) + m       by add_commute[m][suc(zero)]
       ... = suc(m)       by one_add[m]
end

// Addition on Nat is associative (left-to-right form).
theorem add_assoc: all m:Nat, n:Nat, o:Nat.
  (m + n) + o = m + (n + o)
proof
  induction Nat
  case zero {
    arbitrary n:Nat, o:Nat
    conclude (zero + n) + o = zero + (n + o)   by evaluate
  }
  case suc(m') suppose IH {
    arbitrary n:Nat, o:Nat
    equations
      (suc(m') + n) + o = suc((m' + n) + o)  by evaluate
                    ... = suc(m' + (n + o))  by replace IH.
                    ... = suc(m') + (n + o)  by evaluate
  }
end

associative operator+ in Nat

// Right-to-left form of associativity, for rewriting in the other direction.
theorem assoc_add: all m:Nat, n:Nat, o:Nat.
  m + (n + o) = (m + n) + o
proof
  arbitrary m:Nat, n:Nat, o:Nat
  symmetric add_assoc
end

// Left-cancellation as an iff — adding the same term on the left preserves equality.
theorem add_both_sides_of_equal: all x:Nat. all y:Nat, z:Nat.
  x + y = x + z ⇔ y = z
proof
  induction Nat
  case zero {
    arbitrary y:Nat, z:Nat
    evaluate
  }
  case suc(x') suppose IH {
    arbitrary y:Nat, z:Nat
    expand operator+
    have A: suc(x' + y) = suc(x' + z) ⇔ (x' + y = x' + z) by {
      have fwd: if suc(x' + y) = suc(x' + z) then (x' + y = x' + z) by {
        assume seq injective suc seq
      }
      have bkwd: if (x' + y = x' + z) then suc(x' + y) = suc(x' + z) by {
        assume eq replace eq.
      }
      fwd, bkwd
    }
    have B: ((x' + y = x' + z) ⇔ (y = z)) by IH[y,z]
    conclude ((suc(x' + y) = suc(x' + z)) ⇔ (y = z))
      by apply iff_trans[suc(x' + y) = suc(x' + z), x' + y = x' + z, y = z]
         to A, B
  }
end

// left_cancel is obsolete, remove soon.
// Use add_both_sides_of_equal instead.
theorem left_cancel: all x:Nat. all y:Nat, z:Nat.
  if x + y = x + z then y = z
proof
  induction Nat
  case zero {
    arbitrary y:Nat, z:Nat
    suppose prem: zero + y = zero + z
    equations   y = zero + y      by evaluate
              ... = zero + z      by prem
              ... = z          by evaluate
  }
  case suc(x') suppose IH: all y:Nat, z:Nat. if x' + y = x' + z then y = z {
    arbitrary y:Nat, z:Nat
    suppose prem: suc(x') + y = suc(x') + z
    show y = z
    apply IH[y,z] to {
      show x' + y = x' + z
      injective suc
      conclude suc(x' + y) = suc(x' + z)  by evaluate in prem
    }
  }
end

// A sum equals zero only if both summands are zero — used to discharge `n + m = 0` premises.
lemma add_to_zero: all n:Nat. all m:Nat.
  if n + m = zero
  then n = zero and m = zero
proof
  induction Nat
  case zero {
    arbitrary m:Nat
    suppose zmz
    have: m = zero
      by expand operator + in zmz
    replace (recall m = zero).
  }
  case suc(n') suppose IH {
    arbitrary m:Nat
    suppose snmz: suc(n') + m = zero
    conclude false
        by expand operator + in snmz
  }
end