Redundant expressions

Stream: lean4

[Rick de Wolf]

Hi all,
I'm working through some algebraic calculation-style proofs. They often end up having a few long algebraic expressions that need to be typed out multiple times in Lean. Here's a still relatively short example where a quadratic polynomial expression is used multiple times.

example {x : ℝ} (h : x = 1 ∨ x = 2) : x ^ 2 - 3 * x + 2 = 0 := by
  obtain h | h := h
  · calc
      x ^ 2 - 3 * x + 2 = 1^2 - 3*1 + 2 := by rw [h]
      _ = 0 := by norm_num
  · calc
      x ^ 2 - 3 * x + 2 = 2^2 - 3*2 + 2 := by rw [h]
      _ = 0 := by norm_num

I want to copy the expression x ^ 2 - 3 * x + 2 that was typed out in the header of the proof in the two calc blocks without typing them out manually. I.e. I want to replace the two instances of this expression inside the calc blocks by some Lean code along the lines of currentTheorem.goal.leftHandSide. How can I approach this? I have a feeling this involves meta programming in Lean but I'm not sure where to find this in the documentation.

[Eric Wieser]

This works:

example {x : ℝ} (h : x = 1 ∨ x = 2) : x ^ 2 - 3 * x + 2 = 0 := by
  refine (?_ : ?lhs = ?rhs)
  obtain h | h := h
  · calc
      ?lhs = 1^2 - 3*1 + 2 := by rw [h]
      _ = 0 := by norm_num
  · calc
      ?lhs = 2^2 - 3*2 + 2 := by rw [h]
      _ = 0 := by norm_num

[Rick de Wolf]

That's it! I'm trying to find documentation for the refine (tactic?) but I'm not succesful so far. Do you know how I can handle the case where the expression I'm interested in is part of one of the hypotheses in the theorem header? I.e.

example {x : ℝ} (h : x ^ 2 - 3 * x + 2 = 0 ∨ x*y=5) : \pi \neq 5 := by
  ...

[Eric Wieser]

This works but is really a hack:

import Mathlib

example {x : ℝ} (h : x ^ 2 - 3 * x + 2 = 0 ∨ x*y=5) : π ≠ 5 := by
  have : ?lhs = _ ∨ _; exact h; clear this
  -- to prove that we captured `lhs`
  let y := ?lhs ^ 2
  sorry

[Eric Wieser]

Maybe @Kyle Miller can come up with a better way using existing tactics

[Edward van de Meent]

maybe something like generalize might help?

[Rick de Wolf]

Hmm, how would you use that? Looking at the hover documentation it seems to be useful for substituting parts of the goal by another expression.

[Edward van de Meent]

it means you get to name an expression, not just substitute for a variable.

[Edward van de Meent]

i.e. when you want to capture some expression e, write gereralize h: e = z, then when you'd like to refer to e, rather refer to z , then rewrite with h.symm.

[Edward van de Meent]

or maybe i'm misunderstanding your questions...

[Rick de Wolf]

What I'm getting from what you said is this:

example {x : ℝ} (h : x = 1 ∨ x = 2) : x ^ 2 - 3 * x + 2 = 0 := by
  generalize hyp : (x = 1 ∨ x = 2) = z at h
  sorry

This leaves the proof state as:

x : ℝ
z : Prop
hyp : (x = 1 ∨ x = 2) = z
h : z
⊢ x ^ 2 - 3 * x + 2 = 0

[Rick de Wolf]

What I want is to be able to capture some subexpression from the theorem header. Then I can re-use it later in the proof without manually typing the expression again and again. E.g.exact (2 + whateverVariableTheSubExpressionEndedUpIn)/\pi where whateverVariableTheSub.... could be a term that could span half a page for example.

[Rick de Wolf]

I feel, and emphasis on feel, like generalize doesn't do what I want, although it does seem like a useful tactic to know in general :)

[Ruben Van de Velde]

Does something like let y = ?_; change y = _ work?

[Eric Wieser]

