proofs/lib/lemmas/proofs/map_difference_order.bend
bend-collections-laws-containers@1.0.0.0 · 117 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as Logic
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_index.bend as Index
4
5law add_zero:
6 for n: Nat
7 {Nat.add(n, 0n) == n : Nat}
8def 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
13law add_commute:
14 for a: Nat
15 for +b: Nat
16 {Nat.add(a, b) == Nat.add(b, a) : Nat}
17def 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
23law 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}
30def 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
38law 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}
44def 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
52law 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}
57def 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
66law 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}
71def 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
81law 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}
86def 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
93def 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
96law lift_split:
97 for +limit: Nat
98 for +offset: Nat
99 for split: Split(limit, offset)
100 Split(1n+limit, 1n+offset)
101def 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
107law split_offset:
108 for limit: Nat
109 for offset: Nat
110 Split(limit, offset)
111def 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))