logic_and_proof_ch_9_exercises.lean

-- Exercise 1

section
    variable A : Type
    variable f : A → A
    variable P : A → Prop
    variable h : ∀ x, P x → P (f x)
    -- Show the following:
    example : ∀ y, P y → P (f (f y)) :=
    assume y,
    assume Py,
    have Pfy : P (f y), from h y Py,
    show P (f (f y)), from h (f y) Pfy
end

-- Exercise 2

section
    variable U : Type
    variables A B : U → Prop
    example : (∀ x, A x ∧ B x) → ∀ x, A x :=
    assume h1 : (∀ x, A x ∧ B x),
    assume x,
    have AxBx : A x ∧ B x, from h1 x,
    show A x, from and.elim_left AxBx
end

-- Exercise 3

section
    variable U : Type
    variables A B C : U → Prop
    variable h1 : ∀ x, A x ∨ B x
    variable h2 : ∀ x, A x → C x
    variable h3 : ∀ x, B x → C x
    example : ∀ x, C x :=
    assume x,
    or.elim (h1 x)
        (assume Ax, h2 x Ax)
        (assume Bx, h3 x Bx)
end

-- Exercise 4

-- This is an exercise from Chapter 4. Use it as an axiom here.
axiom not_iff_not_self (P : Prop) : ¬ (P ↔ ¬ P)

example (Q : Prop) : ¬ (Q ↔ ¬ Q) :=
    not_iff_not_self Q
section
    variable Person : Type
    variable shaves : Person → Person → Prop
    variable barber : Person
    variable h : ∀ x, shaves barber x ↔ ¬ shaves x x
    -- Show the following:
    example : false :=
    (not_iff_not_self (shaves barber barber)) (h barber)
end

-- Exercise 5

section
    variable U : Type
    variables A B : U → Prop
    example : (∃ x, A x) → ∃ x, A x ∨ B x :=
    assume exAx,
    exists.elim exAx $
    assume x Ax,
    have A x ∨ B x, from or.inl Ax,
    exists.intro x ‹A x ∨ B x›
end

-- Exercise 6

section
    variable U : Type
    variables A B : U → Prop
    variable h1 : ∀ x, A x → B x
    variable h2 : ∃ x, A x
    example : ∃ x, B x :=
    exists.elim h2 $
    assume x Ax,
    exists.intro x (h1 x Ax)
end

-- Exercise 7

section
    variable U : Type
    variables A B C : U → Prop
    example (h1 : ∃ x, A x ∧ B x) (h2 : ∀ x, B x → C x) :
        ∃ x, A x ∧ C x :=
    exists.elim h1 $
    assume x AxBx,
    have A x, from and.elim_left AxBx,
    have B x, from and.elim_right AxBx,
    have C x, from h2 x ‹B x›,
    exists.intro x ⟨‹A x›, ‹C x›⟩
end

-- Exercise 8

section
    variable U : Type
    variables A B C : U → Prop
    example : (¬ ∃ x, A x) → ∀ x, ¬ A x :=
    assume h1 : ¬ ∃ x, A x,
    assume x,
    assume : A x,
    have h2 : ∃ x, A x, from exists.intro x ‹A x›,
    show false, from h1 h2

    example : (∀ x, ¬ A x) → ¬ ∃ x, A x :=
    assume h1 : ∀ x, ¬ A x,
    assume h2 : ∃ x, A x,
    exists.elim h2 $
    assume x (_ : A x),
    have ¬ A x, from h1 x,
    show false, from ‹¬ A x› ‹A x›
end

-- Exercise 9

section
   variable U : Type
   variables R : U → U → Prop
   example : (∃ x, ∀ y, R x y) → ∀ y, ∃ x, R x y :=
   assume h1 : ∃ x, ∀ y, R x y,
   exists.elim h1 $
   assume x (h2 : ∀ y, R x y),
   assume y,
   have R x y, from h2 y,
   exists.intro x ‹R x y›
end

-- Exercise 10

