/- 用 Lean4 将下列自然语言转换为形式化语言：将前面几行前提作为 Axioms，最后一行的命题（或其否定）作为 Theorem 并证明它。-/

-- 例子
/-
Ax1: Babies are illogical;
Ax2: Nobody is despised who can manage a crocodile;
Ax3: Illogical persons are despised.
Prop: Babies cannot manage crocodiles.
-/

variable {Person : Type}

axiom baby : Person → Prop
axiom illogical : Person → Prop
axiom despised : Person → Prop
axiom manage : Person → Prop

axiom Ax1 : ∀ p : Person, baby p → illogical p
axiom Ax2 : ∀ p : Person, manage p → ¬ despised p
axiom Ax3 : ∀ p : Person, illogical p → despised p

theorem BabiesCannotManageCrocodiles :
  ∀ p : Person, baby p → ¬ manage p := by
  intro p hbaby hmanage
  have : illogical p := Ax1 p hbaby
  have : despised p := Ax3 p this
  have : ¬ despised p := Ax2 p hmanage
  contradiction

-- 题目1
/-
Ax1: Every one who is sane can do Logic.
Ax2: No lunatics are fit to serve on a jury.
Ax3: None of your sons can do logic.
Prop: None of your sons are fit to serve on a jury.
-/

variable {Person : Type}

axiom sane : Person → Prop
axiom can_do_logic : Person → Prop
axiom fit_for_jury : Person → Prop
axiom son : Person → Prop

axiom Ax4 : ∀ p : Person, sane p → can_do_logic p
axiom Ax5 : ∀ p : Person, ¬ sane p → ¬ fit_for_jury p
axiom Ax6 : ∀ p : Person, son p → ¬ can_do_logic p

theorem SonsNotFitForJury :
  ∀ p : Person, son p → ¬ fit_for_jury p := by
  intro p hson
  have : ¬ can_do_logic p := Ax6 p hson
  have : ¬ sane p := by
    intro hsane
    have : can_do_logic p := Ax4 p hsane
    contradiction
  exact Ax5 p this

-- 题目2
/-
Ax1: None of the unnoticed things, met with at sea, are mermaids.
Ax2: Things entered in the log, as met with at sea, are sure to be worth remembering.
Ax3: I have never met with anything worth remembering, when on a voyage.
Ax4: Things met with at sea, that are noticed, are sure to be recorded in the log.
Prop: I have never met with a mermaid at sea.
-/

variable {Thing : Type}

axiom noticed : Thing → Prop
axiom met : Thing → Prop
axiom mermaid : Thing → Prop
axiom entered_in_log : Thing → Prop
axiom worth_remembering : Thing → Prop

axiom Ax7 : ∀ t : Thing, ¬ noticed t → met t → ¬ mermaid t
axiom Ax8 : ∀ t : Thing, entered_in_log t → met t → worth_remembering t
axiom Ax9 : ∀ t : Thing, met t → ¬ worth_remembering t
axiom Ax10 : ∀ t : Thing, met t → noticed t → entered_in_log t

theorem NoMermaid :
  ∀ t : Thing, met t → ¬ mermaid t := by
  intro t hmet
  by_cases hnoticed : noticed t
  · have : entered_in_log t := Ax10 t hmet hnoticed
    have : worth_remembering t := Ax8 t this hmet
    have : ¬ worth_remembering t := Ax9 t hmet
    contradiction
  · have : ¬ mermaid t := Ax7 t hnoticed hmet
    exact this

-- 题目3
/-
Ax1: No interesting poems are unpopular among people of real taste.
Ax2: No modern poetry is free from affectation.
Ax3: All your poems are on the subject of soap-bubbles.
Ax4: No affected poetry is popular among people of real taste.
Ax5: No ancient poem is on the subject of soap-bubbles.
Prop: Your poetry is not interesting.
-/

variable {Poem : Type}

axiom interesting : Poem → Prop
axiom popular : Poem → Prop
axiom modern : Poem → Prop
axiom your : Poem → Prop
axiom affected : Poem → Prop
axiom on_subject_of_soap_bubbles : Poem → Prop

axiom Ax11 : ∀ p : Poem, interesting p → popular p
axiom Ax12 : ∀ p : Poem, modern p → affected p
axiom Ax13 : ∀ p : Poem, your p → on_subject_of_soap_bubbles p
axiom Ax14 : ∀ p : Poem, affected p → ¬ popular p
axiom Ax15 : ∀ p : Poem, ¬ modern p → ¬ on_subject_of_soap_bubbles p

theorem YourPoetryNotInteresting :
  ∀ p : Poem, your p → ¬ interesting p := by
  intro p hyour
  have : on_subject_of_soap_bubbles p := Ax13 p hyour
  by_cases hmodern : modern p
  · have : affected p := Ax12 p hmodern
    have : ¬ popular p := Ax14 p this
    have : ¬ interesting p := by
      intro hinteresting
      have : popular p := Ax11 p hinteresting
      contradiction
    exact this
  · have : ¬ on_subject_of_soap_bubbles p := Ax15 p hmodern
    contradiction