1	import Base
2	import ../../../lib/logic.bend as L
3	import ../../../lib/nat.bend as N
4	import ../../../../spec/lib/common.bend as SC
5	
6	# List and arithmetic facts used by the tree proof (generic over the element
7	# type, on the spec/common list functions).
8	
9	def cons_cong(-A: Data, +h: A, +xs: List<&2,A>, +ys: List<&2,A>, e: {xs == ys : List<&2,A>}) -> {Con{h,xs} == Con{h,ys} : List<&2,A>}:
10	  Equal.cong(List<&2,A>,List<&2,A>,zs => Con{h,zs},xs,ys,e)
11	
12	def take_drop(-A: Data, +xs: List<&2,A>, +k: Nat) -> {SC.append(A,SC.take(A,xs,k),SC.drop(A,xs,k)) == xs : List<&2,A>}:
13	  match xs k:
14	    case Nil{} _: {==}
15	    case Con{+h,+t} 0n: {==}
16	    case Con{+h,+t} 1n+j: cons_cong(A,h,SC.append(A,SC.take(A,t,j),SC.drop(A,t,j)),t,take_drop(A,t,j))
17	
18	def length_drop(-A: Data, +xs: List<&2,A>, +k: Nat) -> {SC.length(A,SC.drop(A,xs,k)) == Nat.sub(SC.length(A,xs),k) : Nat}:
19	  match xs k:
20	    case Nil{} 0n: {==}
21	    case Nil{} 1n+j: {==}
22	    case Con{+h,+t} 0n: {==}
23	    case Con{+h,+t} 1n+j: length_drop(A,t,j)
24	
25	def take_all(-A: Data, +xs: List<&2,A>, +k: Nat, +h: {Nat.is_le(SC.length(A,xs),k) == True{} : Bool}) -> {SC.take(A,xs,k) == xs : List<&2,A>}:
26	  match xs k:
27	    case Nil{} _: {==}
28	    case Con{+a,+t} 0n: Empty.absurd({SC.take(A,Con{a,t},0n) == Con{a,t} : List<&2,A>},L.false_true(h))
29	    case Con{+a,+t} 1n+j: cons_cong(A,a,SC.take(A,t,j),t,take_all(A,t,j,h))
30	
31	def drop_all(-A: Data, +xs: List<&2,A>, +k: Nat, +h: {Nat.is_le(SC.length(A,xs),k) == True{} : Bool}) -> {SC.drop(A,xs,k) == Nil{} : List<&2,A>}:
32	  match xs k:
33	    case Nil{} _: {==}
34	    case Con{+a,+t} 0n: Empty.absurd({SC.drop(A,Con{a,t},0n) == Nil{} : List<&2,A>},L.false_true(h))
35	    case Con{+a,+t} 1n+j: drop_all(A,t,j,h)
36	
37	def drop_zero(-A: Data, +ys: List<&2,A>) -> {SC.drop(A,ys,0n) == ys : List<&2,A>}:
38	  match ys:
39	    case Nil{}: {==}
40	    case Con{+b,+u}: {==}
41	
42	def take_zero(-A: Data, +ys: List<&2,A>) -> {SC.take(A,ys,0n) == Nil{} : List<&2,A>}:
43	  match ys:
44	    case Nil{}: {==}
45	    case Con{+b,+u}: {==}
46	
47	def drop_append_left(-A: Data, +xs: List<&2,A>, +ys: List<&2,A>, +k: Nat, +h: {Nat.is_le(k,SC.length(A,xs)) == True{} : Bool}) -> {SC.drop(A,SC.append(A,xs,ys),k) == SC.append(A,SC.drop(A,xs,k),ys) : List<&2,A>}:
48	  match xs k:
49	    case Nil{} 0n: drop_zero(A,ys)
50	    case Nil{} 1n+j: Empty.absurd({SC.drop(A,ys,1n+j) == ys : List<&2,A>},L.false_true(h))
51	    case Con{+a,+t} 0n: {==}
52	    case Con{+a,+t} 1n+j: drop_append_left(A,t,ys,j,h)
53	
54	def take_append_left(-A: Data, +xs: List<&2,A>, +ys: List<&2,A>, +k: Nat, +h: {Nat.is_le(k,SC.length(A,xs)) == True{} : Bool}) -> {SC.take(A,SC.append(A,xs,ys),k) == SC.take(A,xs,k) : List<&2,A>}:
55	  match xs k:
56	    case Nil{} 0n: take_zero(A,ys)
57	    case Nil{} 1n+j: Empty.absurd({SC.take(A,ys,1n+j) == Nil{} : List<&2,A>},L.false_true(h))
58	    case Con{+a,+t} 0n: {==}
59	    case Con{+a,+t} 1n+j: cons_cong(A,a,SC.take(A,SC.append(A,t,ys),j),SC.take(A,t,j),take_append_left(A,t,ys,j,h))
60	
61	def length_take(-A: Data, +xs: List<&2,A>, +k: Nat, +h: {Nat.is_le(k,SC.length(A,xs)) == True{} : Bool}) -> {SC.length(A,SC.take(A,xs,k)) == k : Nat}:
62	  match xs k:
63	    case Nil{} 0n: {==}
64	    case Nil{} 1n+j: Empty.absurd({SC.length(A,SC.take(A,Nil{},1n+j)) == 1n+j : Nat},L.false_true(h))
65	    case Con{+a,+t} 0n: {==}
66	    case Con{+a,+t} 1n+j: N.succ_cong(SC.length(A,SC.take(A,t,j)),j,length_take(A,t,j,h))
67	
68	def length_snoc(-A: Data, +xs: List<&2,A>, +x: A) -> {SC.length(A,SC.append(A,xs,Con{x,Nil{}})) == 1n+SC.length(A,xs) : Nat}:
69	  match xs:
70	    case Nil{}: {==}
71	    case Con{+a,+t}: N.succ_cong(SC.length(A,SC.append(A,t,Con{x,Nil{}})),1n+SC.length(A,t),length_snoc(A,t,x))
72	
73	def is_empty(-A: Data, xs: List<&2,A>) -> Bool:
74	  match xs:
75	    case Nil{}: True{}
76	    case Con{a,t}: False{}
77	
78	def empty_drop(-A: Data, +xs: List<&2,A>, +k: Nat) -> {is_empty(A,SC.drop(A,xs,k)) == Nat.is_le(SC.length(A,xs),k) : Bool}:
79	  match xs k:
80	    case Nil{} 0n: {==}
81	    case Nil{} 1n+j: {==}
82	    case Con{+a,+t} 0n: {==}
83	    case Con{+a,+t} 1n+j: empty_drop(A,t,j)
84	
85	def double_add(+p: Nat) -> {Nat.double(p) == Nat.add(p,p) : Nat}:
86	  match p:
87	    case 0n: {==}
88	    case 1n+q:
89	      %Equal.sym(Nat,Nat.add(q,1n+q),1n+Nat.add(q,q),N.add_succ(q,q)) : {2n+Nat.double(q) == 1n+_ : Nat}
90	      N.succ_cong(1n+Nat.double(q),1n+Nat.add(q,q),N.succ_cong(Nat.double(q),Nat.add(q,q),double_add(q)))
91	
92	def sub_double(+p: Nat) -> {Nat.sub(Nat.double(p),p) == p : Nat}:
93	  %Equal.sym(Nat,Nat.double(p),Nat.add(p,p),double_add(p)) : {Nat.sub(_,p) == p : Nat}
94	  N.add_sub_cancel(p,p)
95	
96	# 2^h is strictly above h - 1, i.e. n < 2^(n+1).
97	def lt_pow2(+n: Nat) -> {Nat.is_lt(n,SC.pow2(n)) == True{} : Bool}:
98	  match n:
99	    case 0n: {==}
100	    case 1n+q:
101	      N.lt_le_trans(1n+q,1n+SC.pow2(q),Nat.double(SC.pow2(q)),lt_pow2(q),N.double_succ_le(SC.pow2(q),N.pow2_pos(q)))
102	
103	def lt_pow2_succ(+n: Nat) -> {Nat.is_lt(n,SC.pow2(1n+n)) == True{} : Bool}:
104	  N.lt_trans(n,SC.pow2(n),SC.pow2(1n+n),lt_pow2(n),N.pow2_lt_succ(n))