dsimp only for universal cleanup

Stream: mathlib4

[Kyle Miller]

Whether or not there is a pretty printer option, it would be nice if there was a post-tactic cleanup hook. Imagine you could tell Lean to run dsimp only at * after every tactic completes. Then students wouldn't need to see beta reduceable lambdas, they wouldn't be frustrated by linarith not working when it obviously should, and no one would have to make their own copies of every tactic.

[Yaël Dillies]

I was thinking, could it be as simple as (famous last words :upside_down:) overriding the tactic block macro so that it inserts those dsimp after each tactic call?

[Heather Macbeth]

For technical reasons I don't think that would be convenient for teaching, since dsimp only resolves numeric goals about Nats.

example : (3:Nat) * 5 = 15 := by dsimp only -- works

See lean4#1994.

[Yaël Dillies]

dsimp has extensive configuration options, though. You can instruct it to only beta-reduce.

[Heather Macbeth]

Oh, what's that option?

[Yaël Dillies]

.. unless those numeric goals also are beta reduction? I would think not, and instead come from the decide call.

[Heather Macbeth]

dsimp doesn't call decide any more.

[Heather Macbeth]

lean4#1888

[Yaël Dillies]

Hmm, puzzling. Let me do some trace-gazing.

[Yaël Dillies]

Okay, docs4#Lean.Meta.Simp.Config is the relevant declaration. I wish it was easier to find :sad:

[Yaël Dillies]

I assume simp and dsimp both use this as configuration? Not so sure, actually...

[Eric Wieser]

dsimp only is sometimes harmful if you have something like (fun x => 1 * x) '' s, which in lean3 it would reduce to has_mul.mul 1 '' s

[Yaël Dillies]

Ahah! There's also docs4#Lean.Meta.DSimp.Config

[Yaël Dillies]

This looks like it's above my paygrade, but here's my attempt

def heatherConfig : Lean.Meta.DSimp.Config where
  zeta       := false
  beta       := true
  eta        := false
  etaStruct  := .none
  iota       := false
  proj       := false
  decide     := false
  autoUnfold := false

example (x : ℕ × ℕ) : (x.1, x.2) = x := by dsimp -- works
example (x : ℕ × ℕ) : (x.1, x.2) = x := by dsimp (config := heatherConfig)  -- works??

example : (3:Nat) * 5 = 15 := by dsimp (config := heatherConfig) -- works??

[Heather Macbeth]

I believe the point is what I wrote up in lean4#1994, as I linked before:

example : (3:Nat) * 5 = 15 := by with_reducible rfl

also works.

[Heather Macbeth]

Here's a previous discussion:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/use/near/317444788

[Yaël Dillies]

Does dsimp try rfl?

[Notification Bot]

17 messages were moved here from #mathlib4 > pp.beta by Heather Macbeth.

[Heather Macbeth]

I wouldn't be surprised if dsimp tried with_reducible rfl. But the real reason I suspect it's the same issue is that it's again a Nat-only issue.

[Kyle Miller]

Here's a beta_reduce tactic that definitely only does beta reduction and nothing else:

import Lean
import Mathlib.Tactic.Basic

namespace Mathlib.Tactic
open Lean Parser Tactic Elab Tactic Meta

syntax (name := beta_reduce) "beta_reduce" (ppSpace location)? : tactic

elab_rules : tactic | `(tactic| beta_reduce $[$loc]?) => do
  withLocation (expandOptLocation (Lean.mkOptionalNode loc))
    (atLocal := fun h ↦ do
      let ty ← Core.betaReduce (← instantiateMVars (← h.getType))
      let newGoal ← (← getMainGoal).changeLocalDecl' h ty
      replaceMainGoal [newGoal])
    (atTarget := withMainContext do
      let ty ← Core.betaReduce (← getMainTarget)
      let newGoal ← (← getMainGoal).change ty
      replaceMainGoal [newGoal])
    (failed := fun _ ↦ throwError "beta_reduce failed")

end Mathlib.Tactic

example : (fun _ => 3) () * 5 = 15 := by
  beta_reduce
  guard_target =ₛ 3 * 5 = 15
  rfl

example (h : x = (fun _ => 3) ()) : x * 5 = 15 := by
  beta_reduce at h
  guard_hyp h :ₛ x = 3
  rw [h]

[Kyle Miller]

I haven't found where this can be hooked into anything in a general way though...

[Kyle Miller]

This lets you do beta_reduce at *

[Heather Macbeth]

Kyle Miller said:

I haven't found where this can be hooked into anything in a general way though...

If you do find it, this seems like a good solution.

[Kyle Miller]

Since we're here, I figured it would be worth abstracting that code a bit to be able to quickly define tactics for other kinds of transformations, for example whnf.

def myeq {α : Sort _} (x y : α) := x = (fun _ => y) ()

example (h : myeq x 3) : x * 5 = 15 := by
  whnf at h
  guard_hyp h :ₛ x = (fun _ => 3) ()
  beta_reduce at h
  guard_hyp h :ₛ x = 3
  rw [h]

code

--import Mathlib.Lean.Expr.Basic
import Lean
import Mathlib.Tactic.Basic

namespace Mathlib.Tactic
open Lean Parser Tactic Elab Tactic Meta

/-- `f` is some function that transforms a type to a defeq type. -/
def mkTypeTransformerTactic (name : String) (f : Expr → TacticM Expr)
    (loc : Option (TSyntax `Lean.Parser.Tactic.location)) : TacticM Unit :=
  withLocation (expandOptLocation (Lean.mkOptionalNode loc))
    (atLocal := fun h ↦ do
      let newGoal ← (← getMainGoal).changeLocalDecl' h <| ← f (← instantiateMVars (← h.getType))
      replaceMainGoal [newGoal])
    (atTarget := withMainContext do
      let newGoal ← (← getMainGoal).change <| ← f (← getMainTarget)
      replaceMainGoal [newGoal])
    (failed := fun _ ↦ throwError "{name} failed")

