Definition: iterate_functor
iterate_functor(I;x,y.R[x; y];T.F[T];a)==r F[⋂b:{x:I| R[a; x]} . iterate_functor(I;x,y.R[x; y];T.F[T];b)]
Lemma: iterate_functor_wf
∀[I:Type]. ∀[R:I ⟶ I ⟶ ℙ].
∀[F:Type ⟶ Type]. ∀[i:I]. (iterate_functor(I;x,y.R[x;y];T.F[T];i) ∈ Type) supposing tcWO(I;x,y.R[x;y])
Definition: general_corec
general_corec(I;x,y.R[x; y];T.F[T]) == ⋂a:I. iterate_functor(I;x,y.R[x; y];T.F[T];a)
Lemma: general_corec_wf
∀[I:Type]. ∀[R:I ⟶ I ⟶ ℙ].
∀[F:Type ⟶ Type]. (general_corec(I;x,y.R[x;y];T.F[T]) ∈ Type) supposing tcWO(I;x,y.R[x;y])
Definition: corec
For any function F: Type -> Type, the iterates F^n(Top), n ∈ ℕ form a family
of types and ⋂n:ℕ. F^n(Top) is a type.
If F is monotone and continuous (preserves omega limits) then the intersection
is the greatest fixpoint for F (see corec-ext)⋅
corec(T.F[T]) == ⋂n:ℕ. primrec(n;Top;λ,T. F[T])
Lemma: corec_wf
∀[F:Type ⟶ Type]. (corec(T.F[T]) ∈ Type)
Lemma: corec-valueall-type
∀[F:Type ⟶ Type]
(valueall-type(corec(T.F[T]))) supposing ((∃n:ℕ. valueall-type(F^n Top)) and (∀A,B:Type. (A ≡ B ⇒ F[A] ≡ F[B])))
Lemma: corec-value-type
∀[F:Type ⟶ Type]
(value-type(corec(T.F[T]))) supposing ((∃n:ℕ. value-type(F^n Top)) and (∀A,B:Type. (A ≡ B ⇒ F[A] ≡ F[B])))
Lemma: corec-ext1
∀[F:Type ⟶ Type]. corec(T.F[T]) ≡ F[corec(T.F[T])] supposing Continuous+(T.F[T])
Lemma: corec-ext
∀[F:Type ⟶ Type]. corec(T.F[T]) ≡ F[corec(T.F[T])] supposing ContinuousMonotone(T.F[T])
Lemma: corec-greatest
∀[F:Type ⟶ Type]. ∀[X:Type]. X ⊆r corec(T.F[T]) supposing X ≡ F[X] supposing Monotone(T.F[T])
Definition: isect-family
⋂a:A. F[a] == λp.⋂a:A. (F[a] p)
Lemma: isect-family_wf
∀[P,A:Type]. ∀[F:A ⟶ P ⟶ Type]. (⋂a:A. F[a] ∈ P ⟶ Type)
Lemma: isect-family-wf2
∀[P:𝕌{j}]. ∀[A:Type]. ∀[F:A ⟶ P ⟶ Type]. (⋂a:A. F[a] ∈ P ⟶ Type)
Definition: sub-family
F ⊆ G == ∀p:P. ((F p) ⊆r (G p))
Lemma: sub-family_wf
∀[P:Type]. ∀[F,G:P ⟶ Type]. (F ⊆ G ∈ ℙ)
Lemma: sub-family_transitivity
∀[P:Type]. ∀[F,G,H:P ⟶ Type]. (F ⊆ H) supposing (F ⊆ G and G ⊆ H)
Lemma: sub-isect-family
∀[P:Type]. ∀[G:P ⟶ Type]. ∀[A:Type]. ∀[F:A ⟶ P ⟶ Type]. G ⊆ ⋂a:A. F[a] supposing ∀a:A. G ⊆ F[a]
Definition: ext-family
F ≡ G == ∀p:P. F p ≡ G p
Lemma: ext-family_wf
∀[P:Type]. ∀[F,G:P ⟶ Type]. (F ≡ G ∈ ℙ)
Lemma: ext-family-iff
∀[P:Type]. ∀[F,G:P ⟶ Type]. uiff(F ≡ G;F ⊆ G ∧ G ⊆ F)
Definition: family-monotone
family-monotone{i:l}(P;H) == ∀F,G:P ⟶ Type. (F ⊆ G ⇒ H F ⊆ H G)
Lemma: family-monotone_wf
∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type]. (family-monotone{i:l}(P;H) ∈ ℙ')
Definition: type-family-continuous
type-family-continuous{i:l}(P;H) == ∀[X:ℕ ⟶ P ⟶ Type]. ⋂n:ℕ. H (X n) ⊆ H ⋂n:ℕ. X n
Lemma: type-family-continuous_wf
∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type]. (type-family-continuous{i:l}(P;H) ∈ ℙ')
Definition: corec-family
A family of type parameterized by P is a member of
the type ⌜P ⟶ Type⌝.
The family of types ⌜λp.Top⌝ is the greatest such family
(under the pointwise subtype ordering).
If H maps ⌜P ⟶ Type⌝ to ⌜P ⟶ Type⌝, then the intersection (as a family)
of the iterates of H is the corecursive family defined by H.
If H satisfies the properties ⌜type-family-continuous{i:l}(P;H)⌝
and ⌜family-monotone{i:l}(P;H)⌝, then the ⌜corec-family(H)⌝ is an
extensional fixed point of H.
(See lemma corec-family-ext)⋅
corec-family(H) == ⋂n:ℕ. H^n (λp.Top)
Lemma: corec-family_wf
∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type]. (corec-family(H) ∈ P ⟶ Type)
Lemma: corec-family-wf2
∀[P:𝕌{j}]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type]. (corec-family(H) ∈ P ⟶ Type)
Lemma: corec-sub-family
∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type]. H corec-family(H) ⊆ corec-family(H) supposing family-monotone{i:l}(P;H)
Lemma: sub-corec-family
∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type].
corec-family(H) ⊆ H corec-family(H) supposing type-family-continuous{i:l}(P;H)
Lemma: corec-family-ext
∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type].
corec-family(H) ≡ H corec-family(H) supposing type-family-continuous{i:l}(P;H) ∧ family-monotone{i:l}(P;H)
Lemma: fix-corec-family-partial1
∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type]. ∀[A:Type].
(∀[F:(P ⟶ Type) ⟶ P ⟶ Type]. ∀[f:(i:P ⟶ (corec-family(H) i) ⟶ partial(A))
⟶ i:P
⟶ (corec-family(H) i)
⟶ partial(A)].
(fix(f) ∈ i:P ⟶ (corec-family(H) i) ⟶ partial(A))) supposing
(mono(A) and
value-type(A))
Lemma: fix_wf_corec-family-partial1
∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type]. ∀[A:Type].
(∀[f:⋂T:P ⟶ Type. ((i:P ⟶ (T i) ⟶ partial(A)) ⟶ i:P ⟶ (H[T] i) ⟶ partial(A))]
(fix(f) ∈ i:P ⟶ (corec-family(H) i) ⟶ partial(A))) supposing
((family-monotone{i:l}(P;H) ∧ type-family-continuous{i:l}(P;H)) and
mono(A) and
value-type(A))
Lemma: fix_wf_corec-family-partial-nat
∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type].
∀[f:⋂T:P ⟶ Type. ((i:P ⟶ (T i) ⟶ partial(ℕ)) ⟶ i:P ⟶ (H[T] i) ⟶ partial(ℕ))]
(fix(f) ∈ i:P ⟶ (corec-family(H) i) ⟶ partial(ℕ))
supposing family-monotone{i:l}(P;H) ∧ type-family-continuous{i:l}(P;H)
Definition: param-co-W
The co-recursive family of parameterized co-W types.
For a given parameter p, a member w of ⌜pco-W p⌝ will be
a pair ⌜<a, f>⌝ where ⌜a ∈ A[p]⌝ and f is a function with
domain ⌜B[p; a]⌝. For b in the domain of f, ⌜f b⌝ is a member
of the co-W type in family that has parameter ⌜C[p;
a;
b]⌝.⋅
pco-W ==
corec-family(λW,p. (a:A[p] × (b:B[p; a] ⟶ (W
C[p;
a;
b]))))
Lemma: param-co-W_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. (pco-W ∈ P ⟶ Type)
Lemma: param-co-W-ext
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].
pco-W ≡ λp.(a:A[p] × (b:B[p;a] ⟶ (pco-W C[p;a;b])))
Definition: pcw-step
A step in a path through a parameterized-co-W type
is a triple ⌜<p, w, d>⌝ where ⌜p ∈ P⌝ is the current parameter,
⌜w ∈ pco-W p⌝ is the current "co-tree" (i.e. non-well-founded tree)
and d is a "decision",
When d is ⌜inl b⌝ where b is a member of the domain
of ⌜snd(w)⌝ (i.e. a member of ⌜B[p; fst(w)]⌝)
then the path will continue with a next step.
When d is ⌜inr ⋅ ⌝ then the path ends at this step.⋅
pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p;
a;
b]) ==
p:P × w:pco-W p × (B[p; fst(w)]?)
Lemma: pcw-step_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].
(pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]) ∈ Type)
Definition: pcw-final-step
pcw-final-step(s) == let p,w,d = s in ↑isr(d)
Lemma: pcw-final-step_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].
∀[s:pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])].
(pcw-final-step(s) ∈ ℙ)
Definition: pcw-step-agree
The first and second parts of the triple s (the parameter p and tree w')
agree with the given parameter p1 and tree w.⋅
StepAgree(s;p1;w) == let p,w',b = s in (p = p1 ∈ P) ∧ (w' = w ∈ (pco-W p1))
Lemma: pcw-step-agree_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].
∀[s:pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])]. ∀[p1:P]. ∀[w:pco-W p1].
(StepAgree(s;p1;w) ∈ ℙ)
Definition: pcw-steprel
If the "decision" d in step s1 = ⌜<p, w, d>⌝ is ⌜inl b⌝
then the next step s2 = ⌜<p', w', d'>⌝ must
have p' = ⌜C[p;
a;
b]⌝ and w' = ⌜f b⌝ (where w = ⌜<a, f>⌝).
If the path "ended" at step s1, then later steps are irrelevant
so there is no restriction.⋅
StepRel(s1;s2) ==
let p,w,d = s1 in
let a,f = w
in case d
of inl(b) =>
StepAgree(s2;C[p;
a;
b];f b)
| inr(x) =>
True
Lemma: pcw-steprel_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].
∀[s1,s2:pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])].
(StepRel(s1;s2) ∈ ℙ)
Definition: pcw-consistent-steps
pcw-consistent-steps(P;p.A[p];p,a.B[p; a];p,a,b.C[p;
a;
b];s1;s2) ==
let p,w,d = s1 in
let p',w',d' = s2 in
(p = p' ∈ P) ∧ (w = w' ∈ (pco-W p)) ∧ ((↑isl(d)) ⇒ (d = d' ∈ (B[p; fst(w)]?)))
Lemma: pcw-consistent-steps_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].
∀[s1,s2:pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])].
(pcw-consistent-steps(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];s1;s2) ∈ ℙ)
Definition: pcw-path
A full path through a co-W type is an infinite sequence of steps
such that each successive step agrees with the previous step.⋅
Path ==
{path:ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p;
a;
b])|
∀i:ℕ. StepRel(path i;path (i + 1))}
Lemma: pcw-path_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. (Path ∈ Type)
Definition: pcw-consistent-paths
pcw-consistent-paths(P;p.A[p];p,a.B[p; a];p,a,b.C[p;
a;
b];f;g) ==
∀n:ℕ
((¬pcw-final-step(f n))
⇒ ((f n)
= (g n)
∈ pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p;
a;
b])))
Lemma: pcw-consistent-paths_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[f,g:Path].
(pcw-consistent-paths(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];f;g) ∈ ℙ)
Definition: pcw-path-rel
pcw-path-rel(P;p.A[p];p,a.B[p; a];p,a,b.C[p;
a;
b];f;g) ==
pcw-consistent-paths(P;p.A[p];p,a.B[p; a];p,a,b.C[p;
a;
b];f;g)
∧ (∃n:ℕ. ((∀i:ℕn. (¬pcw-final-step(f i))) ∧ pcw-final-step(f n) ∧ (¬pcw-final-step(g n))))
Lemma: pcw-path-rel_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[f,g:Path].
(pcw-path-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];f;g) ∈ ℙ)
Lemma: pcw-path-shift
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].
∀path:Path. (λx.(path (x + 1)) ∈ Path)
Definition: pcw-pp
PartialPath ==
{nss:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p;
a;
b]))|
let n,ss = nss
in ∀i:ℕn - 1. StepRel(ss i;ss (i + 1))}
Lemma: pcw-pp_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. (PartialPath ∈ Type)
Definition: pcw-partial
pcw-partial(path;n) == <n, path>
Lemma: pcw-partial_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[path:Path]. ∀[n:ℕ].
(pcw-partial(path;n) ∈ PartialPath)
Definition: pcw-pp-null
pcw-pp-null(pp) == let n,ss = pp in n ≤z 0
Lemma: pcw-pp-null_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[pp:PartialPath].
(pcw-pp-null(pp) ∈ 𝔹)
Definition: pcw-pp-head
pcw-pp-head(pp) == let n,ss = pp in ss 0
Lemma: pcw-pp-head_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[pp:PartialPath].
pcw-pp-head(pp) ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]) supposing ¬↑pcw-pp-null(pp)
Definition: pcw-pp-tail
pcw-pp-tail(pp) == let n,ss = pp in <n - 1, λx.(ss (x + 1))>
Lemma: pcw-pp-tail_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[pp:PartialPath].
pcw-pp-tail(pp) ∈ PartialPath supposing ¬↑pcw-pp-null(pp)
Definition: pcw-pp-barred
A partial path ⌜<n, ss>⌝ is barred if it is non-empty and the last step
has "decision" d = inr ⋅ .
This means that the path does not continue with a decision d = inl b
that picks a member of the domain of ⌜snd(w)⌝.⋅
Barred(pp) == let n,ss = pp in 0 < n ∧ let p,w,d = ss (n - 1) in ↑isr(d)
Lemma: pcw-pp-barred_wf0
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].
∀[pp:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))].
(Barred(pp) ∈ ℙ)
Lemma: pcw-pp-barred_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[pp:PartialPath].
(Barred(pp) ∈ ℙ)
Lemma: decidable__pcw-pp-barred
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].
∀pp:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])). Dec(Barred(pp))
Definition: param-W
For each parameter ⌜par ∈ P⌝, the corresponding type
in the parameterized family of W-types is the subtype of the
corresponding parameterized co-inductive family of co-W types
containing those trees, w, such that every path starting at w
is barred. ⋅
pW == λpar.{w:pco-W par| ∀path:Path. (StepAgree(path 0;par;w) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))}
Lemma: param-W_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. (pW ∈ P ⟶ Type)
Definition: pW-sup
pW-sup(a;f) == <a, f>
Lemma: pW-sup_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[par:P]. ∀[a:A[par]].
∀[f:b:B[par;a] ⟶ (pW C[par;a;b])].
(pW-sup(a;f) ∈ pW par)
Lemma: param-W-ext
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].
pW ≡ λp.(a:A[p] × (b:B[p;a] ⟶ (pW C[p;a;b])))
Lemma: equal-implies-member-param-W
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[p:P]. ∀[w:pW p].
∀[w':pco-W p].
w' ∈ pW p supposing w = w' ∈ (pco-W p)
Definition: param-W-rel
param-W-rel(P;p.A[p];p,a.B[p; a];p,a,b.C[p;
a;
b];par;w) ==
λn,ss,s. if (0) < (n) then (↑isl(snd(snd((ss (n - 1)))))) ∧ StepRel(ss (n - 1);s) else StepAgree(s;par;w)
Lemma: param-W-rel_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[par:P]. ∀[w:pW par].
(param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) ∈ n:ℕ
⟶ (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))
⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
⟶ ℙ)
Lemma: pcw-pp-lemma
∀P:Type. ∀A:P ⟶ Type. ∀B:p:P ⟶ A[p] ⟶ Type. ∀C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P. ∀par:P. ∀w:pW par. ∀n:ℕ. ∀m:ℕn.
∀ss:ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]).
((∀x:ℕn. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) x ss (ss x)))
⇒ (fst(snd((ss m))) ∈ pW (fst((ss m)))))
Definition: pW-rec
let ind(p,a,f,G) = ind[p;
a;
f;
G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;
a;
b],f(b)) in
F(par;w)
==r let a,f = w
in ind[par;
a;
f;
λb.let ind(p,a,f,G) = ind[p;
a;
f;
G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;
a;
b],f(b)) in
F(C[par;
a;
b];f b)]
Lemma: pW-rec_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[Q:par:P ⟶ (pW par) ⟶ ℙ].
∀[ind:par:P
⟶ a:A[par]
⟶ f:(b:B[par;a] ⟶ (pW C[par;a;b]))
⟶ (b:B[par;a] ⟶ Q[C[par;a;b];f b])
⟶ Q[par;pW-sup(a;f)]]. ∀[par:P]. ∀[w:pW par].
(let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;a;b],f(b)) in
F(par;w) ∈ Q[par;w])
Lemma: param-W-induction
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type].
∀C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
∀[Q:par:P ⟶ (pW par) ⟶ ℙ]
((∀par:P. ∀a:A[par]. ∀f:b:B[par;a] ⟶ (pW C[par;a;b]). ((∀b:B[par;a]. Q[C[par;a;b];f b]) ⇒ Q[par;pW-sup(a;f)]))
⇒ (∀par:P. ∀w:pW par. Q[par;w]))
Definition: pw-evenodd
pw-evenodd() == pW
Lemma: pw-evenodd_wf
pw-evenodd() ∈ 𝔹 ⟶ Type
Lemma: evodd-induction
∀[Q:b:𝔹 ⟶ (pw-evenodd() b) ⟶ ℙ]
((∀b:𝔹. ∀a:b = tt?. ∀f:case a of inl(x) => Void | inr(x) => Unit ⟶ (pw-evenodd() (¬bb)).
((∀x:case a of inl(x) => Void | inr(x) => Unit. Q[¬bb;f x]) ⇒ Q[b;pW-sup(a;f)]))
⇒ (∀b:𝔹. ∀n:pw-evenodd() b. Q[b;n]))
Definition: evodd-zero
evodd-zero() == pW-sup(inl Ax;λx.x)
Lemma: evodd-zero_wf
evodd-zero() ∈ pw-evenodd() tt
Definition: evodd-succ
evodd-succ(n) == pW-sup(inr Ax ;λx.n)
Lemma: evodd-succ_wf
∀[b:𝔹]. ∀[n:pw-evenodd() (¬bb)]. (evodd-succ(n) ∈ pw-evenodd() b)
Lemma: evodd-induction2
∀[Q:b:𝔹 ⟶ (pw-evenodd() b) ⟶ ℙ]
(Q[tt;evodd-zero()]
⇒ (∀b:𝔹. ∀x:pw-evenodd() b. (Q[b;x] ⇒ Q[¬bb;evodd-succ(x)]))
⇒ (∀b:𝔹. ∀n:pw-evenodd() b. Q[b;n]))
Lemma: evodd-induction2-ext
∀[Q:b:𝔹 ⟶ (pw-evenodd() b) ⟶ ℙ]
(Q[tt;evodd-zero()]
⇒ (∀b:𝔹. ∀x:pw-evenodd() b. (Q[b;x] ⇒ Q[¬bb;evodd-succ(x)]))
⇒ (∀b:𝔹. ∀n:pw-evenodd() b. Q[b;n]))
Definition: evodd-enum
evodd-enum(n) == primrec(n;<tt, evodd-zero()>;λi,x. let b,z = x in <¬bb, evodd-succ(z)>)
Lemma: evodd-enum_wf
∀[n:ℕ]. (evodd-enum(n) ∈ b:𝔹 × (pw-evenodd() b))
Lemma: evodd-enum-surjection
Surj(ℕ;b:𝔹 × (pw-evenodd() b);λn.evodd-enum(n))
Definition: cw-step
cw-step(A;a.B[a]) == pcw-step(Unit;p.A;p,a.B[a];p,a,b.⋅)
Lemma: cw-step_wf
∀[A:Type]. ∀[B:A ⟶ Type]. (cw-step(A;a.B[a]) ∈ Type)
Definition: W
A parameterized family of W types with the parameter type Unit
must have the "C" function ⌜λp,a,b. ⋅⌝.
Then applying this family to the paramter ⌜⋅⌝, we get the W-type
as an instance of the more general parameterized family of types.⋅
W(A;a.B[a]) == pW ⋅
Lemma: W_wf
∀[A:Type]. ∀[B:A ⟶ Type]. (W(A;a.B[a]) ∈ Type)
Definition: W-rel
W-rel(A;a.B[a];w) == param-W-rel(Unit;p.A;p,a.B[a];p,a,b.⋅;⋅;w)
Lemma: W-rel_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[w:W(A;a.B[a])].
(W-rel(A;a.B[a];w) ∈ n:ℕ ⟶ (ℕn ⟶ cw-step(A;a.B[a])) ⟶ cw-step(A;a.B[a]) ⟶ ℙ)
Lemma: cw-pp-lemma
∀A:Type. ∀B:A ⟶ Type. ∀w:W(A;a.B[a]). ∀n:ℕ. ∀m:ℕn. ∀ss:ℕn ⟶ cw-step(A;a.B[a]).
((∀x:ℕn. (W-rel(A;a.B[a];w) x ss (ss x))) ⇒ (fst(snd((ss m))) ∈ W(A;a.B[a])))
Lemma: pcw-pp-barred-W
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[pp:n:ℕ × (ℕn ⟶ cw-step(A;a.B[a]))]. (Barred(pp) ∈ ℙ)
Lemma: pcw-pp-barred-W-decidable
∀[A:Type]. ∀[B:A ⟶ Type]. ∀n:ℕ. ∀s:ℕn ⟶ cw-step(A;a.B[a]). (Barred(<n, s>) ∨ (¬Barred(<n, s>)))
Lemma: W-path-lemma
∀A:Type. ∀B:A ⟶ Type. ∀x:W(A;a.B[a]). ∀alpha:ℕ ⟶ cw-step(A;a.B[a]).
((∀n:ℕ. (W-rel(A;a.B[a];x) n alpha (alpha n))) ⇒ (alpha ∈ Path))
Lemma: W-ext
∀[A:Type]. ∀[B:A ⟶ Type]. W(A;a.B[a]) ≡ a:A × (B[a] ⟶ W(A;a.B[a]))
Lemma: W-path-lemma2
∀A1:Type. ∀B1:A1 ⟶ Type. ∀a:A1. ∀x1:B1[a] ⟶ W(A1;a.B1[a]). ∀n:ℕ+. ∀s:ℕn ⟶ cw-step(A1;a.B1[a]). ∀a1:A1.
∀w1:b:B1[a1] ⟶ (pco-W ⋅). ∀x:B1[a1]. ∀a2:A1. ∀z1:b:B1[a2] ⟶ (pco-W ⋅).
((∀k:ℕn. (W-rel(A1;a.B1[a];<a, x1>) k s (s k)))
⇒ ((s (n - 1)) = <⋅, <a1, w1>, inl x> ∈ cw-step(A1;a.B1[a]))
⇒ ((w1 x) = <a2, z1> ∈ (pco-W ⋅))
⇒ (z1 ∈ b:B1[a2] ⟶ W(A1;a.B1[a])))
Lemma: W-elimination-facts
∀A:Type. ∀B:A ⟶ Type. ∀w:W(A;a.B[a]).
((cw-step(A;a.B[a]) ∈ Type)
∧ (W-rel(A;a.B[a];w) ∈ n:ℕ ⟶ (ℕn ⟶ cw-step(A;a.B[a])) ⟶ cw-step(A;a.B[a]) ⟶ ℙ)
∧ (W(A;a.B[a]) ∈ Type)
∧ (W(A;a.B[a]) ⊆r (pco-W ⋅))
∧ (∀n:ℕ. ∀s:ℕn ⟶ cw-step(A;a.B[a]). (Barred(<n, s>) ∨ (¬Barred(<n, s>))))
∧ (∀alpha:ℕ ⟶ cw-step(A;a.B[a]). ((∀n:ℕ. (W-rel(A;a.B[a];w) n alpha (alpha n))) ⇒ (alpha ∈ Path)))
∧ (∀[pp:n:ℕ × (ℕn ⟶ cw-step(A;a.B[a]))]. (Barred(pp) ∈ ℙ))
∧ (∀alpha:ℕ ⟶ cw-step(A;a.B[a]). ((∀n:ℕ. (W-rel(A;a.B[a];w) n alpha (alpha n))) ⇒ (↓∃n:ℕ. Barred(<n, alpha>))))
∧ (∀a:A. ∀x1:B[a] ⟶ W(A;a.B[a]). ∀n:ℕ+. ∀s:ℕn ⟶ cw-step(A;a.B[a]). ∀a1:A. ∀w1:b:B[a1] ⟶ (pco-W ⋅). ∀x:B[a1]. ∀a2:A.
∀z1:b:B[a2] ⟶ (pco-W ⋅).
((∀k:ℕn. (W-rel(A;a.B[a];<a, x1>) k s (s k)))
⇒ ((s (n - 1)) = <⋅, <a1, w1>, inl x> ∈ cw-step(A;a.B[a]))
⇒ ((w1 x) = <a2, z1> ∈ (pco-W ⋅))
⇒ (z1 ∈ B[a2] ⟶ W(A;a.B[a])))))
Definition: Wsup
Wsup(a;b) == <a, b>
Lemma: Wsup_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[a:A]. ∀[b:B[a] ⟶ W(A;a.B[a])]. (Wsup(a;b) ∈ W(A;a.B[a]))
Lemma: W-induction1
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[Q:W(A;a.B[a]) ⟶ ℙ].
((∀a:A. ∀f:B[a] ⟶ W(A;a.B[a]). ((∀b:B[a]. Q[f b]) ⇒ Q[Wsup(a;f)])) ⇒ (∀w:W(A;a.B[a]). Q[w]))
Lemma: W-induction1-extract
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[Q:W(A;a.B[a]) ⟶ ℙ].
((∀a:A. ∀f:B[a] ⟶ W(A;a.B[a]). ((∀b:B[a]. Q[f b]) ⇒ Q[Wsup(a;f)])) ⇒ (∀w:W(A;a.B[a]). Q[w]))
Definition: W_ind
W_ind(F;w) == letrec H(par)=λw.let a,f = w in F a f (λb.(H Ax (f b))) in H(Ax) w
Lemma: W_ind_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[Q:W(A;a.B[a]) ⟶ ℙ].
∀[F:∀a:A. ∀f:B[a] ⟶ W(A;a.B[a]). ((∀b:B[a]. Q[f b]) ⇒ Q[Wsup(a;f)])]. ∀[w:W(A;a.B[a])].
(W_ind(F;w) ∈ Q[w])
Lemma: W-induction
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[Q:W(A;a.B[a]) ⟶ ℙ].
((∀a:A. ∀f:B[a] ⟶ W(A;a.B[a]). ((∀b:B[a]. Q[f b]) ⇒ Q[Wsup(a;f)])) ⇒ (∀w:W(A;a.B[a]). Q[w]))
Definition: W-rec
W-rec(a,f,r.F[a;
f;
r];w)
==r let a,f = w
in F[a;
f;
λb.W-rec(a,f,r.F[a;
f;
r];f b)]
Lemma: W-rec_wf
∀[T,A:Type]. ∀[B:A ⟶ Type]. ∀[F:a:A ⟶ (B[a] ⟶ W(A;a.B[a])) ⟶ (B[a] ⟶ T) ⟶ T]. ∀[w:W(A;a.B[a])].
(W-rec(a,f,r.F[a;f;r];w) ∈ T)
Lemma: W_subtype
∀[A1,A2:Type]. ∀[B1:A1 ⟶ Type]. ∀[B2:A2 ⟶ Type].
(W(A1;a.B1[a]) ⊆r W(A2;a.B2[a])) supposing ((∀a:A1. (B2[a] ⊆r B1[a])) and (A1 ⊆r A2))
Definition: Wcmp
Wcmp(A;a.B[a];leq) ==
fix((λWcmp,leq,w1,w2. if leq
then let a,f = w1
in ∀x:B[a]. ((f x) (Wcmp ff) w2)
else let a,f = w2
in ∃x:B[a]. (w1 (Wcmp tt) (f x))
fi ))
leq
Lemma: Wcmp_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[leq:𝔹]. (Wcmp(A;a.B[a];leq) ∈ W(A;a.B[a]) ⟶ W(A;a.B[a]) ⟶ ℙ)
Lemma: Wleq_weakening
∀[A:Type]. ∀[B:A ⟶ Type]. ∀w1,w2:W(A;a.B[a]). ((w1 < w2) ⇒ (w1 ≤ w2))
Lemma: Wleq_weakening2
∀[A:Type]. ∀[B:A ⟶ Type]. ∀w1,w2:W(A;a.B[a]). w1 ≤ w2 supposing w1 = w2 ∈ W(A;a.B[a])
Lemma: Wcmp_transitivity
∀[A:Type]. ∀[B:A ⟶ Type].
∀w1,w2,w3:W(A;a.B[a]).
((((w1 < w2) ⇒ (w2 ≤ w3) ⇒ (w1 < w3)) ∧ ((w1 ≤ w2) ⇒ (w2 < w3) ⇒ (w1 < w3)))
∧ ((w1 ≤ w2) ⇒ (w2 ≤ w3) ⇒ (w1 ≤ w3)))
Lemma: Wless_antireflexive
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[w1:W(A;a.B[a])]. (¬(w1 < w1))
Lemma: W-uwellfounded_witness
λF.fix(F) ∈ ∀[A:Type]. ∀[B:A ⟶ Type]. uWellFnd(W(A;a.B[a]);w1,w2.w1 < w2)
Lemma: W-uwellfounded
∀[A:Type]. ∀[B:A ⟶ Type]. uWellFnd(W(A;a.B[a]);w1,w2.w1 < w2)
Lemma: W-measure-induction
∀[T,A:Type]. ∀[B:A ⟶ Type]. ∀[measure:T ⟶ W(A;a.B[a])]. ∀[P:T ⟶ ℙ].
((∀i:T. ((∀j:{j:T| measure[j] < measure[i]} . P[j]) ⇒ P[i])) ⇒ (∀i:T. P[i]))
Lemma: W-uniform-measure-induction
∀[T,A:Type]. ∀[B:A ⟶ Type]. ∀[measure:T ⟶ W(A;a.B[a])]. ∀[P:T ⟶ ℙ].
((∀[i:T]. ((∀[j:{j:T| measure[j] < measure[i]} ]. P[j]) ⇒ P[i])) ⇒ (∀[i:T]. P[i]))
Definition: W_iterate_functor
W_iterate_functor(A;a.B[a];T.F[T];w)==r F[⋂x:{b:W(A;a.B[a])| b < w} . W_iterate_functor(A;a.B[a];T.F[T];x)]
Lemma: W_iterate_functor_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[F:Type ⟶ Type]. ∀[w:W(A;a.B[a])]. (W_iterate_functor(A;a.B[a];T.F[T];w) ∈ Type)
Definition: W_corec
This is a generalization of ⌜corec(T.F[T])⌝ where instead of iterating
only over the natural numbers, we iterate over all the "ordinals" in
the type ⌜W(A;a.B[a])⌝.⋅
W_corec(A;a.B[a];T.F[T]) == ⋂w:W(A;a.B[a]). W_iterate_functor(A;a.B[a];T.F[T];w)
Lemma: W_corec_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[F:Type ⟶ Type]. (W_corec(A;a.B[a];T.F[T]) ∈ Type)
Definition: Wzero
isZero(w) == ¬B[fst(w)]
Lemma: Wzero_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[w:W(A;a.B[a])]. (isZero(w) ∈ ℙ)
Lemma: Wzero-leq
∀[A:Type]. ∀[B:A ⟶ Type]. ∀w:W(A;a.B[a]). (isZero(w) ⇐⇒ ∀w2:W(A;a.B[a]). (w ≤ w2))
Definition: Wsucc
Wsucc(A;a.B[a];w) == B[fst(w)] ≡ Unit
Lemma: Wsucc_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[w:W(A;a.B[a])]. (Wsucc(A;a.B[a];w) ∈ ℙ)
Definition: Wadd
(w1 + w2) == fix((λWadd,w2. let a,f = w2 in if zero a then w1 else Wsup(a;λx.(Wadd (f x))) fi )) w2
Lemma: Wadd_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero:A ⟶ 𝔹]. ∀[w2,w1:W(A;a.B[a])]. ((w1 + w2) ∈ W(A;a.B[a]))
Lemma: Wadd-assoc
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero:A ⟶ 𝔹]. ∀[w3,w2,w1:W(A;a.B[a])]. ((w1 + (w2 + w3)) = ((w1 + w2) + w3) ∈ W(A;a.B[a]))
Lemma: Wleq-Wadd
∀[A:Type]. ∀[B:A ⟶ Type]. ∀zero:A ⟶ 𝔹. ∀w3,w2,w1:W(A;a.B[a]). ((w1 ≤ w2) ⇒ ((w1 + w3) ≤ (w2 + w3)))
Lemma: Wleq-Wadd3
∀[A:Type]. ∀[B:A ⟶ Type]. ∀zero:A ⟶ 𝔹. ((∀a:A. (¬↑(zero a) ⇐⇒ B[a])) ⇒ (∀w1,w2:W(A;a.B[a]). (w1 ≤ (w1 + w2))))
Lemma: Wleq-Wadd2
∀[A:Type]. ∀[B:A ⟶ Type].
∀zero:A ⟶ 𝔹. ((∀a:A. (¬↑(zero a) ⇐⇒ B[a])) ⇒ (∀w3,w2,w1:W(A;a.B[a]). ((w2 ≤ w3) ⇒ ((w1 + w2) ≤ (w1 + w3)))))
Lemma: Wless-Wadd
∀[A:Type]. ∀[B:A ⟶ Type].
∀zero:A ⟶ 𝔹. ((∀a:A. (¬↑(zero a) ⇐⇒ B[a])) ⇒ (∀w3,w2,w1:W(A;a.B[a]). ((w2 < w3) ⇒ ((w1 + w2) < (w1 + w3)))))
Lemma: Wzero-unique
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero:A ⟶ 𝔹].
∀[z1,z2:W(A;a.B[a])]. z1 = z2 ∈ W(A;a.B[a]) supposing isZero(z1) ∧ isZero(z2)
supposing (∀a1,a2:A. ((↑(zero a1)) ⇒ (↑(zero a2)) ⇒ (a1 = a2 ∈ A))) ∧ (∀a:A. ((¬B[a]) ⇒ (↑(zero a))))
Lemma: Wadd-Wzero
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero:A ⟶ 𝔹].
∀[z:W(A;a.B[a])]
∀[w1:W(A;a.B[a])]. (((w1 + z) = w1 ∈ W(A;a.B[a])) ∧ ((z + w1) = w1 ∈ W(A;a.B[a]))) supposing isZero(z)
supposing (∀a:A. (↑(zero a) ⇐⇒ ¬B[a])) ∧ (∀a1,a2:A. ((↑(zero a1)) ⇒ (↑(zero a2)) ⇒ (a1 = a2 ∈ A)))
Definition: Wmul
(w1 * w2) == fix((λWmul,w2. let a,f = w2 in if succ a then (Wmul (f ⋅) + w1) else Wsup(a;λx.(Wmul (f x))) fi )) w2
Lemma: Wmul_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero,succ:A ⟶ 𝔹]. ∀[w2,w1:W(A;a.B[a])].
(w1 * w2) ∈ W(A;a.B[a]) supposing ∀a:A. ((↑(succ a)) ⇒ (Unit ⊆r B[a]))
Lemma: Wmul-Wadd
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero,succ:A ⟶ 𝔹].
∀[w3,w2,w1:W(A;a.B[a])]. ((w1 * (w2 + w3)) = ((w1 * w2) + (w1 * w3)) ∈ W(A;a.B[a]))
supposing ∀a:A. (((↑(succ a)) ⇒ (Unit ⊆r B[a])) ∧ ((↑(zero a)) ⇒ (¬B[a])))
Lemma: Wmul-assoc
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero,succ:A ⟶ 𝔹]. ∀[w3,w2,w1:W(A;a.B[a])].
(w1 * (w2 * w3)) = ((w1 * w2) * w3) ∈ W(A;a.B[a])
supposing ∀a:A. (((↑(succ a)) ⇒ (Unit ⊆r B[a])) ∧ ((↑(zero a)) ⇒ (¬B[a])))
Lemma: Wmul-Wzero
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero,succ:A ⟶ 𝔹].
∀[z:W(A;a.B[a])]. ∀[w1:W(A;a.B[a])]. ((w1 * z) = z ∈ W(A;a.B[a])) supposing isZero(z)
supposing ∀a:A. ((↑(succ a)) ⇒ (Unit ⊆r B[a]))
Lemma: Wleq-Wmul
∀[A:Type]. ∀[B:A ⟶ Type].
∀zero,succ:A ⟶ 𝔹.
((∀a:A. ((↑(succ a)) ⇒ (Unit ⊆r B[a])))
⇒ (∀a:A. (¬↑(zero a) ⇐⇒ B[a]))
⇒ (∀w3,w2,w1:W(A;a.B[a]). ((w1 ≤ w2) ⇒ ((w1 * w3) ≤ (w2 * w3)))))
Lemma: Wmul-add-properties
∀[A:Type]. ∀[B:A ⟶ Type].
∀zero,succ:A ⟶ 𝔹.
((∀a:A. ((↑(succ a)) ⇒ B[a] ≡ Unit))
⇒ (∀a:A. (¬↑(zero a) ⇐⇒ B[a]))
⇒ (∀a1,a2:A. ((↑(zero a1)) ⇒ (↑(zero a2)) ⇒ (a1 = a2 ∈ A)))
⇒ (∀x,y,z:W(A;a.B[a]).
(((x + (y + z)) = ((x + y) + z) ∈ W(A;a.B[a]))
∧ ((x * (y + z)) = ((x * y) + (x * z)) ∈ W(A;a.B[a]))
∧ ((x * (y * z)) = ((x * y) * z) ∈ W(A;a.B[a]))
∧ (isZero(z) ⇒ isZero(y) ⇒ (z = y ∈ W(A;a.B[a])))
∧ (isZero(z)
⇒ ((((x + z) = x ∈ W(A;a.B[a])) ∧ ((z + x) = x ∈ W(A;a.B[a]))) ∧ ((x * z) = z ∈ W(A;a.B[a])) ∧ (z ≤ x)))
∧ ((x ≤ y) ⇒ (((x + z) ≤ (y + z)) ∧ ((z + x) ≤ (z + y))))
∧ ((x < y) ⇒ ((z + x) < (z + y)))
∧ ((x ≤ y) ⇒ ((x * z) ≤ (y * z))))))
Lemma: sig-to-W
∀[A:Type]. ∀[B:A ⟶ Type]. ((a:A × (¬B[a])) ⇒ W(A;a.B[a]))
Lemma: W-to-not-not-sig
∀[A:Type]. ∀[B:A ⟶ Type]. (W(A;a.B[a]) ⇒ (¬¬(a:A × (¬B[a]))))
Lemma: W-to-not-not-sig2
∀A:Type. ∀B:A ⟶ Type. (W(A;a.B[a]) ⇒ (∀R:Type. (((a:A × (B[a] ⇒ R)) ⇒ R) ⇒ R)))
Lemma: not-not-sig-to-W
∀A:Type. ∀B:A ⟶ Type. ((∀R:Type. (((a:A × (B[a] ⇒ R)) ⇒ R) ⇒ R)) ⇒ W(A;a.B[a]))
Lemma: not-not-sig-to-W-implies-stable
∀[A:Type]. ((∀[B:A ⟶ Type]. ((¬¬(a:A × (¬B[a]))) ⇒ W(A;a.B[a]))) ⇒ Stable{A})
Definition: wfd-tree
wfd-tree(T) == W(𝔹;z.if z then Void else T fi )
Lemma: wfd-tree_wf
∀[T:Type]. (wfd-tree(T) ∈ Type)
Definition: empty-wfd-tree
empty-wfd-tree(t) == wfd-tree-rec(tt;r.ff;t)
Lemma: wfd-tree-induction
∀[T:Type]
∀P:wfd-tree(T) ⟶ ℙ
(P[Wsup(tt;⋅)] ⇒ (∀f:T ⟶ wfd-tree(T). ((∀b:T. P[f b]) ⇒ P[Wsup(ff;f)])) ⇒ {∀t:wfd-tree(T). P[t]})
Definition: wfd-tree-rec
wfd-tree-rec(b;r.F[r];t) == W-rec(a,f,r.if a then b else F[r] fi ;t)
Lemma: wfd-tree-rec_wf
∀[X,T:Type]. ∀[b:X]. ∀[F:(T ⟶ X) ⟶ X]. ∀[t:wfd-tree(T)]. (wfd-tree-rec(b;r.F[r];t) ∈ X)
Lemma: wfd_tree_rec_node_lemma
∀F,f,F,b:Top. (wfd-tree-rec(b;r.F[r];Wsup(ff;f)) ~ F[λx.wfd-tree-rec(b;r.F[r];f x)])
Lemma: wfd_tree_rec_leaf_lemma
∀z,F,b:Top. (wfd-tree-rec(b;x.F[x];Wsup(tt;z)) ~ b)
Lemma: empty-wfd-tree_wf
∀[T:Type]. ∀[t:wfd-tree(T)]. (empty-wfd-tree(t) ∈ 𝔹)
Definition: stump
stump(t) == wfd-tree-rec(λn,s. ff;r.λn,s. if (n =z 0) then tt else r (s 0) (n - 1) (λi.(s (i + 1))) fi ;t)
Lemma: stump_wf
∀[T:Type]. ∀[t:wfd-tree(T)]. (stump(t) ∈ n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹)
Lemma: stump-monotone
∀T:Type. ∀t:wfd-tree(T). ∀n:ℕ. ∀s:ℕn ⟶ T. ((¬↑(stump(t) n s)) ⇒ (∀x:T. (¬↑(stump(t) (n + 1) s++x))))
Lemma: stump-bars
∀T:Type. ∀t:wfd-tree(T). ∀alpha:ℕ ⟶ T. ∃n:ℕ. (¬↑(stump(t) n alpha))
Lemma: stump-nil
∀T:Type. ∀t:wfd-tree(T). ∀s:ℕ0 ⟶ T. (stump(t) 0 s ~ ¬bempty-wfd-tree(t))
Definition: stump'
stump'(t) == λn,s. if (n =z 0) then empty-wfd-tree(t) else (¬b(stump(t) n s)) ∧b (stump(t) (n - 1) s) fi
Lemma: stump'_wf
∀[T:Type]. ∀[t:wfd-tree(T)]. (stump'(t) ∈ n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹)
Lemma: stump'_property
∀T:Type. ∀t:wfd-tree(T). ∀n:ℕ. ∀s:ℕn ⟶ T.
(↑(stump'(t) n s) ⇐⇒ (¬↑(stump(t) n s)) ∧ (0 < n ⇒ (↑(stump(t) (n - 1) s))))
Lemma: stump'-inductive
∀T:Type. ∀t:wfd-tree(T).
(stump'(t)
= wfd-tree-rec(λn,s. (n =z 0);r.λn,s. if (n =z 0) then ff else r (s 0) (n - 1) (λi.(s (i + 1))) fi ;t)
∈ (n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹))
Comment: accessibility
One way to define a well-founded relation R on a type X is to
define inductively the accessible part of X for an arbitrary relation R.
The R is well-founded if every member of X is accessible.
We can define accessible using a W type.
Then we can relate that inductive definition to the other
definitions of well-foundedness.⋅
Definition: accessible
accessible(T;x,y.R[x; y];t) == pW t
Lemma: accessible_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[t:T]. (accessible(T;x,y.R[x;y];t) ∈ ℙ)
Lemma: accessible-iff
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[t:T]. (accessible(T;x,y.R[x;y];t) ⇐⇒ ∀u:T. (R[u;t] ⇒ accessible(T;x,y.R[x;y];u)))
Lemma: accessible-inversion
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[u:T]. ∀v:T. (accessible(T;x,y.R[x;y];u) ⇒ R[v;u] ⇒ accessible(T;x,y.R[x;y];v))
Lemma: accessible-induction
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[P:T ⟶ ℙ].
((∀t:T. ((∀x:T. (R[x;t] ⇒ P[x])) ⇒ P[t])) ⇒ (∀t:T. (accessible(T;x,y.R[x;y];t) ⇒ P[t])))
Lemma: all-accessible-iff-induction
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
(∀t:T. accessible(T;x,y.R[x;y];t) ⇐⇒ ∀[P:T ⟶ ℙ]. ((∀t:T. ((∀x:T. (R[x;t] ⇒ P[x])) ⇒ P[t])) ⇒ (∀t:T. P[t])))
Lemma: all-accessible-iff-weak-TI
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (∀t:T. accessible(T;x,y.R[x;y];t) ⇐⇒ ∀[P:T ⟶ ℙ]. weak-TI(T;x,y.R[y;x];t.P[t]))
Lemma: fix_wf_corec1
∀[F,H:Type ⟶ Type].
∀[G:⋂T:{T:Type| (F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T)} . (H[T] ⟶ H[F[T]]) ⋂ Top ⟶ H[Top]]. (fix(G) ∈ H[corec(T.F[T])])
supposing Continuous(T.H[T]) ∧ Monotone(T.F[T])
Lemma: fix_wf_corec2'
∀[F,H:Type ⟶ Type].
∀[G:⋂T:{T:Type| corec(T.F[T]) ⊆r T} . (H[T] ⟶ H[F[T]]) ⋂ Top ⟶ H[Top]]. (fix(G) ∈ H[corec(T.F[T])])
supposing Continuous(T.H[T])
Lemma: fix_wf_corec2
∀[F,H:Type ⟶ Type].
∀[G:⋂T:Type. (H[T] ⟶ H[F[T]]) ⋂ Top ⟶ H[Top]]. (fix(G) ∈ H[corec(T.F[T])]) supposing Continuous(T.H[T])
Lemma: fix_wf_corec
∀[F:Type ⟶ Type]. ∀[G:⋂T:Type. (T ⟶ F[T])]. (fix(G) ∈ corec(T.F[T]))
Lemma: fix_wf_corec_system
∀[F:Type ⟶ Type]
∀[I:Type]. ∀[G:⋂T:{T:Type| (F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ F[T])].
(fix(G) ∈ I ⟶ corec(T.F[T]))
supposing Monotone(T.F[T])
Lemma: fix_wf_corec-alt-proof
∀[F:Type ⟶ Type]. ∀[G:⋂T:Type. (T ⟶ F[T])]. (fix(G) ∈ corec(T.F[T]))
Lemma: fix_wf_corec_parameter
∀[F:Type ⟶ Type]. ∀[A:Type]. ∀[G:Top ⟶ Top ⟶ Top ⋂ ⋂T:Type. ((A ⟶ T) ⟶ A ⟶ F[T])]. ∀[a:A].
(fix(G) a ∈ corec(T.F[T]))
Lemma: fix_wf_corec_parameter2
∀[F,A:Type ⟶ Type].
∀[G:Top ⟶ Top ⟶ Top ⋂ ⋂T:Type. ((A[T] ⟶ T) ⟶ A[F[T]] ⟶ F[T])]. ∀[a:A[corec(T.F[T])]].
(fix(G) a ∈ corec(T.F[T]))
supposing Continuous+(T.A[T])
Lemma: fix_wf_corec_parameter3
∀[F,A:Type ⟶ Type].
∀[G:Top ⟶ Top ⟶ Top ⋂ ⋂T:{T:Type| corec(T.F[T]) ⊆r T} . ((A[T] ⟶ T) ⟶ A[F[T]] ⟶ F[T])]. ∀[a:A[corec(T.F[T])]].
(fix(G) a ∈ corec(T.F[T]))
supposing Continuous+(T.A[T])
Lemma: fix_wf_corec_3parameter
∀[F,A,B,C:Type ⟶ Type].
(∀[G:Top ⟶ Top ⟶ Top ⟶ Top ⟶ Top ⋂ ⋂T:{T:Type| corec(T.F[T]) ⊆r T}
((A[T] ⟶ B[T] ⟶ C[T] ⟶ T) ⟶ A[F[T]] ⟶ B[F[T]] ⟶ C[F[T]] ⟶ F[T])].
∀[a:A[corec(T.F[T])]]. ∀[b:B[corec(T.F[T])]]. ∀[c:C[corec(T.F[T])]].
(fix(G) a b c ∈ corec(T.F[T]))) supposing
(Continuous+(T.C[T]) and
Continuous+(T.B[T]) and
Continuous+(T.A[T]))
Definition: bar-base
bar-base(T) == corec(X.T + X)
Lemma: bar-base_wf
∀[T:Type]. (bar-base(T) ∈ Type)
Lemma: bar-base-exteq
∀[T:Type]. bar-base(T) ≡ T + bar-base(T)
Lemma: bar-base-subtype
∀[T:Type]. (bar-base(T) ⊆r (T + bar-base(T)))
Lemma: bar-base_subtype
∀[T:Type]. ((T + bar-base(T)) ⊆r bar-base(T))
Definition: bar-val
bar-val(n;x) == fix((λbar-val,n,x. case x of inl(b) => x | inr(z) => if (n =z 0) then inr ⋅ else bar-val (n - 1) z fi \000C)) n x
Lemma: bar-val_wf
∀[n:ℕ]. ∀[T:Type]. ∀[x:bar-base(T)]. (bar-val(n;x) ∈ T?)
Lemma: bar-val-stable
∀[T:Type]. ∀[n:ℕ]. ∀[x:bar-base(T)].
∀[m:ℤ]. bar-val(m;x) = bar-val(n;x) ∈ (T?) supposing n ≤ m supposing ↑isl(bar-val(n;x))
Definition: diverge
diverge() == fix((λdiverge.(inr diverge )))
Lemma: diverge_wf
∀[T:Type]. (diverge() ∈ bar-base(T))
Lemma: bar-val-diverge
∀[T:Type]. ∀[n:ℕ]. (bar-val(n;diverge()) ~ inr ⋅ )
Definition: in-bar
in-bar(b) == inl b
Lemma: in-bar_wf
∀[T:Type]. ∀[b:T]. (in-bar(b) ∈ bar-base(T))
Definition: bar-delay
bar-delay(b) == inr b
Lemma: bar-delay_wf
∀[T:Type]. ∀[x:bar-base(T)]. (bar-delay(x) ∈ bar-base(T))
Definition: bar-converges
x↓a == ∃n:ℕ. (bar-val(n;x) = (inl a) ∈ (T?))
Lemma: bar-converges_wf
∀[T:Type]. ∀[x:bar-base(T)]. ∀[a:T]. (x↓a ∈ ℙ)
Lemma: bar-converges-unique
∀[T:Type]. ∀[x:bar-base(T)]. ∀[a,b:T]. (x↓a ⇒ x↓b ⇒ (a = b ∈ T))
Definition: bar-diverges
x↑ == ∀n:ℕ. (¬↑isl(bar-val(n;x)))
Lemma: bar-diverges_wf
∀[T:Type]. ∀[x:bar-base(T)]. (x↑ ∈ ℙ)
Lemma: bar-converges-not-diverges
∀[T:Type]. ∀[x:bar-base(T)]. ∀[a:T]. (x↓a ⇒ (¬x↑))
Lemma: bar-diverges-iff
∀[T:Type]. ∀[x:bar-base(T)]. (x↑ ⇐⇒ ∀[a:T]. (¬x↓a))
Definition: bar-equal
bar-equal(T;x;y) == ∀a:T. (x↓a ⇐⇒ y↓a)
Lemma: bar-equal_wf
∀[T:Type]. ∀[x,y:bar-base(T)]. (bar-equal(T;x;y) ∈ ℙ)
Lemma: bar-equal-equiv
∀[T:Type]. EquivRel(bar-base(T);x,y.bar-equal(T;x;y))
Lemma: bar-converges_functionality
∀[T:Type]. ∀[x,y:bar-base(T)]. ∀[a:T]. (bar-equal(T;x;y) ⇒ {x↓a ⇐⇒ x↓a})
Lemma: bar-diverges_functionality
∀[T:Type]. ∀[x,y:bar-base(T)]. (bar-equal(T;x;y) ⇒ {x↑ ⇐⇒ y↑})
Lemma: implies-bar-equal
∀[T:Type]. ∀x,y:bar-base(T). (((∃a:T. (x↓a ∧ y↓a)) ∨ (x↑ ∧ y↑)) ⇒ bar-equal(T;x;y))
Lemma: in-bar-converges
∀[T:Type]. ∀[b,a:T]. (in-bar(a)↓b ⇐⇒ a = b ∈ T)
Lemma: in-bar-equal
∀[T:Type]. ∀x:bar-base(T). ∀b:T. (bar-equal(T;x;in-bar(b)) ⇐⇒ x↓b)
Lemma: bar-delay-equal
∀[T:Type]. ∀x:bar-base(T). bar-equal(T;x;bar-delay(x))
Definition: corecbar
corecbar(T) == x,y:bar-base(T)//bar-equal(T;x;y)
Lemma: corecbar_wf
∀[T:Type]. (corecbar(T) ∈ Type)
Definition: F-bisimulation
x,y.R[x; y] is an T.F[T]-bisimulation ==
∀T:Type
(((F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T))
⇒ (∀x,y:corec(T.F[T]). (R[x; y] ⇒ (x = y ∈ T)))
⇒ (∀x,y:corec(T.F[T]). (R[x; y] ⇒ (x = y ∈ F[T]))))
Lemma: F-bisimulation_wf
∀[F:Type ⟶ Type]. ∀[R:corec(T.F[T]) ⟶ corec(T.F[T]) ⟶ ℙ].
x,y.R[x;y] is an T.F[T]-bisimulation ∈ ℙ' supposing ContinuousMonotone(T.F[T])
Lemma: coinduction-principle
∀[F:Type ⟶ Type]
∀[R:corec(T.F[T]) ⟶ corec(T.F[T]) ⟶ ℙ]
∀[x,y:corec(T.F[T])]. x = y ∈ corec(T.F[T]) supposing R[x;y] supposing x,y.R[x;y] is an T.F[T]-bisimulation
supposing ContinuousMonotone(T.F[T])
Definition: indexed-F-bisimulation
x,y.R[x; y] is an T.F[T]-bisimulation (indexed I) ==
∀T:Type
(((F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T))
⇒ (∀x,y:I ⟶ corec(T.F[T]). (R[x; y] ⇒ (x = y ∈ (I ⟶ T))))
⇒ (∀x,y:I ⟶ corec(T.F[T]). (R[x; y] ⇒ (x = y ∈ (I ⟶ F[T])))))
Lemma: indexed-F-bisimulation_wf
∀[I:Type]. ∀[F:Type ⟶ Type]. ∀[R:(I ⟶ corec(T.F[T])) ⟶ (I ⟶ corec(T.F[T])) ⟶ ℙ].
x,y.R[x;y] is an T.F[T]-bisimulation (indexed I) ∈ ℙ' supposing ContinuousMonotone(T.F[T])
Lemma: indexed-coinduction-principle
∀[I:Type]. ∀[F:Type ⟶ Type].
∀[R:(I ⟶ corec(T.F[T])) ⟶ (I ⟶ corec(T.F[T])) ⟶ ℙ]
∀[x,y:I ⟶ corec(T.F[T])]. x = y ∈ (I ⟶ corec(T.F[T])) supposing R[x;y]
supposing x,y.R[x;y] is an T.F[T]-bisimulation (indexed I)
supposing ContinuousMonotone(T.F[T])
Definition: corec-rel
corec-rel(G) == λx,y. ∀n:ℕ. (G^n (λx,y. True) x y)
Lemma: corec-rel_wf
∀[F:Type ⟶ Type]
∀[G:⋂T:Type. ((T ⟶ T ⟶ ℙ) ⟶ F[T] ⟶ F[T] ⟶ ℙ)]. (corec-rel(G) ∈ corec(T.F[T]) ⟶ corec(T.F[T]) ⟶ ℙ)
supposing ContinuousMonotone(T.F[T])
Lemma: corec-rel-wf2
∀[F:𝕌' ⟶ 𝕌']
∀[G:⋂T:𝕌'. ((T ⟶ T ⟶ ℙ) ⟶ F[T] ⟶ F[T] ⟶ ℙ)]. (corec-rel(G) ∈ corec(T.F[T]) ⟶ corec(T.F[T]) ⟶ ℙ)
supposing continuous-monotone{i':l}(T.F[T])
Lemma: equiv-on-corec
∀F:Type ⟶ Type
(ContinuousMonotone(T.F[T])
⇒ (∀G:⋂T:Type. ((T ⟶ T ⟶ ℙ) ⟶ F[T] ⟶ F[T] ⟶ ℙ)
((∀T:Type. ∀E:T ⟶ T ⟶ ℙ. (EquivRel(T;x,y.E x y) ⇒ EquivRel(F[T];x,y.G E x y)))
⇒ EquivRel(corec(T.F[T]);x,y.corec-rel(G) x y))))
Lemma: equiv-on-corec-2
∀F:𝕌' ⟶ 𝕌'
(continuous-monotone{i':l}(T.F[T])
⇒ (∀G:⋂T:𝕌'. ((T ⟶ T ⟶ ℙ) ⟶ F[T] ⟶ F[T] ⟶ ℙ)
((∀T:𝕌'. ∀E:T ⟶ T ⟶ ℙ. (EquivRel(T;x,y.E x y) ⇒ EquivRel(F[T];x,y.G E x y)))
⇒ EquivRel(corec(T.F[T]);x,y.corec-rel(G) x y))))
Lemma: unique-corec-solution
∀[F:Type ⟶ Type]
∀[I:Type]
∀G:⋂T:{T:Type| (F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ F[T])
∃!s:I ⟶ corec(T.F[T]). (s = (G s) ∈ (I ⟶ corec(T.F[T])))
supposing ContinuousMonotone(T.F[T])
Lemma: corec_subtype
∀[F:Type ⟶ Type]. corec(T.F[T]) ⊆r F[corec(T.F[T])] supposing Continuous(T.F[T])
Lemma: corec_subtype_base
∀[F:Type ⟶ Type]. corec(T.F[T]) ⊆r Base supposing ∀n:ℕ. ∀T:Type. (sqntype(n;T) ⇒ sqntype(n + 1;F T))
Lemma: subtype_corec
∀[F:Type ⟶ Type]. F[corec(T.F[T])] ⊆r corec(T.F[T]) supposing Monotone(T.F[T])
Lemma: subtype-corec1
∀[F:Type ⟶ Type]. ∀[T:Type]. T ⊆r corec(T.F[T]) supposing T ⊆r F[T] supposing Monotone(T.F[T])
Lemma: subtype-corec2
∀[A,B:Type ⟶ Type].
(let P = corec(T.A[T] ⟶ B[T]) in P ⊆r (A[P] ⟶ B[P])) supposing (Continuous+(T.B[T]) and Continuous+(T.A[T]))
Lemma: corec-subtype-corec2
∀[F,G:Type ⟶ Type]. corec(T.F[T]) ⊆r corec(T.G[T]) supposing ∀A,B:Type. ((A ⊆r B) ⇒ (F[A] ⊆r G[B]))
Lemma: corec-subtype-corec
∀[F,G:Type ⟶ Type]. (corec(T.F[T]) ⊆r corec(T.G[T])) supposing (Monotone(T.G[T]) and (∀T:Type. (F[T] ⊆r G[T])))
Comment: streams
% A simple example of using the co-induction principle on a
co-recursive type.
We will define infinite streams (of type A) in two different ways
⌜corec(S.A × S)⌝ and ⌜ℕ ⟶ A⌝ and show that there is a bijection between them.
And we will define some operators such as map on the corecursive stream type.
We do an exercise from Pitts' lecture notes to show that
fibs() = stream-map(λn.fib(n);nats()) ∈ stream(ℕ)
%⋅
Definition: stream
stream(A) == corec(S.A × S)
Lemma: stream_wf
∀[A:Type]. (stream(A) ∈ Type)
Lemma: stream-subtype
∀[A,B:Type]. stream(A) ⊆r stream(B) supposing A ⊆r B
Lemma: stream-ext
∀[A:Type]. stream(A) ≡ A × stream(A)
Lemma: stream_subtype_base
∀[T:Type]. stream(T) ⊆r Base supposing T ⊆r Base
Definition: s-hd
s-hd(s) == fst(s)
Lemma: s-hd_wf
∀[A:Type]. ∀[s:stream(A)]. (s-hd(s) ∈ A)
Definition: s-tl
s-tl(s) == snd(s)
Lemma: s-tl_wf
∀[A:Type]. ∀[s:stream(A)]. (s-tl(s) ∈ stream(A))
Definition: s-cons
x.s == <x, s>
Lemma: s-cons_wf
∀[A:Type]. ∀[x:A]. ∀[s:stream(A)]. (x.s ∈ stream(A))
Lemma: s_hd_cons_lemma
∀b,a:Top. (s-hd(a.b) ~ a)
Lemma: s_tl_cons_lemma
∀b,a:Top. (s-tl(a.b) ~ b)
Lemma: stream-decomp
∀[s:stream(Top)]. (s ~ s-hd(s).s-tl(s))
Definition: s-nth
s-nth(n;s) == fix((λs-nth,n,s. let a,s' = s in if (n =z 0) then a else eval m = n - 1 in s-nth m s' fi )) n s
Lemma: s-nth_wf
∀[A:Type]. ∀[n:ℕ]. ∀[s:stream(A)]. (s-nth(n;s) ∈ A)
Lemma: stream-coinduction
∀[A:Type]. ∀[R:stream(A) ⟶ stream(A) ⟶ ℙ].
∀[x,y:stream(A)]. x = y ∈ stream(A) supposing x R y
supposing ∀x,y:stream(A). ((x R y) ⇒ ((s-hd(x) = s-hd(y) ∈ A) ∧ (s-tl(x) R s-tl(y))))
Lemma: stream-extensionality
∀[A:Type]. ∀[x,y:stream(A)]. x = y ∈ stream(A) supposing ∀n:ℕ. (s-nth(n;x) = s-nth(n;y) ∈ A)
Definition: mk-stream
mk-stream(f;x) == fix((λmk-stream,x. <x, let y ⟵ f x in mk-stream y>)) x
Lemma: mk-stream_wf
∀[A:Type]. ∀[f:A ⟶ A]. ∀[x:A]. mk-stream(f;x) ∈ stream(A) supposing valueall-type(A)
Definition: const-stream
const-stream(x) == mk-stream(λz.x;x)
Lemma: const-stream_wf
∀[A:Type]. ∀[x:A]. const-stream(x) ∈ stream(A) supposing valueall-type(A)
Definition: stream-map
stream-map(f;s) == fix((λstream-map,s. let a,s' = s in <f a, stream-map s'>)) s
Lemma: stream-map_wf
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[s:stream(A)]. (stream-map(f;s) ∈ stream(B))
Definition: stream-zip
stream-zip(f;as;bs) == fix((λstream-zip,as,bs. let a,as' = as in let b,bs' = bs in <f a b, stream-zip as' bs'>)) as bs
Lemma: stream-zip_wf
∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[as:stream(A)]. ∀[bs:stream(B)]. (stream-zip(f;as;bs) ∈ stream(C))
Lemma: stream-zip_wf2
∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[n:ℕ]. ∀[as:primrec(n;Top;λ,T. (A × T))]. ∀[bs:primrec(n;Top;λ,T. (B × T))].
(stream-zip(f;as;bs) ∈ primrec(n;Top;λ,T. (C × T)))
Lemma: nth-stream-zip
∀[f:Top]. ∀[n:ℕ]. ∀[as,bs:stream(Top)]. (s-nth(n;stream-zip(f;as;bs)) ~ f s-nth(n;as) s-nth(n;bs))
Lemma: tl-stream-zip
∀[f:Top]. ∀[as,bs:stream(Top)]. (s-tl(stream-zip(f;as;bs)) ~ stream-zip(f;s-tl(as);s-tl(bs)))
Lemma: hd-stream-zip
∀[f:Top]. ∀[as,bs:stream(Top)]. (s-hd(stream-zip(f;as;bs)) ~ f s-hd(as) s-hd(bs))
Lemma: nth-stream-map
∀[f:Top]. ∀[n:ℕ]. ∀[as:stream(Top)]. (s-nth(n;stream-map(f;as)) ~ f s-nth(n;as))
Definition: nats
nats() == mk-stream(λx.(x + 1);0)
Lemma: nats_wf
nats() ∈ stream(ℕ)
Lemma: nth-nats
∀n:ℕ. (s-nth(n;nats()) ~ n)
Lemma: stream-bijection
∀[A:Type]. Bij(stream(A);ℕ ⟶ A;λs,n. s-nth(n;s))
Definition: stream-lex
stream-lex(T;R) == νlex.λs1,s2. ((s-hd(s1) R s-hd(s2)) ∧ ((s-hd(s1) = s-hd(s2) ∈ T) ⇒ (s-tl(s1) lex s-tl(s2))))
Lemma: stream-lex_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (stream-lex(T;R) ∈ stream(T) ⟶ stream(T) ⟶ ℙ)
Lemma: stream-lex-iff
∀T:Type. ∀R:T ⟶ T ⟶ ℙ. ∀s1,s2:stream(T).
(s1 stream-lex(T;R) s2 ⇐⇒ (s-hd(s1) R s-hd(s2)) ∧ ((s-hd(s1) = s-hd(s2) ∈ T) ⇒ (s-tl(s1) stream-lex(T;R) s-tl(s2))))
Lemma: stream-lex_transitivity-proof2
∀T:Type. ∀R:T ⟶ T ⟶ ℙ. (Trans(T;x,y.x R y) ⇒ AntiSym(T;x,y.x R y) ⇒ Trans(stream(T);s1,s2.s1 stream-lex(T;R) s2))
Lemma: stream-lex-monotonic
∀T:Type
((∀x,y:T. Dec(x = y ∈ T))
⇒ (∀R:T ⟶ T ⟶ ℙ
(Trans(T;x,y.x R y)
⇒ AntiSym(T;x,y.x R y)
⇒ (∀f:T ⟶ T ⟶ T
((∀x,y,u,v:T. ((x R y) ⇒ (u R v) ⇒ ((f x u) R (f y v))))
⇒ (∀x,y,u,v:T. ((x R y) ⇒ (u R v) ⇒ (¬((x = y ∈ T) ∧ (u = v ∈ T))) ⇒ (¬((f x u) = (f y v) ∈ T))))
⇒ (∀a,b,c,d:stream(T).
((a stream-lex(T;R) b)
⇒ (c stream-lex(T;R) d)
⇒ (stream-zip(f;a;c) stream-lex(T;R) stream-zip(f;b;d)))))))))
Lemma: stream-lex_transitivity
∀T:Type. ∀R:T ⟶ T ⟶ ℙ. (Trans(T;x,y.x R y) ⇒ AntiSym(T;x,y.x R y) ⇒ Trans(stream(T);s1,s2.s1 stream-lex(T;R) s2))
Definition: stream-pointwise
stream-pointwise(R) == νptwse.λs1,s2. ((s-hd(s1) R s-hd(s2)) ∧ (s-tl(s1) ptwse s-tl(s2)))
Lemma: stream-pointwise_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (stream-pointwise(R) ∈ stream(T) ⟶ stream(T) ⟶ ℙ)
Lemma: stream-pointwise-iff
∀[T:Type]
∀R:T ⟶ T ⟶ ℙ. ∀s1,s2:stream(T).
(s1 stream-pointwise(R) s2 ⇐⇒ (s-hd(s1) R s-hd(s2)) ∧ (s-tl(s1) stream-pointwise(R) s-tl(s2)))
Lemma: stream-pointwise_transitivity
∀T:Type. ∀R:T ⟶ T ⟶ ℙ. (Trans(T;x,y.x R y) ⇒ Trans(stream(T);s1,s2.s1 stream-pointwise(R) s2))
Lemma: equal-zero-streams
fix((λx.<⋅, x>)) ~ fix((λx.<⋅, ⋅, x>))
Definition: s-sub
s-sub(T;s;t) == ∃f:ℕ ⟶ ℕ. ((∀i:ℕ. f i < f (i + 1)) ∧ (∀i:ℕ. (s-nth(i;t) = s-nth(f i;s) ∈ T)))
Lemma: s-sub_wf
∀[T:Type]. ∀[s,t:stream(T)]. (s-sub(T;s;t) ∈ ℙ)
Lemma: s-sub_transitivity
∀[T:Type]. ∀[s,t,r:stream(T)]. (s-sub(T;s;t) ⇒ s-sub(T;t;r) ⇒ s-sub(T;s;r))
Lemma: corec-subtype
∀[F:Type ⟶ Type]. corec(T.F[T]) ⊆r F[corec(T.F[T])] supposing Continuous(T.F[T])
Definition: iterate-fun-stream
iterate-fun-stream(f;x) == fix((λiterate-fun-stream,x. x.iterate-fun-stream (f x))) x
Lemma: iterate-fun-stream_wf
∀[A:Type]. ∀[x:A]. ∀[f:A ⟶ A]. (iterate-fun-stream(f;x) ∈ stream(A))
Lemma: map-iterate-fun-stream
∀[f,x:Top]. (iterate-fun-stream(f;f x) ~ stream-map(f;iterate-fun-stream(f;x)))
Lemma: fix-corec-partial1
∀[A:Type]
(∀[F:Type ⟶ Type]. ∀[f:(corec(T.F[T]) ⟶ partial(A)) ⟶ corec(T.F[T]) ⟶ partial(A)].
(fix(f) ∈ corec(T.F[T]) ⟶ partial(A))) supposing
(mono(A) and
value-type(A))
Lemma: fix_wf_corec-partial1
∀[A:Type]
(∀[F:Type ⟶ Type]
∀[f:⋂T:Type. ((T ⟶ partial(A)) ⟶ F[T] ⟶ partial(A))]. (fix(f) ∈ corec(T.F[T]) ⟶ partial(A))
supposing ContinuousMonotone(T.F[T])) supposing
(mono(A) and
value-type(A))
Lemma: fix_wf_corec_partial_nat
∀[F:Type ⟶ Type]
∀[f:⋂T:Type. ((T ⟶ partial(ℕ)) ⟶ F[T] ⟶ partial(ℕ))]. (fix(f) ∈ corec(T.F[T]) ⟶ partial(ℕ))
supposing ContinuousMonotone(T.F[T])
Home
Index