namespace hw1

namespace Lukasiewicz

-- 可以使用的三条公理
axiom A1 (α β γ : Prop) : (α → (β → γ)) → ((α → β) → (α → γ))
axiom A2 (α β : Prop)   : α → (β → α)
axiom A3 (α β : Prop)   : (¬α → ¬β) → (β → α)

-- 在该部分中，请不要使用 deduction theorem.
-- 如有需要，可以直接使用如下三个引理
-- axiom dne (α : Prop) : ¬¬α → α
-- axiom dni (α : Prop) : α → ¬¬α
-- axiom contra_lemma (α β : Prop) : (α → β) → (¬¬α → ¬¬β)
-- 题1
theorem prob1 (α β γ : Prop) : (α → (β → γ)) → (β → (α → γ)) := by
  sorry

-- 题2
theorem prob2 (α β γ : Prop) : (α → β) → ((γ → α) → (γ → β)) := by
  sorry

-- 题3
theorem prob3 (α β : Prop) : (α → β) → (¬β → ¬α) := by
  sorry

-- 题4
theorem prob4 (α β γ : Prop) : (α → β) → ((α → (β → γ)) → (α → γ)) := by
  sorry

end Lukasiewicz

-- 请使用直觉主义逻辑证明
namespace Intuitionistic

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 prob1 (α β γ : Prop) : (α → (β → γ)) → (β → (α → γ)) := by
  sorry

-- 题2
theorem prob2 (α β γ : Prop) : (α → β) → ((γ → α) → (γ → β)) := by
  sorry

-- 题3
theorem prob3 (α β : Prop) : (α → β) → (¬β → ¬α) := by
  sorry

-- 题4
theorem prob4 (α β γ : Prop) : (α → β) → ((α → (β → γ)) → (α → γ)) := by
  sorry

end Intuitionistic

end hw1


namespace hw2

/- =========================================================
   第一题：证明 {¬, ∨} 是功能完全的
   说明：已知 {¬, ∧, ∨} 是功能完全的。定义一个翻译，把含 {¬, ∧, ∨} 的公式改写成只含 {¬, ∨} 的公式，并证明改写后的公式与原公式实现同一个布尔函数。由此说明 {¬, ∨} 是功能完全的。
   ========================================================= -/

abbrev Valuation := Nat → Bool

inductive Formula where
  | var : Nat → Formula
  | neg : Formula → Formula
  | and : Formula → Formula → Formula
  | or  : Formula → Formula → Formula
deriving Repr

def eval : Formula → Valuation → Bool
  | Formula.var n, v   => v n
  | Formula.neg φ, v   => !(eval φ v)
  | Formula.and φ ψ, v => eval φ v && eval ψ v
  | Formula.or φ ψ, v  => eval φ v || eval ψ v

inductive NOFormula where
  | var : Nat → NOFormula
  | neg : NOFormula → NOFormula
  | or  : NOFormula → NOFormula → NOFormula
deriving Repr

def noeval : NOFormula → Valuation → Bool
  | NOFormula.var n, v  => v n
  | NOFormula.neg φ, v  => !(noeval φ v)
  | NOFormula.or φ ψ, v => noeval φ v || noeval ψ v

def toNO : Formula → NOFormula
  | Formula.var n =>
      NOFormula.var n
  | Formula.neg φ =>
      NOFormula.neg (toNO φ)
  | Formula.or φ ψ =>
      NOFormula.or (toNO φ) (toNO ψ)
  | Formula.and φ ψ =>
      NOFormula.neg (NOFormula.or (NOFormula.neg (toNO φ)) (NOFormula.neg (toNO ψ)))

/- 证明翻译 toNO 后得到的公式与原公式实现同一个布尔函数。 -/
theorem toNO_preserves_truth (φ : Formula) (v : Valuation) :
    noeval (toNO φ) v = eval φ v := by
  sorry

/- 证明 ∧ 可由 {¬, ∨} 通过函数复合定义。 -/
theorem and_realised_by_not_or (φ ψ : Formula) (v : Valuation) :
    noeval (toNO (Formula.and φ ψ)) v = eval (Formula.and φ ψ) v := by
  sorry


/- =========================================================
   第二题：证明 {∨, →} 不是功能完全的
   说明：定义只含 {∨, →} 的公式语言。证明：若一个真值指派使所有命题符号都取真，则任意这类公式在该指派下都为真。再由此说明不存在只含 {∨, →} 的公式能够实现 ¬p₀ 对应的布尔函数，从而 {∨, →} 不是功能完全的。
   ========================================================= -/

abbrev ValuationP := Nat → Prop

inductive OIFormula where
  | var : Nat → OIFormula
  | or  : OIFormula → OIFormula → OIFormula
  | imp : OIFormula → OIFormula → OIFormula
deriving Repr

def peval : OIFormula → ValuationP → Prop
  | OIFormula.var n, v   => v n
  | OIFormula.or φ ψ, v  => peval φ v ∨ peval ψ v
  | OIFormula.imp φ ψ, v => peval φ v → peval ψ v

/- 证明若一个真值指派使所有命题符号都取真，
   则任意只含 {∨, →} 的公式在该真值指派下都为真。 -/
theorem all_true_preserved (φ : OIFormula) :
    ∀ {v : ValuationP}, (∀ n, v n) → peval φ v := by
  sorry

def allTrue : ValuationP := fun _ => True

/- 证明任意只含 {∨, →} 的公式在全真值指派 allTrue 下都为真。 -/
theorem eval_allTrue (φ : OIFormula) : peval φ allTrue := by
  sorry

/- 证明不存在只含 {∨, →} 的公式能够实现 ¬p0 对应的布尔函数；
   从而 {∨, →} 不是功能完全的。 -/
theorem not_realised_by_or_imp :
    ¬ ∃ φ : OIFormula, ∀ v : ValuationP, peval φ v ↔ ¬ v 0 := by
  sorry

end hw2