---

Comment: union_summary
Non canonical functions (isl, outl, outr) for union type. 

Definition: isl
isl(x) ==  case x of inl(y) => tt | inr(z) => ff

Lemma: isl_wf
∀[A,B:Type]. ∀[x:A + B].  (isl(x) ∈ 𝔹)

Definition: isr
isr(x) ==  case x of inl(y) => ff | inr(z) => tt

Lemma: isr_wf
∀[A,B:Type]. ∀[x:A + B].  (isr(x) ∈ 𝔹)

Lemma: inr-one-one
∀[A,B:Type]. ∀[x,y:B].  uiff((inr x ) = (inr y ) ∈ (A + B);x = y ∈ B)

Lemma: inr-one-one'
∀[A,B:Type]. ∀[x,y:B].  x = y ∈ B supposing (inr x ) = (inr y ) ∈ (A + B)

Lemma: inl-one-one
∀[A,B:Type]. ∀[x,y:A].  uiff((inl x) = (inl y) ∈ (A + B);x = y ∈ A)

Lemma: inl-one-one'
∀[A,B:Type]. ∀[x,y:A].  x = y ∈ A supposing (inl x) = (inl y) ∈ (A + B)

Lemma: inl-inr-disjoint
∀[A,B:Type]. ∀[x:A]. ∀[y:B].  uiff((inl x) = (inr y ) ∈ (A + B);False)

Lemma: inr-inl-disjoint
∀[A,B:Type]. ∀[x:B]. ∀[y:A].  uiff((inr x ) = (inl y) ∈ (A + B);False)

Definition: ifthenelse
if b then t else f fi  ==  case b of inl() => t | inr() => f

Lemma: ifthenelse_wf
∀[b:𝔹]. ∀[A:Type]. ∀[p,q:A].  (if b then p else q fi  ∈ A)

Definition: ifunion
ifunion(b; t) ==  if b then t else t fi 

Lemma: subtype_rel_ifthenelse
∀[b:𝔹]. ∀[A1,A2,B1,B2:Type].
  (if b then A1 else B1 fi  ⊆r if b then A2 else B2 fi ) supposing ((A1 ⊆r A2) and (B1 ⊆r B2))

Definition: assert
↑b ==  if b then True else False fi 

Lemma: assert_wf
∀[b:𝔹]. (↑b ∈ ℙ)

Lemma: istype-assert
∀[b:𝔹]. istype(↑b)

Definition: bnot
¬bb ==  if b then ff else tt fi 

Lemma: bnot_wf
∀[b:𝔹]. (¬bb ∈ 𝔹)

Definition: le_int
i ≤z j ==  ¬bj <z i

Lemma: le_int_wf
∀[i,j:ℤ].  (i ≤z j ∈ 𝔹)

Definition: outl
outl(x) ==  case x of inl(y) => y | inr(z) => ⊥

Lemma: outl_wf
∀[A,B:Type]. ∀[x:A + B].  outl(x) ∈ A supposing ↑isl(x)

Definition: outr
outr(x) ==  case x of inl(y) => ⊥ | inr(z) => z

Lemma: outr_wf
∀[A,B:Type]. ∀[x:A + B].  outr(x) ∈ B supposing ↑¬bisl(x)

Lemma: isr-not-isl
∀x:Top + Top. ((↑isr(x)) ⇒ (isl(x) ~ ff))

Lemma: isl-not-isr
∀x:Top + Top. ((↑isl(x)) ⇒ (isr(x) ~ ff))

Lemma: not-isr-isl
∀x:Top + Top. ((¬↑isr(x)) ⇒ (isl(x) ~ tt))

Lemma: not-isr-assert-isl
∀x:Top + Top. ((¬↑isr(x)) ⇒ (↑isl(x)))

Lemma: not-isl-isr
∀x:Top + Top. ((¬↑isl(x)) ⇒ (isr(x) ~ tt))

Lemma: not-isl-assert-isr
∀x:Top + Top. ((¬↑isl(x)) ⇒ (↑isr(x)))

Lemma: injection-eta
∀d:Top + Top. if isl(d) then d ~ inl outl(d) else d ~ inr outr(d)  fi 

Lemma: inl-eta
∀[x:Top]. ∀d:Top + Top. d ~ inl outl(d) supposing d = (inl x) ∈ (Top + Top)

Lemma: inr-eta
∀[x:Top]. ∀d:Top + Top. d ~ inr outr(d)  supposing d = (inr x ) ∈ (Top + Top)

Lemma: not-inl-sqeq-inr
∀[a,b:Base].  (¬(inl a ~ inr b ))

Lemma: istype-inl-sqeq-inr
∀[a,b:Top].  istype(inl a ~ inr b )