theorem foo {A : Type} {a b c : A} : a = b → c = b → a = c :=
assume ab cb,
have bc : b = c, from eq.symm cb,
show a = c, from eq.trans ab bc

-- notice that you can now use foo as a rule. The curly braces mean that
-- you do not have to give A, a, b, or c

section
    variable A : Type
    variables a b c : A
    example (h1 : a = b) (h2 : c = b) : a = c :=
    foo h1 h2
end

section
    variable {A : Type}
    variables {a b c : A}

    -- replace the sorry with a proof, using foo and rfl, without using eq.symm.
    theorem my_symm (h : b = a) : a = b :=
    have a = a, from rfl,
    show a = b, from foo ‹a = a› ‹b = a›

    -- now use foo, rfl, and my_symm to prove transitivity
    theorem my_trans (h1 : a = b) (h2 : b = c) : a = c :=
    foo h1 (my_symm h2)
end

-- Exercise 11

-- these are the axioms for a commutative ring

#check @add_assoc
#check @add_comm
#check @add_zero
#check @zero_add
#check @mul_assoc
#check @mul_comm
#check @mul_one
#check @one_mul
#check @left_distrib
#check @right_distrib
#check @add_left_neg
#check @add_right_neg
#check @sub_eq_add_neg

variables x y z : int

theorem t1 : x - x = 0 :=
calc
  x - x = x + -x : by rw sub_eq_add_neg
    ... = 0      : by rw add_right_neg

-- This alternate proof works:
example : x - x = 0 :=
eq.trans (sub_eq_add_neg x x) (add_right_neg x)

-- So does this:
example : x - x = 0 :=
have h1 : x - x = x + -x, from sub_eq_add_neg x x,
have h2 : x + -x = 0, from add_right_neg x,
show x - x = 0, from eq.trans h1 h2

theorem t2 (h : x + y = x + z) : y = z :=
calc
  y     = 0 + y        : by rw zero_add
    ... = (-x + x) + y : by rw add_left_neg
    ... = -x + (x + y) : by rw add_assoc
    ... = -x + (x + z) : by rw h
    ... = (-x + x) + z : by rw add_assoc
    ... = 0 + z        : by rw add_left_neg
    ... = z            : by rw zero_add

theorem t3 (h : x + y = z + y) : x = z :=
calc
  x     = x + 0        : by rw add_zero
    ... = x + (y + -y) : by rw add_right_neg
    ... = (x + y) + -y : by rw add_assoc
    ... = (z + y) + -y : by rw h
    ... = z + (y + -y) : by rw add_assoc
    ... = z + 0        : by rw add_right_neg
    ... = z            : by rw add_zero

theorem t4 (h : x + y = 0) : x = -y :=
calc
  x     = x + 0        : by rw add_zero
    ... = x + (y + -y) : by rw add_right_neg
    ... = (x + y) + -y : by rw add_assoc
    ... = 0 + -y       : by rw h
    ... = -y           : by rw zero_add

theorem t5 : x * 0 = 0 :=
have h1 : x * 0 + x * 0 = x * 0 + 0, from
calc
  x * 0 + x * 0 = x * (0 + 0) : by rw left_distrib
            ... = x * 0       : by rw add_zero
            ... = x * 0 + 0   : by rw add_zero,
show x * 0 = 0, from t2 _ _ _ h1

theorem t6 : x * (-y) = -(x * y) :=
have h1 : x * (-y) + x * y = 0, from
calc
   x * (-y) + x * y = x * (-y + y) : by rw left_distrib
                ... = x * 0        : by rw add_left_neg
                ... = 0            : by rw t5 x,
show x * (-y) = -(x * y), from t4 _ _ h1

theorem t7 : x + x = 2 * x :=
calc
  x + x = 1 * x + 1 * x : by rw one_mul
    ... = (1 + 1) * x   : by rw right_distrib
    ... = 2 * x         : rfl

hey do you have more from logic and proofs?

This is amazing