-- 兩橫線後面是註釋-- 計算#eval 12+12 -- 計算，結果是24

-- 類型檢查
def f (x :ℕ) :=  x + 3
#check f -- 類型檢查，結果是ℕ→ℕ
#check 2 + 2 = 4 -- 類型檢查，結果是Prop，即命題
def FermatLastTheorem :=  ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n
#check FermatLastTheorem --類型檢查，結果是Prop，即命題

theorem easy : 2 + 2 = 4 :=  rfl
#check easy -- 類型檢查，結果是2+2=4，即命題2+2=4的證明
theorem hard : FermatLastTheorem :=  sorry -- sorry表示暫時跳過證明
#check hard -- 類型檢查，結果是FermatLastTheorem，即命題FermatLastTheorem的證明

-- 定理證明
import Mathlib.Data.Real.Basic-- An example.

example (a b c : ℝ) : a * b * c = b * (a * c) := by

  rw [mul_comm a b]  -- 用乘法交換律，把a * b改寫為b*a

  rw [mul_assoc b a c] -- 用乘法結合律，把(b * a) * c改寫為b * (a * c)

-- rw即「重寫」，是一種證明策略，把一個表達式替換為相等的表達式

-- 一部分換行丟了。。重新發
-- 兩橫線後面是註釋
-- 計算#eval 12+12 -- 計算，結果是24

-- 類型檢查

#check 3 -- 類型檢查，結果是ℕ
def f (x :ℕ) :=  x + 3
#check f -- 類型檢查，結果是ℕ→ℕ
#check 2 + 2 = 4 -- 類型檢查，結果是Prop，即命題
def FermatLastTheorem :=  ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n
#check FermatLastTheorem --類型檢查，結果是Prop，即命題

theorem easy : 2 + 2 = 4 :=  rfl -- 證明2+2=4，rfl表示直接計算的策略
#check easy -- 類型檢查，結果是2+2=4，即命題2+2=4的證明
theorem hard : FermatLastTheorem :=  sorry -- sorry表示暫時跳過證明
#check hard -- 類型檢查，結果是FermatLastTheorem，即命題FermatLastTheorem的證明

-- 定理證明
import Mathlib.Data.Real.Basic -- 導入mathlib中的實數理論

example (a b c : ℝ) : a * b * c = b * (a * c) := by
  rw [mul_comm a b]  -- 用乘法交換律，把a * b改寫為b*a
  rw [mul_assoc b a c] -- 用乘法結合律，把(b * a) * c改寫為b * (a * c)


-- rw即「重寫」，是一種證明策略，把一個表達式替換為相等的表達式

import Mathlib.Data.Real.Basic

-- 一個稍複雜一些的例子，使用intro策略給各個假設命名
theorem my_lemma : ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by  

  intro x y ε epos ele1 xlt ylt  

  calc    |x * y| = |x| * |y| := by exact abs_mul x y    

  _ ≤ |x| * ε := by

    apply mul_le_mul     

    · apply le_refl      

    · exact le_of_lt ylt      

    · exact abs_nonneg y      

    · exact abs_nonneg x    

  _ < 1 * ε := by      

    rw [mul_lt_mul_right]      

    · apply lt_of_lt_of_le xlt ele1      

    · exact epos    

  _ = ε := by rw [one_mul]