# lib/nat.bend -- the arithmetic of Base's Nat, as theorems.
#
# Every lemma here is about the operators Base ships (Nat.add, Nat.mul,
# Nat.double, Nat.cmp), so a program that uses `+n` gets these laws for
# free. A claim is a def whose return type is the proposition and whose
# body is the proof; `bend nat.bend --check` verifies all of them.
#
# Reading a proof: `match x` refines the goal per constructor, a recursive
# call is the induction hypothesis, `{==}` closes a goal whose two sides
# compute to the same term, and `%e : P` rewrites with an equation
# e : {a == b}: the goal must be P with b at the `_` marks, and what
# follows proves P with a there. So `%e` REPLACES b BY a in the goal; to
# replace X by Y you need an equation {Y == X}, and Equal.sym flips one
# that points the other way.

import Base

# ---------------------------------------------------------------------
# successor: injective, never zero
# ---------------------------------------------------------------------

def Nat.pred(n: Nat) -> Nat:
  match n:
    case 0n:
      0n
    case 1n+p:
      p

# a Type computed from a Nat: Empty at zero, Unit above. Rewriting an
# equation {1n+a == 0n} into it turns Unit into Empty.
def Nat.is_succ(n: Nat) -> Type:
  match n:
    case 0n:
      Empty
    case 1n+p:
      Unit

def Nat.succ_neq_zero(-a: Nat, e: {1n+a == 0n : Nat}) -> Empty:
  %e : Nat.is_succ(_)
  Unit{}

def Nat.zero_neq_succ(-a: Nat, e: {0n == 1n+a : Nat}) -> Empty:
  Nat.succ_neq_zero(a, Equal.sym(Nat, 0n, 1n+a, e))

def Nat.succ_inj(-a: Nat, -b: Nat, e: {1n+a == 1n+b : Nat}) -> {a == b : Nat}:
  Equal.cong(Nat, Nat, x => Nat.pred(x), 1n+a, 1n+b, e)

# ---------------------------------------------------------------------
# (Nat, add, 0n) is a commutative monoid
# ---------------------------------------------------------------------

