src/nat.bend

bend-lawful-stdlib@0.1.0.0 · 174 lines · 14 definitions

1import Base
2import bend-lawful-stdlib@0.1.0.0/src/class.bend as C
3
4# nat.bend: Nat arithmetic and order laws.
5#
6#   import ./nat.bend as Nat
7#   Nat.ord(), Nat.add_sg()      # instances for class.bend
8#
9# Equations put the side a caller rewrites away on the right: `%e : P`
10# replaces e's right side in the goal with its left side.
11
12# plain binders, so it fits C.Semigroup's assoc field
13law add_assoc:
14  for a: Nat
15  for b: Nat
16  for c: Nat
17  {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
18
19def add_assoc(a, b, c):
20  match a:
21    case 0n:
22      {==}
23    case 1n+p:
24      %add_assoc(p, b, c) : {1n+Nat.add(p, Nat.add(b, c)) == 1n+_ : Nat}
25      {==}
26
27# a <= b, as a type: Unit when it holds, Empty when it does not.
28def LE(a: Nat, b: Nat) -> Data:
29  match a b:
30    case 0n y:
31      Unit
32    case 1n+x 0n:
33      Empty
34    case 1n+x 1n+y:
35      LE(x, y)
36
37# a < b. LT(i, 0n) computes to Empty.
38def LT(a: Nat, b: Nat) -> Data:
39  LE(1n+a, b)
40
41law le_refl:
42  for a: Nat
43  LE(a, a)
44
45def le_refl(a):
46  match a:
47    case 0n:
48      Unit{}
49    case 1n+p:
50      le_refl(p)
51
52law le_step:
53  for a: Nat
54  LE(a, 1n+a)
55
56def le_step(a):
57  match a:
58    case 0n:
59      Unit{}
60    case 1n+p:
61      le_step(p)
62
63law le_trans:
64  for a: Nat
65  for b: Nat
66  for c: Nat
67  for ab: LE(a, b)
68  for bc: LE(b, c)
69  LE(a, c)
70
71def le_trans(a, b, c, ab, bc):
72  match a b c:
73    case 0n b c:
74      Unit{}
75    case 1n+x 0n c:
76      match ab:
77    case 1n+x 1n+y 0n:
78      match bc:
79    case 1n+x 1n+y 1n+z:
80      le_trans(x, y, z, ab, bc)
81
82# a - k <= a (Nat.sub stops at 0)
83law sub_le:
84  for a: Nat
85  for k: Nat
86  LE(Nat.sub(a, k), a)
87
88def sub_le(a, k):
89  match a k:
90    case 0n 0n:
91      Unit{}
92    case 0n 1n+q:
93      Unit{}
94    case 1n+p 0n:
95      le_refl(1n+p)
96    case 1n++p 1n++q:
97      le_trans(Nat.sub(p, q), p, 1n+p, sub_le(p, q), le_step(p))
98
99# Compares a and b and returns the proof of the side that holds.
100def le_case(a: Nat, b: Nat) -> Or(LE(a, b), LE(b, a)):
101  match a b:
102    case 0n y:
103      Inl{Unit{}}
104    case 1n+x 0n:
105      Inr{Unit{}}
106    case 1n+x 1n+y:
107      le_case(x, y)
108
109# Motives that refute {False{} == True{}} and {True{} == False{}}.
110law IsFalse:
111  for c: Bool
112  Type
113
114def IsFalse(c):
115  match c:
116    case False{}:
117      Unit
118    case True{}:
119      Empty
120
121law IsTrue:
122  for c: Bool
123  Type
124
125def IsTrue(c):
126  match c:
127    case True{}:
128      Unit
129    case False{}:
130      Empty
131
132# The two outcomes of Nat.is_lt as LE proofs. Base's min, max and clamp
133# branch on is_lt.
134law le_of_is_lt:
135  for a: Nat
136  for b: Nat
137  for e: {Nat.is_lt(a, b) == True{} : Bool}
138  LE(a, b)
139
140def le_of_is_lt(a, b, e):
141  match a b:
142    case 0n y:
143      Unit{}
144    case 1n+x 0n:
145      %e : IsFalse(_)
146      Unit{}
147    case 1n+x 1n+y:
148      le_of_is_lt(x, y, e)
149
150law ge_of_not_lt:
151  for a: Nat
152  for b: Nat
153  for e: {Nat.is_lt(a, b) == False{} : Bool}
154  LE(b, a)
155
156def ge_of_not_lt(a, b, e):
157  match a b:
158    case 0n 0n:
159      Unit{}
160    case 0n 1n+y:
161      %e : IsTrue(_)
162      Unit{}
163    case 1n+x 0n:
164      Unit{}
165    case 1n+x 1n+y:
166      ge_of_not_lt(x, y, e)
167
168# Nat ordered by LE
169def ord() -> C.Ord<Nat>:
170  C.Ord{LE, le_case}
171
172# Nat under addition
173def add_sg() -> C.Semigroup<Nat>:
174  C.Semigroup{Nat.add, add_assoc}