Goal changing when hypothesis is introduced

Stream: metaprogramming / tactics

[Anirudh Suresh]

import Mathlib
import Lean
import Lean.Elab.Tactic
import Lean.Elab.Term
import Lean.Meta

open Lean
open Lean.Elab.Tactic
open Lean.Elab.Term
open Lean.Meta
open scoped Matrix
open Matrix


def com_equiv (c1 c2 : ℕ) : Prop :=
  ∀ n : ℕ, c1 + n = c2 + n

infix:80 " ≡ " => com_equiv

namespace Expr

partial def matchApp? (e : Expr) : Option (Expr × Array Expr) :=
  match e with
  | Expr.app f x =>
    match matchApp? f with
    | some (head, args) => some (head, args.push x)
    | none              => some (f, #[x])
  | _ => none

end Expr

partial def matchAppDebug (e : Expr) : MetaM (Option (Expr × Array Expr)) := do

  logInfo m!"[matchAppDebug] incoming e: {e}"
  match e with
  | Expr.app f x =>
    match ← matchAppDebug f with
    | some (head, args) =>
      pure (some (head, args.push x))
    | none =>
      pure (some (f, #[x]))
  | _ =>
    logInfo "[matchAppDebug] not an `app`, returning none"
    pure none

elab "dbg_match_goalc" : tactic => do
  let goalExpr ← getMainTarget
  logInfo m!"[dbg_match_goalc] goalExpr = {goalExpr}"
  let some _ ← matchAppDebug goalExpr |
    logInfo "[dbg_match_goalc] matchAppDebug returned none,   not an application";
    pure ()
  pure ()
lemma l1 {a b: ℕ}: a≡ b:= by {
  dbg_match_goalc
}
lemma l2 {a b: ℕ}: a≡ b:= by {
  have h:1=1:=by simp
  dbg_match_goalc
}

In the code above, I am trying to create a tactic. However, the tactic behaves differently with the introduction of a hypothesis. The debug statement in both l1 and l2 show goalExpr to be the same thing but for some reason, only l1 detects the com_equiv. Is there a way to fix this so that the tactic can work irrespective of the presence of a hypothesis?

[Aaron Liu]

You have to consume the metadata:

partial def matchAppDebug (e : Expr) : MetaM (Option (Expr × Array Expr)) := do

  logInfo m!"[matchAppDebug] incoming e: {e}"
  match e.consumeMData with
  | Expr.app f x =>
    match ← matchAppDebug f with
    | some (head, args) =>
      pure (some (head, args.push x))
    | none =>
      pure (some (f, #[x]))
  | _ =>
    logInfo "[matchAppDebug] not an `app`, returning none"
    pure none

[Damiano Testa]

Also, generally matching directly on expressions is very brittle. You may consider using getMainTarget'', or explicitly adding a whnfR, which is what most mathlib tactic use.

[Damiano Testa]

Moreover, if you want your tactic to be aware of the new hypotheses, you should probably add a withMainContext at the very beginning of your tactic definition.