How do I match on syntax.

Stream: metaprogramming / tactics

[metakuntyyy]

So I want to implement a rewrite and clear tactic. However I can't match on the syntax rwRuleSeq.

import Mathlib

open Lean
open Meta
open Lean.Elab.Tactic
open Lean.Meta.Tactic
open Lean.Parser.Tactic

syntax (name := rwc) "rwc " rwRuleSeq : tactic



@[tactic rwc]
def rewrite_and_clear : Tactic := fun stx => withMainContext do
  match stx with
  | `(rwRuleSeq) =>
    logInfo m! "ayayay"
  | _ =>
    logInfo m! "{stx}"


theorem dada (a b : ℕ ) (h : a = b) : a+b = b := by
  rwc [h]
  sorry

I'd like to enter the first match arm so that I can call the rewrite tactic and then I'd like to call some clear tactics.

[Aaron Liu]

what are you trying to do

[Aaron Liu]

rwRuleSeq is not a syntax, it is a syntax category

[metakuntyyy]

I'm trying to match on [$rs,*] inside rewrite_and_clear, but I don't know how to enter the first arm.

[metakuntyyy]

Got the code from here https://github.com/leanprover/lean4/blob/2fcce7258eeb6e324366bc25f9058293b04b7547/src/Init/Tactics.lean#L603

[metakuntyyy]

I'd like to have access to the main context, so the code in the rewrite tactic doesn't work..

[Aaron Liu]

what do you want to do with this syntax

[Aaron Liu]

there is docs#Lean.Elab.Tactic.withRWRulesSeq

[metakuntyyy]

Well the rwRuleSeq should hopefully contain the hypotheses that I can clear. Other then that I'd pass the call to the rw tactic.

[Aaron Liu]

you can access the parts of the syntax I guess

import Mathlib

open Lean Parser Elab Tactic

syntax (name := rwc) "rwc " rwRuleSeq : tactic



@[tactic rwc]
def rewrite_and_clear : Tactic := fun stx => do
  logInfo stx[0] -- `rwc`
  logInfo stx[1] -- `[h]`
  logInfo stx[1][0] -- `[`
  logInfo stx[1][1] -- `h`
  logInfo stx[1][1][0] -- `h`
  logInfo stx[1][2] -- `]`

set_option pp.rawOnError true
theorem dada (a b : ℕ ) (h : a = b) : a+b = b := by
  rwc [h]
  sorry

[metakuntyyy]

Cool, can you show me how to do it with match? so that the first arm gives me "rwc" and the second arm gives me [$rs,*]?

[Aaron Liu]

you can get the rewrite rules like this

import Mathlib

open Lean Parser Elab Tactic

syntax (name := rwc) "rwc " rwRuleSeq : tactic

macro_rules
  | `(tactic| rwc [$[$rs:rwRule],*]) => do
    Macro.throwUnsupported

[Aaron Liu]

or like this

import Mathlib

open Lean Parser Elab Tactic

syntax (name := rwc) "rwc " rwRuleSeq : tactic

example (stx : Syntax.Tactic) : MetaM Unit := do
  match stx with
  | `(tactic| rwc [$[$rs:rwRule],*]) =>
    return
  | _ => throwUnsupportedSyntax

[metakuntyyy]

How do I hook it up?

import Mathlib

open Lean Parser Elab Tactic

syntax (name := rwc) "rwc " rwRuleSeq : tactic

example (stx : Syntax.Tactic) : TacticM Unit := do
  match stx with
  | `(tactic| rwc [$[$rs:rwRule],*]) =>
    logInfo m! "HAA"
    return
  | _ =>
    logInfo m! "BOO"
    return

theorem dada (a b : ℕ ) (h : a = b) : a+b = b := by
  rwc [h]
  sorry

I want to enter the first arm and it should print HAA, not BOO

[Aaron Liu]

like this I guess?

import Mathlib

open Lean Parser Elab Tactic

syntax (name := rwc) "rwc " rwRuleSeq : tactic

def runRwc (stx : Syntax.Tactic) : TacticM Unit := do
  match stx with
  | `(tactic| rwc [$[$rs:rwRule],*]) =>
    logInfo m! "HAA"
    return
  | _ =>
    logInfo m! "BOO"
    return

@[tactic rwc]
def elabRwc : Tactic := fun stx => runRwc ⟨stx⟩

theorem dada (a b : ℕ ) (h : a = b) : a+b = b := by
  rwc [h]
  sorry

[metakuntyyy]

@Aaron Liu It works. :tada:

[metakuntyyy]

Ok, cool. Inside a TacticM Unit, how can I execute a tactic, like exfalso for example. `(tactic| exfalso) does not work.

[Aaron Liu]

docs#Lean.Elab.Tactic.evalTactic

[metakuntyyy]

Nvm it works.

import Mathlib

open Lean Parser Elab Tactic

syntax (name := rwc) "rwc " rwRuleSeq : tactic

def runRwc (stx : Syntax.Tactic) : TacticM Unit := withMainContext do
  match stx with
  | `(tactic| rwc $s:rwRuleSeq) =>
    match s with
    | `(rwRuleSeq| [$rs,*]) =>
      let seq := rs.getElems
      let y := seq[0]!
      let d ←  `(tactic| exfalso)
      let e ← evalTactic d
      return
    | _ => return
  | _ =>
    logInfo m! "BOO"
    return


@[tactic rwc]
def elabRwc : Tactic := fun stx => runRwc ⟨stx⟩


theorem dada (a b : ℕ ) (h : a = b) (h2: b=2): a+b = b := by
  rwc [h, h2]

  sorry

[metakuntyyy]

Apparently I had to use double bind. :joy:

[metakuntyyy]

Ok, so I have succeeded in rewriting and clearing. Now, how can I improve it?

import Mathlib

open Lean Parser Elab Tactic

syntax (name := rwc) "rwc" rwRuleSeq : tactic

set_option pp.rawOnError true

def runRwc (stx : Syntax.Tactic) : TacticM Unit := withMainContext do
  match stx with
  | `(tactic| rwc $s:rwRuleSeq) =>
    match s with
    | `(rwRuleSeq| [$rs,*]) =>
      let seq := rs.getElems
      logInfo m! "{s}"
      let l := seq.toList
      let d ← `(tactic|rw [$rs,*])
      evalTactic d
      for x in l do
        let yy := x.raw[1]
        let traw : TSyntax `term := TSyntax.mk yy
        let tc ← `(tactic| clear $traw)
        let d ← evalTactic tc
      return
    | _ => return
  | _ =>
    logInfo m! "BOO"
    return


@[tactic rwc]
def elabRwc : Tactic := fun stx => runRwc ⟨stx⟩


theorem dada (a b : ℕ ) (h : a = b) (h2: b=2): a+b = b := by
  rwc[h,h2]

  sorry