refine 追加

lean-ja · Sep 24, 2023 · b5de393 · b5de393
1 parent 7fd9b06
commit b5de393
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 0 deletions.
diff --git a/Examples.lean b/Examples.lean
@@ -19,6 +19,7 @@ import Examples.Induction
 import Examples.Intro
 import Examples.LeftRight
 import Examples.Linarith
+import Examples.Refine
 import Examples.Rel
 import Examples.Rfl
 import Examples.Ring

diff --git a/Examples/Refine.lean b/Examples/Refine.lean
@@ -0,0 +1,12 @@
+variable (P Q : Prop)
+
+-- ANCHOR: first
+example (hP: P) (hQ: Q) : P ∧ Q := by
+  -- 穴埋め形式で証明を作ることができる
+  refine ⟨?_, hQ⟩
+
+  -- ゴールが `⊢ P` になる
+  show P
+
+  exact hP
+-- ANCHOR_END: first
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
@@ -28,6 +28,7 @@
 - [intro: 含意→や全称∀を示す](./intro.md)
 - [left, right: 論理和∨を示す](./left_right.md)
 - [linarith: 線形不等式を示す](./linarith.md)
+- [refine: プレースホルダを使う](./refine.md)
 - [rel: 不等式を使う](./rel.md)
 - [rfl: 定義そのまま](./rfl.md)
 - [ring: 環の等式を示す](./ring.md)

diff --git a/src/refine.md b/src/refine.md
@@ -0,0 +1,7 @@
+# refine
+
+`refine` は `exact` と同様に機能しますが，プレースホルダを受け入れて新しいゴールを生成するという違いがあります．
+
+```lean
+{{#include ../Examples/Refine.lean:first}}
+```