Boolean algebra on ZFSet

This file defines the boolean algebra on ZFSet and the type of booleans ZFBool. It defines the following operations:

• not : negation
• and : conjunction
• or : disjunction
• true : ZF true value
• false : ZF false value
• 𝔹 : set of ZF booleans
• toBool : conversion from ZFBool to Bool
• ofBool : conversion from Bool to ZFBool
• equivBool : the equivalence ZFBool ≃ Bool, along which goals are transferred
• equivProp : the classical equivalence ZFBool ≃ Prop, the other reading of ZFBool

ZF Boolean Algebra

@[reducible, inline]

abbrev ZFSet.zffalse : ZFSet.{u_1}

False value defined as the empty set.

Equations

• ZFSet.zffalse = ∅

@[reducible, inline]

abbrev ZFSet.zftrue : ZFSet.{u_1}

True value defined as the singleton containing the empty set.

Equations

• ZFSet.zftrue = {ZFSet.zffalse}

@[reducible, inline]

abbrev ZFSet.𝔹 : ZFSet.{u_1}

Set of ZF booleans, defined as the set containing zffalse and zftrue.

Equations

• ZFSet.𝔹 = {ZFSet.zffalse, ZFSet.zftrue}

@[reducible, inline]

abbrev ZFSet.ZFBool : Type (u_1 + 1)

Type of ZF booleans.

Equations

• ZFSet.ZFBool = ↥ZFSet.𝔹

theorem ZFSet.zftrue_ne_zffalse : zftrue ≠ zffalse

theorem ZFSet.ZFBool.zftrue_mem_𝔹 : zftrue ∈ 𝔹

theorem ZFSet.ZFBool.zffalse_mem_𝔹 : zffalse ∈ 𝔹

theorem ZFSet.ZFBool.𝔹.nonempty : 𝔹 ≠ ∅

@[reducible, inline]

abbrev ZFSet.ZFBool.false : ZFBool

False value, lifted on ZFBool.

Equations

• ZFSet.ZFBool.false = ⟨ZFSet.zffalse, ZFSet.ZFBool.zffalse_mem_𝔹⟩

@[reducible, inline]

abbrev ZFSet.ZFBool.true : ZFBool

True value, lifted on ZFBool.

Equations

• ZFSet.ZFBool.true = ⟨ZFSet.zftrue, ZFSet.ZFBool.zftrue_mem_𝔹⟩

@[implicit_reducible]

instance ZFSet.ZFBool.Bool_top : Top ZFBool

Equations

• ZFSet.ZFBool.Bool_top = { top := ZFSet.ZFBool.true }

@[implicit_reducible]

instance ZFSet.ZFBool.Bool_bot : Bot ZFBool

Equations

• ZFSet.ZFBool.Bool_bot = { bot := ZFSet.ZFBool.false }

@[simp]

theorem ZFSet.ZFBool.top_eq_true : ⊤ = true

@[simp]

theorem ZFSet.ZFBool.bot_eq_false : ⊥ = false

theorem ZFSet.ZFBool.true_ne_false : ⊤ ≠ ⊥

@[simp]

theorem ZFSet.ZFBool.mem_𝔹_iff (p : ZFSet.{u_1}) : p ∈ 𝔹 ↔ p = zffalse ∨ p = zftrue

@[simp]

theorem ZFSet.ZFBool.powerset_false : zffalse.powerset = zftrue

theorem ZFSet.ZFBool.powerset_𝔹_def : 𝔹.powerset = {∅, {zffalse}, {zftrue}, {zffalse, zftrue}}

The enumeration of the powerset of 𝔹.

@[reducible, inline]

abbrev ZFSet.ZFBool.not (p : ZFBool) : ZFBool

Boolean negation, defined as the symmetric difference with true.

Equations

• p.not = ⟨↑ZFSet.ZFBool.true Δ ↑p, ⋯⟩

noncomputable def ZFSet.ZFBool.casesOn {motive : ZFBool → Sort u_2} (p : ZFBool) (false : motive ⊥) (true : motive ⊤) : motive p

Cases elimination for ZFBool.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ZFSet.ZFBool.casesOn_of_false {motive : ZFBool → Sort u_1} (false_case : motive ⊥) (true_case : motive ⊤) : casesOn ⊥ false_case true_case = false_case

Computation rule of casesOn on ⊥.

@[simp]

