exercises for logic & proof chapter 14

exercises_14.lean

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
     := have h3 : a < b → b < c → a ≤ c, from (λ _ _, or.inl (transR ‹a < b›  ‹b < c›)),
        have h4 : a < b → b = c → a ≤ c, from (λ _ _, or.inl (‹b = c› ▸ ‹a < b› )),
        have h5 : a = b → b < c → a ≤ c, from (λ _ _, or.inl ((eq.symm ‹a = b›) ▸ ‹b < c›)),
        have h6 : a = b → b = c → a ≤ c, from (λ _ _, or.inr (eq.trans ‹a = b› ‹b = c›)),
        show a ≤ c, from or.elim h1
                                (λ _, or.elim h2 (λ _, h3 ‹a < b› ‹b < c›) (λ _, h4 ‹a < b› ‹b = c›))
                                (λ _, or.elim h2 (λ _, h5 ‹a = b› ‹b < c›) (λ _, h6 ‹a = b› ‹b = c›))   
    
    theorem antisymmR' {a b : A} (h1 : a ≤ b) (h2 : b ≤ a) 
     : a = b 
     := have ¬ a < a, from irreflR a,
        show a = b, from or.elim h1
                            (λ _, or.elim h2
                                    (λ _, false.elim (‹¬ a < a› (transR ‹a < b› ‹b < a›)))
                                    (λ _, eq.symm ‹b = a›))
                            (λ _, ‹a = b›)
 end

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 h1 : S a b,
        assume h2 : S b c,
        have R a c, from transR (h1.left) (h2.left),
        have R c a, from transR (h2.right) (h1.right),
        show S a c, from ⟨‹R a c›, ‹R c a›⟩
end

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)

    theorem R_is_strict_partial_order :
        irreflexive R ∧ transitive R := sorry

    theorem R_is_not_strict_partial_order :
        ¬(irreflexive R ∧ transitive R) :=
            assume h : irreflexive R ∧ transitive R,
            show false, from nRac (h.right Rab Rbc)
end

open nat
variables n m : ℕ

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