Lemma: istype-inr-sqeq-inl
∀[a,b:Top].  istype(inr b  ~ inl a)

Lemma: union-eta
∀d:Top + Top. ((d ~ inl outl(d)) ∨ (d ~ inr outr(d) ))

Lemma: respects-equality-union
∀[T1,T2,S1,S2:Type].  (respects-equality(S1;T1) ⇒ respects-equality(S2;T2) ⇒ respects-equality(S1 + S2;T1 + T2))

Lemma: not-btrue-sqeq-bfalse
¬(ff ~ tt)

Comment: assert_com
=========================
`ASSERT'-RELATED THEOREMS
=========================

Lemma: assert_of_tt
↑tt

Lemma: assert_of_ff
¬↑ff

Lemma: assert_elim
∀[b:𝔹]. b = tt supposing ↑b

Lemma: not_assert_elim
∀[b:𝔹]. b = ff supposing ¬↑b

Lemma: sqeqtt_to_assert
∀[b:𝔹]. uiff(b ~ tt;↑b)

Lemma: sqeqff_to_assert
∀[b:𝔹]. uiff(b ~ ff;↑¬bb)

Lemma: eqtt_to_assert
∀[b:𝔹]. uiff(b = tt;↑b)

Lemma: eqff_to_assert
∀[b:𝔹]. uiff(b = ff;↑¬bb)

Lemma: decidable__assert
∀b:𝔹. Dec(↑b)

Lemma: assert_of_bnot
∀[p:𝔹]. uiff(↑¬bp;¬↑p)

Lemma: assert_of_eq_int
∀[x,y:ℤ].  uiff(↑(x =z y);x = y ∈ ℤ)

Lemma: assert_of_lt_int
∀[x,y:ℤ].  uiff(↑x <z y;x < y)

Definition: b-union
The union of two types is a special case of the union of a family of types,
where we use the booleans to index the family.⋅

A ⋃ B ==  ⋃x:𝔹.if x then A else B fi 

Lemma: b-union_wf
∀[A,B:Type].  (A ⋃ B ∈ Type)

Lemma: decide-spread-sq1
∀[x:Top × Top]. ∀[f,g,h:Top].  (case let a,b = x in inl f[a;b] of inl(z) => g[z] | inr(z) => h[z] ~ g[f[fst(x);snd(x)]])

Lemma: decide-spread-sq2
∀[x:Top × Top]. ∀[f,g,h:Top].
  (case let a,b = x in inr f[a;b]  of inl(z) => g[z] | inr(z) => h[z] ~ h[f[fst(x);snd(x)]])

Lemma: decide-decide
∀[x:Top + Top]. ∀[f1,f2,g,h:Top].
  (case case x of inl(z) => f1[z] | inr(z) => f2[z] of inl(z) => g[z] | inr(z) => h[z] ~ case x
   of inl(z) =>
   case f1[z] of inl(z) => g[z] | inr(z) => h[z]
   | inr(z) =>
   case f2[z] of inl(z) => g[z] | inr(z) => h[z])

Lemma: decide-decide2
∀[x:Top + Top]. ∀[f1,f2,h:Top].
  (case x of inl(z) => case x of inl(z) => f1[z] | inr(z) => f2[z] | inr(z) => h[z] ~ case x
   of inl(z) =>
   f1[z]
   | inr(z) =>
   h[z])

Lemma: decide-decide3
∀[x:Top + Top]. ∀[f1,f2,h:Top].
  (case x of inl(z) => h[z] | inr(z) => case x of inl(z) => f1[z] | inr(z) => f2[z] ~ case x
   of inl(z) =>
   h[z]
   | inr(z) =>
   f2[z])

Lemma: spread-spread
∀[t:Top × Top]. ∀[P,Q:Top].  (let x,y = let a,b = t in P[a;b] in Q[x;y] ~ let a,b = t in let x,y = P[a;b] in Q[x;y])

Lemma: spread-ifthenelse
∀[b:𝔹]. ∀[f1,f2,x,y:Top].
  (let u,v = x 
   in if b then f1[u;v] else f2[u;v] fi  ~ if b then let u,v = x in f1[u;v] else let u,v = x in f2[u;v] fi )

Lemma: trivial-ifthenelse
∀[b:𝔹]. ∀[f:Top].  (if b then f else f fi  ~ f)

Lemma: decidable__equal_union
∀[A,B:Type].  ((∀x,y:A.  Dec(x = y ∈ A)) ⇒ (∀u,v:B.  Dec(u = v ∈ B)) ⇒ (∀x,y:A + B.  Dec(x = y ∈ (A + B))))



Home Index