How to learn to write tactics?

Stream: new members

[Kenny Lau]

There's a tactic that I want to write, and I'm starting off with basically zero knowledge of tactics, and I've been following the following algorithm:

1. Find an existing tactic with similar behaviour
2. Copy the source file to Lean 4 Web
3. Try to follow every step of the tactic (putting it in the web editor helps me to click around)

Is there a more efficient algorithm that I can follow? (I suppose I could open it in VSCode as well, but beyond that?)

[Arthur Paulino]

I think https://leanprover-community.github.io/lean4-metaprogramming-book/ would improve your skills to read and understand existing tactics

[Arthur Paulino]

<deleted>

[Chris Bailey]

You can leverage your social connections here and get someone who knows more about writing tactics to help.

[Kevin Buzzard]

Heather's course https://github.com/hrmacbeth/metaprogramming was interesting but it wasn't designed for remote learning, "you had to be there" basically.

[Kevin Buzzard]

did she give lectures about this stuff at Simons and are they videoed?

[Patrick Massot]

Kenny, see also https://github.com/mirefek/lean-tactic-programming-guide

[Kenny Lau]

Thanks!

[Kenny Lau]

I would like to announce that I successfully wrote my first tactic in #28072 :tada:

[Kenny Lau]

(golfing/general advice is very welcome)

[Kenny Lau]

import Mathlib

open Lean

initialize registerTraceClass `rw_equiv_tac

set_option trace.rw_equiv_tac true
-- unknown option 'trace.rw_equiv_tac'

[Kenny Lau]

Does register only work in the next file?

[Kenny Lau]

so i've been told that Qq is very hard to debug

[Kenny Lau]

it's complaining about a type mismatch and i don't know how to fix it

[Aaron Liu]

#mwe?

[Kenny Lau]

also, the expected type window doesn't work very well for me, it seems to be always stuck on the previous state

[Kenny Lau]

import Mathlib

open Lean Meta Tactic Simp Qq

simproc matrix_diagonal (Matrix.diagonal _) := .ofQ fun u α M? ↦ do
  let .succ u := u | return .continue
  let ~q(@Matrix (Fin (OfNat.ofNat $k?)) (Fin (OfNat.ofNat $k?)) $R) := α | return .continue
  let ~q(@Matrix.diagonal.{u, 0} (Fin (OfNat.ofNat $k?)) $R $dF $zR $v) := M? | return .continue
  return .continue

[Aaron Liu]

yeah Qq is sort of broken sometimes

[Kenny Lau]

error:
type mismatch
Matrix.diagonal ?m✝
has type
Matrix (Fin (OfNat.ofNat ?m✝)) (Fin (OfNat.ofNat ?m✝)) ?m✝¹ : Type u
but is expected to have type
«$α» : Type u

[Aaron Liu]

oh I fixed it

[Aaron Liu]

import Mathlib

open Lean Meta Tactic Simp Qq

simproc matrix_diagonal (Matrix.diagonal _) := .ofQ fun u α M? ↦ do
  let .succ u := u | return .continue
  let ~q(@Matrix (Fin (OfNat.ofNat $k?)) (Fin (OfNat.ofNat $k?)) $R) := α | return .continue
  let ~q(@Matrix.diagonal.{u, 0} (Fin (OfNat.ofNat _)) _ $dF $zR $v) := M? | return .continue
  return .continue

[Kenny Lau]

do you know how to read the correct expected type?

[Kenny Lau]

oh... i have to do the french quotes? lol

[Aaron Liu]

probably not?

[Aaron Liu]

I was just trying things until it worked

[Kenny Lau]

i just compared your code with mine and only saw the french quote as the difference

[Aaron Liu]

yeah it works without them too (edited)

[Kenny Lau]

well, ok, so it works with _ or with french quotes «$k?», just not with $k?

[Aaron Liu]

yeah

[Aaron Liu]

I think it's because just $k? will make it a pattern variable

[Kenny Lau]

Lean.Meta.mkForallFVars

[Kenny Lau]

Is there a Qq version of taking the "forall closure"?

[Aaron Liu]

I don't think you can use Qq to do that

[Aaron Liu]

since it doesn't store the context your Exprs are supposed to be typed in

[Aaron Liu]

maybe you can

[Aaron Liu]

actually probably not

[Aaron Liu]

since what would the type be?

[Aaron Liu]

maybe just stick to the non-Qq stuff

[Kenny Lau]

import Mathlib

open Qq Lean

def unapp {u : Level} {G H : Q(Type u)} {mG : Q(Group $G)} {mH : Q(Group $H)}
    (f : Q($G →* $H)) (y : Q($H)) : MetaM (Option Q($G)) := do
  trace[debug] m!"{f}, {y}"
  -- let ~q($f $x) := y | return .none
  -- return .some y
  have fx := y.getAppFnArgs
  return (fx.snd)[5]?

axiom G : Type
axiom H : Type
@[instance] axiom gG : Group G
@[instance] axiom gH : Group H
axiom f : G →* H
axiom x : G

#eval unapp q(f) q(f x)

[Kenny Lau]

so I tried to use Qq to match f x where f is a group hom, and it doesn't work

[Kenny Lau]

the code above correctly extracts x from f x, without using Qq

[Kenny Lau]

the two commented lines are my Qq attempt, which has error (comment out the two lines below that)

[Kenny Lau]

how do I fix this?

[Aaron Liu]

Not sure if this is how you're supposed to do it

def unapp {u : Level} {G H : Q(Type u)} {mG : Q(Group $G)} {mH : Q(Group $H)}
    (f : Q($G →* $H)) (y : Q($H)) : MetaM (Option Q($G)) := do
  let ~q(DFunLike.coe «$f» $x) := y | return .none
  return .some x

[Kenny Lau]

aha, we're back to the french quotes

[Kenny Lau]

aha, you don't even need coe

[Kenny Lau]

thanks!

[Aaron Liu]

The generated code just checks if it's reducibly defeq to f ?x where ?x is a fresh metavariable, without assigning any other metavariables