Skip to content

Commit 1ef95b5

Browse files
SeasawherSeasawher
authored
Merge pull request #364 from lean-ja/Seasawher/issue342
`dsimp` を `simp` から独立させる
2 parents 33e98b4 + e7e2e27 commit 1ef95b5

File tree

4 files changed

+141
-5
lines changed

4 files changed

+141
-5
lines changed

‎Examples/Tactic/Dsimp.lean

+139
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,139 @@
1+
/- # dsimp
2+
3+
`dsimp` は，定義上(definitionally)等しいような変形だけを行うという制約付きの [`simp`](./Simp.md) で，一言でいえば「名前を定義に展開する」タクティクです．
4+
5+
`dsimp [e₁, e₂, ..., eᵢ]` という構文でゴールに登場する名前 `e₁`, ..., `eᵢ` を定義に展開します．-/
6+
7+
/-- 算術式 -/
8+
inductive Expr where
9+
| const : Nat → Expr
10+
| plus : Expr → Expr → Expr
11+
| times : Expr → Expr → Expr
12+
13+
open Expr
14+
15+
/-- サイズ２の Expr を計算によって簡略化する -/
16+
def simpConst : Expr → Expr
17+
| plus (const n₁) (const n₂) => const (n₁ + n₂)
18+
| times (const n₁) (const n₂) => const (n₁ * n₂)
19+
| e => e
20+
21+
/-- simpConst を良い感じに再帰的に適用して，Expr を単一の Expr.const に簡略化する.-/
22+
def fuse : Expr → Expr
23+
| plus e₁ e₂ => simpConst (plus (fuse e₁) (fuse e₂))
24+
| times e₁ e₂ => simpConst (times (fuse e₁) (fuse e₂))
25+
| e => e
26+
27+
/-- fuse は実際に Expr を const に簡略化する. -/
28+
theorem fuse_in_const {e : Expr} : ∃ n, fuse e = .const n := by
29+
induction e with
30+
| const n => exists n
31+
| plus e₁ e₂ ih₁ ih₂ =>
32+
-- ゴールに fuse が登場する
33+
show ∃ n, fuse (e₁.plus e₂) = const n
34+
35+
-- fuse を定義に展開する
36+
dsimp [fuse]
37+
show ∃ n, simpConst (.plus (fuse e₁) (fuse e₂)) = const n
38+
39+
-- ローカルコンテキストの存在命題を利用してゴールを書き換える
40+
obtain ⟨n₁, ih₁⟩ := ih₁
41+
obtain ⟨n₂, ih₂⟩ := ih₂
42+
rw [ih₁, ih₂]
43+
show ∃ n, simpConst (.plus (const n₁) (const n₂)) = const n
44+
45+
-- simpConst を定義に展開する
46+
dsimp [simpConst]
47+
show ∃ n, const (n₁ + n₂) = const n
48+
49+
-- n = n₁ + n₂ とすれば良い
50+
exists n₁ + n₂
51+
| times e₁ e₂ ih₁ ih₂ =>
52+
-- plus の場合と同様
53+
dsimp [fuse, simpConst]
54+
obtain ⟨n₁, ih₁⟩ := ih₁
55+
obtain ⟨n₂, ih₂⟩ := ih₂
56+
rw [ih₁, ih₂]
57+
exists n₁ * n₂
58+
59+
/- ## 舞台裏
60+
「定義上等しいような変形だけを行う」というのは，`rfl` で示せるような命題だけを使用するという意味です．`rfl` で示せないような簡約は `dsimp` ではできません．-/
61+
62+
/-- 自前で定義した自然数 -/
63+
inductive MyNat where
64+
| zero : MyNat
65+
| succ : MyNat → MyNat
66+
67+
/-- MyNat の足し算 -/
68+
def MyNat.add (n m : MyNat) : MyNat :=
69+
match m with
70+
| MyNat.zero => n
71+
| MyNat.succ m => MyNat.succ (MyNat.add n m)
72+
73+
/-- MyNat.add を足し算記号で書けるようにする -/
74+
infix:65 " + " => MyNat.add
75+
76+
/-- ゼロを左から足しても変わらない．
77+
自明なようだが，MyNat.add は m に対する場合分けで定義されているので定義上明らかではない. -/
78+
theorem MyNat.zero_add {n : MyNat} : MyNat.zero + n = n := by
79+
induction n with
80+
| zero => rfl
81+
| succ n ih =>
82+
dsimp [MyNat.add]
83+
rw [ih]
84+
85+
example (n : MyNat) : n + MyNat.zero = n := by
86+
-- rfl で証明ができる
87+
try rfl; done; fail
88+
89+
-- dsimp でも証明ができる
90+
dsimp [MyNat.add]
91+
92+
example (n : MyNat) : MyNat.zero + n = n := by
93+
-- rfl では証明ができない
94+
fail_if_success rfl
95+
96+
-- dsimp でも証明ができない
97+
fail_if_success dsimp [MyNat.add]
98+
99+
rw [MyNat.zero_add]
100+
101+
/- ## unfold との違い
102+
同じく名前を定義に展開するタクティクとして [`unfold`](./Unfold.md) があります．たいていの場合両者は同じように使うことができますが，`unfold` は次のような意外な挙動をすることがあるので `dsimp` を使うことを推奨します．
103+
-/
104+
105+
-- α の部分集合を表す型
106+
def Set (α : Type) := α → Prop
107+
108+
-- 部分集合の共通部分を取る操作
109+
def Set.inter {α : Type} (s t : Set α) : Set α := fun x => s x ∧ t x
110+
111+
-- ∩ という記法を使えるようにする
112+
instance (α : Type) : Inter (Set α) where
113+
inter := Set.inter
114+
115+
variable {α : Type} (s u : Set α)
116+
117+
example: True ∨ (s ∩ u = u ∩ s) := by
118+
-- ∩ 記号を展開する
119+
dsimp [Inter.inter]
120+
121+
-- Set.inter で書き直される
122+
show True ∨ (s.inter u = u.inter s)
123+
124+
left; trivial
125+
126+
example : True ∨ (s ∩ u = u ∩ s) := by
127+
-- ∩ 記号を展開する
128+
unfold Inter.inter
129+
130+
-- 展開結果にインスタンスが入ってしまう
131+
show True ∨ (instInterSet α).1 s u = (instInterSet α).1 u s
132+
133+
-- 再びインスタンスの展開を試みると
134+
unfold instInterSet
135+
136+
-- 振り出しに戻ってしまう！
137+
show True ∨ (s ∩ u = u ∩ s)
138+
139+
left; trivial

