~/bend-docscommunity

nat.bend source

nat.bend on the hub · documented module

# 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:      Unitdef 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 * bdef 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 * cdef 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 * cdef 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 <= bdef 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 cdef 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{}:      Emptydef Bool.is_false(b: Bool) -> Type:  match b:    case True{}:      Empty    case False{}:      Unitdef 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 agreedef 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{}:      Emptydef Cmp.is_EQ(c: Cmp) -> Type:  match c:    case LT{}:      Empty    case EQ{}:      Unit    case GT{}:      Emptydef Cmp.is_GT(c: Cmp) -> Type:  match c:    case LT{}:      Empty    case EQ{}:      Empty    case GT{}:      Unitdef 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 rootdef 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 halfdef 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)))