theorem ZFSet.ZFBool.casesOn_of_true {motive : ZFBool → Sort u_1} (false_case : motive ⊥) (true_case : motive ⊤) : casesOn ⊤ false_case true_case = true_case

Computation rule of casesOn on ⊤.

theorem ZFSet.ZFBool.casesOn_unique {motive : ZFBool → Sort u_1} (false_case : motive ⊥) (true_case : motive ⊤) (g : (p : ZFBool) → motive p) (hfalse : g ⊥ = false_case) (htrue : g ⊤ = true_case) (p : ZFBool) : g p = casesOn p false_case true_case

Uniqueness half of the universal property of ZFBool: casesOn is the only family agreeing with false_case on ⊥ and with true_case on ⊤.

@[reducible, inline]

abbrev ZFSet.ZFBool.and (p q : ZFBool) : ZFBool

Boolean conjunction, defined as set intersection.

Equations

• ⟨Q, hQ⟩ ⋀ ⟨Q_1, hQ_1⟩ = ⟨Q ∩ Q_1, ⋯⟩

def ZFSet.ZFBool.«term_⋀_» : Lean.TrailingParserDescr

Equations

• ZFSet.ZFBool.«term_⋀_» = Lean.ParserDescr.trailingNode `ZFSet.ZFBool.«term_⋀_» 55 55 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋀ ") (Lean.ParserDescr.cat `term 56))

@[reducible, inline]

abbrev ZFSet.ZFBool.or (p q : ZFBool) : ZFBool

Equations

• ⟨Q, hQ⟩ ⋁ ⟨Q_1, hQ_1⟩ = ⟨Q ∪ Q_1, ⋯⟩

def ZFSet.ZFBool.«term_⋁_» : Lean.TrailingParserDescr

Equations

• ZFSet.ZFBool.«term_⋁_» = Lean.ParserDescr.trailingNode `ZFSet.ZFBool.«term_⋁_» 55 55 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋁ ") (Lean.ParserDescr.cat `term 56))

Boolean algebra

@[simp]

theorem ZFSet.ZFBool.not_true_eq_false : ⊤.not = ⊥

@[simp]

theorem ZFSet.ZFBool.not_false_eq_true : ⊥.not = ⊤

theorem ZFSet.ZFBool.and_comm (p q : ZFBool) : p ⋀ q = q ⋀ p

theorem ZFSet.ZFBool.and_assoc (p q r : ZFBool) : p ⋀ q ⋀ r = p ⋀ (q ⋀ r)

@[simp]

theorem ZFSet.ZFBool.and_true (p : ZFBool) : p ⋀ ⊤ = p

@[simp]

theorem ZFSet.ZFBool.and_false (p : ZFBool) : p ⋀ ⊥ = ⊥

theorem ZFSet.ZFBool.and_iff (p q : ZFBool) : p ⋀ q = ⊤ ↔ p = ⊤ ∧ q = ⊤

@[reducible, inline]

abbrev ZFSet.ZFBool.and_intro (p q : ZFBool) : p = ⊤ ∧ q = ⊤ → p ⋀ q = ⊤

Equations

• ⋯ = ⋯

theorem ZFSet.ZFBool.or_comm (p q : ZFBool) : p ⋁ q = q ⋁ p

theorem ZFSet.ZFBool.or_assoc (p q r : ZFBool) : p ⋁ q ⋁ r = p ⋁ (q ⋁ r)

theorem ZFSet.ZFBool.or_true (p : ZFBool) : p ⋁ ⊤ = ⊤

theorem ZFSet.ZFBool.or_false (p : ZFBool) : p ⋁ ⊥ = p

theorem ZFSet.ZFBool.or_iff (p q : ZFBool) : p ⋁ q = ⊤ ↔ p = ⊤ ∨ q = ⊤

@[reducible, inline]

abbrev ZFSet.ZFBool.or_intro (p q : ZFBool) : p = ⊤ ∨ q = ⊤ → p ⋁ q = ⊤

Equations

• ⋯ = ⋯

noncomputable def ZFSet.ZFBool.toBool : ZFBool → Bool

Conversion of ZFBool to Lean.Bool.

Equations

• ZFSet.ZFBool.toBool ⟨Q, hQ⟩ = if h : Q = ZFSet.zftrue then true else if h' : Q = ZFSet.zffalse then false else ⋯.elim

theorem ZFSet.ZFBool.toBool_false : ⊥.toBool = Bool.false

theorem ZFSet.ZFBool.toBool_true : ⊤.toBool = Bool.true

