Theory: partial

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 ∈ T 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)↓) ∧ x = y ∈ T 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 ⊆r 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 ⊆r 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) ⊆r partial(B) supposing A ⊆r B

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

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

Lemma: partial-base
partial(Base) ⊆r Base

Lemma: subtype_partial_sqtype_base
∀T:Type. ((T ⊆r Base) ⇒ (partial(T) ⊆r Base))

Lemma: partial_subtype_base
∀T:Type. ((T ⊆r Base) ⇒ (partial(T) ⊆r Base))

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

Lemma: base-equal-partial
∀[A:Type]
  ∀[a,b:Base].
    a = b ∈ partial(A) supposing (((a)↓ ⇐⇒ (b)↓) ∧ a = b ∈ A 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 ∈ 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].  x = y ∈ T supposing (x)↓ ∧ (x = y ∈ partial(T)) supposing value-type(T)

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

Lemma: termination-equality

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

Lemma: shorter-proof-of-termination-equality

∀[T:Type]. ∀[x,y:partial(T)].  x = y ∈ T 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)].  x = y ∈ T 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
∀[E,S:Type].

  (∀[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
∀[E,S:Type].

  (∀[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].  f a ∈ partial(B[a]) supposing value-type(B[a])

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

Lemma: apply-2-partial
∀[A,B,C:Type].
  (∀[f:Base]
     (∀[a:partial(A)]. ∀[b:partial(B)].  (f a b ∈ partial(C))) supposing
        ((∀a:partial(A). ∀b:partial(B).  ((f a b)↓ ⇒ ((a)↓ ∧ (b)↓))) and
        (∀a:partial(A). ∀b:partial(B).  (((¬is-exception(a)) ∧ (¬is-exception(b))) ⇒ (¬is-exception(f a b)))) and
        (f ∈ A ⟶ B ⟶ C))) supposing
     (value-type(C) and
     (value-type(B) ∧ (B ⊆r Base)) and
     (value-type(A) ∧ (A ⊆r 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 ≤z y ∈ partial(𝔹))

Lemma: le_int-wf-partial2
∀[x,y:partial(ℤ)].  (x ≤z 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 0 = tt ∧ h ⊥ = ff))

Lemma: ifthenelse_wf-partial-base
∀T:Type
  (value-type(T) ⇒ (∀c1,c2:partial(T). ∀b:Base.  if b 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 b then c1 else c2 fi  ∈ partial(T))))

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

Lemma: no-value-bottom
∀[T:Type]. ∀[x:partial(T)]. x ~ ⊥ 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 ⊆r 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
¬Set-AC

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

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

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

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

Lemma: subtype-approx-type
∀[T:Type]. T ⊆r approx-type(T) supposing mono(T) ∨ (T ⊆r 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 ⇒ B ⇒ (<⊥, ⊥> ∈ approx-type(A × B)))

Home Index