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

-- 这次作业不可以直接使用 mathlib 中的定理或 simp, contradiction 等 tactic
-- 可使用的 tactic 只有：let, have, exact, intro
-- 题目1和题目2的证明中请勿使用 deduction theorem，即不能使用 intro。
-- 题目1
theorem thm1 (α : Prop) : α → α := by
  sorry

-- 题目2
theorem prop_syl (α β γ : Prop) (h1 : α → β) (h2 : β → γ) : α → γ := by
  sorry

-- 接下来的题目可以使用 deduction theorem 来简化证明过程。
-- 题目3
theorem EFQ (A B : Prop) : ¬A → A → B := by
  sorry

-- 题目4
theorem thm2 (α : Prop) : ¬¬α → α := by
  sorry

-- 题目5
theorem thm3 (α β γ : Prop) (h1 : α → β) (h2 : β → γ) : α → γ := by
  sorry

-- 题目6
theorem thm4 (α β : Prop) : (α → β) → ((α → ¬β) → ¬α) := by
  sorry


-- 接下来，请在直觉主义逻辑中再一次进行证明
axiom A1' (α β : Prop) : (α ∧ β) → α
axiom A2' (α β : Prop) : (α ∧ β) → β
axiom A3' (α β : Prop) : α → (β → (α ∧ β))
axiom A4 (α β : Prop) : α → (α ∨ β)
axiom A5 (α β : Prop) : β → (α ∨ β)
axiom A6 (α β γ : Prop) : (α → γ) → ((β → γ) → ((α ∨ β) → γ))
axiom A7 (α β : Prop) : α → (β → α)
axiom A8 (α β γ : Prop) : (α → (β → γ)) → ((α → β) → (α → γ))
axiom A9 (α β : Prop) : (α → β) → ((α → ¬β) → ¬α)
axiom A10 (α β : Prop) : ¬α → (α → β)
axiom A11 (α : Prop) : α → True
axiom A12 (α : Prop) : False → α
axiom A13 (α : Prop) : (α → False) → ¬α

-- 不可使用 deduction theorem
-- 题目1
theorem thm1 (α : Prop) : α → α := by
  sorry

-- 题目2
theorem prop_syl (α β γ : Prop) (h1 : α → β) (h2 : β → γ) : α → γ := by
  sorry

-- 可以使用 deduction theorem
-- 题目3
theorem EFQ (A B : Prop) : ¬A → A → B := by
  sorry

-- 题目4
theorem thm2 (α : Prop) : ¬¬α → α := by
  sorry

-- 题目5
theorem thm3 (α β γ : Prop) (h1 : α → β) (h2 : β → γ) : α → γ := by
  sorry

-- 题目6
theorem thm4 (α β : Prop) : (α → β) → ((α → ¬β) → ¬α) := by
  sorry

-- 题目7
theorem thm5 (α β : Prop) : (¬α → ¬β) → (β → α) := by
  sorry