---

Comment: bool_1_summary
Definitions, theorems and tactics for the boolean 
type and boolean-related expressions.

Comment: bool_1_intro
Definitions, theorems, and tactics for boolean type
and standard boolean operators.

Theorems include standard logic ones, as well
as `assert' theorems for converting between boolean 
and prop-valued predicates.

This implementation of bool differs from that in Nuprl V3.
There, the booleans were defined as a subtype of the integers.
Here, the use of the Unit + Unit type enables evaluation
of boolean expressions, especially those involving 
ifthenelse, using Nuprl's direct computation rules. This
is of great help when these expressions are used in 
definitions of recursive functions, whose proof of 
well-formedness relies heavily on direct-computation-style
reasoning.  

 

Comment: BOOL_DEFS
=================
BASIC DEFINITIONS
=================

Definition: exposed-btrue
exposed-btrue ==  inl ⋅

Definition: exposed-bfalse
exposed-bfalse ==  inr ⋅ 

Lemma: bool_sq
SQType(𝔹)

Lemma: bool_sim_true
∀[b:𝔹]. b ~ tt supposing b = tt

Lemma: bool_sim_false
∀[b:𝔹]. b ~ ff supposing b = ff

Lemma: assert_witness
∀[b:𝔹]. ((↑b) ⇒ (Ax ∈ ↑b))

Lemma: comb_for_assert_wf
λb,z. (↑b) ∈ b:𝔹 ⟶ (↓True) ⟶ ℙ

Lemma: ifthenelse-wf
∀[b:𝔹]. ∀[A:Type]. ∀[p:⋂v:↑b. A]. ∀[q:⋂v:¬↑b. A].  (if b then p else q fi  ∈ A)

Definition: band
p ∧b q ==  if p then q else ff fi 

Definition: bor
p ∨bq ==  if p then tt else q fi 

Lemma: btrue_neq_bfalse
¬tt = ff

Lemma: band_wf
∀[p,q:𝔹].  (p ∧b q ∈ 𝔹)

Lemma: bor_wf
∀[p,q:𝔹].  (p ∨bq ∈ 𝔹)

Lemma: band_ff
∀[u:𝔹]. (u ∧b ff ~ ff)

Lemma: band_tt
∀[u:𝔹]. (u ∧b tt ~ u)

Lemma: bor_ff_simp
∀[u:𝔹]. u ∨bff = u

Lemma: bor_tt_simp
∀[u:𝔹]. u ∨btt = tt

Lemma: band_ff_simp
∀[u:𝔹]. u ∧b ff = ff

Lemma: band_tt_simp
∀[u:𝔹]. u ∧b tt = u

Lemma: bnot_bnot
∀[p:Top]. (¬b¬bp ~ p ∧b tt)

Lemma: bnot_bnot_elim
∀[p:𝔹]. ¬b¬bp = p

Lemma: band_assoc
∀[a,b,c:Top].  ((a ∧b b) ∧b c ~ a ∧b b ∧b c)

Lemma: band_commutes
∀[a,b:𝔹].  a ∧b b = b ∧b a

Lemma: bor_assoc
∀[a,b,c:Top].  ((a ∨bb) ∨bc ~ a ∨bb ∨bc)

Lemma: bor_band_distributive
∀[a,b,c:Top].  (a ∨b(b ∧b c) ~ (a ∨bb) ∧b (a ∨bc))

Lemma: band_bor_distributive
∀[a,b,c:Top].  (a ∧b (b ∨bc) ~ (a ∧b b) ∨b(a ∧b c))

Lemma: bor_band_absorption
∀[a,b:Top].  (a ∧b (a ∨bb) ~ a ∧b tt)

Lemma: band_bor_absorption
∀[a,b:Top].  (a ∨b(a ∧b b) ~ a ∧b tt)

Lemma: band_bnot
∀[a:Top]. (a ∧b (¬ba) ~ a ∧b ff)

Lemma: bor_bnot
∀[a:Top]. (a ∨b(¬ba) ~ a ∨btt)

Lemma: bnot_thru_band
∀[p,q:Top].  (¬b(p ∧b q) ~ (¬bp) ∨b(¬bq))

Lemma: bnot_thru_bor
∀[p,q:Top].  (¬b(p ∨bq) ~ (¬bp) ∧b (¬bq))

Lemma: bnot_of_le_int
∀[i,j:ℤ].  ¬bi ≤z j = j <z i

Lemma: bnot_of_lt_int
∀[i,j:ℤ].  ¬bi <z j = j ≤z i

Definition: b2i
b2i(b) ==  if b then 1 else 0 fi 

Lemma: b2i_wf
∀[b:𝔹]. (b2i(b) ∈ ℤ)

Lemma: comb_for_b2i_wf
λb,z. b2i(b) ∈ b:𝔹 ⟶ (↓True) ⟶ ℤ

Lemma: b2i_bounds
∀[b:𝔹]. ((0 ≤ b2i(b)) ∧ (b2i(b) ≤ 1))

Lemma: comb_for_bnot_wf
λb,z. (¬bb) ∈ b:𝔹 ⟶ (↓True) ⟶ 𝔹

Lemma: comb_for_bor_wf
λp,q,z. (p ∨bq) ∈ p:𝔹 ⟶ q:𝔹 ⟶ (↓True) ⟶ 𝔹

Lemma: comb_for_band_wf
λp,q,z. (p ∧b q) ∈ p:𝔹 ⟶ q:𝔹 ⟶ (↓True) ⟶ 𝔹

Definition: eq_bool
p =b q ==  (p ∧b q) ∨b((¬bp) ∧b (¬bq))

Lemma: eq_bool_wf
∀[p,q:𝔹].  (p =b q ∈ 𝔹)

Definition: bxor
p ⊕b q ==  (p ∧b (¬bq)) ∨b((¬bp) ∧b q)

Lemma: bxor_wf
∀[p,q:𝔹].  (p ⊕b q ∈ 𝔹)

Definition: bimplies
p ⇒b q ==  (¬bp) ∨bq

Lemma: bimplies_wf
∀[p:𝔹]. ∀[q:𝔹 supposing ↑p].  (p ⇒b q ∈ 𝔹)

Lemma: comb_for_bimplies_wf
λp,q,z. (p ⇒b q) ∈ p:𝔹 ⟶ q:𝔹 supposing ↑p ⟶ (↓True) ⟶ 𝔹

Definition: rev_bimplies
p ⇐b q ==  q ⇒b p

Lemma: rev_bimplies_wf
∀[p,q:𝔹].  (p ⇐b q ∈ 𝔹)

Comment: bool_thms
================
GENERAL THEOREMS
================

Lemma: bool_ind
∀[P:𝔹 ⟶ ℙ]. (P[ff] ⇒ P[tt] ⇒ {∀b:𝔹. P[b]})

Lemma: decidable__equal_bool
∀a,b:𝔹.  Dec(a = b)

Lemma: bimplies_weakening
∀[u,v:𝔹].  ↑(u ⇒b v) supposing u = v

Lemma: bimplies_transitivity
∀[u,v,w:𝔹].  (↑(u ⇒b w)) supposing ((↑(v ⇒b w)) and (↑(u ⇒b v)))

Lemma: assert_functionality_wrt_bimplies
∀[u,v:𝔹].  {↑v supposing ↑u} supposing ↑(u ⇒b v)

Lemma: assert_functionality_wrt_uiff
∀[u,v:𝔹].  {uiff(↑u;↑v)} supposing u = v

Comment: bool_tactics_1
=========================  TACTICS USED IN `ASSERT' =========================================

