Comment: partial types
Here we define the "partial" (or "bar") types first defined by
 Constable, Smith, Crary

They can be defined as quotient types.⋅

Definition: base-partial
base-partial(T) ==  {x:Base| x ∈ supposing (x)↓ ∧ is-exception(x))} 

Lemma: base-partial_wf
[T:Type]. (base-partial(T) ∈ Type)

Lemma: base-partial-not-exception
[T:Type]. ∀[x:base-partial(T)].  is-exception(x))

Definition: per-partial
per-partial(T;x;y) ==  uiff((x)↓;(y)↓) ∧ y ∈ supposing (x)↓

Lemma: per-partial_wf
[T:Type]. ∀[x,y:Base].  (per-partial(T;x;y) ∈ ℙ)

Lemma: per-partial-reflex
[T:Type]. ∀[x:base-partial(T)].  per-partial(T;x;x)

Lemma: per-partial-equiv_rel
[T:Type]. EquivRel(base-partial(T);x,y.per-partial(T;x;y))

Lemma: per-partial-subtype
A,B:Type. ∀a,b:Base.  ((A ⊆B)  per-partial(A;a;b)  per-partial(B;a;b))

Definition: partial
partial(T) ==  x,y:base-partial(T)//per-partial(T;x;y)

Lemma: partial_wf
[T:Type]. (partial(T) ∈ Type)

Lemma: partial-not-exception
[T:Type]. ∀[x:partial(T)].  is-exception(x))

Lemma: inclusion-partial
[T:Type]. T ⊆partial(T) supposing value-type(T)

Lemma: inclusion-partial2
[T:Type]. ∀x:T. (x ∈ partial(T)) supposing value-type(T)

Lemma: subtype_rel_partial
[A,B:Type].  partial(A) ⊆partial(B) supposing A ⊆B

Lemma: base-partial-partial
[A:Type]. (base-partial(partial(A)) ⊆base-partial(A))

Lemma: partial-partial
[A:Type]. (partial(partial(A)) ⊆partial(A))

Lemma: partial-base
partial(Base) ⊆Base

Lemma: subtype_partial_sqtype_base
T:Type. ((T ⊆Base)  (partial(T) ⊆Base))

Lemma: partial_subtype_base
T:Type. ((T ⊆Base)  (partial(T) ⊆Base))

Lemma: has-value_wf-partial
[A:Type]. ∀[a:partial(A)]. ((a)↓ ∈ ℙsupposing value-type(A)

Lemma: base-equal-partial
    b ∈ partial(A) supposing (((a)↓ ⇐⇒ (b)↓) ∧ b ∈ supposing (a)↓) ∧ is-exception(a)) ∧ is-exception(b)) 
  supposing value-type(A)

Lemma: base-member-partial
[A:Type]. ∀[a:Base]. (a ∈ partial(A)) supposing ((¬is-exception(a)) and a ∈ supposing (a)↓supposing value-type(A)

Lemma: bottom_wf-partial
[A:Type]. ⊥ ∈ partial(A) supposing value-type(A)

Lemma: bottom_wf_function
[A:Type]. ∀[B:A ⟶ Type].  ⊥ ∈ a:A ⟶ partial(B[a]) supposing ∀a:A. value-type(B[a])

Lemma: termination-equality-base
[T:Type]. ∀[x,y:Base].  y ∈ supposing (x)↓ ∧ (x y ∈ partial(T)) supposing value-type(T)

Lemma: termination
[T:Type]. ∀[x:partial(T)]. x ∈ supposing (x)↓ supposing value-type(T)

Lemma: termination-equality
[T:Type]. ∀[x,y:partial(T)].  y ∈ supposing (x)↓ ∧ (x y ∈ partial(T)) supposing value-type(T)

Lemma: shorter-proof-of-termination-equality
[T:Type]. ∀[x,y:partial(T)].  y ∈ supposing (x)↓ ∧ (x y ∈ partial(T)) supposing value-type(T)

Lemma: respects-equality-partial
[T:Type]. respects-equality(partial(T);T) supposing value-type(T)

Lemma: even-shorter-proof-of-termination-equality
[T:Type]. ∀[x,y:partial(T)].  y ∈ supposing (x)↓ ∧ (x y ∈ partial(T)) supposing value-type(T)

Lemma: equal-partial
[T:Type]. ∀[x,y:partial(T)].  uiff(x y ∈ partial(T);uiff((x)↓;(y)↓) ∧ ((x)↓  (x y ∈ T))) supposing value-type(T)

Lemma: fix-not-exception
[G,g:Base].  ¬is-exception(G fix(g)) supposing ∀j:ℕis-exception(G (g^j ⊥)))

