1 import Base 2 import ./logic.bend as L 3 import ./nat.bend as N 4 import ./list.bend as LL 5 import ../../spec/lib/common.bend as SC 6 import ../../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 14 def 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 18 def 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 23 def 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 32 def 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 36 def 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 43 def 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 47 def 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 54 def 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 58 def 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 61 def cons_first(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.nth(A, Con{x, xs}, 0n) == Some{x} : Maybe<&2, A>}: 62 {==} 63 64 def 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 70 def 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) 74 def 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 83 def 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 92 def 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 99 def 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 103 def 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 113 def 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 116 def 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 119 def 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 124 def 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 132 def 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 135 def 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 140 def 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 147 def 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 150 def 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))