/-
    def 声明new constant symbols
    #check,#eval 辅助性命令一般#开头
    类型理论：a -> b 表示从a到b的函数类型
    描述f是关于x的函数 f x(e.g. Nat.succ 2)
    arrows associate to the right （Nat -> Nat -> Nat 是等同于Nat -> (Nat -> Nat)）
    函数的partially apply： Nat.add 3等同于Nat.add 3 n 返回了一个函数等待第二个参数n
-/

-- Lean的底层基础无限类型层次，Type 0是小范围的类型，Type 1是更大的类型，包含Type 0作为一个元素，以此类推
#check Type     -- Type 1
#check Type 1   -- Type 2
-- Lean依赖类型理论扩展的方式
    -- 1. 类型本身，它们的类型是Type

----------------------------------------------------------
-- 定义polymorphic constants（使用universe或者在定义时提供universe parameters）
universe u
def F (\a : Type u) : Type u := Prod \a \a
------------------------------------------
def G.{v} (\a : Type v) :Type v:= Prod \a \a

-- fun 也可以用 λ 代替
#check (fun x => x+1) -- Nat -> Nat,此处leave off type notation省略了类型注释
/-  fun (x : type) => t 其中()可以省略
    对于x：\a 变量，可以构造表达式t:\b
    λ (x: \a) => t 表示函数from \a to \b 将x 映射到t
    其中x 是bound variable，占位符，whose scope does not extend beyond the expression t
-/

def self_name (arg1 arg2 : arg_Type) (arg3 :arg_type) : return_Type := expression
-- 虽然返回类型Lean可以推断，但最好还是显示指出
def fun1 := fun x:Nat => x+x -- def 定义函数就是有名字的fun或λ
def fun2 (x:Nat)  : Nat := x+x
def fun21 (x:Nat)  := x+x

def fun3 : Nat -> Nat := fun x => x+x
def fun3 (x: Nat): Nat -> Nat := fun x => x+x --这个第一个x会提示没有用到
def f := 1

def compose (α β γ :Type) (f: α → β ) (g : γ → α ) (x: γ ):β := f (g x)

#eval compose Nat Nat Nat fun1 fun3 f --4

-- ;或换行都可以
def curiosity :=
    let x := 1+2
    let y := x+1;let z:=y+1
    x+y+z
#eval curiosity -- 12

/-
    ((fun a => t2) t1) 与 (let a := t1;t2)不一样；前者a是对t1的缩写，后者是a是一个变量，是一个整体

    #eval (fun a:Nat => a+a) 1+1 -- 3
    #eval (fun a:Nat => a*a) 1+1 -- 2
    #eval (fun a:Nat => a*a) (1+1) -- 4
    #eval let a:=1+1;a*a --4

    -- 迷惑？？？：bar0会 进行type check，但是bar不会进行！！！！
    def bar0 := let a:=Nat; fun x:a =>x+2
    def bar := (fun a => fun x : a => x + 2) Nat
-/

section outer
variable (\a \b \g :Type)
variable (x: \a) (y: \b) --作用域在section中，包括里面的section也起作用
section
variable (x: \b) 
-- 与外部相同的定义会覆盖外部
end
end outer

namespace foo
    namespace bar
    end bar
end foo

open foo --可以在当前使用非嵌套foo的短名

namespace foo
end foo

-- sorry produces a proof of anything or provides an object of any data type at all,但是不能用来证明False,会报错
-- _  placeholder代表implicit argument，表示自动填充
-- 可以从传入的某个参数确定一些类型参数，此时类型参数可以用_代替

-- 也可以在定义时，用 {}将可以推断的参数括起来，在传入时就无需显示指明

-- (e : T) to specify the type T of an expression e ,这样写告诉Lean的elaborator 在解决隐式参数时使用T作为e的Type

--  @List  -- 描述相同的方法，不过所用的参数都变成了explicit

-- Numerals are overloaded in Lean
#check 2 -- Nat
#check (2 : Int) -- Int

-- Prop is Sort 0
-- Type u is Sort (u+1)
-- if p q: Prop, then p \r q :Prop

-- if p : Prop , t1 t2:p 则 t1 t2是相等的
-- (fun x => t) s and t[s/x] as definitionally equal这个后者直接写这样会报错，所以不理解

/-
    -- 'theorem' command is really a version of 'def' command 对于类型检查器没有任何区别 Lean tags proof as irreducible 不可归约？， which serves as a hint to the parser（elaborator）that is generally no need to unfold them when processing a file.为何不需要展开?
    -- Lean 并行处理证明和进程，因为proof的 irrelevance，一个proof 的正确性无需另一个定理的细节
-/

-- #print theorem_name -- show you the proof of a theorem

-- 显示指明临时假设的类型 #show
variable {p : Prop}
variable {q : Prop}
theorem t1 : p \r q \r p :=
    fun hp : p =>
    fun hq : q =>
    show p from hp -- 原先只写 hp 就可以

axiom hp : p -- 等价于声明 p is true, as witnessed by hp

-- example command states a theorem without naming it or storing it in the permanent context,只是检查了term的类型

