search

lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
15 stars 5 forks source link

dsimp が効きそうで効かない例 #399

Open Seasawher opened 4 days ago

Seasawher commented 4 days ago 
inductive MyNat : Type where
  | zero : MyNat
  | succ : MyNat → MyNat

namespace MyNat

def add (m n : MyNat) : MyNat :=
  match n with
  | zero => m
  | succ n => succ (add m n)

instance : OfNat MyNat 0 where
  ofNat := .zero

instance : OfNat MyNat 1 where
  ofNat := .succ .zero

instance : Add MyNat where
  add := MyNat.add

@[simp] theorem add_zero (n : MyNat) : n + 0 = n := by rfl
@[simp] theorem zero_add (n : MyNat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    dsimp [Add.add, MyNat.add]
    -- goal state: 0 + n.succ = n.succ
    -- why goal is not changed?

    rw [show 0 + n.succ = .succ (0 + n) from by rfl]
    rw [ih]
Seasawher commented 4 days ago

これかなり不思議（せめて dsimp made no progress エラーになってほしい）

Seasawher commented 4 days ago

導入した 0 記号と MyNat.zero が同じであることを黙っていても理解してほしいが

theorem add_assoc (m n l: MyNat) : m + (n + l) = (m + n) + l := by
  induction l with
  | zero => 
    rw [show zero = 0 from rfl]
    simp 
  | succ l ih => 
    show m + (n + l.succ) = m + n + l.succ 

    have lhs : m + (n + l.succ) = .succ (m + n + l) := calc
      m + (n + l.succ) = m + (.succ (n + l)) := rfl
      _ = .succ (m + (n + l)) := rfl
      _ = .succ (m + n + l) := by rw [ih]

    have rhs : m + n + l.succ = .succ (m + n + l) := by rfl

    rw [lhs, rhs]
Seasawher commented 3 days ago

HAdd.hAdd が必要

inductive MyNat : Type where
  | zero : MyNat
  | succ : MyNat → MyNat

namespace MyNat

def add (m n : MyNat) : MyNat :=
  match n with
  | zero => m
  | succ n => succ (add m n)

instance : OfNat MyNat 0 where
  ofNat := .zero

instance : OfNat MyNat 1 where
  ofNat := .succ .zero

instance : Add MyNat where
  add := MyNat.add

@[simp] theorem add_zero (n : MyNat) : n + 0 = n := by rfl
@[simp] theorem zero_add (n : MyNat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    dsimp [HAdd.hAdd, Add.add, MyNat.add] at ih ⊢
    rw [ih]

end MyNat