_Logic and Proof_, Solutions to Selected Exercises from Chaper 15 Using Chapter 16 Machinery

Exercise 15.3.lean

-- Exercise 15.3, second part

import data.set
open function set

variable {R : Type}

variables f g : R → R

constant lt : R → R → Prop
notation x₁ < x₂ := lt x₁ x₂


example
  (h1 : ∀ x₁ x₂ : R, (x₁ < x₂) → f x₁ < f x₂)
      -- f is strictly increasing
  (h2 : injective g)
      -- g is injective
  (h3 : ∀ x, f (g x) = x)
      -- g is a right inverse of f
  (h4 : ∀ x₁ x₂ : R, (   x₁ < x₂ ∧ ¬ x₁ = x₂ ∧ ¬ x₂ < x₁)
                   ∨ ( ¬ x₁ < x₂ ∧   x₁ = x₂ ∧ ¬ x₂ < x₁)
                   ∨ ( ¬ x₁ < x₂ ∧ ¬ x₁ = x₂ ∧   x₂ < x₁))
      -- every x₁ is either <, =, or > every x₂
  : ∀ x₁ x₂ : R, x₁ < x₂ → g x₁ < g x₂ :=
      -- g is strictly increasing
assume x₁ x₂,
show x₁ < x₂ → g x₁ < g x₂,
from classical.by_contradiction (
  assume h5 : ¬ (x₁ < x₂ → g x₁ < g x₂),
  have   h6 : x₁ < x₂ ∧ ¬ g x₁ < g x₂, from sorry,
      -- by ¬ (A → B)  →  A ∧ ¬ B
  have        x₁ < x₂,       from and.left  h6,
  have        ¬ g x₁ < g x₂, from and.right h6,

  have h7 : (   g x₁ < g x₂ ∧ ¬ g x₁ = g x₂ ∧ ¬ g x₂ < g x₁)
          ∨ ( ¬ g x₁ < g x₂ ∧   g x₁ = g x₂ ∧ ¬ g x₂ < g x₁)
          ∨ ( ¬ g x₁ < g x₂ ∧ ¬ g x₁ = g x₂ ∧   g x₂ < g x₁),
    from h4 (g x₁) (g x₂),
  have h8 : g x₁ = g x₂ ∨ g x₂ < g x₁,
  from or.elim h7
    (assume h : g x₁ < g x₂ ∧ ¬ g x₁ = g x₂ ∧ ¬ g x₂ < g x₁,
      show g x₁ = g x₂ ∨ g x₂ < g x₁,
        from false.elim (h6.right h.left))
    (assume h : ( ¬ g x₁ < g x₂ ∧   g x₁ = g x₂ ∧ ¬ g x₂ < g x₁)
              ∨ ( ¬ g x₁ < g x₂ ∧ ¬ g x₁ = g x₂ ∧   g x₂ < g x₁),
      show g x₁ = g x₂ ∨ g x₂ < g x₁,
      from or.elim h
        (assume h : ¬ g x₁ < g x₂ ∧   g x₁ = g x₂ ∧ ¬ g x₂ < g x₁,
          have g x₁ = g x₂, from and.left (and.right h),
          show g x₁ = g x₂ ∨ g x₂ < g x₁,
            from or.inl ‹g x₁ = g x₂›)
        (assume h : ¬ g x₁ < g x₂ ∧ ¬ g x₁ = g x₂ ∧   g x₂ < g x₁,
          have g x₂ < g x₁, from and.right (and.right h),
          show g x₁ = g x₂ ∨ g x₂ < g x₁,
            from or.inr ‹g x₂ < g x₁›)
    ),

  have h9 : (   x₁ < x₂ ∧ ¬ x₁ = x₂ ∧ ¬ x₂ < x₁)
          ∨ ( ¬ x₁ < x₂ ∧   x₁ = x₂ ∧ ¬ x₂ < x₁)
          ∨ ( ¬ x₁ < x₂ ∧ ¬ x₁ = x₂ ∧   x₂ < x₁),
    from h4 x₁ x₂,
  show false,
  from or.elim h8
    (assume : g x₁ = g x₂,
      have x₁ = x₂, from h2 ‹g x₁ = g x₂›,
      show false,
      from or.elim h9
        (assume h : x₁ < x₂ ∧ ¬ x₁ = x₂ ∧ ¬ x₂ < x₁,
          (and.left (and.right h)) ‹x₁ = x₂›)
        (assume h : ( ¬ x₁ < x₂ ∧   x₁ = x₂ ∧ ¬ x₂ < x₁)
                   ∨ ( ¬ x₁ < x₂ ∧ ¬ x₁ = x₂ ∧   x₂ < x₁),
          show false,
          from or.elim h
            (assume h : ¬ x₁ < x₂ ∧   x₁ = x₂ ∧ ¬ x₂ < x₁,
              (and.left h) ‹x₁ < x₂›)
            (assume h : ¬ x₁ < x₂ ∧ ¬ x₁ = x₂ ∧   x₂ < x₁,
              (and.left (and.right h)) ‹x₁ = x₂›)
        )
    )
    (assume : g x₂ < g x₁,
      have h21 : g x₂ < g x₁ → f (g x₂) < f (g x₁),
        from h1 (g x₂) (g x₁),
      have h22 : f (g x₂) < f (g x₁), from h21 ‹g x₂ < g x₁›,
      have x₂ < x₁, from sorry,
  --  from calc
  --    f (g x₂) < f (g x₁) : h22
  --         ... < x₁       : h3 x₁
  --          x₂ < x₁       : h3 x₂,
      show false,
      from or.elim h9
        (assume h : x₁ < x₂ ∧ ¬ x₁ = x₂ ∧ ¬ x₂ < x₁,
          (and.right (and.right h)) ‹x₂ < x₁›)
        (assume h : ( ¬ x₁ < x₂ ∧   x₁ = x₂ ∧ ¬ x₂ < x₁)
                   ∨ ( ¬ x₁ < x₂ ∧ ¬ x₁ = x₂ ∧   x₂ < x₁),
          have ¬ x₁ < x₂,
          from or.elim h
            (assume h : ¬ x₁ < x₂ ∧   x₁ = x₂ ∧ ¬ x₂ < x₁,
              and.left h)
            (assume h : ¬ x₁ < x₂ ∧ ¬ x₁ = x₂ ∧   x₂ < x₁,
              and.left h),
          show false, from ‹¬ x₁ < x₂› ‹x₁ < x₂›
        )
    )
)

