Nuprl - mb_list

Origin Definitions Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb_list_2Nuprl Section: mb_list_2 - More list stuff from Mark Bickford.

Selected Objects
def l_disjoint l_disjoint(T;l1;l2) == x:T. ((x  l1) & (x  l2))

def l_all (xL.P(x)) == x:T. (x  L)  P(x)

THM l_all_cons P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x) & (yL.P(y))

THM filter_trivial P:(T), L:T List. (xL.P(x))  (filter(P;L) ~ L)

THM filter_trivial2 P:(T), L:T List. (xL.P(x))  filter(P;L) = L

THM filter_is_nil P:(T), L:T List. (xL.P(x))  (filter(P;L) ~ nil)

THM list_set_type L:T List, P:(TProp). (xL.P(x))  L  {x:T| P(x) } List

THM l_all_map f:(AB), L:A List, P:(BProp). (xmap(f;L).P(x))  (xL.P(f(x)))

THM l_all_nil P:(TProp). (xnil.P(x))

THM l_all_reduce L:T List, P:(T). (xL.P(x))  reduce(x,y. P(x)y;true;L)

THM sublist_filter L1,L2:T List, P:(T). L2  filter(P;L1)  L2  L1 & (xL2.P(x))

THM l_before_filter l:T List, P:(T), x,y:T.
x before y  filter(P;l)  P(x) & P(y) & x before y  l

THM no_repeats_filter P:(T), l:T List. no_repeats(T;l)  no_repeats(T;filter(P;l))

THM decidable__l_all F:(AProp), L:A List. (k:A. Dec(F(k)))  Dec((kL.F(k)))

def l_exists (xL.P(x)) == x:T. (x  L) & P(x)

THM l_exists_nil P:(TProp). (xnil.P(x))  False

THM l_exists_cons P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x)  (yL.P(y))

THM decidable__l_exists F:(AProp), L:A List. (k:A. Dec(F(k)))  Dec((kL.F(k)))

def mapfilter mapfilter(f;P;L) == map(f;filter(P;L))

THM member_map_filter P:(T), T':Type, f:({x:T| P(x) }T'), L:T List, x:T'.
(x  mapfilter(f;P;L))  (y:T. (y  L) & P(y) & x = f(y))

def sublist_occurence sublist_occurence(T;L1;L2;f)
== increasing(f;||L1||) & (j:||L1||. L1[j] = L2[(f(j))]  T)

THM range_sublist L:T List, n:, f:(n||L||).
increasing(f;n)  (L1:T List. ||L1|| = n   & sublist_occurence(T;L1;L;f))

def disjoint_sublists disjoint_sublists(T;L1;L2;L)
== f1:(||L1||||L||), f2:(||L2||||L||).
== increasing(f1;||L1||) & (j:||L1||. L1[j] = L[(f1(j))]  T)
== & increasing(f2;||L2||) & (j:||L2||. L2[j] = L[(f2(j))]  T)
== & (j1:||L1||, j2:||L2||. f1(j1) = f2(j2))

THM disjoint_sublists_sublist L1,L2,L:T List. disjoint_sublists(T;L1;L2;L)  L1  L & L2  L

def interleaving interleaving(T;L1;L2;L)
== ||L|| = ||L1||+||L2||   & disjoint_sublists(T;L1;L2;L)

THM nil_interleaving L1,L:T List. interleaving(T;nil;L1;L)  L = L1

THM nil_interleaving2 L1,L:T List. interleaving(T;L1;nil;L)  L = L1

THM interleaving_sublist L,L1,L2:T List. interleaving(T;L1;L2;L)  L1  L

def interleaving_occurence interleaving_occurence(T;L1;L2;L;f1;f2)
== ||L|| = ||L1||+||L2||
== & increasing(f1;||L1||) & (j:||L1||. L1[j] = L[(f1(j))]  T)
== & increasing(f2;||L2||) & (j:||L2||. L2[j] = L[(f2(j))]  T)
== & (j1:||L1||, j2:||L2||. f1(j1) = f2(j2)  )

THM interleaving_split L:T List, P:(||L||Prop).
(x:||L||. Dec(P(x)))