Lemma: iff_imp_equal_bool
∀[a,b:𝔹].  a = b supposing ↑a ⇐⇒ ↑b

Lemma: equal_bool_if
∀[a,b:𝔹].  (a = b) supposing ((¬((↑a) ∧ (¬↑b))) and (¬((¬↑a) ∧ (↑b))))

Lemma: assert_equal
∀[a,b:𝔹].  uiff((↑a) = (↑b) ∈ Type;↑a ⇐⇒ ↑b)

Lemma: ifthenelse_functionality_wrt_uimplies
∀b1,b2:𝔹.
  ∀[p1,q1,p2,q2:ℙ].
    (b1 = b2
    ⇒ {q2 supposing q1}
    ⇒ {p2 supposing p1}
    ⇒ {if b2 then p2 else q2 fi  supposing if b1 then p1 else q1 fi })

Lemma: ifthenelse_functionality_wrt_implies
∀b1,b2:𝔹.
  ∀[p1,q1,p2,q2:ℙ].  (b1 = b2 ⇒ {q1 ⇒ q2} ⇒ {p1 ⇒ p2} ⇒ {if b1 then p1 else q1 fi  ⇒ if b2 then p2 else q2 fi })

Lemma: ifthenelse_functionality_wrt_iff
∀b1,b2:𝔹.
  ∀[p1,q1,p2,q2:ℙ].
    (b1 = b2 ⇒ {q1 ⇐⇒ q2} ⇒ {p1 ⇐⇒ p2} ⇒ {if b1 then p1 else q1 fi  ⇐⇒ if b2 then p2 else q2 fi })