theorem ZFSet.ZFBool.toBool_and (p q : ZFBool) : (p ⋀ q).toBool = (p.toBool && q.toBool)

theorem ZFSet.ZFBool.toBool_or (p q : ZFBool) : (p ⋁ q).toBool = (p.toBool || q.toBool)

theorem ZFSet.ZFBool.toBool_not (p : ZFBool) : (p.not.toBool = Bool.true) = ¬p.toBool = Bool.true

theorem ZFSet.ZFBool.not_top_iff_bot {P : ZFBool} : P ≠ ⊤ ↔ P = ⊥

theorem ZFSet.ZFBool.not_bot_iff_top {P : ZFBool} : P ≠ ⊥ ↔ P = ⊤

def ZFSet.ZFBool.ofBool : Bool → ZFBool

Conversion of Lean.Bool to ZFBool

Equations

• ZFSet.ZFBool.ofBool true = ⟨ZFSet.zftrue, ZFSet.ZFBool.zftrue_mem_𝔹⟩
• ZFSet.ZFBool.ofBool false = ⟨ZFSet.zffalse, ZFSet.ZFBool.zffalse_mem_𝔹⟩

theorem ZFSet.ZFBool.mem_ofBool_𝔹 (b : Bool) : ↑(ofBool b) ∈ 𝔹

theorem ZFSet.ZFBool.sub_ofBool_singleton_𝔹 (b : Bool) : {↑(ofBool b)} ⊆ 𝔹

theorem ZFSet.ZFBool.to_Bool_ofBool (b : Bool) : (ofBool b).toBool = b

theorem ZFSet.ZFBool.of_Bool_toBool (b : ZFBool) : ofBool b.toBool = b

theorem ZFSet.ZFBool.ofBool_decide_eq_true_iff {P : Prop} [Decidable P] : ofBool (decide P) = ⊤ ↔ P

theorem ZFSet.ZFBool.ofBool_decide_eq_false_iff {P : Prop} [Decidable P] : ofBool (decide P) = ⊥ ↔ ¬P

noncomputable def ZFSet.ZFBool.equivBool : ZFBool ≃ Bool

Equations

• ZFSet.ZFBool.equivBool = { toFun := ZFSet.ZFBool.toBool, invFun := ZFSet.ZFBool.ofBool, left_inv := ZFSet.ZFBool.of_Bool_toBool, right_inv := ZFSet.ZFBool.to_Bool_ofBool }

@[implicit_reducible]

instance ZFSet.ZFBool.instCoeBool : Coe Bool ZFBool

Equations

• ZFSet.ZFBool.instCoeBool = { coe := ZFSet.ZFBool.ofBool }

@[implicit_reducible]

noncomputable instance ZFSet.ZFBool.instCoeBool_1 : Coe ZFBool Bool

Equations

• ZFSet.ZFBool.instCoeBool_1 = { coe := ZFSet.ZFBool.toBool }

theorem ZFSet.ZFBool.and_coe (p q : ZFBool) : p ⋀ q = ofBool (p.toBool && q.toBool)

theorem ZFSet.ZFBool.or_coe (p q : ZFBool) : p ⋁ q = ofBool (p.toBool || q.toBool)

theorem ZFSet.ZFBool.not_coe (p : ZFBool) : (p.not.toBool = Bool.true) = ¬p.toBool = Bool.true

theorem ZFSet.ZFBool.and_or_distrib_left (p q r : ZFBool) : p ⋀ (q ⋁ r) = p ⋀ q ⋁ (p ⋀ r)

Transfer to Bool and to Prop

ZFBool is the same type as Bool, through equivBool, and — classically — the same type as Prop, through equivProp. Both readings are available to the transfer tactic:

example (p q : ZFBool) : p ⋀ q = q ⋀ p := by
  transfer ZFBool → Bool =>
    exact Bool.and_comm p q

example (p q : ZFBool) : p ⋀ q = q ⋀ p := by
  transfer ZFBool → Prop using ZFBool.equivProp =>
    exact and_comm

The block is proved in the target type, and closing it closes the goal about ZFBool. Bool is the one registered as a TransferEquiv: the class takes its target as an outParam, so a type has at most one instance, and the Prop reading is asked for with using ZFBool.equivProp (or transfer ZFBool.equivProp => …).

