1 import Base 2 import ./defs.bend as D 3 import ./LAWS.bend as L 4 import ./proof_base.bend as B 5 import ./proof_tree.bend as P 6 import ./proof_shape.bend as S 7 import ./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 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. 15 def full_t(-T: Data, -a: Array, -t: P.Tree, +d: Nat, e: {P.fromT(T, t) == a : Array}, 16 hf: {D.full(T, a, d) == True{} : Bool}) -> {D.full(T, P.fromT(T, t), d) == True{} : Bool}: 17 B.subst(Array, x => {D.full(T, x, d) == True{} : Bool}, a, P.fromT(T, t), 18 Equal.sym(Array, P.fromT(T, t), a, e), hf) 19 20 # Creating 21 # ======== 22 23 def L.new_full(T, d, v): 24 P.new_full(T, d, v) 25 26 def L.new_view(T, d, v): 27 P.new_view(T, d, v) 28 29 # Size 30 # ==== 31 32 def view_length.go(-T: Data, -a: Array, +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 38 def L.view_length(T, a, d, hf): 39 view_length.go(T, a, d, hf, P.mirror(T, a)) 40 41 def size_count.go(-T: Data, -a: Array, +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, U32, Array.size(T, a))) == Nat.pow(2n, d) : Nat}: 44 (t, +e) = m 45 %e : {U32.to_nat(Pair.snd(Array, 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 48 def L.size_count(T, a, d, hf, hd): 49 size_count.go(T, a, d, hf, hd, P.mirror(T, a)) 50 51 def L.size_kept(T, a): 52 %Equal.sym(Array & U32, Array.size(T, a), (a, Pair.snd(Array, U32, Array.size(T, a))), P.size_eta(T, a)) : 53 {Pair.fst(Array, U32, _) == a : Array} 54 {==} 55 56 def size_pair.go(-T: Data, -a: Array, +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 & U32}: 58 (t, +e) = m 59 %e : {Array.size(T, _) == (_, U32.shln(1, d)) : Array & U32} 60 P.size_tree(T, d, t, full_t(T, a, t, d, e, hf)) 61 62 def L.size_pair(T, a, d, hf): 63 size_pair.go(T, a, d, hf, P.mirror(T, a)) 64 65 # Reading 66 # ======= 67 68 def get_view.go(-T: Data, -a: Array, +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, 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, 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 75 def L.get_view(T, a, d, i, hf, hd): 76 get_view.go(T, a, d, i, hf, hd, P.mirror(T, a)) 77 78 def get_pair.go(-T: Data, -a: Array, +i: U32, m: P.Mirror(T, a)) -> 79 {Array.get(T, a, i) == (a, Pair.snd(Array, T, Array.get(T, a, i))) : Array & T}: 80 (t, e) = m 81 %e : {Array.get(T, _, i) == (_, Pair.snd(Array, T, Array.get(T, _, i))) : Array & T} 82 P.get_pair_t(T, t, i) 83 84 def L.get_pair(T, a, i): 85 get_pair.go(T, a, i, P.mirror(T, a)) 86 87 def get_kept.go(-T: Data, -a: Array, +i: U32, m: P.Mirror(T, a)) -> 88 {Pair.fst(Array, T, Array.get(T, a, i)) == a : Array}: 89 (t, e) = m 90 %e : {Pair.fst(Array, T, Array.get(T, _, i)) == _ : Array} 91 Equal.cong(Array & T, Array, p => Pair.fst(Array, T, p), Array.get(T, P.fromT(T, t), i), 92 (P.fromT(T, t), Pair.snd(Array, T, Array.get(T, P.fromT(T, t), i))), P.get_pair_t(T, t, i)) 93 94 def L.get_kept(T, a, i): 95 get_kept.go(T, a, i, P.mirror(T, a)) 96 97 def L.get_new(T, d, v, i): 98 P.get_new_t(T, d, v, i) 99 100 # Writing 101 # ======= 102 103 def set_view.go(-T: Data, -a: Array, +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 110 def 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 113 def L.set_full(T, a, d, i, v, hf): 114 S.set_full(T, a, d, i, v, hf) 115 116 def get_set_same.go(-T: Data, -a: Array, +i: U32, +v: T, m: P.Mirror(T, a)) -> 117 {Pair.snd(Array, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T}: 118 (t, e) = m 119 %e : {Pair.snd(Array, T, Array.get(T, Array.set(T, _, i, v), i)) == v : T} 120 P.get_set_same_t(T, t, i, v) 121 122 def L.get_set_same(T, a, i, v): 123 get_set_same.go(T, a, i, v, P.mirror(T, a)) 124 125 def get_set_other.go(-T: Data, -a: Array, +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, Array.get(T, Array.set(T, a, i, v), j)) == Pair.snd(Array, T, Array.get(T, a, j)) : T}: 129 (t, +e) = m 130 %e : {Pair.snd(Array, T, Array.get(T, Array.set(T, _, i, v), j)) == Pair.snd(Array, 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 133 def 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 139 def swap_view.go(-T: Data, -a: Array, +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, 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, 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 146 def 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 149 def swap_old.go(-T: Data, -a: Array, +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, 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, 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 156 def 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 159 def 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 165 def view_inj.go(-T: Data, -a: Array, -b: Array, +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}: 169 (ta, +ea) = ma 170 (tb, +eb) = mb 171 %ea : {_ == b : Array} 172 %eb : {P.fromT(T, ta) == _ : Array} 173 +h1 = B.subst(Array, x => {D.view(T, x) == D.view(T, b) : List<&2, T>}, a, P.fromT(T, ta), 174 Equal.sym(Array, P.fromT(T, ta), a, ea), h) 175 +h2 = B.subst(Array, x => {D.view(T, P.fromT(T, ta)) == D.view(T, x) : List<&2, T>}, b, P.fromT(T, tb), 176 Equal.sym(Array, 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 179 def 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 182 def L.slot_lt(i, d): 183 I.slot_lt_t(i, d) 184 185 def L.slot_small(i, d, h): 186 I.slot_small_t(i, d, h) 187 188 # Cloning 189 # ======= 190 191 def L.clone_pair(T, a): 192 P.clone_pair(T, a)