proofs/crypto/hash/lists.bend
bend-collections-laws-crypto@1.0.0.0 · 92 lines · 7 definitions
1import Base
2
3
4
5law append_nil:
6 for +xs: List<&2, U32>
7 {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>}
8
9def append_nil(xs):
10 match xs:
11 case Nil{}:
12 {==}
13 case h <> t:
14 %append_nil(t) : {h <> List.append(&2, U32, t, Nil{}) == h <> _ : List<&2, U32>}
15 {==}
16
17law append_assoc:
18 for +xs: List<&2, U32>
19 for +ys: List<&2, U32>
20 for +zs: List<&2, U32>
21 {List.append(&2, U32, List.append(&2, U32, xs, ys), zs) == List.append(&2, U32, xs, List.append(&2, U32, ys, zs)) : List<&2, U32>}
22
23def append_assoc(xs, ys, zs):
24 match xs:
25 case Nil{}:
26 {==}
27 case h <> t:
28 %append_assoc(t, ys, zs) :
29 {h <> List.append(&2, U32, List.append(&2, U32, t, ys), zs) == h <> _ : List<&2, U32>}
30 {==}
31
32law append_assoc_rev:
33 for +xs: List<&2, U32>
34 for +ys: List<&2, U32>
35 for +zs: List<&2, U32>
36 {List.append(&2, U32, xs, List.append(&2, U32, ys, zs)) == List.append(&2, U32, List.append(&2, U32, xs, ys), zs) : List<&2, U32>}
37
38def append_assoc_rev(xs, ys, zs):
39 Equal.sym(List<&2, U32>, List.append(&2, U32, List.append(&2, U32, xs, ys), zs),
40 List.append(&2, U32, xs, List.append(&2, U32, ys, zs)), append_assoc(xs, ys, zs))
41
42law add_zero:
43 for +n: Nat
44 {Nat.add(n, 0n) == n : Nat}
45
46def add_zero(n):
47 match n:
48 case 0n:
49 {==}
50 case 1n+p:
51 %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
52 {==}
53
54law add_assoc:
55 for +a: Nat
56 for +b: Nat
57 for +c: Nat
58 {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}
59
60def add_assoc(a, b, c):
61 match a:
62 case 0n:
63 {==}
64 case 1n+p:
65 %add_assoc(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
66 {==}
67
68law length_append:
69 for +xs: List<&2, U32>
70 for +ys: List<&2, U32>
71 {List.length(&2, U32, List.append(&2, U32, xs, ys)) == Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}
72
73def length_append(xs, ys):
74 match xs:
75 case Nil{}:
76 {==}
77 case h <> t:
78 %length_append(t, ys) : {1n+List.length(&2, U32, List.append(&2, U32, t, ys)) == 1n+_ : Nat}
79 {==}
80
81
82law add_length:
83 for +n: Nat
84 for +xs: List<&2, U32>
85 for +ys: List<&2, U32>
86 {Nat.add(Nat.add(n, List.length(&2, U32, xs)), List.length(&2, U32, ys)) == Nat.add(n, List.length(&2, U32, List.append(&2, U32, xs, ys))) : Nat}
87
88def add_length(n, xs, ys):
89 %Equal.sym(Nat, List.length(&2, U32, List.append(&2, U32, xs, ys)),
90 Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)), length_append(xs, ys)) :
91 {Nat.add(Nat.add(n, List.length(&2, U32, xs)), List.length(&2, U32, ys)) == Nat.add(n, _) : Nat}
92 add_assoc(n, List.length(&2, U32, xs), List.length(&2, U32, ys))