(L1,L2:T List, f1:(||L1||||L||), f2:(||L2||||L||).
(interleaving_occurence(T;L1;L2;L;f1;f2)
(& (i:||L1||. P(f1(i))) & (i:||L2||. P(f2(i)))
(& (i:||L||.
(& ((P(i)  (j:||L1||. f1(j) = i)) & (P(i)  (j:||L2||. f2(j) = i))))

THM last_with_property L:T List, P:(||L||Prop).
(x:||L||. Dec(P(x)))

(i:||L||. P(i))  (i:||L||. P(i) & (j:||L||. i<j  P(j)))

def permute_list (L o f) == mklist(||L||;i.L[(f(i))])

THM permute_list_select L:T List, f:(||L||||L||), i:||L||. (L o f)[i] = L[(f(i))]

THM permute_list_length L:T List, f:(||L||||L||). ||(L o f)|| = ||L||

def swap swap(L;i;j) == (L o (i, j))

THM swap_select L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))]

THM swap_length L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||

THM swap_swap L1:T List, i,j:||L1||. swap(swap(L1;i;j);i;j) = L1

THM swapped_select L1,L2:T List, i,j:||L1||.
L2 = swap(L1;i;j)

L2[i] = L1[j] & L2[j] = L1[i] & ||L2|| = ||L1||   & L1 = swap(L2;i;j)
& (x:||L2||. x = i  x = j  L2[x] = L1[x])

THM swap_cons L:T List, x:T, i,j:{1..(||L||+1)}. swap([x / L];i;j) = [x / swap(L;i-1;j-1)]

THM swap_adjacent_decomp i:, L:A List.
i+1<||L||

(X,Y:A List.
(L = (X @ [L[i]; L[(i+1)]] @ Y) & swap(L;i;i+1) = (X @ [L[(i+1)]; L[i]] @ Y))

THM l_before_swap L:T List, i:(||L||-1), a,b:T.
a before b  swap(L;i;i+1)  a before b  L  a = L[(i+1)] & b = L[i]

THM map_swap f:(BA), x:B List, i,j:||x||. map(f;swap(x;i;j)) = swap(map(f;x);i;j)

def guarded_permutation guarded_permutation(T;P)
== (L1,L2. i:(||L1||-1). P(L1,i) & L2 = swap(L1;i;i+1)  T List)^*

THM guarded_permutation_transitivity P:(L:(T List)(||L||-1)Prop). Trans(T List)(_1 guarded_permutation(T;P) _2)

def count_pairs count(x < y in L | P(x;y))
== sum(if (i<j)P(L[i];L[j]) 1 else 0 fi | i < ||L||; j < ||L||)

THM iseg_map f:(AB), L1,L2:A List. L1  L2  map(f;L1)  map(f;L2)

THM partial_sort_exists P:(L:(T List)(||L||-1)), m:((T List)).
(L:T List, i:(||L||-1). P(L,i)  P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L))

(L:T List.
(L':T List.
((L guarded_permutation(T;L,i. P(L,i)) L') & (i:(||L'||-1). P(L',i)))

THM compose_bij f,g:(TT). Bij(T; T; f)  Bij(T; T; g)  Bij(T; T; f o g)

THM rel_exp_list R:(TTProp), k:, x,y:T.
(x R^k y)

(L:T List. ||L|| = k+1   & L[0] = x & last(L) = y & (i:k. L[i] R L[(i+1)]))

THM rel_star_finite n:, R:(nnProp), x,y:n. (x (R^*) y)  (k:(n+1). x R^k y)

THM decidable__rel_star n:, R:(nnProp). (i,j:n. Dec(i R j))  (i,j:n. Dec(i (R^*) j))

def compose_list compose_list(L) == reduce(p,q. p o q;x.x;L)

THM compose_append L1,L2:(TT) List. compose_list(L1) o compose_list(L2) = compose_list(L1 @ L2)

THM flip_lemma k:, x,y,z:k.
y = z  x = y  (x, y) = compose_list([(x, z); (y, z); (x, z)])

def compose_flips compose_flips(L) == compose_list(map(i.(i, i+1);L))

THM compose_flips_append k:, L1,L2:(k-1) List.
compose_flips(L1) o compose_flips(L2) = compose_flips(L1 @ L2)

THM flip_adjacent k:, x,y:k. L:(k-1) List. (x, y) = compose_flips(L)

THM permute_by_flips k:, p:(kk). Bij(k; k; p)  (L:(k-1) List. p = compose_flips(L))

THM permute_sum n:, f:(n), p:(nn).
Bij(n; n; p)  sum(f(p(x)) | x < n) = sum(f(x) | x < n)

THM permute_double_sum n,m:, f:(nm), p:(nn), q:(mm).
Bij(n; n; p)

Bij(m; m; q)  sum(f(p(x),q(y)) | x < n; y < m) = sum(f(x,y) | x < n; y < m)

THM count_pairs_swap L:T List, P:(TT), n:(||L||-1).
count(x < y in swap(L;n;n+1) | P(x,y))
=
count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi
+if P(L[(n+1)],L[n]) 1 else 0 fi

THM partial_sort_exists_2 L:T List, P:(TT).
(x,y:T. P(x,y)  P(y,x))

(L':T List.
((L guarded_permutation(T;L,i. P(L[i],L[(i+1)])) L')
(& (i:(||L'||-1). P(L'[i],L'[(i+1)])))

def swap_adjacent swap adjacent[P(x;y)](L1,L2)
== i:(||L1||-1). P(L1[i];L1[(i+1)]) & L2 = swap(L1;i;i+1)  A List

THM partial_sort L:T List, P:(TTProp).
(x,y:T. Dec(P(x,y)))

(x,y:T. P(x,y)  P(y,x))

(L':T List.
((L (swap adjacent[P(x,y)]^*) L') & (i:(||L'||-1). P(L'[i],L'[(i+1)])))

THM symmetric_swap_adjacent P:(AAProp).
(Sym x,y:A. P(x,y))  (Sym L1,L2:A List. L1 swap adjacent[P(x,y)] L2)

THM swap_adjacent_instance P:(AAProp), X,Y:A List, a,b:A.
P(a,b)  ((X @ [a; b] @ Y) swap adjacent[P(x,y)] (X @ [b; a] @ Y))

THM filter_swap_adjacent P:(AAProp), f:(A), L1,L2:A List.
(L1 swap adjacent[P(x,y)] L2)

(filter(f;L1) swap adjacent[P(x,y)] filter(f;L2))  filter(f;L1) = filter(f;L2)

THM swap_adjacent_map P:(AAProp), f:(BA), x,y:B List.
(x swap adjacent[P(f(x),f(y))] y)  (map(f;x) swap adjacent[P(x,y)] map(f;y))

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Selected Objects
def	l_disjoint	l_disjoint(T;l1;l2) == x:T. ((x l1) & (x l2))
def	l_all	(xL.P(x)) == x:T. (x L) P(x)
THM	l_all_cons	P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y))
THM	filter_trivial	P:(T), L:T List. (xL.P(x)) (filter(P;L) ~ L)
THM	filter_trivial2	P:(T), L:T List. (xL.P(x)) filter(P;L) = L
THM	filter_is_nil	P:(T), L:T List. (xL.P(x)) (filter(P;L) ~ nil)
THM	list_set_type	L:T List, P:(TProp). (xL.P(x)) L {x:T\| P(x) } List
THM	l_all_map	f:(AB), L:A List, P:(BProp). (xmap(f;L).P(x)) (xL.P(f(x)))
THM	l_all_nil	P:(TProp). (xnil.P(x))
THM	l_all_reduce	L:T List, P:(T). (xL.P(x)) reduce(x,y. P(x)y;true;L)
THM	sublist_filter	L1,L2:T List, P:(T). L2 filter(P;L1) L2 L1 & (xL2.P(x))
THM	l_before_filter	l:T List, P:(T), x,y:T. x before y filter(P;l) P(x) & P(y) & x before y l
THM	no_repeats_filter	P:(T), l:T List. no_repeats(T;l) no_repeats(T;filter(P;l))
THM	decidable__l_all	F:(AProp), L:A List. (k:A. Dec(F(k))) Dec((kL.F(k)))
def	l_exists	(xL.P(x)) == x:T. (x L) & P(x)
THM	l_exists_nil	P:(TProp). (xnil.P(x)) False
THM	l_exists_cons	P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) (yL.P(y))
THM	decidable__l_exists	F:(AProp), L:A List. (k:A. Dec(F(k))) Dec((kL.F(k)))
def	mapfilter	mapfilter(f;P;L) == map(f;filter(P;L))
THM	member_map_filter	P:(T), T':Type, f:({x:T\| P(x) }T'), L:T List, x:T'. (x mapfilter(f;P;L)) (y:T. (y L) & P(y) & x = f(y))
def	sublist_occurence	sublist_occurence(T;L1;L2;f) == increasing(f;\|\|L1\|\|) & (j:\|\|L1\|\|. L1[j] = L2[(f(j))] T)
THM	range_sublist	L:T List, n:, f:(n\|\|L\|\|). increasing(f;n) (L1:T List. \|\|L1\|\| = n & sublist_occurence(T;L1;L;f))
def	disjoint_sublists	disjoint_sublists(T;L1;L2;L) == f1:(\|\|L1\|\|\|\|L\|\|), f2:(\|\|L2\|\|\|\|L\|\|). == increasing(f1;\|\|L1\|\|) & (j:\|\|L1\|\|. L1[j] = L[(f1(j))] T) == & increasing(f2;\|\|L2\|\|) & (j:\|\|L2\|\|. L2[j] = L[(f2(j))] T) == & (j1:\|\|L1\|\|, j2:\|\|L2\|\|. f1(j1) = f2(j2))
THM	disjoint_sublists_sublist	L1,L2,L:T List. disjoint_sublists(T;L1;L2;L) L1 L & L2 L
def	interleaving	interleaving(T;L1;L2;L) == \|\|L\|\| = \|\|L1\|\|+\|\|L2\|\| & disjoint_sublists(T;L1;L2;L)
THM	nil_interleaving	L1,L:T List. interleaving(T;nil;L1;L) L = L1
THM	nil_interleaving2	L1,L:T List. interleaving(T;L1;nil;L) L = L1
THM	interleaving_sublist	L,L1,L2:T List. interleaving(T;L1;L2;L) L1 L
def	interleaving_occurence	interleaving_occurence(T;L1;L2;L;f1;f2) == \|\|L\|\| = \|\|L1\|\|+\|\|L2\|\| == & increasing(f1;\|\|L1\|\|) & (j:\|\|L1\|\|. L1[j] = L[(f1(j))] T) == & increasing(f2;\|\|L2\|\|) & (j:\|\|L2\|\|. L2[j] = L[(f2(j))] T) == & (j1:\|\|L1\|\|, j2:\|\|L2\|\|. f1(j1) = f2(j2) )
THM	interleaving_split	L:T List, P:(\|\|L\|\|Prop). (x:\|\|L\|\|. Dec(P(x))) (L1,L2:T List, f1:(\|\|L1\|\|\|\|L\|\|), f2:(\|\|L2\|\|\|\|L\|\|). (interleaving_occurence(T;L1;L2;L;f1;f2) (& (i:\|\|L1\|\|. P(f1(i))) & (i:\|\|L2\|\|. P(f2(i))) (& (i:\|\|L\|\|. (& ((P(i) (j:\|\|L1\|\|. f1(j) = i)) & (P(i) (j:\|\|L2\|\|. f2(j) = i))))
THM	last_with_property	L:T List, P:(\|\|L\|\|Prop). (x:\|\|L\|\|. Dec(P(x))) (i:\|\|L\|\|. P(i)) (i:\|\|L\|\|. P(i) & (j:\|\|L\|\|. i<j P(j)))
def	permute_list	(L o f) == mklist(\|\|L\|\|;i.L[(f(i))])
THM	permute_list_select	L:T List, f:(\|\|L\|\|\|\|L\|\|), i:\|\|L\|\|. (L o f)[i] = L[(f(i))]
THM	permute_list_length	L:T List, f:(\|\|L\|\|\|\|L\|\|). \|\|(L o f)\|\| = \|\|L\|\|
def	swap	swap(L;i;j) == (L o (i, j))
THM	swap_select	L:T List, i,j,x:\|\|L\|\|. swap(L;i;j)[x] = L[((i, j)(x))]
THM	swap_length	L:T List, i,j:\|\|L\|\|. \|\|swap(L;i;j)\|\| = \|\|L\|\|
THM	swap_swap	L1:T List, i,j:\|\|L1\|\|. swap(swap(L1;i;j);i;j) = L1
THM	swapped_select	L1,L2:T List, i,j:\|\|L1\|\|. L2 = swap(L1;i;j) L2[i] = L1[j] & L2[j] = L1[i] & \|\|L2\|\| = \|\|L1\|\| & L1 = swap(L2;i;j) & (x:\|\|L2\|\|. x = i x = j L2[x] = L1[x])
THM	swap_cons	L:T List, x:T, i,j:{1..(\|\|L\|\|+1)}. swap([x / L];i;j) = [x / swap(L;i-1;j-1)]
THM	swap_adjacent_decomp	i:, L:A List. i+1<\|\|L\|\| (X,Y:A List. (L = (X @ [L[i]; L[(i+1)]] @ Y) & swap(L;i;i+1) = (X @ [L[(i+1)]; L[i]] @ Y))
THM	l_before_swap	L:T List, i:(\|\|L\|\|-1), a,b:T. a before b swap(L;i;i+1) a before b L a = L[(i+1)] & b = L[i]
THM	map_swap	f:(BA), x:B List, i,j:\|\|x\|\|. map(f;swap(x;i;j)) = swap(map(f;x);i;j)
def	guarded_permutation	guarded_permutation(T;P) == (L1,L2. i:(\|\|L1\|\|-1). P(L1,i) & L2 = swap(L1;i;i+1) T List)^*
THM	guarded_permutation_transitivity	P:(L:(T List)(\|\|L\|\|-1)Prop). Trans(T List)(_1 guarded_permutation(T;P) _2)
def	count_pairs	count(x < y in L \| P(x;y)) == sum(if (i<j)P(L[i];L[j]) 1 else 0 fi \| i < \|\|L\|\|; j < \|\|L\|\|)
THM	iseg_map	f:(AB), L1,L2:A List. L1 L2 map(f;L1) map(f;L2)
THM	partial_sort_exists	P:(L:(T List)(\|\|L\|\|-1)), m:((T List)). (L:T List, i:(\|\|L\|\|-1). P(L,i) P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L)) (L:T List. (L':T List. ((L guarded_permutation(T;L,i. P(L,i)) L') & (i:(\|\|L'\|\|-1). P(L',i)))
THM	compose_bij	f,g:(TT). Bij(T; T; f) Bij(T; T; g) Bij(T; T; f o g)
THM	rel_exp_list	R:(TTProp), k:, x,y:T. (x R^k y) (L:T List. \|\|L\|\| = k+1 & L[0] = x & last(L) = y & (i:k. L[i] R L[(i+1)]))
THM	rel_star_finite	n:, R:(nnProp), x,y:n. (x (R^*) y) (k:(n+1). x R^k y)
THM	decidable__rel_star	n:, R:(nnProp). (i,j:n. Dec(i R j)) (i,j:n. Dec(i (R^*) j))
def	compose_list	compose_list(L) == reduce(p,q. p o q;x.x;L)
THM	compose_append	L1,L2:(TT) List. compose_list(L1) o compose_list(L2) = compose_list(L1 @ L2)
THM	flip_lemma	k:, x,y,z:k. y = z x = y (x, y) = compose_list([(x, z); (y, z); (x, z)])
def	compose_flips	compose_flips(L) == compose_list(map(i.(i, i+1);L))
THM	compose_flips_append	k:, L1,L2:(k-1) List. compose_flips(L1) o compose_flips(L2) = compose_flips(L1 @ L2)
THM	flip_adjacent	k:, x,y:k. L:(k-1) List. (x, y) = compose_flips(L)
THM	permute_by_flips	k:, p:(kk). Bij(k; k; p) (L:(k-1) List. p = compose_flips(L))
THM	permute_sum	n:, f:(n), p:(nn). Bij(n; n; p) sum(f(p(x)) \| x < n) = sum(f(x) \| x < n)
THM	permute_double_sum	n,m:, f:(nm), p:(nn), q:(mm). Bij(n; n; p) Bij(m; m; q) sum(f(p(x),q(y)) \| x < n; y < m) = sum(f(x,y) \| x < n; y < m)
THM	count_pairs_swap	L:T List, P:(TT), n:(\|\|L\|\|-1). count(x < y in swap(L;n;n+1) \| P(x,y)) = count(x < y in L \| P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi +if P(L[(n+1)],L[n]) 1 else 0 fi
THM	partial_sort_exists_2	L:T List, P:(TT). (x,y:T. P(x,y) P(y,x)) (L':T List. ((L guarded_permutation(T;L,i. P(L[i],L[(i+1)])) L') (& (i:(\|\|L'\|\|-1). P(L'[i],L'[(i+1)])))
def	swap_adjacent	swap adjacent[P(x;y)](L1,L2) == i:(\|\|L1\|\|-1). P(L1[i];L1[(i+1)]) & L2 = swap(L1;i;i+1) A List
THM	partial_sort	L:T List, P:(TTProp). (x,y:T. Dec(P(x,y))) (x,y:T. P(x,y) P(y,x)) (L':T List. ((L (swap adjacent[P(x,y)]^*) L') & (i:(\|\|L'\|\|-1). P(L'[i],L'[(i+1)])))
THM	symmetric_swap_adjacent	P:(AAProp). (Sym x,y:A. P(x,y)) (Sym L1,L2:A List. L1 swap adjacent[P(x,y)] L2)
THM	swap_adjacent_instance	P:(AAProp), X,Y:A List, a,b:A. P(a,b) ((X @ [a; b] @ Y) swap adjacent[P(x,y)] (X @ [b; a] @ Y))
THM	filter_swap_adjacent	P:(AAProp), f:(A), L1,L2:A List. (L1 swap adjacent[P(x,y)] L2) (filter(f;L1) swap adjacent[P(x,y)] filter(f;L2)) filter(f;L1) = filter(f;L2)
THM	swap_adjacent_map	P:(AAProp), f:(BA), x,y:B List. (x swap adjacent[P(f(x),f(y))] y) (map(f;x) swap adjacent[P(x,y)] map(f;y))

Origin Definitions Sections MarkB generic Doc