Using Tactics to Generate Theorems

Stream: lean4

[Jeremy Salwen]

In the following example, I am able to use tactics to generate a new theorem from an old theorem. However, if I try to generalize it to a function I can apply to arbitrary lemmas, lean complains that it can't infer the types. I am curious if this is something that can be worked around, or is there a different approach I need here?

import Lean
import Std.Data.Array.Init.Lemmas
import Mathlib.Init.Function

open Lean Lean.Meta

def f: Nat -> Prop := sorry
def g: Nat -> Nat := sorry
def h: Nat -> Nat -> Nat:= sorry

theorem thm: ∀ (n m:Nat), f (g (h n m)) := sorry

theorem equality: ∀ (n m), g (h n m) = n := sorry

-- This works and generates a theorem `substituted_theorem (n : Nat) : f n`
def substituted_theorem := by
  have x := thm
  simp [equality] at x
  exact x

-- This fails to compile
def convertLemma := λ lem => by
  have x := lem
  simp [equality] at x
  exact x

[Sebastian Ullrich]

Neither fun nor intro allow this; you could write your own intro variant that can deal with mvar types

[Jeremy Salwen]

Could you explain a bit more what you mean? What is the issue with mvar types that intro can't handle, and how would it need to be changed to handle it?

[Sebastian Ullrich]

For one, intro actually works for both function types and lets, so it wouldn't know what to do when the type is an mvar. If your new tactic should only generate function types, that shouldn't be a problem.

[Jeremy Salwen]

I vaguely get the idea that I could try to do something like

def convertLemma := by
  intro lem
  have x := lem
  simp [equality] at x
  exact x

But it wouldn't be able to "pull out" an argument from the goal, which is a metavariable? But what would the type of lem even be at that point?

[Kyle Miller]

Can you say what sorts of things you want to do in general? Will it always be "apply simp with these lemmas to this theorem"?

[Jeremy Salwen]

Kyle Miller said:

Can you say what sorts of things you want to do in general? Will it always be "apply simp with these lemmas to this theorem"?

Yes, basically, but I would probably want to use apply and rw in addition to simp.

[Kyle Miller]

Here's a mathlib metaprogram that does this for a particular domain (it generalizes the target of the theorem and then applies some simp lemmas): https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Reassoc.lean

[Kyle Miller]

something that it also gives is a term elaborator, which lets you write theorem foo := reassoc_of% baz

[Kyle Miller]

if that sort of setup is good, then you can skip reading the initialize registerBuiltinAttribute part

[Jeremy Salwen]

Kyle Miller said:

Here's a mathlib metaprogram that does this for a particular domain (it generalizes the target of the theorem and then applies some simp lemmas): https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Reassoc.lean

Thank you! This does seem to be doing what I want to.

[Kyle Miller]

Generally, these sorts of programs aren't written as tactic blocks, but instead using the lower-level MetaM monad (and do notation) to construct a proof. It's possible to execute tactic blocks too if you need them.

[Jeremy Salwen]

Yeah, I started off trying to write a MetaM command, but then I slowly realized I could do more and more with tactics, and thought it might be possible to do the entire thing with forward-mode tactics!

[Jeremy Salwen]

I am curious though, is there a way to enter tactic mode to rewrite an Expr inside of the MetaM monad?

[Kyle Miller]

Could you give a concrete example of what you want to do?

Or maybe you're interested in looking at how synthesizeUsing works? (You could take a look at this branch too for some variations.)

[Jeremy Salwen]

Kyle Miller said:

Could you give a concrete example of what you want to do?

Or maybe you're interested in looking at how synthesizeUsing works? (You could take a look at this branch too for some variations.)

For example,

def upLemma (e : Expr) : MetaM Expr := do
 mapForallTelescope (myMagicFunctionToSwitchToTacticsMode (
    do
      have x:= e
      simp [my_lemma] at x
      apply congrArg my_function at x
      exact bar
   )
   ) e

I don't think synthesizeUsing is quite what I'm looking for, since it requires you to know the type you are synthesize ahead of time.

[Kyle Miller]

I believe you can give it a fresh metavariable and make sure the tactic ends up assigning it (like with exact bar, which would do it indirectly via the type of bar)

[Jeremy Salwen]

Kyle Miller said:

I believe you can give it a fresh metavariable and make sure the tactic ends up assigning it (like with exact bar, which would do it indirectly via the type of bar)

Ok, thanks,I have got this so far:

def upLemma (e : Expr) : MetaM Expr := do
 let mvar ← Meta.mkFreshExprMVar none
 mapForallTelescope (fun e => synthesizeUsing mvar (do
  apply e
  )
 ) e

I am just not sure how to use the tactic syntax to construct a TacticM, since the above treats apply e as a function call, not a tactic application.

[Kyle Miller]