Exercise 15.5.lean

-- Exercise 15.5 revisited with the machinery of Chapter 16

import data.set
open function set

variables {X Y : Type}
variable  f : X → Y
variables A B : set X

example : f '' A \ f '' B ⊆ f '' (A \ B) :=
assume y,
assume h1 : y ∈ f '' A \ f '' B,
have h2 : y ∈ f '' A ∧ y ∉ f '' B, from h1,
have lemma_A : y ∈ f '' A, from and.left  h2,
have h3 : ¬ (y ∈ f '' B),  from and.right h2,
have h4 : ¬ ∃ x, (x ∈ B ∧ f x = y), from h3,
have lemma_B : ∀ x, ¬ (x ∈ B ∧ f x = y), from (
  assume x,
  assume h5 : x ∈ B ∧ f x = y,
  h4 (show ∃ x, (x ∈ B ∧ f x = y), from exists.intro x h5)
),
exists.elim lemma_A $
assume x0,
assume h6 : x0 ∈ A ∧ f x0 = y,
have f x0 = y, from and.right h6,
have x0 ∈ A,   from and.left  h6,
have x0 ∉ B,
from (
  assume : x0 ∈ B,
  have h7 : x0 ∈ B ∧ f x0 = y,
    from and.intro ‹x0 ∈ B› ‹f x0 = y›,
  (lemma_B x0) h7
),
have h8 : x0 ∈ A ∧ x0 ∉ B,
  from and.intro ‹x0 ∈ A› ‹x0 ∉ B›,
have      x0 ∈ A \ B, from h8,
show y ∈ f '' (A \ B), from ⟨x0, ‹x0 ∈ A \ B›, ‹f x0 = y›⟩