--  Curry-Howard isomorphism同构：and 和 prod是一种同构
-- 当相关类型是推纳类型且可以从context中推断出来，就可以使用Lean的匿名构造符号 \langle \rlangle 或者 \< \>
#check (⟨hp, hq⟩ : p ∧ q)

-- e.bar 是 Foo.bar.e 的缩写，不需要打开一个namespase
variable (ls : List Nat)
#check ls.length
#check List.length ls 

-- for auto construction \< \>
example (h : p \and q): q \and p \and q := \< h.right, h \>
-- 或者 \< h.right , \< h.left, h.right\>\>
-- 或者 And.intro h.right h -- h.left = And.left
-- Or.elim (h :p \or q) (left :p \r c) (right :q \r c) :c简写 h.elim (left) (right)

-- or 有两个构造器constructors，so 不能匿名构造，但仍然可以简写
-- 什么是constructors？？？

-- ex falso sequitur quodlibet False \r c从错误中能推出任意事实
example (hp : p) (hnp : \neg p) : q := Flase.elim (hnp hp) -- absurd hp hnp

-- have (h : p) := s;t 和 (fun (h : p) =>t) s 是一样的；s是p的证明，t是(h:p)期望假设的证明

/-
    suffices to show： resoning backwards from a goal
-/
    example (h : p∧ q) : q ∧ p :=
  have hp : p := h.left
  suffices hq:q from And.intro hq hp -- leave us with two goals,1 . by proving the original goal of q \and p with additional hypothesis hq : q, 2. have to show q
  show q from And.right h

open Classical
variable (p : Prop)
#check em p -- p ∨ ¬ p

-- 反证法形式化
#check byContradiction -- (\neg p -> False) -> p
-- 通过案例
#check byCases -- (p -> q) (\neg p -> q) -> q

-- x : \a ,p x 表示 p that holds of x
-- 任意 x : \a, p x 

/-
introduction:

Given a proof of p x, in a context where x : α is arbitrary, we obtain a proof ∀ x : α, p x.

Given a term t of type β x, in a context where x : α is arbitrary, we have (fun x : α => t) : (x : α) → β x.

elimination:

Given a proof ∀ x : α, p x and any term t : α, we obtain a proof of p t.

Given a term s : (x : α) → β x and any term t : α, we have s t : β t.
-/

-- 可以都用x来表示
example (α : Type)(p q : α → Prop): (∀ x : α , p x ∧ q x) → ∀ x : α , p x :=
  fun (h :∀ x : α , p x ∧ q x) =>
  (fun (z : α ) =>  -- 在此处重命名了变量
  show p z from (h z).left)

example : 2+3 = 5 := rfl -- Eq.refl _

-- Eq.subst h1 h2 {motive : \a -> Prop }(h1 : a = b) (h2 :motive a): motive b可以用 h1 \t h2代替,Eq.subst 推断 \a -> Prop 需要instanse of higher-order unification，但这个问题是不可决定的（为什么？），有时会失败，\t 更有效

#check congrArg  --congrArg.{u, v} {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂
#check congrFun --congrFun.{u, v} {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : f = g) (a : α) : f a = g a
#check congr --congr.{u, v} {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂

-- 乘法分配率
    -- 左结合
#check Nat.mul_add
#check Nat.left_distrib -- a *(b+c) = a*b +a*c
    -- 右结合 省略

/-
calc 
    <expr>_0 'op_1' <expr>_1 ':=' <proof>_1
    --expr<>_0可以单独一行，下面用'_'
    /-
    <expr>_0 
    '_'      'op_1' <expr>_1 ':=' <proof>_1
    -/
    '_'      'op_2' <expr>_2 ':=' <proof>_2
    ...
    '_'      'op_n' <expr>_n ':=' <proof>_n
-- each <proof>_i is a proof for <expr>_{i-1} op_i <expr>_i
-/

/-
`rw` tactics: 重写目标

use a given equality (which can be a hypothesis, a theorem name, or a complex term) to "rewrite" the goal. If doing so reduces the goal to an identity `t = t` ,the tatic applies reflexivity to prove it

`simp` tactics:更机智的重写目标,自动选择和重复的重写

rewrites the goal by applying the given identities repeatedly, in any order, anywhere they are applicable in a term. it also uses other rules that have been previously declared to the system, and applies commutativity wisely to avoid looping. 
-/

--`存在Exists.intro` : Existential introduction. If a : α and h : p a, then ⟨a, h⟩ is a proof that ∃ x : α, p x

-- set_option pp.explicit true 后使用#print 可以display implicit argument
/-
-- Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists p
-- implicit argument {p : α → Prop}意味着Lean能自动推出原命题，但是根据提供的值可以有很多假设：Lean use the context to infer which one is appropriate
example : ∃ x : Nat, x > 0 :=
  have h : 1 > 0 := Nat.zero_lt_succ 0
    Exists.intro 1 h
    -- ⟨1, h⟩
-/

/-
-- Exists.elim.{u} {α : Sort u} {p : α → Prop} {b : Prop}(h₁ : ∃ x, p x) (h₂ : ∀ (a : α), p a → b) : b
-/
variable (α : Type) (p q : α → Prop)

