-- 两横线后面是注释-- 计算#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]