Lumenary.LogicStatements

Formal library

• and_exampletheoremProved here from basic factsNo axioms

  /-- "12 is even **and** 12 is bigger than 20" is false, because its second part is false.
  "12 is even **and** 12 is smaller than 20" is true, because both parts are true. -/
  theorem and_example : ¬ (12 % 2 = 0 ∧ 12 > 20) ∧ (12 % 2 = 0 ∧ 12 < 20) := by
    decide

  Axioms used: No axiomsformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• or_exampletheoremProved here from basic factsNo axioms

  /-- "Or" is inclusive. "6 is even **or** 6 is a multiple of 3" is true — and both of its parts
  are true. "7 is even or 7 is bigger than 10" is false, because neither part is true. -/
  theorem or_example : (6 % 2 = 0 ∨ 6 % 3 = 0) ∧ ¬ (7 % 2 = 0 ∨ 7 > 10) := by
    decide

  Axioms used: No axiomsformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• not_exampletheoremProved here from basic factsNo axioms

  /-- "Not" swaps true and false. "7 is even" is false, so "7 is **not** even" is true. -/
  theorem not_example : ¬ (7 % 2 = 0) := by
    decide

  Axioms used: No axiomsformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• and_tabletheoremProved here from basic factsNo axioms

  /-- The whole truth table of **and**: `p && q` is true in just one row, the row where both are
  true. -/
  theorem and_table :
      (true && true) = true ∧ (true && false) = false ∧
      (false && true) = false ∧ (false && false) = false := by
    decide

  Axioms used: No axiomsformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• or_tabletheoremProved here from basic factsNo axioms

  /-- The whole truth table of **or**: `p || q` is false in just one row, the row where both are
  false. In the first row both parts are true, and so is `p || q`: this "or" is inclusive. -/
  theorem or_table :
      (true || true) = true ∧ (true || false) = true ∧
      (false || true) = true ∧ (false || false) = false := by
    decide

  Axioms used: No axiomsformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• not_nottheoremProved here from basic factsNo axioms

  /-- "Not not p" is the same as `p`: swapping true and false twice changes nothing. Two rows to
  check. -/
  theorem not_not (p : Bool) : (!!p) = p := by
    cases p <;> rfl

  Axioms used: No axiomsformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• de_morgan_andtheoremProved here from basic factsNo axioms

  /-- **De Morgan's law for "and".** "Not (p and q)" has the same truth value as
  "(not p) or (not q)" in every row. There are only four rows (`cases p <;> cases q`), so
  checking all of them is a complete proof. -/
  theorem de_morgan_and (p q : Bool) : (!(p && q)) = (!p || !q) := by
    cases p <;> cases q <;> rfl

  Axioms used: No axiomsformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• de_morgan_ortheoremProved here from basic factsNo axioms

  /-- **De Morgan's law for "or".** "Not (p or q)" has the same truth value as
  "(not p) and (not q)" in all four rows. -/
  theorem de_morgan_or (p q : Bool) : (!(p || q)) = (!p && !q) := by
    cases p <;> cases q <;> rfl

  Axioms used: No axiomsformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• not_or_ifftheoremProved here from basic factsNo axioms

  /-- The same law for statements (`Prop`), proved by reasoning instead of a table. If neither
  `P` nor `Q` may hold, then `P` fails and `Q` fails; and if both fail, "P or Q" cannot hold. -/
  theorem not_or_iff (P Q : Prop) : ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q :=
    ⟨fun h => ⟨fun hp => h (Or.inl hp), fun hq => h (Or.inr hq)⟩,
     fun ⟨hnp, hnq⟩ h => h.elim hnp hnq⟩

  Axioms used: No axiomsformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• ending_in_two_examplestheoremProved here from basic factsNo axioms

  /-- Five confirming examples: 12, 32, 52, 72 and 92 all end in 2, and all of them are divisible
  by 4. -/
  theorem ending_in_two_examples : ∀ n ∈ [12, 32, 52, 72, 92], n % 10 = 2 ∧ n % 4 = 0 := by
    decide

  Axioms used: No axiomsformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• ending_in_two_counterexampletheoremProved here from basic factsNo axioms

  /-- …and yet "every number that ends in 2 is divisible by 4" is **false**. One counterexample
  is enough: 22 ends in 2, but 22 = 4 × 5 + 2 leaves a remainder. -/
  theorem ending_in_two_counterexample : ¬ ∀ n : Nat, n % 10 = 2 → n % 4 = 0 :=
    fun h => absurd (h 22 rfl) (by decide)

  Axioms used: No axiomsformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• odd_not_always_primetheoremProved here from basic factspropext, Quot.sound

  /-- "Every odd number bigger than 1 is prime" (has no factors except 1 and itself) is false:
  3, 5 and 7 fit, but 9 is odd and has the factor 3. -/
  theorem odd_not_always_prime :
      ¬ ∀ n : Nat, n > 1 → n % 2 = 1 → ∀ d, d ∣ n → d = 1 ∨ d = n := by
    intro h
    have h3 := h 9 (by decide) (by decide) 3 ⟨3, rfl⟩
    omega

  Axioms used: propext, Quot.soundformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• even_prime_existstheoremProved here from basic factspropext, Quot.sound

  /-- A "some" statement needs just one example. "Some number is even and has no factors except 1
  and itself" is true: 2 is such a number. -/
  theorem even_prime_exists : ∃ n : Nat, n % 2 = 0 ∧ n > 1 ∧ ∀ d, d ∣ n → d = 1 ∨ d = n := by
    refine ⟨2, rfl, by decide, fun d hd => ?_⟩
    have hle : d ≤ 2 := Nat.le_of_dvd (by decide) hd
    have hpos : 0 < d := Nat.pos_of_dvd_of_pos hd (by decide)
    omega

  Axioms used: propext, Quot.soundformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• double_checked_to_100theoremProved here from basic factsNo axioms

  /-- Checking 100 cases: for each of the numbers 0, 1, …, 99, the double is even. Lean checks
  the cases one by one. This says nothing yet about 100, or 1000. -/
  theorem double_checked_to_100 : ∀ n, n < 100 → (2 * n) % 2 = 0 := by
    decide

  Axioms used: No axiomsformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• double_is_eventheoremApplies a library theorempropext

  /-- Proving every case at once: for **every** whole number `n`, `2 × n` is even, because
  `2 × n` is `n` groups of 2 with nothing left over. This applies core Lean's
  `Nat.mul_mod_right`. -/
  theorem double_is_even (n : Nat) : (2 * n) % 2 = 0 :=
    Nat.mul_mod_right 2 n

  Axioms used: propextformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• not_all_iff_exists_nottheoremProved here from basic factspropext, Quot.sound

  /-- **The opposite of "all pass" is "at least one fails"** — not "none pass". For any list of
  things and any yes-or-no test `p`: it is *not* true that every item passes exactly when some
  item fails. Proved for every list, by working through the list one item at a time. -/
  theorem not_all_iff_exists_not {α : Type} (items : List α) (p : α → Bool) :
      ¬ (∀ x ∈ items, p x = true) ↔ ∃ x ∈ items, p x = false := by
    induction items with
    | nil => simp
    | cons a as ih =>
      cases h : p a <;> simp [h, ih]

  Axioms used: propext, Quot.soundformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

