PROOF.bend

lawful-arrays@0.1.0.0 · 192 lines · 13 definitions

1import Base
2import lawful-arrays@0.1.0.0/defs.bend as D
3import lawful-arrays@0.1.0.0/LAWS.bend as L
4import lawful-arrays@0.1.0.0/proof_base.bend as B
5import lawful-arrays@0.1.0.0/proof_tree.bend as P
6import lawful-arrays@0.1.0.0/proof_shape.bend as S
7import lawful-arrays@0.1.0.0/proof_index.bend as I
8
9# Proofs of the laws: `def L.name` proves `law name` of LAWS.bend. Laws about
10# an array of Data elements go through its mirror (P.mirror): a Tree<T> t with
11# P.fromT(t) == a, about which the lemmas may say as much as they need (an
12# array, a Type, can be used only once in a proof).
13
14# Rewrites a fact about a into the same fact about the mirror.
15def full_t(-T: Data, -a: Array<T>, -t: P.Tree<T>, +d: Nat, e: {P.fromT(T, t) == a : Array<T>},
16  hf: {D.full(T, a, d) == True{} : Bool}) -> {D.full(T, P.fromT(T, t), d) == True{} : Bool}:
17  B.subst(Array<T>, x => {D.full(T, x, d) == True{} : Bool}, a, P.fromT(T, t),
18    Equal.sym(Array<T>, P.fromT(T, t), a, e), hf)
19
20# Creating
21# ========
22
23def L.new_full(T, d, v):
24  P.new_full(T, d, v)
25
26def L.new_view(T, d, v):
27  P.new_view(T, d, v)
28
29# Size
30# ====
31
32def view_length.go(-T: Data, -a: Array<T>, +d: Nat, hf: {D.full(T, a, d) == True{} : Bool},
33  m: P.Mirror(T, a)) -> {List.length(&2, T, D.view(T, a)) == Nat.pow(2n, d) : Nat}:
34  (t, +e) = m
35  %e : {List.length(&2, T, D.view(T, _)) == Nat.pow(2n, d) : Nat}
36  P.view_length(T, d, t, full_t(T, a, t, d, e, hf))
37
38def L.view_length(T, a, d, hf):
39  view_length.go(T, a, d, hf, P.mirror(T, a))
40
41def size_count.go(-T: Data, -a: Array<T>, +d: Nat, hf: {D.full(T, a, d) == True{} : Bool},
42  +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, m: P.Mirror(T, a)) ->
43  {U32.to_nat(Pair.snd(Array<T>, U32, Array.size(T, a))) == Nat.pow(2n, d) : Nat}:
44  (t, +e) = m
45  %e : {U32.to_nat(Pair.snd(Array<T>, U32, Array.size(T, _))) == Nat.pow(2n, d) : Nat}
46  I.size_count_t(T, t, d, full_t(T, a, t, d, e, hf), hd)
47
48def L.size_count(T, a, d, hf, hd):
49  size_count.go(T, a, d, hf, hd, P.mirror(T, a))
50
51def L.size_kept(T, a):
52  %Equal.sym(Array<T> & U32, Array.size(T, a), (a, Pair.snd(Array<T>, U32, Array.size(T, a))), P.size_eta(T, a)) :
53    {Pair.fst(Array<T>, U32, _) == a : Array<T>}
54  {==}
55
56def size_pair.go(-T: Data, -a: Array<T>, +d: Nat, hf: {D.full(T, a, d) == True{} : Bool},
57  m: P.Mirror(T, a)) -> {Array.size(T, a) == (a, U32.shln(1, d)) : Array<T> & U32}:
58  (t, +e) = m
59  %e : {Array.size(T, _) == (_, U32.shln(1, d)) : Array<T> & U32}
60  P.size_tree(T, d, t, full_t(T, a, t, d, e, hf))
61
62def L.size_pair(T, a, d, hf):
63  size_pair.go(T, a, d, hf, P.mirror(T, a))
64
65# Reading
66# =======
67
68def get_view.go(-T: Data, -a: Array<T>, +d: Nat, +i: U32, hf: {D.full(T, a, d) == True{} : Bool},
69  +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, m: P.Mirror(T, a)) ->
70  {Some{Pair.snd(Array<T>, T, Array.get(T, a, i))} == List.get(&2, T, D.view(T, a), D.slot(i, d)) : Maybe<&2, T>}:
71  (t, +e) = m
72  %e : {Some{Pair.snd(Array<T>, T, Array.get(T, _, i))} == List.get(&2, T, D.view(T, _), D.slot(i, d)) : Maybe<&2, T>}
73  I.get_view_t(T, t, d, i, full_t(T, a, t, d, e, hf), hd)
74
75def L.get_view(T, a, d, i, hf, hd):
76  get_view.go(T, a, d, i, hf, hd, P.mirror(T, a))
77
78def get_pair.go(-T: Data, -a: Array<T>, +i: U32, m: P.Mirror(T, a)) ->
79  {Array.get(T, a, i) == (a, Pair.snd(Array<T>, T, Array.get(T, a, i))) : Array<T> & T}:
80  (t, e) = m
81  %e : {Array.get(T, _, i) == (_, Pair.snd(Array<T>, T, Array.get(T, _, i))) : Array<T> & T}
82  P.get_pair_t(T, t, i)
83
84def L.get_pair(T, a, i):
85  get_pair.go(T, a, i, P.mirror(T, a))
86
87def get_kept.go(-T: Data, -a: Array<T>, +i: U32, m: P.Mirror(T, a)) ->
88  {Pair.fst(Array<T>, T, Array.get(T, a, i)) == a : Array<T>}:
89  (t, e) = m
90  %e : {Pair.fst(Array<T>, T, Array.get(T, _, i)) == _ : Array<T>}
91  Equal.cong(Array<T> & T, Array<T>, p => Pair.fst(Array<T>, T, p), Array.get(T, P.fromT(T, t), i),
92    (P.fromT(T, t), Pair.snd(Array<T>, T, Array.get(T, P.fromT(T, t), i))), P.get_pair_t(T, t, i))
93
94def L.get_kept(T, a, i):
95  get_kept.go(T, a, i, P.mirror(T, a))
96
97def L.get_new(T, d, v, i):
98  P.get_new_t(T, d, v, i)
99
100# Writing
101# =======
102
103def set_view.go(-T: Data, -a: Array<T>, +d: Nat, +i: U32, +v: T, hf: {D.full(T, a, d) == True{} : Bool},
104  +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, m: P.Mirror(T, a)) ->
105  {D.view(T, Array.set(T, a, i, v)) == List.set(&2, T, D.view(T, a), D.slot(i, d), v) : List<&2, T>}:
106  (t, +e) = m
107  %e : {D.view(T, Array.set(T, _, i, v)) == List.set(&2, T, D.view(T, _), D.slot(i, d), v) : List<&2, T>}
108  I.set_view_t(T, t, d, i, v, full_t(T, a, t, d, e, hf), hd)
109
110def L.set_view(T, a, d, i, v, hf, hd):
111  set_view.go(T, a, d, i, v, hf, hd, P.mirror(T, a))
112
113def L.set_full(T, a, d, i, v, hf):
114  S.set_full(T, a, d, i, v, hf)
115
116def get_set_same.go(-T: Data, -a: Array<T>, +i: U32, +v: T, m: P.Mirror(T, a)) ->
117  {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T}:
118  (t, e) = m
119  %e : {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, _, i, v), i)) == v : T}
120  P.get_set_same_t(T, t, i, v)
121
122def L.get_set_same(T, a, i, v):
123  get_set_same.go(T, a, i, v, P.mirror(T, a))
124
125def get_set_other.go(-T: Data, -a: Array<T>, +d: Nat, +i: U32, +j: U32, +v: T,
126  hf: {D.full(T, a, d) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool},
127  +hij: {Nat.is_eq(D.slot(i, d), D.slot(j, d)) == False{} : Bool}, m: P.Mirror(T, a)) ->
128  {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), j)) == Pair.snd(Array<T>, T, Array.get(T, a, j)) : T}:
129  (t, +e) = m
130  %e : {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, _, i, v), j)) == Pair.snd(Array<T>, T, Array.get(T, _, j)) : T}
131  I.get_set_other_t(T, t, d, i, j, v, full_t(T, a, t, d, e, hf), hd, hij)
132
133def L.get_set_other(T, a, d, i, j, v, hf, hd, hij):
134  get_set_other.go(T, a, d, i, j, v, hf, hd, hij, P.mirror(T, a))
135
136# Swapping
137# ========
138
139def swap_view.go(-T: Data, -a: Array<T>, +d: Nat, +i: U32, +v: T, hf: {D.full(T, a, d) == True{} : Bool},
140  +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, m: P.Mirror(T, a)) ->
141  {D.view(T, Pair.fst(Array<T>, T, Array.swap(T, a, i, v))) == List.set(&2, T, D.view(T, a), D.slot(i, d), v) : List<&2, T>}:
142  (t, +e) = m
143  %e : {D.view(T, Pair.fst(Array<T>, T, Array.swap(T, _, i, v))) == List.set(&2, T, D.view(T, _), D.slot(i, d), v) : List<&2, T>}
144  I.swap_view_t(T, t, d, i, v, full_t(T, a, t, d, e, hf), hd)
145
146def L.swap_view(T, a, d, i, v, hf, hd):
147  swap_view.go(T, a, d, i, v, hf, hd, P.mirror(T, a))
148
149def swap_old.go(-T: Data, -a: Array<T>, +d: Nat, +i: U32, +v: T, hf: {D.full(T, a, d) == True{} : Bool},
150  +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, m: P.Mirror(T, a)) ->
151  {Some{Pair.snd(Array<T>, T, Array.swap(T, a, i, v))} == List.get(&2, T, D.view(T, a), D.slot(i, d)) : Maybe<&2, T>}:
152  (t, +e) = m
153  %e : {Some{Pair.snd(Array<T>, T, Array.swap(T, _, i, v))} == List.get(&2, T, D.view(T, _), D.slot(i, d)) : Maybe<&2, T>}
154  I.swap_old_t(T, t, d, i, v, full_t(T, a, t, d, e, hf), hd)
155
156def L.swap_old(T, a, d, i, v, hf, hd):
157  swap_old.go(T, a, d, i, v, hf, hd, P.mirror(T, a))
158
159def L.swap_full(T, a, d, i, v, hf):
160  S.swap_full(T, a, d, i, v, hf)
161
162# Shapes, equality and indexes
163# ============================
164
165def view_inj.go(-T: Data, -a: Array<T>, -b: Array<T>, +d: Nat,
166  ha: {D.full(T, a, d) == True{} : Bool}, hb: {D.full(T, b, d) == True{} : Bool},
167  h: {D.view(T, a) == D.view(T, b) : List<&2, T>}, ma: P.Mirror(T, a), mb: P.Mirror(T, b)) ->
168  {a == b : Array<T>}:
169  (ta, +ea) = ma
170  (tb, +eb) = mb
171  %ea : {_ == b : Array<T>}
172  %eb : {P.fromT(T, ta) == _ : Array<T>}
173  +h1 = B.subst(Array<T>, x => {D.view(T, x) == D.view(T, b) : List<&2, T>}, a, P.fromT(T, ta),
174    Equal.sym(Array<T>, P.fromT(T, ta), a, ea), h)
175  +h2 = B.subst(Array<T>, x => {D.view(T, P.fromT(T, ta)) == D.view(T, x) : List<&2, T>}, b, P.fromT(T, tb),
176    Equal.sym(Array<T>, P.fromT(T, tb), b, eb), h1)
177  P.view_inj_t(T, d, ta, tb, full_t(T, a, ta, d, ea, ha), full_t(T, b, tb, d, eb, hb), h2)
178
179def L.view_inj(T, a, b, d, ha, hb, h):
180  view_inj.go(T, a, b, d, ha, hb, h, P.mirror(T, a), P.mirror(T, b))
181
182def L.slot_lt(i, d):
183  I.slot_lt_t(i, d)
184
185def L.slot_small(i, d, h):
186  I.slot_small_t(i, d, h)
187
188# Cloning
189# =======
190
191def L.clone_pair(T, a):
192  P.clone_pair(T, a)