PROOF_div.bend

bend-osdev-u32@0.1.0.0 · 187 lines · 20 definitions

1# Proofs of LAWS_div.bend, from Base's definition of Nat.divmod: with a
2# divisor 1 + bp, Nat.divmod(a, 1 + bp) runs go(a, bp, 0, 0), which counts m
3# down and r up (m + r == bp throughout) and d once per full round. The
4# lemmas are those bend-osdev-ext2, -iodev and -blockdev proved for their
5# own use (PROOF.bend, PROOF_range.bend), now proved here once.
6import Base
7import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
8import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
9import bend-osdev-u32@0.1.0.0/LAWS_div.bend as Laws
10
11def ud.sub_zero(a: Nat) -> {Nat.sub(a, 0n) == a : Nat}:
12  match a:
13    case 0n:
14      {==}
15    case 1n+p:
16      {==}
17
18def ud.pred(n: Nat) -> Nat:
19  match n:
20    case 0n:
21      0n
22    case 1n+p:
23      p
24
25def ud.succ_inj(+x: Nat, +y: Nat, e: {1n+x == 1n+y : Nat}) -> {x == y : Nat}:
26  Equal.cong(Nat, Nat, ud.pred, 1n+x, 1n+y, e)
27
28# a + r == b + r gives a == b
29def ud.add_cancel(+r: Nat, +a: Nat, +b: Nat, e: {Nat.add(a, r) == Nat.add(b, r) : Nat}) -> {a == b : Nat}:
30  match r:
31    case 0n:
32      Equal.trans(Nat, a, Nat.add(b, 0n), b, Equal.trans(Nat, a, Nat.add(a, 0n), Nat.add(b, 0n), Equal.sym(Nat, Nat.add(a, 0n), a, UL.nat_add_zero(a)), e), UL.nat_add_zero(b))
33    case 1n+q:
34      ud.add_cancel(q, a, b, ud.succ_inj(Nat.add(a, q), Nat.add(b, q), Equal.trans(Nat, 1n+Nat.add(a, q), Nat.add(a, 1n+q), 1n+Nat.add(b, q), Equal.sym(Nat, Nat.add(a, 1n+q), 1n+Nat.add(a, q), UL.nat_add_succ(a, q)), Equal.trans(Nat, Nat.add(a, 1n+q), Nat.add(b, 1n+q), 1n+Nat.add(b, q), e, UL.nat_add_succ(b, q)))))
35
36def ud.bool_disc(b: Bool) -> Type:
37  match b:
38    case True{}:
39      Unit
40    case False{}:
41      Empty
42
43def ud.bool_clash(h: {False{} == True{} : Bool}) -> Empty:
44  %Equal.sym(Bool, False{}, True{}, h) : ud.bool_disc(_)
45  Unit{}
46
47def ud.ex_falso(-A: Type, e: Empty) -> A:
48  match e:
49
50def ud.no_lt_one(+np: Nat) -> {Nat.is_lt(1n+np, 1n) == True{} : Bool} -> Empty:
51  match np:
52    case 0n:
53      h => ud.bool_clash(h)
54    case 1n+q:
55      h => ud.bool_clash(h)
56
57# r < bp + 1 gives (bp - r) + r == bp
58def ud.sub_add(+bp: Nat, +r: Nat, h: {Nat.is_lt(r, 1n+bp) == True{} : Bool}) -> {Nat.add(Nat.sub(bp, r), r) == bp : Nat}:
59  match bp r:
60    case 0n 0n:
61      {==}
62    case 0n 1n+q:
63      ud.ex_falso({Nat.add(Nat.sub(0n, 1n+q), 1n+q) == 0n : Nat}, ud.no_lt_one(q, h))
64    case 1n+b 0n:
65      UL.nat_add_zero(1n+b)
66    case 1n+b 1n+q:
67      Equal.trans(Nat, Nat.add(Nat.sub(b, q), 1n+q), 1n+Nat.add(Nat.sub(b, q), q), 1n+b, UL.nat_add_succ(Nat.sub(b, q), q), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(Nat.sub(b, q), q), b, ud.sub_add(b, q, h)))
68
69# Division
70
71def ud.dm_lhs(+n: Nat, +m: Nat, +d: Nat, +r: Nat, +bp: Nat) -> Nat:
72  Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)))
73
74def ud.dm_sum(+n: Nat, +m: Nat, +d: Nat, +r: Nat, +bp: Nat) -> {Nat.add(m, r) == bp : Nat} -> {ud.dm_lhs(n, m, d, r, bp) == Nat.add(n, Nat.add(Nat.mul(d, 1n+bp), r)) : Nat}:
75  match n m:
76    case 0n _:
77      h => {==}
78    case 1n+np 0n:
79      +h =>
80        +dd = Nat.mul(d, 1n+bp)
81        +x = Nat.add(Nat.add(bp, dd), 0n)
82        %Equal.sym(Nat, r, bp, h) : {ud.dm_lhs(1n+np, 0n, d, r, bp) == 1n+Nat.add(np, Nat.add(dd, _)) : Nat}
83        %UL.nat_add_comm(bp, dd) : {ud.dm_lhs(1n+np, 0n, d, r, bp) == 1n+Nat.add(np, _) : Nat}
84        %UL.nat_add_zero(Nat.add(bp, dd)) : {ud.dm_lhs(1n+np, 0n, d, r, bp) == 1n+Nat.add(np, _) : Nat}
85        %UL.nat_add_succ(np, x) : {ud.dm_lhs(1n+np, 0n, d, r, bp) == _ : Nat}
86        ud.dm_sum(np, r, 1n+d, 0n, bp, Equal.trans(Nat, Nat.add(r, 0n), r, bp, UL.nat_add_zero(r), h))
87    case 1n+np 1n+mp:
88      h =>
89        +dd = Nat.mul(d, 1n+bp)
90        %UL.nat_add_succ(np, Nat.add(dd, r)) : {ud.dm_lhs(1n+np, 1n+mp, d, r, bp) == _ : Nat}
91        %UL.nat_add_succ(dd, r) : {ud.dm_lhs(1n+np, 1n+mp, d, r, bp) == Nat.add(np, _) : Nat}
92        ud.dm_sum(np, mp, d, 1n+r, bp, Equal.trans(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), bp, UL.nat_add_succ(mp, r), h))
93
94def ud.div_mod(+k: Nat, +bp: Nat) -> {Nat.add(Nat.mul(Nat.div(k, 1n+bp), 1n+bp), Nat.mod(k, 1n+bp)) == k : Nat}:
95  Equal.trans(Nat, ud.dm_lhs(k, bp, 0n, 0n, bp), Nat.add(k, 0n), k, ud.dm_sum(k, bp, 0n, 0n, bp, UL.nat_add_zero(bp)), UL.nat_add_zero(k))
96
97def ud.lt_add(+m: Nat, +r: Nat) -> {Nat.is_lt(r, 1n+Nat.add(m, r)) == True{} : Bool}:
98  match r:
99    case 0n:
100      {==}
101    case 1n+p:
102      %Equal.sym(Nat, Nat.add(m, 1n+p), 1n+Nat.add(m, p), UL.nat_add_succ(m, p)) : {Nat.is_lt(1n+p, 1n+_) == True{} : Bool}
103      ud.lt_add(m, p)
104
105def ud.dm_lt(+n: Nat, +m: Nat, +d: Nat, +r: Nat, +bp: Nat) -> {Nat.add(m, r) == bp : Nat} -> {Nat.is_lt(Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)), 1n+bp) == True{} : Bool}:
106  match n m:
107    case 0n _:
108      h =>
109        %h : {Nat.is_lt(r, 1n+_) == True{} : Bool}
110        ud.lt_add(m, r)
111    case 1n+np 0n:
112      h => ud.dm_lt(np, r, 1n+d, 0n, bp, Equal.trans(Nat, Nat.add(r, 0n), r, bp, UL.nat_add_zero(r), h))
113    case 1n+np 1n+mp:
114      h => ud.dm_lt(np, mp, d, 1n+r, bp, Equal.trans(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), bp, UL.nat_add_succ(mp, r), h))
115
116def ud.mod_lt(+k: Nat, +bp: Nat) -> {Nat.is_lt(Nat.mod(k, 1n+bp), 1n+bp) == True{} : Bool}:
117  ud.dm_lt(k, bp, 0n, 0n, bp, UL.nat_add_zero(bp))
118
119# fewer steps than m left in the round: the remainder grows by n
120def ud.dm_small(+n: Nat, +m: Nat, +d: Nat, +r: Nat) -> {Nat.is_lt(n, 1n+m) == True{} : Bool} -> {Nat.divmod.go(n, m, d, r) == (d, Nat.add(n, r)) : Nat & Nat}:
121  match n m:
122    case 0n _:
123      h => {==}
124    case 1n+np 0n:
125      h => ud.ex_falso({Nat.divmod.go(1n+np, 0n, d, r) == (d, Nat.add(1n+np, r)) : Nat & Nat}, ud.no_lt_one(np, h))
126    case 1n+np 1n+mp:
127      h =>
128        %UL.nat_add_succ(np, r) : {Nat.divmod.go(1n+np, 1n+mp, d, r) == (d, _) : Nat & Nat}
129        ud.dm_small(np, mp, d, 1n+r, h)
130
131# finishing a round: m steps, then one more starts the next
132def ud.dm_round(+m: Nat, +n: Nat, +d: Nat, +r: Nat) -> {Nat.divmod.go(Nat.add(m, 1n+n), m, d, r) == Nat.divmod.go(n, Nat.add(m, r), 1n+d, 0n) : Nat & Nat}:
133  match m:
134    case 0n:
135      {==}
136    case 1n+mp:
137      %UL.nat_add_succ(mp, r) : {Nat.divmod.go(Nat.add(1n+mp, 1n+n), 1n+mp, d, r) == Nat.divmod.go(n, _, 1n+d, 0n) : Nat & Nat}
138      ud.dm_round(mp, n, d, 1n+r)
139
140def ud.dm_rounds(+g: Nat, +i: Nat, +d: Nat, +bp: Nat) -> {Nat.is_lt(i, 1n+bp) == True{} : Bool} -> {Nat.divmod.go(Nat.add(Nat.mul(g, 1n+bp), i), bp, d, 0n) == (Nat.add(g, d), i) : Nat & Nat}:
141  match g:
142    case 0n:
143      h =>
144        %UL.nat_add_zero(i) : {Nat.divmod.go(i, bp, d, 0n) == (d, _) : Nat & Nat}
145        ud.dm_small(i, bp, d, 0n, h)
146    case 1n+gp:
147      h =>
148        +gg = Nat.mul(gp, 1n+bp)
149        +y = Nat.add(gg, i)
150        %Equal.sym(Nat, Nat.add(Nat.add(bp, gg), i), Nat.add(bp, y), UL.nat_add_assoc(bp, gg, i)) : {Nat.divmod.go(1n+_, bp, d, 0n) == (1n+Nat.add(gp, d), i) : Nat & Nat}
151        %UL.nat_add_succ(bp, y) : {Nat.divmod.go(_, bp, d, 0n) == (1n+Nat.add(gp, d), i) : Nat & Nat}
152        %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(bp, 1n+y), bp, d, 0n), Nat.divmod.go(y, Nat.add(bp, 0n), 1n+d, 0n), ud.dm_round(bp, y, d, 0n)) : {_ == (1n+Nat.add(gp, d), i) : Nat & Nat}
153        %Equal.sym(Nat, Nat.add(bp, 0n), bp, UL.nat_add_zero(bp)) : {Nat.divmod.go(y, _, 1n+d, 0n) == (1n+Nat.add(gp, d), i) : Nat & Nat}
154        %UL.nat_add_succ(gp, d) : {Nat.divmod.go(y, bp, 1n+d, 0n) == (_, i) : Nat & Nat}
155        ud.dm_rounds(gp, i, 1n+d, bp, h)
156
157# Rounding up. Nat.sub(1 + bp, 1) is Nat.sub(bp, 0), which is bp by
158# ud.sub_zero.
159
160# a + bp == (a + (bp - r)) + r, for r < 1 + bp
161def ud.cover_sum(+bp: Nat, +a: Nat, +r: Nat, h: {Nat.is_lt(r, 1n+bp) == True{} : Bool}) -> {Nat.add(a, Nat.sub(bp, 0n)) == Nat.add(Nat.add(a, Nat.sub(bp, r)), r) : Nat}:
162  %Equal.sym(Nat, Nat.sub(bp, 0n), bp, ud.sub_zero(bp)) : {Nat.add(a, _) == Nat.add(Nat.add(a, Nat.sub(bp, r)), r) : Nat}
163  %Equal.sym(Nat, Nat.add(Nat.add(a, Nat.sub(bp, r)), r), Nat.add(a, Nat.add(Nat.sub(bp, r), r)), UL.nat_add_assoc(a, Nat.sub(bp, r), r)) : {Nat.add(a, bp) == _ : Nat}
164  %ud.sub_add(bp, r, h) : {Nat.add(a, _) == Nat.add(a, Nat.add(Nat.sub(bp, r), r)) : Nat}
165  {==}
166
167def ud.cover(+bp: Nat, +a: Nat) -> {Nat.mul(Nat.div(Nat.add(a, Nat.sub(1n+bp, 1n)), 1n+bp), 1n+bp) == Nat.add(a, Nat.sub(Nat.sub(1n+bp, 1n), Nat.mod(Nat.add(a, Nat.sub(1n+bp, 1n)), 1n+bp))) : Nat}:
168  +t = Nat.add(a, Nat.sub(bp, 0n))
169  +q = Nat.div(t, 1n+bp)
170  +r = Nat.mod(t, 1n+bp)
171  %Equal.sym(Nat, Nat.sub(bp, 0n), bp, ud.sub_zero(bp)) : {Nat.mul(q, 1n+bp) == Nat.add(a, Nat.sub(_, r)) : Nat}
172  ud.add_cancel(r, Nat.mul(q, 1n+bp), Nat.add(a, Nat.sub(bp, r)), Equal.trans(Nat, Nat.add(Nat.mul(q, 1n+bp), r), t, Nat.add(Nat.add(a, Nat.sub(bp, r)), r), ud.div_mod(t, bp), ud.cover_sum(bp, a, r, ud.mod_lt(t, bp))))
173
174# The laws
175
176def Laws.nat_div_mod(a, bp):
177  ud.div_mod(a, bp)
178
179def Laws.nat_mod_lt(a, bp):
180  ud.mod_lt(a, bp)
181
182def Laws.nat_divmod_exact(g, i, bp, h):
183  %UL.nat_add_zero(g) : {Nat.divmod.go(Nat.add(Nat.mul(g, 1n+bp), i), bp, 0n, 0n) == (_, i) : Nat & Nat}
184  ud.dm_rounds(g, i, 0n, bp, h)
185
186def Laws.nat_round_up(bp, a):
187  ud.cover(bp, a)