1. Prelude🔗

Definition1.1

Group: Notational conventions and elementary Boolean / predicate scaffolding used throughout Hehner's A Practical Theory of Programming . The book's Section 1.0 calls this Binary Theory ; its laws (reference §11.3.1) are formalized in the Lean module LaPToP.BasicTheories.Binary . (6)

Group member previews

Preview

Theorem 1.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 7

Reverse dependency previews

Preview

Theorem 1.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Expressions in LaPToP evaluate in a Boolean domain. We write \top for true and \bot for false, and treat predicates as Boolean-valued expressions over a state.

Hehner calls this Binary Theory: binary expressions take the values \top (a theorem) and \bot (an antitheorem), with operators \neg, \land, \lor, \Rightarrow, \Leftarrow, =, \neq, and \mathbf{if}\ a\ \mathbf{then}\ b\ \mathbf{else}\ c. In Lean a binary value is a Bool (Binary), \top and \bot are true and false, and the operators are !, &&, ||, Binary.imp, Binary.rimp, ==, !=, and bif … then … else …. The step from binary expressions to predicates over program state is taken later, in Definition 1.7.

Lean code for Definition1.1●5 definitions

abbrevdefined in LaPToP/BasicTheories/Binary.lean

complete

abbrev LaPToP.BasicTheories.Binary : Type

abbrev LaPToP.BasicTheories.Binary : Type

A *binary* value (aPToP §1.0): `⊤` or `⊥`, modelled as `Bool`.

abbrevdefined in LaPToP/BasicTheories/Binary.lean

complete

abbrev LaPToP.BasicTheories.Binary.top : LaPToP.BasicTheories.Binary

abbrev LaPToP.BasicTheories.Binary.top :
  LaPToP.BasicTheories.Binary

`⊤`, the binary value "top", the theorem.

abbrevdefined in LaPToP/BasicTheories/Binary.lean

complete

abbrev LaPToP.BasicTheories.Binary.bot : LaPToP.BasicTheories.Binary

abbrev LaPToP.BasicTheories.Binary.bot :
  LaPToP.BasicTheories.Binary

`⊥`, the binary value "bottom", the antitheorem.

abbrevdefined in LaPToP/BasicTheories/Binary.lean

complete

