1	import Base
2	
3	# Total-order comparison for keys. Base's String.cmp hands the strings back
4	# beside the verdict ((s1, s2), c); we take reusable copies and unpack via a
5	# helper (a match cannot scrutinize the computed call directly).
6	def unpack(pair: (String & String) & Cmp) -> Cmp:
7	  match pair:
8	    case ((_, _), c):
9	      c
10	
11	def cmp(+s1: String, +s2: String) -> Cmp:
12	  unpack(String.cmp(s1, s2))
13	
14	def eq(+s1: String, +s2: String) -> Bool:
15	  String.eq(s1, s2)
16	
17	# Small, coherent views of Cmp used by key-order laws and sorted-run code.
18	def cmp_is_lt(ord: Cmp) -> Bool:
19	  Cmp.is_lt(ord)
20	
21	def cmp_is_eq(ord: Cmp) -> Bool:
22	  Cmp.is_eq(ord)
23	
24	def cmp_is_gt(ord: Cmp) -> Bool:
25	  Cmp.is_gt(ord)
26	
27	def cmp_is_le(ord: Cmp) -> Bool:
28	  Cmp.is_le(ord)
29	
30	def lt(+s1: String, +s2: String) -> Bool:
31	  cmp_is_lt(cmp(s1, s2))
32	
33	def le(+s1: String, +s2: String) -> Bool:
34	  cmp_is_le(cmp(s1, s2))
35	
36	def cmp_reverse(ord: Cmp) -> Cmp:
37	  match ord:
38	    case LT{}:
39	      GT{}
40	    case EQ{}:
41	      EQ{}
42	    case GT{}:
43	      LT{}
44	
45	def implies(s1: Bool, s2: Bool) -> Bool:
46	  match s1:
47	    case False{}:
48	      True{}
49	    case True{}:
50	      s2
51	
52	def iff(+s1: Bool, +s2: Bool) -> Bool:
53	  Bool.and(implies(s1, s2), implies(s2, s1))
54	
55	# True exactly when one of three arbitrary predicates is true.
56	def one_hot3(first: Bool, second: Bool, third: Bool) -> Bool:
57	  match first second third:
58	    case True{} False{} False{}:
59	      True{}
60	    case False{} True{} False{}:
61	      True{}
62	    case False{} False{} True{}:
63	      True{}
64	    case _ _ _:
65	      False{}
66	
67	# Cmp is intrinsically one-hot; this predicate gives K6 a reusable statement.
68	def cmp_one_hot(+ord: Cmp) -> Bool:
69	  one_hot3(cmp_is_lt(ord), cmp_is_eq(ord), cmp_is_gt(ord))
70	
71	def cmp_one_hot_proof(+ord: Cmp) -> {cmp_one_hot(ord) == True{} : Bool}:
72	  match ord:
73	    case LT{}:
74	      {==}
75	    case EQ{}:
76	      {==}
77	    case GT{}:
78	      {==}
79	
80	# `String.eq` is defined by the EQ projection of `String.cmp`; matching the
81	# handed-back comparison pair exposes that definitional correspondence.
82	def cmp_eq_pair(pair: (String & String) & Cmp) -> {cmp_is_eq(unpack(pair)) == String.eq.fin(pair) : Bool}:
83	  match pair:
84	    case ((a, b), c):
85	      match c:
86	        case LT{}:
87	          {==}
88	        case EQ{}:
89	          {==}
90	        case GT{}:
91	          {==}
92	
93	def cmp_eq_bridge(+s1: String, +s2: String) -> {cmp_is_eq(cmp(s1, s2)) == eq(s1, s2) : Bool}:
94	  cmp_eq_pair(String.cmp(s1, s2))
95	
96	# Reflexivity chain for open keys. Every product law about keyed lookup
97	# rewrites with str_eq_refl; it rests on the layers below, down to bits.
98	# (Proving Base's own primitives is the one exception to the trust-root
99	# rule: without open-key comparison facts, NO keyed law is provable.)
100	
101	def bool_refl(+flag: Bool) -> {Bool.cmp(flag, flag) == EQ{} : Cmp}:
102	  match flag:
103	    case False{}:
104	      {==}
105	    case True{}:
106	      {==}
107	
108	def word_refl(width: Nat, +word: Word(width)) -> {Word.cmp(width, word, word) == EQ{} : Cmp}:
109	  match width word:
110	    case 0n WNil{}:
111	      {==}
112	    case 1n+p WCon{ab, at}:
113	      match ab:
114	        case False{}:
115	          %Equal.sym(Cmp, Word.cmp(p, at, at), EQ{}, word_refl(p, at)) : {Word.cmp.fin(False{}, False{}, _) == EQ{} : Cmp}
116	          {==}
117	        case True{}:
118	          %Equal.sym(Cmp, Word.cmp(p, at, at), EQ{}, word_refl(p, at)) : {Word.cmp.fin(True{}, True{}, _) == EQ{} : Cmp}
119	          {==}
120	
121	def u32_refl(+val: U32) -> {U32.cmp(val, val) == EQ{} : Cmp}:
122	  match val:
123	    case U32{w}:
124	      %Equal.sym(Cmp, Word.cmp(32n, w, w), EQ{}, word_refl(32n, w)) : {_ == EQ{} : Cmp}
125	      {==}
126	
127	def char_refl(+ch: Char) -> {Char.cmp(ch, ch) == ((ch, ch), EQ{}) : (Char & Char) & Cmp}:
128	  match ch:
129	    case Chr{x}:
130	      %Equal.sym(Cmp, U32.cmp(x, x), EQ{}, u32_refl(x)) : {((Chr{x}, Chr{x}), _) == ((Chr{x}, Chr{x}), EQ{}) : (Char & Char) & Cmp}
131	      {==}
132	
133	def s_cmp_pair_refl(+str: String) -> {String.cmp(str, str) == ((str, str), EQ{}) : (String & String) & Cmp}:
134	  match str:
135	    case SNil{}:
136	      {==}
137	    case SCon{h, t}:
138	      %Equal.sym((Char & Char) & Cmp, Char.cmp(h, h), ((h, h), EQ{}), char_refl(h)) : {String.cmp.fin(t, t, _) == ((SCon{h, t}, SCon{h, t}), EQ{}) : (String & String) & Cmp}
139	      %Equal.sym((String & String) & Cmp, String.cmp(t, t), ((t, t), EQ{}), s_cmp_pair_refl(t)) : {String.cmp.rec(h, h, _) == ((SCon{h, t}, SCon{h, t}), EQ{}) : (String & String) & Cmp}
140	      {==}
141	
142	def str_refl(+str: String) -> {cmp(str, str) == EQ{} : Cmp}:
143	  %Equal.sym((String & String) & Cmp, String.cmp(str, str), ((str, str), EQ{}), s_cmp_pair_refl(str)) : {unpack(_) == EQ{} : Cmp}
144	  {==}
145	
146	def str_eq_refl(+str: String) -> {eq(str, str) == True{} : Bool}:
147	  match str:
148	    case SNil{}:
149	      {==}
150	    case SCon{h, t}:
151	      %Equal.sym((Char & Char) & Cmp, Char.cmp(h, h), ((h, h), EQ{}), char_refl(h)) : {String.eq.fin(String.cmp.fin(t, t, _)) == True{} : Bool}
152	      %Equal.sym((String & String) & Cmp, String.cmp(t, t), ((t, t), EQ{}), s_cmp_pair_refl(t)) : {String.eq.fin(String.cmp.rec(h, h, _)) == True{} : Bool}
153	      {==}