1	import Base
2	import ./map_routing.bend as Logic
3	import ./map_index.bend as Index
4	
5	law add_zero:
6	  for n: Nat
7	  {Nat.add(n, 0n) == n : Nat}
8	def add_zero(n):
9	  match n:
10	    case 0n: {==}
11	    case 1n+p: Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, 0n), p, add_zero(p))
12	
13	law add_commute:
14	  for a: Nat
15	  for +b: Nat
16	  {Nat.add(a, b) == Nat.add(b, a) : Nat}
17	def add_commute(a, b):
18	  match a:
19	    case 0n: Equal.sym(Nat, Nat.add(b, 0n), b, add_zero(b))
20	    case 1n+ +p:
21	      Equal.trans(Nat, 1n+Nat.add(p, b), 1n+Nat.add(b, p), Nat.add(b, 1n+p), Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, b), Nat.add(b, p), add_commute(p, b)), Equal.sym(Nat, Nat.add(b, 1n+p), 1n+Nat.add(b, p), Index.add_right_successor(b, p)))
22	
23	law add_sub_bound:
24	  for n: Nat
25	  for m: Nat
26	  for +k: Nat
27	  for bound: {Nat.is_le(m, n) == True{} : Bool}
28	  for inside: {Nat.is_le(k, Nat.sub(n, m)) == True{} : Bool}
29	  {Nat.is_le(Nat.add(m, k), n) == True{} : Bool}
30	def add_sub_bound(n, m, k, bound, inside):
31	  match n m:
32	    case 0n 0n: inside
33	    case 0n 1n+p:
34	      Empty.absurd({Nat.is_le(Nat.add(1n+p, k), 0n) == True{} : Bool}, Logic.false_true(bound))
35	    case 1n+p 0n: inside
36	    case 1n+p 1n+q: add_sub_bound(p, q, k, bound, inside)
37	
38	law sub_from_add:
39	  for n: Nat
40	  for k: Nat
41	  for +m: Nat
42	  for bound: {Nat.is_le(Nat.add(k, m), n) == True{} : Bool}
43	  {Nat.is_le(m, Nat.sub(n, k)) == True{} : Bool}
44	def sub_from_add(n, k, m, bound):
45	  match n k:
46	    case 0n 0n: bound
47	    case 0n 1n+p:
48	      Empty.absurd({Nat.is_le(m, 0n) == True{} : Bool}, Logic.false_true(bound))
49	    case 1n+p 0n: bound
50	    case 1n+p 1n+q: sub_from_add(p, q, m, bound)
51	
52	law add_complement:
53	  for n: Nat
54	  for m: Nat
55	  for bound: {Nat.is_le(m, n) == True{} : Bool}
56	  {Nat.add(m, Nat.sub(n, m)) == n : Nat}
57	def add_complement(n, m, bound):
58	  match n m:
59	    case 0n 0n: {==}
60	    case 0n 1n+p:
61	      Empty.absurd({Nat.add(1n+p, 0n) == 0n : Nat}, Logic.false_true(bound))
62	    case 1n+p 0n: {==}
63	    case 1n+ +p 1n+ +q:
64	      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(q, Nat.sub(p, q)), p, add_complement(p, q, bound))
65	
66	law strict_successor:
67	  for a: Nat
68	  for b: Nat
69	  for strict: {Nat.is_lt(a, b) == True{} : Bool}
70	  {Nat.is_le(1n+a, b) == True{} : Bool}
71	def strict_successor(a, b, strict):
72	  match a b:
73	    case 0n 0n: Empty.absurd({False{} == True{} : Bool}, Logic.false_true(strict))
74	    case 0n 1n+p:
75	      match p:
76	        case 0n: {==}
77	        case 1n+q: {==}
78	    case 1n+p 0n: Empty.absurd({False{} == True{} : Bool}, Logic.false_true(strict))
79	    case 1n+p 1n+q: strict_successor(p, q, strict)
80	
81	law less_is_le:
82	  for a: Nat
83	  for b: Nat
84	  for e: {Nat.is_lt(a, b) == True{} : Bool}
85	  {Nat.is_le(a, b) == True{} : Bool}
86	def less_is_le(a, b, e):
87	  match a b:
88	    case 0n 0n: {==}
89	    case 0n 1n+p: {==}
90	    case 1n+p 0n: e
91	    case 1n+p 1n+q: less_is_le(p, q, e)
92	
93	def Split(+limit: Nat, +offset: Nat) -> Type:
94	  Either<&1, &1, {Nat.is_le(offset, limit) == True{} : Bool}, Sigma<&2, &1, Nat, rest => {offset == Nat.add(1n+limit, rest) : Nat}>>
95	
96	law lift_split:
97	  for +limit: Nat
98	  for +offset: Nat
99	  for split: Split(limit, offset)
100	  Split(1n+limit, 1n+offset)
101	def lift_split(limit, offset, split):
102	  match split:
103	    case Inl{e}: Inl{e}
104	    case Inr{Tuple{+rest, e}}:
105	      Inr{(rest, Equal.cong(Nat, Nat, x => 1n+x, offset, Nat.add(1n+limit, rest), e))}
106	
107	law split_offset:
108	  for limit: Nat
109	  for offset: Nat
110	  Split(limit, offset)
111	def split_offset(limit, offset):
112	  match limit offset:
113	    case 0n 0n: Inl{{==}}
114	    case 0n 1n+ +p: Inr{(p, {==})}
115	    case 1n+p 0n: Inl{{==}}
116	    case 1n+ +p 1n+ +q:
117	      lift_split(p, q, split_offset(p, q))