I assume you saw that I was able to use (mathlib's) have to do something similar above, @Ruben Van de Velde?

[Ruben Van de Velde]

Yeah, but it seemed very convoluted

[Rick de Wolf]

Preferably it would be possible to do this using a short expression. At least these two approaches work for taking a part of a hypothesis or a goal. Maybe the second approach could be shortened using a custom tactic?

[Michael Rothgang]

Does the set tactic help?

[Michael Rothgang]

Writing set P := <long expression> will define P as your long expression, and replace it in your goal wherever it occurs. You can use set P := with h to get a hypothesis P=long expression, to rewriting with if you need it.

[Rick de Wolf]

That's a nice tactic to know about, but it's not exactly what I want. Using let or set is a nice and clean way to store long expressions, but it would still require you to type out the expression you want to copy at least one more time.

[Rick de Wolf]

I feel like there should be some way to access the definition of the goal and the parts that make up that goal. Maybe using metaprogramming. I.e. how I described it before using currentTheorem.goal.leftHandSide. This way you can insert any expression you want while you're in the middle of writing a proof step.

[Damiano Testa]

I think that there was a setm tactic in the making on which @Gareth Ma was working.

I think that this may be up for adoption, but I'll let Gareth comment on that!

[Eric Wieser]

It would be nice if change ?lhs = ?rhs and change ?lhs = ?rhs at h were valid here

[Ruben Van de Velde]

Speaking of randomly sticking metavariables somewhere, I'd love to be able to write things like have : (x + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * ?foo := by ring (tangentially related at best)

[Gareth Ma]

Damiano Testa said:

I think that there was a setm tactic in the making on which Gareth Ma was working.

I think that this may be up for adoption, but I'll let Gareth comment on that!

Yes I was working on the setm tactic, but it has been a while. I don’t quite remember what is blocking it either, but if anyone wants to takeover, feel free to. IIRC it’s most working already, there’s a PR and some tests from the PR that shows how to use it.

[Rick de Wolf]

Sounds interesting, what is the purpose of setm?

[Gareth Ma]

IIRC if u have a goal x^2+y^2=z^2 then u can setm ?x + ?y = ?z and it set all of them. I think the m means set multiple, but not sure

[Gareth Ma]

(Someone else suggested the name - I think Damiano? Lol)

[Rick de Wolf]

Also, @Eric Wieser what is the change tactic meant to do? I can't find it in the docs, my search skills still need some work

[Gareth Ma]

From what I understand change changes the term and type of something to another that’s defeq. For example if you have n+0=3 at a hypothesis then you can change n=3 at h, because n+0 is defeq to n for nat.

[Gareth Ma]

Sorry I’m on phone

[Rick de Wolf]

I am on a train, so same here :)

[Rick de Wolf]

Your setm descriptions sounds quite useful! It would still require a separate line of Lean code to obtain whatever expression you want, and I'd prefer a quick inline version, but maybe I could build on this!

[Rick de Wolf]

I'd need to work on more than just my search skills for that :P I assume setm involves some metaprogramming? Or is it basic Lean?

[Gareth Ma]

6BC93A01-D402-4240-8977-9C287F1B6F8C.jpg

[Rick de Wolf]

Rick de Wolf said:

I'd need to work on more than just my search skills for that :P I assume setm involves some metaprogramming? Or is it basic Lean?

I.e. the code of setm itself requires metaprogramming. Not whether a user of setm would need metaprogramming.

[Rick de Wolf]

Based on your description of change I'm not sure how it helps with expression 'copy-paste'. Could you elaborate @Eric Wieser?

[Eric Wieser]

If the rules were "change is allowed to assign metavariables" then it would work out of the box

[Gareth Ma]

If that’s the case then my setm is duplicating the same functionality?

[Eric Wieser]

Only in the same way that set duplicates generalize, so I think there is still room for setm

[Rick de Wolf]

That's starting to make sense now. So I assume what you'd need to make that work is that a metavariable can be definitionally equal to any expression?

[Eric Wieser]

That's already how it works, see docs#Lean.Meta.isDefEq

[Eric Wieser]

But if you call withNewMCtxDepth, then any metavariables created outside that call are not eligible for that behavior

[Rick de Wolf]

I dont entirely understand what prevents change from being useful in the 'copy-paste' problem, but do you think there is a chance it could be fixed?

[Damiano Testa]

With respect to the name setm is in analogy with congrm and the name there is congr with a match, since the user introduces a pattern that the tactic tries to match in the given goal/hypothesis.

[Eric Wieser]

Eric Wieser said:

If the rules were "change is allowed to assign metavariables" then it would work out of the box

This makes change behave in the way I was suggesting:

