src/nat.bend source

src/nat.bend on the hub · documented module

import Baseimport ./class.bend as C# nat.bend: Nat arithmetic and order laws.##   import ./nat.bend as Nat#   Nat.ord(), Nat.add_sg()      # instances for class.bend## Equations put the side a caller rewrites away on the right: `%e : P`# replaces e's right side in the goal with its left side.# plain binders, so it fits C.Semigroup's assoc fieldlaw add_assoc:  for a: Nat  for b: Nat  for c: Nat  {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}def add_assoc(a, b, c):  match a:    case 0n:      {==}    case 1n+p:      %add_assoc(p, b, c) : {1n+Nat.add(p, Nat.add(b, c)) == 1n+_ : Nat}      {==}# a <= b, as a type: Unit when it holds, Empty when it does not.def LE(a: Nat, b: Nat) -> Data:  match a b:    case 0n y:      Unit    case 1n+x 0n:      Empty    case 1n+x 1n+y:      LE(x, y)# a < b. LT(i, 0n) computes to Empty.def LT(a: Nat, b: Nat) -> Data:  LE(1n+a, b)law le_refl:  for a: Nat  LE(a, a)def le_refl(a):  match a:    case 0n:      Unit{}    case 1n+p:      le_refl(p)law le_step:  for a: Nat  LE(a, 1n+a)def le_step(a):  match a:    case 0n:      Unit{}    case 1n+p:      le_step(p)law le_trans:  for a: Nat  for b: Nat  for c: Nat  for ab: LE(a, b)  for bc: LE(b, c)  LE(a, c)def le_trans(a, b, c, ab, bc):  match a b c:    case 0n b c:      Unit{}    case 1n+x 0n c:      match ab:    case 1n+x 1n+y 0n:      match bc:    case 1n+x 1n+y 1n+z:      le_trans(x, y, z, ab, bc)# a - k <= a (Nat.sub stops at 0)law sub_le:  for a: Nat  for k: Nat  LE(Nat.sub(a, k), a)def sub_le(a, k):  match a k:    case 0n 0n:      Unit{}    case 0n 1n+q:      Unit{}    case 1n+p 0n:      le_refl(1n+p)    case 1n++p 1n++q:      le_trans(Nat.sub(p, q), p, 1n+p, sub_le(p, q), le_step(p))# Compares a and b and returns the proof of the side that holds.def le_case(a: Nat, b: Nat) -> Or(LE(a, b), LE(b, a)):  match a b:    case 0n y:      Inl{Unit{}}    case 1n+x 0n:      Inr{Unit{}}    case 1n+x 1n+y:      le_case(x, y)# Motives that refute {False{} == True{}} and {True{} == False{}}.law IsFalse:  for c: Bool  Typedef IsFalse(c):  match c:    case False{}:      Unit    case True{}:      Emptylaw IsTrue:  for c: Bool  Typedef IsTrue(c):  match c:    case True{}:      Unit    case False{}:      Empty# The two outcomes of Nat.is_lt as LE proofs. Base's min, max and clamp# branch on is_lt.law le_of_is_lt:  for a: Nat  for b: Nat  for e: {Nat.is_lt(a, b) == True{} : Bool}  LE(a, b)def le_of_is_lt(a, b, e):  match a b:    case 0n y:      Unit{}    case 1n+x 0n:      %e : IsFalse(_)      Unit{}    case 1n+x 1n+y:      le_of_is_lt(x, y, e)law ge_of_not_lt:  for a: Nat  for b: Nat  for e: {Nat.is_lt(a, b) == False{} : Bool}  LE(b, a)def ge_of_not_lt(a, b, e):  match a b:    case 0n 0n:      Unit{}    case 0n 1n+y:      %e : IsTrue(_)      Unit{}    case 1n+x 0n:      Unit{}    case 1n+x 1n+y:      ge_of_not_lt(x, y, e)# Nat ordered by LEdef ord() -> C.Ord<Nat>:  C.Ord{LE, le_case}# Nat under additiondef add_sg() -> C.Semigroup<Nat>:  C.Semigroup{Nat.add, add_assoc}