example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  Exists.elim h
    (fun w =>
     fun hw : p w ∧ q w =>
     show ∃ x, q x ∧ p x from ⟨w, hw.right, hw.left⟩)
/-`match .\a -> prop.. with | ...` :拆分组件(组件自命名，可拆的数目多种多样自助)
    the `match` statement destructs the exstential assertion into the components `w` and `hw`, which can be then used in the body of the statement to prove the proposition.
-/
variable (α : Type) (p q : α → Prop)

example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  match h with
  | ⟨w, hw⟩ => ⟨w, hw.right, hw.left⟩

--
variable (α : Type) (p q : α → Prop)
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  match h with
  | ⟨w, hpw, hqw⟩ => ⟨w, hqw, hpw⟩
  -- | ...=> ...
/- `let` : pattern-matching ,similar to `match h with | <> => <>`-/
example {α : Type}{p q : α → Prop} (h : ∃ x ,p x ∧ q x ): ∃ x , q x ∧ p x:=
  let ⟨ w, hpw, hqw⟩:= h
  ⟨ w,hqw,hpw⟩

variable (f : Nat → Nat)
variable (h : ∀ x : Nat, f x ≤ f (x + 1))
example : f 0 ≤ f 3 :=
  have : f 0 ≤ f 1 := h 0
  have : f 0 ≤ f 2 := Nat.le_trans this (h 1) -- this : f 0 ≤ f 1
  show f 0 ≤ f 3 from Nat.le_trans (by assumption) (h 2) -- (by assumption)如果目标可以inferred，就用assumption代
  
  -- by assumption的替代品那你，显示指出goal，notation "‹" p "›" => show p by assumption --`\f< \f>`

example : f 0 ≥ f 1 → f 1 ≥ f 2 → f 0 = f 2 :=
   fun p :(f 0 ≥ f 1) =>
    fun _ :(f 1 ≥ f 2) => -- 这个placeholder
    have :  f 0 ≥ f 2 :=
      Nat.le_trans ‹f 1 ≥ f 2 › ‹f 0 ≥ f 1 ›
    have :f 0 ≤ f 2 :=
      Nat.le_trans (h 0 ) (h 1)

    Nat.le_antisymm this ‹f 0 ≥ f 2 ›  

/-
`exact` is a variant of `apply` ,which signals that the expression given should fill the goal exactly.

-/

-- In the case of `apply` tactic, the tags are inferred from the parameters' names used in the And.intro declaration. 

-- can structure your tatics using the notation `case <tag> => <tatics>`,我认为这样可以改变解决默认的解决顺序
    -- 也可以\. 结构化证明过程
-- And.intro {a b : Prop} (left : a) (right : b) : a ∧ b
theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
  apply And.intro
  case right =>
    apply And.intro
    case left => exact hq
    case right => exact hp
  case left => exact hp

/-
tactic `intro` : introduces a hypothesis, a variable of any type, is a command for constructing function abstraction interactively  (i.e., terms of the form fun x => e) 也可以像`match`一样提供多个参数,也可已使用`intros`
intro 
| \<\> => ...
| \<\> => ...

也可以不提供任何参数：in which case, it chooses names and introduces as many variables as it can.结果是Lean自动生成名字(不能访问)，可以通过  use the combinator `unhygienic` to disable this restriction.

-/
example : ∀ a b c : Nat, a = b → a = c → c = b := by
  intros -- 相当于跟着a✝² b✝ c✝ a✝¹ a✝ 
  rename_i a b c h1 h2
  apply Eq.trans
  apply Eq.symm
  assumption
  assumption

example : ∀ a b c : Nat, a = b → a = c → c = b := by unhygienic
  intros -- 相当于跟着 a b c a_1 a_2
  apply Eq.trans
  apply Eq.symm
  exact a_2
  exact a_1
/-
tactic `rename_i `:`rename_i x_1 ... x_n` :
renames the last n inaccessible names using the given names.
-/

/-
tactic `assumption` : 
looks through the assumptions in context of the current goal, and if there is one matching the conclusion, it applies it.
-/

/-
The `rfl` tactic is syntactic sugar for `exact rfl`
-/

/-
The `revert` tactic is an reverse to `intro`, 把假设转为目标
-/

/-`generalize` tactic replace an arbitrary expression in the goal by a fresh variable: 将目标中的任意表达式替换成新变量 `generalize [h :]expre = variable`,但替换可能会导致goal不可证明-/
example : 2 + 3 = 5 :=by
  generalize h : 3 = x -- goal: 2 + x = 5
  rw[← h] -- 2 +3 = 5已经证明完毕了

/-`admit` :tactic
 is the analogue相似 of the `sorry` tactics-/

/-`cases` : 
decompose any element of an inductively defined type,子目标解决顺序任意；对于子目标使用相同策略的证明有用，和`match`的语法类似 cases h(具有多个可能值) with ,我认为区别在于match需要用函数构造，而cases直接使用tag作为函数名了
其中h的选择：可以是某个定理名（来自库或文件），也可以是某个变量表达式
-/
| <tag1> => <tactics1> -- tag是Lean在声明中的参数名
| <tag2> => <tactics2>
-/
  -- cases h(有多种可能) with
  -- | inl hp => apply Or.inr hp -- inl是tag，hp是参数（根据此情况需要传入的参数）
  -- | inr hq => apply Or.inl; exact hq
