1	import Base
2	
3	# List and Nat facts for the incremental hasher.
4	
5	law append_nil:
6	  for +xs: List<&2, U32>
7	  {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>}
8	
9	def 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	
17	law 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	
23	def 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	
32	law 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	
38	def 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	
42	law add_zero:
43	  for +n: Nat
44	  {Nat.add(n, 0n) == n : Nat}
45	
46	def 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	
54	law 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	
60	def 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	
68	law 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	
73	def 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	# n + |xs| + |ys| == n + |xs ++ ys|
82	law 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	
88	def 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))