Tactic writing

Stream: lean4

[Alice Laroche]

Hello,
I want both state to be equal, but it doesn't happen.
I need to do it through MetaM because other goal will be closed too in future code

import Lean.Meta
import Lean.Elab
import Lean.Meta.Tactic.Rewrite

open Lean Meta Elab Tactic
open Lean.Elab.Term

elab "myTactic " : tactic => do
  liftMetaTactic fun mvarId => do
    let (h, mvarId) <- intro1P mvarId
    let goals <- apply mvarId (mkApp (mkConst ``Or.elim) (mkFVar h))
    return goals



theorem test {p: Prop} : (p ∨ p) -> p := by intro h
                                            apply Or.elim h
                                            trace_state

theorem test' {p: Prop} : (p ∨ p) -> p := by myTactic
                                             trace_state

[Leonardo de Moura]

Note that Or.elim has implicit arguments

#check @Or.elim

So, mkApp (mkConst ``Or.elim) (mkFVar h) is not constructing the term you are expecting.
We have some auxiliary functions for setting the value of implicit arguments (e.g., mkAppM and mkAppOptM). Here is an example:

elab "myTactic " : tactic => do
  liftMetaTactic fun mvarId => do
    let (h, mvarId) <- intro1P mvarId
    let r ← cases mvarId h
    withMVarContext mvarId do
      let goals <- apply mvarId (← mkAppOptM ``Or.elim #[none, none, (← getMVarType mvarId), mkFVar h])
      return goals

You can also use the cases tactic at myTactic. Example:

elab "myTactic " : tactic => do
  liftMetaTactic fun mvarId => do
    let (h, mvarId) <- intro1P mvarId
    let r ← cases mvarId h
    return r.toList.map (·.mvarId)

[Leonardo de Moura]

Not sure whether the following example is compatible with your plans, but evalTacticAt may be useful

elab "myTactic " : tactic => do
  let mvarId ← getMainGoal
  let [mvarId] ← evalTacticAt (← `(tactic| intro h)) mvarId | unreachable!
  let mvarIds ← evalTacticAt (← `(tactic| apply Or.elim h)) mvarId
  replaceMainGoal mvarIds

[Arthur Paulino]

I tried something like that but I don't understand why h is coming with a cross: h✝:

case left
p : Prop
h✝ : p ∨ p
⊢ p → p
case right
p : Prop
h✝ : p ∨ p
⊢ p → p

It doesn't happen when doing intro h; apply Or.elim h

[Alice Laroche]

For the first one, i get
tactic apply failed, metavariable has already been assigned
The second one seem fine
The last example doesn't allow me to get the introducted fvars for futur uses, so it won't do the job.

[Alice Laroche]

Arthur Paulino said:

I tried something like that but I don't understand why h is coming with a cross: h✝:

case left
p : Prop
h✝ : p ∨ p
⊢ p → p
case right
p : Prop
h✝ : p ∨ p
⊢ p → p

It doesn't happen when doing intro h; apply Or.elim h

Those are the default name, you can change that behevior like that

elab "myTactic " : tactic => do
  liftMetaTactic fun mvarId => do
    let (h, mvarId) <- intro1P mvarId
    let r ← cases mvarId h #[{ varNames := [`h]}, { varNames := [`h]}]
    return r.toList.map (·.mvarId)

[Arthur Paulino]

Alice Laroche said:

For the first one, i get
tactic apply failed, metavariable has already been assigned
The second one seem fine
The last example doesn't allow me to get the introducted fvars for futur uses, so it won't do the job.

remove the line let r ← cases mvarId h in the first one. It was probably a typo

[Alice Laroche]

Arthur Paulino said:

remove the line let r ← cases mvarId h in the first one. It was probably a typo

Ah yes, it make more sense...

[Leonardo de Moura]

I tried something like that but I don't understand why h is coming with a cross: h:cross::

It is because of hygiene.

[Leonardo de Moura]

If one wants they can workaround the hygienic macro system using tricks like

elab "myTactic " : tactic => do
  let h := mkIdent `h
  let mvarId ← getMainGoal
  let [mvarId] ← evalTacticAt (← `(tactic| intro $h)) mvarId | unreachable!
  let mvarIds ← evalTacticAt (← `(tactic| apply Or.elim $h)) mvarId
  replaceMainGoal mvarIds