1	import Base
2	import ./lifecycle.bend as Lifecycle
3	
4	def half(number: Nat) -> Nat:
5	  match number:
6	    case 0n:
7	      0n
8	    case 1n:
9	      0n
10	    case 2n+p:
11	      1n+half(p)
12	
13	def even(number: Nat) -> Bool:
14	  match number:
15	    case 0n:
16	      True{}
17	    case 1n:
18	      False{}
19	    case 2n+p:
20	      even(p)
21	
22	def half_double(+number: Nat) -> {half(Nat.double(number)) == number : Nat}:
23	  match number:
24	    case 0n:
25	      {==}
26	    case 1n+p:
27	      Equal.cong(Nat, Nat, n => 1n+n, half(Nat.double(p)), p, half_double(p))
28	
29	def even_double(+number: Nat) -> {even(Nat.double(number)) == True{} : Bool}:
30	  match number:
31	    case 0n:
32	      {==}
33	    case 1n+p:
34	      even_double(p)
35	
36	def even_successor_double(+number: Nat) -> {even(1n+Nat.double(number)) == False{} : Bool}:
37	  match number:
38	    case 0n:
39	      {==}
40	    case 1n+p:
41	      even_successor_double(p)
42	
43	def double_injective(+left: Nat, +right: Nat, equal: {Nat.double(left) == Nat.double(right) : Nat}) -> {left == right : Nat}:
44	  Equal.trans(Nat, left, half(Nat.double(left)), right,
45	    Equal.sym(Nat, half(Nat.double(left)), left, half_double(left)),
46	    Equal.trans(Nat, half(Nat.double(left)), half(Nat.double(right)), right,
47	      Equal.cong(Nat, Nat, n => half(n), Nat.double(left), Nat.double(right), equal), half_double(right)))
48	
49	def parity_clash(+left: Nat, +right: Nat, equal: {Nat.double(left) == 1n+Nat.double(right) : Nat}) -> Empty:
50	  Lifecycle.false_true(Equal.trans(Bool, True{}, even(Nat.double(left)), False{},
51	    Equal.sym(Bool, even(Nat.double(left)), True{}, even_double(left)),
52	    Equal.trans(Bool, even(Nat.double(left)), even(1n+Nat.double(right)), False{},
53	      Equal.cong(Nat, Bool, n => even(n), Nat.double(left), 1n+Nat.double(right), equal), even_successor_double(right))))
54	
55	def predecessor(number: Nat) -> Nat:
56	  match number:
57	    case 0n:
58	      0n
59	    case 1n+p:
60	      p
61	
62	def successor_injective(-left: Nat, -right: Nat, equal: {1n+left == 1n+right : Nat}) -> {left == right : Nat}:
63	  Equal.cong(Nat, Nat, n => predecessor(n), 1n+left, 1n+right, equal)
64	
65	def word_natural_injective(+width: Nat, +left: Word(width), +right: Word(width)) ->
66	  {Word.to_nat(width, left) == Word.to_nat(width, right) : Nat} -> {left == right : Word(width)}:
67	  match width:
68	    case 0n:
69	      match left right:
70	        case WNil{} WNil{}:
71	          equal => {==}
72	    case 1n+p:
73	      match left right:
74	        case WCon{False{}, +lt} WCon{False{}, +rt}:
75	          equal => Equal.cong(Word(p), Word(1n+p), w => WCon{False{}, w}, lt, rt,
76	            word_natural_injective(p, lt, rt)(double_injective(Word.to_nat(p, lt), Word.to_nat(p, rt), equal)))
77	        case WCon{False{}, +lt} WCon{True{}, +rt}:
78	          equal => Empty.absurd({WCon{False{}, lt} == WCon{True{}, rt} : Word(1n+p)},
79	            parity_clash(Word.to_nat(p, lt), Word.to_nat(p, rt), equal))
80	        case WCon{True{}, +lt} WCon{False{}, +rt}:
81	          equal => Empty.absurd({WCon{True{}, lt} == WCon{False{}, rt} : Word(1n+p)},
82	            parity_clash(Word.to_nat(p, rt), Word.to_nat(p, lt),
83	              Equal.sym(Nat, 1n+Nat.double(Word.to_nat(p, lt)), Nat.double(Word.to_nat(p, rt)), equal)))
84	        case WCon{True{}, +lt} WCon{True{}, +rt}:
85	          equal => Equal.cong(Word(p), Word(1n+p), w => WCon{True{}, w}, lt, rt,
86	            word_natural_injective(p, lt, rt)(double_injective(Word.to_nat(p, lt), Word.to_nat(p, rt),
87	              successor_injective(Nat.double(Word.to_nat(p, lt)), Nat.double(Word.to_nat(p, rt)), equal))))
88	
89	def u32_natural_injective(+left: U32, +right: U32) ->
90	  {U32.to_nat(left) == U32.to_nat(right) : Nat} -> {left == right : U32}:
91	  match left right:
92	    case U32{+lw} U32{+rw}:
93	      equal => Equal.cong(Word(32n), U32, w => U32{w}, lw, rw, word_natural_injective(32n, lw, rw)(equal))