syntax (name := beta_reduce) "beta_reduce" (ppSpace location)? : tactic

elab_rules : tactic | `(tactic| beta_reduce $[$loc]?) => do
  mkTypeTransformerTactic "beta_reduce" (fun e => Core.betaReduce e) loc

syntax (name := whnf) "whnf" (ppSpace location)? : tactic

elab_rules : tactic | `(tactic| whnf $[$loc]?) => do
  mkTypeTransformerTactic "whnf" (fun e => Meta.whnf e) loc

end Mathlib.Tactic

example : (fun _ => 3) () * 5 = 15 := by
  beta_reduce
  guard_target =ₛ 3 * 5 = 15
  rfl

example (h : x = (fun _ => 3) ()) : x * 5 = 15 := by
  beta_reduce at h
  guard_hyp h :ₛ x = 3
  rw [h]

def myeq {α : Sort _} (x y : α) := x = (fun _ => y) ()

example (h : myeq x 3) : x * 5 = 15 := by
  whnf at h
  guard_hyp h :ₛ x = (fun _ => 3) ()
  beta_reduce at h
  guard_hyp h :ₛ x = 3
  rw [h]

[Anand Rao Tadipatri]

I have extended @Kyle Miller's code to implement @Yaël Dillies's suggestion of modifying the by tactic to perform a beta-reduction after each tactic call.

--import Mathlib.Lean.Expr.Basic
import Lean
import Mathlib.Tactic.Basic

namespace Mathlib.Tactic

open Lean Elab Parser Term Meta Tactic

/-- `f` is some function that transforms a type to a defeq type. -/
def mkTypeTransformerTactic (name : String) (f : Expr → TacticM Expr)
    (loc : Option (TSyntax `Lean.Parser.Tactic.location)) : TacticM Unit :=
  withLocation (expandOptLocation (Lean.mkOptionalNode loc))
    (atLocal := fun h ↦ do
      let newGoal ← (← getMainGoal).changeLocalDecl h <| ← f (← instantiateMVars (← h.getType))
      replaceMainGoal [newGoal])
    (atTarget := withMainContext do
      let newGoal ← (← getMainGoal).change <| ← f (← getMainTarget)
      replaceMainGoal [newGoal])
    (failed := fun _ ↦ throwError "{name} failed")

syntax (name := beta_reduce) "beta_reduce" (ppSpace location)? : tactic

elab_rules : tactic | `(tactic| beta_reduce $[$loc]?) => do
  mkTypeTransformerTactic "beta_reduce" (fun e => Core.betaReduce e) loc

syntax (name := whnf) "whnf" (ppSpace location)? : tactic

elab_rules : tactic | `(tactic| whnf $[$loc]?) => do
  mkTypeTransformerTactic "whnf" (fun e => Meta.whnf e) loc

end Mathlib.Tactic

example : (fun _ => 3) () * 5 = 15 := by
  beta_reduce
  guard_target =ₛ 3 * 5 = 15
  rfl

example (h : x = (fun _ => 3) ()) : x * 5 = 15 := by
  beta_reduce at h
  guard_hyp h :ₛ x = 3
  rw [h]

def myeq {α : Sort _} (x y : α) := x = (fun _ => y) ()

example (h : myeq x 3) : x * 5 = 15 := by
  whnf at h
  guard_hyp h :ₛ x = (fun _ => 3) ()
  beta_reduce at h
  guard_hyp h :ₛ x = 3
  rw [h]

namespace Array

def interleave (as : Array α) (x : α) : Array α := Id.run do
  let mut r := #[]
  for a in as do
    r := r.push x
    r := r.push a
  return r

end Array

namespace Mathlib.Tactic

open Lean Elab Parser Term Meta Tactic

-- a clone of the `by` tactic
syntax (name := byTactic') "by' " tacticSeq : term

@[term_elab byTactic'] def elabByTactic' : TermElab := fun stx expectedType? => do
  match expectedType? with
  | some expectedType =>
  let mvar ← mkFreshExprMVar expectedType MetavarKind.syntheticOpaque
  let mvarId := mvar.mvarId!
  let ref ← getRef
  registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic stx (← saveContext)
  return mvar
  | none =>
    tryPostpone
    throwError ("invalid 'by\'' tactic, expected type has not been provided")

macro_rules
  | `(by $[$tacs]*) => do
    let tacs' := tacs.interleave <| ← `(tactic| beta_reduce at *)
    `(by' $[$tacs']*)

end Mathlib.Tactic

example (h : myeq x 3) : x * 5 = 15 := by
  whnf at h
  rw [h]

This almost does what is needed - in the final example, the hypothesis is automatically simplified to x = 3 when the cursor is placed before rw [h]. However, I don't know how to make the change happen immediately, instead of on the next line.

[Kyle Miller]

@Anand Rao Nice; maybe there's a way to tag the beta_reduce at * tactic with a fake source position so that the generated info is available where you'd expect.

I wish overriding by were a complete solution. This doesn't help with · tactic blocks, or blocks of tactics that appear inside other tactics (like structured cases or induction) unfortunately, since those call evalTactic themselves directly without going through by syntax.

[Kyle Miller]

If there were a way to override evalTactic at runtime then that would be a clear place to insert a hook... (Lean 3 would let you do this, but since Lean 4 is compiled this doesn't seem to be possible.)

If evalTactic started with a call to some user-defined hook (ideally, something to wrap the whole evaluation, like what profileitM is doing), then we could insert this beta_reduce cleanup code easily.

[Anand Rao Tadipatri]

@Kyle Miller I think it might be still possible to get this to work by overriding the by tactic block. The problem you mentioned seems to arise precisely when a tactic uses a tacticSeq as a part of its syntax. I have been working on intercepting the by tactic for unrelated reasons (my code is here), and I think I might be able to adapt this to produce a "nested" version of the code I posted above.

[Kyle Miller]

I wonder if we could take the raw Syntax, scan through the whole thing looking for tacticSeq, and then intersperse whatever we want between everything. That might save you some work in your traceTacticSnap function, so you don't have to parse every piece of tactic syntax yourself. On the other hand, it might not be 100% accurate to do what I'm suggesting.

[Anand Rao Tadipatri]

That seems like a sound approach that should work in general - even with completely new tactics that use tacticSeq as a part of their syntax. I don't mind doing a case-by-case analysis of the tactic syntax for now though, since there are not too many tactics in Lean core and mathlib4 that use tacticSeq. I'd like to implement try your approach too, since it is probably more robust and I'll get to learn how to do a deep traversal of a syntax tree.

[Yaël Dillies]

rw [a, b, c] is morally rw a, rw b, rw c, so I'm wondering whether we should have somewhere in the tactic framework a "tactic clock" that each tactic is free to tick when a tactic call "morally" happened. So for example every tactic would tick at least once, and rw [a, b, c] would tick thrice. Then we could run the tactic hook at every tactic tick.

[Kyle Miller]

@Yaël Dillies rw is implemented as a macro that expands out to three rewrite tactics in that case, so that should happen automatically (if I understand it correctly -- edit I didn't, it doesn't work this way).

[Anand Rao Tadipatri]

Here is a version of my code that works for "nested" tactic sequences:

--import Mathlib.Lean.Expr.Basic
import Lean
import Mathlib.Tactic.Basic


open Lean Elab Parser Term Meta Tactic

namespace Mathlib.Tactic

/-- `f` is some function that transforms a type to a defeq type. -/
def mkTypeTransformerTactic (name : String) (f : Expr → TacticM Expr)
    (loc : Option (TSyntax `Lean.Parser.Tactic.location)) : TacticM Unit :=
  withLocation (expandOptLocation (Lean.mkOptionalNode loc))
    (atLocal := fun h ↦ do
      let newGoal ← (← getMainGoal).changeLocalDecl h <| ← f (← instantiateMVars (← h.getType))
      replaceMainGoal [newGoal])
    (atTarget := withMainContext do
      let newGoal ← (← getMainGoal).change <| ← f (← getMainTarget)
      replaceMainGoal [newGoal])
    (failed := fun _ ↦ throwError "{name} failed")

