コード例において，仮定やゴールの状態をタクティクで補足する

lean-ja · Sep 24, 2023 · 17e76c0 · 17e76c0
1 parent 9e0cc0c
commit 17e76c0
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 3 deletions.
diff --git a/Examples/Apply.lean b/Examples/Apply.lean
@@ -1,9 +1,11 @@
 -- ANCHOR: first
 -- `P → Q` かつ `P` ならば `Q`
 example (h: P → Q) (hP: P) : Q := by
-  -- ゴールが `P` に変わる
   apply h
 
+  -- ゴールが `P` に変わっている
+  show P
+
   exact hP
 -- ANCHOR_END: first
 

diff --git a/Examples/ByCases.lean b/Examples/ByCases.lean
@@ -1,3 +1,5 @@
+import Std.Tactic.GuardExpr
+
 -- ANCHOR: first
 example (P: Prop) : ¬¬P → P := by
   intro hnnP
@@ -7,9 +9,13 @@ example (P: Prop) : ¬¬P → P := by
 
   case inl =>
     -- `P` が成り立つとき
+    guard_hyp hP : P
+
     assumption
 
   case inr =>
-    -- `P` が成り立たないとき
+    -- `¬ P` が成り立つとき
+    guard_hyp hP : ¬P
+
     contradiction
 -- ANCHOR_END: first
diff --git a/Examples/ByContra.lean b/Examples/ByContra.lean
@@ -6,8 +6,9 @@ example (h: ¬Q → ¬P) : P → Q := by
   -- `P` であると仮定する
   intro hP
 
-  -- `¬Q` であると仮定する
+  -- `¬Q` であると仮定して矛盾を導きたい
   by_contra hnQ
+  show False
 
   -- `¬ Q → ¬ P` と `¬Q` から `¬P` が導かれる
   have := h hnQ

diff --git a/Examples/Intro.lean b/Examples/Intro.lean
@@ -3,6 +3,9 @@ example (hPQ: P → Q) (hQR: Q → R) : P → R := by
   -- 示したいことが `P → R` なので，`P` だと仮定する
   intro hP
 
+  -- `R` を示したい
+  show R
+
   -- 仮定 `hPQ : P → Q` と `hP : P` から `Q` が導かれる
   have hQ : Q := hPQ hP
 
@@ -17,6 +20,9 @@ example (P Q : Nat → Prop) (h : ∀ n, P n ↔ Q n) : ∀ y, P (y + 1) → Q (
   -- そして `P (y + 1) → Q(y + 1)` を示したいので，`P (y + 1)` を仮定する
   intro y hyP
 
+  -- `Q (y + 1)` を示せば良い
+  show Q (y + 1)
+
   -- 同値を使ってゴールを書き換える
   rw [← h]
 
@@ -32,6 +38,9 @@ example (h: P → Q) : ¬Q → ¬P := by
   -- さらに `intro` を行って仮定 `hP : P` を導入する
   intro hnQ hP
 
+  -- 矛盾を示したい
+  show False
+
   -- `hP : P` と `h : P → Q` から `Q` が導かれる
   have hQ : Q := h hP