Lemma: ifthenelse_functionality_wrt_rev_implies
∀b1,b2:𝔹.
  ∀[p1,q1,p2,q2:ℙ].  (b1 = b2 ⇒ {q1 ⇐ q2} ⇒ {p1 ⇐ p2} ⇒ {if b1 then p1 else q1 fi  ⇐ if b2 then p2 else q2 fi })

Lemma: ifthenelse_functionality_wrt_uimplies2
∀b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 = b2 ⇒ {q2 supposing q1} ⇒ {if b1 then p else q1 fi  ⇒ if b2 then p else q2 fi })

Lemma: ifthenelse_functionality_wrt_implies2
∀b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 = b2 ⇒ {q1 ⇒ q2} ⇒ {if b1 then p else q1 fi  ⇒ if b2 then p else q2 fi })

Lemma: ifthenelse_functionality_wrt_iff2
∀b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 = b2 ⇒ {q1 ⇐⇒ q2} ⇒ {if b1 then p else q1 fi  ⇐⇒ if b2 then p else q2 fi })

Lemma: ifthenelse_functionality_wrt_implies3
∀b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 = b2 ⇒ {q1 ⇒ q2} ⇒ {if b1 then q1 else p fi  ⇒ if b2 then q2 else p fi })

Lemma: ifthenelse_functionality_wrt_iff3
∀b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 = b2 ⇒ {q1 ⇐⇒ q2} ⇒ {if b1 then q1 else p fi  ⇐⇒ if b2 then q2 else p fi })

Lemma: ifthenelse_functionality_wrt_rev_implies2
∀b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 = b2 ⇒ {q1 ⇐ q2} ⇒ {if b1 then p else q1 fi  ⇐ if b2 then p else q2 fi })

Lemma: ifthenelse_functionality_wrt_rev_implies3
∀b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 = b2 ⇒ {q1 ⇐ q2} ⇒ {if b1 then q1 else p fi  ⇐ if b2 then q2 else p fi })

Lemma: ifthenelse_functionality_wrt_uimplies3
∀b1,b2:𝔹.  ∀[p,q1,q2:ℙ].  (b1 = b2 ⇒ {q2 supposing q1} ⇒ {if b1 then q1 else p fi  ⇒ if b2 then q2 else p fi })

Lemma: eq_atom-reflexive
∀[x:Atom]. x =a x = tt

Lemma: neg_assert_of_eq_int
∀[x,y:ℤ].  uiff(¬↑(x =z y);x ≠ y)

Lemma: neg_assert_of_eq_atom
∀[x,y:Atom].  uiff(¬↑x =a y;x ≠ y ∈ Atom )

Comment: assert_eqint_rw
The assert_eq_int_rw object is now redundant. However, it
is still referenced in at least the rational library.
⋅

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

Lemma: assert_of_eq_bool
∀[p,q:𝔹].  uiff(↑p =b q;p = q)

Lemma: assert-bnot
∀[p:𝔹]. ((↑¬bp) ⇒ (¬↑p))

Lemma: assert_of_band
∀p:𝔹. ∀q:⋂:↑p. 𝔹.  uiff(↑(p ∧b q);(↑p) ∧ (↑q))

Lemma: assert_of_bor
∀p:𝔹. ∀[q:𝔹]. uiff(↑(p ∨bq);(↑p) ∨ (↑q))