Lemma: has-value-equality-fix
[T,E,S:Type].  ∀[G:T ⟶ partial(E)]. ∀[g:T ⟶ T].  ((G fix(g))↓ ∈ ℙsupposing value-type(E) ∧ (⊥ ∈ T)

Lemma: fixpoint-induction-bottom-base
E,S:Type. ∀G,g:Base.
  ((G ∈ S ⟶ partial(E))  (g ∈ S ⟶ S)  value-type(E)  mono(E)  (⊥ ∈ S)  (G fix(g) ∈ partial(E)))

Lemma: fixpoint-induction-bottom
  (∀[G:S ⟶ partial(E)]. ∀[g:S ⟶ S].  (G fix(g) ∈ partial(E))) supposing ((⊥ ∈ S) and mono(E) and value-type(E))

Lemma: fixpoint-induction-bottom2
  (∀[G:S ⟶ partial(E)]. ∀[g:S ⟶ S].  (G fix(g) ∈ partial(E))) supposing ((⊥ ∈ S) and mono(E) and value-type(E))

Lemma: fix_wf_partial
[A:Type]. ∀[f:partial(A) ⟶ partial(A)]. (fix(f) ∈ partial(A)) supposing value-type(A) ∧ mono(A)

Lemma: apply-partial
[A:Type]. ∀[B:A ⟶ Type]. ∀[f:partial(a:A ⟶ B[a])]. ∀[a:A].  a ∈ partial(B[a]) supposing value-type(B[a])

Lemma: apply-partial-indep
[A,B:Type]. ∀[f:partial(A ⟶ B)]. ∀[a:A].  a ∈ partial(B) supposing value-type(B)

Lemma: apply-2-partial
     (∀[a:partial(A)]. ∀[b:partial(B)].  (f b ∈ partial(C))) supposing 
        ((∀a:partial(A). ∀b:partial(B).  ((f b)↓  ((a)↓ ∧ (b)↓))) and 
        (∀a:partial(A). ∀b:partial(B).  (((¬is-exception(a)) ∧ is-exception(b)))  is-exception(f b)))) and 
        (f ∈ A ⟶ B ⟶ C))) supposing 
     (value-type(C) and 
     (value-type(B) ∧ (B ⊆Base)) and 
     (value-type(A) ∧ (A ⊆Base)))

Lemma: add-wf-partial
[x,y:partial(Base)].  (x y ∈ partial(ℤ))

Lemma: add-wf-partial-nat
[x,y:partial(ℕ)].  (x y ∈ partial(ℕ))

Lemma: nat-partial-nat
[n:ℕ]. (n ∈ partial(ℕ))

Lemma: subtract-wf-partial
[x,y:partial(Base)].  (x y ∈ partial(ℤ))

Lemma: eq_int-wf-partial
[x,y:partial(Base)].  ((x =z y) ∈ partial(𝔹))

Lemma: eq_int-wf-partial2
[x,y:partial(ℤ)].  ((x =z y) ∈ partial(𝔹))

Lemma: le_int-wf-partial
[x,y:partial(Base)].  (x ≤y ∈ partial(𝔹))

