1	import Base
2	import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/string_compare.bend as Compare
3	
4	def false_type(b: Bool) -> Data:
5	    match b:
6	        case False{}: Unit
7	        case True{}: Empty
8	
9	def false_true(e: {False{} == True{} : Bool}) -> Empty:
10	    %e : false_type(_)
11	    Unit{}
12	
13	def cmp_eq_of_true(c: Cmp,
14	    accepted: {Cmp.is_eq(c) == True{} : Bool}) -> {c == EQ{} : Cmp}:
15	    match c:
16	        case EQ{}: {==}
17	        case LT{}: Empty.absurd({LT{} == EQ{} : Cmp}, false_true(accepted))
18	        case GT{}: Empty.absurd({GT{} == EQ{} : Cmp}, false_true(accepted))
19	
20	def tag_is_snd(r: (String & String) & Cmp) ->
21	    {Compare.comparison_tag(String, r) ==
22	     Pair.snd(String & String, Cmp, r) : Cmp}:
23	    match r:
24	        case ((a, b), c): {==}
25	
26	def string_eq_sound(+a: String, +b: String,
27	    accepted: {String.eq(a, b) == True{} : Bool}) -> {a == b : String}:
28	    Compare.string_equal_from_comparison(a, b,
29	        Equal.trans(Cmp,
30	            Compare.comparison_tag(String, String.cmp(a, b)),
31	            String.order(a, b), EQ{},
32	            tag_is_snd(String.cmp(a, b)),
33	            cmp_eq_of_true(String.order(a, b), accepted)))
34	
35	def string_eq_self(+s: String) ->
36	    {String.eq(s, s) == True{} : Bool}:
37	    Equal.cong((String & String) & Cmp, Bool,
38	        result => Cmp.is_eq(Pair.snd(String & String, Cmp, result)),
39	        String.cmp(s, s), ((s, s), EQ{}),
40	        Compare.string_compare_self(s))