Lemma: assert_of_bimplies
∀[p:𝔹]. ∀[q:𝔹 supposing ↑p].  uiff(↑(p ⇒b q);↑q supposing ↑p)

Comment: bool_tactics
=======================
TACTICS AND CONVERSIONS
=======================

Lemma: ite_rw_false
∀[T:Type]. ∀[b:𝔹]. ∀[x,y:T].  if b then x else y fi  = y ∈ T supposing ¬↑b

Lemma: ite_rw_true
∀[T:Type]. ∀[b:𝔹]. ∀[x,y:T].  if b then x else y fi  = x ∈ T supposing ↑b

Lemma: fun_thru_ite
∀[S,T:Type]. ∀[f:S ⟶ T]. ∀[b:𝔹]. ∀[p,q:S].  ((f if b then p else q fi ) = if b then f p else f q fi  ∈ T)

Comment: old_bool_1_stuff
=========
OLD STUFF
=========
Obselete tactics and theorems that are maybe used in
old proofs.

Lemma: eq_int_eq_false
∀[i,j:ℤ].  (i =z j) = ff supposing i ≠ j

Lemma: eq_int_eq_true
∀[i,j:ℤ].  (i =z j) = tt supposing i = j ∈ ℤ

Lemma: eq_int_eq_false_elim
∀[i,j:ℤ].  i ≠ j supposing (i =z j) = ff

Lemma: eq_int_eq_true_elim
∀[i,j:ℤ].  i = j ∈ ℤ supposing (i =z j) = tt

Lemma: eq_int_cases_test
∀[A:Type]. ∀x,y:A.  ∀[P:A ⟶ ℙ]. ∀i,j:ℤ.  ((P if (i =z j) then x else y fi ) ⇒ (P if (i =z j) then x else y fi ))

Lemma: comb_for_lt_int_wf
λi,j,z. i <z j ∈ i:ℤ ⟶ j:ℤ ⟶ (↓True) ⟶ 𝔹

Lemma: assert-pushdown-test
∀C:𝔹. ↑((C ∧b C) ∨bC) supposing ↑(C ∧b C)

Lemma: subtype_rel_b-union
∀[A1,B1,A2,B2:Type].  (A1 ⋃ B1) ⊆r (A2 ⋃ B2) supposing (A1 ⊆r A2) ∧ (B1 ⊆r B2)

Lemma: subtype_rel_b-union-left
∀[A,B:Type].  (A ⊆r (A ⋃ B))

Lemma: subtype_rel_b-union-right
∀[A,B:Type].  (B ⊆r (A ⋃ B))

Lemma: subtype_rel_union_left
∀[A,B:Type].  (A ⊆r (A ⋃ B))

Lemma: subtype_rel_union_right
∀[A,B:Type].  (B ⊆r (A ⋃ B))

Lemma: subtype_rel_b-union_iff
∀[A,B,C:Type].  uiff((B ⋃ C) ⊆r A;(B ⊆r A) ∧ (C ⊆r A))

Definition: isect2
T1 ⋂ T2 ==  ⋂b:𝔹. if b then T1 else T2 fi 

Lemma: isect2_wf
∀[T1,T2:Type].  (T1 ⋂ T2 ∈ Type)

Lemma: isect2_decomp
∀[t1,t2:Type]. ∀[x:t1 ⋂ t2].  ((x ∈ t1) ∧ (x ∈ t2))

Lemma: subtype_rel_isect2
∀[A,B,C:Type].  uiff(A ⊆r B ⋂ C;(A ⊆r B) ∧ (A ⊆r C))

Lemma: isect2_subtype_rel
∀[A,B:Type].  (A ⋂ B ⊆r A)

Lemma: isect2_subtype_rel2
∀[A,B:Type].  (A ⋂ B ⊆r B)

Lemma: isect2_subtype_rel3
∀[A,B,C:Type].  A ⋂ B ⊆r C supposing (A ⊆r C) ∨ (B ⊆r C)

Lemma: isect_prod_lemma
∀[A,B,C:Type].  (A × B ⋂ A × C ⊆r (A × B ⋂ C))

Definition: b-isect
b-isect(T1;T2) ==  ⋂b:⇃(𝔹). if b then T1 else T2 fi 

