extractGoal

Stream: metaprogramming / tactics

[Damiano Testa]

As a way of teaching myself some tactic-writing, I have been toying around with extractGoal. Has this tactic already been ported? I could not find it...

[Kyle Miller]

It looks like it hasn't (it's not in std4, mathlib4, nor either of their lists of pending PRs)

[Damiano Testa]

Ok, so I'll give it a try!

[Damiano Testa]

Here is a first attempt: there are some issues, but I don't have more time today!

import Std.Data.List.Basic

open Lean Elab Meta Tactic

def dict : BinderInfo → String × String
  | .default => ("(", ")")
  | .implicit => ("{", "}")
  | .strictImplicit => ("⦃", "⦄")
  | .instImplicit => ("[", "]")

def ppLdecl (d : LocalDecl) : MetaM Format := do
let name := if d.binderInfo.isInstImplicit then f!""
            else
              let prename := d.userName.toString
              (if prename == "this" then f!"_this" else f!"{prename}") ++ f!" : "
let middle := name ++ (← ppExpr d.type)
let (l,r) := dict d.binderInfo
pure (l ++ middle ++ r)

-- TODO: Deal with universes
-- TODO: Deal with `let`
-- TODO: Add tactic code actions?
-- TODO: Deal with named instances
-- TODO: `extractGoal thmName`
elab (name := extractGoal) name:"extractGoal" : tactic => do (← getMainGoal).withContext do
  let ctx ← getLCtx
  let dc := ctx.decls.toList.reduceOption.drop 1
  let names ← dc.mapM fun x => ppLdecl x
  let g ← getMainTarget
  let targ := f!"{← ppExpr g}"
  let bod := ((names.drop 1).foldl (fun x y => x ++ f!"\n    " ++ y) (f!"example " ++ names[0]!)) ++ f!" :\n    " ++ targ
  logInfoAt name (bod ++ f!" := by\n  sorry")

theorem tr1 {α} [Add α] ⦃_g : Int⦄ {s : Nat} {a : Int} {_d : Expr} (_x : Nat) : (s ≠ _x ∧ 74 = 3) ∨ 14 = 0 := by
  have : 3 + 5 = 5 := sorry
  let y : Nat := 37
  extractGoal
/-
example {α : Type u_1}
    [Add α]
    ⦃_g : Int⦄
    {s : Nat}
    {a : Int}
    {_d : Expr}
    (_x : Nat)
    (_this : 3 + 5 = 5)
    (y : Nat) :   -- ok, this requires some work!
    s ≠ _x ∧ 74 = 3 ∨ 14 = 0 := by
  sorry
-/


example : (4 ≠ 6 ∧ 74 = 3) ∨ 14 = 0 := by
  extractGoal
/-
example  :
    4 ≠ 6 ∧ 74 = 3 ∨ 14 = 0 := by
  sorry
-/

[Damiano Testa]

Any comments are really really welcome: I feel like I have no idea what I am doing!

[Damiano Testa]

I have a first PR ready for extractGoal: it does not have the full functionality of what it had in mathlib3, but I would like to get feedback on it.

[Damiano Testa]

What should I do with the copyright headers? I personally do not care, but I also do not know who implemented the mathlib3 version or whether they even want to be associated with the current version!

[Patrick Massot]

I'm pretty sure the Lean 3 version was written by @Simon Hudon

[Damiano Testa]

Ok, so should I leave Simon as copyright and author and add my name to the author's list? I certainly do not intend to give someone else more work, simply because I decided to port this!

[Damiano Testa]

!4#4595

[Damiano Testa]

If the context contains autoimplicit/hygienic Sort/Type/variables, how should extract_goal print them? Currently, this is how I implemented it:

example (n : ℕ) : x = x ∨ n = n := by   -- an autoImplicit `x` and its `Sort`
  cases n   -- to generate a hygienic `n`
  . exact Or.inr rfl
  . extract_goal
    exact Or.inr rfl

-- state at `extract_goal`:
/-
α✝: Sort ?u.266
x: α✝
n✝: ℕ
⊢ x = x ∨ Nat.succ n✝ = Nat.succ n✝
-/

-- `extract_goal` output:
/-
example {α_hyg : Sort univ_α_hyg}
    {x : α_hyg}
    (n_hyg : ℕ) :
    x = x ∨ Nat.succ n_hyg = Nat.succ n_hyg := by
  sorry
-/

Thus, hygienic stuff gets the _hyg suffix, implicit universe levels get a univ_-prefix, followed by the name of the corresponding Sort.

[Kevin Buzzard]

That sounds like a reasonable idea...

[Damiano Testa]

I tried as much as possible to get a copy-pasteable output: the hygienic daggers do not work.

[Mario Carneiro]

there is a function for getting names with _1 etc based on what is in the context. I would just use eraseMacroScopes to get the base name and then add _1 _2 to make them unique if there are overlaps.

[Damiano Testa]

Mario, I am failing to implement your suggestion. In particular, I have been unable to reach universe levels and give them unique names. Below is a #mwe of where I am stuck

import Std.Data.List.Basic

open Lean Elab Meta Tactic LocalContext Name

elab (name := ppOpts) "ppOpts" : tactic => withMainContext do
  let ctx := (← getMainDecl).lctx
  let decls := ctx.decls.toList.reduceOption.drop 1
  let _ := ← decls.mapM (fun d => do
    dbg_trace f!"username:    {d.userName}"
    dbg_trace f!"eraseScopes: {d.userName.eraseMacroScopes}"
    dbg_trace f!"type:        {(← ppExpr d.type)}"
    dbg_trace f!"unused:      {(getUnusedName ctx d.userName.eraseMacroScopes)}\n")

example : x = x ∨ y = y := by
  ppOpts
  exact Or.inl rfl
-- state is
/-
α✝¹: Sort ?u.4531
x: α✝¹
α✝: Sort ?u.4534
y: α✝
⊢ x = x ∨ y = y
-/

-- output of `ppOpts is
/-
username:    α._@.Mathlib.mwe_extractGoal._hyg.423
eraseScopes: α
type:        Sort ?u.4531
unused:      α

username:    x
eraseScopes: x
type:        α✝¹
unused:      x_1

username:    α._@.Mathlib.mwe_extractGoal._hyg.424
eraseScopes: α
type:        Sort ?u.4534
unused:      α

username:    y
eraseScopes: y
type:        α✝
unused:      y_1
-/

Some issues with my code:

• the two autoimplicit Sorts appear to get the same "unused name";
• I do not know how to access the universe levels of their Sorts;
• getUnusedName gives a new name to x and y, whereas using their original names would have been ok.

[Damiano Testa]

I'm no longer at my computer, but I guess that I see now why the unused names are repeated: the variable α is not in context -- the hygienic one is. Thus, it is available as unused. I should maybe recreate the local context with the new declarations, but maybe then the version that I had is not so bad...

The issue with renaming Levels I still cannot figure out.