def Nat.add_zero(a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      %Nat.add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
      {==}

def Nat.add_succ(a: Nat, -b: Nat) -> {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      %Equal.sym(Nat, Nat.add(p, 1n+b), 1n+Nat.add(p, b), Nat.add_succ(p, b)) : {1n+_ == 2n+Nat.add(p, b) : Nat}
      {==}

def Nat.add_comm(a: Nat, +b: Nat) -> {Nat.add(a, b) == Nat.add(b, a) : Nat}:
  match a:
    case 0n:
      Equal.sym(Nat, Nat.add(b, 0n), b, Nat.add_zero(b))
    case 1n+p:
      +p2 = p
      %Equal.sym(Nat, Nat.add(b, 1n+p2), 1n+Nat.add(b, p2), Nat.add_succ(b, p2)) : {1n+Nat.add(p2, b) == _ : Nat}
      %Nat.add_comm(p2, b) : {1n+Nat.add(p2, b) == 1n+_ : Nat}
      {==}

def Nat.add_assoc(a: Nat, -b: Nat, -c: Nat) -> {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      %Nat.add_assoc(p, b, c) : {1n+Nat.add(p, Nat.add(b, c)) == 1n+_ : Nat}
      {==}

# a + (b + c) = b + (a + c)
def Nat.add_swap(+a: Nat, +b: Nat, +c: Nat) -> {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}:
  %Equal.sym(Nat, Nat.add(b, Nat.add(a, c)), Nat.add(Nat.add(b, a), c), Nat.add_assoc(b, a, c)) : {Nat.add(a, Nat.add(b, c)) == _ : Nat}
  %Nat.add_comm(a, b) : {Nat.add(a, Nat.add(b, c)) == Nat.add(_, c) : Nat}
  Nat.add_assoc(a, b, c)

# (a + b) + (c + d) = (a + c) + (b + d)
def Nat.add_add_swap(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}:
  %Nat.add_assoc(a, c, Nat.add(b, d)) : {Nat.add(Nat.add(a, b), Nat.add(c, d)) == _ : Nat}
  %Nat.add_swap(b, c, d) : {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(a, _) : Nat}
  Equal.sym(Nat, Nat.add(a, Nat.add(b, Nat.add(c, d))), Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add_assoc(a, b, Nat.add(c, d)))

# ---------------------------------------------------------------------
# (Nat, mul, 1n) is a commutative monoid that distributes over add
# ---------------------------------------------------------------------

def Nat.mul_zero(a: Nat) -> {Nat.mul(a, 0n) == 0n : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      Nat.mul_zero(p)

def Nat.mul_one(a: Nat) -> {Nat.mul(a, 1n) == a : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      %Nat.mul_one(p) : {1n+Nat.mul(p, 1n) == 1n+_ : Nat}
      {==}

def Nat.one_mul(a: Nat) -> {Nat.mul(1n, a) == a : Nat}:
  Nat.add_zero(a)

# a * (1 + b) = a + a * b
def Nat.mul_succ(a: Nat, +b: Nat) -> {Nat.mul(a, 1n+b) == Nat.add(a, Nat.mul(a, b)) : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      +p2 = p
      %Nat.add_swap(b, p2, Nat.mul(p2, b)) : {1n+Nat.add(b, Nat.mul(p2, 1n+b)) == 1n+_ : Nat}
      %Nat.mul_succ(p2, b) : {1n+Nat.add(b, Nat.mul(p2, 1n+b)) == 1n+Nat.add(b, _) : Nat}
      {==}

def Nat.mul_comm(a: Nat, +b: Nat) -> {Nat.mul(a, b) == Nat.mul(b, a) : Nat}:
  match a:
    case 0n:
      Equal.sym(Nat, Nat.mul(b, 0n), 0n, Nat.mul_zero(b))
    case 1n+p:
      +p2 = p
      %Equal.sym(Nat, Nat.mul(b, 1n+p2), Nat.add(b, Nat.mul(b, p2)), Nat.mul_succ(b, p2)) : {Nat.add(b, Nat.mul(p2, b)) == _ : Nat}
      %Nat.mul_comm(p2, b) : {Nat.add(b, Nat.mul(p2, b)) == Nat.add(b, _) : Nat}
      {==}

# (a + b) * c = a * c + b * c
def Nat.add_mul(a: Nat, -b: Nat, +c: Nat) -> {Nat.mul(Nat.add(a, b), c) == Nat.add(Nat.mul(a, c), Nat.mul(b, c)) : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      %Equal.sym(Nat, Nat.mul(Nat.add(p, b), c), Nat.add(Nat.mul(p, c), Nat.mul(b, c)), Nat.add_mul(p, b, c)) : {Nat.add(c, _) == Nat.add(Nat.add(c, Nat.mul(p, c)), Nat.mul(b, c)) : Nat}
      Nat.add_assoc(c, Nat.mul(p, c), Nat.mul(b, c))

# a * (b + c) = a * b + a * c
def Nat.mul_add(a: Nat, +b: Nat, +c: Nat) -> {Nat.mul(a, Nat.add(b, c)) == Nat.add(Nat.mul(a, b), Nat.mul(a, c)) : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      +p2 = p
      %Equal.sym(Nat, Nat.mul(p2, Nat.add(b, c)), Nat.add(Nat.mul(p2, b), Nat.mul(p2, c)), Nat.mul_add(p2, b, c)) : {Nat.add(Nat.add(b, c), _) == Nat.add(Nat.add(b, Nat.mul(p2, b)), Nat.add(c, Nat.mul(p2, c))) : Nat}
      Nat.add_add_swap(b, c, Nat.mul(p2, b), Nat.mul(p2, c))

def Nat.mul_assoc(a: Nat, +b: Nat, +c: Nat) -> {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      +p2 = p
      %Equal.sym(Nat, Nat.mul(Nat.add(b, Nat.mul(p2, b)), c), Nat.add(Nat.mul(b, c), Nat.mul(Nat.mul(p2, b), c)), Nat.add_mul(b, Nat.mul(p2, b), c)) : {Nat.add(Nat.mul(b, c), Nat.mul(p2, Nat.mul(b, c))) == _ : Nat}
      %Nat.mul_assoc(p2, b, c) : {Nat.add(Nat.mul(b, c), Nat.mul(p2, Nat.mul(b, c))) == Nat.add(Nat.mul(b, c), _) : Nat}
      {==}

# ---------------------------------------------------------------------
# doubling
# ---------------------------------------------------------------------

def Nat.double_add(a: Nat) -> {Nat.double(a) == Nat.add(a, a) : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      +p2 = p
      %Equal.sym(Nat, Nat.add(p2, 1n+p2), 1n+Nat.add(p2, p2), Nat.add_succ(p2, p2)) : {2n+Nat.double(p2) == 1n+_ : Nat}
      %Nat.double_add(p2) : {2n+Nat.double(p2) == 2n+_ : Nat}
      {==}

def Nat.two_mul(+a: Nat) -> {Nat.mul(2n, a) == Nat.double(a) : Nat}:
  %Equal.sym(Nat, Nat.double(a), Nat.add(a, a), Nat.double_add(a)) : {Nat.add(a, Nat.add(a, 0n)) == _ : Nat}
  %Nat.add_zero(a) : {Nat.add(a, Nat.add(a, 0n)) == Nat.add(a, _) : Nat}
  {==}

def Nat.double_inj(a: Nat, b: Nat, e: {Nat.double(a) == Nat.double(b) : Nat}) -> {a == b : Nat}:
  match a b:
    case 0n 0n:
      {==}
    case 0n 1n+q:
      Empty.absurd({0n == 1n+q : Nat}, Nat.zero_neq_succ(1n+Nat.double(q), e))
    case 1n+p 0n:
      Empty.absurd({1n+p == 0n : Nat}, Nat.succ_neq_zero(1n+Nat.double(p), e))
    case 1n+p 1n+q:
      Equal.cong(Nat, Nat, x => 1n+x, p, q, Nat.double_inj(p, q, Nat.succ_inj(Nat.double(p), Nat.double(q), Nat.succ_inj(1n+Nat.double(p), 1n+Nat.double(q), e))))

# ---------------------------------------------------------------------
# cancellation
# ---------------------------------------------------------------------

def Nat.add_cancel_l(a: Nat, -b: Nat, -c: Nat, e: {Nat.add(a, b) == Nat.add(a, c) : Nat}) -> {b == c : Nat}:
  match a:
    case 0n:
      e
    case 1n+p:
      Nat.add_cancel_l(p, b, c, Nat.succ_inj(Nat.add(p, b), Nat.add(p, c), e))

def Nat.add_cancel_r(+a: Nat, +b: Nat, +c: Nat, e: {Nat.add(b, a) == Nat.add(c, a) : Nat}) -> {b == c : Nat}:
  Nat.add_cancel_l(a, b, c, Equal.trans(Nat, Nat.add(a, b), Nat.add(b, a), Nat.add(a, c), Nat.add_comm(a, b), Equal.trans(Nat, Nat.add(b, a), Nat.add(c, a), Nat.add(a, c), e, Nat.add_comm(c, a))))

def Nat.add_eq_zero_l(a: Nat, -b: Nat, e: {Nat.add(a, b) == 0n : Nat}) -> {a == 0n : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      Empty.absurd({1n+p == 0n : Nat}, Nat.succ_neq_zero(Nat.add(p, b), e))

def Nat.add_eq_zero_r(+a: Nat, +b: Nat, e: {Nat.add(a, b) == 0n : Nat}) -> {b == 0n : Nat}:
  Nat.add_eq_zero_l(b, a, Equal.trans(Nat, Nat.add(b, a), Nat.add(a, b), 0n, Nat.add_comm(b, a), e))

# ---------------------------------------------------------------------
# order. Le(a, b) is a Type computed from a and b: Unit when a <= b,
# Empty otherwise, so a closed instance is proved by Unit{} and a false
# one is refuted by matching its (empty) evidence.
# ---------------------------------------------------------------------

def Nat.Le(a: Nat, b: Nat) -> Type:
  match a:
    case 0n:
      Unit
    case 1n+ap:
      match b:
        case 0n:
          Empty
        case 1n+bp:
          Nat.Le(ap, bp)

def Nat.Lt(a: Nat, b: Nat) -> Type:
  Nat.Le(1n+a, b)

def Nat.le_refl(a: Nat) -> Nat.Le(a, a):
  match a:
    case 0n:
      Unit{}
    case 1n+p:
      Nat.le_refl(p)

def Nat.le_succ(a: Nat, b: Nat, h: Nat.Le(a, b)) -> Nat.Le(a, 1n+b):
  match a:
    case 0n:
      Unit{}
    case 1n+p:
      match b:
        case 0n:
          match h:
        case 1n+q:
          Nat.le_succ(p, q, h)

# a < b implies a <= b
def Nat.lt_le(a: Nat, b: Nat, h: Nat.Lt(a, b)) -> Nat.Le(a, b):
  match b:
    case 0n:
      match h:
    case 1n+q:
      Nat.le_succ(a, q, h)

def Nat.le_trans(a: Nat, b: Nat, c: Nat, h1: Nat.Le(a, b), h2: Nat.Le(b, c)) -> Nat.Le(a, c):
  match a:
    case 0n:
      Unit{}
    case 1n+p:
      match b:
        case 0n:
          match h1:
        case 1n+q:
          match c:
            case 0n:
              match h2:
            case 1n+r:
              Nat.le_trans(p, q, r, h1, h2)

def Nat.le_antisym(a: Nat, b: Nat, h1: Nat.Le(a, b), h2: Nat.Le(b, a)) -> {a == b : Nat}:
  match a b:
    case 0n 0n:
      {==}
    case 0n 1n+q:
      match h2:
    case 1n+p 0n:
      match h1:
    case 1n+p 1n+q:
      Equal.cong(Nat, Nat, x => 1n+x, p, q, Nat.le_antisym(p, q, h1, h2))

def Nat.lt_irrefl(a: Nat, h: Nat.Lt(a, a)) -> Empty:
  match a:
    case 0n:
      match h:
    case 1n+p:
      Nat.lt_irrefl(p, h)

def Nat.eq_le(+a: Nat, -b: Nat, e: {a == b : Nat}) -> Nat.Le(a, b):
  %e : Nat.Le(a, _)
  Nat.le_refl(a)

def Nat.le_add_r(a: Nat, -b: Nat) -> Nat.Le(a, Nat.add(a, b)):
  match a:
    case 0n:
      Unit{}
    case 1n+p:
      Nat.le_add_r(p, b)

def Nat.le_add_l(+a: Nat, +b: Nat) -> Nat.Le(b, Nat.add(a, b)):
  %Nat.add_comm(b, a) : Nat.Le(b, _)
  Nat.le_add_r(b, a)

def Nat.le_add_both(a: Nat, +b: Nat, +c: Nat, +d: Nat, h1: Nat.Le(a, b), h2: Nat.Le(c, d)) -> Nat.Le(Nat.add(a, c), Nat.add(b, d)):
  match a:
    case 0n:
      Nat.le_trans(c, d, Nat.add(b, d), h2, Nat.le_add_l(b, d))
    case 1n+p:
      match b:
        case 0n:
          match h1:
        case 1n+q:
          Nat.le_add_both(p, q, c, d, h1, h2)

def Nat.le_add_mono_l(c: Nat, -a: Nat, -b: Nat, h: Nat.Le(a, b)) -> Nat.Le(Nat.add(c, a), Nat.add(c, b)):
  match c:
    case 0n:
      h
    case 1n+p:
      Nat.le_add_mono_l(p, a, b, h)

# a <= b exactly when b = a + c for some c
def Nat.le_diff.con(-ap: Nat, -bp: Nat, w: (&c: Nat -> {Nat.add(ap, c) == bp : Nat})) -> (&c: Nat -> {Nat.add(1n+ap, c) == 1n+bp : Nat}):
  (c, prf) = w
  (c, Equal.cong(Nat, Nat, x => 1n+x, Nat.add(ap, c), bp, prf))

def Nat.le_diff(a: Nat, b: Nat, h: Nat.Le(a, b)) -> (&c: Nat -> {Nat.add(a, c) == b : Nat}):
  match a:
    case 0n:
      (b, {==})
    case 1n+ap:
      match b:
        case 0n:
          match h:
        case 1n+bp:
          Nat.le_diff.con(ap, bp, Nat.le_diff(ap, bp, h))

# ---------------------------------------------------------------------
# Bool and Cmp facts used to reflect decisions into propositions
# ---------------------------------------------------------------------

def Bool.is_true(b: Bool) -> Type:
  match b:
    case True{}:
      Unit
    case False{}:
      Empty

def Bool.is_false(b: Bool) -> Type:
  match b:
    case True{}:
      Empty
    case False{}:
      Unit

def Bool.false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
  %e : Bool.is_false(_)
  Unit{}

def Bool.true_ne_false(e: {True{} == False{} : Bool}) -> Empty:
  %e : Bool.is_true(_)
  Unit{}

def Bool.not_not(b: Bool) -> {Bool.not(Bool.not(b)) == b : Bool}:
  match b:
    case True{}:
      {==}
    case False{}:
      {==}

def Bool.or_idem(b: Bool) -> {Bool.or(b, b) == b : Bool}:
  match b:
    case True{}:
      {==}
    case False{}:
      {==}

# Bool.same(a, b): True when a and b agree
def Bool.same(a: Bool, b: Bool) -> Bool:
  match a b:
    case True{} True{}:
      True{}
    case True{} False{}:
      False{}
    case False{} True{}:
      False{}
    case False{} False{}:
      True{}

def Bool.same_true(b: Bool) -> {Bool.same(True{}, b) == b : Bool}:
  match b:
    case True{}:
      {==}
    case False{}:
      {==}

def Bool.not_same_l(a: Bool, b: Bool) -> {Bool.not(Bool.same(a, b)) == Bool.same(Bool.not(a), b) : Bool}:
  match a b:
    case True{} True{}:
      {==}
    case True{} False{}:
      {==}
    case False{} True{}:
      {==}
    case False{} False{}:
      {==}

def Bool.same_or(a: Bool, b: Bool) -> {Bool.same(b, Bool.or(a, b)) == Bool.or(Bool.not(a), b) : Bool}:
  match a b:
    case True{} True{}:
      {==}
    case True{} False{}:
      {==}
    case False{} True{}:
      {==}
    case False{} False{}:
      {==}

def Cmp.is_LT(c: Cmp) -> Type:
  match c:
    case LT{}:
      Unit
    case EQ{}:
      Empty
    case GT{}:
      Empty

def Cmp.is_EQ(c: Cmp) -> Type:
  match c:
    case LT{}:
      Empty
    case EQ{}:
      Unit
    case GT{}:
      Empty

def Cmp.is_GT(c: Cmp) -> Type:
  match c:
    case LT{}:
      Empty
    case EQ{}:
      Empty
    case GT{}:
      Unit

def Cmp.eq_ne_lt(e: {EQ{} == LT{} : Cmp}) -> Empty:
  %e : Cmp.is_EQ(_)
  Unit{}

def Cmp.gt_ne_lt(e: {GT{} == LT{} : Cmp}) -> Empty:
  %e : Cmp.is_GT(_)
  Unit{}

def Cmp.lt_ne_eq(e: {LT{} == EQ{} : Cmp}) -> Empty:
  %e : Cmp.is_LT(_)
  Unit{}

def Cmp.gt_ne_eq(e: {GT{} == EQ{} : Cmp}) -> Empty:
  %e : Cmp.is_GT(_)
  Unit{}

# Nat.cmp answers LT only when a < b, and EQ only when a = b: the
# run-time comparison is faithful to the proposition.
def Nat.cmp_lt(a: Nat, b: Nat, e: {Nat.cmp(a, b) == LT{} : Cmp}) -> Nat.Lt(a, b):
  match a b:
    case 0n 0n:
      Cmp.eq_ne_lt(e)
    case 0n 1n+q:
      Unit{}
    case 1n+p 0n:
      Cmp.gt_ne_lt(e)
    case 1n+p 1n+q:
      Nat.cmp_lt(p, q, e)

def Nat.cmp_eq(a: Nat, b: Nat, e: {Nat.cmp(a, b) == EQ{} : Cmp}) -> {a == b : Nat}:
  match a b:
    case 0n 0n:
      {==}
    case 0n 1n+q:
      Empty.absurd({0n == 1n+q : Nat}, Cmp.lt_ne_eq(e))
    case 1n+p 0n:
      Empty.absurd({1n+p == 0n : Nat}, Cmp.gt_ne_eq(e))
    case 1n+p 1n+q:
      Equal.cong(Nat, Nat, x => 1n+x, p, q, Nat.cmp_eq(p, q, e))

def Nat.is_lt_true(a: Nat, b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> Nat.Lt(a, b):
  match a b:
    case 0n 0n:
      Bool.false_ne_true(e)
    case 0n 1n+q:
      Unit{}
    case 1n+p 0n:
      Bool.false_ne_true(e)
    case 1n+p 1n+q:
      Nat.is_lt_true(p, q, e)

# ---------------------------------------------------------------------
# parity
# ---------------------------------------------------------------------

def Nat.even(n: Nat) -> Bool:
  match n:
    case 0n:
      True{}
    case 1n+p:
      Bool.not(Nat.even(p))

def Nat.half(n: Nat) -> Nat:
  match n:
    case 0n:
      0n
    case 1n+0n:
      0n
    case 2n+p:
      1n+Nat.half(p)

def Nat.even_add(a: Nat, +b: Nat) -> {Nat.even(Nat.add(a, b)) == Bool.same(Nat.even(a), Nat.even(b)) : Bool}:
  match a:
    case 0n:
      Equal.sym(Bool, Bool.same(True{}, Nat.even(b)), Nat.even(b), Bool.same_true(Nat.even(b)))
    case 1n+p:
      +p2 = p
      %Equal.sym(Bool, Nat.even(Nat.add(p2, b)), Bool.same(Nat.even(p2), Nat.even(b)), Nat.even_add(p2, b)) : {Bool.not(_) == Bool.same(Bool.not(Nat.even(p2)), Nat.even(b)) : Bool}
      Bool.not_same_l(Nat.even(p2), Nat.even(b))

def Nat.even_mul(a: Nat, +b: Nat) -> {Nat.even(Nat.mul(a, b)) == Bool.or(Nat.even(a), Nat.even(b)) : Bool}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      +p2 = p
      %Equal.sym(Bool, Nat.even(Nat.add(b, Nat.mul(p2, b))), Bool.same(Nat.even(b), Nat.even(Nat.mul(p2, b))), Nat.even_add(b, Nat.mul(p2, b))) : {_ == Bool.or(Bool.not(Nat.even(p2)), Nat.even(b)) : Bool}
      %Equal.sym(Bool, Nat.even(Nat.mul(p2, b)), Bool.or(Nat.even(p2), Nat.even(b)), Nat.even_mul(p2, b)) : {Bool.same(Nat.even(b), _) == Bool.or(Bool.not(Nat.even(p2)), Nat.even(b)) : Bool}
      Bool.same_or(Nat.even(p2), Nat.even(b))

# a square has the parity of its root
def Nat.even_sq(+n: Nat) -> {Nat.even(Nat.mul(n, n)) == Nat.even(n) : Bool}:
  %Equal.sym(Bool, Nat.even(Nat.mul(n, n)), Bool.or(Nat.even(n), Nat.even(n)), Nat.even_mul(n, n)) : {_ == Nat.even(n) : Bool}
  Bool.or_idem(Nat.even(n))

def Nat.even_double(a: Nat) -> {Nat.even(Nat.double(a)) == True{} : Bool}:
  match a:
    case 0n:
      {==}
    case 1n+p:
      %Equal.sym(Bool, Nat.even(Nat.double(p)), True{}, Nat.even_double(p)) : {Bool.not(Bool.not(_)) == True{} : Bool}
      {==}

# an even number is the double of its half
def Nat.even_half(n: Nat, e: {Nat.even(n) == True{} : Bool}) -> {n == Nat.double(Nat.half(n)) : Nat}:
  match n:
    case 0n:
      {==}
    case 1n+0n:
      Empty.absurd({1n == Nat.double(Nat.half(1n)) : Nat}, Bool.false_ne_true(e))
    case 2n+p:
      +p2 = p
      Equal.cong(Nat, Nat, x => 2n+x, p2, Nat.double(Nat.half(p2)),
        Nat.even_half(p2, Equal.trans(Bool, Nat.even(p2), Bool.not(Bool.not(Nat.even(p2))), True{},
          Equal.sym(Bool, Bool.not(Bool.not(Nat.even(p2))), Nat.even(p2), Bool.not_not(Nat.even(p2))), e)))