If you take a look at the branch link, there are some small examples of `(tactic| ... ) syntax and evalTactic.

[Kyle Miller]

Embedding an expression inside the tactic syntax isn't immediate though (and you might consider running the non-interactive tactics that the interactive tactics are frontends to yourself). One function is docs4#Lean.Elab.Term.exprToSyntax, but it's in the TermElabM monad, so you need to do some monad lifting to use it.

[Kyle Miller]

for example docs4#Lean.Meta.apply for the non-interactive version

[Jeremy Salwen]

Hmm, it seems like mapForallTelescope does not work well with this approach:

def upLemma (e : Expr) : MetaM Expr := do
 let mvar ← Meta.mkFreshExprMVar none
 mapForallTelescope (fun e => do synthesizeUsing mvar (← `(tactic| exact e))
 ) e

Gives

application type mismatch
  synthesizeUsing mvar __do_lift✝
argument
  __do_lift✝
has type
  TSyntax `tactic : Type
but is expected to have type
  Tactic.TacticM Unit : Type

I thought it would be cool to use tactic syntax here, but I think probably it will be simpler to just find the equivalent functions in the MetaM monad.

[Kyle Miller]

The error here is that synthesizeUsing is expecting a Tactic.TacticM Unit, not a Tactic `tactic

[Kyle Miller]

You need a evalTactic in there to convert, like in the linked branch's code

[Kyle Miller]

But there's another problem that the e inside the tactic syntax is not referring to the e outside. You need to use antiquotations and something like the exprToSyntax I mentioned to link them up.

[Kyle Miller]

The `(tactic| ...) quotation should be thought of as being of the same sort of thing as a string (though more interesting than just a sequence of characters). You need to use antiquotations to splice things (ideally Syntax, not Exprs) into it.

[Jeremy Salwen]

Ah, I was misled by the comment here:
https://github.com/leanprover-community/mathlib4/blob/72c82cf2a8e2ed4dadce4e12d5fc1a97a84128ba/Mathlib/Util/SynthesizeUsing.lean#LL42C1-L47C1

let (gs, e) ← synthesizeUsing ty (← `(tactic| congr!))

Which I think should be

let (gs, e) ← synthesizeUsingTactic ty (← `(tactic| congr!))

I think I understand a bit better now, and I got it working! Many thanks!

import Lean
import Std.Data.Array.Init.Lemmas
import Mathlib.Init.Function
import Mathlib.Util.AddRelatedDecl
import Mathlib.Util.SynthesizeUsing
import Mathlib.Lean.Meta
import Mathlib.Lean.Meta.Simp
import Lean.Elab.Term

open Lean Meta Elab Term Lean.Meta Tactic
open Mathlib.Tactic

def upLemma (e : Expr) : MetaM Expr := do
 let mvar ← Meta.mkFreshTypeMVar
 synthesizeUsing mvar (do evalTactic (← `(tactic| exact $(← exprToSyntax e))))

elab "upLemma% " t:term : term => do
  upLemma (← elabTerm t none)

def z := upLemma% (@Array.push_data Nat)

[Kyle Miller]

@Jeremy Salwen Sorry for the documentation being misleading (and for being a beta tester!). I've corrected it and added a more sophisticated example based on your code: https://github.com/leanprover-community/mathlib4/blob/9cb74d7cb7610ada87159591070e2a21da966c79/Mathlib/Util/SynthesizeUsing.lean#L69-L78

It turns out there's a big gotcha with this approach that took me a while to get to the bottom of. I was testing out

(← `(tactic| have h := $(← Term.exprToSyntax e); simp at h; exact h))

for a simpTerm% term elaborator. It looks fine, but in the case I was trying (simpTerm% h where h : a + 0 = b) it didn't appear to be simplifying!

It turns out that if simp applies a rfl lemma to a local hypothesis, it doesn't really do anything to the proof term and it just changes the type. Since a + 0 = a is true by definition for Nat, then while simp at h was giving h : a = b, the exact h would have the original unsimplified type.

There's a fix though: do exact id h instead. This captures the type of h as it appears in the local context.

[Kyle Miller]

I thought I'd mention this in case you also run into mysterious errors.

[Mario Carneiro]

there is a function like mkExpectedTypeHint for handling this

[Kyle Miller]

Yeah, I think the underlying issue is that simp uses docs4#Lean.MVarId.replaceLocalDeclDefEq, which isn't using mkExpectedTypeHint to record the change...

[Kyle Miller]

so this exact id h thing is a workaround. I guess it could also be used after synthesizeUsing to add a hint using mvar as the new type (part of this is just an exercise to do as much as possible in a tactic script rather than using non-interactive tactics)

[Kyle Miller]

Here's with mkExpectedTypeHint:

def simpTerm (e : Expr) : MetaM Expr := do
  let mvar ← Meta.mkFreshTypeMVar
  let e' ← synthesizeUsing' mvar
    (do evalTactic (← `(tactic| have h := $(← Term.exprToSyntax e); simp at h; exact h)))
  Meta.mkExpectedTypeHint e' mvar

elab "simpTerm% " t:term : term => do simpTerm (← Term.elabTerm t none)

variable (h : a + 0 = b)
#check simpTerm% h
-- ... : a = b

[Jeremy Salwen]

@Kyle Miller Thanks so much for helping with this!