Definition: pair-blex
pair-blex(eq;Ra;Rb) ==  λx,y. ((Ra (fst(x)) (fst(y))) ∨b((eq (fst(x)) (fst(y))) ∧b (Rb (snd(x)) (snd(y)))))

Lemma: pair-blex_wf
∀[A,B:Type]. ∀[eq,Ra:A ⟶ A ⟶ 𝔹]. ∀[Rb:B ⟶ B ⟶ 𝔹].  (pair-blex(eq;Ra;Rb) ∈ (A × B) ⟶ (A × B) ⟶ 𝔹)

Definition: dcdr-to-bool
[d]b ==  case d of inl(x) => inl ⋅ | inr(x) => inr ⋅ 

Lemma: dcdr-to-bool_wf
∀[P:ℙ]. ∀[d:Dec(P)].  ([d]b ∈ 𝔹)

Lemma: dcdr-to-bool-equivalence
∀[P:ℙ]. ∀d:Dec(P). (↑[d]b ⇐⇒ P)

Lemma: ite-bool-1
∀[b:𝔹]. ∀[x:Top].  (if b then x else tt fi  ~ (¬bb) ∨bx)

Lemma: ite-bool-2
∀[b:𝔹]. ∀[x:Top].  (if b then x else ff fi  ~ b ∧b x)

Lemma: ite-bool-3
∀[b:𝔹]. ∀[x:Top].  (if b then tt else x fi  ~ b ∨bx)

Lemma: ite-bool-4
∀[b:𝔹]. ∀[x:Top].  (if b then ff else x fi  ~ (¬bb) ∧b x)

Lemma: bor-bfalse
∀[b:𝔹]. (b ∨bff ~ b)

Lemma: bor-btrue
∀[b:𝔹]. (b ∨btt ~ tt)

Lemma: band-btrue
∀[b:𝔹]. (b ∧b tt ~ b)

Lemma: band-bfalse
∀[b:𝔹]. (b ∧b ff ~ ff)

Lemma: band-simplify
∀[b:𝔹]. ∀[f:Top].  (b ∧b f[b] ~ b ∧b f[tt])

Lemma: band-idempotent
∀[b:𝔹]. (b ∧b b ~ b)

Lemma: bor-simplify
∀[b:𝔹]. ∀[f:Top].  (b ∨bf[b] ~ b ∨bf[ff])

Lemma: bor-assoc
∀[b:𝔹]. ∀[c,d:Top].  (b ∨bc ∨bd ~ (b ∨bc) ∨bd)

Lemma: bor-inl
∀[a,b:Top].  ((inl a) ∨bb ~ tt)

Lemma: bor-inr
∀[a,b:Top].  ((inr a ) ∨bb ~ b)

Lemma: band-inl
∀[a,b:Top].  ((inl a) ∧b b ~ b)

Lemma: band-inr
∀[a,b:Top].  ((inr a ) ∧b b ~ ff)

Lemma: testxxx_lemma
∀b:Top. (tt ∨bb ~ tt)

Lemma: ifthenelse-inl
∀[a,b,c:Top].  (if inl a then b else c fi  ~ b)

Lemma: ifthenelse-inr
∀[a,b,c:Top].  (if inr a  then b else c fi  ~ c)

Lemma: bnot-inl
∀[a:Top]. (¬b(inl a) ~ ff)

Lemma: bnot-inr
∀[a:Top]. (¬b(inr a ) ~ tt)

Lemma: free-from-atom-bool
∀[a:Atom1]. ∀[n:𝔹].  a#n:𝔹

Lemma: free-from-atom-bool-subtype
∀[a:Atom1]. ∀[T:Type].  ∀[n:T]. a#n:T supposing T ⊆r 𝔹

Lemma: has-value-bor
∀[a,b:Base].  (a)↓ supposing (a ∨bb)↓

Lemma: has-value-bor-type
∀[a,b:Base].  a ∈ Top + Top supposing (a ∨bb)↓

Lemma: has-value-band
∀[a,b:Base].  (a)↓ supposing (a ∧b b)↓

Lemma: has-value-band-type
∀[a,b:Base].  a ∈ Top + Top supposing (a ∧b b)↓

