_Logic and Proof_, Answers to Chapter 14 Exercises

Chapter 14 Exercises.lean

-- Exercise 14.1

section
parameters {A : Type} {R : A → A → Prop}
parameter (irreflR : irreflexive R)
parameter (transR : transitive R)

local infix < := R

def R' (a b : A) : Prop := R a b ∨ a = b
local infix ≤ := R'

theorem reflR' (a : A) : a ≤ a :=
have a = a, from rfl,
show a ≤ a, from or.inr ‹a = a›

theorem transR' {a b c : A} (h1 : a ≤ b) (h2 : b ≤ c):
  a ≤ c :=
or.elim h1
  (assume : a < b,
    have    a < c, from or.elim h2
      (assume : b < c,
        show    a < c, from transR ‹a < b› ‹b < c›)
      (assume : b = c,
        show    a < c, from eq.subst ‹b = c› ‹a < b›),
    show    a ≤ c, from or.inl ‹a < c›)
  (assume : a = b,
    show    a ≤ c, from eq.subst (eq.symm ‹a = b›) h2)

theorem antisymmR' {a b : A} (h1 : a ≤ b) (h2 : b ≤ a) :
  a = b :=
or.elim h1
  (assume : a < b,
    show a = b, from
      or.elim h2
        (assume : b < a,
          have  ¬ a < a, from irreflR a,
          have    a < a, from transR ‹a < b› ‹b < a›,
          show    a = b, from false.elim (‹¬ a < a› ‹a < a›))
        (assume : b = a,
          show    a = b, from eq.symm ‹b = a›)
    )
  (assume : a = b,
    this)

end


-- Exercise 14.2

section
parameters {A : Type} {R : A → A → Prop}
parameter (reflR : reflexive R)
parameter (transR : transitive R)

def S (a b : A) : Prop := R a b ∧ R b a

example : transitive S :=
assume a b c,
assume : S a b,
assume : S b c,
have h1 : R a b ∧ R b a, from ‹S a b›,
have h2 : R b c ∧ R c b, from ‹S b c›,
have R a c, from transR (and.left  h1) (and.left  h2),
have R c a, from transR (and.right h2) (and.right h1),
show S a c, from and.intro ‹R a c› ‹R c a›
end


-- Exercise 14.3

section
  parameters {A : Type} {a b c : A} {R : A → A → Prop}
  parameter (Rab : R a b)
  parameter (Rbc : R b c)
  parameter (nRac : ¬ R a c)

  -- Prove one of the following two theorems:

--theorem R_is_strict_partial_order :
--  irreflexive R ∧ transitive R :=
--sorry

  theorem R_is_not_strict_partial_order :
    ¬(irreflexive R ∧ transitive R) :=
  have n_transR : ¬ transitive R, from
    assume transR : transitive R,
    have Rac : R a c, from transR Rab Rbc,
    show false, from nRac Rac,
  assume h1 : irreflexive R ∧ transitive R,
  show false, from n_transR (and.right h1)
end


-- Exercise 14.4

open nat

example : 1 ≤ 4 :=
have 1 ≤ 2, from                  (nat.le_succ 1),
have 1 ≤ 3, from le_trans ‹1 ≤ 2› (nat.le_succ 2),
show 1 ≤ 4, from le_trans ‹1 ≤ 3› (nat.le_succ 3)

Paste this into the live in-browser version of the Lean theorem prover.