1	import Base
2	
3	# Decidable equality makes certificates for Bool and Nat unique. These lemmas
4	# compare proofs without evaluating the computation that produced each proof.
5	def bool_code(a: Bool, b: Bool) -> Data:
6	    match a b:
7	        case False{} False{}: Unit
8	        case True{} True{}: Unit
9	        case _ _: Empty
10	
11	def bool_code_refl(a: Bool) -> bool_code(a, a):
12	    match a:
13	        case False{}: Unit{}
14	        case True{}: Unit{}
15	
16	def bool_encode(+a: Bool, +b: Bool, proof: {a == b : Bool}) -> bool_code(a, b):
17	    %proof : bool_code(a, _)
18	    bool_code_refl(a)
19	
20	def bool_decode(+a: Bool, +b: Bool, code: bool_code(a, b)) -> {a == b : Bool}:
21	    match a b:
22	        case False{} False{}: {==}
23	        case True{} True{}: {==}
24	        case False{} True{}: Empty.absurd({a == b : Bool}, code)
25	        case True{} False{}: Empty.absurd({a == b : Bool}, code)
26	
27	def bool_decode_refl(+a: Bool) ->
28	    {bool_decode(a, a, bool_code_refl(a)) == {==} : {a == a : Bool}}:
29	    match a:
30	        case False{}: {==}
31	        case True{}: {==}
32	
33	def bool_decode_encode(+a: Bool, +b: Bool, +proof: {a == b : Bool}) ->
34	    {bool_decode(a, b, bool_encode(a, b, proof)) == proof : {a == b : Bool}}:
35	    %path@proof : {bool_decode(a, _, bool_encode(a, _, path)) == path :
36	        {a == _ : Bool}}
37	    bool_decode_refl(a)
38	
39	def bool_code_unique(+a: Bool, +b: Bool,
40	    +first: bool_code(a, b), second: bool_code(a, b)) ->
41	    {first == second : bool_code(a, b)}:
42	    match a b:
43	        case False{} False{}:
44	            match first second:
45	                case Unit{} Unit{}: {==}
46	        case True{} True{}:
47	            match first second:
48	                case Unit{} Unit{}: {==}
49	        case False{} True{}:
50	            Empty.absurd({first == second : bool_code(a, b)}, first)
51	        case True{} False{}:
52	            Empty.absurd({first == second : bool_code(a, b)}, first)
53	
54	def bool_unique(+a: Bool, +b: Bool,
55	    +first: {a == b : Bool}, +second: {a == b : Bool}) ->
56	    {first == second : {a == b : Bool}}:
57	    +first_code = bool_encode(a, b, first)
58	    +second_code = bool_encode(a, b, second)
59	    codes_same = bool_code_unique(a, b, first_code, second_code)
60	    decoded_same = Equal.cong(bool_code(a, b), {a == b : Bool},
61	        code => bool_decode(a, b, code), first_code, second_code, codes_same)
62	    Equal.trans({a == b : Bool}, first, bool_decode(a, b, first_code), second,
63	        Equal.sym({a == b : Bool}, bool_decode(a, b, first_code), first,
64	            bool_decode_encode(a, b, first)),
65	        Equal.trans({a == b : Bool}, bool_decode(a, b, first_code),
66	            bool_decode(a, b, second_code), second, decoded_same,
67	            bool_decode_encode(a, b, second)))
68	
69	def nat_code(a: Nat, b: Nat) -> Data:
70	    match a b:
71	        case 0n 0n: Unit
72	        case 1n+p 1n+q: nat_code(p, q)
73	        case _ _: Empty
74	
75	def nat_code_refl(a: Nat) -> nat_code(a, a):
76	    match a:
77	        case 0n: Unit{}
78	        case 1n+p: nat_code_refl(p)
79	
80	def nat_encode(+a: Nat, +b: Nat, proof: {a == b : Nat}) -> nat_code(a, b):
81	    %proof : nat_code(a, _)
82	    nat_code_refl(a)
83	
84	def nat_decode(+a: Nat, +b: Nat, code: nat_code(a, b)) -> {a == b : Nat}:
85	    match a b:
86	        case 0n 0n: {==}
87	        case 0n 1n+q: Empty.absurd({a == b : Nat}, code)
88	        case 1n+p 0n: Empty.absurd({a == b : Nat}, code)
89	        case 1n+p 1n+q:
90	            Equal.cong(Nat, Nat, value => 1n+value, p, q,
91	                nat_decode(p, q, code))
92	
93	def nat_decode_refl(+a: Nat) ->
94	    {nat_decode(a, a, nat_code_refl(a)) == {==} : {a == a : Nat}}:
95	    match a:
96	        case 0n: {==}
97	        case 1n+p:
98	            %Equal.sym({p == p : Nat},
99	                nat_decode(p, p, nat_code_refl(p)), {==},
100	                nat_decode_refl(p)) :
101	                {Equal.cong(Nat, Nat, value => 1n+value, p, p, _) == {==} :
102	                    {1n+p == 1n+p : Nat}}
103	            {==}
104	
105	def nat_decode_encode(+a: Nat, +b: Nat, +proof: {a == b : Nat}) ->
106	    {nat_decode(a, b, nat_encode(a, b, proof)) == proof : {a == b : Nat}}:
107	    %path@proof : {nat_decode(a, _, nat_encode(a, _, path)) == path :
108	        {a == _ : Nat}}
109	    nat_decode_refl(a)
110	
111	def nat_code_unique(+a: Nat, +b: Nat,
112	    +first: nat_code(a, b), second: nat_code(a, b)) ->
113	    {first == second : nat_code(a, b)}:
114	    match a b:
115	        case 0n 0n:
116	            match first second:
117	                case Unit{} Unit{}: {==}
118	        case 0n 1n+q:
119	            Empty.absurd({first == second : nat_code(a, b)}, first)
120	        case 1n+p 0n:
121	            Empty.absurd({first == second : nat_code(a, b)}, first)
122	        case 1n+p 1n+q: nat_code_unique(p, q, first, second)
123	
124	def nat_unique(+a: Nat, +b: Nat,
125	    +first: {a == b : Nat}, +second: {a == b : Nat}) ->
126	    {first == second : {a == b : Nat}}:
127	    +first_code = nat_encode(a, b, first)
128	    +second_code = nat_encode(a, b, second)
129	    codes_same = nat_code_unique(a, b, first_code, second_code)
130	    decoded_same = Equal.cong(nat_code(a, b), {a == b : Nat},
131	        code => nat_decode(a, b, code), first_code, second_code, codes_same)
132	    Equal.trans({a == b : Nat}, first, nat_decode(a, b, first_code), second,
133	        Equal.sym({a == b : Nat}, nat_decode(a, b, first_code), first,
134	            nat_decode_encode(a, b, first)),
135	        Equal.trans({a == b : Nat}, nat_decode(a, b, first_code),
136	            nat_decode(a, b, second_code), second, decoded_same,
137	            nat_decode_encode(a, b, second)))