elab_rules : tactic
  | `(tactic| change $newType:term $[$loc:location]?) => do
    withLocation (expandOptLocation (Lean.mkOptionalNode loc))
      (atLocal := fun h => do
        let hTy ← h.getType
        -- In a previous iteration, this was a hack to get the new type to elaborate in the
        -- same sort of way that it would for a `show` expression for the goal.
        -- We don't want the semantics of `show` anyway though, so it's not clear whether this
        -- is still a hack.
        let mvar ← mkFreshExprMVar none
        -- using a type ascription rather tha
        let (_, mvars) ← elabTermWithHoles
                          (← `(term | ($(← Term.exprToSyntax mvar) : $newType))) hTy `change
        liftMetaTactic fun mvarId => do
          return (← mvarId.changeLocalDecl h (← inferType mvar)) :: mvars)
      (atTarget := evalTactic <| ← `(tactic| refine_lift (?_ : $newType)))
      (failed := fun _ => throwError "change tactic failed")

Unfortunately, this requires it to assign _all_ metavariables, so now you can't create subgoals with change like you currently can.

[Rick de Wolf]

Sorry for the slight delay in answering :) All of these approaches sound interesting to me, but the first two that were proposed, by Eric, seem like the best way to go for now. The other approaches require typing out the expression one more time, which seems a little "unergonomic" to me. I will hopefully have more time to look into this after I'm back from my holiday, then I'll be able to test these approaches properly :) Thanks for all the suggestions!

[Gareth Ma]

Maybe my definition of "typing out the expression" is different, but I'm pretty sure mine doesn't require that

[Kyle Miller]

I'm sure you have more complicated examples where this wouldn't work, but my approach would be to give a high-level automation-based proof. If you were to explain this to someone, you'd say "just substitute the possible values in for x and then evaluate", right?

example {x : ℝ} (h : x = 1 ∨ x = 2) : x ^ 2 - 3 * x + 2 = 0 := by
  cases h <;> subst_vars <;> norm_num

[Eric Wieser]

@Kyle Miller, do you have a feeling for whether the change to change I propose is possible? The difficulty arises from wanting ?foo to create a metavariable that is either immediately assigned by unification, or deferred to a subgoal if unification fails. Currently the behavior is to always defer and forbid assignment, while my message above always assigns but doesn't allow any deference.

[Kyle Miller]

Are there examples where deference is wanted? I know there are tests for it, but (if I remember correctly) they're there just to make sure that they're handled correctly due to it being theoretically possible, not necessarily useful.

[Kyle Miller]

(It might be worth testing with (id $(← Term.exprToSyntax mvar) : $newType) too. Maybe it was fixed in the meantime, but I remember at some point convert needed an id to make sure some metavariables were collected properly.)

[Eric Wieser]

I could imagine wanting something like

example : foo n x = 0 := by
  change fooHom n ?hn x = 0

where hn : n.Prime or something

[Kyle Miller]

This seems to work:

@[builtin_tactic change] elab_rules : tactic
  | `(tactic| change $newType:term $[$loc:location]?) => do
    withLocation (expandOptLocation (Lean.mkOptionalNode loc))
      (atLocal := fun h => do
        let hTy ← h.getType
        let mvar ← mkFreshExprMVar none
        let (_, mvars) ← elabTermWithHoles
                          (← `(term | (id $(← Term.exprToSyntax mvar) : $newType))) hTy `change
        liftMetaTactic fun mvarId => do
          return (← mvarId.changeLocalDecl h (← inferType mvar)) :: mvars)
      (atTarget := evalTactic <| ← `(tactic| refine_lift (id ?_ : $newType)))
      (failed := fun _ => throwError "change tactic failed")

[Kyle Miller]

def Prime (n : Nat) := n ≠ 1

def foo (n : Nat) : Nat := n
def fooHom (n : Nat) (h : Prime n) : Nat := n

example (h : foo 2 = 4) : foo 2 = 4 := by
  change ?m = _
  let x := ?m
  -- x : Nat := foo 2
  change fooHom _ ?hp = _
  sorry -- fooHom 2 ?hp = 4
  sorry -- Prime 2

[Kyle Miller]

(Each id is necessary to make sure metavariables are collected from the type of the metavariable. It might be a bug in getMVarsNoDelayed but I'm not sure.)

[Eric Wieser]

Happy to PR that?

[Kyle Miller]

If you have time, it'd be worth creating a PR on nightly-with-mathlib and seeing how bad the fallout is with mathlib. I'm not sure when I can get to investigating this one myself.

[Eric Wieser]

lean4#5063

[Eric Wieser]

Unfortunately this is running into batteries#889

[Eric Wieser]

(actually, there are lots of failures)