example (p q : Prop) : p ∧ q → q ∧ p := by
  intros h
  cases h with
  | intro left right => apply And.intro right left

example (p q : Prop) : p ∧ q → q ∧ p := by
  intros h
  match h with
  | And.intro left right => apply And.intro right left


-- 使用相同策略
example (p : Prop): p ∨ p → p := by
  intro h
  cases h
  repeat assumption

/-combinator `tac1 <;> tac2` ： 
<;> operator provides a parallel version of the sequencing operation: tac1 is applied to the current goal, and then apply the tactic `tac2` to each subgoal produced by tactic `tac1`
-/
example (p : Prop) : p ∨ p → p := by
  intro h
  cases h <;> assumption

/-`constructor`: apply the first applicable constructor of an inductively defined type

-/
example (p q : Prop) : p ∧ q → q ∧ p := by
  intros h
  match h with
  | And.intro left right => constructor; exact right; exact left -- constructor
example (p q : Prop) : p ∧ q → q ∧ p := by
  intros h
  match h with
  | And.intro left right => constructor<;> assumption -- tac1 <;> tac2

-- case and constructor
example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := by
  intros h
  cases h with
  | intro w hpw => constructor ; apply Or.inl; exact hpw

/-`contradiction`:
contradiction closes the main goal if its hypotheses are "trivially contradictory".
example (h : False) : q := by
  contradiction
-/

-- “combine” `intro h` with `match h ...`
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  apply Iff.intro
  . intro h
    match h with
    -- 可以推断出来
    | And.intro _ (Or.inl _) => apply Or.inl (⟨by assumption ,by assumption⟩ ) -- 自动推断 by assumption
    | And.intro hp (Or.inr hr) => apply Or.inr (⟨hp ,hr⟩ )
  . intro -- intro 和match 合二为一了
    | Or.inl ⟨hp, hq⟩ => constructor; exact hp; apply Or.inl; exact hq
    | Or.inr ⟨hp, hr⟩ => constructor; exact hp; apply Or.inr; exact hr

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := 
  by intro h
  by exact
    have hp : p := h.left
    have hqr : q ∨ r := h.right
    show (p ∧ q) ∨ (p ∧ r) by -- 此处是show .. by 是term-style
      cases hqr with
      | inl hq => exact Or.inl ⟨hp, hq⟩
      | inr hr => exact Or.inr ⟨hp, hr⟩

/-`show` tactic:
declares the type of the goal that is about to be solved,while remaining in tactic mode
`show t` finds the first goal whose target unifies with t. It makes that the main goal, performs the unification, and replaces the target with the unified version of t.重写目标为定义上相等的东西
-/
example (n : Nat) : n + 1 = Nat.succ n := by
  show Nat.succ n = Nat.succ n
  rfl

/-`have` tactic:
intoduces a new subgoal,
have name_label : xxx := ... 
1. can omit the label in the `have` tactic, in which case, the default label `this` is used
2. can omit types in the `have` tactic 
-/ 
example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
  intro ⟨hp, hqr⟩
  show (p ∧ q) ∨ (p ∧ r)
  cases hqr with
  | inl hq =>
    have hpq: p ∧ q := And.intro hp hq-- 定义label
    apply Or.inl
    exact hpq
  | inr hr =>
    have : p ∧ r := And.intro hp hr -- 省略label
    apply Or.inr
    exact this

/-`let` tactic:
introduce local definitions
the difference between `let` and `have` is that `let` introduces a local definition in the contextt, so that the definition of the local declaration can be unfolded in the proof.
-- let a : Nat := 3 * 2 -- 类型可以省略
-/

/- notation`.` : 
空格敏感，依赖于对齐来检测whether the tactic block ends.

不用`.` 也可以使用{} 和 ; 来确定block
-/

/-
apply foo
  . <proof of first goal>
  . <proof of second goal>
  
  case <tag of first goal>  => <proof of first goal>
  case <tag of second goal> => <proof of second goal>
 
  { <proof of first goal>  }
  { <proof of second goal> }
  
-/

/-
The `first | t₁ | t₂ | ... | tₙ` applies each `tᵢ` until one succeeds, or else fails

`skip` tactic does nothing and succeeds

-/
example (p q : Prop) (hp : p) : p ∨ q := by
  first | apply Or.inl; assumption | apply Or.inr; assumption

example (p q : Prop) (hq : q) : p ∨ q := by
  first | apply Or.inl; assumption | apply Or.inr; assumption

/-
`try` tac runs tac and succeeds even if tac failed.
!! `repeat (try tac)` will loop forver,because `try tac` will always succeed
-/
example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by
  -- 第一个constructor 将goal 变为 case left : p 和 case right : q ∧ r
  -- 第二个constructor只在case right 才会执行
  constructor <;> (try constructor) <;> assumption
end

