proofs/crypto/sha/list_proofs.bend

bend-collections-laws-crypto@1.0.0.0 · 97 lines · 7 definitions

1import Base
2
3law append_assoc:
4  for -A: Data
5  for xs: List<&2, A>
6  for ys: List<&2, A>
7  for zs: List<&2, A>
8  {List.append(&2, A, List.append(&2, A, xs, ys), zs)
9    == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>}
10
11def append_assoc(A, xs, ys, zs):
12  match xs:
13    case Nil{}:
14      {==}
15    case h <> t:
16      %append_assoc(A, t, ys, zs) :
17        {h <> List.append(&2, A, List.append(&2, A, t, ys), zs) == h <> _ : List<&2, A>}
18      {==}
19
20law reverse_twice:
21  for -A: Data
22  for xs: List<&2, A>
23  for acc: List<&2, A>
24  for ys: List<&2, A>
25  {List.reverse.go(&2, A, List.reverse.go(&2, A, xs, acc), ys)
26    == List.reverse.go(&2, A, acc, List.append(&2, A, xs, ys)) : List<&2, A>}
27
28def reverse_twice(A, xs, acc, ys):
29  match xs:
30    case Nil{}:
31      {==}
32    case h <> t:
33      reverse_twice(A, t, h <> acc, ys)
34
35law reverse_append:
36  for -A: Data
37  for xs: List<&2, A>
38  for ys: List<&2, A>
39  {List.reverse.go(&2, A, List.reverse(&2, A, xs), ys)
40    == List.append(&2, A, xs, ys) : List<&2, A>}
41
42def reverse_append(A, xs, ys):
43  reverse_twice(A, xs, Nil{}, ys)
44
45law add_succ:
46  for n: Nat
47  for m: Nat
48  {Nat.add(n, 1n+m) == 1n+Nat.add(n, m) : Nat}
49
50def add_succ(n, m):
51  match n:
52    case 0n:
53      {==}
54    case 1n+p:
55      %add_succ(p, m) : {1n+Nat.add(p, 1n+m) == 1n+_ : Nat}
56      {==}
57
58law add_zero:
59  for n: Nat
60  {Nat.add(n, 0n) == n : Nat}
61
62def add_zero(n):
63  match n:
64    case 0n:
65      {==}
66    case 1n+p:
67      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
68      {==}
69
70law append_assoc_reverse:
71  for -A: Data
72  for +xs: List<&2, A>
73  for +ys: List<&2, A>
74  for +zs: List<&2, A>
75  {List.append(&2, A, xs, List.append(&2, A, ys, zs))
76    == List.append(&2, A, List.append(&2, A, xs, ys), zs) : List<&2, A>}
77
78def append_assoc_reverse(A, xs, ys, zs):
79  Equal.sym(List<&2, A>, List.append(&2, A, List.append(&2, A, xs, ys), zs),
80    List.append(&2, A, xs, List.append(&2, A, ys, zs)), append_assoc(A, xs, ys, zs))
81
82law add_swap:
83  for +n: Nat
84  for +k: Nat
85  for +m: Nat
86  {Nat.add(n, Nat.add(k, m)) == Nat.add(k, Nat.add(n, m)) : Nat}
87
88def add_swap(n, k, m):
89  match k:
90    case 0n:
91      {==}
92    case 1n+p:
93      Equal.trans(Nat, Nat.add(n, 1n+Nat.add(p, m)),
94        1n+Nat.add(n, Nat.add(p, m)), 1n+Nat.add(p, Nat.add(n, m)),
95        add_succ(n, Nat.add(p, m)),
96        Equal.cong(Nat, Nat, x => 1n+x, Nat.add(n, Nat.add(p, m)),
97          Nat.add(p, Nat.add(n, m)), add_swap(n, p, m)))