Comment: fun_1_summary
Polymorphic identity and composition functions.
Lemmas covering properties suchas injectivity and
surjectivity.
Comment: fun_1_intro
Definitions are introduced for polymorphic identity and
composition functions, and for predicates such as
injectivity and surjectivity.
Basic properties of the functions are proven, as are
inter-relationshsips between the predicates.
Variants on lambda abstraction and the identity function are
introduced that include type tags that vanish when the definitions
are unfolded. Use of these type tags is encouraged, since the
type inference routines sometimes have difficulties without them
(the current type inference routine works on terms bottom up, and
doesn't handle polymorhic types as well as it should).
Definition: identity
Id == λx.x
Lemma: identity_wf
∀[A:Type]. (Id ∈ A ⟶ A)
Definition: tidentity
Id{T} == Id
Lemma: tidentity_wf
∀[A:Type]. (Id{A} ∈ A ⟶ A)
Lemma: my_tidentity_wf
∀[A:Type]. (Id{A} ∈ A ⟶ A)
Lemma: eta_conv
∀[A,B:Type]. ∀[f:A ⟶ B]. ((λx.(f x)) = f ∈ (A ⟶ B))
Definition: tlambda
λx:T. b[x] == λx.b[x]
Definition: compose
f o g == λx.(f (g x))
Lemma: compose_wf
∀[A,B,C:Type]. ∀[f:B ⟶ C]. ∀[g:A ⟶ B]. (f o g ∈ A ⟶ C)
Lemma: comb_for_compose_wf
λA,B,C,f,g,z. (f o g) ∈ A:Type ⟶ B:Type ⟶ C:Type ⟶ f:(B ⟶ C) ⟶ g:(A ⟶ B) ⟶ (↓True) ⟶ A ⟶ C
Lemma: comp_assoc
∀[A,B,C,D:Type]. ∀[f:A ⟶ B]. ∀[g:B ⟶ C]. ∀[h:C ⟶ D]. ((h o (g o f)) = ((h o g) o f) ∈ (A ⟶ D))
Lemma: comp_id_l
∀[A,B:Type]. ∀[f:A ⟶ B]. ((Id{B} o f) = f ∈ (A ⟶ B))
Lemma: comp_id_r
∀[A,B:Type]. ∀[f:A ⟶ B]. ((f o Id{A}) = f ∈ (A ⟶ B))
Definition: inv_funs
InvFuns(A;B;f;g) == ((g o f) = Id{A} ∈ (A ⟶ A)) ∧ ((f o g) = Id{B} ∈ (B ⟶ B))
Lemma: inv_funs_wf
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[g:B ⟶ A]. (InvFuns(A;B;f;g) ∈ ℙ)
Lemma: inv_funs-iff
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[g:B ⟶ A]. (InvFuns(A;B;f;g) ⇐⇒ (∀a:A. ((g (f a)) = a ∈ A)) ∧ (∀b:B. ((f (g b)) = b ∈ B)))
Lemma: sq_stable__inv_funs
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[g:B ⟶ A]. SqStable(InvFuns(A;B;f;g))
Definition: one_one_corr
1-1-Corresp(A;B) == ∃f:A ⟶ B. ∃g:B ⟶ A. InvFuns(A;B;f;g)
Lemma: one_one_corr_wf
∀[A,B:Type]. (1-1-Corresp(A;B) ∈ ℙ)
Definition: inject
(basic):: Inj(A;B;f) == ∀a1,a2:A. (((f a1) = (f a2) ∈ B) ⇒ (a1 = a2 ∈ A))
Lemma: inject_wf
∀[A,B:Type]. ∀[f:A ⟶ B]. (Inj(A;B;f) ∈ ℙ)
Lemma: sq_stable__inject
∀[A,B:Type]. ∀[f:A ⟶ B]. SqStable(Inj(A;B;f))
Definition: surject
Surj(A;B;f) == ∀b:B. ∃a:A. ((f a) = b ∈ B)
Lemma: surject_wf
∀[A,B:Type]. ∀[f:A ⟶ B]. (Surj(A;B;f) ∈ ℙ)
Lemma: compose-surjections
∀[A,B,C:Type]. ∀[f:A ⟶ B]. ∀[g:B ⟶ C]. (Surj(A;B;f) ⇒ Surj(B;C;g) ⇒ Surj(A;C;g o f))
Definition: biject
Bij(A;B;f) == Inj(A;B;f) ∧ Surj(A;B;f)
Lemma: biject_wf
∀[A,B:Type]. ∀[f:A ⟶ B]. (Bij(A;B;f) ∈ ℙ)
Lemma: ext-eq-implies-biject
∀[T,S:Type]. (T ≡ S ⇒ Bij(S;T;λx.x))
Lemma: ax_choice
∀[A,B:Type]. ∀[Q:A ⟶ B ⟶ ℙ]. ((∀x:A. ∃y:B. Q[x;y]) ⇒ (∃f:A ⟶ B. ∀x:A. Q[x;f x]))
Lemma: dep_ax_choice
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[Q:x:A ⟶ B[x] ⟶ Type]. ((∀x:A. ∃y:B[x]. Q[x;y]) ⇒ (∃f:x:A ⟶ B[x]. ∀x:A. Q[x;f x]))
Lemma: inv_funs_sym
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[g:B ⟶ A]. InvFuns(B;A;g;f) supposing InvFuns(A;B;f;g)
Lemma: bij_imp_exists_inv
∀[A,B:Type]. ∀f:A ⟶ B. (Bij(A;B;f) ⇒ (∃g:B ⟶ A. InvFuns(A;B;f;g)))
Lemma: fun_with_inv_is_bij
∀[A,B:Type]. ∀f:A ⟶ B. ∀g:B ⟶ A. Bij(A;B;f) supposing InvFuns(A;B;f;g)
Lemma: bij_iff_1_1_corr
∀[A,B:Type]. (∃f:A ⟶ B. Bij(A;B;f) ⇐⇒ 1-1-Corresp(A;B))
Lemma: compose_increasing
∀[k,m:ℕ]. ∀[f:ℕk ⟶ ℕm]. ∀[g:ℕm ⟶ ℤ]. (increasing(g o f;k)) supposing (increasing(g;m) and increasing(f;k))
Lemma: increasing_inj
∀[k,m:ℕ]. ∀[f:ℕk ⟶ ℕm]. Inj(ℕk;ℕm;f) supposing increasing(f;k)
Lemma: bijection_restriction
∀k:ℕ. ∀f:ℕk ⟶ ℕk.
Bij(ℕk;ℕk;f) ⇒ {(f ∈ ℕk - 1 ⟶ ℕk - 1) ∧ Bij(ℕk - 1;ℕk - 1;f)} supposing (f (k - 1)) = (k - 1) ∈ ℤ supposing 0 < k
Lemma: compose-injections
∀[T:Type]. ∀[f,g:{f:T ⟶ T| Inj(T;T;f)} ]. (f o g ∈ {f:T ⟶ T| Inj(T;T;f)} )
Lemma: injection-if-compose-injection
∀[T:Type]. ∀[f,g:T ⟶ T]. Inj(T;T;f) supposing Inj(T;T;g o f)
Lemma: inject-compose
∀[T:Type]. ∀[f,g:T ⟶ T]. (Inj(T;T;f o g)) supposing (Inj(T;T;g) and Inj(T;T;f))
Lemma: injection-composition
∀[A,B,C:Type]. ∀[f:A ⟶ B]. ∀[g:B ⟶ C]. (Inj(A;C;g o f)) supposing (Inj(B;C;g) and Inj(A;B;f))
Definition: fun_exp
f^n == primrec(n;λx.x;λi,g. (f o g))
Lemma: fun_exp_wf
∀[T:Type]. ∀[n:ℕ]. ∀[f:T ⟶ T]. (f^n ∈ T ⟶ T)
Lemma: fun_exp_unroll
∀[n:ℕ]. ∀[f:Top]. (f^n ~ if (n =z 0) then λx.x else f o f^n - 1 fi )
Lemma: fun_exp_unroll_1
∀[n:ℕ+]. ∀[f:Top]. (f^n ~ λx.(f (f^n - 1 x)))
Lemma: comb_for_fun_exp_wf
λT,n,f,z. f^n ∈ T:Type ⟶ n:ℕ ⟶ f:(T ⟶ T) ⟶ (↓True) ⟶ T ⟶ T
Lemma: simple-dependent-choice
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
((∀x:T. ∃y:T. R[x;y]) ⇒ (∀x0:T. ∃f:ℕ ⟶ T. (((f 0) = x0 ∈ T) ∧ (∀i:ℕ. R[f i;f (i + 1)]))))
Lemma: dependent-choice
∀[T:ℕ ⟶ Type]. ∀[R:n:ℕ ⟶ T[n] ⟶ T[n + 1] ⟶ ℙ].
((∀n:ℕ. ∀x:T[n]. ∃y:T[n + 1]. R[n;x;y])
⇒ (∀x0:T[0]. ∃f:n:ℕ ⟶ T[n]. (((f 0) = x0 ∈ T[0]) ∧ (∀n:ℕ. R[n;f n;f (n + 1)]))))
Lemma: cWO-induction-extract-sqequal
λf.fix((λF,t. (f t F))) ~ TERMOF{cWO-induction_1-ext:o, \\v:l, i:l}
Lemma: cWO-induction
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[Q:T ⟶ ℙ]. TI(T;x,y.R[x;y];t.Q[t]) supposing cWO(T;x,y.R[x;y])
Lemma: fun_exp_compose
∀[T:Type]. ∀[n:ℕ]. ∀[h,f:T ⟶ T]. ((f^n o h) = primrec(n;h;λi,g. (f o g)) ∈ (T ⟶ T))
Lemma: fun_exp_add
∀[T:Type]. ∀[n,m:ℕ]. ∀[f:T ⟶ T]. (f^n + m = (f^n o f^m) ∈ (T ⟶ T))
Lemma: fun_exp_add_apply
∀[T:Type]. ∀[n,m:ℕ]. ∀[f:T ⟶ T]. ∀[x:T]. ((f^n (f^m x)) = (f^n + m x) ∈ T)
Lemma: fun_exp_add_apply1
∀[T:Type]. ∀[n:ℕ]. ∀[f:T ⟶ T]. ∀[x:T]. ((f^n (f x)) = (f^n + 1 x) ∈ T)
Lemma: fun_exp_apply_add1
∀[T:Type]. ∀[n:ℕ]. ∀[f:T ⟶ T]. ∀[x:T]. ((f (f^n x)) = (f^n + 1 x) ∈ T)
Lemma: fun_exp_com
∀[T:Type]. ∀[n,m:ℕ]. ∀[f:T ⟶ T]. ∀[x:T]. ((f^m (f^n x)) = (f^n (f^m x)) ∈ T)
Lemma: fun_exp0_lemma
∀f:Top. (f^0 ~ λx.x)
Lemma: fun_exp1_lemma
∀f:Top. (f^1 ~ f o (λx.x))
Lemma: fun_exp_add1
∀[f,x:Top]. ∀[n:ℕ]. (f (f^n x) ~ f^n + 1 x)
Lemma: fun_exp_add1_sub
∀[T:Type]. ∀[f:T ⟶ T]. ∀[x:T]. ∀[n:ℕ+]. ((f (f^n - 1 x)) = (f^n x) ∈ T)
Lemma: fun_exp_compose2
∀[A,B:Type]. ∀[h:A ⟶ A]. ∀[n:ℕ]. (λg.(g o h)^n = (λg.(g o h^n)) ∈ ((A ⟶ B) ⟶ A ⟶ B))
Lemma: fun_exp_add_sq
∀[n,m:ℕ]. ∀[f,i:Top]. (f^n + m i ~ f^n (f^m i))
Lemma: fun_exp_add-sq
∀[n,m:ℕ]. ∀[f,x:Top]. (f^n + m x ~ f^n (f^m x))
Lemma: fun_exp_add1-sq
∀[n:ℕ]. ∀[f,x:Top]. (f (f^n x) ~ f^n + 1 x)
Lemma: fun_exp_add1-sq2
∀[n:ℕ]. ∀[f,x:Top]. (f^n (f x) ~ f^n + 1 x)
Lemma: fun_exp-injection
∀[T:Type]. ∀[f:T ⟶ T]. ∀[n:ℕ]. Inj(T;T;f^n) supposing Inj(T;T;f)
Lemma: fun_exp-fixedpoint
∀[T:Type]. ∀[f:T ⟶ T]. ∀[x:T]. ∀[n:ℕ]. ((f^n x) = x ∈ T) supposing (f x) = x ∈ T
Lemma: fun_exp-id
∀[n:ℕ]. ∀[x:Top]. (λi.i^n x ~ x)
Lemma: fun_exp-increasing
∀[T:Type]. ((T ⊆r ℤ) ⇒ (∀f:T ⟶ T. ((∀n:T. n < f n) ⇒ (∀n:T. ∀i,j:ℕ. (i < j ⇒ f^i n < f^j n)))))
Lemma: surject-nat-bool
∃g:ℕ ⟶ 𝔹. Surj(ℕ;𝔹;g)
Lemma: biject-bool-nsub2
∃f:𝔹 ⟶ ℕ2. Bij(𝔹;ℕ2;f)
Lemma: fixpoint-upper-bound
∀j:ℕ. ∀F:Top. (F^j ⊥ ≤ fix(F))
Lemma: fix-strict
∀[F:Base]. strict1(fix(F)) supposing strict2(λx,y. (F y x))
Lemma: evalall-sqequal
∀[x:Base]. evalall(x) ~ x supposing (evalall(x))↓
Lemma: evalall-sqle
∀[x:Base]. evalall(x) ≤ x supposing (evalall(x))↓
Lemma: evalall-sqequal2
∀[x:Base]. evalall(x) ~ x supposing (evalall(x))↓
Lemma: evalall-reduce
∀[T:Type]. ∀[t:T]. evalall(t) ~ t supposing valueall-type(T)
Lemma: evalall-equal
∀[T:Type]. ∀[t:T]. evalall(t) = t ∈ T supposing valueall-type(T)
Lemma: evalall-evalall
∀[t:Top]. (evalall(evalall(t)) ~ evalall(t))
Lemma: evalall-ifthenelse
∀[a,b,c:Top]. (evalall(if a then b else c fi ) ~ if a then evalall(b) else evalall(c) fi )
Lemma: has-valueall-apply
∀[a,g:Base]. has-valueall(g) supposing has-valueall(g a)
Lemma: valueall-type-value-type
∀[A:Type]. value-type(A) supposing valueall-type(A)
Lemma: valueall-type-has-value
∀[T:Type]. ∀[t:T]. (t)↓ supposing valueall-type(T)
Lemma: cbv-all-identity
∀[T:Type]. ∀[t:T]. let x ⟵ t in x ∈ T supposing valueall-type(T)
Lemma: cbva-intro-test
∀[T:Type]. ∀x:T. T supposing valueall-type(T)
Lemma: cbv-intro-test
∀[T:Type]. ∀x:T. T supposing value-type(T)
Lemma: test-cbva-normalize
∀[a,B:Top]. (let x ⟵ a in <let y ⟵ x in B[y], let z ⟵ a in B[z] + 22, eval w = a in B[w] + 3 + 1> ~ let x ⟵ a in <B\000C[x], B[x] + 22, (B[x] + 3) + 1>)
Lemma: test-cbv-normalize
∀[a,B:Top]. (eval x = a in <let y ⟵ x in B[y], eval z = a in B[z] + 22, eval w = a in B[w] + 3 + 1> ~ eval x = a in <l\000Cet y ⟵ x in B[y], B[x] + 22, (B[x] + 3) + 1>)
Lemma: test-decide-normalize
∀[a,B:Top].
(case a of inl(_) => a + 1 | inr(y) => B[y] + a ~ case a of inl(x) => (inl x) + 1 | inr(y) => B[y] + (inr y ))
Lemma: test-spread-normalize
∀[a,B:Top]. (let x,y = a in if a is a pair then B[a] otherwise 2 ~ let x,y = a in B[<x, y>])
Lemma: test-cform-normalize
∀[a,B:Top].
(if a is a pair then <B[if a is a pair then 1 otherwise 2]
, B[if a = Ax then 3 otherwise if a is lambda then 3
otherwise if a is an integer then 3
else if a is an atom then 3
otherwise isatom1(a;3;isatom2(a;3;4))]
> otherwise B[if a is a pair then 1 otherwise 2] ~ if a is a pair then <B[1], B[4]> otherwise B[2\000C])
Lemma: test2-cform-normalize
∀[a,B:Top].
(if a is lambda then <B[if a is lambda then 1 otherwise 2]
, B[if a = Ax then 3 otherwise if a is a pair then 3
otherwise if a is an integer then 3
else if a is an atom then 3
otherwise isatom1(a;3;isatom2(a;3;4))]
> otherwise B[if a is lambda then 1 otherwise 2] ~ if a is lambda then <B[1], B[4]> otherwise B[2\000C])
Lemma: test3-cform-normalize
∀[a,B:Top].
(if a is inl then <B[if a is inl then 1
else 2]
, B[if a = Ax then 3 otherwise if a is a pair then 3
otherwise if a is an integer then 3
else if a is an atom then 3
otherwise isatom1(a;3;isatom2(a;3;4))]
>
else B[if a is inl then 1
else 2] ~ if a is inl then <B[1], B[4]>
else B[2])
Lemma: test4-cform-normalize
∀[a,B:Top].
(if a is an integer then <B[if a is an integer then 1
else 2]
, B[if a = Ax then 3 otherwise if a is a pair then 3 otherwise if a is lambda then 3
otherwise if a is an atom
then 3 otherwise 4]
>
else B[if a is an integer then 1
else 2] ~ if a is an integer then <B[1], B[4]>
else B[2])
Lemma: test5-cform-normalize
∀[a,B:Top].
(if a is an atom then <B[if a is an atom then 1 otherwise 2]
, B[if a = Ax then 3 otherwise if a is a pair then 3 otherwise if a is lambda then 3
otherwise if a is an integer
3
else 4]
> otherwise B[if a is an atom then 1 otherwise 2] ~ if a is an atom then <B[1], B[4]> otherwise \000CB[2])
Lemma: cbva-intro-test3
∀x:ℤ. {y:ℤ| x * x < y}
Lemma: lifting-callbyvalueall-pair
∀[a,b,B:Top]. (let x ⟵ <a, b> in B[x] ~ let x ⟵ a in let y ⟵ b in B[<x, y>])
Lemma: lifting-callbyvalueall-inl
∀[a,B:Top]. (let x ⟵ inl a in B[x] ~ let x ⟵ a in B[inl x])
Lemma: lifting-callbyvalueall-inr
∀[a,B:Top]. (let x ⟵ inr a in B[x] ~ let x ⟵ a in B[inr x ])
Lemma: lifting-apply-callbyvalueall
∀[a,B,c:Top]. (let x ⟵ a in B[x] c ~ let x ⟵ a in B[x] c)
Lemma: normalization-callbyvalueall-spread1
∀[F,G,H,a:Top].
(let x ⟵ a
in F[x] let u,v = x in H[x;u;v] let y ⟵ u in G[x;u;v;y] ~ let x ⟵ a
in F[x] let u,v = x in H[x;u;v] G[x;u;v;u])
Lemma: normalization-callbyvalueall-spread2
∀[F,G,H,a:Top].
(let x ⟵ a
in F[x] let u,v = x in H[x;u;v] let y ⟵ v in G[x;u;v;y] ~ let x ⟵ a
in F[x] let u,v = x in H[x;u;v] G[x;u;v;v])
Lemma: iteration_terminates
∀[T:Type]
∀f:T ⟶ T. ∀m:T ⟶ ℕ.
∀x:T. ∃n:ℕ. ((f (f^n x)) = (f^n x) ∈ T)
supposing ∀x:T. (((m (f x)) ≤ (m x)) ∧ (f x) = x ∈ T supposing (m (f x)) = (m x) ∈ ℤ)
Definition: assoc
(basic):: Assoc(T;op) == ∀[x,y,z:T]. ((x op (y op z)) = ((x op y) op z) ∈ T)
Lemma: assoc_wf
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. (Assoc(T;op) ∈ ℙ)
Lemma: sq_stable__assoc
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. SqStable(Assoc(T;op))
Definition: comm
(basic):: Comm(T;op) == ∀[x,y:T]. ((x op y) = (y op x) ∈ T)
Lemma: comm_wf
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. (Comm(T;op) ∈ ℙ)
Lemma: sq_stable__comm
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. SqStable(Comm(T;op))
Definition: inverse
(basic):: Inverse(T;op;id;inv) == ∀[x:T]. (((x op (inv x)) = id ∈ T) ∧ (((inv x) op x) = id ∈ T))
Lemma: inverse_wf
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T]. (Inverse(T;op;id;inv) ∈ ℙ)
Lemma: sq_stable__inverse
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T]. SqStable(Inverse(T;op;id;inv))
Lemma: Dickson's lemma
∀p:ℕ. ∀A:ℕp ⟶ ℕ ⟶ ℕ. ∃j:ℕ. ∃i:ℕj. ∀k:ℕp. (A[k;i] ≤ A[k;j])
Lemma: fixpoint_ub
∀j:ℕ. ∀G:Top. (G^j ⊥ ≤ fix(G))
Home
Index