/-`all_goals tac` : 
applies tac to all open goals
-/
example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by
  constructor
  all_goals (try constructor)
  all_goals assumption

/-`any_goals tac`:
与`all_goal`类似，except it succeeds if its argument succeed on at least one goal
 -/
example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  repeat any_goals constructor
  all_goals assumption
  -- repeat (first | constructor | assumption )

/-`focus t `combinator ensures that `t` only effects the current goal,temporarily hiding the others from the scope.So, if t ordinarily only effects the current goal, focus (all_goals t) has the same effect as t. 
-/
example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by
  constructor
  case right => constructor ; all_goals assumption
  case left => focus (all_goals apply hp) -- 等价于 focus (apply hp)

/-`rewrite [t]`: t is a term whose type asserts an equality.
1. 有多个可以替换时默认选择第一个进行替换
2. noatation `rw [t] at h` : 在h中rw
-/

-- 例子
example (w x y z : Nat) (p : Nat → Prop)
        : x * y + (z * w) * x = x * w * z + y * x := by
  simp

/-`simp`
1. do propositional rewriting. using hypothesis p, it rewrites p ∧ q to q and p ∨ q to true
2. 对于新的定义，也可以使用simp，可以在定义时标注 @[simp] （表示定理具有 [simp] 属性； 第二种方式是拉出来写 `attribute [simp] theorem_name`）就可以在使用`simp`时不显式指明定理
-/

example (p q : Prop) (hp : p) : p ∧ q ↔ q := by
  simp [*] -- 重写：p ∧ q = q
example (x y z : Nat) : (x + 0) * (0 + y * 1 + z * 0) = x * y := by
  simp -- 使用了带有simp属性的等式

example (x y z : Nat) (p : Nat → Prop) (h : p (x * y))
        : p ((x + 0) * (0 + y * 1 + z * 0)) := by
  simp at *; assumption


def mk_symm (xs : List α) :=
 xs ++ xs.reverse
theorem reverse_mk_symm (xs : List α)
        : (mk_symm xs).reverse = mk_symm xs := by
  simp [mk_symm]

example (xs ys : List Nat)
        : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by
  simp [reverse_mk_symm]

attribute [simp] reverse_mk_symm -- 这个属性一直存在(只要导入了含有属性声明的文件，约束属性作用域的办法： using the `local` modifier)
-- attribute [local simp] reverse_mk_symm -- 局部属性，outside the section, the simplifier will no longer use this theorem by default

example (xs ys : List Nat) (p : List Nat → Prop)
        (h : p (xs ++ mk_symm ys).reverse)
        : p (mk_symm ys ++ xs.reverse) := by
  simp at h; assumption


/-“wildcard 通配符” *：
 代表所有的hypotheses and the goal
 e.g. simp [*]
 -/

/-`simp_arith`:
 is shorthand for simp with arith := true and decide := true. This enables the use of normalization by linear arithmetic.
-/
section
def f (x y z: Nat): Nat :=
  match x , y ,z with
  | 0, _, _ => y
  | _, 0, _ => z
  | _, _, 0 => x
  | _, _, _ => 1
example (x y z : Nat) : x ≠ 0 → y ≠ 0 → z ≠ 0 → z = w → f x y w = 1 := by
  intros -- f x y w = 1
  simp [f]    /-(match x, y, w with
              | 0, x, x_1 => y
              | x, 0, x_1 => w
              | x_1, x_2, 0 => x
              | x, x_1, x_2 => 1) =
              1-/
  split ;repeat (first | contradiction| rfl)

  -- split <;> first | contradiction | rfl

  -- split
  -- case h_1 => contradiction
  -- case h_2 => contradiction
  -- case h_3 => contradiction
  -- case h_4 => rfl
end

example (xs ys : List Nat) (p : List Nat → Prop)
        (h : p (xs ++ mk_symm ys).reverse)
        : p ((mk_symm ys).reverse ++ xs.reverse) := by
  simp [-reverse_mk_symm] at h; assumption -- -负号

example (xs ys : List Nat) (p : List Nat → Prop)
        (h : p (xs ++ mk_symm ys).reverse)
        : p ((mk_symm ys).reverse ++ xs.reverse) := by
  simp only [List.reverse_append] at h; assumption -- only的应用

/-`simp` tactic 的useful configuration options:
{contextual := true, arith := true, decide := true, ...}
-/
-- 用x= 0 化简  y + x = y ，用x ≠ 0 化简 x ≠ 0
example : if x = 0 then y + x = y else x ≠ 0 := by
  simp (config := { contextual := true })

example : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := by
  simp_arith -- is a shorthand for `simp (config := {arith := true})`

--define a new tactic `my_tac`
syntax "my_tac" : tactic
macro_rules
  | `(tactic| my_tac)=> `(tactic| assumption)
example (h : p) : p := by
  my_tac

-- extend `my_tac`
macro_rules
  | `(tactic| my_tac) => `(tactic|  rfl)

example (x : α ): x = x:=by my_tac

-- extend `my_tac`
macro_rules
  | `(tactic | my_tac) => `(tactic| apply And.intro <;>my_tac )
example (x : α) (h : p) : x = x ∧ p := by
  my_tac

