28-02-2022There's a famous statistical argument that goes along the lines of, "A monkey seated at a typewriter bashing keys at random will, given enough time, churn out the complete works of Shakespeare." I want to formulate a special case of this argument: "An undergraduate seated at a type checker will, given maybe a Saturday afternoon, churn out the proof to a biconditional."-me, after spending a Saturday afternoon banging on my keyboard with Lean open

```
-- Lean 3
-- needs `meta` because Lean doesn't know
-- how to prove this recursion terminates
meta def collatz : ℕ → ℕ :=
fun | n => if n = 1 then 1
else if n%2 = 0 then collatz (n/2)
else collatz (3*n + 1)
```

```
-- Lean 4
-- needs `unsafe` because Lean doesn't know
-- how to prove this recursion terminates
unsafe def collatz : Nat → Nat :=
fun | n => if n = 1 then 1
else if n%2 = 0 then collatz (n/2)
else collatz (3*n + 1)
```

For defining tactics, we have five new keywords:

```
syntax (name := myTactic) "myTactic" ident (" : " term)? : tactic
-- declares the syntax of myTactic to be `myTactic a` or `myTactic a : t`
-- so myTactic takes in some identifier, and optionally its type
```

```
macro_rules
|`(tactic| myTactic $i:ident) => `(tactic| repeat apply trace "hi")
|`(tactic| myTactic $i:ident : $t:term) => `(tactic| repeat apply trace "hi with type!")
-- notice the powerful syntax matching
```

```
-- Lean 3
meta def swap : tactic unit :=
do gs ← get_goals,
match gs with
| (g₁ :: g₂ :: rs) := set_goals (g₂ :: g₁ :: rs)
| e := skip
end
```

```
-- Lean 4
syntax (name := swap) "swap" : tactic
elab_rules : tactic
|`(tactic| swap) => do
let gs ← getGoals
match gs with
| (g₁::g₂::r) => setGoals (g₂::g₁::r)
| e => setGoals e
```

`set x := y`

for some `y`

already in our contex. Then all we want to do is get the type of `y`

, get the expression of `y`

, and add `x := y`

to our context. Then we can go through our context and change all instances of `y`

with `x`

.
But let's focus on the first part—adding to our context. It seems like it would be simple; afterall, in Mathlib (3) it's just a `definev`

. Lean 4 has a similar `define`

, but integrating it into a tactic is tricky. Here was my solution:
```
private def defineV (nm : Name) (tp : Expr) (tme : Expr) : TacticM Unit := do
liftMetaTactic1 fun mvarId => do
let h2 ← (define mvarId nm tp tme)
let (h, h2) ← intro1P h2
withMVarContext h2 do
return h2
```

With this, we can call `defineV`

inside our tactic. As far as I could fine, there is no tactic that simply adds something to the context as easily as Lean 3's `definev`

(or `assert`

or whatever your favorite method was). Why can't we just plop `define`

into our Lean 4 tactic? It comes back to the new monad types...
`elab_rules`

, we're using the type `tactic`

. If we check out `define`

, we see it's of type `MVarId → Name → Expr → Expr → MetaM MVarId`

. So it's of type `MetaM`

. So, we need to `define`

out of the "universe" of MetaM and into the "universe" of TacticM. That's exactly what `liftMetaTactic1`

does.
Tackling the above

`defineV`

line by line should prove to be informative. `private def defineV (nm : Name) (tp : Expr) (tme : Expr) : TacticM Unit := do`

This tells us that our

`defineV`

function is of type `TacticM Unit`

, so we're able to use it in our tactic!
`liftMetaTactic1 fun mvarId => do`

As just explained,

`liftMetaTactic1`

`liftMetaTactic1`

, we see `(MVarId → MetaM (Option MVarId)) → TacticM Unit`

. So, it takes in a function from `MVarId`

to `MetaM (Option MVarId)`

. What does this mean? Well, `liftMetaTactic1`

applies the input function to the main goal. `let h2 ← (define mvarId nm tp tme)`

Here, we apply

`define`

. Our context should now have gone from `Ctx |- target`

to `Ctx |- let nm : tp := tme; target`

. `let (h, h2) ← intro1P h2`

This introduces the

`let`

statement out of the goal. ```
withMVarContext h2 do
return h2
```

This returns the MVarId resulting from introducting the let statement from the line above.
20-03-2022

I was looking for a way to rewrite the names of variables in my

`set`

tactic. I traveled to a million different
preexisting files looking for a way to do this using `change`

or some core-oriented methods. After writing a (somewhat)
complex `defineV`

function, it was written in my mind that I needed a complicated use of `change`

or something.
In reality, I just needed to rewrite the variable names. Rewrite. Rewrite...
```
evalTactic (← `(tactic| try rw [(id rfl : $pv = $a)] at *))
```

It was such a frustratingly simple solution. So remember to take a step back every once in a while and reevaluate whether what you're
doing is as complicated as it needs to be. Pick your tools right. Don't hammer a screw.