Small Exercises

small_exercises.lean

-- Theorems/Exercises from "Logical Investigations, with the Nuprl Proof Assistant"
-- by Robert L. Constable and Anne Trostle
-- http://www.nuprl.org/MathLibrary/LogicalInvestigations/
import logic

-- 2. The Minimal Implicational Calculus
theorem thm1 {A B : Prop} : A → B → A :=
assume Ha Hb, Ha

theorem thm2 {A B C : Prop} : (A → B) → (A → B → C) → (A → C) :=
assume Hab Habc Ha,
  Habc Ha (Hab Ha)

theorem thm3 {A B C : Prop} : (A → B) → (B → C) → (A → C) :=
assume Hab Hbc Ha,
  Hbc (Hab Ha)

-- 3. False Propositions and Negation
theorem thm4 {P Q : Prop} : ¬P → P → Q :=
assume Hnp Hp,
  absurd Hp Hnp

theorem thm5 {P : Prop} : P → ¬¬P :=
assume (Hp : P) (HnP : ¬P),
  absurd Hp HnP

theorem thm6 {P Q : Prop} : (P → Q) → (¬Q → ¬P) :=
assume (Hpq : P → Q) (Hnq : ¬Q) (Hp : P),
  have Hq : Q, from Hpq Hp,
  show false, from absurd Hq Hnq

theorem thm7 {P Q : Prop} : (P → ¬P) → (P → Q) :=
assume Hpnp Hp,
  absurd Hp (Hpnp Hp)

theorem thm8 {P Q : Prop} : ¬(P → Q) → (P → ¬Q) :=
assume (Hn : ¬(P → Q)) (Hp : P) (Hq : Q),
  -- Rermak we don't even need the hypothesis Hp
  have H : P → Q, from assume H', Hq,
  absurd H Hn

-- 4. Conjunction and Disjunction
theorem thm9 {P : Prop} : (P ∨ ¬P) → (¬¬P → P) :=
assume (em : P ∨ ¬P) (Hnn : ¬¬P),
  or.elim em
    (assume Hp, Hp)
    (assume Hn, absurd Hn Hnn)

theorem thm10 {P : Prop} : ¬¬(P ∨ ¬P) :=
assume Hnem : ¬(P ∨ ¬P),
  have Hnp : ¬P, from
    assume Hp : P,
      have Hem : P ∨ ¬P, from or.inl Hp,
      absurd Hem Hnem,
  have Hem : P ∨ ¬P, from or.inr Hnp,
  absurd Hem Hnem

theorem thm11 {P Q : Prop} : ¬P ∨ ¬Q → ¬(P ∧ Q) :=
assume (H : ¬P ∨ ¬Q) (Hn : P ∧ Q),
  or.elim H
    (assume Hnp : ¬P, absurd (and.elim_left Hn) Hnp)
    (assume Hnq : ¬Q, absurd (and.elim_right Hn) Hnq)

theorem thm12 {P Q : Prop} : ¬(P ∨ Q) → ¬P ∧ ¬Q :=
assume H : ¬(P ∨ Q),
  have Hnp : ¬P, from assume Hp : P, absurd (or.inl Hp) H,
  have Hnq : ¬Q, from assume Hq : Q, absurd (or.inr Hq) H,
  and.intro Hnp Hnq

theorem thm13 {P Q : Prop} : ¬P ∧ ¬Q → ¬(P ∨ Q) :=
assume (H : ¬P ∧ ¬Q) (Hn : P ∨ Q),
  or.elim Hn
    (assume Hp : P, absurd Hp (and.elim_left H))
    (assume Hq : Q, absurd Hq (and.elim_right H))