Extract problematic goal out

Proofs/AES-GCM/GCMInitV8Sym.lean

@@ -7,6 +7,7 @@ import Arm.BitVec
 import Proofs.«AES-GCM».GCMInitV8Pre
 import Tactics.Sym
 import Tactics.Aggregate
+import Tactics.ExtractGoal
 import Specs.GCMV8
 
 namespace GCMInitV8Program
@@ -33,9 +34,11 @@ theorem gcm_init_v8_program_run_152 (s0 sf : ArmState)
   sym_n 152
   done
 
-set_option maxRecDepth 1000000 in
-set_option maxHeartbeats 2000000 in
-set_option sat.timeout 180 in
+set_option maxRecDepth 100000 in
+set_option maxHeartbeats 500000 in
+set_option sat.timeout 120 in
+set_option pp.deepTerms true in
+set_option pp.maxSteps 10000 in
 -- set_option linter.unusedVariables false in
 -- set_option profiler true in
 theorem gcm_init_v8_program_correct (s0 sf : ArmState)
@@ -44,7 +47,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState)
     (h_s0_pc : read_pc s0 = gcm_init_v8_program.min)
     (h_s0_sp_aligned : CheckSPAlignment s0)
     (h_run : sf = run gcm_init_v8_program.length s0)
-    (_h_mem : Memory.Region.pairwiseSeparate
+    (h_mem : Memory.Region.pairwiseSeparate
       [ ⟨(H_addr s0), 128⟩,
         ⟨(Htable_addr s0), 2048⟩ ])
     : -- effects
@@ -110,4 +113,6 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState)
       Nat.zero_mod, Nat.zero_add, Nat.sub_zero, Nat.mul_one, Nat.zero_mul, Nat.one_mul,
       Nat.reduceSub, BitVec.reduceMul, BitVec.reduceXOr, BitVec.mul_one, Nat.add_one_sub_one,
       BitVec.one_mul]
-    bv_decide
+    extract_goal
+    sorry
+    -- bv_decide

Tactics.lean

@@ -10,3 +10,4 @@ import «Tactics».StepThms
 import «Tactics».Rename
 import «Tactics».Name
 import «Tactics».ClearNamed
+import «Tactics».ExtractGoal

Tactics/ExtractGoal.lean