‎Examples/Tactic/Simp.lean

-4
Original file line numberDiff line numberDiff line change
@@ -125,10 +125,6 @@ example {x y : Nat} : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := by
125125
126126
`simp_all` は `simp [*] at *` の強化版で，ローカルコンテキストとゴールをこれ以上単純化できなくなるまですべて単純化します．
127127
128-
## dsimp
129-
130-
`dsimp` は，定義上(definitionally)等しいもの同士しか単純化しないという制約付きの `simp` です．
131-
132128
## simps 属性
133129
補題を `simp` で使えるようにするのは `@[simp]` タグを付けることで可能ですが，`simps` 属性(または `@[simps]` タグ)を利用すると `simp` で使用するための補題を自動的に生成してくれます．これは Mathlib で定義されている機能であり，使用するには `Mathlib.Tactic.Basic` の読み込みが必要です．
134130

‎Examples/Tactic/Unfold.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
55
何も指定しなければゴールを変形しようとします．ローカルコンテキストにある項 `h` について展開を行うには，`unfold ... at h` のように `at` を付けます．
66
7-
[`simp`](./Simp.md) の派生である `dsimp` タクティクを使っても同様のことができます． -/
7+
[`dsimp`](./Dsimp.md) タクティクを使っても同様のことができます．基本的に `dsimp` を使用することが推奨されます．-/
88

99
def myFun (n : Nat) : Nat :=
1010
n + 1

‎src/SUMMARY.md

+1
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,7 @@
6767
- [convert: 惜しい補題を使う](./Tactic/Convert.md)
6868
- [decide: 決定可能な命題を示す](./Tactic/Decide.md)
6969
- [done: 証明終了を宣言](./Tactic/Done.md)
70+
- [dsimp: 定義に展開](./Tactic/Dsimp.md)
7071
- [exact: 証明を直接構成](./Tactic/Exact.md)
7172
- [exact?: exact できるか検索](./Tactic/ExactQuestion.md)
7273
- [exfalso: 矛盾を示すことに帰着](./Tactic/Exfalso.md)

0 commit comments

Comments
 (0)