proofs/containers/intrusive_doubly_linked_list/shape.bend
bend-collections-laws-containers@1.0.0.0 · 243 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/model.bend as G
3
4
5# The graph is a proof shadow. These are pointwise map laws, proved here,
6# not postconditions assumed of the list operation.
7
8def next_sn(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +x: N) -> {G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x) == G.choose(~Maybe<&2,N>,eq(n,x),v,G.next(~N, ~R, ~P, ~eq,g,x)) : Maybe<&2,N>}:
9 match g:
10 case G.Graph{ns,ps,rs,f}: {==}
11
12def prev_sn(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +x: N) -> {G.prev(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x) == G.prev(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}:
13 match g:
14 case G.Graph{ns,ps,rs,f}: {==}
15
16def next_sp(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +x: N) -> {G.next(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),x) == G.next(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}:
17 match g:
18 case G.Graph{ns,ps,rs,f}: {==}
19
20def prev_sp(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +x: N) -> {G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),x) == G.choose(~Maybe<&2,N>,eq(n,x),v,G.prev(~N, ~R, ~P, ~eq,g,x)) : Maybe<&2,N>}:
21 match g:
22 case G.Graph{ns,ps,rs,f}: {==}
23
24def next_sh(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +v: Maybe<&2,N>, +x: N) -> {G.next(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,g,r,v),x) == G.next(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}:
25 match g:
26 case G.Graph{ns,ps,rs,f}: {==}
27
28def prev_sh(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +v: Maybe<&2,N>, +x: N) -> {G.prev(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,g,r,v),x) == G.prev(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}:
29 match g:
30 case G.Graph{ns,ps,rs,f}: {==}
31
32def next_sn_other(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +x: N, neq: {eq(n,x) == False{} : Bool}) -> {G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x) == G.next(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}:
33 %Equal.sym(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x),G.choose(~Maybe<&2,N>,eq(n,x),v,G.next(~N, ~R, ~P, ~eq,g,x)),next_sn(~N, ~R, ~P, ~eq,g,n,v,x)) : {_ == G.next(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}
34 %Equal.sym(Bool,eq(n,x),False{},neq) : {G.choose(~Maybe<&2,N>,_,v,G.next(~N, ~R, ~P, ~eq,g,x)) == G.next(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}
35 {==}
36
37def prev_sp_other(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +x: N, neq: {eq(n,x) == False{} : Bool}) -> {G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),x) == G.prev(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}:
38 %Equal.sym(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),x),G.choose(~Maybe<&2,N>,eq(n,x),v,G.prev(~N, ~R, ~P, ~eq,g,x)),prev_sp(~N, ~R, ~P, ~eq,g,n,v,x)) : {_ == G.prev(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}
39 %Equal.sym(Bool,eq(n,x),False{},neq) : {G.choose(~Maybe<&2,N>,_,v,G.prev(~N, ~R, ~P, ~eq,g,x)) == G.prev(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}
40 {==}
41
42def next_sn_self(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, same: {eq(n,n) == True{} : Bool}) -> {G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),n) == v : Maybe<&2,N>}:
43 %Equal.sym(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),n),G.choose(~Maybe<&2,N>,eq(n,n),v,G.next(~N, ~R, ~P, ~eq,g,n)),next_sn(~N, ~R, ~P, ~eq,g,n,v,n)) : {_ == v : Maybe<&2,N>}
44 %Equal.sym(Bool,eq(n,n),True{},same) : {G.choose(~Maybe<&2,N>,_,v,G.next(~N, ~R, ~P, ~eq,g,n)) == v : Maybe<&2,N>}
45 {==}
46
47def prev_sp_self(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, same: {eq(n,n) == True{} : Bool}) -> {G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),n) == v : Maybe<&2,N>}:
48 %Equal.sym(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),n),G.choose(~Maybe<&2,N>,eq(n,n),v,G.prev(~N, ~R, ~P, ~eq,g,n)),prev_sp(~N, ~R, ~P, ~eq,g,n,v,n)) : {_ == v : Maybe<&2,N>}
49 %Equal.sym(Bool,eq(n,n),True{},same) : {G.choose(~Maybe<&2,N>,_,v,G.prev(~N, ~R, ~P, ~eq,g,n)) == v : Maybe<&2,N>}
50 {==}
51
52def segment_sn_frame(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +xs: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, away: G.away(~N,~eq,n,xs), good: G.segment(~N, ~R, ~P, ~eq,g,p,xs,q)) -> G.segment(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),p,xs,q):
53 match xs away good:
54 case Nil{} _ _: Unit{}
55 case Con{+x,+rest} Tuple{Tuple{neq,rev},ar} Tuple{hp,Tuple{hn,ht}}:
56 (Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x),G.prev(~N, ~R, ~P, ~eq,g,x),p,prev_sn(~N, ~R, ~P, ~eq,g,n,v,x),hp),
57 (Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x),G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,rest,q),next_sn_other(~N, ~R, ~P, ~eq,g,n,v,x,neq),hn),
58 segment_sn_frame(~N, ~R, ~P, ~eq,g,n,v,rest,Some{x},q,ar,ht)))
59
60def segment_sp_frame(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +xs: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, away: G.away(~N,~eq,n,xs), good: G.segment(~N, ~R, ~P, ~eq,g,p,xs,q)) -> G.segment(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),p,xs,q):
61 match xs away good:
62 case Nil{} _ _: Unit{}
63 case Con{+x,+rest} Tuple{Tuple{neq,rev},ar} Tuple{hp,Tuple{hn,ht}}:
64 (Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),x),G.prev(~N, ~R, ~P, ~eq,g,x),p,prev_sp_other(~N, ~R, ~P, ~eq,g,n,v,x,neq),hp),
65 (Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),x),G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,rest,q),next_sp(~N, ~R, ~P, ~eq,g,n,v,x),hn),
66 segment_sp_frame(~N, ~R, ~P, ~eq,g,n,v,rest,Some{x},q,ar,ht)))
67
68def segment_sh_frame(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +v: Maybe<&2,N>, +xs: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, good: G.segment(~N, ~R, ~P, ~eq,g,p,xs,q)) -> G.segment(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,g,r,v),p,xs,q):
69 match xs good:
70 case Nil{} _: Unit{}
71 case Con{+x,+rest} Tuple{hp,Tuple{hn,ht}}:
72 (Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,g,r,v),x),G.prev(~N, ~R, ~P, ~eq,g,x),p,prev_sh(~N, ~R, ~P, ~eq,g,r,v,x),hp),
73 (Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,g,r,v),x),G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,rest,q),next_sh(~N, ~R, ~P, ~eq,g,r,v,x),hn),
74 segment_sh_frame(~N, ~R, ~P, ~eq,g,r,v,rest,Some{x},q,ht)))
75
76# Changing a segment's first predecessor preserves its entire suffix.
77def segment_first_prev(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +x: N, +rest: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, +v: Maybe<&2,N>, same: {eq(x,x) == True{} : Bool}, away: G.away(~N,~eq,x,rest), good: G.segment(~N, ~R, ~P, ~eq,g,p,Con{x,rest},q)) -> G.segment(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,x,v),v,Con{x,rest},q):
78 match good:
79 case Tuple{hp,Tuple{hn,ht}}:
80 (prev_sp_self(~N, ~R, ~P, ~eq,g,x,v,same),
81 (Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,x,v),x),G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,rest,q),next_sp(~N, ~R, ~P, ~eq,g,x,v,x),hn),
82 segment_sp_frame(~N, ~R, ~P, ~eq,g,x,v,rest,Some{x},q,away,ht)))
83
84def away_at(~N: Data, ~eq: N -> N -> Bool, +prefix: List<&2,N>, +n: N, +suffix: List<&2,N>, +x: N, h: G.away(~N,~eq,x,G.append(~N,prefix,Con{n,suffix}))) -> G.both({eq(x,n) == False{} : Bool}, {eq(n,x) == False{} : Bool}):
85 match prefix h:
86 case Nil{} Tuple{hn,ht}: hn
87 case Con{a,rest} Tuple{ha,ht}: away_at(~N,~eq,rest,n,suffix,x,ht)
88
89def away_delete(~N: Data, ~eq: N -> N -> Bool, +prefix: List<&2,N>, +n: N, +suffix: List<&2,N>, +x: N, h: G.away(~N,~eq,x,G.append(~N,prefix,Con{n,suffix}))) -> G.away(~N,~eq,x,G.append(~N,prefix,suffix)):
90 match prefix h:
91 case Nil{} Tuple{hn,ht}: ht
92 case Con{a,rest} Tuple{ha,ht}: (ha,away_delete(~N,~eq,rest,n,suffix,x,ht))
93
94def unique_delete(~N: Data, ~eq: N -> N -> Bool, +prefix: List<&2,N>, +n: N, +suffix: List<&2,N>, h: G.unique(~N,~eq,G.append(~N,prefix,Con{n,suffix}))) -> G.unique(~N,~eq,G.append(~N,prefix,suffix)):
95 match prefix h:
96 case Nil{} Tuple{hn,ht}: ht
97 case Con{+a,+rest} Tuple{ha,ht}: (away_delete(~N,~eq,rest,n,suffix,a,ha),unique_delete(~N,~eq,rest,n,suffix,ht))
98
99def swapped(~N: Data, ~eq: N -> N -> Bool, +a: N, +b: N, h: G.both({eq(a,b) == False{} : Bool}, {eq(b,a) == False{} : Bool})) -> G.both({eq(b,a) == False{} : Bool}, {eq(a,b) == False{} : Bool}):
100 match h:
101 case Tuple{ab,ba}: (ba,ab)
102
103def deleted_away(~N: Data, ~eq: N -> N -> Bool, +prefix: List<&2,N>, +n: N, +suffix: List<&2,N>, h: G.unique(~N,~eq,G.append(~N,prefix,Con{n,suffix}))) -> G.away(~N,~eq,n,G.append(~N,prefix,suffix)):
104 match prefix h:
105 case Nil{} Tuple{hn,ht}: hn
106 case Con{+a,+rest} Tuple{ha,ht}: (swapped(~N,~eq,a,n,away_at(~N,~eq,rest,n,suffix,a,ha)),deleted_away(~N,~eq,rest,n,suffix,ht))
107
108def first_append(~N: Data, +a: List<&2,N>, +b: List<&2,N>, +q: Maybe<&2,N>) -> {G.first(~N,G.append(~N,a,b),q) == G.first(~N,a,G.first(~N,b,q)) : Maybe<&2,N>}:
109 match a:
110 case Nil{}: {==}
111 case Con{x,rest}: {==}
112
113def first_end(~N: Data, +a: List<&2,N>, +n: N, +q: Maybe<&2,N>, +v: Maybe<&2,N>) -> {G.first(~N,G.append(~N,a,Con{n,Nil{}}),q) == G.first(~N,G.append(~N,a,Con{n,Nil{}}),v) : Maybe<&2,N>}:
114 match a:
115 case Nil{}: {==}
116 case Con{x,rest}: {==}
117
118def segment_last_next(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +prefix: List<&2,N>, +n: N, +p: Maybe<&2,N>, +q: Maybe<&2,N>, +v: Maybe<&2,N>, +same: {eq(n,n) == True{} : Bool}, unique: G.unique(~N,~eq,G.append(~N,prefix,Con{n,Nil{}})), good: G.segment(~N, ~R, ~P, ~eq,g,p,G.append(~N,prefix,Con{n,Nil{}}),q)) -> G.segment(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),p,G.append(~N,prefix,Con{n,Nil{}}),v):
119 match prefix unique good:
120 case Nil{} _ Tuple{hp,Tuple{hn,ht}}:
121 (Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),n),G.prev(~N, ~R, ~P, ~eq,g,n),p,prev_sn(~N, ~R, ~P, ~eq,g,n,v,n),hp),(next_sn_self(~N, ~R, ~P, ~eq,g,n,v,same),Unit{}))
122 case Con{+x,+rest} Tuple{away,un} Tuple{hp,Tuple{hn,ht}}:
123 (Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x),G.prev(~N, ~R, ~P, ~eq,g,x),p,prev_sn(~N, ~R, ~P, ~eq,g,n,v,x),hp),
124 (Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x),G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,G.append(~N,rest,Con{n,Nil{}}),v),next_sn_other(~N, ~R, ~P, ~eq,g,n,v,x,G.right({eq(x,n) == False{} : Bool},{eq(n,x) == False{} : Bool},away_at(~N,~eq,rest,n,Nil{},x,away))),Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,G.append(~N,rest,Con{n,Nil{}}),q),G.first(~N,G.append(~N,rest,Con{n,Nil{}}),v),hn,first_end(~N,rest,n,q,v))),
125 segment_last_next(~N, ~R, ~P, ~eq,g,rest,n,Some{x},q,v,same,un,ht)))
126
127def segment_join(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +g: G.Graph<N,R,P>, +b: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, ga: G.segment(~N, ~R, ~P, ~eq,g,p,a,G.first(~N,b,q)), gb: G.segment(~N, ~R, ~P, ~eq,g,G.last(~N,a,p),b,q)) -> G.segment(~N, ~R, ~P, ~eq,g,p,G.append(~N,a,b),q):
128 match a ga:
129 case Nil{} _: gb
130 case Con{+x,+rest} Tuple{hp,Tuple{hn,ht}}:
131 (hp,(Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,rest,G.first(~N,b,q)),G.first(~N,G.append(~N,rest,b),q),hn,Equal.sym(Maybe<&2,N>,G.first(~N,G.append(~N,rest,b),q),G.first(~N,rest,G.first(~N,b,q)),first_append(~N,rest,b,q))),segment_join(~N, ~R, ~P, ~eq,rest,g,b,Some{x},q,ht,gb)))
132
133def away_join(~N: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +b: List<&2,N>, +n: N, ga: G.away(~N,~eq,n,a), gb: G.away(~N,~eq,n,b)) -> G.away(~N,~eq,n,G.append(~N,a,b)):
134 match a ga:
135 case Nil{} _: gb
136 case Con{x,rest} Tuple{hx,ht}: (hx,away_join(~N,~eq,rest,b,n,ht,gb))
137
138def unique_join(~N: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +b: List<&2,N>, ua: G.unique(~N,~eq,a), +ub: G.unique(~N,~eq,b), dis: G.disjoint(~N,~eq,a,b)) -> G.unique(~N,~eq,G.append(~N,a,b)):
139 match a ua dis:
140 case Nil{} _ _: ub
141 case Con{+x,+rest} Tuple{away,ut} Tuple{ab,dt}: (away_join(~N,~eq,rest,b,x,away,ab),unique_join(~N,~eq,rest,b,ut,ub,dt))
142
143def disjoint_last(~N: Data, ~eq: N -> N -> Bool, +prefix: List<&2,N>, +n: N, +suffix: List<&2,N>, dis: G.disjoint(~N,~eq,G.append(~N,prefix,Con{n,Nil{}}),suffix)) -> G.away(~N,~eq,n,suffix):
144 match prefix dis:
145 case Nil{} Tuple{a,d}: a
146 case Con{x,rest} Tuple{a,d}: disjoint_last(~N,~eq,rest,n,suffix,d)
147
148def disjoint_head(~N: Data, ~eq: N -> N -> Bool, +prefix: List<&2,N>, +n: N, +suffix: List<&2,N>, dis: G.disjoint(~N,~eq,prefix,Con{n,suffix})) -> G.away(~N,~eq,n,prefix):
149 match prefix dis:
150 case Nil{} _: Unit{}
151 case Con{+x,+rest} Tuple{Tuple{hn,ht},dt}: (swapped(~N,~eq,x,n,hn),disjoint_head(~N,~eq,rest,n,suffix,dt))
152
153def last_end(~N: Data, +a: List<&2,N>, +n: N, +p: Maybe<&2,N>) -> {G.last(~N,G.append(~N,a,Con{n,Nil{}}),p) == Some{n} : Maybe<&2,N>}:
154 match a:
155 case Nil{}: {==}
156 case Con{x,rest}: last_end(~N,rest,n,Some{x})
157
158# A prefix/suffix split is the ordinary witness for removing a known member.
159# The following lemmas extract the representation facts from the whole chain.
160def first_middle(~N: Data, +a: List<&2,N>, +n: N, +b: List<&2,N>, +q: Maybe<&2,N>) -> {G.first(~N,G.append(~N,a,Con{n,b}),q) == G.first(~N,a,Some{n}) : Maybe<&2,N>}:
161 match a:
162 case Nil{}: {==}
163 case Con{x,rest}: {==}
164
165def prefix_segment(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +g: G.Graph<N,R,P>, +n: N, +b: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, good: G.segment(~N, ~R, ~P, ~eq,g,p,G.append(~N,a,Con{n,b}),q)) -> G.segment(~N, ~R, ~P, ~eq,g,p,a,Some{n}):
166 match a good:
167 case Nil{} _: Unit{}
168 case Con{+x,+rest} Tuple{hp,Tuple{hn,ht}}:
169 (hp,(Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,G.append(~N,rest,Con{n,b}),q),G.first(~N,rest,Some{n}),hn,first_middle(~N,rest,n,b,q)),prefix_segment(~N, ~R, ~P, ~eq,rest,g,n,b,Some{x},q,ht)))
170
171def member_prev(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +g: G.Graph<N,R,P>, +n: N, +b: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, good: G.segment(~N, ~R, ~P, ~eq,g,p,G.append(~N,a,Con{n,b}),q)) -> {G.prev(~N, ~R, ~P, ~eq,g,n) == G.last(~N,a,p) : Maybe<&2,N>}:
172 match a good:
173 case Nil{} Tuple{hp,tail}: hp
174 case Con{x,rest} Tuple{hp,Tuple{hn,ht}}: member_prev(~N, ~R, ~P, ~eq,rest,g,n,b,Some{x},q,ht)
175
176def member_next(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +g: G.Graph<N,R,P>, +n: N, +b: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, good: G.segment(~N, ~R, ~P, ~eq,g,p,G.append(~N,a,Con{n,b}),q)) -> {G.next(~N, ~R, ~P, ~eq,g,n) == G.first(~N,b,q) : Maybe<&2,N>}:
177 match a good:
178 case Nil{} Tuple{hp,Tuple{hn,ht}}: hn
179 case Con{x,rest} Tuple{hp,Tuple{hn,ht}}: member_next(~N, ~R, ~P, ~eq,rest,g,n,b,Some{x},q,ht)
180
181def suffix_segment(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +g: G.Graph<N,R,P>, +n: N, +b: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, good: G.segment(~N, ~R, ~P, ~eq,g,p,G.append(~N,a,Con{n,b}),q)) -> G.segment(~N, ~R, ~P, ~eq,g,Some{n},b,q):
182 match a good:
183 case Nil{} Tuple{hp,Tuple{hn,ht}}: ht
184 case Con{x,rest} Tuple{hp,Tuple{hn,ht}}: suffix_segment(~N, ~R, ~P, ~eq,rest,g,n,b,Some{x},q,ht)
185
186def head_sn(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +r: R) -> {G.head(~N, ~R, ~P,~req,G.sn(~N, ~R, ~P,g,n,v),r) == G.head(~N, ~R, ~P,~req,g,r) : Maybe<&2,N>}:
187 match g:
188 case G.Graph{ns,ps,rs,f}: {==}
189
190def head_sp(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +r: R) -> {G.head(~N, ~R, ~P,~req,G.sp(~N, ~R, ~P,g,n,v),r) == G.head(~N, ~R, ~P,~req,g,r) : Maybe<&2,N>}:
191 match g:
192 case G.Graph{ns,ps,rs,f}: {==}
193
194def frame_sn(~N: Data, ~R: Data, ~P: Data, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>) -> {G.frame(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,v)) == G.frame(~N, ~R, ~P,g) : P}:
195 match g:
196 case G.Graph{ns,ps,rs,f}: {==}
197
198def frame_sp(~N: Data, ~R: Data, ~P: Data, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>) -> {G.frame(~N, ~R, ~P,G.sp(~N, ~R, ~P,g,n,v)) == G.frame(~N, ~R, ~P,g) : P}:
199 match g:
200 case G.Graph{ns,ps,rs,f}: {==}
201
202def frame_sh(~N: Data, ~R: Data, ~P: Data, +g: G.Graph<N,R,P>, +r: R, +v: Maybe<&2,N>) -> {G.frame(~N, ~R, ~P,G.sh(~N, ~R, ~P,g,r,v)) == G.frame(~N, ~R, ~P,g) : P}:
203 match g:
204 case G.Graph{ns,ps,rs,f}: {==}
205
206def head_sh(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +v: Maybe<&2,N>, +x: R) -> {G.head(~N, ~R, ~P,~req,G.sh(~N, ~R, ~P,g,r,v),x) == G.choose(~Maybe<&2,N>,req(r,x),v,G.head(~N, ~R, ~P,~req,g,x)) : Maybe<&2,N>}:
207 match g:
208 case G.Graph{ns,ps,rs,f}: {==}
209
210def head_sh_self(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +v: Maybe<&2,N>, same: {req(r,r) == True{} : Bool}) -> {G.head(~N, ~R, ~P,~req,G.sh(~N, ~R, ~P,g,r,v),r) == v : Maybe<&2,N>}:
211 %Equal.sym(Maybe<&2,N>,G.head(~N, ~R, ~P,~req,G.sh(~N, ~R, ~P,g,r,v),r),G.choose(~Maybe<&2,N>,req(r,r),v,G.head(~N, ~R, ~P,~req,g,r)),head_sh(~N, ~R, ~P,~req,g,r,v,r)) : {_ == v : Maybe<&2,N>}
212 %Equal.sym(Bool,req(r,r),True{},same) : {G.choose(~Maybe<&2,N>,_,v,G.head(~N, ~R, ~P,~req,g,r)) == v : Maybe<&2,N>}
213 {==}
214
215def head_sh_other(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +v: Maybe<&2,N>, +x: R, neq: {req(r,x) == False{} : Bool}) -> {G.head(~N, ~R, ~P,~req,G.sh(~N, ~R, ~P,g,r,v),x) == G.head(~N, ~R, ~P,~req,g,x) : Maybe<&2,N>}:
216 %Equal.sym(Maybe<&2,N>,G.head(~N, ~R, ~P,~req,G.sh(~N, ~R, ~P,g,r,v),x),G.choose(~Maybe<&2,N>,req(r,x),v,G.head(~N, ~R, ~P,~req,g,x)),head_sh(~N, ~R, ~P,~req,g,r,v,x)) : {_ == G.head(~N, ~R, ~P,~req,g,x) : Maybe<&2,N>}
217 %Equal.sym(Bool,req(r,x),False{},neq) : {G.choose(~Maybe<&2,N>,_,v,G.head(~N, ~R, ~P,~req,g,x)) == G.head(~N, ~R, ~P,~req,g,x) : Maybe<&2,N>}
218 {==}
219
220def away_left(~N: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +b: List<&2,N>, +n: N, h: G.away(~N,~eq,n,G.append(~N,a,b))) -> G.away(~N,~eq,n,a):
221 match a h:
222 case Nil{} _: Unit{}
223 case Con{x,rest} Tuple{hx,ht}: (hx,away_left(~N,~eq,rest,b,n,ht))
224
225def away_right(~N: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +b: List<&2,N>, +n: N, h: G.away(~N,~eq,n,G.append(~N,a,b))) -> G.away(~N,~eq,n,b):
226 match a h:
227 case Nil{} _: h
228 case Con{x,rest} Tuple{hx,ht}: away_right(~N,~eq,rest,b,n,ht)
229
230def unique_left(~N: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +b: List<&2,N>, h: G.unique(~N,~eq,G.append(~N,a,b))) -> G.unique(~N,~eq,a):
231 match a h:
232 case Nil{} _: Unit{}
233 case Con{+x,+rest} Tuple{ax,ut}: (away_left(~N,~eq,rest,b,x,ax),unique_left(~N,~eq,rest,b,ut))
234
235def unique_right(~N: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +b: List<&2,N>, h: G.unique(~N,~eq,G.append(~N,a,b))) -> G.unique(~N,~eq,b):
236 match a h:
237 case Nil{} _: h
238 case Con{x,rest} Tuple{ax,ut}: unique_right(~N,~eq,rest,b,ut)
239
240def disjoint_unique(~N: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +b: List<&2,N>, h: G.unique(~N,~eq,G.append(~N,a,b))) -> G.disjoint(~N,~eq,a,b):
241 match a h:
242 case Nil{} _: Unit{}
243 case Con{+x,+rest} Tuple{ax,ut}: (away_right(~N,~eq,rest,b,x,ax),disjoint_unique(~N,~eq,rest,b,ut))