-- `open` 后面可以加括号指明至对于括号里面的打开命名空间,也就是可以直接使用括号里面的短别名
open Nat (succ zero gcd)
#check zero
#check add -- error
#check Nat.add --对的

-- 让Nat.mul的别名为times, Nat.plus的别名为plus
open Nat renaming mul → times, add → plus
#eval plus (times 2 2) 3  -- 7

/-`exprot`:
在当前namespace中创建短别名，如果export在一个命名空间外使用，则创建的别名是the top level
-/
export Nat (succ zero gcd)

/-`instance`command:
assiggn the notation 小于等于 to some relation
-/
def isPrefix (l₁ : List α) (l₂ : List α) : Prop :=
  ∃ t, l₁ ++ t = l₂

instance : LE (List α) where
  le := isPrefix
-- 变成局部
/-
def instLe : LE (List α) :=
  { le := isPrefix }

section
attribute [local instance] instLe

example (as : List α) : as ≤ as :=
  ⟨[], by simp⟩

end
-/
theorem List.isPrefix_self (as : List α) : as ≤ as :=
  ⟨[], by simp⟩

/-annotion : 
`{}` 
`\{{ and \}}` : weaker than `{}`,表示一个占位符应该只被添加在下一个显示参数之前
-/

/-introduing new `prefix` `infix` `postfix` operators-/
infixl :  65 "+" => HAdd.hAdd -- 65 is the precedence level
-- initial_command_name(describing the operator kind) : parsing precedence(natural number) : "a_token" => a_fuction(the operator should be translated to )
-- 其中`precedence` 代表how "tightly" an operator binds to its arguments,encoding the order of operations(1024优先级可以简写为`max`)

/-`notation`:
接受一系列的tokens和命名的term placeholders with precedences
-/

variable (m n : Nat)
variable (i j : Int)
#check (m + i) --↑m + i : Int
#check Int.ofNat m -- Int

#check @Eq
#print -- (展示type of the symbol and definition of a definition or theorem; 展示indicates that fact, and shows the type of a constant or an axiom)

-- set_option <name> <value>
-- `set_option pp.all true` carries out these settings all at once, whereas `set_option pp.all` false reverts to the previous values.
-- pp.notation :使用defined notation to display output

-- Sort 类型比Type更general
def compose (g : β → γ) (f : α → β) (x : α) : γ :=
  g (f x)

#check @compose
-- {β : Sort u_1} → {γ : Sort u_2} → {α : Sort u_3} → (β → γ) → (α → β) → α → γ

-- 在Lean4中对于中缀操作符：使用 · as a placeholder
#check (· + 1)
-- fun a => a + 1
#check (2 - ·)
-- fun a => 2 - a
#eval [1, 2, 3, 4, 5].foldl (·*·) 1
-- 120

def f (x y z : Nat) :=
  x + y + z

#check (f · 1 ·)
-- fun a b => f a 1 b

#eval [(1, 2), (3, 4), (5, 6)].map (·.1)
-- [1, 3, 5]

-- 需要括号打断· 和 ·
#check (Prod.mk · (· + 1)) --fun x => (x, fun x => x + 1) : ?m.49894 → ?m.49894 × (Nat → Nat)

-- Inductive type is built up from a specified list of constructors
inductive Foo where
  | constructor₁ : ... → Foo
  | constructor₂ : ... → Foo
  ...
  | constructorₙ : ... → Foo

/-使用match expression定义Weekday的函数-/
inductive Weekday where
 | sunday : Weekday
 | monday : Weekday
 | tuesday : Weekday
 | wednesday : Weekday
 | thursday : Weekday
 | friday : Weekday
 | saturday : Weekday
 deriving Repr -- instruct Lean to generate a function that converts Weekday objects into text.
open Weekday

def numberOfDay (d : Weekday) : Nat :=
  match d with
  | sunday    => 1
  | monday    => 2
  | tuesday   => 3
  | wednesday => 4
  | thursday  => 5
  | friday    => 6
  | saturday  => 7

#eval numberOfDay Weekday.sunday  -- 1
#eval numberOfDay Weekday.monday  -- 2

/-使用match定义函数：-/
namespace Hidden
def and (a b : Bool) : Bool :=
  match a with
  | true  => b
  | false => false
end Hidden

inductive Prod (α : Type u)(β : Type v)
| mk  (a :α) (b :β)   : Prod α β -- 可以对参数命名
-- mk : α → β → Prod α β

/-
介绍了
1. inductive type : Prod
2. mk : constructor
3. fst , snd : projections
4. eliminators `rec` `recOn`
-/
structure Prod (α : Type u) (β : Type v) where
  mk :: (fst : α) (snd : β)

structure Color where
  (red : Nat)(green : Nat)(blue : Nat) -- 不用()用换行也行
  deriving Repr

-- dependent Product sugma 
-- Sigma.mk.{u, v} {α : Type u} {β : α → Type v} (fst : α) (snd : β fst) : Sigma β
namespace Hidden
inductive Sigma {α : Type u} (β : α → Type v) where
  | mk : (a : α) → β a → Sigma β
end Hidden

