************ LIST_0 ************
The list type used to be a primitive, but now
we define it using the rec-type and unit, union, and product types.
The list_ind operator is defined by recursion,
and cons and nil are just pair and Axiom.
====================
BASIC LIST FUNCTIONS
====================
Type-checking naturally partial list functions
can be rather onerous. Therefore when possible
I've made functions more total than they need to
be. Also, to simplify life for type checking
I've made it so that all length restrictions are
spun off as separate subgoals and avoided having
multiple wf lemmas giving types both in List and
List(n).⋅⋅
Lemma: isaxiom_wf_listunion
∀[A,B:Type]. ∀[L:Unit ⋃ (A × B)]. (isaxiom(L) ∈ 𝔹)
Lemma: axiom-listunion
∀[A,B:Type]. ∀[L:Unit ⋃ (A × B)]. L ∈ Unit supposing isaxiom(L) = tt
Lemma: non-axiom-listunion
∀[A,B:Type]. ∀[L:Unit ⋃ (A × B)]. L ∈ A × B supposing isaxiom(L) = ff
Lemma: list-functor
∀[T:Type]. ContinuousMonotone(L.Unit ⋃ (T × L))
Definition: colist
The co-recursive type of
all terms built from Ax (= []) and pairs <t, l> (= ⌜[t / l]⌝)
where ⌜t ∈ T⌝ and ⌜l ∈ colist(T)⌝. It includes both the finite lists and
infinite streams.⋅
colist(T) == corec(L.Unit ⋃ (T × L))
Lemma: colist_wf
∀[T:Type]. (colist(T) ∈ Type)
Lemma: subtype_rel_colist
∀[A,B:Type]. colist(A) ⊆r colist(B) supposing A ⊆r B
Lemma: colist-fix-partial
∀[A:Type]
(∀[T:Type]. ∀[f:⋂L:Type. ((L ⟶ partial(A)) ⟶ (Unit ⋃ (T × L)) ⟶ partial(A))].
(fix(f) ∈ colist(T) ⟶ partial(A))) supposing
(mono(A) and
value-type(A))
Lemma: colist-ext
∀[T:Type]. colist(T) ≡ Unit ⋃ (T × colist(T))
Lemma: unit_subtype_colist
∀[T:Type]. (Unit ⊆r colist(T))
Lemma: product_subtype_colist
∀[T:Type]. ((T × colist(T)) ⊆r colist(T))
Lemma: colist-value-type
∀[T:Type]. value-type(colist(T))
Definition: co-nil
() == ⋅
Lemma: co-nil_wf
∀[T:Type]. (() ∈ colist(T))
Definition: co-cons
[x / L] == <x, L>
Lemma: co-cons_wf
∀[T:Type]. ∀[x:T]. ∀[L:colist(T)]. ([x / L] ∈ colist(T))
Lemma: isaxiom-wf-colist
∀[T:Type]. ∀[x:colist(T)]. (isaxiom(x) ∈ 𝔹)
Lemma: colist-fix-ap-partial
∀[A:Type]
(∀[T:Type]. ∀[f:⋂L:Type. ((L ⟶ partial(A)) ⟶ (Unit ⋃ (T × L)) ⟶ partial(A))]. ∀[L:colist(T)].
(fix(f) L ∈ partial(A))) supposing
(mono(A) and
value-type(A))
Definition: colength
colength(L)==r if L = Ax then 0 otherwise let a,b = L in 1 + colength(b)
Lemma: colength_wf
∀[T:Type]. ∀[L:colist(T)]. (colength(L) ∈ partial(ℕ))
Definition: list
The list type was once a primitive in Nuprl. Later, it was defined using
the "Mendler" fixpoint type. Now we define lists as those "co-lists"
for which the length (a partially defined function) has a value.
Once we show that the list iterator is well formed (see list_ind_wf)
then we can use list as an abstract type. This "implementation" shows that
we only need induction on ⌜ℕ⌝ to build lists, and do not need the power
of the Mendler fixpoint or a general inductive construction.⋅
T List == {L:colist(T)| (colength(L))↓}
Lemma: list_wf
∀[T:Type]. (T List ∈ Type)
Lemma: list-wf
∀[A:Type]. (A List ∈ Type)
Lemma: list-ext
∀[A:Type]. A List ≡ Unit ⋃ (A × (A List))
Lemma: colength_wf_list
∀[T:Type]. ∀[L:T List]. (colength(L) ∈ ℕ)
Definition: nil
[] == ⋅
Lemma: nil_wf
∀[T:Type]. ([] ∈ T List)
Lemma: subtype_rel_list
∀[A,B:Type]. (A List) ⊆r (B List) supposing A ⊆r B
Lemma: list-value-type
∀[T:Type]. value-type(T List)
Lemma: product_subtype_list
∀[T:Type]. ((T × (T List)) ⊆r (T List))
Definition: cons
[a / b] == <a, b>
Lemma: cons_wf
∀[S:Type]. ∀[a:S]. ∀[b:S List]. ([a / b] ∈ S List)
Lemma: colength-cons-not-zero
∀[T:Type]. ∀[v:T List]. ∀[u:Top]. False supposing colength([u / v]) = 0 ∈ ℕ
Lemma: subtype_rel_list_set
∀[A,B:Type]. ∀[P:A ⟶ Type]. ∀[Q:B ⟶ Type].
(({a:A| P[a]} List) ⊆r ({b:B| Q[b]} List)) supposing ((∀x:A. (P[x] ⇒ Q[x])) and ({a:A| P[a]} ⊆r B))
Lemma: unit_subtype_list
∀[T:Type]. (Unit ⊆r (T List))
Lemma: evalall_nil_lemma
evalall([]) ~ []
Lemma: colength-zero
∀[L:Top List]. ((colength(L) = 0 ∈ ℤ) ⇒ (L ~ []))
Lemma: colength-positive
∀[T:Type]. ∀[L:T List].
(0 < colength(L)
⇒ {(fst(L) ∈ T) ∧ (snd(L) ∈ T List) ∧ (colength(L) = (1 + colength(snd(L))) ∈ ℤ) ∧ (L ~ [fst(L) / (snd(L))])})
Lemma: pi1_cons_lemma
∀b,a:Top. (fst([a / b]) ~ a)
Lemma: spread_cons_lemma
∀f,y,x:Top. (let a,b = [x / y] in f[a;b] ~ f[x;y])
Definition: hd
hd(l) == fst(l)
Lemma: reduce_hd_cons_lemma
∀b,a:Top. (hd([a / b]) ~ a)
Definition: tl
tl(l) == if l = Ax then [] otherwise snd(l)
Lemma: reduce_tl_cons_lemma
∀b,a:Top. (tl([a / b]) ~ b)
Lemma: reduce_tl_nil_lemma
tl([]) ~ []
Lemma: not-cons-sq-nil
∀[u,v:Top]. (([u / v] ~ []) = (0 ~ 1) ∈ Type)
Lemma: has-valueall-cons
∀[a,b:Base]. uiff(has-valueall(a) ∧ has-valueall(b);has-valueall([a / b]))
Lemma: has-valueall-single
∀[a:Base]. uiff(has-valueall(a);has-valueall([a]))
Lemma: evalall-cons
∀a,b:Top. (evalall([a / b]) ~ eval u = evalall(a) in eval v = evalall(b) in [u / v])
Definition: listify
listify(f;m;n) == fix((λlistify,m. if n ≤z m then [] else [f m / (listify (m + 1))] fi )) m
Lemma: listify_wf
∀[T:Type]. ∀[m,n:ℤ]. ∀[f:{m..n-} ⟶ T]. (listify(f;m;n) ∈ T List)
Lemma: colength-positive2
∀[T:Type]. ∀[L:T List].
∀n:ℕ
(0 < n
⇒ (colength(L) = n ∈ ℤ)
⇒ {(fst(L) ∈ T) ∧ (snd(L) ∈ T List) ∧ (colength(L) = (1 + colength(snd(L))) ∈ ℤ) ∧ (L ~ [fst(L) / (snd(L))])})
Lemma: comb_for_listify_wf
λT,m,n,f,z. listify(f;m;n) ∈ T:Type ⟶ m:ℤ ⟶ n:ℤ ⟶ f:({m..n-} ⟶ T) ⟶ (↓True) ⟶ (T List)
Lemma: list-functionality-induction
∀T,A:Type. ∀F:Base.
((F[[]] ∈ A)
⇒ (∀a1,a2,L1,L2:Base. ((a1 = a2 ∈ T) ⇒ (F[L1] = F[L2] ∈ A) ⇒ (F[[a1 / L1]] = F[[a2 / L2]] ∈ A)))
⇒ (∀L:T List. (F[L] ∈ A)))
Lemma: pair-sq-axiom-wf
∀[a,b:Top]. (<a, b> ~ Ax ∈ Type)
Lemma: colist-cases
∀[T:Type]. ∀x:colist(T). ((x ~ Ax) ∨ (x ∈ T × colist(T)))
Lemma: list-cases
∀[T:Type]. ∀x:T List. ((x ~ []) ∨ (x ∈ T × (T List)))
Lemma: list-cases2
∀[T:Type]. ∀x:T List. ((x ~ []) ∨ (x ~ [hd(x) / tl(x)]))
Lemma: tl_wf
∀[A:Type]. ∀[l:A List]. (tl(l) ∈ A List)
Definition: list_ind
rec-case(L) of
[] => nilcase
h::t =>
r.F[h;
t;
r] ==
fix((λlist_ind,L. eval v = L in
if v is a pair then let h,t = v
in F[h;
t;
list_ind t] otherwise if v = Ax then nilcase otherwise ⊥))
L
Lemma: list_ind_nil_lemma
∀A,x:Top. (rec-case([]) of [] => x | h::t => r.A[h;t;r] ~ x)
Lemma: list_ind_cons_lemma
∀A,x,b,a:Top. (rec-case([a / b]) of [] => x | h::t => r.A[h;t;r] ~ A[a;b;rec-case(b) of [] => x | h::t => r.A[h;t;r]])
Lemma: list_ind-general-wf
∀[A:Type]. ∀[B:(A List) ⟶ ℙ]. ∀[x:B[[]]]. ∀[F:∀a:A. ∀L:A List. (B[L] ⇒ B[[a / L]])]. ∀[L:A List].
(rec-case(L) of
[] => x
h::t =>
r.F[h;t;r] ∈ B[L])
Lemma: list_ind_wf
∀[A,B:Type]. ∀[x:B]. ∀[F:A ⟶ (A List) ⟶ B ⟶ B]. ∀[L:A List]. (rec-case(L) of [] => x | h::t => r.F[h;t;r] ∈ B)
Lemma: list_subtype_base
∀[A:Type]. (A List) ⊆r Base supposing A ⊆r Base
Definition: l-ind
l-ind(L;nilcase;h,t,r.F[h;
t;
r])
==r eval v = L in
if v = Ax then nilcase otherwise let h,t = v
in F[h;
t;
l-ind(t;nilcase;h,t,r.F[h;
t;
r])]
Lemma: l_ind_nil_lemma
∀A,x:Top. (l-ind([];x;h,t,r.A[h;t;r]) ~ x)
Lemma: l_ind_cons_lemma
∀A,x,b,a:Top. (l-ind([a / b];x;h,t,r.A[h;t;r]) ~ A[a;b;l-ind(b;x;h,t,r.A[h;t;r])])
Lemma: l-ind_wf
∀[A,B:Type]. ∀[L:A List]. ∀[x:B]. ∀[F:A ⟶ (A List) ⟶ B ⟶ B]. (l-ind(L;x;h,t,r.F[h;t;r]) ∈ B)
Definition: list_accum
accumulate (with value x and list item a):
f[x; a]
over list:
L
with starting value:
y) ==
fix((λlist_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in list_accum f[y; h] t otherwise if v = Ax then y otherwise ⊥))
y
L
Lemma: list_accum_wf
∀[T,T':Type]. ∀[l:T List]. ∀[y:T']. ∀[f:T' ⟶ T ⟶ T'].
(accumulate (with value x and list item a):
f[x;a]
over list:
l
with starting value:
y) ∈ T')
Lemma: list-valueall-type
∀[T:Type]. valueall-type(T List) supposing valueall-type(T)
Lemma: list_induction
∀[T:Type]. ∀[P:(T List) ⟶ ℙ]. (P[[]] ⇒ (∀aaaa:T. ∀LLLL:T List. (P[LLLL] ⇒ P[[aaaa / LLLL]])) ⇒ (∀L:T List. P[L]))
Lemma: cons_neq_nil
∀[T:Type]. ∀[h:T]. ∀[t:T List]. (¬([h / t] = [] ∈ (T List)))
Lemma: sqle-list_ind
∀[F:Base]
∀[G:Base]
∀[H,J:Base].
∀as,b1,b2:Base.
F[rec-case(as) of
[] => b1
h::t =>
r.H[h;t;r]] ≤ G[rec-case(as) of
[] => b2
h::t =>
r.J[h;t;r]]
supposing F[b1] ≤ G[b2]
supposing ∀x,y,r1,r2:Base. ((F[r1] ≤ G[r2]) ⇒ (F[H[x;y;r1]] ≤ G[J[x;y;r2]]))
supposing strict1(λx.G[x])
supposing strict1(λx.F[x])
Lemma: l-ind-sqequal-list_ind
∀[L,x,F:Top]. (l-ind(L;x;h,t,r.F[h;t;r]) ~ rec-case(L) of [] => x | h::t => r.F[h;t;r])
Definition: eval_list
eval_list(t) == rec-case(t) of [] => [] | h::t => r.eval s = r in <h, s>
Lemma: eval_list_wf
∀[T:Type]. ∀[L:T List]. (eval_list(L) ∈ T List)
Definition: reduce
Reduce is the foldr operation⋅
reduce(f;k;as) == rec-case(as) of [] => k | a::as' => r.f a r
Lemma: reduce_nil_lemma
∀k,f:Top. (reduce(f;k;[]) ~ k)
Lemma: reduce_cons_lemma
∀b,a,k,f:Top. (reduce(f;k;[a / b]) ~ f a reduce(f;k;b))
Lemma: reduce_wf
∀[A,B:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[k:B]. ∀[as:A List]. (reduce(f;k;as) ∈ B)
Lemma: list_accum_nil_lemma
∀z,f:Top. (accumulate (with value x and list item y): f[x;y]over list: []with starting value: z) ~ z)
Lemma: list_accum_cons_lemma
∀y,x,z,f:Top.
(accumulate (with value a and list item b):
f[a;b]
over list:
[x / y]
with starting value:
z) ~ accumulate (with value a and list item b):
f[a;b]
over list:
y
with starting value:
f[z;x]))
Lemma: sqle-list_accum
∀[F:Base]
∀[G:Base]
∀[H,J:Base].
∀as,b1,b2:Base.
F[accumulate (with value v and list item a):
H[v;a]
over list:
as
with starting value:
b1)] ≤ G[accumulate (with value v and list item a):
J[v;a]
over list:
as
with starting value:
b2)]
supposing F[b1] ≤ G[b2]
supposing ∀a,r1,r2:Base. ((F[r1] ≤ G[r2]) ⇒ (F[H[r1;a]] ≤ G[J[r2;a]]))
supposing strict1(λx.G[x])
supposing strict1(λx.F[x])
Lemma: sqequal-list_accum
∀[F:Base]
∀[G:Base]
∀[H,J:Base].
∀as,b1,b2:Base.
F[accumulate (with value v and list item a):
H[v;a]
over list:
as
with starting value:
b1)] ~ G[accumulate (with value v and list item a):
J[v;a]
over list:
as
with starting value:
b2)]
supposing F[b1] ~ G[b2]
supposing (∀a,r1,r2:Base. ((F[r1] ≤ G[r2]) ⇒ (F[H[r1;a]] ≤ G[J[r2;a]])))
∧ (∀a,r1,r2:Base. ((G[r1] ≤ F[r2]) ⇒ (G[J[r1;a]] ≤ F[H[r2;a]])))
supposing strict1(λx.G[x])
supposing strict1(λx.F[x])
Lemma: sqle-list_accum-list_ind
∀[F:Base]
∀[G:Base]
∀[H,J:Base].
∀as,b1,b2:Base.
F[accumulate (with value v and list item a):
H[v;a]
over list:
as
with starting value:
b1)] ≤ G[b1;rec-case(as) of
[] => b2
h::t =>
r.J[h;r]]
supposing ∀x:Base. (F[x] ≤ G[x;b2])
supposing ∀a,b,c:Base. (G[H[b;a];c] ≤ G[b;J[a;c]])
supposing ∀z:Base. strict1(λx.G[z;x])
supposing strict1(λx.F[x])
Lemma: sqle-list_ind-list_accum
∀[F:Base]
∀[G:Base]
∀[H,J:Base].
∀as,b1,b2:Base.
G[b1;rec-case(as) of
[] => b2
h::t =>
r.J[h;r]] ≤ F[accumulate (with value v and list item a):
H[v;a]
over list:
as
with starting value:
b1)]
supposing ∀x:Base. (G[x;b2] ≤ F[x])
supposing ∀a,b,c:Base. (G[b;J[a;c]] ≤ G[H[b;a];c])
supposing ∀z:Base. strict1(λx.G[z;x])
supposing strict1(λx.F[x])
Definition: append
as @ bs == rec-case(as) of [] => bs | a::as' => r.[a / r]
Lemma: append_wf
∀[T:Type]. ∀[as,bs:T List]. (as @ bs ∈ T List)
Definition: eager-append
eager-append(as;bs) == rec-case(as) of [] => bs | a::as' => r.eval r' = r in [a / r']
Lemma: eager-append_wf
∀[T:Type]. ∀[as,bs:T List]. (eager-append(as;bs) ∈ T List)
Definition: map
map(f;as) == rec-case(as) of [] => [] | h::t => r.[f h / r]
Lemma: map_nil_lemma
∀f:Top. (map(f;[]) ~ [])
Lemma: map_cons_lemma
∀b,a,f:Top. (map(f;[a / b]) ~ [f a / map(f;b)])
Lemma: map_wf
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[l:A List]. (map(f;l) ∈ B List)
Definition: eager-map
eager-map(f;as) == rec-case(as) of [] => [] | h::t => r.eval h' = f h in eval r' = r in [h' / r']
Lemma: eager-map_wf
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[l:A List]. (eager-map(f;l) ∈ B List) supposing value-type(B)
Lemma: eager_map_nil_lemma
∀f:Top. (eager-map(f;[]) ~ [])
Lemma: eager_map_cons_lemma
∀v,u,f:Top. (eager-map(f;[u / v]) ~ eval x = f u in eval r = eager-map(f;v) in [x / r])
Definition: nth_tl
nth_tl(n;as) == fix((λnth_tl,n,as. if n ≤z 0 then as else nth_tl (n - 1) tl(as) fi )) n as
Lemma: nth_tl_wf
∀[A:Type]. ∀[as:A List]. ∀[i:ℤ]. (nth_tl(i;as) ∈ A List)
Definition: rev-append
rev(as) + bs == accumulate (with value r and list item a): [a / r]over list: aswith starting value: bs)
Lemma: rev-append_wf
∀[T:Type]. ∀[as,bs:T List]. (rev(as) + bs ∈ T List)
Lemma: eq_cons_imp_eq_tls
∀[A:Type]. ∀[a,b:A]. ∀[as,bs:A List]. as = bs ∈ (A List) supposing [a / as] = [b / bs] ∈ (A List)
Definition: reject
as\[i] ==
fix((λreject,i,as. if i ≤z 0 then tl(as) else case as of [] => [] | a'::as' => [a' / (reject (i - 1) as')] esac fi )) \000Ci as
Lemma: reject_wf
∀[A:Type]. ∀[l:A List]. ∀[n:ℤ]. (l\[n] ∈ A List)
Definition: eager-map-append
eager-map-append(f;as;bs) ==
accumulate (with value L and list item a):
eval x = f a in
eval L' = L in
[x / L']
over list:
as
with starting value:
bs)
Lemma: eager-map-append_wf
∀[T:Type]
∀[A:Type]. ∀[f:A ⟶ T]. ∀[as:A List]. ∀[bs:T List]. (eager-map-append(f;as;bs) ∈ T List) supposing value-type(T)
Definition: mapc
Illustration of use of add_rec_def for a curried function⋅
mapc(f) == fix((λmapc,f,as. case as of [] => [] | a::as1 => [f a / (mapc f as1)] esac)) f
Lemma: mapc_wf
∀[A,B:Type]. ∀[f:A ⟶ B]. (mapc(f) ∈ (A List) ⟶ (B List))
Definition: insert-int
insert-int(x;l) == rec-case(l) of [] => [x] | a::as => v.if (a) < (x) then eval y = v in [a / y] else [x; [a / as]]
Lemma: insert-int_wf
∀[T:Type]. ∀[x:T]. ∀[l:T List]. (insert-int(x;l) ∈ T List) supposing T ⊆r ℤ
Lemma: insert_int_nil_lemma
∀a:Top. (insert-int(a;[]) ~ [a])
Lemma: insert-int-cons
∀v:ℤ List. ∀u,a:ℤ. (insert-int(a;[u / v]) ~ if u <z a then [u / insert-int(a;v)] else [a; [u / v]] fi )
Definition: update-alist
update-alist(eq;L;x;z;v.f[v]) == rec-case(L) of [] => [<x, z>] | p::ps => r.let a,v = p in if eq a x then [<x, f[v]> / \000Cps] else [p / r] fi
Lemma: update-alist_wf
∀[A,T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[L:(T × A) List]. ∀[z:A]. ∀[f:A ⟶ A].
(update-alist(eq;L;x;z;v.f[v]) ∈ (T × A) List)
Lemma: sqequal-list_ind
∀[F:Base]
∀[G:Base]
∀[H,J:Base].
∀as,b1,b2:Base.
F[rec-case(as) of
[] => b1
h::t =>
r.H[h;t;r]] ~ G[rec-case(as) of
[] => b2
h::t =>
r.J[h;t;r]]
supposing F[b1] ~ G[b2]
supposing (∀x,y,r1,r2:Base. ((F[r1] ≤ G[r2]) ⇒ (F[H[x;y;r1]] ≤ G[J[x;y;r2]])))
∧ (∀x,y,r1,r2:Base. ((G[r1] ≤ F[r2]) ⇒ (G[J[x;y;r1]] ≤ F[H[x;y;r2]])))
supposing strict1(λx.G[x])
supposing strict1(λx.F[x])
Lemma: eval_list_nil_lemma
eval_list([]) ~ []
Lemma: eval_list_cons_lemma
∀b,a:Top. (eval_list([a / b]) ~ eval b' = eval_list(b) in [a / b'])
Lemma: sqequal-list_accum-list_ind
∀[F:Base]
∀[G:Base]
∀[H,J:Base].
∀as,b1,b2:Base.
F[accumulate (with value v and list item a):
H[v;a]
over list:
as
with starting value:
b1)] ~ G[b1;rec-case(as) of
[] => b2
h::t =>
r.J[h;r]]
supposing ∀x:Base. (F[x] ~ G[x;b2])
supposing ∀a,b,c:Base. (G[H[b;a];c] ~ G[b;J[a;c]])
supposing ∀z:Base. strict1(λx.G[z;x])
supposing strict1(λx.F[x])
Lemma: comb_for_append_wf
λT,as,bs,z. (as @ bs) ∈ T:Type ⟶ as:(T List) ⟶ bs:(T List) ⟶ (↓True) ⟶ (T List)
Lemma: list_accum_cons
∀[A,B,y,f:Top].
(accumulate (with value x and list item a):
f[x;a]
over list:
[A / B]
with starting value:
y) ~ accumulate (with value x and list item a):
f[x;a]
over list:
B
with starting value:
f[y;A]))
Lemma: comb_for_map_wf
λA,B,f,l,z. map(f;l) ∈ A:Type ⟶ B:Type ⟶ f:(A ⟶ B) ⟶ l:(A List) ⟶ (↓True) ⟶ (B List)
Lemma: map-pair
∀[f,a,b:Top]. (map(f;<a, b>) ~ <f a, map(f;b)>)
Lemma: map-axiom
∀[f:Top]. (map(f;Ax) ~ Ax)
Lemma: eager-map-is-map
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[l:A List]. (eager-map(f;l) ~ map(f;l)) supposing value-type(B)
Lemma: list_accum-map
∀[L,y,f,g:Top].
(accumulate (with value x and list item a):
f[x;a]
over list:
map(g;L)
with starting value:
y) ~ accumulate (with value x and list item a):
f[x;g a]
over list:
L
with starting value:
y))
Lemma: map-ifthenelse
∀[f,x,y,b:Top]. (map(f;if b then x else y fi ) ~ if b then map(f;x) else map(f;y) fi )
Lemma: reduce-ifthenelse
∀[f,k,x,y,b:Top]. (reduce(f;k;if b then x else y fi ) ~ if b then reduce(f;k;x) else reduce(f;k;y) fi )
Lemma: rev-append-pair
∀[a,b,c:Top]. (rev(<a, b>) + c ~ rev(b) + <a, c>)
Lemma: rev-append-axiom
∀[c:Top]. (rev(Ax) + c ~ c)
Lemma: rev_app_nil_lemma
∀bs:Top. (rev([]) + bs ~ bs)
Lemma: rev_app_cons_lemma
∀bs,as,a:Top. (rev([a / as]) + bs ~ rev(as) + [a / bs])
Definition: reverse
rev(as) == rev(as) + []
Lemma: reverse_wf
∀[T:Type]. ∀[as:T List]. (rev(as) ∈ T List)
Lemma: reject_cons_hd
∀[T:Type]. ∀[a:T]. ∀[as:T List]. ∀[i:ℤ]. [a / as]\[i] = as ∈ (T List) supposing i ≤ 0
Definition: for
For{T,op,id} x ∈ as. f[x] == reduce(op;id;map(λx:T. f[x];as))
Lemma: for_wf
∀[A,B,C:Type]. ∀[f:B ⟶ C ⟶ C]. ∀[k:C]. ∀[as:A List]. ∀[g:A ⟶ B]. (For{A,f,k} x ∈ as. g[x] ∈ C)
Definition: filter
filter(P;l) == reduce(λa,v. if P a then [a / v] else v fi ;[];l)
Lemma: filter_wf
∀[T:Type]. ∀[l:T List]. ∀[P:T ⟶ 𝔹]. (filter(P;l) ∈ T List)
Definition: concat
concat(ll) == reduce(λl,l'. (l @ l');[];ll)
Lemma: concat_wf
∀[T:Type]. ∀[ll:T List List]. (concat(ll) ∈ T List)
Lemma: strict4-append
strict4(λx,y,z,w. (x @ y))
Lemma: strict4-map
strict4(λx,y,z,s. map(y;x))
Lemma: eager_map_append_nil_lemma
∀bs,f:Top. (eager-map-append(f;[];bs) ~ bs)
Definition: eager-product-map
eager-product-map(f;as;bs) == rec-case(as) of [] => [] | a::more_as => r.eager-map-append(f a;bs;r)
Lemma: eager-product-map_wf
∀[T:Type]
∀[A,B:Type]. ∀[f:A ⟶ B ⟶ T]. ∀[as:A List]. ∀[bs:B List]. (eager-product-map(f;as;bs) ∈ T List)
supposing value-type(T)
Definition: merge-int
merge-int(as;bs) == reduce(λb,l. insert-int(b;l);as;bs)
Lemma: merge-int_wf
∀[T:Type]. ∀[as,bs:T List]. (merge-int(as;bs) ∈ T List) supposing T ⊆r ℤ
Definition: deq-member
x ∈b L == reduce(λa,b. ((eq a x) ∨bb);ff;L)
Lemma: deq-member_wf
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[L:A List]. ∀[x:A]. (x ∈b L ∈ 𝔹)
Definition: null
null(as) == if as is a pair then ff otherwise if as = Ax then tt otherwise ⊥
Lemma: null_nil_lemma
null([]) ~ tt
Lemma: null_cons_lemma
∀b,a:Top. (null([a / b]) ~ ff)
Lemma: null_wf
∀[T:Type]. ∀[as:T List]. (null(as) ∈ 𝔹)
Lemma: null_wf2
null([]) ∈ 𝔹
Lemma: assert_of_null
∀[T:Type]. ∀[as:T List]. uiff(↑null(as);as = [] ∈ (T List))
Lemma: assert-null-base
∀[as:Base]. uiff(null(as) ~ tt;as ~ [])
Lemma: subtype_rel_list-iff
∀[A,B:Type]. uiff((A List) ⊆r (B List);A ⊆r B)
Lemma: map_is_nil
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[l:A List]. uiff(map(f;l) = [] ∈ (B List);l = [] ∈ (A List))
Lemma: null-map
∀[f,L:Top]. (null(map(f;L)) ~ null(L))
Lemma: append-unroll
∀[as,bs:Top]. (as @ bs ~ if as is a pair then [fst(as) / ((snd(as)) @ bs)] otherwise if as = Ax then bs otherwise ⊥)
Lemma: eager-append-is-append
∀[as,bs:Top List]. (eager-append(as;bs) ~ as @ bs)
Lemma: has-value-append
∀[l,k:Base]. (l)↓ supposing (l @ k)↓
Lemma: append_assoc
∀[as,bs,cs:Top]. ((as @ bs) @ cs ~ as @ bs @ cs)
Lemma: eager-append_assoc
∀[as,bs,cs:Top List]. (eager-append(eager-append(as;bs);cs) ~ eager-append(as;eager-append(bs;cs)))
Lemma: append_back_nil
∀[T:Type]. ∀[as:T List]. (as @ [] ~ as)
Lemma: append-nil
∀[l:Top List]. (l @ [] ~ l)
Lemma: append-nil-sqle
∀[t:Top]. (t @ [] ≤ t)
Lemma: prod-if-ispair-append-nil
∀[l:Base]. (l ∈ Top × Top) supposing ((↑ispair(l @ [])) and (l @ [])↓)
Lemma: pi1-if-ispair-append-nil
∀[l:Base]. (fst((l @ [])) ~ fst(l)) supposing ((↑ispair(l @ [])) and (l @ [])↓)
Lemma: pi2-if-ispair-append-nil
∀[l:Base]. (snd((l @ [])) ~ (snd(l)) @ []) supposing ((↑ispair(l @ [])) and (l @ [])↓)
Lemma: has-value-append-nil
∀[l:Base]. (l)↓ supposing (l @ [])↓
Lemma: ispair-or-isaxiom-append-nil
∀l:Base. ((l @ [])↓ ⇒ ((↑ispair(l @ [])) ∨ (↑isaxiom(l @ []))))
Lemma: isaxiom-append-nil
∀[l:Base]. (↑isaxiom(l)) supposing ((↑isaxiom(l @ [])) and (l @ [])↓)
Lemma: evalall-append-implies-list-base
∀[a,b:Base]. a ∈ Base List supposing (evalall(a @ b))↓
Lemma: evalall-append-sqle
∀a,b:Top. (evalall(a @ b) ≤ eval u = evalall(a) in eval v = evalall(b) in evalall(u @ v))
Lemma: map_append_sq
∀[f,a,b:Top]. (map(f;a @ b) ~ map(f;a) @ map(f;b))
Lemma: list_accum_append
∀[A:Top List]. ∀[B,y,f:Top].
(accumulate (with value x and list item a):
f[x;a]
over list:
A @ B
with starting value:
y) ~ accumulate (with value x and list item a):
f[x;a]
over list:
B
with starting value:
accumulate (with value x and list item a):
f[x;a]
over list:
A
with starting value:
y)))
Lemma: rev-append-append
∀[as:Top List]. ∀[bs,cs:Top]. (rev(as @ bs) + cs ~ rev(bs) + rev(as) + cs)
Lemma: rev-append-rev-append
∀[as:Top List]. ∀[bs,cs:Top]. (rev(rev(as) + bs) + cs ~ rev(bs) + as @ cs)
Lemma: concat_conv_single_nil_lemma
concat([[]]) ~ []
Lemma: concat-unroll
∀a:Top. (concat(a) ~ if a is a pair then (fst(a)) @ concat(snd(a)) otherwise if a = Ax then [] otherwise ⊥)
Definition: cbv-concat
cbv-concat(ll) == reduce(λl,l'. eval x = l in eval y = l' in x @ y;[];ll)
Lemma: cbv-concat-sq
∀[ll:Top List List]. (cbv-concat(ll) ~ concat(ll))
Lemma: cbv-concat_wf
∀[T:Type]. ∀[ll:T List List]. (cbv-concat(ll) ∈ T List)
Lemma: append_nil_sq
∀[l:Top List]. (l @ [] ~ l)
Lemma: append_assoc_sq
∀[as,bs,cs:Top]. ((as @ bs) @ cs ~ as @ bs @ cs)
Definition: list-accum
list-accum(t,a,h.f[t;
a;
h];b;L) ==
if L is a pair then let h,t = L
in list-accum(t,a,h.f[t;
a;
h];f[t;
b;
h];t) otherwise if L = Ax then b otherwise ⊥
Lemma: list-accum_wf
∀[T,T':Type]. ∀[l:T List]. ∀[b:T']. ∀[f:(T List) ⟶ T' ⟶ T ⟶ T']. (list-accum(t,a,h.f[t;a;h];b;l) ∈ T')
Lemma: list_acc_nil_red_lemma
∀b,f:Top. (list-accum(t,a,h.f[t;a;h];b;[]) ~ b)
Lemma: list_acc_cons_red_lemma
∀v,u,b,f:Top. (list-accum(t,a,h.f[t;a;h];b;[u / v]) ~ list-accum(t,a,h.f[t;a;h];f[v;b;u];v))
Lemma: list-accum-append
∀[l1:Top List]. ∀[l2,b,f:Top].
(list-accum(t,a,h.f[t;a;h];b;l1 @ l2) ~ list-accum(t,a,h.f[t;a;h];list-accum(t,a,h.f[t @ l2;a;h];b;l1);l2))
Lemma: evalall-append-nil
∀[l:Base]. evalall(l @ []) ~ l supposing (evalall(l @ []))↓
Lemma: has-valueall-append-nil
∀[l:Base]. l @ [] ~ l supposing has-valueall(l @ [])
Lemma: map_append
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[as,as':A List]. (map(f;as @ as') = (map(f;as) @ map(f;as')) ∈ (B List))
Lemma: concat-single
∀[l:Top List]. (concat([l]) ~ l)
Definition: length
||as|| == rec-case(as) of [] => 0 | a::b => r.r + 1
Lemma: length_wf
∀[A:Type]. ∀[l:A List]. (||l|| ∈ ℤ)
Lemma: length_of_nil_lemma
||[]|| ~ 0
Lemma: length_wf2
||[]|| ∈ ℤ
Lemma: length_of_cons_lemma
∀as,a:Top. (||[a / as]|| ~ ||as|| + 1)
Lemma: hd_wf
∀[A:Type]. ∀[l:A List]. hd(l) ∈ A supposing ||l|| ≥ 1
Lemma: non_neg_length
∀[A:Type]. ∀[l:A List]. (||l|| ≥ 0 )
Lemma: length_wf_nat
∀[A:Type]. ∀[L:A List]. (||L|| ∈ ℕ)
Lemma: length_wf_nil
||[]|| ∈ ℕ
Lemma: length-wf-has-value
∀[l:Base]. ||l|| ∈ ℤ supposing (||l||)↓
Lemma: length-nat-if-has-value
∀l:Base. ((||l||)↓ ⇒ (||l|| ∈ ℕ))
Lemma: list-if-has-value-length
∀l:Base. l ∈ Base List supposing (||l||)↓
Lemma: list-if-has-value-list_ind
∀b,f:Base.
∀l:Base. l ∈ Base List supposing (rec-case(l) of [] => b | a::b => r.f[a;r])↓ supposing ∀x:Base. strict(λu.f[x;u])
Lemma: list-if-has-value-length2
∀l:Base. l ∈ Base List supposing (||l||)↓
Lemma: comb_for_length_wf1
λA,l,z. ||l|| ∈ A:Type ⟶ l:(A List) ⟶ (↓True) ⟶ ℤ
Lemma: comb_for_length_wf2
λz.||[]|| ∈ (↓True) ⟶ ℤ
Lemma: length_cons
∀[A:Type]. ∀[a:A]. ∀[as:A List]. (||[a / as]|| = (||as|| + 1) ∈ ℤ)
Lemma: length_nil
||[]|| = 0 ∈ ℤ
Lemma: length-nil
||[]|| ~ 0
Lemma: length-singleton
∀[x:Top]. (||[x]|| ~ 1)
Lemma: pos_length
∀[A:Type]. ∀[l:A List]. ||l|| ≥ 1 supposing ¬(l = [] ∈ (A List))
Lemma: length_one
∀[T:Type]. ∀L:T List. uiff(||L|| = 1 ∈ ℤ;∃x:T. (L = [x] ∈ (T List)))
Lemma: test-arith-length-additions
∀T:Type. ∀a:T. ∀b:T List. ∀i:ℤ. (i < ||[a / b]|| ⇒ i < ||b|| + 1)
Lemma: length_of_null_list
∀[A:Type]. ∀[as:A List]. ||as|| = 0 ∈ ℤ supposing as = [] ∈ (A List)
Lemma: length-is-colength
∀[t:Top]. (||t|| ~ colength(t))
Lemma: non_nil_length
∀[T:Type]. ∀[L:T List]. 0 < ||L|| supposing ¬(L = [] ∈ (T List))
Lemma: map-length
∀[f,as:Top]. (||map(f;as)|| ~ ||as||)
Lemma: map_length
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[as:A List]. (||map(f;as)|| = ||as|| ∈ ℤ)
Lemma: length-map
∀[f:Top]. ∀[T:Type]. ∀[L:T List]. (||map(f;L)|| ~ ||L||)
Lemma: length-map-sq
∀[f:Top]. ∀[L:Top List]. (||map(f;L)|| ~ ||L||)
Lemma: length_tl
∀[A:Type]. ∀[l:A List]. ||tl(l)|| = (||l|| - 1) ∈ ℤ supposing ||l|| ≥ 1
Lemma: respects-equality-list
∀[A,B:Type]. respects-equality(A List;B List) supposing respects-equality(A;B)
Lemma: reject_cons_tl
∀[T:Type]. ∀[a:T]. ∀[as:T List]. ∀[i:ℤ].
([a / as]\[i] = [a / as\[i - 1]] ∈ (T List)) supposing ((i ≤ ||as||) and 0 < i)
Lemma: listify_length
∀[T:Type]. ∀m,n:ℤ. ∀f:{m..n-} ⟶ T. (n < m ∨ (||listify(f;m;n)|| = (n - m) ∈ ℤ))
Definition: list_n
A List(n) == {x:A List| ||x|| = n ∈ ℤ}
Lemma: list_n_wf
∀[A:Type]. ∀[n:ℤ]. (A List(n) ∈ Type)
Definition: listp
A List+ == {l:A List| 0 < ||l||}
Lemma: listp_wf
∀[A:Type]. (A List+ ∈ Type)
Lemma: length-insert-int
∀[T:Type]. ∀[x:T]. ∀[l:T List]. (||insert-int(x;l)|| = (||l|| + 1) ∈ ℤ) supposing T ⊆r ℤ
Lemma: length_cons_ge_one
∀[x:Top]. ∀[l:Top List]. (||[x / l]|| ≥ 1 )
Lemma: cons-listp
∀[T:Type]. ∀[l:T List]. ∀[x:T]. ([x / l] ∈ T List+)
Lemma: cons-not-nil
∀[S:Type]. ∀[a:S]. ∀[b:S List]. (¬([a / b] = [] ∈ (S List)))
Lemma: nil-not-cons
∀[S:Type]. ∀[a:S]. ∀[b:S List]. (¬([] = [a / b] ∈ (S List)))
Lemma: length-append
∀[as,bs:Top]. (||as @ bs|| ~ ||as|| + ||bs||)
Lemma: map_length_nat
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[as:A List]. (||map(f;as)|| = ||as|| ∈ ℕ)
Lemma: length-merge-int
∀[T:Type]. ∀[as,bs:T List]. (||merge-int(bs;as)|| = (||bs|| + ||as||) ∈ ℤ) supposing T ⊆r ℤ
Lemma: length_append
∀[as,bs:Top List]. (||as @ bs|| = (||as|| + ||bs||) ∈ ℤ)
Lemma: length_of_not_nil
∀[A:Type]. ∀[as:A List]. uiff(¬(as = [] ∈ (A List));||as|| ≥ 1 )
Lemma: length_nth_tl
∀[A:Type]. ∀[as:A List]. ∀[n:{0...||as||}]. (||nth_tl(n;as)|| = (||as|| - n) ∈ ℤ)
Lemma: length-rev-append
∀[as,bs:Top]. (||rev(as) + bs|| ~ ||as|| + ||bs||)
Definition: select
L[n] == fix((λselect,n,L. let x,y = L in if (n) < (1) then x else eval m = n - 1 in select m y)) n L
Lemma: select_wf
∀[A:Type]. ∀[l:A List]. ∀[n:ℤ]. (l[n] ∈ A) supposing (n < ||l|| and (0 ≤ n))
Lemma: test-select-nil
[][33] ~ ⊥
Lemma: select-cons-hd
∀[a,as:Top]. ∀[i:ℤ]. [a / as][i] ~ a supposing i ≤ 0
Lemma: select-cons-tl
∀[a,as:Top]. ∀[i:ℤ]. [a / as][i] ~ as[i - 1] supposing 0 < i
Lemma: select_cons_tl_sq2
∀[i:ℕ]. ∀[x,l:Top]. ([x / l][i + 1] ~ l[i])
Lemma: select0
∀[L:Top]. (L[0] ~ hd(L))
Lemma: select-nil
∀[i:Top]. ([][i] ~ ⊥)
Lemma: respects-equality-list-type
∀[A,B:Type]. ∀L:A List. ((∀i:ℕ||L||. (L[i] ∈ B)) ⇒ (L ∈ B List)) supposing respects-equality(A;B)
Lemma: hd-nil
hd([]) ~ ⊥
Lemma: select-as-hd
∀[L:Top List]. (L[0] ~ hd(L))
Definition: l_member
(x ∈ l) == ∃i:ℕ. (i < ||l|| c∧ (x = l[i] ∈ T))
Lemma: l_member_wf
∀[T:Type]. ∀[x:T]. ∀[l:T List]. ((x ∈ l) ∈ ℙ)
Lemma: cons-has-member
∀[S:Type]. ∀a:S. ∀[b:S List]. ∃x:S. (x ∈ [a / b])
Definition: sorted
sorted(L) == ∀i:ℕ||L||. ∀j:ℕi. (L[j] ≤ L[i])
Lemma: sorted_wf
∀[T:Type]. ∀[L:T List]. (sorted(L) ∈ ℙ) supposing T ⊆r ℤ
Definition: no_repeats
no_repeats(T;l) == ∀[i,j:ℕ]. (¬(l[i] = l[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||l|| and i < ||l||)
Lemma: no_repeats_wf
∀[T:Type]. ∀[l:T List]. (no_repeats(T;l) ∈ ℙ)
Definition: last
last(L) == L[||L|| - 1]
Lemma: last_wf
∀[T:Type]. ∀[L:T List]. last(L) ∈ T supposing ¬↑null(L)
Lemma: select_cons_hd
∀[T:Type]. ∀[a:T]. ∀[as:T List]. ∀[i:ℤ]. [a / as][i] = a ∈ T supposing i ≤ 0
Lemma: select_cons_tl
∀[T:Type]. ∀[a:T]. ∀[as:T List]. ∀[i:ℤ]. ([a / as][i] = as[i - 1] ∈ T) supposing ((i ≤ ||as||) and 0 < i)
Lemma: select_cons_tl_sq
∀[T:Type]. ∀[x:T]. ∀[l:T List]. ∀[i:ℕ||l||]. ([x / l][i + 1] ~ l[i])
Lemma: select_tl
∀[A:Type]. ∀[as:A List]. ∀[n:ℕ||as|| - 1]. (tl(as)[n] = as[n + 1] ∈ A)
Lemma: select-cons
∀[x,L:Top]. ∀[i:ℤ]. ([x / L][i] ~ if i ≤z 0 then x else L[i - 1] fi )
Lemma: select-append
∀[L1,L2:Top List]. ∀[i:ℕ]. (L1 @ L2[i] ~ if i <z ||L1|| then L1[i] else L2[i - ||L1||] fi )
Lemma: select-is-bottom
∀[X:Top List]. ∀[i:ℕ]. X[i] ~ ⊥ supposing ||X|| ≤ i
Lemma: member_exists
∀[T:Type]. ∀L:T List. ∃x:T. (x ∈ L) supposing ¬(L = [] ∈ (T List))
Lemma: nil_member
∀[T:Type]. ∀x:T. ((x ∈ []) ⇐⇒ False)
Lemma: select_member
∀[T:Type]. ∀L:T List. ∀i:ℕ||L||. (L[i] ∈ L)
Lemma: free-from-atom-l_member
∀[T:Type]. ∀[L:T List]. ∀[a:Atom1]. ∀[x:T]. (a#x:T) supposing (a#L:T List and (x ∈ L))
Lemma: member_singleton
∀[T:Type]. ∀a,x:T. ((x ∈ [a]) ⇐⇒ x = a ∈ T)
Lemma: member-merge-int
∀bs,as:ℤ List. ∀x:ℤ. ((x ∈ merge-int(as;bs)) ⇐⇒ (x ∈ as) ∨ (x ∈ bs))
Definition: first-success
first-success(f;L) ==
rec-case(L) of
[] => inr ⋅
a::as =>
r.case f a of inl(x) => inl <0, x> | inr(_) => case r of inl(p) => let i,x = p in inl <i + 1, x> | inr(z) => inr z
Lemma: first-success_wf
∀[T:Type]. ∀[A:T ⟶ Type]. ∀[f:x:T ⟶ (A[x]?)]. ∀[L:T List]. (first-success(f;L) ∈ i:ℕ||L|| × A[L[i]]?)
Lemma: no_repeats_witness
∀[T:Type]. ∀[l:T List]. (no_repeats(T;l) ⇒ (λx.Ax ∈ no_repeats(T;l)))
Lemma: sq_stable__no_repeats
∀[T:Type]. ∀[l:T List]. SqStable(no_repeats(T;l))
Lemma: no_repeats_nil
∀[T:Top]. no_repeats(T;[])
Lemma: no_repeats_nil_uiff
∀[T:Top]. uiff(no_repeats(T;[]);True)
Lemma: last_nil
last([]) ~ ⊥
Lemma: last_member
∀[T:Type]. ∀L:T List. (last(L) ∈ L) supposing ¬↑null(L)
Lemma: last_cons2
∀[L:Top List]. ∀[x:Top]. (last([x / L]) ~ if null(L) then x else last(L) fi )
Lemma: select_append_back
∀[T:Type]. ∀[as,bs:T List]. ∀[i:{||as||..||as|| + ||bs||-}]. (as @ bs[i] = bs[i - ||as||] ∈ T)
Lemma: select_append_front
∀[T:Type]. ∀[as,bs:T List]. ∀[i:ℕ||as||]. (as @ bs[i] = as[i] ∈ T)
Lemma: select-map
∀[f:Top]. ∀[L:Top List]. ∀[i:ℕ||L||]. (map(f;L)[i] ~ f L[i])
Lemma: select-rev-append
∀[T:Type]. ∀[L,bs:T List]. ∀[i:ℕ||L|| + ||bs||].
(rev(L) + bs[i] = if i <z ||L|| then L[||L|| - 1 - i] else bs[i - ||L||] fi ∈ T)
Lemma: map_select
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[as:A List]. ∀[n:ℕ||as||]. (map(f;as)[n] = (f as[n]) ∈ B)
Lemma: listify_select_id
∀[T:Type]. ∀[as:T List]. ((λi:ℕ||as||. as[i])[ℕ||as||] = as ∈ (T List))
Lemma: select_listify_id
∀[T:Type]. ∀[n:ℕ]. ∀[f:ℕn ⟶ T]. ∀[i:ℕn]. ((f)[ℕn][i] = (f i) ∈ T)
Lemma: member_tl
∀[T:Type]. ∀as:T List. ∀x:T. (x ∈ tl(as)) ⇒ (x ∈ as) supposing 0 < ||as||
Lemma: member-implies-null-eq-bfalse
∀[T:Type]. ∀[L:T List]. ∀[x:T]. null(L) = ff supposing (x ∈ L)
Lemma: cons_member
∀[T:Type]. ∀l:T List. ∀a,x:T. ((x ∈ [a / l]) ⇐⇒ (x = a ∈ T) ∨ (x ∈ l))
Lemma: list_extensionality
∀[T:Type]. ∀[a,b:T List].
(a = b ∈ (T List)) supposing ((∀i:ℕ. (i < ||a|| ⇒ (a[i] = b[i] ∈ T))) and (||a|| = ||b|| ∈ ℤ))
Definition: repeat-on-success
repeat-on-success(f;g;h;as;b)
==r case first-success(f;as)
of inl(v) =>
eval as' = evalall(g v as) in
eval b' = h v b in
repeat-on-success(f;g;h;as';b')
| inr(_) =>
<as, b>
Lemma: repeat-on-success_wf
∀[A,B:Type].
(∀[C:Type]. ∀[f:A ⟶ (C?)]. ∀[g:(ℕ × C) ⟶ (A List) ⟶ (A List)].
∀[h:(ℕ × C) ⟶ B ⟶ B]. ∀[as:A List]. ∀[b:B]. (repeat-on-success(f;g;h;as;b) ∈ A List × B)
supposing ∃m:(A List) ⟶ ℕ
∀as:A List. ∀c:C. ∀j:ℕ.
((first-success(f;as) = (inl <j, c>) ∈ (ℕ × C?)) ⇒ m (g <j, c> as) < m as)) supposing
(value-type(B) and
valueall-type(A))
Lemma: no_repeats_inject
∀[T:Type]. ∀[l:T List]. uiff(no_repeats(T;l);Inj(ℕ||l||;T;λi.l[i]))
Lemma: last_cons
∀[T:Type]. ∀[L:T List]. ∀[x:T]. last([x / L]) = last(L) ∈ T supposing ¬↑null(L)
Lemma: list-subtype
∀[A:Type]. ∀[d:A List]. (d ∈ {a:A| (a ∈ d)} List)
Definition: l_all
(∀x∈L.P[x]) == ∀i:ℕ||L||. P[L[i]]
Lemma: l_all_wf
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ ℙ]. ((∀x∈L.P[x]) ∈ ℙ)
Lemma: not-not-l_all-xmiddle
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ ℙ]. (¬¬(∀x∈L.P[x] ∨ (¬P[x])))
Lemma: not-not-l_all-shift
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ ℙ]. ((∀x∈L.¬¬P[x]) ⇒ (¬¬(∀x∈L.P[x])))
Definition: l_exists
(∃x∈L. P[x]) == ∃i:ℕ||L||. P[L[i]]
Lemma: l_exists_wf
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ ℙ]. ((∃x∈L. P[x]) ∈ ℙ)
Lemma: l_exists_wf_nil
∀[P:Void ⟶ Void]. ((∃x∈[]. P[x]) ∈ ℙ)
Lemma: filter_wf5
∀[T:Type]. ∀[l:T List]. ∀[P:{x:T| (x ∈ l)} ⟶ 𝔹]. (filter(P;l) ∈ T List)
Lemma: filter_wf2
∀[T:Type]. ∀[l:T List]. ∀[P:{x:T| (x ∈ l)} ⟶ 𝔹]. (filter(P;l) ∈ {x:T| (x ∈ l)} List)
Lemma: filter_wf_top
∀[T:Type]. ∀[l:T List]. ∀[P:{x:T| (x ∈ l)} ⟶ 𝔹]. (filter(P;l) ∈ Top List)
Lemma: l_all_iff
∀[T:Type]. ∀L:T List. ∀[P:{x:T| (x ∈ L)} ⟶ ℙ]. ((∀x∈L.P[x]) ⇐⇒ ∀x:T. ((x ∈ L) ⇒ P[x]))
Lemma: l_all_nil
∀[P:Top]. (∀x∈[].P[x])
Lemma: l_all_nil_iff
∀[P:Top]. uiff((∀x∈[].P[x]);True)
Lemma: l_all_single
∀[T:Type]. ∀t:T. ∀[P:{x:T| x = t ∈ T} ⟶ ℙ]. ((∀x∈[t].P[x]) ⇐⇒ P[t])
Lemma: l_exists_functionality
∀[T:Type]
∀L:T List. ∀[P,Q:{x:T| (x ∈ L)} ⟶ ℙ]. ((∀x:{x:T| (x ∈ L)} . (P[x] ⇐⇒ Q[x])) ⇒ {(∃x∈L. P[x]) ⇐⇒ (∃x∈L. Q[x])})
Lemma: l_exists_iff
∀[T:Type]. ∀L:T List. ∀[P:{x:T| (x ∈ L)} ⟶ ℙ]. ((∃x∈L. P[x]) ⇐⇒ ∃x:T. ((x ∈ L) ∧ P[x]))
Lemma: l_exists_nil
∀[P:Top]. ((∃x∈[]. P[x]) ⇐⇒ False)
Lemma: l_exists_or
∀[T:Type]. ∀L:T List. ∀P,Q:{x:T| (x ∈ L)} ⟶ ℙ. ((∃x∈L. P[x]) ∨ (∃x∈L. Q[x]) ⇐⇒ (∃x∈L. P[x] ∨ Q[x]))
Lemma: l_all_not
∀[T:Type]. ∀L:T List. ∀P:T ⟶ ℙ. ((∀x∈L.¬P[x]) ⇐⇒ ¬(∃x∈L. P[x]))
Lemma: sq_stable__l_all
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ ℙ]. ((∀[x:{x:T| (x ∈ L)} ]. SqStable(P[x])) ⇒ SqStable((∀x∈L.P[x])))
Lemma: l_all_functionality
∀[T:Type]. ∀L:T List. ∀P,Q:T ⟶ ℙ. ((∀x:T. ((x ∈ L) ⇒ (P[x] ⇐⇒ Q[x]))) ⇒ {(∀x∈L.P[x]) ⇐⇒ (∀x∈L.Q[x])})
Lemma: l_all_wf_nil
∀[P:Void ⟶ Void]. ((∀x∈[].P[x]) ∈ ℙ)
Lemma: l_all_cons
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀x:T. ∀L:T List. ((∀y∈[x / L].P[y]) ⇐⇒ P[x] ∧ (∀y∈L.P[y]))
Lemma: not-l_exists
∀[T:Type]. ∀L:T List. ∀[P:{x:T| (x ∈ L)} ⟶ ℙ]. (¬(∃x∈L. P[x]) ⇐⇒ (∀x∈L.¬P[x]))
Lemma: l_exists_cons
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀x:T. ∀L:T List. ((∃y∈[x / L]. P[y]) ⇐⇒ P[x] ∨ (∃y∈L. P[y]))
Lemma: l_exists_single
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀x:T. ((∃y∈[x]. P[y]) ⇐⇒ P[x])
Lemma: list-set-type
∀[T:Type]. ∀[L:T List]. (L ∈ {x:T| (x ∈ L)} List)
Lemma: list-set-type2
∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ ℙ]. L ∈ {x:T| P[x]} List supposing (∀x∈L.P[x])
Lemma: length-reverse
∀[L:Top]. (||rev(L)|| ~ ||L||)
Lemma: select-reverse
∀[T:Type]. ∀[L:T List]. ∀[i:ℕ||rev(L)||]. (rev(L)[i] = L[||L|| - 1 - i] ∈ T)
Lemma: member-reverse
∀[T:Type]. ∀L:T List. ∀x:T. ((x ∈ rev(L)) ⇐⇒ (x ∈ L))
Lemma: hd-reverse-is-last
∀[T:Type]. ∀[L:T List]. hd(rev(L)) = last(L) ∈ T supposing 0 < ||L||
Lemma: no_repeats_reverse
∀[T:Type]. ∀[L:T List]. uiff(no_repeats(T;rev(L));no_repeats(T;L))
Lemma: l_all_reverse
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀L:T List. ((∀x∈rev(L).P[x]) ⇐⇒ (∀x∈L.P[x]))
Lemma: l_exists_reduce
∀[T:Type]. ∀L:T List. ∀P:T ⟶ 𝔹. ((∃x∈L. ↑P[x]) ⇐⇒ ↑reduce(λx,y. (P[x] ∨by);ff;L))
Lemma: isr-first-success
∀[T:Type]. ∀[A:T ⟶ Type]. ∀[f:x:T ⟶ (A[x]?)]. ∀[L:T List]. (↑isr(first-success(f;L)) ⇐⇒ (∀a∈L.↑isr(f a)))
Lemma: l_all_reduce
∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹]. uiff((∀x∈L.↑P[x]);↑reduce(λx,y. (P[x] ∧b y);tt;L))
Lemma: member_append
∀[T:Type]. ∀x:T. ∀l1,l2:T List. ((x ∈ l1 @ l2) ⇐⇒ (x ∈ l1) ∨ (x ∈ l2))
Lemma: append_is_nil
∀[T:Type]. ∀[l1,l2:T List]. uiff((l1 @ l2) = [] ∈ (T List);(l1 = [] ∈ (T List)) ∧ (l2 = [] ∈ (T List)))
Lemma: l_member_decomp
∀[T:Type]. ∀l:T List. ∀x:T. ((x ∈ l) ⇐⇒ ∃l1,l2:T List. (l = (l1 @ [x] @ l2) ∈ (T List)))
Lemma: l_exists_append
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀L1,L2:T List. ((∃x∈L1 @ L2. P[x]) ⇐⇒ (∃x∈L1. P[x]) ∨ (∃x∈L2. P[x]))
Lemma: l_all_append
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀L1,L2:T List. ((∀x∈L1 @ L2.P[x]) ⇐⇒ (∀x∈L1.P[x]) ∧ (∀x∈L2.P[x]))
Lemma: member_map
∀[T,T':Type]. ∀a:T List. ∀x:T'. ∀f:T ⟶ T'. ((x ∈ map(f;a)) ⇐⇒ ∃y:T. ((y ∈ a) ∧ (x = (f y) ∈ T')))
Lemma: member-map
∀[T,T':Type]. ∀f:T ⟶ T'. ∀a:T List. ∀x:T'. ((x ∈ map(f;a)) ⇐⇒ ∃y:T. ((y ∈ a) ∧ (x = (f y) ∈ T')))
Lemma: l_exists_map
∀[A,B:Type]. ∀f:A ⟶ B. ∀L:A List. ∀[P:B ⟶ ℙ]. ((∃x∈map(f;L). P[x]) ⇐⇒ (∃x∈L. P[f x]))
Lemma: l_all_map
∀[A,B:Type]. ∀f:A ⟶ B. ∀L:A List. ∀[P:B ⟶ ℙ]. ((∀x∈map(f;L).P[x]) ⇐⇒ (∀x∈L.P[f x]))
Definition: map2
map2(f;as;bs)
==r if as = Ax then [] otherwise if bs = Ax then [] otherwise let a,more_as = as
in let b,more_bs = bs
in eval x = f a b in
eval L = map2(f;more_as;more_bs) in
[x / L]
Lemma: map2_wf
∀[T:Type]. ∀[A,B:Type]. ∀[f:A ⟶ B ⟶ T]. ∀[as:A List]. ∀[bs:B List]. (map2(f;as;bs) ∈ T List) supposing value-type(T)
Lemma: cons_one_one
∀[T:Type]. ∀[a,a':T]. ∀[b,b':T List]. uiff([a / b] = [a' / b'] ∈ (T List);{(a = a' ∈ T) ∧ (b = b' ∈ (T List))})
Lemma: co-cons-not-co-nil
∀[T:Type]. ∀[a:T]. ∀[b:colist(T)]. uiff([a / b] = () ∈ colist(T);False)
Lemma: co-cons_one_one
∀[T:Type]. ∀[a,a':T]. ∀[b,b':colist(T)]. uiff([a / b] = [a' / b'] ∈ colist(T);{(a = a' ∈ T) ∧ (b = b' ∈ colist(T))})
Definition: sort-int
sort-int(as) == merge-int([];as)
Lemma: sort-int_wf
∀[T:Type]. ∀[as:T List]. (sort-int(as) ∈ T List) supposing T ⊆r ℤ
Lemma: decidable__l_member
∀[A:Type]. ∀x:A. ((∀x,y:A. Dec(x = y ∈ A)) ⇒ (∀L:A List. Dec((x ∈ L))))
Lemma: sq_stable__l_member
∀[A:Type]. ∀x:A. ((∀x,y:A. Dec(x = y ∈ A)) ⇒ (∀L:A List. SqStable((x ∈ L))))
Definition: combine-list
combine-list(x,y.f[x; y];L) ==
accumulate (with value x and list item y):
f[x; y]
over list:
tl(L)
with starting value:
hd(L))
Lemma: combine-list_wf
∀[A:Type]. ∀[f:A ⟶ A ⟶ A]. ∀[L:A List]. combine-list(x,y.f[x;y];L) ∈ A supposing 0 < ||L||
Lemma: combine-list-cons
∀[A:Type]. ∀[f:A ⟶ A ⟶ A].
∀[L:A List]. ∀[a:A]. (combine-list(x,y.f[x;y];[a / L]) = f[a;combine-list(x,y.f[x;y];L)] ∈ A) supposing 0 < ||L||
supposing Assoc(A;λx,y. f[x;y])
Lemma: combine-list-member
∀[T:Type]
∀f:T ⟶ T ⟶ T. ∀L:T List.
((∀x,y:T. ((f[x;y] = x ∈ T) ∨ (f[x;y] = y ∈ T))) ⇒ 0 < ||L|| ⇒ (combine-list(x,y.f[x;y];L) ∈ L))
Definition: imax-list
imax-list(L) == combine-list(x,y.imax(x;y);L)
Lemma: imax-list_wf
∀[L:ℤ List]. imax-list(L) ∈ ℤ supposing 0 < ||L||
Lemma: concat-cons
∀[l,ll:Top]. (concat([l / ll]) ~ l @ concat(ll))
Lemma: concat_append
∀[a,b:Top]. (concat(a @ b) ~ concat(a) @ concat(b))
Lemma: concat-map-nil
∀[L:Top List]. (concat(map(λx.[];L)) ~ [])
Lemma: decidable__equal_int
∀x,y:ℤ. Dec(x = y ∈ ℤ)
Lemma: decidable__equal_function
∀[T:Type]. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ (∀i,j:ℤ. ∀f,g:{i..j-} ⟶ T. Dec(f = g ∈ ({i..j-} ⟶ T))))
Lemma: sorted-cons
∀[T:Type]. ∀[x:T]. ∀[L:T List]. uiff(sorted([x / L]);sorted(L) ∧ (∀z∈L.x ≤ z)) supposing T ⊆r ℤ
Definition: intlex-aux
intlex-aux(l1;l2)
==r if l1 is a pair then let a,as = l1
in let b,bs = l2
in if (a) < (b) then inl Ax else if a=b then intlex-aux(as;bs) else (inr Ax )
otherwise inl Ax
Lemma: intlex-aux_wf
∀[l1:ℤ List]. ∀[l2:{as:ℤ List| ||as|| = ||l1|| ∈ ℤ} ]. (intlex-aux(l1;l2) ∈ 𝔹)
Lemma: insert-int-comm
∀T:Type. ∀a,b:T. ((T ⊆r ℤ) ⇒ (∀L:T List. (insert-int(b;insert-int(a;L)) = insert-int(a;insert-int(b;L)) ∈ (T List))))
Lemma: no_repeats_cons
∀[T:Type]. ∀[l:T List]. ∀[x:T]. uiff(no_repeats(T;[x / l]);no_repeats(T;l) ∧ (¬(x ∈ l)))
Definition: s-insert
s-insert(x;l) ==
rec-case(l) of
[] => [x]
a::as =>
v.if (x =z a) then [a / as]
if x <z a then [x; [a / as]]
else [a / v]
fi
Lemma: s-insert_wf
∀[T:Type]. ∀[x:T]. ∀[L:T List]. (s-insert(x;L) ∈ T List) supposing T ⊆r ℤ
Lemma: member-s-insert
∀[T:Type]. ∀x:T. ∀L:T List. ∀z:T. ((z ∈ s-insert(x;L)) ⇐⇒ (z = x ∈ T) ∨ (z ∈ L)) supposing T ⊆r ℤ
Lemma: s-insert-sorted
∀[T:Type]. ∀[x:T]. ∀[L:T List]. sorted(s-insert(x;L)) supposing sorted(L) supposing T ⊆r ℤ
Lemma: intlex-aux-antisym
∀[l1:ℤ List]. ∀[l2:{as:ℤ List| ||as|| = ||l1|| ∈ ℤ} ].
(l1 = l2 ∈ (ℤ List)) supposing (intlex-aux(l2;l1) = tt and intlex-aux(l1;l2) = tt)
Lemma: intlex-aux-transitive
∀[l1:ℤ List]. ∀[l2,l3:{as:ℤ List| ||as|| = ||l1|| ∈ ℤ} ].
(intlex-aux(l1;l3) = tt) supposing (intlex-aux(l2;l3) = tt and intlex-aux(l1;l2) = tt)
Definition: intlex
l1 ≤_lex l2 == eval n1 = ||l1|| in eval n2 = ||l2|| in n1 <z n2 ∨b((n1 =z n2) ∧b intlex-aux(l1;l2))
Lemma: intlex_wf
∀[l1,l2:ℤ List]. (l1 ≤_lex l2 ∈ 𝔹)
Lemma: member-insert-int
∀[T:Type]. ∀l:T List. ∀x,z:T. ((z ∈ insert-int(x;l)) ⇐⇒ (z = x ∈ T) ∨ (z ∈ l)) supposing T ⊆r ℤ
Lemma: insert-int-sorted
∀[T:Type]. ∀[x:T]. ∀[l:T List]. sorted(insert-int(x;l)) supposing sorted(l) supposing T ⊆r ℤ
Lemma: merge-int-sorted
∀[T:Type]. ∀[as,bs:T List]. sorted(merge-int(bs;as)) supposing sorted(bs) supposing T ⊆r ℤ
Lemma: member-merge-int
∀bs,as:ℤ List. ∀x:ℤ. ((x ∈ merge-int(as;bs)) ⇐⇒ (x ∈ as) ∨ (x ∈ bs))
Lemma: no_repeats_singleton
∀[T:Type]. ∀[x:T]. no_repeats(T;[x])
Lemma: no_repeats_singleton_uiff
∀[T:Type]. ∀[x:T]. uiff(no_repeats(T;[x]);True)
Lemma: intlex-length
∀[l1,l2:ℤ List]. ||l1|| ≤ ||l2|| supposing ↑l1 ≤_lex l2
Lemma: intlex-by-length
∀[l1,l2:ℤ List]. ↑l1 ≤_lex l2 supposing ||l1|| < ||l2||
Lemma: intlex-antisym
∀[l1,l2:ℤ List]. (l1 = l2 ∈ (ℤ List)) supposing (l2 ≤_lex l1 = tt and l1 ≤_lex l2 = tt)
Lemma: intlex-transitive
∀[l1,l2,l3:ℤ List]. (l1 ≤_lex l3 = tt) supposing (l2 ≤_lex l3 = tt and l1 ≤_lex l2 = tt)
Lemma: intlex-total
∀as,bs:ℤ List. ((↑as ≤_lex bs) ∨ (↑bs ≤_lex as))
Lemma: intlex-cons
∀l1,l2:ℤ List. ∀x,y:ℤ.
uiff(↑[x / l1] ≤_lex [y / l2];||l1|| < ||l2|| ∨ (x < y ∧ (||l1|| = ||l2|| ∈ ℤ)) ∨ ((x = y ∈ ℤ) ∧ (↑l1 ≤_lex l2)))
Definition: apply_alist
This version of apply alist assumes that the thing ⌜x⌝ being looked for
occurs in the association list.
Another version ⌜apply-alist(eq;L;x)⌝ will return ⌜inr ⋅ ⌝ when x does
not occur.⋅
apply_alist(eq;L;x) == let a,more = L in let x',v = a in case eq x' x of inl(_) => v | inr(_) => apply_alist(eq;more;x)
Lemma: apply_alist_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[V:Type]. ∀[L:(T × V) List].
apply_alist(eq;L;x) ∈ {v:V| (<x, v> ∈ L)} supposing (x ∈ map(λa.(fst(a));L))
Definition: apply-alist
apply-alist(eq;L;x) == rec-case(L) of [] => inr ⋅ | p::ps => r.if eq (fst(p)) x then inl (snd(p)) else r fi
Lemma: apply-alist_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[V:Type]. ∀[L:(T × V) List]. (apply-alist(eq;L;x) ∈ V?)
Lemma: apply_alist-eager-map
∀[T:Type]
∀[eq:EqDecider(T)]. ∀[f:Top]. ∀[L:T List]. ∀[i:{i:T| (i ∈ L)} ]. (apply_alist(eq;eager-map(λi.<i, f i>;L);i) ~ f i)
supposing value-type(T) ∧ (T ⊆r Base)
Lemma: apply_alist-eager-map2
∀[A:Type]. ∀[L:A List]. ∀[T:Type].
∀[eq:EqDecider(T)]. ∀[g:A ⟶ T]. ∀[f:Top]. ∀[i:{i:T| (i ∈ eager-map(g;L))} ].
(apply_alist(eq;eager-map(λa.<g a, f (g a)>;L);i) ~ f i)
supposing value-type(T) ∧ (T ⊆r Base)
Lemma: apply_alist-eager-map-atom
∀[T:Type]. ∀[L:T List]. ∀[g:T ⟶ Atom]. ∀[f:Top]. ∀[i:{i:Atom| (i ∈ eager-map(g;L))} ].
(apply_alist(AtomDeq;eager-map(λa.<g a, f (g a)>;L);i) ~ f i)
Lemma: apply-alist-function
∀[T,A:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[F:T ⟶ A]. ∀[L:T List].
apply-alist(eq;map(λx.<x, F[x]>;L);x) = (inl F[x]) ∈ (A?) supposing (x ∈ L)
Lemma: apply_alist_cons_lemma
∀x,v,u,eq:Top. (apply-alist(eq;[u / v];x) ~ if eqof(eq) (fst(u)) x then inl (snd(u)) else apply-alist(eq;v;x) fi )
Lemma: apply-updated-alist
∀[A,T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:T]. ∀[L:(T × A) List]. ∀[z:A]. ∀[f:A ⟶ A].
(apply-alist(eq;update-alist(eq;L;x;z;v.f[v]);y)
= case apply-alist(eq;L;y)
of inl(v) =>
inl if eq x y then f[v] else v fi
| inr(any) =>
if eq x y then inl z else inr ⋅ fi
∈ (A?))
Lemma: apply-alist-cases
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[L:(T × Top) List].
(apply-alist(eq;L;x) ~ ff supposing ¬(x ∈ map(λp.(fst(p));L))
∧ (∀[i:ℕ||L||]
(apply-alist(eq;L;x) ~ inl (snd(L[i]))) supposing (((fst(L[i])) = x ∈ T) and (∀j:ℕi. (¬((fst(L[j])) = x ∈ T))))))
Lemma: intlex-cons-same
∀[l1,l2:ℤ List]. ∀[x:ℤ]. uiff(↑[x / l1] ≤_lex [x / l2];↑l1 ≤_lex l2)
Definition: firstn
firstn(n;as) ==
fix((λfirstn,n,as. case as of [] => [] | a::as' => if 0 <z n then [a / (firstn (n - 1) as')] else [] fi esac)) n as
Lemma: firstn_wf
∀[A:Type]. ∀[as:A List]. ∀[n:ℤ]. (firstn(n;as) ∈ A List)
Lemma: comb_for_firstn_wf
λA,as,n,z. firstn(n;as) ∈ A:Type ⟶ as:(A List) ⟶ n:ℤ ⟶ (↓True) ⟶ (A List)
Lemma: length_firstn
∀[A:Type]. ∀[as:A List]. ∀[n:{0...||as||}]. (||firstn(n;as)|| ~ n)
Lemma: length-firstn-le
∀[as:Top List]. ∀[n:ℕ]. (||firstn(n;as)|| ≤ n)
Lemma: first0
∀[L:Top List]. (firstn(0;L) ~ [])
Lemma: firstn-firstn
∀[L:Top List]. ∀[n:ℕ]. ∀[m:ℕn]. (firstn(m;firstn(n;L)) ~ firstn(m;L))
Definition: segment
as[m..n-] == firstn(n - m;nth_tl(m;as))
Lemma: segment_wf
∀[T:Type]. ∀[as:T List]. ∀[m,n:ℤ]. (as[m..n-] ∈ T List)
Lemma: whole_segment-sq
∀as:Top List. (as[0..||as||-] ~ as)
Lemma: whole_segment
∀T:Type. ∀as:T List. ((as[0..||as||-]) = as ∈ (T List))
Lemma: length_firstn_eq
∀[A:Type]. ∀[as:A List]. ∀[n:{0...||as||}]. (||firstn(n;as)|| = n ∈ ℤ)
Lemma: comb_for_segment_wf
λT,as,m,n,z. (as[m..n-]) ∈ T:Type ⟶ as:(T List) ⟶ m:ℤ ⟶ n:ℤ ⟶ (↓True) ⟶ (T List)
Lemma: length_segment
∀[T:Type]. ∀[as:T List]. ∀[i:{0...||as||}]. ∀[j:{i...||as||}]. (||as[i..j-]|| = (j - i) ∈ ℤ)
Lemma: list_decomp
∀[T:Type]. ∀[L:T List]. L ~ [hd(L) / tl(L)] supposing 0 < ||L||
Lemma: firstn_decomp
∀[T:Type]. ∀[j:ℕ]. ∀[l:T List]. (firstn(j - 1;l) @ [l[j - 1]] ~ firstn(j;l)) supposing (j - 1 < ||l|| and 0 < j)
Lemma: select-firstn
∀[L:Top List]. ∀[n:ℕ]. ∀[x:ℕn]. (firstn(n;L)[x] ~ L[x])
Lemma: select_firstn
∀[T:Type]. ∀[as:T List]. ∀[n:{0...||as||}]. ∀[i:ℕn]. (firstn(n;as)[i] = as[i] ∈ T)
Lemma: filter_nil_lemma
∀P:Top. (filter(P;[]) ~ [])
Lemma: filter_cons_lemma
∀t,h,f:Top. (filter(f;[h / t]) ~ if f h then [h / filter(f;t)] else filter(f;t) fi )
Lemma: filter-cons
∀[P,x,L:Top]. (filter(P;[x / L]) ~ if P x then [x / filter(P;L)] else filter(P;L) fi )
Definition: list_accum'
list_accum'(f;v;L)==r if null(L) then v else let v' ⟵ f v L in let a,as = L in list_accum'(f;v';as) fi
Lemma: list_accum'_wf
∀[A,B:Type].
∀[f:B ⟶ {L:A List| 0 < ||L||} ⟶ B]. ∀[L:A List]. ∀[v:B]. (list_accum'(f;v;L) ∈ B) supposing valueall-type(B)
Definition: find_transitions
find_transitions(f;L) ==
let h,hs = L
in eval b = f h hd(hs) in
snd(snd(list_accum'(λd,l. let i,b,p,q = d
in if isr(p) ∧b isr(q)
then d
else let a,as = l
in eval i' = i + 1 in
if null(as)
then eval b' = f a h in
if b ∧b (¬bb')
then eval q' = if isl(q) then inr 0 else q fi in
<i', b', inr i , q'>
if b' ∧b (¬bb)
then eval p' = if isl(p) then inr 0 else p fi in
<i', b', p', inr i >
if isr(p) then <i', b', p, inr 0 >
if isr(q) then <i', b', inr 0 , q>
else <i', b', p, q>
fi
else eval b' = f a hd(as) in
if b ∧b (¬bb') then <i', b', inr i , q>
if b' ∧b (¬bb) then <i', b', p, inr i >
else <i', b', p, q>
fi
fi
fi ;<1, b, inl ⋅, inl ⋅>;tl(L))))
Lemma: find_transitions_wf
∀[A:Type]. ∀[f:A ⟶ A ⟶ 𝔹]. ∀[L:A List]. find_transitions(f;L) ∈ Unit + ℤ × (Unit + ℤ) supposing 1 < ||L||
Lemma: length-map2
∀[T:Type]
∀[A,B:Type]. ∀[f:A ⟶ B ⟶ T]. ∀[as:A List]. ∀[bs:B List].
||map2(f;as;bs)|| = ||as|| ∈ ℤ supposing ||as|| = ||bs|| ∈ ℤ
supposing value-type(T)
Lemma: select-map2
∀[T:Type]
∀[A,B:Type]. ∀[f:A ⟶ B ⟶ T]. ∀[as:A List]. ∀[bs:B List].
∀[i:ℕ||as||]. (map2(f;as;bs)[i] = (f as[i] bs[i]) ∈ T) supposing ||as|| = ||bs|| ∈ ℤ
supposing value-type(T)
Lemma: sort-int-trivial
∀T:Type. ∀bs:T List. ((T ⊆r ℤ) ⇒ sorted(bs) ⇒ (sort-int(bs) = bs ∈ (T List)))
Lemma: merge-int-comm
∀[T:Type]
∀[as,bs:T List]. merge-int(as;bs) = merge-int(bs;as) ∈ (T List) supposing sorted(as) ∧ sorted(bs) supposing T ⊆r ℤ
Lemma: insert-int-1-1
∀[T:Type]
∀[as,bs:T List].
(∀[x:T]. as = bs ∈ (T List) supposing insert-int(x;as) = insert-int(x;bs) ∈ (T List)) supposing
(sorted(bs) and
sorted(as))
supposing T ⊆r ℤ
Lemma: merge-int-1-1
∀[T:Type]
∀[cs,as,bs:T List].
(as = bs ∈ (T List)) supposing ((merge-int(as;cs) = merge-int(bs;cs) ∈ (T List)) and sorted(bs) and sorted(as))
supposing T ⊆r ℤ
Lemma: merge-int-one-one
∀[T:Type]
∀[as,bs,cs:T List].
(as = bs ∈ (T List)) supposing
((merge-int(cs;as) = merge-int(cs;bs) ∈ (T List)) and
sorted(bs) and
sorted(as) and
sorted(cs))
supposing T ⊆r ℤ
Lemma: intlex-aux-reflexive
∀[l1,l2:ℤ List]. intlex-aux(l1;l2) = tt supposing l1 = l2 ∈ (ℤ List)
Lemma: intlex-reflexive
∀[l1,l2:ℤ List]. l1 ≤_lex l2 = tt supposing l1 = l2 ∈ (ℤ List)
Lemma: insert-int-lex
∀as,bs:ℤ List. ∀x:ℤ. ((↑as ≤_lex bs) ⇒ (↑insert-int(x;as) ≤_lex insert-int(x;bs)))
Lemma: merge-int-lex
∀cs,as,bs:ℤ List. ((↑as ≤_lex bs) ⇒ (↑merge-int(as;cs) ≤_lex merge-int(bs;cs)))
Lemma: filter_trivial
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. filter(P;L) ~ L supposing (∀x∈L.↑P[x])
Lemma: filter_trivial2
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. filter(P;L) = L ∈ (T List) supposing (∀x∈L.↑P[x])
Lemma: filter_tt
∀[L:Top List]. (filter(λx.tt;L) ~ L)
Lemma: filter-bfalse
∀[L:Top List]. (filter(λx.ff;L) ~ [])
Lemma: filter_type
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[l:T List]. (filter(P;l) ∈ {x:T| ↑(P x)} List)
Lemma: filter_type2
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[l:T List]. (filter(λx.P[x];l) ∈ {x:T| ↑P[x]} List)
Lemma: filter_wf3
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[l:T List]. (filter(λx.P[x];l) ∈ {x:T| ↑P[x]} List)
Lemma: filter_wf4
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[l:T List]. (filter(λx.P[x];l) ∈ {x:T| (x ∈ l) ∧ (↑P[x])} List)
Lemma: filter_wf4_2
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[l:T List]. (filter(P;l) ∈ {x:T| (x ∈ l) ∧ (↑P[x])} List)
Lemma: member-filter
∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L:T List. ∀x:{x:T| ↑P[x]} . ((x ∈ filter(λx.P[x];L)) ⇐⇒ (x ∈ L))
Lemma: filter_is_nil
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. filter(P;L) ~ [] supposing (∀x∈L.¬↑(P x))
Lemma: filter_is_nil2
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. filter(P;L) ~ [] supposing (∀x∈L.¬↑P[x])
Lemma: null_filter
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. ↑null(filter(P;L)) supposing (∀x∈L.¬↑P[x])
Lemma: null-filter2
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. uiff(↑null(filter(P;L));(∀x∈L.¬↑(P x)))
Lemma: null-filter
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. uiff(↑null(filter(P;L));(∀x∈L.¬↑P[x]))
Lemma: non_null_filter
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. ¬↑null(filter(P;L)) supposing (∃x∈L. ↑P[x])
Lemma: member_filter
∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L:T List. ∀x:T. ((x ∈ filter(P;L)) ⇐⇒ (x ∈ L) ∧ (↑(P x)))
Lemma: sorted-filter
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. sorted(filter(P;L)) supposing sorted(L) supposing T ⊆r ℤ
Lemma: l_all_filter
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. (∀x∈filter(P;L).↑(P x))
Lemma: l_all_filter_iff
∀[T:Type]. ∀[Q:T ⟶ ℙ]. ∀P:T ⟶ 𝔹. ∀L:T List. ((∀x∈filter(P;L).Q[x]) ⇐⇒ ∀x:T. ((x ∈ L) ⇒ (↑(P x)) ⇒ Q[x]))
Lemma: l_all_implies_l_all_filter
∀[T:Type]. ∀[Q:T ⟶ ℙ]. ∀P:T ⟶ 𝔹. ∀L:T List. ((∀x∈L.Q[x]) ⇒ (∀x∈filter(P;L).Q[x]))
Lemma: hd_member
∀[T:Type]. ∀L:T List. (hd(L) ∈ L) supposing ¬↑null(L)
Lemma: non_null_filter_iff
∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L:T List. uiff((∃x∈L. ↑P[x]);¬↑null(filter(P;L)))
Lemma: member_filter_2
∀[T:Type]. ∀L:T List. ∀P:{x:T| (x ∈ L)} ⟶ 𝔹. ∀x:T. ((x ∈ filter(P;L)) ⇐⇒ (x ∈ L) ∧ (↑(P x)))
Lemma: eval_list_sq
∀[t:Top List]. (eval_list(t) ~ t)
Definition: insert
insert(a;L) == eval x = eval_list(L) in if a ∈b x then x else [a / x] fi
Lemma: insert_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[L:T List]. (insert(a;L) ∈ T List)
Lemma: deq_member_nil_lemma
∀x,eq:Top. (x ∈b [] ~ ff)
Lemma: deq_member_cons_lemma
∀v,u,x,eq:Top. (x ∈b [u / v] ~ (eq u x) ∨bx ∈b v)
Lemma: insert_nil_lemma
∀x,eq:Top. (insert(x;[]) ~ [x])
Lemma: assert-deq-member
∀[A:Type]. ∀eq:EqDecider(A). ∀L:A List. ∀x:A. (↑x ∈b L ⇐⇒ (x ∈ L))
Lemma: deq-member-append
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[L1,L2:A List]. ∀[x:A]. (x ∈b L1 @ L2 ~ x ∈b L1 ∨bx ∈b L2)
Lemma: insert-cases
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[L:T List].
(insert(a;L) ~ L supposing (a ∈ L) ∧ insert(a;L) ~ [a / L] supposing ¬(a ∈ L))
Lemma: insert-cases2
∀[T:Type]. ∀eq:EqDecider(T). ∀a:T. ∀L:T List. (((a ∈ L) ∧ (insert(a;L) ~ L)) ∨ ((¬(a ∈ L)) ∧ (insert(a;L) ~ [a / L])))
Lemma: insert-not-nil
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[L:T List]. (¬(insert(a;L) = [] ∈ (T List)))
Lemma: last-insert
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[x:T]. (last(insert(x;L)) = if null(L) then x else last(L) fi ∈ T)
Lemma: member-insert
∀[T:Type]. ∀eq:EqDecider(T). ∀a:T. ∀L:T List. ∀b:T. ((b ∈ insert(a;L)) ⇐⇒ (b = a ∈ T) ∨ (b ∈ L))
Lemma: insert_property
∀[T:Type]
∀eq:EqDecider(T). ∀a:T. ∀L:T List.
((∀b:T. ((b ∈ insert(a;L)) ⇐⇒ (b = a ∈ T) ∨ (b ∈ L))) ∧ no_repeats(T;insert(a;L)) supposing no_repeats(T;L))
Definition: l-union
as ⋃ bs == reduce(λa,L. insert(a;L);as;bs)
Lemma: l-union_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:T List]. (as ⋃ bs ∈ T List)
Lemma: no_repeats-insert
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[L:T List]. no_repeats(T;insert(a;L)) supposing no_repeats(T;L)
Lemma: trivial_map
∀[T:Type]. ∀[a:T List]. ∀[f:T ⟶ T]. map(f;a) = a ∈ (T List) supposing ∀x:T. ((x ∈ a) ⇒ ((f x) = x ∈ T))
Lemma: rev-append-property-top
∀[as,bs,cs:Top]. (rev(as) + bs @ cs ~ rev(as) + bs @ cs)
Lemma: reverse-cons
∀[as,a:Top]. (rev([a / as]) ~ rev(as) @ [a])
Lemma: reverse_nil_lemma
rev([]) ~ []
Lemma: map_map
∀[f,g,a:Top]. (map(g;map(f;a)) ~ map(g o f;a))
Lemma: map-map
∀[as,f,g:Top]. (map(g;map(f;as)) ~ map(g o f;as))
Lemma: map-id
∀[L:Top List]. (map(λx.x;L) ~ L)
Definition: eager-accum
eager-accum(x,a.f[x; a];y;l) ==
fix((λeager-accum,y,l. if l = Ax then y otherwise let h,t = l in let z ⟵ f[y; h] in eager-accum z t)) y l
Lemma: eager-accum_wf
∀[T,T':Type]. ∀[l:T List]. ∀[y:T']. ∀[f:T' ⟶ T ⟶ T']. eager-accum(x,a.f[x;a];y;l) ∈ T' supposing valueall-type(T')
Definition: merge-int-accum
merge-int-accum(as;bs) == eager-accum(l,b.insert-int(b;l);as;bs)
Lemma: merge-int-accum_wf
∀[as,bs:ℤ List]. (merge-int-accum(as;bs) ∈ ℤ List)
Lemma: merge-int-accum-sq
∀[bs,as:ℤ List]. (merge-int-accum(as;bs) ~ merge-int(as;bs))
Lemma: pos-length
∀[A:Type]. ∀[l:A List]. uiff(¬(l = [] ∈ (A List));0 < ||l||)
Definition: list-deq
list-deq(eq) ==
λas,bs. (rec-case(as) of
[] => λL.null(L)
a::as' =>
r.λL.rec-case(L) of
[] => ff
b::bs' =>
r2.(eq a b) ∧b (r bs')
bs)
Lemma: list-deq_wf1
∀[A:Type]. ∀[eq:A ⟶ A ⟶ 𝔹]. (list-deq(eq) ∈ (A List) ⟶ (A List) ⟶ 𝔹)
Lemma: list-deq_wf
∀[A:Type]. ∀[eq:EqDecider(A)]. (list-deq(eq) ∈ EqDecider(A List))
Definition: list_eq
list_eq(eq;as;bs) ==
if null(as) then null(bs) else (¬bnull(bs)) ∧b let a,aa = as in let b,bb = bs in (eq a b) ∧b list_eq(eq;aa;bb) fi
Lemma: list_eq_wf
∀[A:Type]. ∀[eq:A ⟶ A ⟶ 𝔹]. ∀[as,bs:A List]. (list_eq(eq;as;bs) ∈ 𝔹)
Lemma: assert-list_eq
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[as,bs:A List]. uiff(↑list_eq(eq;as;bs);as = bs ∈ (A List))
Lemma: list_eq-sq-list-deq
∀[eq:Top]. ∀[as,bs:Top List]. (list_eq(eq;as;bs) ~ list-deq(eq) as bs)
Lemma: firstn_all
∀[L:Top List]. ∀[n:ℤ]. firstn(n;L) ~ L supposing ||L|| ≤ n
Lemma: firstn-append
∀[L1,L2:Top List]. ∀[n:ℕ]. (firstn(n;L1 @ L2) ~ if n ≤z ||L1|| then firstn(n;L1) else L1 @ firstn(n - ||L1||;L2) fi )
Lemma: strong-continuous-list
∀[F:Type ⟶ Type]. Continuous+(T.F[T] List) supposing Continuous+(T.F[T])
Lemma: list-continuity
∀[X:ℕ ⟶ Type]. ((⋂n:ℕ. (X[n] List)) ⊆r ((⋂n:ℕ. X[n]) List))
Lemma: sqntype_list
∀[A:Type]. ∀[n:ℕ]. sqntype(n;A List) supposing sqntype(n;A)
Home
Index