Lemma: has-value-ifthenelse
∀[a,b,c:Base].  (a)↓ supposing (if a then b else c fi )↓

Lemma: has-value-ifthenelse-type
∀[a,b,c:Base].  a ∈ Top + Top supposing (if a then b else c fi )↓

Lemma: has-value-bnot
∀[a:Base]. (a)↓ supposing (¬ba)↓

Lemma: has-value-bnot-type
∀[a:Base]. a ∈ Top + Top supposing (¬ba)↓

Lemma: band-is-inl
∀[a,b:Top + Top]. ∀[c:Top].  (a ~ inl outl(a)) ∧ (b ~ inl outl(b)) supposing (a ∧b b) = (inl c) ∈ (Top + Top)

Lemma: band-is-inl-base
∀[a,b:Base].
  ∀[c:Top]. (a ~ inl outl(a)) ∧ (b ~ inl outl(b)) supposing (a ∧b b) = (inl c) ∈ (Top + Top) 
  supposing a ∧b b ∈ Top + Top

Lemma: band-sqequal-inl
∀[a,b,c:Base].  {(a ~ inl outl(a)) ∧ (b ~ inl outl(b))} supposing a ∧b b ~ inl c

Lemma: simple_fan_theorem
∀[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])) ⇒ (∃k:ℕ [(∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f])]) supposing ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])

Lemma: simple_fan_theorem-ext
∀[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])) ⇒ (∃k:ℕ [(∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f])]) supposing ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])

Definition: b-exists
(∃i<n.P[i])_b ==  primrec(n;ff;λi,x. (P[i] ∨bx))

Lemma: b-exists_wf
∀[n:ℕ]. ∀[P:ℕn ⟶ 𝔹].  ((∃i<n.P[i])_b ∈ 𝔹)

Lemma: assert-b-exists
∀n:ℕ. ∀P:ℕn ⟶ 𝔹.  (↑(∃i<n.P[i])_b ⇐⇒ ∃i:ℕn. (↑P[i]))

Lemma: b-exists-bfalse
∀[n:ℕ]. ((∃x<n.ff)_b ~ ff)

Definition: bdd-all
bdd-all(n;i.P[i]) ==  primrec(n;tt;λi,x. (P[i] ∧b x))

Lemma: bdd-all_wf
∀[n:ℕ]. ∀[P:ℕn ⟶ 𝔹].  (bdd-all(n;i.P[i]) ∈ 𝔹)

Lemma: bdd-all-btrue
∀[n:ℕ]. (bdd-all(n;x.tt) ~ tt)

Lemma: assert-bdd-all
∀n:ℕ. ∀P:ℕn ⟶ 𝔹.  (↑bdd-all(n;i.P[i]) ⇐⇒ ∀i:ℕn. (↑P[i]))

Lemma: not-assert-bdd-all
∀n:ℕ. ∀P:ℕn ⟶ 𝔹.  (¬↑bdd-all(n;i.P[i]) ⇐⇒ ∃i:ℕn. (¬↑P[i]))

Lemma: bdd_all_zero_lemma
∀P:Top. (bdd-all(0;x.P[x]) ~ tt)

Lemma: ifthenelse-simplify0
∀[b:𝔹]. ∀[x,y:Top].  (if b then x[b] else y[b] fi  ~ if b then x[tt] else y[ff] fi )

Lemma: ifthenelse-simplify1
∀[b,c:𝔹]. ∀[x,y:Top].  (if b then if c then x else y fi  else y fi  ~ if b ∧b c then x else y fi )

Lemma: ifthenelse-simplify2
∀[b,c:𝔹]. ∀[x,y:Top].  (if b then x if c then x else y fi  ~ if b ∨bc then x else y fi )

Lemma: ifthenelse-simplify3
∀[b:𝔹]. (if b then tt else ff fi  ~ b)

Lemma: ifthenelse-prop
∀b:𝔹. ∀p,q:ℙ'.  (if b then p else q fi  ⇐⇒ ((↑b) ∧ p) ∨ ((¬↑b) ∧ q))

Lemma: ifthenelse-false-left
∀b:𝔹. ∀[q:ℙ]. (if b then False else q fi  ⇐⇒ (¬↑b) ∧ q)