inductive Or (a b: Prop) where
| inl : a -> Or a b 
| inr : b -> Or a b

inductive Exists {α : Type u} (p : α → Prop) where
  | intro (w : α) (hw : p w) : Exists p

inductive Nat where
  | zero : Nat
  | succ : Nat → Nat
  deriving Repr

def add (a   b : Nat): Nat :=
  match a with
  | Nat.zero => b
  | Nat.succ a' => Nat.succ (add a' b)

-- 归纳证明例子
open Nat
theorem add_comm (m n : Nat) : m + n = n + m :=
  Nat.recOn (motive := fun x => m + x = x + m) n
   (show m + 0 = 0 + m by rw [Nat.zero_add, Nat.add_zero])
   (fun (n : Nat) (ih : m + n = n + m) =>
    show m + succ n = succ n + m from
    calc m + succ n
      _ = succ (m + n) := rfl
      _ = succ (n + m) := by rw [ih]
      _ = succ n + m   := sorry)

-- sorry 处依旧可以用归纳证明 succ n + 0,  succ n + succ m

inductive List (α : Type u) where
  | nil : List α
  | cons : α → List α → List α

-- 排中律Decidable.em
theorem em (p : Prop) [Decidable p] : p ∨ ¬p :=
  byCases Or.inl Or.inr

-- 其中...表示一系列的参数类型，叫做`indices`
inductive foo : ... → Sort u where
  | constructor1 : ... → foo ...
  | constructor₂ : ... → foo ...
  ...
  | constructorₙ : ... → foo ...

mutual
    inductive Tree (α : Type u) where
      | node : α → TreeList α → Tree α

    inductive TreeList (α : Type u) where
      | nil  : TreeList α
      | cons : Tree α → TreeList α → TreeList α
end

inductive Tree (α : Type u) where
  | mk : α → List (Tree α) → Tree α -- 用List(Tree \a )代替TreeList 

/-`zero` and `succ` notation 具有 [match_pattern] attribute, they can be used in pattern matching
-/
-- def的多cases形式
def sub1 : Nat → Nat
  | zero   => zero
  | succ x => x
-- 不用zero和succ
def sub1' : Nat → Nat
  | 0 => 0
  | x +1 => x

-- 一个参数示例
def sub2 : Nat → Nat
  | zero => 0
  | succ zero => 0
  | succ (x + 1)=> x
#check sub2.match_1 -- 这里面写出了sub2的完整定义
#check sub2 -- Nat →  Nat

def sub2' : Nat → Nat :=
  fun x =>
  match x with
  | zero => 0
  | 1 => 0
  | x + 2 => x

-- 两个参数示例
def foo : Nat → Nat → Nat
  | 0,   n   => 0
  | m+1, 0   => 1
  | m+1, n+1 => 2
-- 只对一个参数模式匹配
def and : Bool → Bool → Bool
  | true, a=> a
  | false , _ => false -- 这里的_表示wildcard pattern或者匿名变量，并不代表implicit argument

/-出现在`:` 之前的参数不参与pattern matching，Lean also allows parameters to occur after `:`,but it cannot pattern match on them-/
-- α 不参与 pattern matching
def tail1 {α : Type u} : List α → List α
  | []      => []
  | a :: as => as
-- α也没有参与 pattern matching，只对list进行了分割
def tail2 : {α : Type u} → List α → List α
  | α, []      => []
  | α, a :: as => as

def foo : Nat → Nat → Nat
  | 0,   n   => 0
  | m, 0   => 1
  | m, n => 2

-- `_`作为通配符
def foo : Nat → Nat → Nat
  | 0,   _   => 0-- m n 的值没有用到，可以写成_
  | _, 0   => 1
  | _, _ => default -- default是Inhabited类型的默认值

/-`Option`: simulate the incomplete patterns.The idea is to return `some a`for the provided patterns, and use `none` for the incomplete cases

-/
def f2 : Nat → Nat → Option Nat
  | 0, _  => some 1
  | _, 0  => some 2
  | _, _  => none     -- the "incomplete" case

theorem zero_add : ∀ n, add zero n = n
  | zero => rfl
  | succ n => congrArg succ (zero_add n) -- 递归
  -- | succ n => by simp [add, zero_add] 
-- 要证明 add zero (succ n) = succ n  =>
--f :=succ x = x + 1;
-- h:=  add zero n = n 结果 succ (add zero n)  = succ n
-- 另一种写法
theorem zero_add : ∀ n, add zero n = n
  | zero => by simp [add]
  | succ n => by rw[add, zero_add]

open Nat
def add (m : Nat) : Nat → Nat
  | zero => m
  | succ n => succ (add m n)

-- 也可以使用match
def add' (m n: Nat) :  Nat :=
  match n with
  | zero => m
  | succ n => succ (add m n)

/-
`let rec`和`where`在`def`中的应用
-/
def fibFast (n : Nat) : Nat :=
  (loop n).2
where
  loop : Nat → Nat × Nat
    | 0   => (0, 1)
    | n+1 => let p := loop n; (p.2, p.1 + p.2)