• not_all_ripetheoremProved here from basic factspropext

  /-- A basket of four mangoes, ripe or not. "All the mangoes are ripe" is false, but "none of the
  mangoes is ripe" is false too: the opposite of "all" is "at least one is not". -/
  theorem not_all_ripe :
      ¬ (∀ ripe ∈ [true, true, false, true], ripe = true) ∧
      ¬ (∀ ripe ∈ [true, true, false, true], ripe = false) ∧
      (∃ ripe ∈ [true, true, false, true], ripe = false) := by
    decide

  Axioms used: propextformal/Lumenary/LogicStatements.leanTry it in the Lean web editor

Formal exercises

Each exercise contains a sorry for you to replace. Open it in the Lean web editor, or clone the repository and run lake build.

/-- Show that "6 is even or 6 is a multiple of 3" is true, and that "7 is even or 7 is bigger
than 10" is false.
Hint: these are statements about small numbers, so Lean can calculate: try `decide`. -/
theorem or_example : (6 % 2 = 0 ∨ 6 % 3 = 0) ∧ ¬ (7 % 2 = 0 ∨ 7 > 10) := by
  sorry

/-- "Or" is inclusive. "6 is even **or** 6 is a multiple of 3" is true — and both of its parts
are true. "7 is even or 7 is bigger than 10" is false, because neither part is true. -/
theorem or_example : (6 % 2 = 0 ∨ 6 % 3 = 0) ∧ ¬ (7 % 2 = 0 ∨ 7 > 10) := by
  decide

/-- Prove De Morgan's law for "or" by checking every row of the truth table.
Hint: `cases p <;> cases q <;> rfl` splits into the four rows and checks each one. -/
theorem de_morgan_or (p q : Bool) : (!(p || q)) = (!p && !q) := by
  sorry

/-- **De Morgan's law for "or".** "Not (p or q)" has the same truth value as
"(not p) and (not q)" in all four rows. -/
theorem de_morgan_or (p q : Bool) : (!(p || q)) = (!p && !q) := by
  cases p <;> cases q <;> rfl

/-- Show that not every number ending in 2 is divisible by 4.
Hint: start with `intro h`. Then `h 22 rfl` says that `22 % 4 = 0`. Is that true? -/
theorem ending_in_two_counterexample : ¬ ∀ n : Nat, n % 10 = 2 → n % 4 = 0 := by
  sorry

/-- …and yet "every number that ends in 2 is divisible by 4" is **false**. One counterexample
is enough: 22 ends in 2, but 22 = 4 × 5 + 2 leaves a remainder. -/
theorem ending_in_two_counterexample : ¬ ∀ n : Nat, n % 10 = 2 → n % 4 = 0 :=
  fun h => absurd (h 22 rfl) (by decide)