proofs/lib/order.bend
bend-collections-laws-containers@1.0.0.0 · 238 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/lib/order.bend as SO
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/string_compare.bend as NM
7
8# Total-order laws for a static comparator ~cmp : A -> A -> Cmp, and their
9# checked U32 (U32.cmp) and String (String.order) instances.
10# flip: cmp(b, a) = flip(cmp(a, b))
11# antisym: cmp(a, b) = EQ implies a == b
12# trans: a <= b and b <= c implies a <= c (<= is cmp in {LT, EQ})
13
14def flipc(c: Cmp) -> Cmp:
15 SO.flipc(c)
16
17def lec(c: Cmp) -> Bool:
18 Cmp.is_le(c)
19
20# the laws are stated in spec/lib/order.bend
21def Order(~A: Data, ~cmp: A -> A -> Cmp) -> Type:
22 SO.Order(~A, ~cmp)
23
24def flip(~A: Data, ~cmp: A -> A -> Cmp, o: Order(~A, ~cmp), +a: A, +b: A) -> {cmp(b, a) == flipc(cmp(a, b)) : Cmp}:
25 match o:
26 case Tuple{f, r}:
27 f(a, b)
28
29def antisym(~A: Data, ~cmp: A -> A -> Cmp, o: Order(~A, ~cmp), +a: A, +b: A, +e: {cmp(a, b) == EQ{} : Cmp}) -> {a == b : A}:
30 match o:
31 case Tuple{f, Tuple{s, t}}:
32 s(a, b, e)
33
34def trans(~A: Data, ~cmp: A -> A -> Cmp, o: Order(~A, ~cmp), +a: A, +b: A, +c: A, +ab: {Cmp.is_le(cmp(a, b)) == True{} : Bool}, +bc: {Cmp.is_le(cmp(b, c)) == True{} : Bool}) -> {Cmp.is_le(cmp(a, c)) == True{} : Bool}:
35 match o:
36 case Tuple{f, Tuple{s, t}}:
37 t(a, b, c, ab, bc)
38
39# ---- consequences ----
40
41def self_flip(+c: Cmp, +e: {c == flipc(c) : Cmp}) -> {c == EQ{} : Cmp}:
42 match c:
43 case LT{}:
44 Empty.absurd({LT{} == EQ{} : Cmp}, L.cmp_lt_gt(e))
45 case EQ{}:
46 {==}
47 case GT{}:
48 Empty.absurd({GT{} == EQ{} : Cmp}, L.cmp_lt_gt(Equal.sym(Cmp, GT{}, LT{}, e)))
49
50def refl(~A: Data, ~cmp: A -> A -> Cmp, ~o: Order(~A, ~cmp), +a: A) -> {cmp(a, a) == EQ{} : Cmp}:
51 self_flip(cmp(a, a), flip(~A, ~cmp, o, a, a))
52
53def le_refl(~A: Data, ~cmp: A -> A -> Cmp, ~o: Order(~A, ~cmp), +a: A) -> {Cmp.is_le(cmp(a, a)) == True{} : Bool}:
54 %Equal.sym(Cmp, cmp(a, a), EQ{}, refl(~A, ~cmp, ~o, a)) : {Cmp.is_le(_) == True{} : Bool}
55 {==}
56
57def not_le_flip(+c: Cmp, +e: {Cmp.is_le(c) == False{} : Bool}) -> {Cmp.is_le(flipc(c)) == True{} : Bool}:
58 match c:
59 case LT{}:
60 Empty.absurd({Cmp.is_le(flipc(LT{})) == True{} : Bool}, L.true_false(e))
61 case EQ{}:
62 Empty.absurd({Cmp.is_le(flipc(EQ{})) == True{} : Bool}, L.true_false(e))
63 case GT{}:
64 {==}
65
66# Totality: not a <= b gives b <= a.
67def total(~A: Data, ~cmp: A -> A -> Cmp, ~o: Order(~A, ~cmp), +a: A, +b: A, +e: {Cmp.is_le(cmp(a, b)) == False{} : Bool}) -> {Cmp.is_le(cmp(b, a)) == True{} : Bool}:
68 %Equal.sym(Cmp, cmp(b, a), flipc(cmp(a, b)), flip(~A, ~cmp, o, a, b)) : {Cmp.is_le(_) == True{} : Bool}
69 not_le_flip(cmp(a, b), e)
70
71def both_le_eq(+c: Cmp, +e1: {Cmp.is_le(c) == True{} : Bool}, +e2: {Cmp.is_le(flipc(c)) == True{} : Bool}) -> {c == EQ{} : Cmp}:
72 match c:
73 case LT{}:
74 Empty.absurd({LT{} == EQ{} : Cmp}, L.false_true(e2))
75 case EQ{}:
76 {==}
77 case GT{}:
78 Empty.absurd({GT{} == EQ{} : Cmp}, L.false_true(e1))
79
80def le_antisym(~A: Data, ~cmp: A -> A -> Cmp, ~o: Order(~A, ~cmp), +a: A, +b: A, +ab: {Cmp.is_le(cmp(a, b)) == True{} : Bool}, +ba: {Cmp.is_le(cmp(b, a)) == True{} : Bool}) -> {a == b : A}:
81 antisym(~A, ~cmp, o, a, b, both_le_eq(cmp(a, b), ab, L.subst(Cmp, c => {Cmp.is_le(c) == True{} : Bool}, cmp(b, a), flipc(cmp(a, b)), flip(~A, ~cmp, o, a, b), ba)))
82
83# ---- Nat comparison ----
84
85def nat_flip(+a: Nat, +b: Nat) -> {Nat.cmp(b, a) == flipc(Nat.cmp(a, b)) : Cmp}:
86 match a b:
87 case 0n 0n:
88 {==}
89 case 0n 1n+q:
90 {==}
91 case 1n+p 0n:
92 {==}
93 case 1n+p 1n+q:
94 nat_flip(p, q)
95
96def nat_eq(+a: Nat, +b: Nat, +e: {Nat.cmp(a, b) == EQ{} : Cmp}) -> {a == b : Nat}:
97 N.eq_from_is_eq(a, b, L.subst(Cmp, c => {Cmp.is_eq(c) == True{} : Bool}, EQ{}, Nat.cmp(a, b), Equal.sym(Cmp, Nat.cmp(a, b), EQ{}, e), {==}))
98
99# ---- U32 instance ----
100
101def u32_flip(+a: U32, +b: U32) -> {U32.cmp(b, a) == flipc(U32.cmp(a, b)) : Cmp}:
102 %Equal.sym(Cmp, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), U.u32_cmp(a, b)) : {U32.cmp(b, a) == flipc(_) : Cmp}
103 %Equal.sym(Cmp, U32.cmp(b, a), Nat.cmp(U32.to_nat(b), U32.to_nat(a)), U.u32_cmp(b, a)) : {_ == flipc(Nat.cmp(U32.to_nat(a), U32.to_nat(b))) : Cmp}
104 nat_flip(U32.to_nat(a), U32.to_nat(b))
105
106def u32_antisym(+a: U32, +b: U32, +e: {U32.cmp(a, b) == EQ{} : Cmp}) -> {a == b : U32}:
107 U.injective(a, b, nat_eq(U32.to_nat(a), U32.to_nat(b), Equal.trans(Cmp, Nat.cmp(U32.to_nat(a), U32.to_nat(b)), U32.cmp(a, b), EQ{}, Equal.sym(Cmp, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), U.u32_cmp(a, b)), e)))
108
109def u32_trans(+a: U32, +b: U32, +c: U32, +ab: {Cmp.is_le(U32.cmp(a, b)) == True{} : Bool}, +bc: {Cmp.is_le(U32.cmp(b, c)) == True{} : Bool}) -> {Cmp.is_le(U32.cmp(a, c)) == True{} : Bool}:
110 %Equal.sym(Cmp, U32.cmp(a, c), Nat.cmp(U32.to_nat(a), U32.to_nat(c)), U.u32_cmp(a, c)) : {Cmp.is_le(_) == True{} : Bool}
111 N.le_trans(U32.to_nat(a), U32.to_nat(b), U32.to_nat(c),
112 L.subst(Cmp, x => {Cmp.is_le(x) == True{} : Bool}, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), U.u32_cmp(a, b), ab),
113 L.subst(Cmp, x => {Cmp.is_le(x) == True{} : Bool}, U32.cmp(b, c), Nat.cmp(U32.to_nat(b), U32.to_nat(c)), U.u32_cmp(b, c), bc))
114
115def u32_order() -> Order(~U32, ~U32.cmp):
116 (u32_flip, (u32_antisym, u32_trans))
117
118def nat_trans(+a: Nat, +b: Nat, +c: Nat, +ab: {Cmp.is_le(Nat.cmp(a, b)) == True{} : Bool}, +bc: {Cmp.is_le(Nat.cmp(b, c)) == True{} : Bool}) -> {Cmp.is_le(Nat.cmp(a, c)) == True{} : Bool}:
119 N.le_trans(a, b, c, ab, bc)
120
121def nat_order() -> Order(~Nat, ~Nat.cmp):
122 (nat_flip, (nat_eq, nat_trans))
123
124# ---- String instance (String.order, lexicographic on character codes) ----
125
126def lex(c: Cmp, r: Cmp) -> Cmp:
127 match c:
128 case LT{}:
129 LT{}
130 case EQ{}:
131 r
132 case GT{}:
133 GT{}
134
135def order_tag(+a: String, +b: String) -> {String.order(a, b) == NM.comparison_tag(String, String.cmp(a, b)) : Cmp}:
136 %Equal.sym((String & String) & Cmp, String.cmp(a, b), ((a, b), NM.comparison_tag(String, String.cmp(a, b))), NM.string_comparison_shape(a, b)) : {Pair.snd(String & String, Cmp, _) == NM.comparison_tag(String, _) : Cmp}
137 {==}
138
139def so_cons_c(+x: U32, +t1: String, +y: U32, +t2: String, +c: Cmp, +ec: {U32.cmp(x, y) == c : Cmp}) -> {String.order(SCon{Chr{x}, t1}, SCon{Chr{y}, t2}) == lex(c, String.order(t1, t2)) : Cmp}:
140 match c:
141 case LT{}:
142 %Equal.sym(Cmp, U32.cmp(x, y), LT{}, ec) : {Pair.snd(String & String, Cmp, String.cmp.fin(t1, t2, ((Chr{x}, Chr{y}), _))) == LT{} : Cmp}
143 {==}
144 case GT{}:
145 %Equal.sym(Cmp, U32.cmp(x, y), GT{}, ec) : {Pair.snd(String & String, Cmp, String.cmp.fin(t1, t2, ((Chr{x}, Chr{y}), _))) == GT{} : Cmp}
146 {==}
147 case EQ{}:
148 %Equal.sym(Cmp, U32.cmp(x, y), EQ{}, ec) : {Pair.snd(String & String, Cmp, String.cmp.fin(t1, t2, ((Chr{x}, Chr{y}), _))) == String.order(t1, t2) : Cmp}
149 %Equal.sym((String & String) & Cmp, String.cmp(t1, t2), ((t1, t2), NM.comparison_tag(String, String.cmp(t1, t2))), NM.string_comparison_shape(t1, t2)) : {Pair.snd(String & String, Cmp, String.cmp.rec(Chr{x}, Chr{y}, _)) == Pair.snd(String & String, Cmp, _) : Cmp}
150 {==}
151
152def so_cons(+x: U32, +t1: String, +y: U32, +t2: String) -> {String.order(SCon{Chr{x}, t1}, SCon{Chr{y}, t2}) == lex(U32.cmp(x, y), String.order(t1, t2)) : Cmp}:
153 so_cons_c(x, t1, y, t2, U32.cmp(x, y), {==})
154
155def flip_lex(+c: Cmp, +r: Cmp) -> {lex(flipc(c), flipc(r)) == flipc(lex(c, r)) : Cmp}:
156 match c:
157 case LT{}:
158 {==}
159 case EQ{}:
160 {==}
161 case GT{}:
162 {==}
163
164def s_flip(+a: String, +b: String) -> {String.order(b, a) == flipc(String.order(a, b)) : Cmp}:
165 match a b:
166 case SNil{} SNil{}:
167 {==}
168 case SNil{} SCon{h, t}:
169 {==}
170 case SCon{h, t} SNil{}:
171 {==}
172 case SCon{Chr{+x}, +t1} SCon{Chr{+y}, +t2}:
173 %Equal.sym(Cmp, String.order(SCon{Chr{y}, t2}, SCon{Chr{x}, t1}), lex(U32.cmp(y, x), String.order(t2, t1)), so_cons(y, t2, x, t1)) : {_ == flipc(String.order(SCon{Chr{x}, t1}, SCon{Chr{y}, t2})) : Cmp}
174 %Equal.sym(Cmp, String.order(SCon{Chr{x}, t1}, SCon{Chr{y}, t2}), lex(U32.cmp(x, y), String.order(t1, t2)), so_cons(x, t1, y, t2)) : {lex(U32.cmp(y, x), String.order(t2, t1)) == flipc(_) : Cmp}
175 %Equal.sym(Cmp, U32.cmp(y, x), flipc(U32.cmp(x, y)), u32_flip(x, y)) : {lex(_, String.order(t2, t1)) == flipc(lex(U32.cmp(x, y), String.order(t1, t2))) : Cmp}
176 %Equal.sym(Cmp, String.order(t2, t1), flipc(String.order(t1, t2)), s_flip(t1, t2)) : {lex(flipc(U32.cmp(x, y)), _) == flipc(lex(U32.cmp(x, y), String.order(t1, t2))) : Cmp}
177 flip_lex(U32.cmp(x, y), String.order(t1, t2))
178
179def s_antisym(+a: String, +b: String, +e: {String.order(a, b) == EQ{} : Cmp}) -> {a == b : String}:
180 NM.string_equal_from_comparison(a, b, Equal.trans(Cmp, NM.comparison_tag(String, String.cmp(a, b)), String.order(a, b), EQ{}, Equal.sym(Cmp, String.order(a, b), NM.comparison_tag(String, String.cmp(a, b)), order_tag(a, b)), e))
181
182def lt_is(+c: Cmp, +e: {Cmp.is_lt(c) == True{} : Bool}) -> {c == LT{} : Cmp}:
183 match c:
184 case LT{}:
185 {==}
186 case EQ{}:
187 Empty.absurd({EQ{} == LT{} : Cmp}, L.false_true(e))
188 case GT{}:
189 Empty.absurd({GT{} == LT{} : Cmp}, L.false_true(e))
190
191def u32_lt_le(+x: U32, +y: U32, +z: U32, +xy: {U32.cmp(x, y) == LT{} : Cmp}, +yz: {Cmp.is_le(U32.cmp(y, z)) == True{} : Bool}) -> {U32.cmp(x, z) == LT{} : Cmp}:
192 lt_is(U32.cmp(x, z),
193 L.subst(Cmp, k => {Cmp.is_lt(k) == True{} : Bool}, Nat.cmp(U32.to_nat(x), U32.to_nat(z)), U32.cmp(x, z), Equal.sym(Cmp, U32.cmp(x, z), Nat.cmp(U32.to_nat(x), U32.to_nat(z)), U.u32_cmp(x, z)),
194 N.lt_le_trans(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z),
195 L.subst(Cmp, k => {Cmp.is_lt(k) == True{} : Bool}, LT{}, Nat.cmp(U32.to_nat(x), U32.to_nat(y)), Equal.trans(Cmp, LT{}, U32.cmp(x, y), Nat.cmp(U32.to_nat(x), U32.to_nat(y)), Equal.sym(Cmp, U32.cmp(x, y), LT{}, xy), U.u32_cmp(x, y)), {==}),
196 L.subst(Cmp, k => {Cmp.is_le(k) == True{} : Bool}, U32.cmp(y, z), Nat.cmp(U32.to_nat(y), U32.to_nat(z)), U.u32_cmp(y, z), yz))))
197
198# The head-character case of transitivity, given the tails' statement.
199def s_trans_heads(+x: U32, +y: U32, +z: U32, +o12: Cmp, +o23: Cmp, +o13: Cmp, +cxy: Cmp, +exy: {U32.cmp(x, y) == cxy : Cmp}, +cyz: Cmp, +eyz: {U32.cmp(y, z) == cyz : Cmp}, +ab: {Cmp.is_le(lex(cxy, o12)) == True{} : Bool}, +bc: {Cmp.is_le(lex(cyz, o23)) == True{} : Bool}, ih: @+ab2: {Cmp.is_le(o12) == True{} : Bool} -> @+bc2: {Cmp.is_le(o23) == True{} : Bool} -> {Cmp.is_le(o13) == True{} : Bool}) -> {Cmp.is_le(lex(U32.cmp(x, z), o13)) == True{} : Bool}:
200 match cxy cyz:
201 case GT{} _:
202 Empty.absurd({Cmp.is_le(lex(U32.cmp(x, z), o13)) == True{} : Bool}, L.false_true(ab))
203 case _ GT{}:
204 Empty.absurd({Cmp.is_le(lex(U32.cmp(x, z), o13)) == True{} : Bool}, L.false_true(bc))
205 case LT{} LT{}:
206 %Equal.sym(Cmp, U32.cmp(x, z), LT{}, u32_lt_le(x, y, z, exy, L.subst(Cmp, k => {Cmp.is_le(k) == True{} : Bool}, LT{}, U32.cmp(y, z), Equal.sym(Cmp, U32.cmp(y, z), LT{}, eyz), {==}))) : {Cmp.is_le(lex(_, o13)) == True{} : Bool}
207 {==}
208 case LT{} EQ{}:
209 %Equal.sym(Cmp, U32.cmp(x, z), LT{}, u32_lt_le(x, y, z, exy, L.subst(Cmp, k => {Cmp.is_le(k) == True{} : Bool}, EQ{}, U32.cmp(y, z), Equal.sym(Cmp, U32.cmp(y, z), EQ{}, eyz), {==}))) : {Cmp.is_le(lex(_, o13)) == True{} : Bool}
210 {==}
211 case EQ{} LT{}:
212 %Equal.sym(U32, x, y, u32_antisym(x, y, exy)) : {Cmp.is_le(lex(U32.cmp(_, z), o13)) == True{} : Bool}
213 %Equal.sym(Cmp, U32.cmp(y, z), LT{}, eyz) : {Cmp.is_le(lex(_, o13)) == True{} : Bool}
214 {==}
215 case EQ{} EQ{}:
216 %Equal.sym(U32, x, y, u32_antisym(x, y, exy)) : {Cmp.is_le(lex(U32.cmp(_, z), o13)) == True{} : Bool}
217 %Equal.sym(Cmp, U32.cmp(y, z), EQ{}, eyz) : {Cmp.is_le(lex(_, o13)) == True{} : Bool}
218 ih(ab, bc)
219
220def s_trans(+a: String, +b: String, +c: String, +ab: {Cmp.is_le(String.order(a, b)) == True{} : Bool}, +bc: {Cmp.is_le(String.order(b, c)) == True{} : Bool}) -> {Cmp.is_le(String.order(a, c)) == True{} : Bool}:
221 match a b c:
222 case SNil{} _ SNil{}:
223 {==}
224 case SNil{} _ SCon{h, t}:
225 {==}
226 case SCon{h, t} SNil{} _:
227 Empty.absurd({Cmp.is_le(String.order(SCon{h, t}, c)) == True{} : Bool}, L.false_true(ab))
228 case SCon{h1, t1} SCon{h2, t2} SNil{}:
229 Empty.absurd({Cmp.is_le(String.order(SCon{h1, t1}, SNil{})) == True{} : Bool}, L.false_true(bc))
230 case SCon{Chr{+x}, +t1} SCon{Chr{+y}, +t2} SCon{Chr{+z}, +t3}:
231 %Equal.sym(Cmp, String.order(SCon{Chr{x}, t1}, SCon{Chr{z}, t3}), lex(U32.cmp(x, z), String.order(t1, t3)), so_cons(x, t1, z, t3)) : {Cmp.is_le(_) == True{} : Bool}
232 s_trans_heads(x, y, z, String.order(t1, t2), String.order(t2, t3), String.order(t1, t3), U32.cmp(x, y), {==}, U32.cmp(y, z), {==},
233 L.subst(Cmp, k => {Cmp.is_le(k) == True{} : Bool}, String.order(SCon{Chr{x}, t1}, SCon{Chr{y}, t2}), lex(U32.cmp(x, y), String.order(t1, t2)), so_cons(x, t1, y, t2), ab),
234 L.subst(Cmp, k => {Cmp.is_le(k) == True{} : Bool}, String.order(SCon{Chr{y}, t2}, SCon{Chr{z}, t3}), lex(U32.cmp(y, z), String.order(t2, t3)), so_cons(y, t2, z, t3), bc),
235 ab2 => bc2 => s_trans(t1, t2, t3, ab2, bc2))
236
237def string_order() -> Order(~String, ~String.order):
238 (s_flip, (s_antisym, s_trans))