From 46dfe7b911502d2a204a6b6a91b24ddf400f0fe5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 24 Nov 2020 16:56:09 -0800
Subject: [PATCH] doc: expand `tactics.md`

---
 doc/highlight.js |  2 +-
 doc/tactics.md   | 83 +++++++++++++++++++++++++++++++++++++++++++++++-
 2 files changed, 83 insertions(+), 2 deletions(-)

diff --git a/doc/highlight.js b/doc/highlight.js
index 3002b486d1..64c1d36df1 100644
--- a/doc/highlight.js
+++ b/doc/highlight.js
@@ -1118,7 +1118,7 @@ hljs.registerLanguage("lean", function(hljs) {
       'syntax macro_rules macro ' +
       'fun ' +
       '#check #eval #reduce #print ' +
-      'section namespace end',
+      'section namespace end infix prefix ',
     built_in:
       'Type Prop|10 Sort rw|10 rewrite rwa erw subst substs ' +
       'simp dsimp simpa simp_intros finish using generalizing ' +
diff --git a/doc/tactics.md b/doc/tactics.md
index ad93dfaf9a..6898b3fb51 100644
--- a/doc/tactics.md
+++ b/doc/tactics.md
@@ -194,6 +194,87 @@ TODO
 
 TODO
 
+## Dependent pattern matching
+
+The `match-with` expression implements dependent pattern matching. You can use it to create concise proofs.
+
+```lean
+inductive Mem : α → List α → Prop where
+  | head (a : α) (as : List α)   : Mem a (a::as)
+  | tail (a b : α) (bs : List α) : Mem a bs → Mem a (b::bs)
+
+infix:50 "∈" => Mem
+
+theorem memSplit {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a :: t :=
+  match a, as, h with
+  | _, _, Mem.head a bs     => ⟨[], ⟨bs, rfl⟩⟩
+  | _, _, Mem.tail a b bs h =>
+    match bs, memSplit h with
+    | _, ⟨s, ⟨t, rfl⟩⟩ => ⟨b::s, ⟨t, List.consAppend .. ▸ rfl⟩⟩
+```
+
+In the tactic DSL, the right-hand-side of each alternative in a `match-with` is a sequence of tactics instead of a term.
+Here is a similar proof using the tactic DSL.
+
+```lean
+# inductive Mem : α → List α → Prop where
+#  | head (a : α) (as : List α)   : Mem a (a::as)
+#  | tail (a b : α) (bs : List α) : Mem a bs → Mem a (b::bs)
+# infix:50 "∈" => Mem
+theorem memSplit {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a :: t := by
+  match a, as, h with
+  | _, _, Mem.head a bs     => exists []; exists bs; rfl
+  | _, _, Mem.tail a b bs h =>
+    match bs, memSplit h with
+    | _, ⟨s, ⟨t, rfl⟩⟩ =>
+      exists b::s; exists t;
+      rw [List.consAppend]; rfl
+```
+
+We can use `match-with` nested in tactics.
+Here is a similar proof that uses the `induction` tactic instead of recursion.
+
+```lean
+# inductive Mem : α → List α → Prop where
+#  | head (a : α) (as : List α)   : Mem a (a::as)
+#  | tail (a b : α) (bs : List α) : Mem a bs → Mem a (b::bs)
+# infix:50 "∈" => Mem
+theorem memSplit {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a :: t := by
+  induction as with
+  | nil          => cases h
+  | cons b bs ih => cases h with
+    | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
+    | tail a b bs h =>
+      match bs, ih h with
+      | _, ⟨s, ⟨t, rfl⟩⟩ =>
+        exists b::s; exists t
+        rw [List.consAppend]; rfl
+```
+
+You can create your own notation using existing tactics. In the following example,
+we define a simple `obtain` tactic using macros. We say it is simple because it takes only one
+discriminant. Later, we show how to create more complex automation using macros.
+
+```lean
+# inductive Mem : α → List α → Prop where
+#  | head (a : α) (as : List α)   : Mem a (a::as)
+#  | tail (a b : α) (bs : List α) : Mem a bs → Mem a (b::bs)
+# infix:50 "∈" => Mem
+macro "obtain " p:term " from " d:term : tactic =>
+  `(tactic| match $d:term with | $p:term => ?_)
+
+theorem memSplit {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a :: t := by
+  induction as with
+  | cons b bs ih => cases h with
+    | tail a b bs h =>
+      obtain ⟨s, ⟨t, h⟩⟩ from ih h
+      exists b::s; exists t
+      rw [h, List.consAppend]; rfl
+    | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
+  | nil => cases h
+
+```
+
 ## Extensible tactics
 
 In the following example, we define the notation `trivial` for the tactic DSL using
@@ -258,7 +339,7 @@ where
     | 0   => rw [Nat.zeroAdd]; rfl
     | n+1 =>
       show List.length (List.replicate.loop a n (a::as)) = Nat.succ n + as.length
-      rw [aux n, List.lengthConsEq, Nat.addSucc, Nat.succAdd]
+      rw [replicateLoopEq n, List.lengthConsEq, Nat.addSucc, Nat.succAdd]
       rfl
 ```