Testing if tactics work

Stream: metaprogramming / tactics

[Siddhartha Gadgil]

I need to test whether a tactic sequence can run and close a goal programmatically. I am trying to do this using Elab.runTactic but it seems to fail. The following is a minimal example: the first statement uses the same tactics in the interpreter and the other tries in a meta-function giving an error:

theorem eg₁ : ∀ (a : Nat), Nat.succ a = Nat.zero → False := by
  intro a h; exact (Eq.mpr (congrArg (fun _a ↦ match _a with | Nat.zero => True | Nat.succ a => False) h) True.intro)

open Lean Meta Elab Term Tactic Parser.Tactic
def chkTacticSeq (type: Expr)(tacs : TSyntax ``tacticSeq):
  TermElabM Unit :=
  do
  try
    let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
    let _ ← Elab.runTactic mvar.mvarId! tacs
    return
  catch e =>
    throwError "Error: {e.toMessageData}"


def testEg : TermElabM Unit := do
  let type ← elabType <| ← `(∀ (a : Nat), Nat.succ a = Nat.zero → False)
  let pf ← `(tacticSeq| intro a h; exact (Eq.mpr (congrArg (fun _a ↦ match _a with | Nat.zero => True | Nat.succ a => False) h) True.intro))
  chkTacticSeq type pf

#eval testEg /- Error: application type mismatch
  Eq.mpr (congrArg (fun _a ↦ sorryAx Prop true) h✝)
argument
  congrArg (fun _a ↦ sorryAx Prop true) h✝
has type
  sorryAx Prop true = sorryAx Prop true : Prop
but is expected to have type
  False = True : Prop -/

[Siddhartha Gadgil]

Any help is appreciated.

[Siddhartha Gadgil]

I am using similar code quite a lot, and this seems to be something to do with the intro tactics specifically.

[Damiano Testa]

I'm not at lean now, but the sorryAx look like lean made up some syntax that it did not understand from your code. Could using mkIdent profusely help?

[Damiano Testa]

In fact, try doing just one intro but with intro $(mkIdent `a) (untested).

[Mario Carneiro]

when I run your code I get the following message, in addition to the mentioned type error:

<CoreM>:0:0: error: auxiliary declaration cannot be created when declaration name is not available

I believe it's complaining that match can't construct the auxiliary definition because the declaration name is not set

[Mario Carneiro]

The other issue is that even if you do have a declaration name set, runTactic is in MetaM and does not propagate the setting. This works:

    let _ ← Elab.runTactic mvar.mvarId! tacs (← read) (← get)
...
#eval withDeclName `foo testEg

[Siddhartha Gadgil]

For the same goal, I am trying to construct an argument (motive := motive) for a term. How do I do this. Stuff like

let stx ← `(($y:term := $y:term))
```  did not work