Lemma: ifthenelse-false-right
∀b:𝔹. ∀[q:ℙ]. (if b then q else False fi  ⇐⇒ (↑b) ∧ q)

Lemma: apply-ifthenelse
∀[T,U:Type]. ∀[f:T ⟶ U]. ∀[b:𝔹]. ∀[x,y:T].  (f[if b then x else y fi ] ~ if b then f[x] else f[y] fi )

Lemma: apply-ifthenelse2
∀[T1,U1,T2,U2:Type]. ∀[x:T1]. ∀[y:T2]. ∀[b:𝔹]. ∀[f:if b then T1 ⟶ U1 else T2 ⟶ U2 fi ].
  (f[if b then x else y fi ] ~ if b then f[x] else f[y] fi )

Lemma: apply-ifthenelse-pi1
∀[T1,U1,T2,U2:Type]. ∀[x:T1 × U1]. ∀[y:T2 × U2]. ∀[b:𝔹].
  (fst(if b then x else y fi ) ~ if b then fst(x) else fst(y) fi )

Lemma: apply-ifthenelse-pi1-eq
∀[T1,U1,T2,U2:Type]. ∀[x:T1 × U1]. ∀[y:T2 × U2]. ∀[b:𝔹].
  ((fst(if b then x else y fi )) = if b then fst(x) else fst(y) fi  ∈ if b then T1 else T2 fi )

Lemma: apply-ifthenelse-pi2
∀[T1,U1,T2,U2:Type]. ∀[x:T1 × U1]. ∀[y:T2 × U2]. ∀[b:𝔹].
  (snd(if b then x else y fi ) ~ if b then snd(x) else snd(y) fi )

Lemma: apply-ifthenelse-pi2-eq
∀[T1,U1,T2,U2:Type]. ∀[x:T1 × U1]. ∀[y:T2 × U2]. ∀[b:𝔹].
  ((snd(if b then x else y fi )) = if b then snd(x) else snd(y) fi  ∈ if b then U1 else U2 fi )

Definition: imax
imax(a;b) ==  eval a = a in eval b = b in   if a ≤z b then b else a fi 

Lemma: imax_wf
∀[a,b:ℤ].  (imax(a;b) ∈ ℤ)

Lemma: imax_unfold
∀[a,b:ℤ].  (imax(a;b) = if a ≤z b then b else a fi  ∈ ℤ)

Lemma: imax_nat
∀[a:ℤ]. ∀[b:ℕ].  (imax(a;b) ∈ ℕ)

Lemma: simple_fan_theorem'
∀[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])) ⇒ (∃k:ℕ [(∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f])]) supposing ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])

Definition: FAN
FAN(d) ==  bar_recursion(d;λn,s,f. 1;λn,s,f. (imax(f tt;f ff) + 1);0;λm.eval x = m in ⊥)

Lemma: simple_fan_theorem'-ext
∀[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])) ⇒ (∃k:ℕ [(∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f])]) supposing ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])

Lemma: FAN_wf
∀[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  ∀[d:∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])]. (FAN(d) ∈ {k:ℕ| ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]} ) supposing ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])

Lemma: less-as-ifthenelse
∀[r,s,x,y:Top].  (if (r) < (s)  then x  else y ~ if r <z s then x else y fi )

Lemma: int_eq-as-ifthenelse
∀[r,s,x,y:Top].  (if r=s then x else y ~ if (r =z s) then x else y fi )

Lemma: ifthenelse-as-bor
∀[b:𝔹]. ∀[x:Top].  (if b then tt else x fi  ~ b ∨bx)

Lemma: ifthenelse-as-bor
∀[b:𝔹]. ∀[x:Top].  (if b then tt else x fi  ~ b ∨bx)

Lemma: ifthenelse-as-bor-bnot
∀[b:𝔹]. ∀[x:Top].  (if b then x else tt fi  ~ (¬bb) ∨bx)

Lemma: ifthenelse-as-band
∀[b:𝔹]. ∀[x:Top].  (if b then x else ff fi  ~ b ∧b x)

Lemma: ifthenelse-as-band-bnot
∀[b:𝔹]. ∀[x:Top].  (if b then ff else x fi  ~ (¬bb) ∧b x)



Home Index