1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
4	import ../../math/typed/width.bend as WW
5	
6	# The few semiring facts the rewrite generator (tools/generators/rw.py,
7	# %norm) uses besides nat_algebra and width.
8	
9	def zero_add(+x: Nat) -> {Nat.add(0n, x) == x : Nat}:
10	  {==}
11	
12	def zero_mul(+x: Nat) -> {Nat.mul(0n, x) == 0n : Nat}:
13	  {==}
14	
15	def one_mul(+x: Nat) -> {Nat.mul(1n, x) == x : Nat}:
16	  NA.add_zero(x)
17	
18	def shift0(+x: Nat) -> {C.shift(0n, x) == x : Nat}:
19	  {==}
20	
21	def mul_swap(+a: Nat, +b: Nat, +c: Nat) -> {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(b, Nat.mul(a, c)) : Nat}:
22	  %NA.mul_assoc(a, b, c) : {_ == Nat.mul(b, Nat.mul(a, c)) : Nat}
23	  %NA.mul_assoc(b, a, c) : {Nat.mul(Nat.mul(a, b), c) == _ : Nat}
24	  %NA.mul_comm(a, b) : {Nat.mul(Nat.mul(a, b), c) == Nat.mul(_, c) : Nat}
25	  {==}
26	
27	def shift_shift(+j: Nat, +k: Nat, +x: Nat) -> {C.shift(j, C.shift(k, x)) == C.shift(Nat.add(j, k), x) : Nat}:
28	  Equal.sym(Nat, C.shift(Nat.add(j, k), x), C.shift(j, C.shift(k, x)), WW.shift_comp(j, k, x))
29	
30	def succ_add(+k: Nat, +x: Nat) -> {Nat.add(k, x) == Nat.add(x, k) : Nat}:
31	  NA.add_comm(k, x)