1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/order.bend as O
4	import ../../lib/list.bend as LL
5	import ../../../spec/lib/common.bend as SC
6	import ../../../spec/containers/binary_heap.bend as S
7	
8	# Insertion-sorted lists as canonical multisets, under a total order ~o.
9	# All lemmas are templates over (~A, ~cmp, ~o); they are checked through the
10	# U32 and String instances at the end of this file and in END_TO_END.bend.
11	
12	def and_swap(+a: Bool, +b: Bool, +c: Bool) -> {Bool.and(a, Bool.and(b, c)) == Bool.and(b, Bool.and(a, c)) : Bool}:
13	  match a b:
14	    case True{} True{}:
15	      {==}
16	    case True{} False{}:
17	      {==}
18	    case False{} True{}:
19	      {==}
20	    case False{} False{}:
21	      {==}
22	
23	def ins_cons(~A: Data, ~cmp: A -> A -> Cmp, +x: A, +h: A, +t: List<&2, A>, +b: Bool, +e: {S.le(~A, ~cmp, x, h) == b : Bool}) -> {S.ins(~A, ~cmp, x, Con{h, t}) == Bool.pick(List<&2, A>, b, Con{x, Con{h, t}}, Con{h, S.ins(~A, ~cmp, x, t)}) : List<&2, A>}:
24	  %e : {S.ins(~A, ~cmp, x, Con{h, t}) == Bool.pick(List<&2, A>, _, Con{x, Con{h, t}}, Con{h, S.ins(~A, ~cmp, x, t)}) : List<&2, A>}
25	  {==}
26	
27	def all_ge_ins_c(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +z: A, +x: A, +h: A, +t: List<&2, A>, +b: Bool, +e: {S.le(~A, ~cmp, x, h) == b : Bool}, +ih: {S.all_ge(~A, ~cmp, z, S.ins(~A, ~cmp, x, t)) == Bool.and(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, t)) : Bool}) -> {S.all_ge(~A, ~cmp, z, S.ins(~A, ~cmp, x, Con{h, t})) == Bool.and(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, Con{h, t})) : Bool}:
28	  match b:
29	    case True{}:
30	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{x, Con{h, t}}, ins_cons(~A, ~cmp, x, h, t, True{}, e)) : {S.all_ge(~A, ~cmp, z, _) == Bool.and(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, Con{h, t})) : Bool}
31	      {==}
32	    case False{}:
33	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{h, S.ins(~A, ~cmp, x, t)}, ins_cons(~A, ~cmp, x, h, t, False{}, e)) : {S.all_ge(~A, ~cmp, z, _) == Bool.and(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, Con{h, t})) : Bool}
34	      %Equal.sym(Bool, S.all_ge(~A, ~cmp, z, S.ins(~A, ~cmp, x, t)), Bool.and(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, t)), ih) : {Bool.and(S.le(~A, ~cmp, z, h), _) == Bool.and(S.le(~A, ~cmp, z, x), Bool.and(S.le(~A, ~cmp, z, h), S.all_ge(~A, ~cmp, z, t))) : Bool}
35	      and_swap(S.le(~A, ~cmp, z, h), S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, t))
36	
37	def all_ge_ins(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +z: A, +x: A, +xs: List<&2, A>) -> {S.all_ge(~A, ~cmp, z, S.ins(~A, ~cmp, x, xs)) == Bool.and(S.le(~A, ~cmp, z, x), S.all_ge(~A, ~cmp, z, xs)) : Bool}:
38	  match xs:
39	    case Nil{}:
40	      {==}
41	    case Con{+h, +t}:
42	      all_ge_ins_c(~A, ~cmp, ~o, z, x, h, t, S.le(~A, ~cmp, x, h), {==}, all_ge_ins(~A, ~cmp, ~o, z, x, t))
43	
44	# A value not larger than every element goes first.
45	def ins_min(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +x: A, +xs: List<&2, A>, +h: {S.all_ge(~A, ~cmp, x, xs) == True{} : Bool}) -> {S.ins(~A, ~cmp, x, xs) == Con{x, xs} : List<&2, A>}:
46	  match xs:
47	    case Nil{}:
48	      {==}
49	    case Con{+y, +t}:
50	      %Equal.sym(Bool, S.le(~A, ~cmp, x, y), True{}, L.and_left(S.le(~A, ~cmp, x, y), S.all_ge(~A, ~cmp, x, t), h)) : {Bool.pick(List<&2, A>, _, Con{x, Con{y, t}}, Con{y, S.ins(~A, ~cmp, x, t)}) == Con{x, Con{y, t}} : List<&2, A>}
51	      {==}
52	
53	# Insertion order is irrelevant (uses totality, transitivity, antisymmetry).
54	def comm_nil(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +x: A, +y: A, +bxy: Bool, +exy: {S.le(~A, ~cmp, x, y) == bxy : Bool}, +byx: Bool, +eyx: {S.le(~A, ~cmp, y, x) == byx : Bool}) -> {S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, Nil{})) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Nil{})) : List<&2, A>}:
55	  match bxy byx:
56	    case True{} True{}:
57	      %O.le_antisym(~A, ~cmp, ~o, x, y, exy, eyx) : {S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, _, Nil{})) == S.ins(~A, ~cmp, _, S.ins(~A, ~cmp, x, Nil{})) : List<&2, A>}
58	      {==}
59	    case True{} False{}:
60	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{y, Nil{}}), Con{x, Con{y, Nil{}}}, ins_cons(~A, ~cmp, x, y, Nil{}, True{}, exy)) : {_ == S.ins(~A, ~cmp, y, Con{x, Nil{}}) : List<&2, A>}
61	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{x, Nil{}}), Con{x, Con{y, Nil{}}}, ins_cons(~A, ~cmp, y, x, Nil{}, False{}, eyx)) : {Con{x, Con{y, Nil{}}} == _ : List<&2, A>}
62	      {==}
63	    case False{} True{}:
64	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{y, Nil{}}), Con{y, Con{x, Nil{}}}, ins_cons(~A, ~cmp, x, y, Nil{}, False{}, exy)) : {_ == S.ins(~A, ~cmp, y, Con{x, Nil{}}) : List<&2, A>}
65	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{x, Nil{}}), Con{y, Con{x, Nil{}}}, ins_cons(~A, ~cmp, y, x, Nil{}, True{}, eyx)) : {Con{y, Con{x, Nil{}}} == _ : List<&2, A>}
66	      {==}
67	    case False{} False{}:
68	      Empty.absurd({S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, Nil{})) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Nil{})) : List<&2, A>}, L.true_not_false(S.le(~A, ~cmp, y, x), O.total(~A, ~cmp, ~o, x, y, exy), eyx))
69	
70	def comm_cons(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +x: A, +y: A, +h: A, +t: List<&2, A>, +bxy: Bool, +exy: {S.le(~A, ~cmp, x, y) == bxy : Bool}, +byx: Bool, +eyx: {S.le(~A, ~cmp, y, x) == byx : Bool}, +bxh: Bool, +exh: {S.le(~A, ~cmp, x, h) == bxh : Bool}, +byh: Bool, +eyh: {S.le(~A, ~cmp, y, h) == byh : Bool}, +ih: {S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t)) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, t)) : List<&2, A>}) -> {S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, Con{h, t})) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}:
71	  match bxy byx bxh byh:
72	    case False{} False{} _ _:
73	      Empty.absurd({S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, Con{h, t})) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}, L.true_not_false(S.le(~A, ~cmp, y, x), O.total(~A, ~cmp, ~o, x, y, exy), eyx))
74	    case True{} True{} _ _:
75	      %O.le_antisym(~A, ~cmp, ~o, x, y, exy, eyx) : {S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, _, Con{h, t})) == S.ins(~A, ~cmp, _, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
76	      {==}
77	    case True{} False{} True{} True{}:
78	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{y, Con{h, t}}, ins_cons(~A, ~cmp, y, h, t, True{}, eyh)) : {S.ins(~A, ~cmp, x, _) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
79	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{x, Con{h, t}}, ins_cons(~A, ~cmp, x, h, t, True{}, exh)) : {S.ins(~A, ~cmp, x, Con{y, Con{h, t}}) == S.ins(~A, ~cmp, y, _) : List<&2, A>}
80	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{y, Con{h, t}}), Con{x, Con{y, Con{h, t}}}, ins_cons(~A, ~cmp, x, y, Con{h, t}, True{}, exy)) : {_ == S.ins(~A, ~cmp, y, Con{x, Con{h, t}}) : List<&2, A>}
81	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{x, Con{h, t}}), Con{x, S.ins(~A, ~cmp, y, Con{h, t})}, ins_cons(~A, ~cmp, y, x, Con{h, t}, False{}, eyx)) : {Con{x, Con{y, Con{h, t}}} == _ : List<&2, A>}
82	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{y, Con{h, t}}, ins_cons(~A, ~cmp, y, h, t, True{}, eyh)) : {Con{x, Con{y, Con{h, t}}} == Con{x, _} : List<&2, A>}
83	      {==}
84	    case True{} False{} False{} True{}:
85	      Empty.absurd({S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, Con{h, t})) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}, L.true_not_false(S.le(~A, ~cmp, x, h), O.trans(~A, ~cmp, o, x, y, h, exy, eyh), exh))
86	    case True{} False{} True{} False{}:
87	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{h, S.ins(~A, ~cmp, y, t)}, ins_cons(~A, ~cmp, y, h, t, False{}, eyh)) : {S.ins(~A, ~cmp, x, _) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
88	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, S.ins(~A, ~cmp, y, t)}), Con{x, Con{h, S.ins(~A, ~cmp, y, t)}}, ins_cons(~A, ~cmp, x, h, S.ins(~A, ~cmp, y, t), True{}, exh)) : {_ == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
89	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{x, Con{h, t}}, ins_cons(~A, ~cmp, x, h, t, True{}, exh)) : {Con{x, Con{h, S.ins(~A, ~cmp, y, t)}} == S.ins(~A, ~cmp, y, _) : List<&2, A>}
90	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{x, Con{h, t}}), Con{x, S.ins(~A, ~cmp, y, Con{h, t})}, ins_cons(~A, ~cmp, y, x, Con{h, t}, False{}, eyx)) : {Con{x, Con{h, S.ins(~A, ~cmp, y, t)}} == _ : List<&2, A>}
91	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{h, S.ins(~A, ~cmp, y, t)}, ins_cons(~A, ~cmp, y, h, t, False{}, eyh)) : {Con{x, Con{h, S.ins(~A, ~cmp, y, t)}} == Con{x, _} : List<&2, A>}
92	      {==}
93	    case True{} False{} False{} False{}:
94	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{h, S.ins(~A, ~cmp, y, t)}, ins_cons(~A, ~cmp, y, h, t, False{}, eyh)) : {S.ins(~A, ~cmp, x, _) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
95	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, S.ins(~A, ~cmp, y, t)}), Con{h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t))}, ins_cons(~A, ~cmp, x, h, S.ins(~A, ~cmp, y, t), False{}, exh)) : {_ == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
96	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{h, S.ins(~A, ~cmp, x, t)}, ins_cons(~A, ~cmp, x, h, t, False{}, exh)) : {Con{h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t))} == S.ins(~A, ~cmp, y, _) : List<&2, A>}
97	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, S.ins(~A, ~cmp, x, t)}), Con{h, S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, t))}, ins_cons(~A, ~cmp, y, h, S.ins(~A, ~cmp, x, t), False{}, eyh)) : {Con{h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t))} == _ : List<&2, A>}
98	      LL.cons_cong(A, h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t)), S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, t)), ih)
99	    case False{} True{} True{} True{}:
100	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{y, Con{h, t}}, ins_cons(~A, ~cmp, y, h, t, True{}, eyh)) : {S.ins(~A, ~cmp, x, _) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
101	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{y, Con{h, t}}), Con{y, S.ins(~A, ~cmp, x, Con{h, t})}, ins_cons(~A, ~cmp, x, y, Con{h, t}, False{}, exy)) : {_ == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
102	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{x, Con{h, t}}, ins_cons(~A, ~cmp, x, h, t, True{}, exh)) : {Con{y, _} == S.ins(~A, ~cmp, y, _) : List<&2, A>}
103	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{x, Con{h, t}}), Con{y, Con{x, Con{h, t}}}, ins_cons(~A, ~cmp, y, x, Con{h, t}, True{}, eyx)) : {Con{y, Con{x, Con{h, t}}} == _ : List<&2, A>}
104	      {==}
105	    case False{} True{} False{} True{}:
106	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{y, Con{h, t}}, ins_cons(~A, ~cmp, y, h, t, True{}, eyh)) : {S.ins(~A, ~cmp, x, _) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
107	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{y, Con{h, t}}), Con{y, S.ins(~A, ~cmp, x, Con{h, t})}, ins_cons(~A, ~cmp, x, y, Con{h, t}, False{}, exy)) : {_ == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
108	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{h, S.ins(~A, ~cmp, x, t)}, ins_cons(~A, ~cmp, x, h, t, False{}, exh)) : {Con{y, _} == S.ins(~A, ~cmp, y, _) : List<&2, A>}
109	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, S.ins(~A, ~cmp, x, t)}), Con{y, Con{h, S.ins(~A, ~cmp, x, t)}}, ins_cons(~A, ~cmp, y, h, S.ins(~A, ~cmp, x, t), True{}, eyh)) : {Con{y, Con{h, S.ins(~A, ~cmp, x, t)}} == _ : List<&2, A>}
110	      {==}
111	    case False{} True{} True{} False{}:
112	      Empty.absurd({S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, Con{h, t})) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}, L.true_not_false(S.le(~A, ~cmp, y, h), O.trans(~A, ~cmp, o, y, x, h, eyx, exh), eyh))
113	    case False{} True{} False{} False{}:
114	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, t}), Con{h, S.ins(~A, ~cmp, y, t)}, ins_cons(~A, ~cmp, y, h, t, False{}, eyh)) : {S.ins(~A, ~cmp, x, _) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
115	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, S.ins(~A, ~cmp, y, t)}), Con{h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t))}, ins_cons(~A, ~cmp, x, h, S.ins(~A, ~cmp, y, t), False{}, exh)) : {_ == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, Con{h, t})) : List<&2, A>}
116	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, x, Con{h, t}), Con{h, S.ins(~A, ~cmp, x, t)}, ins_cons(~A, ~cmp, x, h, t, False{}, exh)) : {Con{h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t))} == S.ins(~A, ~cmp, y, _) : List<&2, A>}
117	      %Equal.sym(List<&2, A>, S.ins(~A, ~cmp, y, Con{h, S.ins(~A, ~cmp, x, t)}), Con{h, S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, t))}, ins_cons(~A, ~cmp, y, h, S.ins(~A, ~cmp, x, t), False{}, eyh)) : {Con{h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t))} == _ : List<&2, A>}
118	      LL.cons_cong(A, h, S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, t)), S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, t)), ih)
119	
120	def ins_comm(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +x: A, +y: A, +s: List<&2, A>) -> {S.ins(~A, ~cmp, x, S.ins(~A, ~cmp, y, s)) == S.ins(~A, ~cmp, y, S.ins(~A, ~cmp, x, s)) : List<&2, A>}:
121	  match s:
122	    case Nil{}:
123	      comm_nil(~A, ~cmp, ~o, x, y, S.le(~A, ~cmp, x, y), {==}, S.le(~A, ~cmp, y, x), {==})
124	    case Con{+h, +t}:
125	      comm_cons(~A, ~cmp, ~o, x, y, h, t, S.le(~A, ~cmp, x, y), {==}, S.le(~A, ~cmp, y, x), {==}, S.le(~A, ~cmp, x, h), {==}, S.le(~A, ~cmp, y, h), {==}, ins_comm(~A, ~cmp, ~o, x, y, t))