-- 三条公理，这次的作业只能够使用这三条公理以及 MP 规则进行证明。
axiom A1 (α β γ : Prop) : (α → (β → γ)) → ((α → β) → (α → γ))
axiom A2 (α β : Prop) : α → (β → α)
axiom A3 (α β : Prop) : (¬α → ¬β) → (β → α)

-- 这次作业不可以直接使用 mathlib 中的定理或 simp, contradiction 等 tactic
-- 可使用的 tactic 只有：let, have, exact, intro；也请不要使用 ¬α 等价于 α → False 的定义。
-- 题目1和题目2的证明中请勿使用 deduction theorem，即不能使用 intro。
-- 题目1
theorem thm1 (α : Prop) : α → α := by
  let h1 : (α → ((α → α) → α)) → ((α → (α → α)) → (α → α)) := A1 α (α → α) α
  let h2 : (α → ((α → α) → α)) := A2 α (α → α)
  have h3 : (α → (α → α)) → (α → α) := h1 h2
  let h4 : (α → (α → α)) := A2 α α
  have h5 : (α → α) := h3 h4
  exact h5

-- 题目2
theorem prop_syl (α β γ : Prop) (h1 : α → β) (h2 : β → γ) : α → γ := by
  have h3 : (β → γ) → (α → (β → γ)) := A2 (β → γ) α
  have h4 : α → (β → γ) := h3 h2
  have h5 : (α → (β → γ)) → ((α → β) → (α → γ)) := A1 α β γ
  have h6 : (α → β) → (α → γ) := h5 h4
  exact h6 h1

-- 接下来的题目可以使用 deduction theorem 来简化证明过程。
-- 题目3
theorem EFQ (A B : Prop) : ¬A → A → B := by
  intro hna hash
  have h1 : ¬B → ¬A := A2 (¬A) (¬B) hna
  have h2 : A → B := A3 B A h1
  exact h2 hash

-- 题目4
theorem thm2 (α : Prop) : ¬¬α → α := by
  intro h
  have h1 : ¬¬¬¬α → ¬¬α := A2 (¬¬α) (¬¬¬¬α) h
  have h2 : ¬α → ¬¬¬α := A3 (¬¬¬α) (¬α) h1
  have h3 : ¬¬α → α := A3 α (¬¬α) h2
  exact h3 h

-- 题目5
theorem thm3 (α β γ : Prop) (h1 : α → β) (h2 : β → γ) : α → γ := by
  intro ha
  have h3 : β := h1 ha
  exact h2 h3

-- 题目6
theorem thm4 (α β : Prop) : (α → β) → ((α → ¬β) → ¬α) := by
  intro h1 h2
  have h3 : α → ¬α := by
    intro ha
    exact EFQ β (¬α) (h2 ha) (h1 ha)
  have h4 : ¬¬α → ¬(¬α → ¬α) := by
    intro hnna
    have ha : α := thm2 α hnna
    exact EFQ α (¬(¬α → ¬α)) (h3 ha) ha
  have id_na : ¬α → ¬α := thm1 (¬α)
  exact A3 (¬α) (¬α → ¬α) h4 id_na

variable {A B C : Prop}