abbrev LaPToP.BasicTheories.Binary.imp (a b : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary

abbrev LaPToP.BasicTheories.Binary.imp
  (a b : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary

`a ⇒ b`, implication ("if `a` then `b`"): `¬a ∨ b`.

abbrevdefined in LaPToP/BasicTheories/Binary.lean

complete

abbrev LaPToP.BasicTheories.Binary.rimp (a b : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary

abbrev LaPToP.BasicTheories.Binary.rimp
  (a b : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary

`a ⇐ b`, reverse implication ("`a` if `b`"): `b ⇒ a`.

Theorem1.2

Group member previews

Preview

Definition 1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

OwnerEric HehnerEffortsmallPriorityhighTagspreludeboolean

For every Boolean b, either b or \neg b holds: b \lor \neg b. This is the classical excluded-middle sanity check for Definition 1.1.

Lean code for Theorem1.2●1 theorem

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.excluded_middle
  (a : LaPToP.BasicTheories.Binary) : (a || !a) = true

theorem LaPToP.BasicTheories.Binary.excluded_middle
  (a : LaPToP.BasicTheories.Binary) :
  (a || !a) = true

`a ∨ ¬a` (Excluded Middle).

Proof for Theorem 1.2

uses 0

Case-split on b. Each case is immediate.

Lean code for Theorem1.2

theorem boolean_excluded_middle (b : Bool) :
    b = true ∨ b = false := byb:Bool⊢ b = true ∨ b = false
  cases bfalse⊢ false = true ∨ false = falsetrue⊢ true = true ∨ true = false <;>false⊢ false = true ∨ false = falsetrue⊢ true = true ∨ true = false simpAll goals completed! 🐙

Theorem1.3

Group member previews

Preview

Definition 1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

OwnerEric HehnerEffortsmallTagspreludebinaryhehner-11.3.1

The elementary laws of Binary Theory (reference §11.3.1), for binary a, b: Binary \top, \neg\bot, \top \neq \bot; Mirror (a \Leftarrow b) = (b \Rightarrow a); Double Negation \neg\neg a = a; Noncontradiction \neg(a \land \neg a); Base \neg(a \land \bot), a \lor \top, a \Rightarrow \top, \bot \Rightarrow a; Identity \top \land a = a, \bot \lor a = a, (\top \Rightarrow a) = a, (\top = a) = a; Idempotent a \land a = a, a \lor a = a; Reflexive a \Rightarrow a, a = a; Indirect Proof (\neg a \Rightarrow \bot) = a, (\neg a \Rightarrow a) = a; Specialization a \land b \Rightarrow a; Generalization a \Rightarrow a \lor b. Together with Theorem 1.2, these are the laws Hehner uses most in calculations over Definition 1.1.

Lean code for Theorem1.3●22 theorems

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.top_eq :
  LaPToP.BasicTheories.Binary.top = true

theorem LaPToP.BasicTheories.Binary.top_eq :
  LaPToP.BasicTheories.Binary.top = true

`⊤` is a theorem.

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.not_bot :
  (!LaPToP.BasicTheories.Binary.bot) = true

theorem LaPToP.BasicTheories.Binary.not_bot :
  (!LaPToP.BasicTheories.Binary.bot) =
    true

`¬⊥` is a theorem.

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.top_ne_bot :
  (LaPToP.BasicTheories.Binary.top != LaPToP.BasicTheories.Binary.bot) =
    true

theorem LaPToP.BasicTheories.Binary.top_ne_bot :
  (LaPToP.BasicTheories.Binary.top !=
      LaPToP.BasicTheories.Binary.bot) =
    true

`⊤ ⧧ ⊥`.

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.rimp_eq_imp
  (a b : LaPToP.BasicTheories.Binary) : a.rimp b = b.imp a

theorem LaPToP.BasicTheories.Binary.rimp_eq_imp
  (a b : LaPToP.BasicTheories.Binary) :
  a.rimp b = b.imp a

`a ⇐ b = b ⇒ a` (Mirror).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.not_not (a : LaPToP.BasicTheories.Binary) :
  (!!a) = a

theorem LaPToP.BasicTheories.Binary.not_not
  (a : LaPToP.BasicTheories.Binary) :
  (!!a) = a

`¬¬a = a` (Double Negation).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.noncontradiction
  (a : LaPToP.BasicTheories.Binary) : (!(a && !a)) = true

theorem LaPToP.BasicTheories.Binary.noncontradiction
  (a : LaPToP.BasicTheories.Binary) :
  (!(a && !a)) = true

`¬(a ∧ ¬a)` (Noncontradiction).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.not_and_bot
  (a : LaPToP.BasicTheories.Binary) :
  (!(a && LaPToP.BasicTheories.Binary.bot)) = true

theorem LaPToP.BasicTheories.Binary.not_and_bot
  (a : LaPToP.BasicTheories.Binary) :
  (!(a &&
        LaPToP.BasicTheories.Binary.bot)) =
    true

`¬(a ∧ ⊥)` (Base).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.or_top (a : LaPToP.BasicTheories.Binary) :
  (a || LaPToP.BasicTheories.Binary.top) = true

theorem LaPToP.BasicTheories.Binary.or_top
  (a : LaPToP.BasicTheories.Binary) :
  (a || LaPToP.BasicTheories.Binary.top) =
    true

`a ∨ ⊤` (Base).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_top (a : LaPToP.BasicTheories.Binary) :
  a.imp LaPToP.BasicTheories.Binary.top = true

theorem LaPToP.BasicTheories.Binary.imp_top
  (a : LaPToP.BasicTheories.Binary) :
  a.imp LaPToP.BasicTheories.Binary.top =
    true

`a ⇒ ⊤` (Base).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.bot_imp (a : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.bot.imp a = true

theorem LaPToP.BasicTheories.Binary.bot_imp
  (a : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.bot.imp a =
    true

`⊥ ⇒ a` (Base).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.top_and (a : LaPToP.BasicTheories.Binary) :
  (LaPToP.BasicTheories.Binary.top && a) = a

theorem LaPToP.BasicTheories.Binary.top_and
  (a : LaPToP.BasicTheories.Binary) :
  (LaPToP.BasicTheories.Binary.top && a) =
    a

`⊤ ∧ a = a` (Identity).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.bot_or (a : LaPToP.BasicTheories.Binary) :
  (LaPToP.BasicTheories.Binary.bot || a) = a

theorem LaPToP.BasicTheories.Binary.bot_or
  (a : LaPToP.BasicTheories.Binary) :
  (LaPToP.BasicTheories.Binary.bot || a) =
    a

`⊥ ∨ a = a` (Identity).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.top_imp (a : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.top.imp a = a

theorem LaPToP.BasicTheories.Binary.top_imp
  (a : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.top.imp a =
    a

`⊤ ⇒ a = a` (Identity).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.top_beq (a : LaPToP.BasicTheories.Binary) :
  (LaPToP.BasicTheories.Binary.top == a) = a

theorem LaPToP.BasicTheories.Binary.top_beq
  (a : LaPToP.BasicTheories.Binary) :
  (LaPToP.BasicTheories.Binary.top == a) =
    a

`(⊤ = a) = a` (Identity).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.and_self (a : LaPToP.BasicTheories.Binary) :
  (a && a) = a

theorem LaPToP.BasicTheories.Binary.and_self
  (a : LaPToP.BasicTheories.Binary) :
  (a && a) = a

`a ∧ a = a` (Idempotent).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.or_self (a : LaPToP.BasicTheories.Binary) :
  (a || a) = a

theorem LaPToP.BasicTheories.Binary.or_self
  (a : LaPToP.BasicTheories.Binary) :
  (a || a) = a

`a ∨ a = a` (Idempotent).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_self (a : LaPToP.BasicTheories.Binary) :
  a.imp a = true

theorem LaPToP.BasicTheories.Binary.imp_self
  (a : LaPToP.BasicTheories.Binary) :
  a.imp a = true

`a ⇒ a` (Reflexive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.beq_self (a : LaPToP.BasicTheories.Binary) :
  (a == a) = true

theorem LaPToP.BasicTheories.Binary.beq_self
  (a : LaPToP.BasicTheories.Binary) :
  (a == a) = true

`a = a` (Reflexive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.not_imp_bot
  (a : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (!a) LaPToP.BasicTheories.Binary.bot =
    a

theorem LaPToP.BasicTheories.Binary.not_imp_bot
  (a : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (!a)
      LaPToP.BasicTheories.Binary.bot =
    a

`(¬a ⇒ ⊥) = a` (Indirect Proof).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.not_imp_self
  (a : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (!a) a = a

theorem LaPToP.BasicTheories.Binary.not_imp_self
  (a : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (!a) a =
    a

`(¬a ⇒ a) = a` (Indirect Proof).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.and_imp_left
  (a b : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a && b) a = true

theorem LaPToP.BasicTheories.Binary.and_imp_left
  (a b : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a && b)
      a =
    true

`a ∧ b ⇒ a` (Specialization).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_or_left
  (a b : LaPToP.BasicTheories.Binary) : a.imp (a || b) = true

theorem LaPToP.BasicTheories.Binary.imp_or_left
  (a b : LaPToP.BasicTheories.Binary) :
  a.imp (a || b) = true

`a ⇒ a ∨ b` (Generalization).

Proof for Theorem 1.3

uses 0

Each law is a truth table: case-split on the variables and evaluate (revert …; decide).

Theorem1.4

Group member previews

Preview

Definition 1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

OwnerEric HehnerEffortsmallTagspreludebinaryhehner-11.3.1

The algebraic laws of Binary Theory (reference §11.3.1), for binary a, b, c: Associative for \land, \lor, =, \neq and the mixed (a = (b \neq c)) = ((a = b) \neq c); Symmetry for \land, \lor, =, \neq; Antisymmetry (a \Rightarrow b) \land (b \Rightarrow a) = (a = b); Discharge a \land (a \Rightarrow b) = a \land b, (a \Rightarrow a \land b) = (a \Rightarrow b); Duality \neg(a \land b) = \neg a \lor \neg b, \neg(a \lor b) = \neg a \land \neg b; Exclusion (a \Rightarrow \neg b) = (b \Rightarrow \neg a), (a = \neg b) = (a \neq b) = (\neg a = b); Inclusion (a \Rightarrow b) = \neg a \lor b = (a \land b = a) = (a \lor b = b); Absorption a \land (a \lor b) = a, a \lor (a \land b) = a; Distributive (ten laws, e.g. a \Rightarrow (b \Rightarrow c) = (a \Rightarrow b) \Rightarrow (a \Rightarrow c)); Antidistributive (a \land b \Rightarrow c) = (a \Rightarrow c) \lor (b \Rightarrow c), (a \lor b \Rightarrow c) = (a \Rightarrow c) \land (b \Rightarrow c); Portation (a \land b \Rightarrow c) = (a \Rightarrow (b \Rightarrow c)) = (a \Rightarrow \neg b \lor c); Equality and Difference (a = b) = (a \land b) \lor (\neg a \land \neg b), (a \neq b) = (a \land \neg b) \lor (\neg a \land b). Uses Definition 1.1.

Lean code for Theorem1.4●38 theorems

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.and_assoc
  (a b c : LaPToP.BasicTheories.Binary) :
  (a && (b && c)) = (a && b && c)

theorem LaPToP.BasicTheories.Binary.and_assoc
  (a b c : LaPToP.BasicTheories.Binary) :
  (a && (b && c)) = (a && b && c)

`a ∧ (b ∧ c) = (a ∧ b) ∧ c` (Associative).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.or_assoc
  (a b c : LaPToP.BasicTheories.Binary) :
  (a || (b || c)) = (a || b || c)

theorem LaPToP.BasicTheories.Binary.or_assoc
  (a b c : LaPToP.BasicTheories.Binary) :
  (a || (b || c)) = (a || b || c)

`a ∨ (b ∨ c) = (a ∨ b) ∨ c` (Associative).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.beq_assoc
  (a b c : LaPToP.BasicTheories.Binary) :
  (a == (b == c)) = ((a == b) == c)

theorem LaPToP.BasicTheories.Binary.beq_assoc
  (a b c : LaPToP.BasicTheories.Binary) :
  (a == (b == c)) = ((a == b) == c)

`(a = (b = c)) = ((a = b) = c)` (Associative).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.bne_assoc
  (a b c : LaPToP.BasicTheories.Binary) :
  (a != (b != c)) = ((a != b) != c)

theorem LaPToP.BasicTheories.Binary.bne_assoc
  (a b c : LaPToP.BasicTheories.Binary) :
  (a != (b != c)) = ((a != b) != c)

`a ⧧ (b ⧧ c) = (a ⧧ b) ⧧ c` (Associative).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.beq_bne_assoc
  (a b c : LaPToP.BasicTheories.Binary) :
  (a == (b != c)) = ((a == b) != c)

theorem LaPToP.BasicTheories.Binary.beq_bne_assoc
  (a b c : LaPToP.BasicTheories.Binary) :
  (a == (b != c)) = ((a == b) != c)

`(a = (b ⧧ c)) = ((a = b) ⧧ c)` (Associative).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.and_comm
  (a b : LaPToP.BasicTheories.Binary) : (a && b) = (b && a)

theorem LaPToP.BasicTheories.Binary.and_comm
  (a b : LaPToP.BasicTheories.Binary) :
  (a && b) = (b && a)

`a ∧ b = b ∧ a` (Symmetry).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.or_comm
  (a b : LaPToP.BasicTheories.Binary) : (a || b) = (b || a)

theorem LaPToP.BasicTheories.Binary.or_comm
  (a b : LaPToP.BasicTheories.Binary) :
  (a || b) = (b || a)

`a ∨ b = b ∨ a` (Symmetry).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.beq_comm
  (a b : LaPToP.BasicTheories.Binary) : (a == b) = (b == a)

theorem LaPToP.BasicTheories.Binary.beq_comm
  (a b : LaPToP.BasicTheories.Binary) :
  (a == b) = (b == a)

`(a = b) = (b = a)` (Symmetry).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.bne_comm
  (a b : LaPToP.BasicTheories.Binary) : (a != b) = (b != a)

theorem LaPToP.BasicTheories.Binary.bne_comm
  (a b : LaPToP.BasicTheories.Binary) :
  (a != b) = (b != a)

`a ⧧ b = b ⧧ a` (Symmetry).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_and_imp
  (a b : LaPToP.BasicTheories.Binary) : (a.imp b && b.imp a) = (a == b)

theorem LaPToP.BasicTheories.Binary.imp_and_imp
  (a b : LaPToP.BasicTheories.Binary) :
  (a.imp b && b.imp a) = (a == b)

`(a ⇒ b) ∧ (b ⇒ a) = (a = b)` (Antisymmetry, Double Implication).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.and_imp_self
  (a b : LaPToP.BasicTheories.Binary) : (a && a.imp b) = (a && b)

theorem LaPToP.BasicTheories.Binary.and_imp_self
  (a b : LaPToP.BasicTheories.Binary) :
  (a && a.imp b) = (a && b)

`a ∧ (a ⇒ b) = a ∧ b` (Discharge).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_and_self
  (a b : LaPToP.BasicTheories.Binary) : a.imp (a && b) = a.imp b

theorem LaPToP.BasicTheories.Binary.imp_and_self
  (a b : LaPToP.BasicTheories.Binary) :
  a.imp (a && b) = a.imp b

`a ⇒ (a ∧ b) = a ⇒ b` (Discharge).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.not_and
  (a b : LaPToP.BasicTheories.Binary) : (!(a && b)) = (!a || !b)

theorem LaPToP.BasicTheories.Binary.not_and
  (a b : LaPToP.BasicTheories.Binary) :
  (!(a && b)) = (!a || !b)

`¬(a ∧ b) = ¬a ∨ ¬b` (Duality).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.not_or (a b : LaPToP.BasicTheories.Binary) :
  (!(a || b)) = (!a && !b)

theorem LaPToP.BasicTheories.Binary.not_or
  (a b : LaPToP.BasicTheories.Binary) :
  (!(a || b)) = (!a && !b)

`¬(a ∨ b) = ¬a ∧ ¬b` (Duality).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_not_comm
  (a b : LaPToP.BasicTheories.Binary) : (a.imp !b) = b.imp !a

theorem LaPToP.BasicTheories.Binary.imp_not_comm
  (a b : LaPToP.BasicTheories.Binary) :
  (a.imp !b) = b.imp !a

`(a ⇒ ¬b) = (b ⇒ ¬a)` (Exclusion, Contrapositive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.beq_not
  (a b : LaPToP.BasicTheories.Binary) : (a == !b) = (a != b)

theorem LaPToP.BasicTheories.Binary.beq_not
  (a b : LaPToP.BasicTheories.Binary) :
  (a == !b) = (a != b)

`(a = ¬b) = (a ⧧ b)` (Exclusion).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.bne_eq_not_beq
  (a b : LaPToP.BasicTheories.Binary) : (a != b) = !a == b

theorem LaPToP.BasicTheories.Binary.bne_eq_not_beq
  (a b : LaPToP.BasicTheories.Binary) :
  (a != b) = !a == b

`(a ⧧ b) = (¬a = b)` (Exclusion).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_eq_not_or
  (a b : LaPToP.BasicTheories.Binary) : a.imp b = (!a || b)

theorem LaPToP.BasicTheories.Binary.imp_eq_not_or
  (a b : LaPToP.BasicTheories.Binary) :
  a.imp b = (!a || b)

`a ⇒ b = ¬a ∨ b` (Inclusion, Material Implication).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_eq_and_beq
  (a b : LaPToP.BasicTheories.Binary) : a.imp b = ((a && b) == a)

theorem LaPToP.BasicTheories.Binary.imp_eq_and_beq
  (a b : LaPToP.BasicTheories.Binary) :
  a.imp b = ((a && b) == a)

`a ⇒ b = (a ∧ b = a)` (Inclusion).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_eq_or_beq
  (a b : LaPToP.BasicTheories.Binary) : a.imp b = ((a || b) == b)

theorem LaPToP.BasicTheories.Binary.imp_eq_or_beq
  (a b : LaPToP.BasicTheories.Binary) :
  a.imp b = ((a || b) == b)

`a ⇒ b = (a ∨ b = b)` (Inclusion).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.and_or_self
  (a b : LaPToP.BasicTheories.Binary) : (a && (a || b)) = a

theorem LaPToP.BasicTheories.Binary.and_or_self
  (a b : LaPToP.BasicTheories.Binary) :
  (a && (a || b)) = a

`a ∧ (a ∨ b) = a` (Absorption).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.or_and_self
  (a b : LaPToP.BasicTheories.Binary) : (a || a && b) = a

theorem LaPToP.BasicTheories.Binary.or_and_self
  (a b : LaPToP.BasicTheories.Binary) :
  (a || a && b) = a

`a ∨ (a ∧ b) = a` (Absorption).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.and_and_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  (a && (b && c)) = (a && b && (a && c))

theorem LaPToP.BasicTheories.Binary.and_and_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  (a && (b && c)) = (a && b && (a && c))

`a ∧ (b ∧ c) = (a ∧ b) ∧ (a ∧ c)` (Distributive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.and_or_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  (a && (b || c)) = (a && b || a && c)

theorem LaPToP.BasicTheories.Binary.and_or_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  (a && (b || c)) = (a && b || a && c)

`a ∧ (b ∨ c) = (a ∧ b) ∨ (a ∧ c)` (Distributive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.or_and_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  (a || b && c) = ((a || b) && (a || c))

theorem LaPToP.BasicTheories.Binary.or_and_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  (a || b && c) = ((a || b) && (a || c))

`a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c)` (Distributive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.or_or_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  (a || (b || c)) = (a || b || (a || c))

theorem LaPToP.BasicTheories.Binary.or_or_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  (a || (b || c)) = (a || b || (a || c))

`a ∨ (b ∨ c) = (a ∨ b) ∨ (a ∨ c)` (Distributive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.or_imp_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  (a || b.imp c) = LaPToP.BasicTheories.Binary.imp (a || b) (a || c)

theorem LaPToP.BasicTheories.Binary.or_imp_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  (a || b.imp c) =
    LaPToP.BasicTheories.Binary.imp
      (a || b) (a || c)

`a ∨ (b ⇒ c) = (a ∨ b) ⇒ (a ∨ c)` (Distributive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.or_beq_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  (a || b == c) = ((a || b) == (a || c))

theorem LaPToP.BasicTheories.Binary.or_beq_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  (a || b == c) = ((a || b) == (a || c))

`(a ∨ (b = c)) = ((a ∨ b) = (a ∨ c))` (Distributive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_and_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  a.imp (b && c) = (a.imp b && a.imp c)

theorem LaPToP.BasicTheories.Binary.imp_and_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  a.imp (b && c) = (a.imp b && a.imp c)

`a ⇒ (b ∧ c) = (a ⇒ b) ∧ (a ⇒ c)` (Distributive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_or_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  a.imp (b || c) = (a.imp b || a.imp c)

theorem LaPToP.BasicTheories.Binary.imp_or_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  a.imp (b || c) = (a.imp b || a.imp c)

`a ⇒ (b ∨ c) = (a ⇒ b) ∨ (a ⇒ c)` (Distributive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_imp_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  a.imp (b.imp c) = (a.imp b).imp (a.imp c)

theorem LaPToP.BasicTheories.Binary.imp_imp_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  a.imp (b.imp c) =
    (a.imp b).imp (a.imp c)

`a ⇒ (b ⇒ c) = (a ⇒ b) ⇒ (a ⇒ c)` (Distributive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_beq_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  a.imp (b == c) = (a.imp b == a.imp c)

theorem LaPToP.BasicTheories.Binary.imp_beq_distrib
  (a b c : LaPToP.BasicTheories.Binary) :
  a.imp (b == c) = (a.imp b == a.imp c)

`(a ⇒ (b = c)) = ((a ⇒ b) = (a ⇒ c))` (Distributive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.and_imp_antidistrib
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a && b) c = (a.imp c || b.imp c)

theorem LaPToP.BasicTheories.Binary.and_imp_antidistrib
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a && b)
      c =
    (a.imp c || b.imp c)

`(a ∧ b ⇒ c) = (a ⇒ c) ∨ (b ⇒ c)` (Antidistributive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.or_imp_antidistrib
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a || b) c = (a.imp c && b.imp c)

theorem LaPToP.BasicTheories.Binary.or_imp_antidistrib
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a || b)
      c =
    (a.imp c && b.imp c)

`(a ∨ b ⇒ c) = (a ⇒ c) ∧ (b ⇒ c)` (Antidistributive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.and_imp_eq_imp_imp
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a && b) c = a.imp (b.imp c)

theorem LaPToP.BasicTheories.Binary.and_imp_eq_imp_imp
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a && b)
      c =
    a.imp (b.imp c)

`(a ∧ b ⇒ c) = (a ⇒ (b ⇒ c))` (Portation).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.and_imp_eq_imp_not_or
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a && b) c = a.imp (!b || c)

theorem LaPToP.BasicTheories.Binary.and_imp_eq_imp_not_or
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a && b)
      c =
    a.imp (!b || c)

`(a ∧ b ⇒ c) = (a ⇒ ¬b ∨ c)` (Portation).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.beq_eq_or
  (a b : LaPToP.BasicTheories.Binary) : (a == b) = (a && b || !a && !b)

theorem LaPToP.BasicTheories.Binary.beq_eq_or
  (a b : LaPToP.BasicTheories.Binary) :
  (a == b) = (a && b || !a && !b)

`(a = b) = (a ∧ b) ∨ (¬a ∧ ¬b)` (Equality).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.bne_eq_or
  (a b : LaPToP.BasicTheories.Binary) : (a != b) = (a && !b || !a && b)

theorem LaPToP.BasicTheories.Binary.bne_eq_or
  (a b : LaPToP.BasicTheories.Binary) :
  (a != b) = (a && !b || !a && b)

`(a ⧧ b) = (a ∧ ¬b) ∨ (¬a ∧ b)` (Difference).

Proof for Theorem 1.4

uses 0

Truth tables (revert …; decide); Material Implication is the definition of Binary.imp.

Theorem1.5

Group member previews

Preview

Definition 1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

OwnerEric HehnerEffortsmallTagspreludebinaryhehner-11.3.1

The laws of Binary Theory that license proof steps (reference §11.3.1): Direct Proof (a \Rightarrow b) \land a \Rightarrow b, (a \Rightarrow b) \land \neg b \Rightarrow \neg a, (a \lor b) \land \neg a \Rightarrow b; Transitive for \land, \Rightarrow, = and the mixed forms (a \Rightarrow b) \land (b = c) \Rightarrow (a \Rightarrow c), (a = b) \land (b \Rightarrow c) \Rightarrow (a \Rightarrow c); Antimonotonic (a \Rightarrow b) = (\neg a \Leftarrow \neg b), a \Rightarrow b \Rightarrow ((a \Rightarrow c) \Leftarrow (b \Rightarrow c)); Monotonic a \Rightarrow b \Rightarrow (a \land c \Rightarrow b \land c), a \Rightarrow b \Rightarrow (a \lor c \Rightarrow b \lor c), a \Rightarrow b \Rightarrow ((c \Rightarrow a) \Rightarrow (c \Rightarrow b)); Conflation (a \Rightarrow b) \land (c \Rightarrow d) \Rightarrow (a \land c \Rightarrow b \land d) and the \lor version; Resolution a \land c \Rightarrow (a \lor b) \land (\neg b \lor c) = (a \land \neg b) \lor (b \land c) \Rightarrow a \lor c, stated as its three steps. These justify the monotonicity and antimonotonicity reasoning of Section 1.0.1 and the calculation style of Definition 2.22. Uses Definition 1.1.

Lean code for Theorem1.5●18 theorems

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.modus_ponens
  (a b : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a.imp b && a) b = true

theorem LaPToP.BasicTheories.Binary.modus_ponens
  (a b : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp
      (a.imp b && a) b =
    true

`(a ⇒ b) ∧ a ⇒ b` (Direct Proof, modus ponens).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.modus_tollens
  (a b : LaPToP.BasicTheories.Binary) :
  (LaPToP.BasicTheories.Binary.imp (a.imp b && !b) !a) = true

theorem LaPToP.BasicTheories.Binary.modus_tollens
  (a b : LaPToP.BasicTheories.Binary) :
  (LaPToP.BasicTheories.Binary.imp
      (a.imp b && !b) !a) =
    true

`(a ⇒ b) ∧ ¬b ⇒ ¬a` (Direct Proof, modus tollens).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.or_and_not_imp
  (a b : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp ((a || b) && !a) b = true

theorem LaPToP.BasicTheories.Binary.or_and_not_imp
  (a b : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp
      ((a || b) && !a) b =
    true

`(a ∨ b) ∧ ¬a ⇒ b` (Direct Proof, disjunctive syllogism).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.and_and_trans
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a && b && (b && c)) (a && c) = true

theorem LaPToP.BasicTheories.Binary.and_and_trans
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp
      (a && b && (b && c)) (a && c) =
    true

`(a ∧ b) ∧ (b ∧ c) ⇒ (a ∧ c)` (Transitive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_trans
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a.imp b && b.imp c) (a.imp c) = true

theorem LaPToP.BasicTheories.Binary.imp_trans
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp
      (a.imp b && b.imp c) (a.imp c) =
    true

`(a ⇒ b) ∧ (b ⇒ c) ⇒ (a ⇒ c)` (Transitive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.beq_trans
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a == b && b == c) (a == c) = true

theorem LaPToP.BasicTheories.Binary.beq_trans
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp
      (a == b && b == c) (a == c) =
    true

`(a = b) ∧ (b = c) ⇒ (a = c)` (Transitive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_beq_trans
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a.imp b && b == c) (a.imp c) = true

theorem LaPToP.BasicTheories.Binary.imp_beq_trans
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp
      (a.imp b && b == c) (a.imp c) =
    true

`(a ⇒ b) ∧ (b = c) ⇒ (a ⇒ c)` (Transitive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.beq_imp_trans
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a == b && b.imp c) (a.imp c) = true

theorem LaPToP.BasicTheories.Binary.beq_imp_trans
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp
      (a == b && b.imp c) (a.imp c) =
    true

`(a = b) ∧ (b ⇒ c) ⇒ (a ⇒ c)` (Transitive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_eq_rimp_not
  (a b : LaPToP.BasicTheories.Binary) :
  a.imp b = LaPToP.BasicTheories.Binary.rimp (!a) !b

theorem LaPToP.BasicTheories.Binary.imp_eq_rimp_not
  (a b : LaPToP.BasicTheories.Binary) :
  a.imp b =
    LaPToP.BasicTheories.Binary.rimp (!a)
      !b

`a ⇒ b = ¬a ⇐ ¬b` (Antimonotonic, Contrapositive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_rimp_imp
  (a b c : LaPToP.BasicTheories.Binary) :
  (a.imp b).imp ((a.imp c).rimp (b.imp c)) = true

theorem LaPToP.BasicTheories.Binary.imp_rimp_imp
  (a b c : LaPToP.BasicTheories.Binary) :
  (a.imp b).imp
      ((a.imp c).rimp (b.imp c)) =
    true

`a ⇒ b ⇒ ((a ⇒ c) ⇐ (b ⇒ c))` (Antimonotonic).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_and_right
  (a b c : LaPToP.BasicTheories.Binary) :
  (a.imp b).imp (LaPToP.BasicTheories.Binary.imp (a && c) (b && c)) =
    true

theorem LaPToP.BasicTheories.Binary.imp_and_right
  (a b c : LaPToP.BasicTheories.Binary) :
  (a.imp b).imp
      (LaPToP.BasicTheories.Binary.imp
        (a && c) (b && c)) =
    true

`a ⇒ b ⇒ (a ∧ c ⇒ b ∧ c)` (Monotonic).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_or_right
  (a b c : LaPToP.BasicTheories.Binary) :
  (a.imp b).imp (LaPToP.BasicTheories.Binary.imp (a || c) (b || c)) =
    true

theorem LaPToP.BasicTheories.Binary.imp_or_right
  (a b c : LaPToP.BasicTheories.Binary) :
  (a.imp b).imp
      (LaPToP.BasicTheories.Binary.imp
        (a || c) (b || c)) =
    true

`a ⇒ b ⇒ (a ∨ c ⇒ b ∨ c)` (Monotonic).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_imp_left
  (a b c : LaPToP.BasicTheories.Binary) :
  (a.imp b).imp ((c.imp a).imp (c.imp b)) = true

theorem LaPToP.BasicTheories.Binary.imp_imp_left
  (a b c : LaPToP.BasicTheories.Binary) :
  (a.imp b).imp
      ((c.imp a).imp (c.imp b)) =
    true

`a ⇒ b ⇒ ((c ⇒ a) ⇒ (c ⇒ b))` (Monotonic).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_and_imp_and
  (a b c d : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a.imp b && c.imp d)
      (LaPToP.BasicTheories.Binary.imp (a && c) (b && d)) =
    true

theorem LaPToP.BasicTheories.Binary.imp_and_imp_and
  (a b c d :
    LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp
      (a.imp b && c.imp d)
      (LaPToP.BasicTheories.Binary.imp
        (a && c) (b && d)) =
    true

`(a ⇒ b) ∧ (c ⇒ d) ⇒ (a ∧ c ⇒ b ∧ d)` (Conflation).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.imp_and_imp_or
  (a b c d : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a.imp b && c.imp d)
      (LaPToP.BasicTheories.Binary.imp (a || c) (b || d)) =
    true

theorem LaPToP.BasicTheories.Binary.imp_and_imp_or
  (a b c d :
    LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp
      (a.imp b && c.imp d)
      (LaPToP.BasicTheories.Binary.imp
        (a || c) (b || d)) =
    true

`(a ⇒ b) ∧ (c ⇒ d) ⇒ (a ∨ c ⇒ b ∨ d)` (Conflation).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.resolution_left
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a && c) ((a || b) && (!b || c)) =
    true

theorem LaPToP.BasicTheories.Binary.resolution_left
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a && c)
      ((a || b) && (!b || c)) =
    true

`a ∧ c ⇒ (a ∨ b) ∧ (¬b ∨ c)` (Resolution, first step).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.resolution_middle
  (a b c : LaPToP.BasicTheories.Binary) :
  ((a || b) && (!b || c)) = (a && !b || b && c)

theorem LaPToP.BasicTheories.Binary.resolution_middle
  (a b c : LaPToP.BasicTheories.Binary) :
  ((a || b) && (!b || c)) =
    (a && !b || b && c)

`(a ∨ b) ∧ (¬b ∨ c) = (a ∧ ¬b) ∨ (b ∧ c)` (Resolution, middle step).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.resolution_right
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp (a && !b || b && c) (a || c) = true

theorem LaPToP.BasicTheories.Binary.resolution_right
  (a b c : LaPToP.BasicTheories.Binary) :
  LaPToP.BasicTheories.Binary.imp
      (a && !b || b && c) (a || c) =
    true

`(a ∧ ¬b) ∨ (b ∧ c) ⇒ a ∨ c` (Resolution, last step).

Proof for Theorem 1.5

uses 0

Truth tables (revert …; decide).

Theorem1.6

Group member previews

Preview

Definition 1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

OwnerEric HehnerEffortsmallTagspreludebinaryhehner-11.3.1

The laws for \mathbf{if}\ a\ \mathbf{then}\ b\ \mathbf{else}\ c (reference §11.3.1): Case Creation a = \mathbf{if}\ b\ \mathbf{then}\ b \Rightarrow a\ \mathbf{else}\ \neg b \Rightarrow a (and the \land, =/\neq forms); Case Analysis \mathbf{if}\ a\ \mathbf{then}\ b\ \mathbf{else}\ c = (a \land b) \lor (\neg a \land c) = (a \Rightarrow b) \land (\neg a \Rightarrow c); One Case (six laws, e.g. \mathbf{if}\ a\ \mathbf{then}\ b\ \mathbf{else}\ \top = (a \Rightarrow b)); Case Absorption (six laws, e.g. \mathbf{if}\ a\ \mathbf{then}\ b\ \mathbf{else}\ c = \mathbf{if}\ a\ \mathbf{then}\ a \land b\ \mathbf{else}\ c); Case Distributive \neg\,\mathbf{if}\ a\ \mathbf{then}\ b\ \mathbf{else}\ c = \mathbf{if}\ a\ \mathbf{then}\ \neg b\ \mathbf{else}\ \neg c, (\mathbf{if}\ a\ \mathbf{then}\ b\ \mathbf{else}\ c) \land d = \mathbf{if}\ a\ \mathbf{then}\ b \land d\ \mathbf{else}\ c \land d, and \mathbf{if}\ a\ \mathbf{then}\ b \land c\ \mathbf{else}\ d \land e = (\mathbf{if}\ a\ \mathbf{then}\ b\ \mathbf{else}\ d) \land (\mathbf{if}\ a\ \mathbf{then}\ c\ \mathbf{else}\ e), "and similarly replacing \land by any of \lor = \neq \Rightarrow \Leftarrow" — stated once for an arbitrary binary operator. Uses Definition 1.1.

Lean code for Theorem1.6●22 theorems

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.case_creation_imp
  (a b : LaPToP.BasicTheories.Binary) :
  a = bif b then b.imp a else LaPToP.BasicTheories.Binary.imp (!b) a

theorem LaPToP.BasicTheories.Binary.case_creation_imp
  (a b : LaPToP.BasicTheories.Binary) :
  a =
    bif b then b.imp a
    else
      LaPToP.BasicTheories.Binary.imp (!b)
        a

`a = if b then b ⇒ a else ¬b ⇒ a` (Case Creation).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.case_creation_and
  (a b : LaPToP.BasicTheories.Binary) :
  a = bif b then b && a else !b && a

theorem LaPToP.BasicTheories.Binary.case_creation_and
  (a b : LaPToP.BasicTheories.Binary) :
  a = bif b then b && a else !b && a

`a = if b then b ∧ a else ¬b ∧ a` (Case Creation).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.case_creation_beq
  (a b : LaPToP.BasicTheories.Binary) :
  a = bif b then b == a else b != a

theorem LaPToP.BasicTheories.Binary.case_creation_beq
  (a b : LaPToP.BasicTheories.Binary) :
  a = bif b then b == a else b != a

`a = if b then b = a else b ⧧ a` (Case Creation).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_eq_or
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) = (a && b || !a && c)

theorem LaPToP.BasicTheories.Binary.cond_eq_or
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) =
    (a && b || !a && c)

`if a then b else c = (a ∧ b) ∨ (¬a ∧ c)` (Case Analysis).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_eq_and
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) =
    (a.imp b && LaPToP.BasicTheories.Binary.imp (!a) c)

theorem LaPToP.BasicTheories.Binary.cond_eq_and
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) =
    (a.imp b &&
      LaPToP.BasicTheories.Binary.imp (!a)
        c)

`if a then b else c = (a ⇒ b) ∧ (¬a ⇒ c)` (Case Analysis).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_top_left
  (a b : LaPToP.BasicTheories.Binary) :
  (bif a then LaPToP.BasicTheories.Binary.top else b) = (a || b)

theorem LaPToP.BasicTheories.Binary.cond_top_left
  (a b : LaPToP.BasicTheories.Binary) :
  (bif a then
      LaPToP.BasicTheories.Binary.top
    else b) =
    (a || b)

`if a then ⊤ else b = a ∨ b` (One Case).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_bot_left
  (a b : LaPToP.BasicTheories.Binary) :
  (bif a then LaPToP.BasicTheories.Binary.bot else b) = (!a && b)

theorem LaPToP.BasicTheories.Binary.cond_bot_left
  (a b : LaPToP.BasicTheories.Binary) :
  (bif a then
      LaPToP.BasicTheories.Binary.bot
    else b) =
    (!a && b)

`if a then ⊥ else b = ¬a ∧ b` (One Case).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_top_right
  (a b : LaPToP.BasicTheories.Binary) :
  (bif a then b else LaPToP.BasicTheories.Binary.top) = a.imp b

theorem LaPToP.BasicTheories.Binary.cond_top_right
  (a b : LaPToP.BasicTheories.Binary) :
  (bif a then b
    else
      LaPToP.BasicTheories.Binary.top) =
    a.imp b

`if a then b else ⊤ = a ⇒ b` (One Case).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_bot_right
  (a b : LaPToP.BasicTheories.Binary) :
  (bif a then b else LaPToP.BasicTheories.Binary.bot) = (a && b)

theorem LaPToP.BasicTheories.Binary.cond_bot_right
  (a b : LaPToP.BasicTheories.Binary) :
  (bif a then b
    else
      LaPToP.BasicTheories.Binary.bot) =
    (a && b)

`if a then b else ⊥ = a ∧ b` (One Case).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_not_right
  (a b : LaPToP.BasicTheories.Binary) :
  (bif a then b else !b) = (a == b)

theorem LaPToP.BasicTheories.Binary.cond_not_right
  (a b : LaPToP.BasicTheories.Binary) :
  (bif a then b else !b) = (a == b)

`if a then b else ¬b = (a = b)` (One Case).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_not_left
  (a b : LaPToP.BasicTheories.Binary) :
  (bif a then !b else b) = (a != b)

theorem LaPToP.BasicTheories.Binary.cond_not_left
  (a b : LaPToP.BasicTheories.Binary) :
  (bif a then !b else b) = (a != b)

`if a then ¬b else b = a ⧧ b` (One Case).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_absorb_and
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) = bif a then a && b else c

theorem LaPToP.BasicTheories.Binary.cond_absorb_and
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) =
    bif a then a && b else c

`if a then b else c = if a then a ∧ b else c` (Case Absorption).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_absorb_imp
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) = bif a then a.imp b else c

theorem LaPToP.BasicTheories.Binary.cond_absorb_imp
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) =
    bif a then a.imp b else c

`if a then b else c = if a then a ⇒ b else c` (Case Absorption).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_absorb_beq
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) = bif a then a == b else c

theorem LaPToP.BasicTheories.Binary.cond_absorb_beq
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) =
    bif a then a == b else c

`if a then b else c = if a then a = b else c` (Case Absorption).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_absorb_not_and
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) = bif a then b else !a && c

theorem LaPToP.BasicTheories.Binary.cond_absorb_not_and
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) =
    bif a then b else !a && c

`if a then b else c = if a then b else ¬a ∧ c` (Case Absorption).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_absorb_or
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) = bif a then b else a || c

theorem LaPToP.BasicTheories.Binary.cond_absorb_or
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) =
    bif a then b else a || c

`if a then b else c = if a then b else a ∨ c` (Case Absorption).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_absorb_bne
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) = bif a then b else a != c

theorem LaPToP.BasicTheories.Binary.cond_absorb_bne
  (a b c : LaPToP.BasicTheories.Binary) :
  (bif a then b else c) =
    bif a then b else a != c

`if a then b else c = if a then b else a ⧧ c` (Case Absorption).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.not_cond
  (a b c : LaPToP.BasicTheories.Binary) :
  (!bif a then b else c) = bif a then !b else !c

theorem LaPToP.BasicTheories.Binary.not_cond
  (a b c : LaPToP.BasicTheories.Binary) :
  (!bif a then b else c) =
    bif a then !b else !c

`¬ if a then b else c = if a then ¬b else ¬c` (Case Distributive).

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_op
  (a b c d : LaPToP.BasicTheories.Binary)
  (f :
    LaPToP.BasicTheories.Binary →
      LaPToP.BasicTheories.Binary → LaPToP.BasicTheories.Binary) :
  f (bif a then b else c) d = bif a then f b d else f c d

theorem LaPToP.BasicTheories.Binary.cond_op
  (a b c d : LaPToP.BasicTheories.Binary)
  (f :
    LaPToP.BasicTheories.Binary →
      LaPToP.BasicTheories.Binary →
        LaPToP.BasicTheories.Binary) :
  f (bif a then b else c) d =
    bif a then f b d else f c d

`if a then b else c ∧ d = if a then b ∧ d else c ∧ d` (Case Distributive), for `∧`
and, in the same way, for any binary operator `f`.

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_op_cond
  (a b c d e : LaPToP.BasicTheories.Binary)
  (f :
    LaPToP.BasicTheories.Binary →
      LaPToP.BasicTheories.Binary → LaPToP.BasicTheories.Binary) :
  (bif a then f b c else f d e) =
    f (bif a then b else d) (bif a then c else e)

theorem LaPToP.BasicTheories.Binary.cond_op_cond
  (a b c d e :
    LaPToP.BasicTheories.Binary)
  (f :
    LaPToP.BasicTheories.Binary →
      LaPToP.BasicTheories.Binary →
        LaPToP.BasicTheories.Binary) :
  (bif a then f b c else f d e) =
    f (bif a then b else d)
      (bif a then c else e)

`if a then b ∧ c else d ∧ e = if a then b else d ∧ if a then c else e` (Case
Distributive), for `∧` and, in the same way, for any binary operator `f`.

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_and
  (a b c d : LaPToP.BasicTheories.Binary) :
  ((bif a then b else c) && d) = bif a then b && d else c && d

theorem LaPToP.BasicTheories.Binary.cond_and
  (a b c d :
    LaPToP.BasicTheories.Binary) :
  ((bif a then b else c) && d) =
    bif a then b && d else c && d

The `∧` instance of `cond_op`, as printed in the book.

theoremdefined in LaPToP/BasicTheories/Binary.lean

complete

theorem LaPToP.BasicTheories.Binary.cond_and_cond
  (a b c d e : LaPToP.BasicTheories.Binary) :
  (bif a then b && c else d && e) =
    ((bif a then b else d) && bif a then c else e)

theorem LaPToP.BasicTheories.Binary.cond_and_cond
  (a b c d e :
    LaPToP.BasicTheories.Binary) :
  (bif a then b && c else d && e) =
    ((bif a then b else d) &&
      bif a then c else e)

The `∧` instance of `cond_op_cond`, as printed in the book.

Proof for Theorem 1.6

uses 0

Truth tables (revert …; decide); the generic Case Distributive laws are a case split on the condition followed by rfl.

Definition1.7

Group member previews

Preview

Definition 1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 2

Reverse dependency previews

Preview

Definition 5.1

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

A state assigns values to program variables. Informal specifications and programs are expressions over those variables; refining one specification into another is the central activity of the book.

Lean code for Definition1.7●1 definition

abbrevdefined in LaPToP/ProgramTheory/Specifications.lean

complete

abbrev LaPToP.ProgramTheory.Spec.State.{u, v} (Var : Type u) (Val : Type v) :
  Type (max u v)

abbrev LaPToP.ProgramTheory.Spec.State.{u, v}
  (Var : Type u) (Val : Type v) :
  Type (max u v)

A state as an assignment of values to state variables (aPToP §4): a
function from variable names to values.