ZFBool carries no algebraic structure, so nothing comes for free from the map_… lemmas of TransferAlgebra: the two constants and the three connectives are stated below, once per reading. Those about the connectives need no_index on their left-hand side, because ZFBool.and, ZFBool.or and ZFBool.not are abbreviations: indexed as they stand, they would be unfolded to the underlying set operations and never fire.

The coercions

A ZFBool read as a proposition is p.toBool = true, the coercion to Bool followed by the coercion of a Bool to a proposition. Both readings need that to travel, so it is brought back to an equation in ZFBool, which the equivalence at hand is then pushed through. The lemma fires before its subterms are visited: rewriting p.toBool into equivBool p first would leave a Bool behind, which is what only one of the two readings wants. A coerced ZFBool that is not compared to anything travels to Bool only, through toBool_eq_equivBool below.

theorem ZFSet.ZFBool.toBool_eq_iff (p : ZFBool) (b : Bool) : p.toBool = b ↔ p = ofBool b

theorem ZFSet.ZFBool.ofBool_inj (b c : Bool) : ofBool b = ofBool c ↔ b = c

theorem ZFSet.ZFBool.ofBool_true : ofBool Bool.true = ⊤

theorem ZFSet.ZFBool.ofBool_false : ofBool Bool.false = ⊥

Transfer to Bool

@[implicit_reducible]

noncomputable instance ZFSet.ZFBool.instTransferEquivBool : TransferEquiv ZFBool Bool

Equivalence used by the transfer tactic to move goals between ZFBool and Bool.

Equations

• ZFSet.ZFBool.instTransferEquivBool = { equiv := ZFSet.ZFBool.equivBool }

theorem ZFSet.ZFBool.toBool_eq_equivBool (p : ZFBool) : p.toBool = equivBool p

A ZFBool left as a Bool is its image under the equivalence.

theorem ZFSet.ZFBool.equivBool_ofBool (b : Bool) : equivBool (ofBool b) = b

theorem ZFSet.ZFBool.equivBool_true : equivBool true = Bool.true

theorem ZFSet.ZFBool.equivBool_false : equivBool false = Bool.false

theorem ZFSet.ZFBool.equivBool_top : equivBool ⊤ = Bool.true

theorem ZFSet.ZFBool.equivBool_bot : equivBool ⊥ = Bool.false

theorem ZFSet.ZFBool.equivBool_and (p q : ZFBool) : equivBool (p ⋀ q) = (equivBool p && equivBool q)

theorem ZFSet.ZFBool.equivBool_or (p q : ZFBool) : equivBool (p ⋁ q) = (equivBool p || equivBool q)

theorem ZFSet.ZFBool.equivBool_not (p : ZFBool) : equivBool p.not = !equivBool p

Transfer to Prop

Classically Bool and Prop are the same type, so ZFBool is Prop as well: equivProp p is the proposition p = ⊤. Under this reading the connectives of ZFBool are the connectives of Prop, and an equation between ZFBools is an equivalence of propositions.

noncomputable def ZFSet.ZFBool.equivProp : ZFBool ≃ Prop

The classical equivalence between ZFBool and Prop: p stands for the proposition that p is ⊤. Not an instance, Bool being the registered target of ZFBool; pass it explicitly, as transfer ZFBool → Prop using ZFBool.equivProp.

Equations

• ZFSet.ZFBool.equivProp = ZFSet.ZFBool.equivBool.trans Equiv.propEquivBool.symm

theorem ZFSet.ZFBool.equivProp_apply (p : ZFBool) : equivProp p = (p.toBool = Bool.true)

theorem ZFSet.ZFBool.equivProp_ofBool (b : Bool) : equivProp (ofBool b) ↔ b = Bool.true

theorem ZFSet.ZFBool.equivProp_top : equivProp ⊤ ↔ True

theorem ZFSet.ZFBool.equivProp_bot : equivProp ⊥ ↔ False

theorem ZFSet.ZFBool.equivProp_true : equivProp true ↔ True

theorem ZFSet.ZFBool.equivProp_false : equivProp false ↔ False

theorem ZFSet.ZFBool.equivProp_and (p q : ZFBool) : equivProp (p ⋀ q) ↔ equivProp p ∧ equivProp q

theorem ZFSet.ZFBool.equivProp_or (p q : ZFBool) : equivProp (p ⋁ q) ↔ equivProp p ∨ equivProp q

theorem ZFSet.ZFBool.equivProp_not (p : ZFBool) : equivProp p.not ↔ ¬equivProp p