1	import Base
2	
3	# Propositional helpers shared by every proof module.
4	
5	def truth(b: Bool) -> Type:
6	  match b:
7	    case False{}:
8	      Empty
9	    case True{}:
10	      Unit
11	
12	def false_true(e: {False{} == True{} : Bool}) -> Empty:
13	  %Equal.sym(Bool, False{}, True{}, e) : truth(_)
14	  Unit{}
15	
16	def true_false(e: {True{} == False{} : Bool}) -> Empty:
17	  false_true(Equal.sym(Bool, True{}, False{}, e))
18	
19	def and_left(a: Bool, b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
20	  match a:
21	    case False{}:
22	      Empty.absurd({False{} == True{} : Bool}, false_true(e))
23	    case True{}:
24	      {==}
25	
26	def and_right(a: Bool, b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
27	  match a:
28	    case False{}:
29	      Empty.absurd({b == True{} : Bool}, false_true(e))
30	    case True{}:
31	      e
32	
33	def and_intro(a: Bool, b: Bool, ea: {a == True{} : Bool}, eb: {b == True{} : Bool}) -> {Bool.and(a, b) == True{} : Bool}:
34	  %Equal.sym(Bool, a, True{}, ea) : {Bool.and(_, b) == True{} : Bool}
35	  eb
36	
37	def not_true(b: Bool, e: {Bool.not(b) == True{} : Bool}) -> {b == False{} : Bool}:
38	  match b:
39	    case False{}:
40	      {==}
41	    case True{}:
42	      Empty.absurd({True{} == False{} : Bool}, false_true(e))
43	
44	def not_false(b: Bool, e: {b == False{} : Bool}) -> {Bool.not(b) == True{} : Bool}:
45	  %Equal.sym(Bool, b, False{}, e) : {Bool.not(_) == True{} : Bool}
46	  {==}
47	
48	def bool_cases(b: Bool) -> Or({b == True{} : Bool}, {b == False{} : Bool}):
49	  match b:
50	    case True{}:
51	      Inl{{==}}
52	    case False{}:
53	      Inr{{==}}
54	
55	def true_not_false(b: Bool, t: {b == True{} : Bool}, f: {b == False{} : Bool}) -> Empty:
56	  false_true(Equal.trans(Bool, False{}, b, True{}, Equal.sym(Bool, b, False{}, f), t))
57	
58	# Cmp discrimination.
59	def cmp_code(c: Cmp) -> Nat:
60	  match c:
61	    case LT{}:
62	      0n
63	    case EQ{}:
64	      1n
65	    case GT{}:
66	      2n
67	
68	def cmp_lt_eq(e: {LT{} == EQ{} : Cmp}) -> Empty:
69	  %e : truth(Cmp.is_lt(_))
70	  Unit{}
71	
72	def cmp_lt_gt(e: {LT{} == GT{} : Cmp}) -> Empty:
73	  %e : truth(Cmp.is_lt(_))
74	  Unit{}
75	
76	def cmp_eq_gt(e: {EQ{} == GT{} : Cmp}) -> Empty:
77	  %e : truth(Cmp.is_eq(_))
78	  Unit{}
79	
80	# Maybe discrimination.
81	def none_some(-A: Data, x: A, e: {None{} == Some{x} : Maybe<&2, A>}) -> Empty:
82	  %Equal.sym(Maybe<&2, A>, None{}, Some{x}, e) : truth(Maybe.is_some(&2, A, _))
83	  Unit{}
84	
85	def some_value(-A: Data, m: Maybe<&2, A>, d: A) -> A:
86	  match m:
87	    case None{}:
88	      d
89	    case Some{x}:
90	      x
91	
92	def some_inj(-A: Data, x: A, y: A, e: {Some{x} == Some{y} : Maybe<&2, A>}) -> {x == y : A}:
93	  Equal.cong(Maybe<&2, A>, A, m => some_value(A, m, x), Some{x}, Some{y}, e)
94	
95	def pair_fst(-A: Type, -B: Type, a: A, b: B, c: A, d: B, e: {(a, b) == (c, d) : A & B}) -> {a == c : A}:
96	  Equal.cong(A & B, A, p => Pair.fst(A, B, p), (a, b), (c, d), e)
97	
98	def pair_snd(-A: Type, -B: Type, a: A, b: B, c: A, d: B, e: {(a, b) == (c, d) : A & B}) -> {b == d : B}:
99	  Equal.cong(A & B, B, p => Pair.snd(A, B, p), (a, b), (c, d), e)
100	
101	def pair_eq(-A: Type, -B: Type, a: A, b: B, c: A, d: B, ea: {a == c : A}, eb: {b == d : B}) -> {(a, b) == (c, d) : A & B}:
102	  %ea : {(a, b) == (_, d) : A & B}
103	  %eb : {(a, b) == (a, _) : A & B}
104	  {==}
105	
106	# Transport a proof along an equation.
107	def subst(-A: Type, -P: A -> Type, -a: A, -b: A, e: {a == b : A}, pa: P(a)) -> P(b):
108	  %e : P(_)
109	  pa
110	
111	# Dependent pair projections (call results cannot be destructured directly).
112	def sfst(-A: Type, -B: @-x: A -> Type, p: Sigma<&1, &1, A, B>) -> A:
113	  match p:
114	    case Tuple{a, b}:
115	      a
116	
117	def ssnd(-A: Type, -B: @-x: A -> Type, p: Sigma<&1, &1, A, B>) -> B(sfst(A, B, p)):
118	  match p:
119	    case Tuple{a, b}:
120	      b
121	
122	def pair_eta(-A: Type, -B: Type, p: A & B) -> {p == (Pair.fst(A, B, p), Pair.snd(A, B, p)) : A & B}:
123	  match p:
124	    case Tuple{a, b}:
125	      {==}