1	import Base
2	import ./core.bend as Shape
3	import ./index_proofs.bend as Index
4	import ./broadcast_proofs.bend as Broadcast
5	
6	def contradiction(-value: Bool, yes: {True{} == value : Bool}, no: {False{} == value : Bool}) -> Empty:
7	  Shape.clash(Equal.trans(Bool, True{}, value, False{}, yes, Equal.sym(Bool, False{}, value, no)))
8	
9	def le_true(+a: Nat, +b: Nat, bound: Shape.LE(a, b)) -> {True{} == Nat.is_le(a, b) : Bool}:
10	  match a b:
11	    case 0n 0n:
12	      {==}
13	    case 0n 1n+q:
14	      {==}
15	    case 1n+p 0n:
16	      match bound:
17	    case 1n+p 1n+q:
18	      le_true(p, q, bound)
19	
20	def lt_true(+a: Nat, +b: Nat, bound: Shape.LT(a, b)) -> {True{} == Nat.is_lt(a, b) : Bool}:
21	  match a b:
22	    case 0n 0n:
23	      match bound:
24	    case 0n 1n+q:
25	      {==}
26	    case 1n+p 0n:
27	      match bound:
28	    case 1n+p 1n+q:
29	      lt_true(p, q, bound)
30	
31	def le_add_left(+a: Nat, -x: Nat, +c: Nat, bound: Shape.LE(Nat.add(a, x), c)) -> Shape.LE(a, c):
32	  match a c:
33	    case 0n c:
34	      Unit{}
35	    case 1n+p 0n:
36	      match bound:
37	    case 1n+p 1n+q:
38	      le_add_left(p, x, q, bound)
39	
40	def le_rewrite(-a: Nat, -b: Nat, -c: Nat, equal: {b == a : Nat}, bound: Shape.LE(b, c)) -> Shape.LE(a, c):
41	  %equal : Shape.LE(_, c)
42	  bound
43	
44	def add_swap(+a: Nat, +b: Nat, -c: Nat) -> {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}:
45	  match a:
46	    case 0n:
47	      {==}
48	    case 1n+p:
49	      %Equal.sym(Nat, Nat.add(p, Nat.add(b, c)), Nat.add(b, Nat.add(p, c)), add_swap(p, b, c)) : {1n+_ == Nat.add(b, 1n+Nat.add(p, c)) : Nat}
50	      Broadcast.add_succ(b, Nat.add(p, c))
51	
52	def mul_succ_right(+a: Nat, +q: Nat) -> {Nat.mul(a, 1n+q) == Nat.add(a, Nat.mul(a, q)) : Nat}:
53	  match a:
54	    case 0n:
55	      {==}
56	    case 1n+p:
57	      %Equal.sym(Nat, Nat.mul(p, 1n+q), Nat.add(p, Nat.mul(p, q)), mul_succ_right(p, q)) : {1n+Nat.add(q, _) == 1n+Nat.add(p, Nat.add(q, Nat.mul(p, q))) : Nat}
58	      %add_swap(q, p, Nat.mul(p, q)) : {1n+Nat.add(q, Nat.add(p, Nat.mul(p, q))) == 1n+_ : Nat}
59	      {==}
60	
61	def mul_zero_right(+a: Nat) -> {Nat.mul(a, 0n) == 0n : Nat}:
62	  match a:
63	    case 0n:
64	      {==}
65	    case 1n+p:
66	      mul_zero_right(p)
67	
68	def mul_one_right(+a: Nat) -> {Nat.mul(a, 1n) == a : Nat}:
69	  match a:
70	    case 0n:
71	      {==}
72	    case 1n+p:
73	      Equal.cong(Nat, Nat, value => 1n+value, Nat.mul(p, 1n), p, mul_one_right(p))
74	
75	def mul_comm(+a: Nat, +b: Nat) -> {Nat.mul(a, b) == Nat.mul(b, a) : Nat}:
76	  match a:
77	    case 0n:
78	      Equal.sym(Nat, Nat.mul(b, 0n), 0n, mul_zero_right(b))
79	    case 1n+p:
80	      %Equal.sym(Nat, Nat.mul(b, 1n+p), Nat.add(b, Nat.mul(b, p)), mul_succ_right(b, p)) : {Nat.add(b, Nat.mul(p, b)) == _ : Nat}
81	      Equal.cong(Nat, Nat, value => Nat.add(b, value), Nat.mul(p, b), Nat.mul(b, p), mul_comm(p, b))
82	
83	def mul_add_right(+a: Nat, +b: Nat, +c: Nat) -> {Nat.mul(Nat.add(a, b), c) == Nat.add(Nat.mul(a, c), Nat.mul(b, c)) : Nat}:
84	  match a:
85	    case 0n:
86	      {==}
87	    case 1n+p:
88	      %Equal.sym(Nat, Nat.mul(Nat.add(p, b), c), Nat.add(Nat.mul(p, c), Nat.mul(b, c)), mul_add_right(p, b, c)) : {Nat.add(c, _) == Nat.add(Nat.add(c, Nat.mul(p, c)), Nat.mul(b, c)) : Nat}
89	      Index.add_assoc(c, Nat.mul(p, c), Nat.mul(b, c))
90	
91	def mul_assoc(+a: Nat, +b: Nat, +c: Nat) -> {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, Nat.mul(b, c)) : Nat}:
92	  match a:
93	    case 0n:
94	      {==}
95	    case 1n+p:
96	      %Equal.sym(Nat, Nat.mul(Nat.add(b, Nat.mul(p, b)), c), Nat.add(Nat.mul(b, c), Nat.mul(Nat.mul(p, b), c)), mul_add_right(b, Nat.mul(p, b), c)) : {_ == Nat.mul(1n+p, Nat.mul(b, c)) : Nat}
97	      %Equal.sym(Nat, Nat.mul(Nat.mul(p, b), c), Nat.mul(p, Nat.mul(b, c)), mul_assoc(p, b, c)) : {Nat.add(Nat.mul(b, c), _) == Nat.mul(1n+p, Nat.mul(b, c)) : Nat}
98	      {==}
99	
100	def lt_zero(+a: Nat, bound: Shape.LT(a, 0n)) -> Empty:
101	  match a:
102	    case 0n:
103	      match bound:
104	    case 1n+p:
105	      match bound:
106	
107	def lt_le(+a: Nat, +b: Nat, bound: Shape.LT(a, 1n+b)) -> Shape.LE(a, b):
108	  match a b:
109	    case 0n b:
110	      Unit{}
111	    case 1n+p 0n:
112	      Empty.absurd(Empty, lt_zero(p, bound))
113	    case 1n+p 1n+q:
114	      lt_le(p, q, bound)
115	
116	def drain(+k: Nat, -n: Nat, -m: Nat, -d: Nat, +r: Nat) -> {Nat.divmod.go(Nat.add(k, n), Nat.add(k, m), d, r) == Nat.divmod.go(n, m, d, Nat.add(k, r)) : Nat & Nat}:
117	  match k:
118	    case 0n:
119	      {==}
120	    case 1n+j:
121	      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(j, n), Nat.add(j, m), d, 1n+r), Nat.divmod.go(n, m, d, Nat.add(j, 1n+r)), drain(j, n, m, d, 1n+r)) : {_ == Nat.divmod.go(n, m, d, 1n+Nat.add(j, r)) : Nat & Nat}
122	      %Broadcast.add_succ(j, r) : {Nat.divmod.go(n, m, d, _) == Nat.divmod.go(n, m, d, 1n+Nat.add(j, r)) : Nat & Nat}
123	      {==}
124	
125	def remainder(+r: Nat, +m: Nat, -d: Nat, +a: Nat, bound: Shape.LE(r, m)) -> {Nat.divmod.go(r, m, d, a) == (d, Nat.add(r, a)) : Nat & Nat}:
126	  match r m:
127	    case 0n m:
128	      {==}
129	    case 1n+p 0n:
130	      match bound:
131	    case 1n+p 1n+q:
132	      %Equal.sym(Nat & Nat, Nat.divmod.go(p, q, d, 1n+a), (d, Nat.add(p, 1n+a)), remainder(p, q, d, 1n+a, bound)) : {_ == (d, 1n+Nat.add(p, a)) : Nat & Nat}
133	      %Broadcast.add_succ(p, a) : {(d, _) == (d, 1n+Nat.add(p, a)) : Nat & Nat}
134	      {==}
135	
136	def periods(+q: Nat, +b: Nat, +r: Nat, +d: Nat, bound: Shape.LE(r, b)) -> {Nat.divmod.go(Nat.add(Nat.mul(q, 1n+b), r), b, d, 0n) == (Nat.add(q, d), r) : Nat & Nat}:
137	  match q:
138	    case 0n:
139	      %Equal.sym(Nat & Nat, Nat.divmod.go(r, b, d, 0n), (d, Nat.add(r, 0n)), remainder(r, b, d, 0n, bound)) : {_ == (d, r) : Nat & Nat}
140	      %Equal.sym(Nat, Nat.add(r, 0n), r, Broadcast.add_zero(r)) : {(d, _) == (d, r) : Nat & Nat}
141	      {==}
142	    case 1n+p:
143	      +rest = Nat.add(Nat.mul(p, 1n+b), r)
144	      %Index.add_assoc(b, Nat.mul(p, 1n+b), r) : {Nat.divmod.go(1n+_, b, d, 0n) == (1n+Nat.add(p, d), r) : Nat & Nat}
145	      %Equal.sym(Nat, 1n+Nat.add(b, rest), Nat.add(b, 1n+rest), Broadcast.add_succ(b, rest)) : {Nat.divmod.go(_, b, d, 0n) == (1n+Nat.add(p, d), r) : Nat & Nat}
146	      %Broadcast.add_zero(b) : {Nat.divmod.go(Nat.add(b, 1n+rest), _, d, 0n) == (1n+Nat.add(p, d), r) : Nat & Nat}
147	      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(b, 1n+rest), Nat.add(b, 0n), d, 0n), Nat.divmod.go(1n+rest, 0n, d, Nat.add(b, 0n)), drain(b, 1n+rest, 0n, d, 0n)) : {_ == (1n+Nat.add(p, d), r) : Nat & Nat}
148	      %Equal.sym(Nat, Nat.add(b, 0n), b, Broadcast.add_zero(b)) : {Nat.divmod.go(1n+rest, 0n, d, _) == (1n+Nat.add(p, d), r) : Nat & Nat}
149	      %Equal.sym(Nat & Nat, Nat.divmod.go(rest, b, 1n+d, 0n), (Nat.add(p, 1n+d), r), periods(p, b, r, 1n+d, bound)) : {_ == (1n+Nat.add(p, d), r) : Nat & Nat}
150	      %Broadcast.add_succ(p, d) : {(_, r) == (1n+Nat.add(p, d), r) : Nat & Nat}
151	      {==}
152	
153	def divmod_exact(+q: Nat, +b: Nat, +r: Nat, bound: Shape.LT(r, b)) -> {(q, r) == Nat.divmod(Nat.add(Nat.mul(q, b), r), b) : Nat & Nat}:
154	  match b:
155	    case 0n:
156	      Empty.absurd({(q, r) == Nat.divmod(Nat.add(Nat.mul(q, 0n), r), 0n) : Nat & Nat}, lt_zero(r, bound))
157	    case 1n+p:
158	      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(Nat.mul(q, 1n+p), r), p, 0n, 0n), (Nat.add(q, 0n), r), periods(q, p, r, 0n, lt_le(r, p, bound))) : {(q, r) == _ : Nat & Nat}
159	      %Equal.sym(Nat, Nat.add(q, 0n), q, Broadcast.add_zero(q)) : {(q, r) == (_, r) : Nat & Nat}
160	      {==}