@@ -0,0 +1,171 @@
+/-
+Copyright (c) 2017 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Hudon, Kyle Miller, Damiano Testa
+-/
+import Lean.Elab.Tactic.ElabTerm
+import Lean.Meta.Tactic.Cleanup
+import Lean.PrettyPrinter
+import Batteries.Lean.Meta.Inaccessible
+
+/-!
+#  `extract_goal`: Format the current goal as a stand-alone example
+
+Useful for testing tactics or creating
+[minimal working examples](https://leanprover-community.github.io/mwe.html).
+
+```lean
+example (i j k : Nat) (h₀ : i ≤ j) (h₁ : j ≤ k) : i ≤ k := by
+  extract_goal
+
+/-
+theorem extracted_1 (i j k : Nat) (h₀ : i ≤ j) (h₁ : j ≤ k) : i ≤ k := sorry
+-/
+```
+
+* TODO: Add tactic code actions?
+* Output may produce lines with more than 100 characters
+
+### Caveat
+
+Tl;dr: sometimes, using `set_option [your pp option] in extract_goal` may work where `extract_goal`
+does not.
+
+The extracted goal may depend on imports and `pp` options, since it relies on delaboration.
+For this reason, the extracted goal may not be equivalent to the given goal.
+However, the tactic responds to pretty printing options.
+For example, calling `set_option pp.all true in extract_goal` in the examples below actually works.
+
+```lean
+-- `theorem int_eq_nat` is the output of the `extract_goal` from the example below
+-- the type ascription is removed and the `↑` is replaced by `Int.ofNat`:
+-- Lean infers the correct (false) statement
+theorem int_eq_nat {z : Int} : ∃ n, Int.ofNat n = z := sorry
+
+example {z : Int} : ∃ n : Nat, ↑n = z := by
+  extract_goal  -- produces `int_eq_nat`
+  apply int_eq_nat  -- works
+```
+
+However, importing `Batteries.Classes.Cast`, makes `extract_goal` produce a different theorem
+
+```lean
+import Batteries.Classes.Cast
+
+-- `theorem extracted_1` is the output of the `extract_goal` from the example below
+-- the type ascription is erased and the `↑` is untouched:
+-- Lean infers a different statement, since it fills in `↑` with `id` and uses `n : Int`
+theorem extracted_1 {z : Int} : ∃ n, ↑n = z := ⟨_, rfl⟩
+
+example {z : Int} : ∃ n : Nat, ↑n = z := by
+  extract_goal
+  apply extracted_1
+/-
+tactic 'apply' failed, failed to unify
+  ∃ n, n = ?z
+with
+  ∃ n, ↑n = z
+z: Int
+⊢ ∃ n, ↑n = z
+-/
+```
+
+Similarly, the extracted goal may fail to type-check:
+```lean
+example (a : α) : ∃ f : α → α, f a = a := by
+  extract_goal
+  exact ⟨id, rfl⟩
+
+theorem extracted_1.{u_1} {α : Sort u_1} (a : α) : ∃ f, f a = a := sorry
+-- `f` is uninterpreted: `⊢ ∃ f, sorryAx α true = a`
+```
+and also
+```lean
+import Mathlib.Algebra.Polynomial.Basic
+
+--  The `extract_goal` below produces this statement:
+theorem extracted_1 : X = X := sorry
+-- Yet, Lean is unable to figure out what is the coefficients Semiring for `X`
+/-
+typeclass instance problem is stuck, it is often due to metavariables
+  Semiring ?m.28495
+-/
+
+example : (X : Nat[X]) = X := by
+  extract_goal
+```
+-/
+
+namespace Mathlib.Tactic.ExtractGoal
+
+open Lean Elab Tactic Meta
+
+/-- Have `extract_goal` extract the full local context. -/
+syntax star := "*"
+
+/-- Configuration for `extract_goal` for which variables from the context to include. -/
+syntax config := star <|> (colGt ppSpace ident)*
+
+/--
+- `extract_goal` formats the current goal as a stand-alone theorem or definition after
+  cleaning up the local context of irrelevant variables.
+  A variable is *relevant* if (1) it occurs in the target type, (2) there is a relevant variable
+  that depends on it, or (3) the type of the variable is a proposition that depends on a
+  relevant variable.
+
+  If the target is `False`, then for convenience `extract_goal` includes all variables.
+- `extract_goal *` formats the current goal without cleaning up the local context.
+- `extract_goal a b c ...` formats the current goal after removing everything that the given
+  variables `a`, `b`, `c`, ... do not depend on.
+- `extract_goal ... using name` uses the name `name` for the theorem or definition rather than
+  the autogenerated name.
+
+The tactic tries to produce an output that can be copy-pasted and just work,
+but its success depends on whether the expressions are amenable
+to being unambiguously pretty printed.
+
+The tactic responds to pretty printing options.
+For example, `set_option pp.all true in extract_goal` gives the `pp.all` form.
+-/
+syntax (name := extractGoal) "extract_goal" config (" using " ident)? : tactic
+
+elab_rules : tactic
+  | `(tactic| extract_goal $cfg:config $[using $name?]?) => do
+    let name ← if let some name := name?
+                then pure name.getId
+                else mkAuxName ((← getCurrNamespace) ++ `extracted) 1
+    let msg ← withoutModifyingEnv <| withoutModifyingState do
+      let g ← getMainGoal
+      let g ← do match cfg with
+        | `(config| *) => pure g
+        | `(config| ) =>
+          if (← g.getType >>= instantiateMVars).consumeMData.isConstOf ``False then
+            -- In a contradiction proof, it is not very helpful to clear all hypotheses!
+            pure g
+          else
+            g.cleanup
+        | `(config| $fvars:ident*) =>
+          -- Note: `getFVarIds` does `withMainContext`
+          g.cleanup (toPreserve := (← getFVarIds fvars)) (indirectProps := false)
+        | _ => throwUnsupportedSyntax
+      let (g, _) ← g.renameInaccessibleFVars
+      let (_, g) ← g.revert (clearAuxDeclsInsteadOfRevert := true) (← g.getDecl).lctx.getFVarIds
+      let ty ← instantiateMVars (← g.getType)
+      if ty.hasExprMVar then
+        -- TODO: turn metavariables into new hypotheses?
+        throwError "Extracted goal has metavariables: {ty}"
+      let ty ← Term.levelMVarToParam ty
+      let seenLevels := collectLevelParams {} ty
+      let levels := (← Term.getLevelNames).filter
+                      fun u => seenLevels.visitedLevel.contains (.param u)
+      addAndCompile <| Declaration.axiomDecl
+        { name := name
+          levelParams := levels
+          isUnsafe := false
+          type := ty }
+      let sig ← addMessageContext <| MessageData.signature name
+      let cmd := if ← Meta.isProp ty then "theorem" else "def"
+      pure m!"{cmd} {sig} := sorry"
+    logInfo msg
+
+end Mathlib.Tactic.ExtractGoal

lake-manifest.json

@@ -60,6 +60,16 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "lnsym",
  "lakeDir": ".lake"}

lakefile.lean

@@ -45,3 +45,4 @@ lean_exe «lnsym» where
 
 require ELFSage from git "https://github.com/draperlaboratory/ELFSage.git" @ "main"
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "main"