From be2038e9029212244b37770434c627011f9897e5 Mon Sep 17 00:00:00 2001
From: 0x182d4454fb211940 <ianwoodformal@gmail.com>
Date: Thu, 28 Jul 2022 09:41:32 +0100
Subject: [PATCH 1/6] feat(tactic/expand_exists): parse docstrings, absolute
 names

---
 src/tactic/expand_exists.lean | 28 +++++++++++++++++++++++++---
 1 file changed, 25 insertions(+), 3 deletions(-)

diff --git a/src/tactic/expand_exists.lean b/src/tactic/expand_exists.lean
index 9d3a8e62c899b..2b95761af2813 100644
--- a/src/tactic/expand_exists.lean
+++ b/src/tactic/expand_exists.lean
@@ -27,11 +27,33 @@ lemma it_spec (n : ℕ) : n < it n := classical.some_spec (it_exists n)
 -/
 
 namespace tactic
+setup_tactic_parser
 
 open expr
 
 namespace expand_exists
 
+@[derive has_reflect]
+meta structure arg :=
+(is_root : bool)
+(name : name)
+(docstring : option string)
+
+meta def parse_docstring : parser $ (option string) :=
+do
+  pe <- parser.pexpr,
+  e <- to_expr pe,
+  val <- some <$> eval_expr string e,
+  return val
+
+meta def parse_arg : parser arg :=
+do
+  is_root <- option.is_some <$> (tk "@")?,
+  name <- ident,
+  is_docstring <- option.is_some <$> (tk "=")?,
+  doc <- if is_docstring then parse_docstring else pure none,
+  return ⟨is_root, name, doc⟩
+
 /--
 Data known when parsing pi expressions.
 
