Reposted by Masahiro Sakai
Masahiro Sakai
@msakai.bsky.social
293 followers 267 following 886 posts
Engineer at Noeon Research ← Engineer at Preferred Networks ← Research Scientist at 東芝.『抽象によるソフトウェア設計』『型システム入門』共訳者, Haskeller, github.com/msakai, twitter.com/masahiro_sakai facebook.com/masahiro.sakai
![コード4.26： LeanBook/NatCommMonoid/Simp.lean
1 example (n : MyNat) : 1 + n = n + 1 := calc
2 _ = .succ 0 + n := by rfl -- 1 は定義から.succ 0 に等しい
3 _ = .succ (0 + n) := by rw [MyNat.succ_add] -- .succ を外に出す
4 _ = .succ n := by rw [MyNat.zero_add] -- 0 + n = n を使って単純化
5 _ = n + 1 := by rfl -- n + 1 は定義から.succ n に等しい](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:nzrc5jvlmmqt6hnlm7fivo3f/bafkreih2tjy6ernfmcqd42v6eykxpl3znrtmh7jesyzwaox5syvtl36ea4)
![コード4.25： LeanBook/NatCommMonoid/Simp.lean
1 example (m n : MyNat) : .succ m + n = .succ (m + n) := by
2 induction n with
3 | zero => rfl
4 -- n = n' のケースまで示せていたと仮定して、n = n'.succ のケースを示す
5 | succ n' ih => calc
6 _ = (m.succ + n').succ := by rw [MyNat.add_succ] -- 左辺を _ で省略すると、
7 -- ゴールの左辺だと認識される
8 _ = (m + n').succ.succ := by rw [MyNat.succ_add] -- 左辺は同じなので_ で省略できる
9 _ = (m + n'.succ).succ := by rw [MyNat.add_succ]](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:nzrc5jvlmmqt6hnlm7fivo3f/bafkreihgz766xfkcgmmbjbfxjtqg2coyrrc55vdjxjkc7kci2tlti3l2ua)