def fibFast' (n : Nat): Nat:=
  let rec loop : Nat → Nat × Nat
    | 0 => (0,1)
    | n + 1 => let p := loop n; (p.2, p.2 + p.1)
  (loop n).2

/-`below` `brecOn`介绍：
To handle structural recursion, the equation compiler uses course-of-values recursion, using constants below and brecOn that are automatically generated with each inductively defined type
-/
variable (C : Nat → Type u)

#check (@Nat.below C : Nat → Type u)

#reduce @Nat.below C (3 : Nat)-- 存储C 0， C 1， C 2元素的数据结构

-- 下面是值过程递归的例子
#check (@Nat.brecOn C : (n : Nat) → ((n : Nat) → @Nat.below C n → C n) → C n)

def append : List α → List α → List α
  | [] , bs => bs
  | a :: as , bs => a :: append as bs

-- le_div_iff₀这个theorem，以及rm[]
-- 使用方面linarith(线性计算)，和ring(交换)
-- 以及证明时可以把用的定理直接提出来，theorem
-- have h:引入假设，calc 分步计算，让过程更加清晰，因为写出了要证明的每一步的结果
-- tatics： apply , repeat

-- 归纳
-- inductive types (which are types generated infuctively by a given list of constructors)
-- e.g. the natual numbers are declared as follows( in Prelude.lean)
inductive Nat where
  | zero : Nat -- constructor
  | succ (n : Nat): Nat -- constructor
---------------------------------------------------------

@[simp] -- specifys that the defining equation should be added to the database of identities that the simplifier uses by default

structure structure_name where
  ...

-- 此注解表示自动生成定理: 当结构体的两个实例组成部分对应相同时，这两个实例相等
@[ext] -- extensionality,tells Lean to automatically generate theorems that can be used to prove that two instances of a structure are equal when their components are equal.

def inst_name : struc_name where
  ...
  -- e.g. x:=1
---------------------------------
def inst_name : struct_name :=
  ...
  --e.g. <value1 , ,...> -- anonymous constructor notation
---------------------------------
def inst_name :=
  struc_name.mk ...valuek valuek+1 ...
  -- struc_name.mk 是constructor，也可以自己命名，需要在define structure 的时候，比where多 了name和::
  -- structure struc_name where constructor_name ::
  --    ...
-- open a namespace
namespace namespace_name
...
end namespace_name

-- so that the theorem name is Point.add_comm,even when the namespace is open
protected theorem add_comm (a b :Point) :add a b = add b a:=by
  sorry

--1. 使用hypothesis ：任意
--2. 使用repeat
example : min a b = min b a := by
  have h : ∀ x y : ℝ, min x y ≤ min y x := by
    intro x y
    apply le_min
    apply min_le_right
    apply min_le_left
  apply le_antisymm
  apply h
  apply h
-----------------------
example : min a b = min b a := by
  apply le_antisymm
  repeat
    apply le_min
    apply min_le_right
    apply min_le_left

example (a b : R) : a - b = a + -b :=by
  rw[sub_eq_add_neg a b]
end

example (a b : R) : a - b = a + -b :=
  sub_eq_add_neg a b
end

--
section ... end
-- 变量声明
variable(v1 v2 v3 ... : type) 
-- 检查类型，或描述用法
#check ...
#check a -- a:R
#check mul_comm -- mul_comm.{u_1} {G : Type u_1} [CommMagma G] (a b : G) : a * b = b * a

#check norm_num -- 常量计算与比较，Normalize numerical expressions. Supports the operations + - * / ⁻¹ ^ and % over numerical types such as ℕ, ℤ, ℚ, ℝ, ℂ and some general algebraic types, and can prove goals of the form A = B, A ≠ B, A < B and A ≤ B, where A and B are numerical expressions. It also has a relatively simple primality prover.

-- Nat.gcd m n :最大公约数,在显示的时候会显示出来m.gcd.n

example:(a+b)*(a+b) = a*a+2*a*b +b*b:
    calc
        xx :by
            xx
        _=xxx:=by
            xx
        _=xxxx:=by
            xxxx

theorem zero_mul(a: R):0*a  =0 := by
    have h: 0*a+0*a = 0*a+0 :=by
        rw[←add_mul,add_zero,add_zero]
    rw[add_left_cancel h]

nth_rw <第几个>[]替换
rw[mul_assoc]--a*b*c = a*(b*c)
rw[mul_assoc]--a*(b*c)=a*b*c
sub_self -- a-a=0

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

/-
Copyright (c) 2023 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser
-/
syntax (name := eqns) "eqns" ident* : attr

initialize eqnsAttribute : NameMapExtension (Array Name) ←
  registerNameMapAttribute {
    name  := `eqns
    descr := "Overrides the equation lemmas for a declation to the provided list"
    add   :=  fun
    | _, `(attr| eqns $[$names]*) => -- 这里面的第二个参数是模式匹配，捕获了eqns关键字后面的所有标识符
      pure <| names.map (fun n => n.getId)
    | _, _ => Lean.Elab.throwUnsupportedSyntax }

initialize Lean.Meta.registerGetEqnsFn (fun name => do
  pure (eqnsAttribute.find? (← getEnv) name))