Definition: bar-recursion
bar-recursion(d;
b;
i;
s) ==
fix((λbar-recursion,s. case d s of inl(r) => b s r | inr(r) => i s (λt.(bar-recursion (s @ [t]))))) s
Lemma: bar-recursion_wf
∀[T:Type]. ∀[R,A:(T List) ⟶ ℙ]. ∀[d:∀s:T List. Dec(R[s])]. ∀[b:∀s:T List. (R[s] ⇒ A[s])]. ∀[i:∀s:T List
((∀t:T. A[s @ [t]])
⇒ A[s])].
∀[s:T List].
((∀alpha:ℕ ⟶ T. (↓∃n:ℕ. R[s @ map(alpha;upto(n))])) ⇒ (bar-recursion(d;b;i;s) ∈ A[s]))
Definition: bbar-recursion
bbar-recursion(d;b;i;s) == fix((λbbar-recursion,s. if d s then b s else i s (λt.(bbar-recursion (s @ [t]))) fi )) s
Lemma: bbar-recursion_wf
∀[T:Type]. ∀[R:(T List) ⟶ 𝔹]. ∀[A:(T List) ⟶ ℙ]. ∀[b:∀s:{s:T List| ↑R[s]} . A[s]]. ∀[i:∀s:{s:T List| ¬↑R[s]}
((∀t:T. A[s @ [t]]) ⇒ A[s])].
∀[s:T List].
((∀alpha:ℕ ⟶ T. (↓∃n:ℕ. (↑R[s @ map(alpha;upto(n))]))) ⇒ (bbar-recursion(R;b;i;s) ∈ A[s]))
Lemma: bar-induction (dup of thm in list_1)
∀[T:Type]. ∀[R,A:(T List) ⟶ ℙ].
((∀s:T List. Dec(R[s]))
⇒ (∀s:T List. (R[s] ⇒ A[s]))
⇒ (∀s:T List. ((∀t:T. A[s @ [t]]) ⇒ A[s]))
⇒ (∀s:T List. ((∀alpha:ℕ ⟶ T. (↓∃n:ℕ. R[s @ map(alpha;upto(n))])) ⇒ A[s])))
Lemma: bool-bar-induction
∀[T:Type]. ∀[A:(T List) ⟶ ℙ].
∀R:(T List) ⟶ 𝔹
((∀s:{s:T List| ↑R[s]} . A[s])
⇒ (∀s:{s:T List| ¬↑R[s]} . ((∀t:T. A[s @ [t]]) ⇒ A[s]))
⇒ (∀alpha:ℕ ⟶ T. (↓∃n:ℕ. (↑R[map(alpha;upto(n))])))
⇒ A[[]])
Lemma: simple-fan-theorem
∀[X:(𝔹 List) ⟶ ℙ]. ∀bar:tbar(𝔹;X). ∀d:Decidable(X). (∃k:ℕ [(∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (X map(f;upto(n))))])
Lemma: fan-theorem
∀[X:(𝔹 List) ⟶ ℙ]. (tbar(𝔹;X) ⇒ Decidable(X) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (X map(f;upto(n)))))
Definition: fan-realizer
fan-realizer ==
λbar,d. eval k = bar_recursion(λn,s. (d map(s;upto(n)));
λ_,__,___. 1;
λ_,__,e. eval a = e tt in eval b = e ff in if (a) < (b) then 1 + b else (1 + a);
0;λm.eval x = m in
⊥) in
<k, λf.outl(int_seg_decide(λn.(d map(f;upto(n)));0;k))>
Lemma: fan-realizer_wf
fan-realizer ∈ ∀[X:(𝔹 List) ⟶ ℙ]. (tbar(𝔹;X) ⇒ Decidable(X) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (X map(f;upto(n)))))
Lemma: fan-realizer_test
∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. ((λl.(3 ≤ ||l||)) map(f;upto(n)))
Lemma: fan-realizer_test2
∀m:ℕ. ∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. ((λl.(m ≤ ||l||)) map(f;upto(n)))
Lemma: weak-konig-lemma!
WKL!
Definition: co-w
co-w(A) == corec(T.Unit + (A ⟶ T))
Lemma: co-w_wf
∀[A:Type]. (co-w(A) ∈ Type)
Lemma: co-w-ext
∀[A:Type]. co-w(A) ≡ Unit + (A ⟶ co-w(A))
Definition: co-w-null
co-w-null(w) == isl(w)
Lemma: co-w-null_wf
∀[A:Type]. ∀[w:co-w(A)]. (co-w-null(w) ∈ 𝔹)
Definition: co-w-select
w@s == fix((λco-w-select,w,s. if null(s) ∨bisl(w) then w else co-w-select (outr(w) hd(s)) tl(s) fi )) w s
Lemma: co-w-select_wf
∀[A:Type]. ∀[s:A List]. ∀[w:co-w(A)]. (w@s ∈ co-w(A))
Lemma: co_w_select_nil_lemma
∀w:Top. (w@[] ~ w)
Definition: w-bars
w-bars(w;p) == ↓∃n:ℕ. (↑co-w-null(w@map(p;upto(n))))
Lemma: w-bars_wf
∀[A:Type]. ∀[w:co-w(A)]. ∀[p:ℕ ⟶ A]. (w-bars(w;p) ∈ ℙ)
Definition: wfd-tree
wfd-tree(A) == {w:co-w(A)| ∀p:ℕ ⟶ A. w-bars(w;p)}
Lemma: wfd-tree2_wf
∀[A:Type]. (wfd-tree(A) ∈ Type)
Definition: w-nil
w-nil() == inl ⋅
Lemma: w-nil_wf
∀[A:Type]. (w-nil() ∈ wfd-tree(A))
Lemma: assert-co-w-null
∀[A:Type]. ∀[w:co-w(A)]. uiff(↑co-w-null(w);w = w-nil() ∈ co-w(A))
Definition: mk-wfd-tree
mk-wfd-tree(f) == inr f
Lemma: mk-wfd-tree_wf
∀[A:Type]. ∀[f:A ⟶ wfd-tree(A)]. (mk-wfd-tree(f) ∈ wfd-tree(A))
Definition: wfd-subtrees
wfd-subtrees(w) == outr(w)
Lemma: wfd-subtrees_wf
∀[A:Type]. ∀[w:wfd-tree(A)]. wfd-subtrees(w) ∈ A ⟶ wfd-tree(A) supposing ¬↑co-w-null(w)
Lemma: wfd-tree-cases
∀[A:Type]
∀w:wfd-tree(A). ((w = w-nil() ∈ wfd-tree(A)) ∨ ((¬↑co-w-null(w)) ∧ (w = mk-wfd-tree(wfd-subtrees(w)) ∈ wfd-tree(A))))
Lemma: co-w-select-wfd
∀[A:Type]. ∀[s:A List]. ∀[w:wfd-tree(A)]. (w@s ∈ wfd-tree(A))
Lemma: wfd-tree-induction
∀[A:Type]. ∀[P:wfd-tree(A) ⟶ ℙ].
(P[w-nil()] ⇒ (∀f:A ⟶ wfd-tree(A). ((∀a:A. P[f a]) ⇒ P[mk-wfd-tree(f)])) ⇒ (∀w:wfd-tree(A). P[w]))
Lemma: wfd-tree-induction-ext
∀[A:Type]. ∀[P:wfd-tree(A) ⟶ ℙ].
(P[w-nil()] ⇒ (∀f:A ⟶ wfd-tree(A). ((∀a:A. P[f a]) ⇒ P[mk-wfd-tree(f)])) ⇒ (∀w:wfd-tree(A). P[w]))
Definition: co-W
co-W(A;a.B[a]) == corec(T.a:A × (B[a] ⟶ T))
Lemma: co-W_wf
∀[A:Type]. ∀[B:A ⟶ Type]. (co-W(A;a.B[a]) ∈ Type)
Lemma: co-W-ext
∀[A:Type]. ∀[B:A ⟶ Type]. co-W(A;a.B[a]) ≡ a:A × (B[a] ⟶ co-W(A;a.B[a]))
Definition: W-select
W-select(w;s)
==r if null(s) then inl w else let a,f = w in case hd(s) a of inl(b) => W-select(f b;tl(s)) | inr(z) => inr z fi
Lemma: W-select_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[s:(a:A ⟶ (B[a]?)) List]. ∀[w:co-W(A;a.B[a])]. (W-select(w;s) ∈ co-W(A;a.B[a])?)
Lemma: W_select_nil_lemma
∀w:Top. (W-select(w;[]) ~ inl w)
Definition: W-null
W-null(eq;a0;w) == eq a0 (fst(w))
Definition: W-bars
W-bars(w;p) == ↓∃n:ℕ. (↑isr(W-select(w;map(p;upto(n)))))
Lemma: W-bars_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[w:co-W(A;a.B[a])]. ∀p:ℕ ⟶ a:A ⟶ (B[a]?). (W-bars(w;p) ∈ ℙ)
Lemma: sq_stable__W-bars
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[w:co-W(A;a.B[a])]. ∀p:ℕ ⟶ a:A ⟶ (B[a]?). SqStable(W-bars(w;p))
Definition: W-type
W-type(A; a.B[a]) == {w:co-W(A;a.B[a])| ∀p:ℕ ⟶ a:A ⟶ (B[a]?). W-bars(w;p)}
Lemma: W-type_wf
∀[A:Type]. ∀[B:A ⟶ Type]. (W-type(A; a.B[a]) ∈ Type)
Definition: W-sup
W-sup(a;f) == <a, f>
Lemma: W-sup_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[a:A]. ∀[f:B[a] ⟶ W-type(A; a.B[a])]. (W-sup(a;f) ∈ W-type(A; a.B[a]))
Lemma: W-type-ext
∀[A:Type]. ∀[B:A ⟶ Type]. W-type(A; a.B[a]) ≡ a:A × (B[a] ⟶ W-type(A; a.B[a])) supposing ∀x,y:A. Dec(x = y ∈ A)
Definition: Wselect
Wselect(w;s) == W-select(w;s)
Lemma: Wselect_wf
∀[A:Type]
∀[B:A ⟶ Type]. ∀[s:(a:A ⟶ (B[a]?)) List]. ∀[w:W-type(A; a.B[a])]. (Wselect(w;s) ∈ W-type(A; a.B[a])?)
supposing ∀x,y:A. Dec(x = y ∈ A)
Lemma: W-type-induction
∀[A:Type]
((∀x,y:A. Dec(x = y ∈ A))
⇒ (∀[B:A ⟶ Type]. ∀[P:W-type(A; a.B[a]) ⟶ ℙ].
((∀a:A. ∀f:B[a] ⟶ W-type(A; a.B[a]). ((∀b:B[a]. P[f b]) ⇒ P[W-sup(a;f)])) ⇒ (∀w:W-type(A; a.B[a]). P[w]))))
Home
Index