Lemma: le_int-wf-partial2
[x,y:partial(ℤ)].  (x ≤y ∈ partial(𝔹))

Lemma: imax-wf-partial
[x,y:partial(ℤ)].  (imax(x;y) ∈ partial(ℤ))

Lemma: bnot-wf-partial
[b:partial(Base)]. bb ∈ partial(𝔹))

Lemma: band-wf-partial
[a:partial(Base)]. ∀[b:partial(𝔹)].  (a ∧b b ∈ partial(𝔹))

Lemma: no-halt-decider
¬(∃h:partial(ℤ) ⟶ 𝔹(h tt ∧ h ⊥ ff))

Lemma: ifthenelse_wf-partial-base
  (value-type(T)  (∀c1,c2:partial(T). ∀b:Base.  if then c1 else c2 fi  ∈ partial(T) supposing ¬is-exception(b)))

Lemma: ifthenelse_wf-partial
T:Type. (value-type(T)  (∀c1,c2:partial(T). ∀b:partial(𝔹).  (if then c1 else c2 fi  ∈ partial(T))))

Lemma: partial-type-continuous
[X:ℕ ⟶ {T:Type| value-type(T)} ]. ((⋂n:ℕpartial(X[n])) ⊆partial(⋂n:ℕX[n]))

Lemma: no-value-bottom
[T:Type]. ∀[x:partial(T)]. ~ ⊥ supposing ¬(x)↓ supposing value-type(T)

Lemma: partial-void
z:partial(Void). (z ~ ⊥)

Lemma: fix-diverges
f:partial(Void) ⟶ partial(Void). (fix(f) ~ ⊥)

Lemma: strict-fun
[f:Base]. f ∈ partial(Void) ⟶ partial(Void) supposing f ⊥ ~ ⊥

Lemma: fixpoint-induction2
A:Type. ∀T:A ⟶ Type.
  ((A ⊆Base)
   (∀a:A. value-type(T[a]))
   (∀a:A. mono(T[a]))
   (∀f:(a:A ⟶ partial(T[a])) ⟶ a:A ⟶ partial(T[a]) ⋂ Base. (fix(f) ∈ a:A ⟶ partial(T[a]))))

Lemma: add-has-value-partial-nat
[x,y:partial(ℕ)].  {(x ∈ ℤ) ∧ (y ∈ ℤ)} supposing (x y)↓

Lemma: add-has-value-iff
[x,y:partial(ℕ)].  uiff((x y)↓;(x)↓ ∧ (y)↓)

Lemma: no-excluded-middle-using-partial
¬(∀P:ℙ(P ∨ P)))

Lemma: no-excluded-middle-using-partial2
¬(∀P:ℙ((↓P) ∨ P)))

Lemma: no-excluded-middle-squash-using-partial
¬↓∀P:ℙ(P ∨ P))

Lemma: set-axiom-of-choice-is-false

Lemma: strong-subtype-partial
[T:Type]. (value-type(T)  strong-subtype(T;partial(T)))

Lemma: partial-strong-subtype-base
[T:Type]. ((T ⊆Base)  strong-subtype(partial(T);Base))

Definition: approx-type
approx-type(T) ==  pertype(λ2y.approx-per(T;x;y))

Lemma: approx-type_wf
[T:Type]. (approx-type(T) ∈ Type)

Lemma: subtype-approx-type
[T:Type]. T ⊆approx-type(T) supposing mono(T) ∨ (T ⊆Base)

Lemma: member-approx-type
[T:Type]. ∀x:Base. uiff(x ∈ approx-type(T);↓∃t:Base. ((x ≤ t) ∧ (t ∈ T)))

Lemma: bottom-member-approx-type
[T:Type]. (T  (⊥ ∈ approx-type(T)))

Lemma: bottom-pair-member-approx-type
[A,B:Type].  (A   (<⊥, ⊥> ∈ approx-type(A × B)))

Home Index