proofs/lib/sequence.bend
bend-collections-laws-containers@1.0.0.0 · 153 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/lib/sequence.bend as Q
7
8# Lemmas on the SPARK formal-vector model predicates (spec/lib/sequence.bend).
9# Lean 4's List lemmas (List.getElem_append_left, getElem_set_ne,
10# getElem_dropLast, getElem_reverse) are the shape of the lemmas below.
11
12# ---- arithmetic ----
13
14def succ_sub_one(+n: Nat) -> {Nat.sub(1n+n, 1n) == n : Nat}:
15 %Equal.sym(Nat, Nat.sub(1n+n, 0n+1n), Nat.sub(n, 0n), {==}) : {_ == n : Nat}
16 N.sub_zero(n)
17
18def add_one(+i: Nat) -> {Nat.add(i, 1n) == 1n+i : Nat}:
19 Equal.trans(Nat, Nat.add(i, 1n), 1n+Nat.add(i, 0n), 1n+i, N.add_succ(i, 0n), N.succ_cong(Nat.add(i, 0n), i, N.add_zero(i)))
20
21# ---- Append (snoc): Length + 1, Equal_Prefix (old, new), the new element last ----
22
23def re_snoc(-A: Data, +xs: List<&2, A>, +x: A, +i: Nat, +h: {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}) -> {SC.nth(A, xs, i) == SC.nth(A, SC.snoc(A, xs, x), i) : Maybe<&2, A>}:
24 match xs i:
25 case Nil{} _:
26 Empty.absurd({SC.nth(A, Nil{}, i) == SC.nth(A, SC.snoc(A, Nil{}, x), i) : Maybe<&2, A>}, N.lt_zero_absurd(i, h))
27 case Con{a, t} 0n:
28 {==}
29 case Con{a, +t} 1n+p:
30 re_snoc(A, t, x, p, h)
31
32def snoc_prefix(-A: Data, +xs: List<&2, A>, +x: A) -> Q.EqualPrefix(A, xs, SC.snoc(A, xs, x)):
33 %Equal.sym(Nat, SC.length(A, SC.snoc(A, xs, x)), 1n+SC.length(A, xs), LL.length_snoc(A, xs, x)) : {Nat.is_le(SC.length(A, xs), _) == True{} : Bool} & Q.RangeEqual(A, xs, SC.snoc(A, xs, x), 0n, SC.length(A, xs))
34 (N.le_succ(SC.length(A, xs)), i => h1 => h2 => re_snoc(A, xs, x, i, h2))
35
36def snoc_last(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.nth(A, SC.snoc(A, xs, x), SC.length(A, xs)) == Some{x} : Maybe<&2, A>}:
37 match xs:
38 case Nil{}:
39 {==}
40 case Con{+a, +t}:
41 snoc_last(A, t, x)
42
43def snoc_length(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.length(A, SC.snoc(A, xs, x)) == 1n+SC.length(A, xs) : Nat}:
44 LL.length_snoc(A, xs, x)
45
46# Last_Element after Append is the new item
47def snoc_last_elem(-A: Data, +xs: List<&2, A>, +x: A) -> {Q.last_elem(A, SC.snoc(A, xs, x)) == Some{x} : Maybe<&2, A>}:
48 %Equal.sym(Nat, SC.length(A, SC.snoc(A, xs, x)), 1n+SC.length(A, xs), LL.length_snoc(A, xs, x)) : {SC.nth(A, SC.snoc(A, xs, x), Nat.sub(_, 1n)) == Some{x} : Maybe<&2, A>}
49 %Equal.sym(Nat, Nat.sub(1n+SC.length(A, xs), 1n), SC.length(A, xs), succ_sub_one(SC.length(A, xs))) : {SC.nth(A, SC.snoc(A, xs, x), _) == Some{x} : Maybe<&2, A>}
50 snoc_last(A, xs, x)
51
52# ---- Prepend (cons): Length + 1, the new element first, Range_Shifted (old, new, 0, Last, 1) ----
53
54def cons_shift_at(-A: Data, +xs: List<&2, A>, +x: A, +i: Nat) -> {SC.nth(A, xs, i) == SC.nth(A, Con{x, xs}, Nat.add(i, 1n)) : Maybe<&2, A>}:
55 %Equal.sym(Nat, Nat.add(i, 1n), 1n+i, add_one(i)) : {SC.nth(A, xs, i) == SC.nth(A, Con{x, xs}, _) : Maybe<&2, A>}
56 {==}
57
58def cons_shifted(-A: Data, +xs: List<&2, A>, +x: A) -> Q.RangeShifted(A, xs, Con{x, xs}, 0n, SC.length(A, xs), 1n):
59 i => h1 => h2 => cons_shift_at(A, xs, x, i)
60
61def cons_first(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.nth(A, Con{x, xs}, 0n) == Some{x} : Maybe<&2, A>}:
62 {==}
63
64def cons_length(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.length(A, Con{x, xs}) == 1n+SC.length(A, xs) : Nat}:
65 {==}
66
67# ---- Delete_First (tail): Length - 1, Range_Shifted (new, old, 0, Last (new), 1) ----
68# with new = t and old = Con{h, t} this is the Prepend shift read backwards
69
70def tail_shifted(-A: Data, +h: A, +t: List<&2, A>) -> Q.RangeShifted(A, t, Con{h, t}, 0n, SC.length(A, t), 1n):
71 cons_shifted(A, t, h)
72
73# First_Element is Element (Model, First_Index)
74def first_elem(-A: Data, +xs: List<&2, A>) -> {SC.head(A, xs) == SC.nth(A, xs, 0n) : Maybe<&2, A>}:
75 match xs:
76 case Nil{}:
77 {==}
78 case Con{h, t}:
79 {==}
80
81# ---- Delete_Last (init): Length - 1, Equal_Prefix (new, old); the dropped element was Last_Element ----
82
83def re_init(-A: Data, +t: List<&2, A>, +h: A, +i: Nat, +hi: {Nat.is_lt(i, SC.length(A, SC.init(A, Con{h, t}))) == True{} : Bool}) -> {SC.nth(A, SC.init(A, Con{h, t}), i) == SC.nth(A, Con{h, t}, i) : Maybe<&2, A>}:
84 match t i:
85 case Nil{} _:
86 Empty.absurd({SC.nth(A, SC.init(A, Con{h, Nil{}}), i) == SC.nth(A, Con{h, Nil{}}, i) : Maybe<&2, A>}, N.lt_zero_absurd(i, hi))
87 case Con{a, b} 0n:
88 {==}
89 case Con{+a, +b} 1n+p:
90 re_init(A, b, a, p, hi)
91
92def init_length(-A: Data, +t: List<&2, A>, +h: A) -> {SC.length(A, SC.init(A, Con{h, t})) == SC.length(A, t) : Nat}:
93 match t:
94 case Nil{}:
95 {==}
96 case Con{+a, +b}:
97 N.succ_cong(SC.length(A, SC.init(A, Con{a, b})), SC.length(A, b), init_length(A, b, a))
98
99def init_prefix(-A: Data, +t: List<&2, A>, +h: A) -> Q.EqualPrefix(A, SC.init(A, Con{h, t}), Con{h, t}):
100 %Equal.sym(Nat, SC.length(A, SC.init(A, Con{h, t})), SC.length(A, t), init_length(A, t, h)) : {Nat.is_le(_, 1n+SC.length(A, t)) == True{} : Bool} & Q.RangeEqual(A, SC.init(A, Con{h, t}), Con{h, t}, 0n, SC.length(A, SC.init(A, Con{h, t})))
101 (N.le_succ(SC.length(A, t)), i => h1 => h2 => re_init(A, t, h, i, h2))
102
103def last_is_elem(-A: Data, +t: List<&2, A>, +h: A) -> {SC.last(A, Con{h, t}) == Q.last_elem(A, Con{h, t}) : Maybe<&2, A>}:
104 match t:
105 case Nil{}:
106 {==}
107 case Con{+a, +b}:
108 %Equal.sym(Nat, Nat.sub(1n+(1n+SC.length(A, b)), 1n), 1n+SC.length(A, b), succ_sub_one(1n+SC.length(A, b))) : {SC.last(A, Con{a, b}) == SC.nth(A, Con{h, Con{a, b}}, _) : Maybe<&2, A>}
109 Equal.trans(Maybe<&2, A>, SC.last(A, Con{a, b}), SC.nth(A, Con{a, b}, Nat.sub(1n+SC.length(A, b), 1n)), SC.nth(A, Con{a, b}, SC.length(A, b)), last_is_elem(A, b, a), Equal.cong(Nat, Maybe<&2, A>, z => SC.nth(A, Con{a, b}, z), Nat.sub(1n+SC.length(A, b), 1n), SC.length(A, b), succ_sub_one(SC.length(A, b))))
110
111# ---- Replace_Element (update): Length kept, the element at Index replaced, Equal_Except elsewhere ----
112
113def update_except(-A: Data, +xs: List<&2, A>, +i: Nat, +v: A) -> Q.EqualExcept(A, xs, SC.update(A, xs, i, v), i):
114 (Equal.sym(Nat, SC.length(A, SC.update(A, xs, i, v)), SC.length(A, xs), LL.length_update(A, xs, i, v)), j => ne => Equal.sym(Maybe<&2, A>, SC.nth(A, SC.update(A, xs, i, v), j), SC.nth(A, xs, j), LL.nth_update_other(A, xs, i, j, v, ne)))
115
116def update_at(-A: Data, +xs: List<&2, A>, +i: Nat, +v: A, +h: {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}) -> {SC.nth(A, SC.update(A, xs, i, v), i) == Some{v} : Maybe<&2, A>}:
117 LL.nth_update_same(A, xs, i, v, h)
118
119def update_length(-A: Data, +xs: List<&2, A>, +i: Nat, +v: A) -> {SC.length(A, SC.update(A, xs, i, v)) == SC.length(A, xs) : Nat}:
120 LL.length_update(A, xs, i, v)
121
122# ---- Reserve_Capacity / Assign / reads: the model is unchanged (M.Equal) ----
123
124def same_prefix(-A: Data, +xs: List<&2, A>) -> Q.EqualPrefix(A, xs, xs):
125 (N.le_refl(SC.length(A, xs)), i => h1 => h2 => {==})
126
127# ---- Insert in the middle: a ++ c becomes a ++ [n] ++ c (Insert at Before = Length (a)) ----
128# Range_Equal (old, new, First, Before - 1), Element (new, Before) = New_Item,
129# Range_Shifted (old, new, Before, Last'Old, 1), Length + 1. Read with the
130# roles swapped (old = a ++ [n] ++ c, new = a ++ c) it is Delete at Before.
131
132def mid_equal(-A: Data, +a: List<&2, A>, +c: List<&2, A>, +n: A) -> Q.RangeEqual(A, SC.append(A, a, c), SC.append(A, a, Con{n, c}), 0n, SC.length(A, a)):
133 i => h1 => h2 => Equal.trans(Maybe<&2, A>, SC.nth(A, SC.append(A, a, c), i), SC.nth(A, a, i), SC.nth(A, SC.append(A, a, Con{n, c}), i), LL.nth_append_left(A, a, c, i, h2), Equal.sym(Maybe<&2, A>, SC.nth(A, SC.append(A, a, Con{n, c}), i), SC.nth(A, a, i), LL.nth_append_left(A, a, Con{n, c}, i, h2)))
134
135def mid_at(-A: Data, +a: List<&2, A>, +c: List<&2, A>, +n: A) -> {SC.nth(A, SC.append(A, a, Con{n, c}), SC.length(A, a)) == Some{n} : Maybe<&2, A>}:
136 %Equal.sym(Maybe<&2, A>, SC.nth(A, SC.append(A, a, Con{n, c}), SC.length(A, a)), SC.nth(A, Con{n, c}, Nat.sub(SC.length(A, a), SC.length(A, a))), LL.nth_append_right(A, a, Con{n, c}, SC.length(A, a), N.le_refl(SC.length(A, a)))) : {_ == Some{n} : Maybe<&2, A>}
137 %Equal.sym(Nat, Nat.sub(SC.length(A, a), SC.length(A, a)), 0n, N.sub_self(SC.length(A, a))) : {SC.nth(A, Con{n, c}, _) == Some{n} : Maybe<&2, A>}
138 {==}
139
140def mid_shift_at(-A: Data, +a: List<&2, A>, +c: List<&2, A>, +n: A, +i: Nat, +h1: {Nat.is_le(SC.length(A, a), i) == True{} : Bool}) -> {SC.nth(A, SC.append(A, a, c), i) == SC.nth(A, SC.append(A, a, Con{n, c}), Nat.add(i, 1n)) : Maybe<&2, A>}:
141 %Equal.sym(Nat, Nat.add(i, 1n), 1n+i, add_one(i)) : {SC.nth(A, SC.append(A, a, c), i) == SC.nth(A, SC.append(A, a, Con{n, c}), _) : Maybe<&2, A>}
142 %Equal.sym(Maybe<&2, A>, SC.nth(A, SC.append(A, a, c), i), SC.nth(A, c, Nat.sub(i, SC.length(A, a))), LL.nth_append_right(A, a, c, i, h1)) : {_ == SC.nth(A, SC.append(A, a, Con{n, c}), 1n+i) : Maybe<&2, A>}
143 %Equal.sym(Maybe<&2, A>, SC.nth(A, SC.append(A, a, Con{n, c}), 1n+i), SC.nth(A, Con{n, c}, Nat.sub(1n+i, SC.length(A, a))), LL.nth_append_right(A, a, Con{n, c}, 1n+i, N.le_trans(SC.length(A, a), i, 1n+i, h1, N.le_succ(i)))) : {SC.nth(A, c, Nat.sub(i, SC.length(A, a))) == _ : Maybe<&2, A>}
144 %Equal.sym(Nat, Nat.sub(1n+i, SC.length(A, a)), 1n+Nat.sub(i, SC.length(A, a)), N.sub_succ_left(i, SC.length(A, a), h1)) : {SC.nth(A, c, Nat.sub(i, SC.length(A, a))) == SC.nth(A, Con{n, c}, _) : Maybe<&2, A>}
145 {==}
146
147def mid_shifted(-A: Data, +a: List<&2, A>, +c: List<&2, A>, +n: A) -> Q.RangeShifted(A, SC.append(A, a, c), SC.append(A, a, Con{n, c}), SC.length(A, a), SC.length(A, SC.append(A, a, c)), 1n):
148 i => h1 => h2 => mid_shift_at(A, a, c, n, i, h1)
149
150def mid_length(-A: Data, +a: List<&2, A>, +c: List<&2, A>, +n: A) -> {SC.length(A, SC.append(A, a, Con{n, c})) == 1n+SC.length(A, SC.append(A, a, c)) : Nat}:
151 %Equal.sym(Nat, SC.length(A, SC.append(A, a, Con{n, c})), Nat.add(SC.length(A, a), 1n+SC.length(A, c)), LL.length_append(A, a, Con{n, c})) : {_ == 1n+SC.length(A, SC.append(A, a, c)) : Nat}
152 %Equal.sym(Nat, SC.length(A, SC.append(A, a, c)), Nat.add(SC.length(A, a), SC.length(A, c)), LL.length_append(A, a, c)) : {Nat.add(SC.length(A, a), 1n+SC.length(A, c)) == 1n+_ : Nat}
153 N.add_succ(SC.length(A, a), SC.length(A, c))