syntax (name := beta_reduce) "beta_reduce" (ppSpace location)? : tactic

elab_rules : tactic | `(tactic| beta_reduce $[$loc]?) => do
  mkTypeTransformerTactic "beta_reduce" (fun e => Core.betaReduce e) loc

syntax (name := whnf) "whnf" (ppSpace location)? : tactic

elab_rules : tactic | `(tactic| whnf $[$loc]?) => do
  mkTypeTransformerTactic "whnf" (fun e => Meta.whnf e) loc

end Mathlib.Tactic

example : (fun _ => 3) () * 5 = 15 := by
  beta_reduce
  guard_target =ₛ 3 * 5 = 15
  rfl

example (h : x = (fun _ => 3) ()) : x * 5 = 15 := by
  beta_reduce at h
  guard_hyp h :ₛ x = 3
  rw [h]

def myeq {α : Sort _} (x y : α) := x = (fun _ => y) ()

example (h : myeq x 3) : x * 5 = 15 := by
  whnf at h
  guard_hyp h :ₛ x = (fun _ => 3) ()
  beta_reduce at h
  guard_hyp h :ₛ x = 3
  rw [h]

namespace Array

def interleave (as : Array α) (x : α) : Array α := Id.run do
  let mut r := #[]
  for a in as do
    r := r.push x
    r := r.push a
  return r

end Array

syntax (name := reduce_and_eval_tac) "reduce_and_eval_tac" tactic : tactic
syntax (name := reduce_seq) "reduce_seq" tacticSeq : tactic

