Comment: fun_1_summary
Polymorphic identity and composition functions. 
Lemmas covering properties suchas injectivity and 

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
==  λx.(f (g x))

Lemma: compose_wf
[A,B,C:Type]. ∀[f:B ⟶ C]. ∀[g:A ⟶ B].  (f g ∈ A ⟶ C)

Lemma: comb_for_compose_wf
λA,B,C,f,g,z. (f 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 (g f)) ((h g) f) ∈ (A ⟶ D))

Lemma: comp_id_l
[A,B:Type]. ∀[f:A ⟶ B].  ((Id{B} f) f ∈ (A ⟶ B))

Lemma: comp_id_r
[A,B:Type]. ∀[f:A ⟶ B].  ((f Id{A}) f ∈ (A ⟶ B))

Definition: inv_funs
InvFuns(A;B;f;g) ==  ((g f) Id{A} ∈ (A ⟶ A)) ∧ ((f 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 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 ≡  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 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 ∈ ℕ1 ⟶ ℕ1) ∧ Bij(ℕ1;ℕ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 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 f)

Lemma: inject-compose
[T:Type]. ∀[f,g:T ⟶ T].  (Inj(T;T;f 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 f)) supposing (Inj(B;C;g) and Inj(A;B;f))

Definition: fun_exp
f^n ==  primrec(n;λx.x;λi,g. (f 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^n fi )

Lemma: fun_exp_unroll_1
[n:ℕ+]. ∀[f:Top].  (f^n ~ λx.(f (f^n 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 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 h) primrec(n;h;λi,g. (f g)) ∈ (T ⟶ T))

Lemma: fun_exp_add
[T:Type]. ∀[n,m:ℕ]. ∀[f:T ⟶ T].  (f^n (f^n 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 x) ∈ T)

Lemma: fun_exp_add_apply1
[T:Type]. ∀[n:ℕ]. ∀[f:T ⟶ T]. ∀[x:T].  ((f^n (f x)) (f^n x) ∈ T)

Lemma: fun_exp_apply_add1
[T:Type]. ∀[n:ℕ]. ∀[f:T ⟶ T]. ∀[x:T].  ((f (f^n x)) (f^n 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 x.x))

Lemma: fun_exp_add1
[f,x:Top]. ∀[n:ℕ].  (f (f^n x) f^n x)

Lemma: fun_exp_add1_sub
[T:Type]. ∀[f:T ⟶ T]. ∀[x:T]. ∀[n:ℕ+].  ((f (f^n x)) (f^n x) ∈ T)

Lemma: fun_exp_compose2
[A,B:Type]. ∀[h:A ⟶ A]. ∀[n:ℕ].  g.(g h)^n g.(g h^n)) ∈ ((A ⟶ B) ⟶ A ⟶ B))

Lemma: fun_exp_add_sq
[n,m:ℕ]. ∀[f,i:Top].  (f^n f^n (f^m i))

Lemma: fun_exp_add-sq
[n,m:ℕ]. ∀[f,x:Top].  (f^n f^n (f^m x))

Lemma: fun_exp_add1-sq
[n:ℕ]. ∀[f,x:Top].  (f (f^n x) f^n x)

Lemma: fun_exp_add1-sq2
[n:ℕ]. ∀[f,x:Top].  (f^n (f x) f^n 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)

Lemma: fun_exp-increasing
[T:Type]. ((T ⊆r ℤ (∀f:T ⟶ T. ((∀n:T. n < n)  (∀n:T. ∀i,j:ℕ.  (i <  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 x))

Lemma: evalall-sqequal
[x:Base]. evalall(x) supposing (evalall(x))↓

Lemma: evalall-sqle
[x:Base]. evalall(x) ≤ supposing (evalall(x))↓

Lemma: evalall-sqequal2
[x:Base]. evalall(x) supposing (evalall(x))↓

Lemma: evalall-reduce
[T:Type]. ∀[t:T].  evalall(t) supposing valueall-type(T)

Lemma: evalall-equal
[T:Type]. ∀[t:T].  evalall(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 then else fi if 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 ⟵ in x ∈ supposing valueall-type(T)

Lemma: cbva-intro-test
[T:Type]. ∀x:T. supposing valueall-type(T)

Lemma: cbv-intro-test
[T:Type]. ∀x:T. supposing value-type(T)

Lemma: test-cbva-normalize
[a,B:Top].  (let x ⟵ in <let y ⟵ in B[y], let z ⟵ in B[z] 22, eval in B[w] 1> let x ⟵ in <B\000C[x], B[x] 22, (B[x] 3) 1>)

Lemma: test-cbv-normalize
[a,B:Top].  (eval in <let y ⟵ in B[y], eval in B[z] 22, eval in B[w] 1> eval in <l\000Cet y ⟵ in B[y], B[x] 22, (B[x] 3) 1>)

Lemma: test-decide-normalize
  (case of inl(_) => inr(y) => B[y] case of inl(x) => (inl x) inr(y) => B[y] (inr ))

Lemma: test-spread-normalize
[a,B:Top].  (let x,y in if is pair then B[a] otherwise let x,y in B[<x, y>])

Lemma: test-cform-normalize
  (if is pair then <B[if is pair then otherwise 2]
                       B[if Ax then otherwise if is lambda then 3
                                                      otherwise if is an integer then 3
                                                                else if is an atom then 3
                                                                     otherwise isatom1(a;3;isatom2(a;3;4))]
                       > otherwise B[if is pair then otherwise 2] if is pair then <B[1], B[4]> otherwise B[2\000C])

Lemma: test2-cform-normalize
  (if is lambda then <B[if is lambda then otherwise 2]
                       B[if Ax then otherwise if is pair then 3
                                                      otherwise if is an integer then 3
                                                                else if is an atom then 3
                                                                     otherwise isatom1(a;3;isatom2(a;3;4))]
                       > otherwise B[if is lambda then otherwise 2] if is lambda then <B[1], B[4]> otherwise B[2\000C])

Lemma: test3-cform-normalize
  (if is inl then <B[if is inl then 1
                       else 2]
                    B[if Ax then otherwise if is pair then 3
                                                   otherwise if is an integer then 3
                                                             else if is an atom then 3
                                                                  otherwise isatom1(a;3;isatom2(a;3;4))]
   else B[if is inl then 1
          else 2] if is inl then <B[1], B[4]>
                    else B[2])

Lemma: test4-cform-normalize
  (if is an integer then <B[if is an integer then 1
                              else 2]
                           B[if Ax then otherwise if is pair then otherwise if is lambda then 3
                                                                                          otherwise if is an atom
                                                                                                    then otherwise 4]
   else B[if is an integer then 1
          else 2] if is an integer then <B[1], B[4]>
                    else B[2])

Lemma: test5-cform-normalize
  (if is an atom then <B[if is an atom then otherwise 2]
                        B[if Ax then otherwise if is pair then otherwise if is lambda then 3
                                                                                       otherwise if is an integer
                                                                                                 else 4]
                        > otherwise B[if is an atom then otherwise 2] if is an atom then <B[1], B[4]> otherwise \000CB[2])

Lemma: cbva-intro-test3
x:ℤ{y:ℤx < y} 

Lemma: lifting-callbyvalueall-pair
[a,b,B:Top].  (let x ⟵ <a, b> in B[x] let x ⟵ in let y ⟵ in B[<x, y>])

Lemma: lifting-callbyvalueall-inl
[a,B:Top].  (let x ⟵ inl in B[x] let x ⟵ in B[inl x])

Lemma: lifting-callbyvalueall-inr
[a,B:Top].  (let x ⟵ inr a  in B[x] let x ⟵ in B[inr ])

Lemma: lifting-apply-callbyvalueall
[a,B,c:Top].  (let x ⟵ in B[x] let x ⟵ in B[x] c)

Lemma: normalization-callbyvalueall-spread1
  (let x ⟵ a
   in F[x] let u,v in H[x;u;v] let y ⟵ in G[x;u;v;y] let x ⟵ a
                                                              in F[x] let u,v in H[x;u;v] G[x;u;v;u])

Lemma: normalization-callbyvalueall-spread2
  (let x ⟵ a
   in F[x] let u,v in H[x;u;v] let y ⟵ in G[x;u;v;y] let x ⟵ a
                                                              in F[x] let u,v in H[x;u;v] G[x;u;v;v])

Lemma: iteration_terminates
  ∀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 ∈ 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