Definition: tuple-type
tuple-type(L) == rec-case(L) of [] => Unit | T::Ts => r.if null(Ts) then T else T × r fi
Lemma: tuple-type_wf
∀[L:Type List]. (tuple-type(L) ∈ Type)
Definition: n-tuple
n-tuple(n) == tuple-type(map(λx.Top;upto(n)))
Lemma: n-tuple_wf
∀[n:ℕ]. (n-tuple(n) ∈ Type)
Lemma: n-tuple-decomp
∀[n:ℕ]. (n-tuple(n) ~ if (n =z 0) then Unit if (n =z 1) then Top else Top × n-tuple(n - 1) fi )
Lemma: tupletype_nil_lemma
tuple-type([]) ~ Unit
Lemma: tupletype_cons_lemma
∀L,T:Top. (tuple-type([T / L]) ~ if null(L) then T else T × tuple-type(L) fi )
Lemma: tuple-type-valueall-type
∀[L:{T:Type| valueall-type(T)} List]. valueall-type(tuple-type(L))
Lemma: subtype_rel_tuple-type
∀[As,Bs:Type List]. tuple-type(As) ⊆r tuple-type(Bs) supposing (||As|| = ||Bs|| ∈ ℤ) ∧ (∀i:ℕ||As||. (As[i] ⊆r Bs[i]))
Lemma: tuple-type-ext
∀[L,L':Type List]. tuple-type(L) ≡ tuple-type(L') supposing (||L|| = ||L'|| ∈ ℤ) ∧ (∀i:ℕ||L||. L[i] ≡ L'[i])
Lemma: tuple-type-subtype-n-tuple
∀[L:Type List]. ∀[n:ℕ]. tuple-type(L) ⊆r n-tuple(n) supposing ||L|| = n ∈ ℤ
Definition: tuple
tuple(n;i.F[i]) == rec-case(map(λi.F[i];upto(n))) of [] => ⋅ | a::as => r.if null(as) then a else <a, r> fi
Lemma: tuple_wf
∀[L:Type List]. ∀[F:i:ℕ||L|| ⟶ L[i]]. ∀[n:{n:ℤ| n = ||L|| ∈ ℤ} ]. (tuple(n;i.F[i]) ∈ tuple-type(L))
Lemma: tuple-decomp
∀[n:ℕ]. ∀[F:Top]. (tuple(n;i.F[i]) ~ if (n =z 0) then ⋅ if (n =z 1) then F[0] else <F[0], tuple(n - 1;i.F[i + 1])> fi )
Lemma: tuple_wf_ntuple
∀[n:ℕ]. ∀[F:Top]. (tuple(n;i.F[i]) ∈ n-tuple(n))
Lemma: tuple1_lemma
∀F:Top. (tuple(1;x.F[x]) ~ F[0])
Lemma: tuple2_lemma
∀F:Top. (tuple(2;x.F[x]) ~ <F[0], F[1]>)
Definition: ap-tuple
ap-tuple(len;f;t) ==
fix((λap-tuple,len,f,t. if (len =z 0) then t
if (len =z 1) then f t
else <(fst(f)) (fst(t)), ap-tuple (len - 1) (snd(f)) (snd(t))>
fi ))
len
f
t
Lemma: ap-tuple_wf
∀[n:ℕ]. ∀[A,B:Type List].
∀[f:tuple-type(map(λp.((fst(p)) ⟶ (snd(p)));zip(A;B)))]. ∀[t:tuple-type(A)]. (ap-tuple(n;f;t) ∈ tuple-type(B))
supposing (||A|| = n ∈ ℤ) ∧ (||B|| = n ∈ ℤ)
Definition: ap2-tuple
ap2-tuple(len;f;x;t) ==
fix((λap2-tuple,len,f,t. if (len =z 0) then t
if (len =z 1) then f x t
else <(fst(f)) x (fst(t)), ap2-tuple (len - 1) (snd(f)) (snd(t))>
fi ))
len
f
t
Lemma: ap2-tuple_wf
∀[n:ℕ]. ∀[A,B:Type List].
∀[C:Type]. ∀[x:C]. ∀[f:tuple-type(map(λp.(C ⟶ (fst(p)) ⟶ (snd(p)));zip(A;B)))]. ∀[t:tuple-type(A)].
(ap2-tuple(n;f;x;t) ∈ tuple-type(B))
supposing (||A|| = n ∈ ℤ) ∧ (||B|| = n ∈ ℤ)
Lemma: ap2-tuple_wf_ntuple
∀[n:ℕ]. ∀[x:Top]. ∀[f,t:n-tuple(n)]. (ap2-tuple(n;f;x;t) ∈ n-tuple(n))
Definition: map-tuple
map-tuple(len;f;t) ==
fix((λmap-tuple,len,t. if (len =z 0) then t if (len =z 1) then f t else <f (fst(t)), map-tuple (len - 1) (snd(t))> fi \000C)) len t
Lemma: map-tuple_wf
∀[n:ℕ]. ∀[A,B:Type List].
∀[f:⋂i:ℕn. (A[i] ⟶ B[i])]. ∀[t:tuple-type(A)]. (map-tuple(n;f;t) ∈ tuple-type(B))
supposing (||A|| = n ∈ ℤ) ∧ (||B|| = n ∈ ℤ)
Lemma: map-tuple_wf_ntuple
∀[n:ℕ]. ∀[f:Top]. ∀[t:n-tuple(n)]. (map-tuple(n;f;t) ∈ n-tuple(n))
Definition: tuple-sum
tuple-sum(f;L;x) ==
if null(L) then 0 else let a,as = L in if null(as) then f a x else let u,v = x in (f a u) + tuple-sum(f;as;v) fi fi
Lemma: tuple-sum_wf
∀[P:Type]. ∀[as:P List]. ∀[G:P ⟶ Type]. ∀[x:tuple-type(map(G;as))]. ∀[f:i:P ⟶ (G i) ⟶ ℕ]. (tuple-sum(f;as;x) ∈ ℕ)
Lemma: tuple-sum-wf-partial
∀[P:Type]. ∀[G:P ⟶ Type]. ∀[f:i:P ⟶ (G i) ⟶ partial(ℕ)]. ∀[as:P List]. ∀[x:tuple-type(map(G;as))].
(tuple-sum(f;as;x) ∈ partial(ℕ))
Definition: update-tuple
update-tuple(len;x;n;y) ==
fix((λupdate-tuple,len,x,n. if (n =z 0)
then if (len =z 1) then y else <y, snd(x)> fi
else <fst(x), update-tuple (len - 1) (snd(x)) (n - 1)>
fi ))
len
x
n
Lemma: update-tuple_wf
∀[L:Type List]. ∀[n:ℕ]. ∀[x:tuple-type(L)]. ∀[y:L[n]]. (update-tuple(||L||;x;n;y) ∈ tuple-type(L)) supposing n < ||L||
Definition: select-tuple
x.n ==
fix((λselect-tuple,len,x,n. if (n =z 0)
then if (len =z 1) then x else fst(x) fi
else select-tuple (len - 1) (snd(x)) (n - 1)
fi ))
len
x
n
Lemma: select-tuple_wf
∀[L:Type List]. ∀[n:ℕ]. ∀[k:ℤ]. ∀[x:tuple-type(L)]. (x.n ∈ L[n]) supposing n < ||L|| ∧ (k = ||L|| ∈ ℤ)
Lemma: select-tuple-tuple
∀[n:ℕ]. ∀[i:ℕn]. ∀[F:Top]. (tuple(n;i.F[i]).i ~ F[i])
Lemma: map-tuple-as-tuple
∀[n:ℕ]. ∀[f:Top]. ∀[t:n-tuple(n)]. (map-tuple(n;f;t) ~ tuple(n;i.f t.i))
Lemma: map-tuple-tuple
∀[n:ℕ]. ∀[f,G:Top]. (map-tuple(n;f;tuple(n;i.G[i])) ~ tuple(n;i.f G[i]))
Lemma: ap-tuple-as-tuple
∀[n:ℕ]. ∀[f,t:n-tuple(n)]. (ap-tuple(n;f;t) ~ tuple(n;i.f.i t.i))
Lemma: ap2-tuple-as-tuple
∀[n:ℕ]. ∀[f,t:n-tuple(n)]. ∀[x:Top]. (ap2-tuple(n;f;x;t) ~ tuple(n;i.f.i x t.i))
Lemma: map-tuple-ap2-tuple
∀[n:ℕ]. ∀[f,x:Top]. ∀[g,t:n-tuple(n)].
(map-tuple(n;f;ap2-tuple(n;g;x;t)) ~ ap2-tuple(n;map-tuple(n;λh,x,z. (f (h x z));g);x;t))
Lemma: le-tuple-sum
∀[P:Type]. ∀[as:P List]. ∀[G:P ⟶ Type]. ∀[x:tuple-type(map(G;as))]. ∀[f:i:P ⟶ (G i) ⟶ ℕ].
∀k:ℕ||as||. ((f as[k] x.k) ≤ tuple-sum(f;as;x))
Definition: split-tuple
split-tuple(x;n) ==
fix((λsplit-tuple,x,n. if (n =z 0) then <⋅, x>
if (n =z 1) then <fst(x), snd(x)>
else let a,b = split-tuple (snd(x)) (n - 1)
in <<fst(x), a>, b>
fi ))
x
n
Lemma: split-tuple_wf
∀[L:Type List]. ∀[x:tuple-type(L)]. ∀[n:ℕ||L||]. (split-tuple(x;n) ∈ tuple-type(firstn(n;L)) × tuple-type(nth_tl(n;L)))
Definition: shorten-tuple
shorten-tuple(x;n) == fix((λshorten-tuple,x,n. if n ≤z 0 then x else shorten-tuple (snd(x)) (n - 1) fi )) x n
Lemma: shorten-tuple-split-tuple
∀[n:ℕ]. ∀[x:Top]. (shorten-tuple(x;n) ~ snd(split-tuple(x;n)))
Lemma: shorten-tuple_wf
∀[L:Type List]. ∀[n:ℕ||L||]. ∀[x:tuple-type(L)]. (shorten-tuple(x;n) ∈ tuple-type(nth_tl(n;L)))
Lemma: shorten-tuple_wf2
∀[L1,L2:Type List]. ∀[x:tuple-type(L1 @ L2)]. shorten-tuple(x;||L1||) ∈ tuple-type(L2) supposing 0 < ||L2||
Definition: append-tuple
append-tuple(n;m;x;y) ==
fix((λappend-tuple,n,x. if n ≤z 0 then y
if (n =z 1) then if m ≤z 0 then x else <x, y> fi
else let a,b = x
in <a, append-tuple (n - 1) b>
fi ))
n
x
Lemma: append-tuple_wf
∀[L1,L2:Type List]. ∀[x:tuple-type(L1)]. ∀[y:tuple-type(L2)]. (append-tuple(||L1||;||L2||;x;y) ∈ tuple-type(L1 @ L2))
Lemma: append-tuple-zero
∀[L:Type List]. ∀[x:tuple-type(L)]. ∀[y:Top]. (append-tuple(||L||;0;x;y) ~ if (||L|| =z 0) then y else x fi )
Lemma: append-tuple-split-tuple
∀[L:Type List]. ∀[x:tuple-type(L)]. ∀[n:ℕ||L||].
(append-tuple(n;||L|| - n;fst(split-tuple(x;n));snd(split-tuple(x;n))) ~ x)
Lemma: split-tuple-append-tuple
∀[L1,L2:Type List].
∀[x:tuple-type(L1)]. ∀[y:tuple-type(L2)]. (split-tuple(append-tuple(||L1||;||L2||;x;y);||L1||) ~ <x, y>) supposing 0 \000C< ||L2||
Lemma: append-tuple-shorten-tuple
∀[L:Type List]. ∀[x:tuple-type(L)]. ∀[n:ℕ||L||].
(append-tuple(n;||L|| - n;fst(split-tuple(x;n));shorten-tuple(x;n)) ~ x)
Lemma: append-tuple-simplify
∀[p:Top × Top]. (fst(snd(let x,y = p in <x, y, ⋅>)) ~ snd(p))
Lemma: shorten-tuple-simplify
∀[p:Top × Top × Top]. (fst(shorten-tuple(p;1)) ~ fst(snd(p)))
Lemma: shorten-tuple-simplify2
∀[p:Top × Top × Top]. (snd(shorten-tuple(p;1)) ~ snd(snd(p)))
Lemma: append-tuple-simplify2
∀[p:Top × Top]. (fst(let x,y = p in <x, y, ⋅>) ~ fst(p))
Lemma: append-tuple-one-one
∀[L1,L2:Type List].
∀[x1,x2:tuple-type(L1)]. ∀[y1,y2:tuple-type(L2)].
{(x1 = x2 ∈ tuple-type(L1)) ∧ (y1 = y2 ∈ tuple-type(L2))}
supposing append-tuple(||L1||;||L2||;x1;y1) = append-tuple(||L1||;||L2||;x2;y2) ∈ tuple-type(L1 @ L2)
supposing 0 < ||L2||
Lemma: shorten-tuple-append-tuple
∀[L1,L2:Type List].
∀[x:tuple-type(L1)]. ∀[y:tuple-type(L2)].
(shorten-tuple(append-tuple(||L1||;||L2||;x;y);||L1||) = y ∈ tuple-type(L2))
supposing 0 < ||L2||
Lemma: select-update-tuple
∀[m,n:ℕ]. ∀[L:Type List].
(∀[x:tuple-type(L)]. ∀[y:Top]. (update-tuple(||L||;x;n;y).m ~ if (n =z m) then y else x.m fi )) supposing
(m < ||L|| and
n < ||L||)
Lemma: select-shorten-tuple
∀[n,m:ℕ]. ∀[L:Type List]. ∀[x:tuple-type(L)]. (shorten-tuple(x;n).m ~ x.n + m) supposing n + m < ||L||
Definition: ptuple
ptuple(lbl,p.a[lbl; p];X) ==
λparam.(labl:{lbl:Atom| 0 < ||a[lbl; param]||} × tuple-type(map(λx.case x
of inl(y) =>
case y of inl(p) => X p | inr(p) => (X p) List
| inr(E) =>
E;a[labl; param])))
Lemma: ptuple_wf
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[X:P ⟶ Type]. (ptuple(lbl,p.a[lbl;p];X) ∈ P ⟶ Type)
Lemma: tuple-type-continuous
∀[P:Type]. ∀[X:ℕ ⟶ P ⟶ Type]. ∀[L:P List]. ((⋂n:ℕ. tuple-type(map(X n;L))) ⊆r tuple-type(map(λp.⋂n:ℕ. (X n p);L)))
Lemma: tuple-type-monotone
∀[P:Type]. ∀[F,G:P ⟶ Type]. ∀[v:P List]. (tuple-type(map(F;v)) ⊆r tuple-type(map(G;v))) supposing F ⊆ G
Lemma: ptuple-continuous
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. type-family-continuous{i:l}(P;λX.ptuple(lbl,p.a[lbl;p];X))
Lemma: ptuple-monotone
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. family-monotone{i:l}(P;λX.ptuple(lbl,p.a[lbl;p];X))
Definition: pcorec
pcorec(lbl,p.a[lbl; p]) == corec-family(λX.ptuple(lbl,p.a[lbl; p];X))
Lemma: pcorec_wf
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. (pcorec(lbl,p.a[lbl;p]) ∈ P ⟶ Type)
Lemma: pcorec-ext
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)].
pcorec(lbl,p.a[lbl;p]) ≡ ptuple(lbl,p.a[lbl;p];pcorec(lbl,p.a[lbl;p]))
Lemma: fix_wf-pcorec-partial-nat
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[f:⋂X:P ⟶ Type
((i:P ⟶ (X i) ⟶ partial(ℕ))
⟶ i:P
⟶ (ptuple(lbl,p.a[lbl;p];X) i)
⟶ partial(ℕ))].
(fix(f) ∈ i:P ⟶ (pcorec(lbl,p.a[lbl;p]) i) ⟶ partial(ℕ))
Definition: add-sz
add-sz(sz;L;x) ==
tuple-sum(λc,u. case c of inl(z) => case z of inl(p) => sz p u | inr(p) => l_sum(map(sz p;u)) | inr(E) => 0;L;x)
Lemma: add-sz_wf
∀[P:Type]. ∀[X:P ⟶ Type]. ∀[sz:i:P ⟶ (X i) ⟶ partial(ℕ)]. ∀[L:(P + P + Type) List].
∀[x:tuple-type(map(λx.case x of inl(y) => case y of inl(p) => X p | inr(p) => (X p) List | inr(E) => E;L))].
(add-sz(sz;L;x) ∈ partial(ℕ))
Definition: pcorec-size
pcorec-size(lbl,p.a[lbl; p]) == fix((λsz,p,x. let lbl,z = x in 1 + add-sz(sz;a[lbl; p];z)))
Lemma: pcorec-size_wf
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)].
(pcorec-size(lbl,p.a[lbl;p]) ∈ i:P ⟶ (pcorec(lbl,p.a[lbl;p]) i) ⟶ partial(ℕ))
Lemma: unroll-pcorec-size
∀[a:Top]. (pcorec-size(lbl,p.a[lbl;p]) ~ λp,x. let lbl,z = x in 1 + add-sz(pcorec-size(lbl,p.a[lbl;p]);a[lbl;p];z))
Definition: prec
prec(lbl,p.a[lbl; p];i) == {x:pcorec(lbl,p.a[lbl; p]) i| (pcorec-size(lbl,p.a[lbl; p]) i x)↓}
Lemma: prec_wf
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[i:P]. (prec(lbl,p.a[lbl;p];i) ∈ Type)
Lemma: prec-ext
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[i:P].
prec(lbl,p.a[lbl;p];i) ≡ labl:{lbl:Atom| 0 < ||a[lbl;i]||} × tuple-type(map(λx.case x
of inl(y) =>
case y
of inl(p) =>
prec(lbl,p.a[lbl;p];p)
| inr(p) =>
prec(lbl,p.a[lbl;p];p) List
| inr(E) =>
E;a[labl;i]))
Definition: prec-size
||i;x|| == pcorec-size(lbl,p.a[lbl; p]) i x
Lemma: prec-size_wf
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[i:P]. ∀[x:prec(lbl,p.a[lbl;p];i)]. (||i;x|| ∈ ℕ)
Lemma: prec-size-induction
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[Q:i:P ⟶ prec(lbl,p.a[lbl;p];i) ⟶ TYPE].
((∀i:P. ∀x:prec(lbl,p.a[lbl;p];i). ((∀j:P. ∀z:{z:prec(lbl,p.a[lbl;p];j)| ||j;z|| < ||i;x||} . Q[j;z]) ⇒ Q[i;x]))
⇒ (∀i:P. ∀x:prec(lbl,p.a[lbl;p];i). Q[i;x]))
Lemma: prec-size-induction-ext
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[Q:i:P ⟶ prec(lbl,p.a[lbl;p];i) ⟶ TYPE].
((∀i:P. ∀x:prec(lbl,p.a[lbl;p];i). ((∀j:P. ∀z:{z:prec(lbl,p.a[lbl;p];j)| ||j;z|| < ||i;x||} . Q[j;z]) ⇒ Q[i;x]))
⇒ (∀i:P. ∀x:prec(lbl,p.a[lbl;p];i). Q[i;x]))
Lemma: unroll-prec-size
∀[a,i,x:Top]. (||i;x|| ~ let lbl,z = x in 1 + add-sz(pcorec-size(lbl,p.a[lbl;p]);a[lbl;i];z))
Lemma: prec-size-unfold
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[i:P]. ∀[x:prec(lbl,p.a[lbl;p];i)].
(||i;x||
= let lbl,z = x
in 1
+ tuple-sum(λc,x. case c
of inl(p) =>
case p of inl(j) => ||j;x|| | inr(j) => l_sum(map(λz.||j;z||;x))
| inr(_) =>
0;a[lbl;i];z)
∈ ℤ)
Definition: prec-arg-types
prec-arg-types(lbl,p.a[lbl; p];i;lbl) ==
map(λx.case x
of inl(y) =>
case y of inl(p) => prec(lbl,p.a[lbl; p];p) | inr(p) => prec(lbl,p.a[lbl; p];p) List
| inr(E) =>
E;a[lbl; i])
Lemma: prec-arg-types_wf
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[i:P]. ∀[lbl:Atom].
(prec-arg-types(lbl,p.a[lbl;p];i;lbl) ∈ Type List)
Definition: mk-prec
mk-prec(lbl;x) == <lbl, x>
Lemma: mk-prec_wf
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[i:P]. ∀[labl:{lbl:Atom| 0 < ||a[lbl;i]||} ].
∀[x:tuple-type(prec-arg-types(lbl,p.a[lbl;p];i;labl))].
(mk-prec(labl;x) ∈ prec(lbl,p.a[lbl;p];i))
Definition: dest-prec
dest-prec(x) == x
Lemma: dest-prec_wf
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[i:P]. ∀[x:prec(lbl,p.a[lbl;p];i)].
(dest-prec(x) ∈ lbl:{lbl:Atom| 0 < ||a[lbl;i]||} × tuple-type(prec-arg-types(lbl,p.a[lbl;p];i;lbl)))
Lemma: dest_mk_prec_lemma
∀x,lbl:Top. (dest-prec(mk-prec(lbl;x)) ~ <lbl, x>)
Definition: prec-label
prec-label(x) == fst(x)
Lemma: prec-label_wf
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[i:P]. ∀[x:prec(lbl,p.a[lbl;p];i)].
(prec-label(x) ∈ {lbl:Atom| 0 < ||a[lbl;i]||} )
Definition: prec-tuple
prec-tuple(x) == snd(x)
Lemma: prec-tuple_wf
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[i:P]. ∀[x:prec(lbl,p.a[lbl;p];i)].
(prec-tuple(x) ∈ tuple-type(prec-arg-types(lbl,p.a[lbl;p];i;prec-label(x))))
Lemma: prec-sq
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[i:P]. ∀[x:prec(lbl,p.a[lbl;p];i)].
(x ~ mk-prec(prec-label(x);prec-tuple(x)))
Definition: prec-sub
prec-sub(P;lbl,p.a[lbl; p];j;x;i;y) ==
let lbl,z = dest-prec(y)
in let L = a[lbl; i] in
let n = ||L|| in
∃k:ℕn
((↑isl(L[k]))
∧ (((outl(L[k]) = (inl j) ∈ (P + P)) ∧ (x = z.k ∈ prec(lbl,i.a[lbl; i];j)))
∨ ((outl(L[k]) = (inr j ) ∈ (P + P)) ∧ (x ∈ z.k))))
Lemma: prec-sub_wf
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[j:P]. ∀[x:prec(lbl,p.a[lbl;p];j)]. ∀[i:P].
∀[y:prec(lbl,p.a[lbl;p];i)].
(prec-sub(P;lbl,p.a[lbl;p];j;x;i;y) ∈ ℙ)
Lemma: prec-sub-size
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[j:P]. ∀[x:prec(lbl,p.a[lbl;p];j)]. ∀[i:P].
∀[y:prec(lbl,p.a[lbl;p];i)].
||j;x|| < ||i;y|| supposing prec-sub(P;lbl,p.a[lbl;p];j;x;i;y)
Definition: prec_sub
prec_sub(P;lbl,p.a[lbl; p]) == λu,v. let j,x = u in let i,y = v in prec-sub(P;lbl,p.a[lbl; p];j;x;i;y)
Lemma: prec_sub_wf
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)].
(prec_sub(P;lbl,p.a[lbl;p]) ∈ (i:P × prec(lbl,p.a[lbl;p];i)) ⟶ (i:P × prec(lbl,p.a[lbl;p];i)) ⟶ ℙ)
Definition: prec_sub+
prec_sub+(P;lbl,p.a[lbl; p]) == prec_sub(P;lbl,p.a[lbl; p])+
Lemma: prec_sub+_wf
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)].
(prec_sub+(P;lbl,p.a[lbl;p]) ∈ (i:P × prec(lbl,p.a[lbl;p];i)) ⟶ (i:P × prec(lbl,p.a[lbl;p];i)) ⟶ ℙ)
Lemma: prec-sub+-size
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[j:P]. ∀[x:prec(lbl,p.a[lbl;p];j)]. ∀[i:P].
∀[y:prec(lbl,p.a[lbl;p];i)].
||j;x|| < ||i;y|| supposing prec_sub+(P;lbl,p.a[lbl;p]) <j, x> <i, y>
Lemma: prec-induction
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[Q:i:P ⟶ prec(lbl,p.a[lbl;p];i) ⟶ TYPE].
((∀i:P. ∀x:prec(lbl,p.a[lbl;p];i). ((∀j:P. ∀z:{z:prec(lbl,p.a[lbl;p];j)| prec_sub+(P;lbl,p.a[lbl;p]) <j, z> <i, x>} .\000C Q[j;z]) ⇒ Q[i;x]))
⇒ (∀i:P. ∀x:prec(lbl,p.a[lbl;p];i). Q[i;x]))
Lemma: prec-induction-ext
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[Q:i:P ⟶ prec(lbl,p.a[lbl;p];i) ⟶ TYPE].
((∀i:P. ∀x:prec(lbl,p.a[lbl;p];i). ((∀j:P. ∀z:{z:prec(lbl,p.a[lbl;p];j)| prec_sub+(P;lbl,p.a[lbl;p]) <j, z> <i, x>} .\000C Q[j;z]) ⇒ Q[i;x]))
⇒ (∀i:P. ∀x:prec(lbl,p.a[lbl;p];i). Q[i;x]))
Lemma: prec-definition
∀[P:Type]. ∀[a:Atom ⟶ P ⟶ ((P + P + Type) List)]. ∀[A:P ⟶ Type]. ∀[R:i:P ⟶ prec(lbl,p.a[lbl;p];i) ⟶ A[i] ⟶ ℙ].
((∀i:P. ∀x:prec(lbl,p.a[lbl;p];i).
((∀j:P. ∀z:{z:prec(lbl,p.a[lbl;p];j)| prec_sub+(P;lbl,p.a[lbl;p]) <j, z> <i, x>} . (∃a:A[j] [R[j;z;a]])) ⇒ (∃a:A\000C[i] [R[i;x;a]])))
⇒ (∀i:P. ∀x:prec(lbl,p.a[lbl;p];i). (∃a:A[i] [R[i;x;a]])))
Definition: mrec_spec
MutualRectypeSpec == (Atom × ((Atom × ((Atom + Atom + Type) List)) List)) List
Lemma: mrec_spec_wf
MutualRectypeSpec ∈ 𝕌'
Definition: mrec-spec
mrec-spec(L;lbl;p) ==
case apply-alist(AtomDeq;L;p)
of inl(L2) =>
case apply-alist(AtomDeq;L2;lbl) of inl(as) => as | inr(_) => []
| inr(_) =>
[]
Lemma: mrec-spec_wf
∀[L:MutualRectypeSpec]. ∀[lbl,p:Atom]. (mrec-spec(L;lbl;p) ∈ (Atom + Atom + Type) List)
Definition: mrec
mrec(L;i) == prec(lbl,p.mrec-spec(L;lbl;p);i)
Lemma: mrec_wf
∀[L:MutualRectypeSpec]. ∀[i:Atom]. (mrec(L;i) ∈ Type)
Definition: mkinds
mKinds == {a:Atom| (a ∈ eager-map(λp.(fst(p));L))}
Lemma: mkinds_wf
∀[L:MutualRectypeSpec]. (mKinds ∈ Type)
Definition: mtype
mtype(L;i) == apply_alist(AtomDeq;eager-map(λp.let i,x = p in <i, mrec(L;i)>;L);i)
Lemma: mtype-sqequal
∀[L:MutualRectypeSpec]. ∀[i:mKinds]. (mtype(L;i) ~ mrec(L;i))
Lemma: mtype_wf
∀[L:MutualRectypeSpec]. ∀[i:mKinds]. (mtype(L;i) ∈ Type)
Lemma: mrec-label-cases
∀s:MutualRectypeSpec. ∀n:Atom. ∀lbl:{lbl:Atom| 0 < ||mrec-spec(s;lbl;n)||} .
((↑isl(apply-alist(AtomDeq;s;n))) ∧ (lbl ∈ map(λp.(fst(p));outl(apply-alist(AtomDeq;s;n)))))
Lemma: mrec-label-cases1
∀s:MutualRectypeSpec. ∀n:Atom. ∀lbl:{lbl:Atom| 0 < ||mrec-spec(s;lbl;n)||} .
(lbl ∈ eager-map(λp.(fst(p));outl(apply-alist(AtomDeq;s;n))))
Definition: mrec-member
mrec-member(s;n;lbl) ==
case rec-case(map(λp.(fst(p));outl(rec-case(s) of
[] => inr Ax
p::ps =>
r.if fst(p) =a n then inl (snd(p)) else r fi ))) of
[] => inr (λ_.Ax)
a::L =>
r.case r
of inl(z) =>
if lbl=a then inl <0, Ax, Ax> else inl let i,_,_ = z in <i + 1, Ax, Ax> fi
| inr(_) =>
if lbl=a then inl <0, Ax, Ax> else inr (λ_.Ax) fi
of inl(x) =>
x
| inr(_) =>
Ax
Lemma: mrec-label-cases1-ext
∀s:MutualRectypeSpec. ∀n:Atom. ∀lbl:{lbl:Atom| 0 < ||mrec-spec(s;lbl;n)||} .
(lbl ∈ eager-map(λp.(fst(p));outl(apply-alist(AtomDeq;s;n))))
Lemma: mrec-label-cases2
∀s:MutualRectypeSpec. ∀n:Atom. ∀lbl:{lbl:Atom| 0 < ||mrec-spec(s;lbl;n)||} . (n ∈ eager-map(λp.(fst(p));s))
Definition: mobj
mobj(L) == i:mKinds × mtype(L;i)
Lemma: mobj_wf
∀[L:MutualRectypeSpec]. (mobj(L) ∈ Type)
Definition: mobj-kind
mobj-kind(x) == fst(x)
Lemma: mobj-kind_wf
∀[s:MutualRectypeSpec]. ∀[x:mobj(s)]. (mobj-kind(x) ∈ mKinds)
Definition: mobj-data
mobj-data(x) == snd(x)
Lemma: mobj-data_wf
∀[s:MutualRectypeSpec]. ∀[x:mobj(s)]. (mobj-data(x) ∈ mtype(s;mobj-kind(x)))
Lemma: mobj-ext
∀[L:MutualRectypeSpec]. mobj(L) ≡ i:Atom × mrec(L;i)
Definition: mobj-label
mobj-label(x) == prec-label(mobj-data(x))
Lemma: mobj-label_wf
∀[S:MutualRectypeSpec]. ∀[x:mobj(S)]. (mobj-label(x) ∈ {lbl:Atom| 0 < ||mrec-spec(S;lbl;mobj-kind(x))||} )
Definition: mobj-tuple
mobj-tuple(x) == prec-tuple(mobj-data(x))
Lemma: mobj-tuple_wf
∀[S:MutualRectypeSpec]. ∀[x:mobj(S)].
(mobj-tuple(x) ∈ tuple-type(prec-arg-types(lbl,p.mrec-spec(S;lbl;p);mobj-kind(x);mobj-label(x))))
Lemma: mobj-sq
∀[S:MutualRectypeSpec]. ∀[x:mobj(S)]. (x ~ <mobj-kind(x), mk-prec(mobj-label(x);mobj-tuple(x))>)
Lemma: mobj-cases
∀[S:MutualRectypeSpec]. ∀[P:mobj(S) ⟶ TYPE].
((∀k:mKinds. ∀lbl:{lbl:Atom| 0 < ||mrec-spec(S;lbl;k)||} .
∀t:tuple-type(prec-arg-types(lbl,p.mrec-spec(S;lbl;p);k;lbl)).
P[<k, mk-prec(lbl;t)>])
⇒ (∀x:mobj(S). P[x]))
Definition: mrec-lt
x < y == prec_sub+(Atom;lbl,p.mrec-spec(L;lbl;p)) x y
Lemma: mrec-lt_wf
∀[L:MutualRectypeSpec]. ∀[x,y:mobj(L)]. (x < y ∈ ℙ)
Lemma: mrec-lt_transitivity
∀[L:MutualRectypeSpec]. ∀[x,y,z:mobj(L)]. (x < y ⇒ y < z ⇒ x < z)
Lemma: implies-mrec-lt
∀[L:MutualRectypeSpec]. ∀[x:mobj(L)]. ∀y:mobj(L). ((prec_sub(Atom;lbl,p.mrec-spec(L;lbl;p)) x y) ⇒ x < y)
Lemma: mrec-induction
∀[L:MutualRectypeSpec]. ∀[P:mobj(L) ⟶ TYPE].
((∀x:mobj(L). ((∀z:{z:mobj(L)| z < x} . P[z]) ⇒ P[x])) ⇒ (∀x:mobj(L). P[x]))
Definition: mrecind
mrecind(L;x.P[x]) ==
∀k:mKinds. ∀lbl:{lbl:Atom| 0 < ||mrec-spec(L;lbl;k)||} . ∀t:tuple-type(prec-arg-types(lbl,p.mrec-spec(L;lbl;p);k;lbl))\000C.
((∀j:ℕ||mrec-spec(L;lbl;k)||
case mrec-spec(L;lbl;k)[j] of inl(y) => case y of inl(p) => P[<p, t.j>] | inr(p) => (∀u∈t.j.P[<p, u>]) | inr(_) \000C=> True)
⇒ P[<k, mk-prec(lbl;t)>])
Lemma: mrecind_wf
∀[L:MutualRectypeSpec]. ∀[P:mobj(L) ⟶ ℙ]. (mrecind(L;x.P[x]) ∈ ℙ)
Lemma: istype-mrecind
∀[L:MutualRectypeSpec]. ∀[P:mobj(L) ⟶ TYPE]. istype(mrecind(L;x.P[x]))
Lemma: mrec-induction2
∀L:MutualRectypeSpec. ∀[P:mobj(L) ⟶ TYPE]. (mrecind(L;x.P[x]) ⇒ (∀x:mobj(L). P[x]))
Lemma: mrec-induction2-ext
∀L:MutualRectypeSpec. ∀[P:mobj(L) ⟶ TYPE]. (mrecind(L;x.P[x]) ⇒ (∀x:mobj(L). P[x]))
Definition: mrec_ind
mrec_ind(L;h;x) ==
let i,x1 = x
in letrec r(i)=λx.(h i (fst(x)) (snd(x))
let L' = case apply-alist(AtomDeq;L;i)
of inl(L2) =>
case apply-alist(AtomDeq;L2;fst(x)) of inl(as) => as | inr(_) => Ax
| inr(_) =>
Ax in
λj.case L'[j]
of inl(x@0) =>
case x@0 of inl(x1) => r x1 snd(x).j | inr(y) => λi@0.(r y snd(x).j[i@0])
| inr(y) =>
Ax) in
r(i)
x1
Lemma: mrec_ind_wf
∀L:MutualRectypeSpec. ∀[P:mobj(L) ⟶ TYPE]. ∀[h:mrecind(L;x.P[x])]. ∀[x:mobj(L)]. (mrec_ind(L;h;x) ∈ P[x])
Definition: mrec-ind
mrec-ind(h;o) == let lbl,tpl = o in letrec r(i)=λx.(h <i, x> (λo'.let j,z = o' in r j z)) in r(lbl) tpl
Lemma: mrec-ind_wf
∀[L:MutualRectypeSpec]. ∀[A:mobj(L) ⟶ TYPE]. ∀[h:x:mobj(L) ⟶ (z:{z:mobj(L)| z < x} ⟶ A[z]) ⟶ A[x]]. ∀[o:mobj(L)].
(mrec-ind(h;o) ∈ A[o])
Lemma: mk-prec_wf-mrec
∀[L:MutualRectypeSpec]. ∀[i,labl:Atom]. ∀[x:tuple-type(prec-arg-types(lbl,p.mrec-spec(L;lbl;p);i;labl))].
mk-prec(labl;x) ∈ mrec(L;i) supposing 0 < ||mrec-spec(L;labl;i)||
Definition: tuple-equiv
tuple-equiv(L) == λt,t'. let n = ||L|| in ∀i:ℕn. ((snd(L[i])) t.i t'.i)
Lemma: tuple-equiv_wf
∀[L:(X:Type × (X ⟶ X ⟶ ℙ)) List]
(tuple-equiv(L) ∈ tuple-type(map(λp.(fst(p));L)) ⟶ tuple-type(map(λp.(fst(p));L)) ⟶ ℙ)
Lemma: tuple-equiv-is-equiv
∀L:(X:Type × (X ⟶ X ⟶ ℙ)) List
((∀i:ℕ||L||. let X,E = L[i] in EquivRel(X;x,y.E x y))
⇒ EquivRel(tuple-type(map(λp.(fst(p));L));t,t'.tuple-equiv(L) t t'))
Home
Index