@@ -197,11 +219,11 @@ Note that without the last argument `nat_greater_nonzero`, `nat_greater_lt` woul
 ```
 -/
 @[user_attribute]
-meta def expand_exists_attr : user_attribute unit (list name) :=
+meta def expand_exists_attr : user_attribute unit (list expand_exists.arg) :=
 { name := "expand_exists",
   descr := "From a proof that (a) value(s) exist(s) with certain properties, "
   ++ "constructs (an) instance(s) satisfying those properties.",
-  parser := lean.parser.many lean.parser.ident,
+  parser := expand_exists.parse_arg*,
   after_set := some $ λ decl prio persistent, do
     d <- get_decl decl,
     names <- expand_exists_attr.get_param decl,
@@ -210,7 +232,7 @@ meta def expand_exists_attr : user_attribute unit (list name) :=
       decl := λ is_t n ty val, (tactic.to_expr val >>= λ val,
         tactic.add_decl (if is_t then declaration.thm n d.univ_params ty (pure val)
           else declaration.defn n d.univ_params ty val default tt)),
-      names := names } d.type }
+      names := sorry } d.type }
 
 add_tactic_doc
 { name := "expand_exists",

From 715a24f1fa6ba16d7317b8a536330987d541888c Mon Sep 17 00:00:00 2001
From: 0x182d4454fb211940 <ianwoodformal@gmail.com>
Date: Thu, 28 Jul 2022 10:07:15 +0100
Subject: [PATCH 2/6] feat(tactic/expand_exists): apply parsed arguments

---
 src/tactic/expand_exists.lean | 54 +++++++++++++++++++----------------
 1 file changed, 30 insertions(+), 24 deletions(-)

diff --git a/src/tactic/expand_exists.lean b/src/tactic/expand_exists.lean
index 2b95761af2813..0f848efeb9975 100644
--- a/src/tactic/expand_exists.lean
+++ b/src/tactic/expand_exists.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ian Wood
 -/
 import meta.expr
+import tactic.core
 
 /-!
 # `expand_exists`
@@ -57,12 +58,12 @@ do
 /--
 Data known when parsing pi expressions.
 
-`decl`'s arguments are: is_theorem, name, type, value.
+`decl`'s arguments are: is_theorem, arg, type, value.
 -/
 meta structure parse_ctx :=
 (original_decl : declaration)
-(decl : bool → name → expr → pexpr → tactic unit)
-(names : list name)
+(decl : bool → arg → expr → pexpr → tactic name)
+(args : list arg)
 (pis_depth : ℕ := 0)
 
 /--
@@ -108,26 +109,27 @@ meta def parse_one_prop (ctx : parse_ctx_props) (p : expr) : tactic unit :=
 do
   let p : expr := instantiate_exists_decls { ..ctx } p,
   let val : pexpr := ctx.project_proof ctx.spec_chain,
-  n <- match ctx.names with
-  | [n] := return n
+  a <- match ctx.args with
+  | [a] := return a
   | [] := fail "missing name for proposition"
   | _ := fail "too many names for propositions (are you missing an and?)"
   end,
-  ctx.decl true n p val
+  ctx.decl true a p val,
+  skip
 
 /--
 Parses a proposition and decides if it should be broken down (eg `P ∧ Q` -> `P` and `Q`) depending
-on how many `names` are left. Then creates the associated specification proof(s).
+on how many `args` are left. Then creates the associated specification proof(s).
 -/
 meta def parse_props : parse_ctx_props → expr → tactic unit
 | ctx (app (app (const "and" []) p) q) := do
-  match ctx.names with
-  | [n] := parse_one_prop ctx (app (app (const `and []) p) q)
-  | (n :: tail) :=
-    parse_one_prop { names := [n],
+  match ctx.args with
+  | [a] := parse_one_prop ctx (app (app (const `and []) p) q)
+  | (a :: tail) :=
+    parse_one_prop { args := [a],
       project_proof := (λ p, (const `and.left []) p) ∘ ctx.project_proof,
       ..ctx } p
-    >> parse_props { names := tail,
+    >> parse_props { args := tail,
       project_proof := (λ p, (const `and.right []) p) ∘ ctx.project_proof,
       ..ctx } q
   | [] := fail "missing name for proposition"
@@ -142,18 +144,18 @@ meta def parse_exists : parse_ctx_exists → expr → tactic unit
 | ctx (app (app (const "Exists" [lvl]) type) (lam var_name bi var_type body)) := do
   /- TODO: Is this needed, and/or does this create issues? -/
   (if type = var_type then tactic.skip else tactic.fail "exists types should be equal"),
-  ⟨n, names⟩ <- match ctx.names with
-  | (n :: tail) := return (n, tail)
+  ⟨a, args⟩ <- match ctx.args with
+  | (a :: tail) := return (a, tail)
   | [] := fail "missing name for exists"
   end,
   -- Type may be dependant on earlier arguments.
   let type := instantiate_exists_decls ctx type,
   let value : pexpr := (const `classical.some [lvl]) ctx.spec_chain,
-  ctx.decl false n type value,
+  decl_name <- ctx.decl false a type value,
 
-  let exists_decls := ctx.exists_decls.concat n,
+  let exists_decls := ctx.exists_decls.concat decl_name,
   let some_spec : pexpr := (const `classical.some_spec [lvl]) ctx.spec_chain,
-  let ctx : parse_ctx_exists := { names := names,
+  let ctx : parse_ctx_exists := { args := args,
     spec_chain := some_spec,
     exists_decls := exists_decls,
     ..ctx },
@@ -166,8 +168,8 @@ Parses a `∀ (a : α), p a`. If `p` is not a pi expression, it will call `parse
 meta def parse_pis : parse_ctx → expr → tactic unit
 | ctx (pi n bi ty body) :=
   -- When making a declaration, wrap in an equivalent pi expression.
-  let decl := (λ is_theorem name type val,
-    ctx.decl is_theorem name (pi n bi ty type) (lam n bi (to_pexpr ty) val)) in
+  let decl := (λ is_theorem arg type val,
+    ctx.decl is_theorem arg (pi n bi ty type) (lam n bi (to_pexpr ty) val)) in
   parse_pis { decl := decl, pis_depth := ctx.pis_depth + 1, ..ctx } body
 | ctx (app (app (const "Exists" [lvl]) type) p) :=
   let with_args := (λ (e : expr),
@@ -226,13 +228,17 @@ meta def expand_exists_attr : user_attribute unit (list expand_exists.arg) :=
   parser := expand_exists.parse_arg*,
   after_set := some $ λ decl prio persistent, do
     d <- get_decl decl,
-    names <- expand_exists_attr.get_param decl,
+    args <- expand_exists_attr.get_param decl,
     expand_exists.parse_pis
     { original_decl := d,
-      decl := λ is_t n ty val, (tactic.to_expr val >>= λ val,
-        tactic.add_decl (if is_t then declaration.thm n d.univ_params ty (pure val)
-          else declaration.defn n d.univ_params ty val default tt)),
-      names := sorry } d.type }
+      decl := (λ is_t a ty val, do
+        let name := if a.is_root then a.name else d.to_name.get_prefix ++ a.name,
+        val <- tactic.to_expr val,
+        decl <- tactic.add_decl $ if is_t then declaration.thm name d.univ_params ty (pure val)
+          else declaration.defn name d.univ_params ty val default tt,
+        a.docstring.mmap $ tactic.add_doc_string name,
+        return name),
+      args := args } d.type }
 
 add_tactic_doc
 { name := "expand_exists",

From 0154d673d0a99b8935f167e37831e67bc3633736 Mon Sep 17 00:00:00 2001
From: 0x182d4454fb211940 <ianwoodformal@gmail.com>
Date: Thu, 28 Jul 2022 10:19:37 +0100
Subject: [PATCH 3/6] test(tactic/expand_exists): add tests for docstring and
 namespaces

---
 test/expand_exists.lean | 48 ++++++++++++++++++++++++++++++-----------
 1 file changed, 35 insertions(+), 13 deletions(-)

diff --git a/test/expand_exists.lean b/test/expand_exists.lean
index 852e8fd132dfd..7aff0e41d220b 100644
--- a/test/expand_exists.lean
+++ b/test/expand_exists.lean
@@ -9,18 +9,17 @@ import tactic.expand_exists
 @[expand_exists nat_greater nat_greater_spec]
 lemma nat_greater_exists (n : ℕ) : ∃ m : ℕ, n < m := ⟨n + 1, by fconstructor⟩
 
-noncomputable def nat_greater_res : ℕ → ℕ := nat_greater
-lemma nat_greater_spec_res : ∀ (n : ℕ), n < nat_greater n := nat_greater_spec
+noncomputable example : ℕ → ℕ := nat_greater
+example : ∀ (n : ℕ), n < nat_greater n := nat_greater_spec
 
 @[expand_exists dependent_type dependent_type_val dependent_type_spec]
 lemma dependent_type_exists {α : Type*} (a : α) : ∃ {β : Type} (b : β), (a, b) = (a, b) :=
 ⟨unit, (), rfl⟩
 
-def dependent_type_res {α : Type*} (a : α) : Type := dependent_type a
-noncomputable def dependent_type_val_res {α : Type*} (a : α) : dependent_type a :=
-dependent_type_val a
-lemma dependent_type_spec_res
-{α : Type*} (a : α) : (a, dependent_type_val a) = (a, dependent_type_val a) := dependent_type_spec a
+example {α : Type*} (a : α) : Type := dependent_type a
+noncomputable example {α : Type*} (a : α) : dependent_type a := dependent_type_val a
+example {α : Type*} (a : α) : (a, dependent_type_val a) = (a, dependent_type_val a) :=
+dependent_type_spec a
 
 @[expand_exists nat_greater_nosplit nat_greater_nosplit_spec,
   expand_exists nat_greater_split nat_greater_split_lt nat_greater_split_neq]
@@ -31,11 +30,34 @@ lemma nat_greater_exists₂ (n : ℕ) : ∃ m : ℕ, n < m ∧ m ≠ 0 := begin
   finish,
 end
 
-noncomputable def nat_greater_nosplit_res : ℕ → ℕ := nat_greater_nosplit
-noncomputable def nat_greater_split_res : ℕ → ℕ := nat_greater_split
+noncomputable example : ℕ → ℕ := nat_greater_nosplit
+noncomputable example : ℕ → ℕ := nat_greater_split
 
-lemma nat_greater_nosplit_spec_res :
-∀ (n : ℕ), n < nat_greater_nosplit n ∧ nat_greater_nosplit n ≠ 0 := nat_greater_nosplit_spec
+example : ∀ (n : ℕ), n < nat_greater_nosplit n ∧ nat_greater_nosplit n ≠ 0 :=
+nat_greater_nosplit_spec
 
-lemma nat_greater_split_spec_lt_res : ∀ (n : ℕ), n < nat_greater_nosplit n := nat_greater_split_lt
-lemma nat_greater_split_spec_neq_res : ∀ (n : ℕ), nat_greater_nosplit n ≠ 0 := nat_greater_split_neq
+example : ∀ (n : ℕ), n < nat_greater_nosplit n := nat_greater_split_lt
+example : ∀ (n : ℕ), nat_greater_nosplit n ≠ 0 := nat_greater_split_neq
+
+@[expand_exists a_doc_string="test" no_doc_string again_a_doc_string="test"]
+lemma doc_string_test (n : ℕ) : ∃ (a b : ℕ), a = b := ⟨n, n, rfl⟩
+
+noncomputable example : ℕ → ℕ := a_doc_string
+noncomputable example : ℕ → ℕ := no_doc_string
+example (n : ℕ) : a_doc_string n = no_doc_string n := again_a_doc_string n
+
+namespace foo
+namespace bar
+inductive baz
+| a : baz
+| b : baz → baz
+
+@[expand_exists in_bar @foo.in_foo @in_root]
+lemma namespace_test (x : baz) : ∃ (y z : baz), x.b = y ∧ y = z := ⟨x.b, x.b, rfl, rfl⟩
+
+end bar
+end foo
+
+noncomputable example : foo.bar.baz → foo.bar.baz := foo.bar.in_bar
+noncomputable example : foo.bar.baz → foo.bar.baz := foo.in_foo
+example (x : foo.bar.baz) : x.b = foo.bar.in_bar x ∧ foo.bar.in_bar x = foo.in_foo x := in_root x

From 1c81d260446d67e1c49159fd173843717c1e9596 Mon Sep 17 00:00:00 2001
From: 0x182d4454fb211940 <ianwoodformal@gmail.com>
Date: Thu, 28 Jul 2022 10:27:51 +0100
Subject: [PATCH 4/6] doc(tactic/expand_exists): document namespace & docstring

---
 src/tactic/expand_exists.lean | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/src/tactic/expand_exists.lean b/src/tactic/expand_exists.lean
index 0f848efeb9975..dc5d8eef2bf3c 100644
--- a/src/tactic/expand_exists.lean
+++ b/src/tactic/expand_exists.lean
@@ -219,6 +219,32 @@ Note that without the last argument `nat_greater_nonzero`, `nat_greater_lt` woul
 ```lean
 #check nat_greater_lt -- nat_greater_lt : ∀ (n : ℕ), n < nat_greater n ∧ nat_greater n ≠ 0
 ```
+
+All definitions will be created in the same namespace as the `exists` lemma. You can prepend the
+name with `@` to create it in the root namespace:
+
+```lean
+namespace foo
+@[expand_exists @a b]
+lemma a_exists : ∃ (a : α), a = a := ...
+end foo
+
+#check a     -- α
+#check foo.b -- a = a
+```
+
+A docstring can be added either using `add_decl_doc` after the lemma, or by appending `="..."` to
+the name:
+
+```lean
+@[expand_exists foo="a foo with property bar" bar]
+lemma foo_exists : ∃ (f : foo), bar f := ...
+
+/--
+the property satisfied by foo
+-/
+add_decl_doc bar
+```
 -/
 @[user_attribute]
 meta def expand_exists_attr : user_attribute unit (list expand_exists.arg) :=

From f7efac2f2c1b5266ada1083465e1bedd5f864f62 Mon Sep 17 00:00:00 2001
From: 0x182d4454fb211940 <ianwoodformal@gmail.com>
Date: Thu, 28 Jul 2022 19:33:09 +0100
Subject: [PATCH 5/6] feat(tactic/expand_exists): use `_root_` instead of `@`

---
 src/tactic/expand_exists.lean | 19 +++++++++++++------
 test/expand_exists.lean       |  2 +-
 2 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/src/tactic/expand_exists.lean b/src/tactic/expand_exists.lean
index dc5d8eef2bf3c..c5e7ca94bf81b 100644
--- a/src/tactic/expand_exists.lean
+++ b/src/tactic/expand_exists.lean
@@ -34,12 +34,17 @@ open expr
 
 namespace expand_exists
 
+/--
+Argument for `expand_exists`, containing a `name` and may contain a docstring.
+-/
 @[derive has_reflect]
 meta structure arg :=
-(is_root : bool)
 (name : name)
 (docstring : option string)
 
+/--
+Try to parse a string.
+-/
 meta def parse_docstring : parser $ (option string) :=
 do
   pe <- parser.pexpr,
@@ -47,13 +52,15 @@ do
   val <- some <$> eval_expr string e,
   return val
 
+/--
+Parse an argument
+-/
 meta def parse_arg : parser arg :=
 do
-  is_root <- option.is_some <$> (tk "@")?,
   name <- ident,
   is_docstring <- option.is_some <$> (tk "=")?,
   doc <- if is_docstring then parse_docstring else pure none,
-  return ⟨is_root, name, doc⟩
+  return ⟨name, doc⟩
 
 /--
 Data known when parsing pi expressions.
@@ -221,11 +228,11 @@ Note that without the last argument `nat_greater_nonzero`, `nat_greater_lt` woul
 ```
 
 All definitions will be created in the same namespace as the `exists` lemma. You can prepend the
-name with `@` to create it in the root namespace:
+name with `_root_` to create it in the root namespace:
 
 ```lean
 namespace foo
-@[expand_exists @a b]
+@[expand_exists _root_.a b]
 lemma a_exists : ∃ (a : α), a = a := ...
 end foo
 
@@ -258,7 +265,7 @@ meta def expand_exists_attr : user_attribute unit (list expand_exists.arg) :=
     expand_exists.parse_pis
     { original_decl := d,
       decl := (λ is_t a ty val, do
-        let name := if a.is_root then a.name else d.to_name.get_prefix ++ a.name,
+        let name := d.to_name.get_prefix.append_namespace a.name,
         val <- tactic.to_expr val,
         decl <- tactic.add_decl $ if is_t then declaration.thm name d.univ_params ty (pure val)
           else declaration.defn name d.univ_params ty val default tt,
diff --git a/test/expand_exists.lean b/test/expand_exists.lean
index 7aff0e41d220b..9e96c6f0ac66c 100644
--- a/test/expand_exists.lean
+++ b/test/expand_exists.lean
@@ -52,7 +52,7 @@ inductive baz
 | a : baz
 | b : baz → baz
 
-@[expand_exists in_bar @foo.in_foo @in_root]
+@[expand_exists in_bar _root_.foo.in_foo _root_.in_root]
 lemma namespace_test (x : baz) : ∃ (y z : baz), x.b = y ∧ y = z := ⟨x.b, x.b, rfl, rfl⟩
 
 end bar

From 46abb216a874999454936de2ad2c1a696cc09a8f Mon Sep 17 00:00:00 2001
From: 0x182d4454fb211940 <ianwoodformal@gmail.com>
Date: Sat, 30 Jul 2022 19:25:07 +0100
Subject: [PATCH 6/6] feat(tactic/expand_exists): replace syntax with proposed
 list syntax

---
 src/tactic/expand_exists.lean | 30 ++++++++++++++++++------------
 test/expand_exists.lean       |  2 +-
 2 files changed, 19 insertions(+), 13 deletions(-)

diff --git a/src/tactic/expand_exists.lean b/src/tactic/expand_exists.lean
index c5e7ca94bf81b..104085cf0c2aa 100644
--- a/src/tactic/expand_exists.lean
+++ b/src/tactic/expand_exists.lean
@@ -43,25 +43,30 @@ meta structure arg :=
 (docstring : option string)
 
 /--
-Try to parse a string.
+Maybe parse a string.
 -/
-meta def parse_docstring : parser $ (option string) :=
-do
-  pe <- parser.pexpr,
+meta def parse_docstring : parser $ option string :=
+parser.pexpr?
+>>= option.mmap (λ pe, do
   e <- to_expr pe,
-  val <- some <$> eval_expr string e,
-  return val
+  eval_expr string e)
 
 /--
-Parse an argument
+Parse an argument in list form.
 -/
 meta def parse_arg : parser arg :=
 do
   name <- ident,
-  is_docstring <- option.is_some <$> (tk "=")?,
-  doc <- if is_docstring then parse_docstring else pure none,
+  doc <- parse_docstring,
   return ⟨name, doc⟩
 
+/--
+Parse arguments, either a space-separated list of lemma names, or a comma-separated list of lemma
+names, potentially with docstrings.
+-/
+meta def parse_args : parser $ list arg :=
+(list_of parse_arg) <|> list.map (λ x, ⟨x, none⟩) <$> ident*
+
 /--
 Data known when parsing pi expressions.
 
@@ -240,11 +245,12 @@ end foo
 #check foo.b -- a = a
 ```
 
-A docstring can be added either using `add_decl_doc` after the lemma, or by appending `="..."` to
+You can also write the definition names in list form. This also allows you to specify docstrings in
+the attribute. Alternantively, you can use `add_decl_doc` to do this.
 the name:
 
 ```lean
-@[expand_exists foo="a foo with property bar" bar]
+@[expand_exists [foo "a foo with property bar", bar]]
 lemma foo_exists : ∃ (f : foo), bar f := ...
 
 /--
@@ -258,7 +264,7 @@ meta def expand_exists_attr : user_attribute unit (list expand_exists.arg) :=
 { name := "expand_exists",
   descr := "From a proof that (a) value(s) exist(s) with certain properties, "
   ++ "constructs (an) instance(s) satisfying those properties.",
-  parser := expand_exists.parse_arg*,
+  parser := expand_exists.parse_args,
   after_set := some $ λ decl prio persistent, do
     d <- get_decl decl,
     args <- expand_exists_attr.get_param decl,
diff --git a/test/expand_exists.lean b/test/expand_exists.lean
index 9e96c6f0ac66c..b76702294a4a8 100644
--- a/test/expand_exists.lean
+++ b/test/expand_exists.lean
@@ -39,7 +39,7 @@ nat_greater_nosplit_spec
 example : ∀ (n : ℕ), n < nat_greater_nosplit n := nat_greater_split_lt
 example : ∀ (n : ℕ), nat_greater_nosplit n ≠ 0 := nat_greater_split_neq
 
-@[expand_exists a_doc_string="test" no_doc_string again_a_doc_string="test"]
+@[expand_exists [a_doc_string "test", no_doc_string, again_a_doc_string "test"]]
 lemma doc_string_test (n : ℕ) : ∃ (a b : ℕ), a = b := ⟨n, n, rfl⟩
 
 noncomputable example : ℕ → ℕ := a_doc_string