macro_rules
  | `(tactic| reduce_seq $[$tacs]*) => do
    let tacs' ← tacs.mapM <| fun tac ↦ `(tactic| reduce_and_eval_tac $tac)
    `(tactic| {$[$tacs']*})

def matchAltTac := Term.matchAlt (rhsParser := matchRhs)

@[tactic reduce_and_eval_tac]
def reduceAndEvalTac : Tactic
  | `(tactic| reduce_and_eval_tac $tac) =>
    match tac with
    | `(tactic| focus $[$tacs]*) => do
      evalTactic <| ← `(tactic| focus reduce_seq $[$tacs]*)
    | `(tactic| · $[$tacs]*) => do
      evalTactic <| ← `(tactic| · reduce_seq $[$tacs]*)
    | `(tactic| {$[$tacs]*}) => do
      evalTactic <| ← `(tactic| {reduce_seq $[$tacs]*})
    | `(tactic| ($[$tacs]*)) => do
      evalTactic <| ← `(tactic| (reduce_seq $[$tacs]*))
    | `(tactic| case $[$tag $hs*]|* =>%$arr $tac:tacticSeq) => do
      evalTactic <| ← `(tactic| case $[$tag $hs*]|* =>%$arr reduce_seq $tac:tacticSeq)
    | `(tactic| case' $[$tag $hs*]|* =>%$arr $tac:tacticSeq) => do
      evalTactic <| ← `(tactic| case' $[$tag $hs*]|* =>%$arr reduce_seq $tac:tacticSeq)
    | `(tactic| induction $[$ts],* $[using $id:ident]?  $[generalizing $gs*]? with $[$tac]? $is*) => do
      let is' : TSyntaxArray ``inductionAlt ←
        is.mapM <| fun
          | `(inductionAlt| $il* => $ts:tacticSeq) => `(inductionAlt| $il* => reduce_seq $ts)
          | i => return ⟨i⟩
      evalTactic <| ← `(tactic| induction $[$ts],* $[using $id:ident]?  $[generalizing $gs*]? with $[$tac]? $is'*)
    | `(tactic| cases $[$cs],* $[using $id:ident]? with $[$tac]? $is*) => do
      let is' : TSyntaxArray ``inductionAlt ←
        is.mapM <| fun
          | `(inductionAlt| $il* => $ts:tacticSeq) => `(inductionAlt| $il* => reduce_seq $ts)
          | i => return ⟨i⟩
      evalTactic <| ← `(tactic| cases $[$cs],* $[using $id:ident]? with $[$tac]? $is'*)
    | `(tactic| match $[$gen]? $[$motive]? $discrs,* with $alts:matchAlt*) => do
      let alts' : TSyntaxArray ``matchAlt ←
        alts.mapM <| fun
          | `(matchAltTac| | $[$pats,*]|* => $rhs:tacticSeq) => do
              let alt ← `(matchAltTac| | $[$pats,*]|* => reduce_seq $rhs)
              return ⟨alt⟩
          | alt =>  return ⟨alt⟩
      evalTactic <| ← `(tactic| match $[$gen]? $[$motive]? $discrs,* with $alts':matchAlt*)
    | _ => do
      evalTactic <| ← `(tactic| beta_reduce at *)
      evalTactic tac
  | _ => panic!"Invalid syntax for `eval_tac_and_reduce`."

namespace Mathlib.Tactic

-- a clone of the `by` tactic
syntax (name := byTactic') "by' " tacticSeq : term

@[term_elab byTactic'] def elabByTactic' : TermElab := fun stx expectedType? => do
  match expectedType? with
  | some expectedType =>
  let mvar ← mkFreshExprMVar expectedType MetavarKind.syntheticOpaque
  let mvarId := mvar.mvarId!
  let ref ← getRef
  registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic stx (← saveContext)
  return mvar
  | none =>
    tryPostpone
    throwError ("invalid 'by\'' tactic, expected type has not been provided")

macro_rules
  | `(by $tacs) => `(by' reduce_seq $tacs)

end Mathlib.Tactic

set_option linter.unreachableTactic false

example (h : myeq x 3) : 1 = 1 ∧ x * 5 = 15 := by
  refine' ⟨_, _⟩
  . rfl
  · whnf at h
    rw [h]

[Anand Rao Tadipatri]

The rough idea is that I have two new tactics - reduce_and_eval_tactic and reduce_seq. The first is meant to run beta_reduce at * and then evaluate the given tactic, while the second is meant to modify a tacticSeq to perform the intermediate beta-reduction. The behaviour of reduce_and_eval_tac for · tactic blocks, induction applications, and a few other cases is handled in a special way by making a call to reduce_seq. My code covers most of the main tactics in Lean4 and mathlib4 that use tacticSeq; there are a few like classical and permute_goals that I have excluded for now.

[Anand Rao Tadipatri]

@Yaël Dillies I have modified my code to perform a beta-reduction after each rewrite:

--import Mathlib.Lean.Expr.Basic
import Lean
import Mathlib.Tactic.Basic


open Lean Elab Parser Term Meta Tactic

namespace Mathlib.Tactic

/-- `f` is some function that transforms a type to a defeq type. -/
def mkTypeTransformerTactic (name : String) (f : Expr → TacticM Expr)
    (loc : Option (TSyntax `Lean.Parser.Tactic.location)) : TacticM Unit :=
  withLocation (expandOptLocation (Lean.mkOptionalNode loc))
    (atLocal := fun h ↦ do
      let newGoal ← (← getMainGoal).changeLocalDecl h <| ← f (← instantiateMVars (← h.getType))
      replaceMainGoal [newGoal])
    (atTarget := withMainContext do
      let newGoal ← (← getMainGoal).change <| ← f (← getMainTarget)
      replaceMainGoal [newGoal])
    (failed := fun _ ↦ throwError "{name} failed")

syntax (name := beta_reduce) "beta_reduce" (ppSpace location)? : tactic

elab_rules : tactic | `(tactic| beta_reduce $[$loc]?) => do
  mkTypeTransformerTactic "beta_reduce" (fun e => Core.betaReduce e) loc

syntax (name := whnf) "whnf" (ppSpace location)? : tactic

elab_rules : tactic | `(tactic| whnf $[$loc]?) => do
  mkTypeTransformerTactic "whnf" (fun e => Meta.whnf e) loc

end Mathlib.Tactic

example : (fun _ => 3) () * 5 = 15 := by
  beta_reduce
  guard_target =ₛ 3 * 5 = 15
  rfl

example (h : x = (fun _ => 3) ()) : x * 5 = 15 := by
  beta_reduce at h
  guard_hyp h :ₛ x = 3
  rw [h]

def myeq {α : Sort _} (x y : α) := x = (fun _ => y) ()

example (h : myeq x 3) : x * 5 = 15 := by
  whnf at h
  guard_hyp h :ₛ x = (fun _ => 3) ()
  beta_reduce at h
  guard_hyp h :ₛ x = 3
  rw [h]

namespace Array

def interleave (as : Array α) (x : α) : Array α := Id.run do
  let mut r := #[]
  for a in as do
    r := r.push x
    r := r.push a
  return r

end Array

syntax (name := reduce_and_eval_tac) "reduce_and_eval_tac" tactic : tactic
syntax (name := reduce_seq) "reduce_seq" tacticSeq : tactic

macro_rules
  | `(tactic| reduce_seq $[$tacs]*) => do
    let tacs' ← tacs.mapM <| fun tac ↦ `(tactic| reduce_and_eval_tac $tac)
    `(tactic| {$[$tacs']*})

def matchAltTac := Term.matchAlt (rhsParser := matchRhs)

@[tactic reduce_and_eval_tac]
def reduceAndEvalTac : Tactic
  | `(tactic| reduce_and_eval_tac $tac) =>
    match tac with
    | `(tactic| focus $[$tacs]*) => do
      evalTactic <| ← `(tactic| focus reduce_seq $[$tacs]*)
    | `(tactic| · $[$tacs]*) => do
      evalTactic <| ← `(tactic| · reduce_seq $[$tacs]*)
    | `(tactic| {$[$tacs]*}) => do
      evalTactic <| ← `(tactic| {reduce_seq $[$tacs]*})
    | `(tactic| ($[$tacs]*)) => do
      evalTactic <| ← `(tactic| (reduce_seq $[$tacs]*))
    | `(tactic| case $[$tag $hs*]|* =>%$arr $tac:tacticSeq) => do
      evalTactic <| ← `(tactic| case $[$tag $hs*]|* =>%$arr reduce_seq $tac:tacticSeq)
    | `(tactic| case' $[$tag $hs*]|* =>%$arr $tac:tacticSeq) => do
      evalTactic <| ← `(tactic| case' $[$tag $hs*]|* =>%$arr reduce_seq $tac:tacticSeq)
    | `(tactic| rw $[$cfg]? [$rs,*] $[$loc]?) => do
        evalTactic <| ← `(tactic| beta_reduce at *)
        for r in (rs : TSyntaxArray `Lean.Parser.Tactic.rwRule) do
          evalTactic <| ← `(tactic| beta_reduce at *)
          evalTactic <| ← `(tactic| rw $[$cfg]? [$r] $[$loc]?)
        if (← getUnsolvedGoals).length > 0 then
          evalTactic <| ← `(tactic| beta_reduce at *)
    | `(tactic| erw [$rs,*] $[$loc]?) => do
        evalTactic <| ← `(tactic| beta_reduce at *)
        for r in (rs : TSyntaxArray `Lean.Parser.Tactic.rwRule) do
          evalTactic <| ← `(tactic| beta_reduce at *)
          evalTactic <| ← `(tactic| erw [$r] $[$loc]?)
        if (← getUnsolvedGoals).length > 0 then
          evalTactic <| ← `(tactic| beta_reduce at *)
    | `(tactic| rwa [$rs,*] $[$loc]?) => do
      evalTactic <| ← `(tactic| beta_reduce at *)
      for r in (rs : TSyntaxArray `Lean.Parser.Tactic.rwRule) do
          evalTactic <| ← `(tactic| beta_reduce at *)
          evalTactic <| ← `(tactic| rw [$r] $[$loc]?)
      evalTactic <| ← `(tactic| beta_reduce at *)
      evalTactic <| ← `(tactic| assumption)
    | `(tactic| induction $[$ts],* $[using $id:ident]?  $[generalizing $gs*]? with $[$tac]? $is*) => do
      let is' : TSyntaxArray ``inductionAlt ←
        is.mapM <| fun
          | `(inductionAlt| $il* => $ts:tacticSeq) => `(inductionAlt| $il* => reduce_seq $ts)
          | i => return ⟨i⟩
      evalTactic <| ← `(tactic| induction $[$ts],* $[using $id:ident]?  $[generalizing $gs*]? with $[$tac]? $is'*)
    | `(tactic| cases $[$cs],* $[using $id:ident]? with $[$tac]? $is*) => do
      let is' : TSyntaxArray ``inductionAlt ←
        is.mapM <| fun
          | `(inductionAlt| $il* => $ts:tacticSeq) => `(inductionAlt| $il* => reduce_seq $ts)
          | i => return ⟨i⟩
      evalTactic <| ← `(tactic| cases $[$cs],* $[using $id:ident]? with $[$tac]? $is'*)
    | `(tactic| match $[$gen]? $[$motive]? $discrs,* with $alts:matchAlt*) => do
      let alts' : TSyntaxArray ``matchAlt ←
        alts.mapM <| fun
          | `(matchAltTac| | $[$pats,*]|* => $rhs:tacticSeq) => do
              let alt ← `(matchAltTac| | $[$pats,*]|* => reduce_seq $rhs)
              return ⟨alt⟩
          | alt =>  return ⟨alt⟩
      evalTactic <| ← `(tactic| match $[$gen]? $[$motive]? $discrs,* with $alts':matchAlt*)
    | _ => do
      evalTactic <| ← `(tactic| beta_reduce at *)
      evalTactic tac
      if (← getUnsolvedGoals).length > 0 then
        evalTactic <| ← `(tactic| beta_reduce at *)
  | _ => panic!"Invalid syntax for `eval_tac_and_reduce`."

namespace Mathlib.Tactic

-- a clone of the `by` tactic
syntax (name := byTactic') "by' " tacticSeq : term

@[term_elab byTactic'] def elabByTactic' : TermElab := fun stx expectedType? => do
  match expectedType? with
  | some expectedType =>
  let mvar ← mkFreshExprMVar expectedType MetavarKind.syntheticOpaque
  let mvarId := mvar.mvarId!
  let ref ← getRef
  registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic stx (← saveContext)
  return mvar
  | none =>
    tryPostpone
    throwError ("invalid 'by\'' tactic, expected type has not been provided")

macro_rules
  | `(by $tacs) => `(by' reduce_seq $tacs)

end Mathlib.Tactic

set_option linter.unreachableTactic false

example (h : myeq x 3) : 1 = 1 ∧ x * 5 = 15 := by
  refine' ⟨_, _⟩
  . rfl
  · whnf at h
    simp [h]

[Anand Rao Tadipatri]

This is correct only if the substitution rw [a, b, c] -> rw [a]; rw [b]; rw [c] is valid in Lean.

[Ruben Van de Velde]

It's not valid if rw [a, b] already gets the goal in a state where the implicit rfl solves it - in that case rw [c] separately will fail with "no goals"

[Kyle Miller]

Here's another implementation that overrides a number of sequencing forms and doesn't peer into too much syntax, so it's fairly short. It's not able to do anything between rw steps though (I was wrong about how rw works -- handles inserting tactic info step by step itself, and it doesn't macro expand into anything).

import Lean
import Mathlib.Tactic.Basic
import Mathlib.Tactic.Linarith

namespace Mathlib.Tactic
open Lean Parser Tactic Elab Tactic Meta

/-- Runs `f` on every local variable and the target. `f` is allowed to fail, and if it
does that local variable or target is not changed. -/
def transformAllTypes (mvarId : MVarId) (f : Expr → MetaM Expr) := do
  let mut mvarId := mvarId
  for fvarId in (← mvarId.getDecl).lctx.getFVarIds.reverse do
    try
      let ty := ((← mvarId.getDecl).lctx.get! fvarId).type
      mvarId ← mvarId.changeLocalDecl' fvarId <| ← f (← instantiateMVars ty)
    catch _ => pure ()
  try
    mvarId ← mvarId.change <| ← f (← instantiateMVars (← mvarId.getType))
  catch _ => pure ()
  return mvarId

/-- Beta reduce all local variables and targets across all goals. -/
def betaReduceEverything : TacticM Unit := do
  let gs ← getGoals
  let gs' ← gs.mapM (fun g => transformAllTypes g (fun e => Core.betaReduce e))
  setGoals gs'

/-- `tactic_wrapper` is inserted around every tactic in a tactic sequence.
Implement this tactic to alter the behavior of the tactic processor. -/
syntax (name := wrapper) "tactic_wrapper " tactic : tactic

def sepByTacticWrapper (stx : Syntax) : TacticM Syntax := do
  let .node info kind args := stx | throwUnsupportedSyntax
  let mut args' := #[]
  for arg in args, i in [:args.size] do
    if i % 2 == 0 then
      if arg.getKind == ``wrapper then
        args' := args'.push arg
      else
       args' := args'.push <| (← withRef arg `(tactic| tactic_wrapper $(.mk arg))).raw
    else
      args' := args'.push arg
  return .node info kind args'

/-- Inserts a `tactic_wrapper` around every tactic in a tactic sequence.

Different sequence-like tactics store their tactic sequences in different syntax positions. -/
def transformTacticSeq (stx : Syntax) (pos : Nat) : TacticM Syntax := do
  let .node info kind args := stx | throwUnsupportedSyntax
  let args' := args.setD pos (← sepByTacticWrapper (args.getD pos default))
  return .node info kind args'

@[tactic tacticSeq1Indented] def evalTacticSeq1Indented' : Tactic := fun stx => do
  evalTacticSeq1Indented (← transformTacticSeq stx 0)

@[tactic tacticSeqBracketed] def evalTacticSeqBracketed' : Tactic := fun stx => do
  evalTacticSeqBracketed (← transformTacticSeq stx 1)

@[tactic cdot] def evalTacticCDot' : Tactic := fun stx => do
  evalTacticCDot (← transformTacticSeq stx 1)

@[tactic seq1] def evalSeq1' : Tactic := fun stx => do
  evalSeq1 (← transformTacticSeq stx 0)

elab_rules : tactic
  | `(tactic| tactic_wrapper $tac) => do
    --logInfo m!"tactic: {tac}"
    betaReduceEverything
    evalTactic tac
    betaReduceEverything
    --logInfo m!"finished {tac}"

end Mathlib.Tactic

example : (fun _ => 3) () * 5 = 15 := by
  guard_target =ₛ 3 * 5 = 15
  rfl

example (h : x = (fun _ => 3) ()) : x * 5 = 15 := by
  guard_hyp h :ₛ x = 3
  rw [h]

example (h : (fun _ => x) () = y) (h' : y = z) : x = z := by
  rw [h, h']

example (f : ℤ → ℤ) (h : 0 < (fun y => - f y) x + 1) : f x < 1 := by
  linarith -- works! (would usually need `dsimp at h`)

example (n : Nat) (f : ℤ → ℤ) (h : 0 < (fun y => - f y) x + 1) : f x < 1 := by
  cases n with
  | zero =>
    change 0 < (fun y => - f y) x + 1 at h
    linarith
  | succ => linarith

[Kyle Miller]

This at least solves the problem I ran into myself with Tutorial 0079 and linarith. Here's an analog:

example (f : ℤ → ℤ) (h : 0 < (fun y => - f y) x + 1) : f x < 1 := by
  linarith -- works! (would usually need `dsimp at h`)

[Kyle Miller]

Here's a test that it still works even with structured tactics:

example (n : Nat) (f : ℤ → ℤ) (h : 0 < - f x + 1) : f x < 1 := by
  cases n with
  | zero =>
    change 0 < (fun y => - f y) x + 1 at h
    linarith
  | succ => linarith

[Kyle Miller]

@Anand Rao It doesn't appear to be necessary to do it, but if you're interested here's another version that overrides by without needing to re-implement by or create any new syntax. It does a syntax transformation ahead of time, while also overriding the other sequencing tactics just in case there's a macro expansion and we want to intervene.

code

import Lean
import Mathlib.Tactic.Basic
import Mathlib.Tactic.Linarith

namespace Mathlib.Tactic
open Lean Parser Tactic Elab Tactic Meta

/-- Runs `f` on every local variable and the target. `f` is allowed to fail, and if it
does that local variable or target is not changed. -/
def transformAllTypes (mvarId : MVarId) (f : Expr → MetaM Expr) := do
  let mut mvarId := mvarId
  for fvarId in (← mvarId.getDecl).lctx.getFVarIds.reverse do
    try
      let ty := ((← mvarId.getDecl).lctx.get! fvarId).type
      mvarId ← mvarId.changeLocalDecl' fvarId <| ← f (← instantiateMVars ty)
    catch _ => pure ()
  try
    mvarId ← mvarId.change <| ← f (← instantiateMVars (← mvarId.getType))
  catch _ => pure ()
  return mvarId

/-- Beta reduce all local variables and targets across all goals. -/
def betaReduceEverything : TacticM Unit := do
  let gs ← getGoals
  let gs' ← gs.mapM (fun g => transformAllTypes g (fun e => Core.betaReduce e))
  setGoals gs'

/-- `tactic_wrapper` is inserted around every tactic in a tactic sequence.
Implement this tactic to alter the behavior of the tactic processor. -/
syntax (name := wrapper) "tactic_wrapper " tactic : tactic

def sepByTacticWrapper (stx : Syntax) : MetaM Syntax := do
  let .node info kind args := stx | throwUnsupportedSyntax
  let mut args' := #[]
  for arg in args, i in [:args.size] do
    if i % 2 == 0 then
      if arg.getKind == ``wrapper then
        args' := args'.push arg
      else
       args' := args'.push <| (← withRef arg `(tactic| tactic_wrapper $(.mk arg))).raw
    else
      args' := args'.push arg
  return .node info kind args'

/-- Inserts a `tactic_wrapper` around every tactic in a tactic sequence.

Different sequence-like tactics store their tactic sequences in different syntax positions. -/
def transformTacticSeq (stx : Syntax) (pos : Nat) : MetaM Syntax := do
  let .node info kind args := stx | throwUnsupportedSyntax
  let args' := args.setD pos (← sepByTacticWrapper (args.getD pos default))
  return .node info kind args'

partial def transformTacticSeqs (s : Syntax) : MetaM Syntax :=
  match s with
  | .atom .. => return s
  | .ident .. => return s
  | .missing => return s
  | .node info kind args => do
    let s := Syntax.node info kind <| ← args.mapM transformTacticSeqs
    if kind == ``tacticSeq1Indented then
      transformTacticSeq s 0
    else if kind == ``tacticSeqBracketed then
      transformTacticSeq s 1
    else if kind == ``cdot then
      transformTacticSeq s 1
    else if kind == ``seq1 then
      transformTacticSeq s 0
    else
      return s

@[tactic tacticSeq1Indented] def evalTacticSeq1Indented' : Tactic := fun stx => do
  evalTacticSeq1Indented (← transformTacticSeqs stx)

@[tactic tacticSeqBracketed] def evalTacticSeqBracketed' : Tactic := fun stx => do
  evalTacticSeqBracketed (← transformTacticSeqs stx)

@[tactic cdot] def evalTacticCDot' : Tactic := fun stx => do
  evalTacticCDot (← transformTacticSeqs stx)

@[tactic seq1] def evalSeq1' : Tactic := fun stx => do
  evalSeq1 (← transformTacticSeqs stx)

@[term_elab byTactic] def elabByTactic' : Term.TermElab := fun stx expectedType? => do
  let stx ← transformTacticSeqs stx
  Term.elabByTactic stx expectedType?

elab_rules : tactic
  | `(tactic| tactic_wrapper $tac) => do
    --logInfo m!"tactic: {tac}"
    betaReduceEverything
    evalTactic tac
    betaReduceEverything
    --logInfo m!"finished {tac}"

end Mathlib.Tactic

example : (fun _ => 3) () * 5 = 15 := by
  guard_target =ₛ 3 * 5 = 15
  rfl

example (h : x = (fun _ => 3) ()) : x * 5 = 15 := by
  guard_hyp h :ₛ x = 3
  rw [h]

example (h : (fun _ => x) () = y) (h' : y = z) : x = z := by
  rw [h, h']

example (n : Nat) (f : ℤ → ℤ) (h : 0 < - f x + 1) : f x < 1 := by
  cases n with
  | zero =>
    change 0 < (fun y => - f y) x + 1 at h
    linarith
  | succ => linarith

[Kyle Miller]

@Heather Macbeth I think so long as you don't have any student tacticians who might try writing something too fancy, the meta code in this comment should do global beta reduction between all tactic steps, except for inside tactics like rw. (Caveat emptor: it should probably be better tested!)

[Yaël Dillies]

Wow! Progress was quick.

[Anand Rao Tadipatri]

Kyle Miller said:

Anand Rao It doesn't appear to be necessary to do it, but if you're interested here's another version that overrides by without needing to re-implement by or create any new syntax. It does a syntax transformation ahead of time, while also overriding the other sequencing tactics just in case there's a macro expansion and we want to intervene.

Thanks! This is very helpful.

[Kyle Miller]

I'm surprised it worked out! @Anand Rao's idea of transforming the syntax (which I hadn't considered myself since it seemed impractical) ended up actually being practical, which I'm not sure I'd have believed without seeing the first implementation.

[Yaël Dillies]

Kyle Miller said:

I do want to mention that in Patrick's tutorials, number 0079 is a source of periodic questions since pp.beta is set to true but it's easy to get lambdas in this exercise, and these cause linarith to mysteriously fail.

Eg https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Unexpected.20behaviour.20of.20linarith

[Heather Macbeth]

Thank you for working on this, Anand and Kyle!

I tried it and it solves my beta-reduction problem with Function.Injective beautifully. Here is another related annoyance which it doesn't solve:

notation3 "forall_sufficiently_large "(...)", "r:(scoped P => ∃ C, ∀ x ≥ C, P x) => r

example : forall_sufficiently_large n : ℤ, n ^ 3 ≥ 4 * n ^ 2 + 7 := by
  use 5
  sorry

(Need to add the import

import Mathlib.Mathport.Notation

to Kyle's code.)

[Heather Macbeth]

I get the goal state

⊢ ∀ (x : ℤ), x ≥ 5 → x ^ 3 ≥ 4 * x ^ 2 + 7

after the use 5, just as desired. But the goal state before the use is not beta-reduced:

⊢ ∃ C, ∀ (x : ℤ), x ≥ C → (fun n => n ^ 3 ≥ 4 * n ^ 2 + 7) x

[Heather Macbeth]

Some ideas for fixing this:

• also beta-reduce at the start of the tactic block, before any tactic?
• fix this one by just pretty-printing with pp.beta (once that's implemented) and ignoring the internals?
• fix my "sufficiently large" notation so that it pretty-prints (it doesn't currently) so that this issue is moot?

[Yaël Dillies]

I'm now wondering whether beta-reducing everything in sight might have undesirable side effects. It will turn ∑ x, f x into finset.univ.sum f, which is unfortunate. Is it possible to tag specific arguments to a function as "beta-irreducible"? (Note, this isn't specific to this "beta-reduce everything" approach. I personally get this kind of misbehavior a lot when using simp_rw)

[Kyle Miller]

It looks like it's beta reducing is happening before use, but it's just not being reported if your cursor is in any of the whitespace leading up to use. Your cursor has to be right before the u. I haven't been able to figure out how to fix this (even using the idea to wrap the contents of a by block with the beta reducer).

[Kyle Miller]

@Yaël Dillies Isn't that eta reduction, not beta reduction?

[Heather Macbeth]

Maybe then we want a hybrid approach: the po.beta option to make it display correctly, together with the tactic block beta-reduction-at-each-step to make it behave correctly.

[Kyle Miller]

Another question is whether we can make a hook of our own to preprocess expressions before they're pretty printed, since then we can ensure we perform the exact same transformations.

[Kyle Miller]

@Heather Macbeth Here's a "pretty printer option" hack for pp.beta:

open Lean PrettyPrinter Delaborator

def betaReduceFirst : Delab := do
  let e ← SubExpr.getExpr
  let e' ← Core.betaReduce e
  if e == e' then failure
  withTheReader SubExpr (fun cfg => { cfg with expr := e'}) delab

attribute [delab app, delab lam, delab forallE, delab letE, delab mdata, delab proj]
  betaReduceFirst

[Kyle Miller]

Maybe it's safe (or even better) doing just delab app rather than every expression type, and if so there's probably a better function than Core.betaReduce that would just beta reduce the current application.

(attribute [delab app] betaReduceFirst alone definitely works for the forall_sufficiently_large example)

[Heather Macbeth]

Nice!! Thanks!

[Yaël Dillies]

Oh yeah, sorry. I shall repost my concerns in an eta thread.

[Heather Macbeth]

@Kyle Miller Can you PR it? It would be nice to make sure this continues to work, I'm not confident in my ability to maintain it.

[Reid Barton]

Would it be reasonable/possible to make the notation forall_sufficiently_large itself beta reduce the application P x?

[Kyle Miller]

@Reid Barton Looks like it. This seems to work:

syntax (name := beta_reduce) "beta_reduced% " term : term
@[term_elab beta_reduce] def elabBetaReduce : Elab.Term.TermElab := fun stx expectedType? => do
  let e ← Elab.Term.elabTerm stx[1] expectedType?
  let e ← Core.betaReduce e
  return e

notation3 "forall_sufficiently_large "(...)", "r:(scoped P => ∃ C, ∀ x ≥ C, beta_reduced% P x) => r

[Reid Barton]

Nice! Does Core.betaReduce only beta-reduce the outermost application, or could it also apply to stuff inside P?

[Kyle Miller]

It's global, so this would be more controlled:

syntax (name := beta_reduce) "beta_reduce_app% " term : term
@[term_elab beta_reduce] def elabBetaReduce : Elab.Term.TermElab := fun stx expectedType? => do
  let e ← Elab.Term.elabTerm stx[1] expectedType?
  let e := Expr.beta e.getAppFn e.getAppArgs
  return e

notation3 "forall_sufficiently_large "(...)", "r:(scoped P => ∃ C, ∀ x ≥ C, beta_reduce_app% P x) => r

[Kyle Miller]

It might still beta reduce more than you bargained for, but at least it's localized to a single application sequence.