Is there a slicker way to do "apply f to both sides"?

Stream: Is there code for X?

[Terence Tao]

Hi again.

In my informal proof style, I am used to having a hypothesis such as h: complicated_expression_1 = complicated_expression_2 and applying a function f to both sides to obtain a conclusion h': f(complicated_expression 1) = f(complicated expression_2). I would like to do this in Lean without having to keep typing out complicated_expression_1 and complicated_expression_2. Currently the best way I have to do this in Lean is code such as the following

example (complicated_expression_1 complicated_expression_2 : ℕ) (f: ℕ → ℕ) (h : complicated_expression_1 = complicated_expression_2): f complicated_expression_1 = f complicated_expression_2 := by
  have h' : _ := congrArg f h
  assumption

Is there a better way to do this? I would have thought that one of the standard tactics like rw or apply should do this, but I couldn't get the syntax to work.

[Eric Wieser]

apply_fun f at h should work, but your spelling is pretty canonical too

[Eric Wieser]

Note you can drop the : _, and congr_arg is preferred over congrArg

[Terence Tao]

Do I have to import something to get apply_fun or congr_arg to work? I'm getting "unknown tactic" and "unknown identifier" currently.

[Eric Wieser]

Probably import Mathlib.Tactic will help

[Eric Wieser]

It's hard to say exactly why it's not working for you without seeing the full set of imports that make a #mwe, unless of course that (the empty set) is your full set of imports!

[Terence Tao]

Thanks! I was using the empty set of imports for my example.

[Jireh Loreaux]

@Terence Tao the congrm tactic is also very useful, let me find the thread that introduces it.

[Eric Wieser]

If you have no imports at all, then there's another trap hiding there: ℕ is not docs#Nat, but an arbitrary variable {ℕ : Type _}!

[Jireh Loreaux]

here is the thread for congrm: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/congrm

[Eric Wieser]

(deleted)

[Jireh Loreaux]

probably #help tactic congrm in the VS Code extension provides good documentation for its use though.

[Eric Wieser]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Congrm.html and https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/TermCongr.html were the documentation links I should have pasted

[Jireh Loreaux]

Just so it's clear: your example can be achieved with congrm as:

import Mathlib.Tactic.Congrm

example (complicated_expression_1 complicated_expression_2 : Nat) (f : Nat → Nat)
    (h : complicated_expression_1 = complicated_expression_2) :
    f complicated_expression_1 = f complicated_expression_2 := by
  congrm(f $h)

[Terence Tao]

Nice! congrm looks extremely flexible for this sort of thing.

[Terence Tao]

One related question. Given a hypothesis h : complicated_expression_1 = complicated_expression_2, is it possible to extract out the LHS and RHS as expressions without having to type them out explicitly? I'd like something roughly like let LHS := (typeof h).1; let RHS := (typeof h).2, although this particular code doesn't work.

[Yaël Dillies]

It is certainly possible to write a macro for this. I don't think a user-facing one exists right now.

[Jireh Loreaux]

But I'm skeptical this is actually something you want. Can you point to your use case?

[Shreyas Srinivas]

Doesn't conv work for hypotheses? EDIT: It does. Source: The line just above the pattern matching section of conv in tpil

[Eric Wieser]

I was hoping this would work:

import Mathlib

example (h : 1 + 2 = 2 + 1) : true := by
  let LHS : ℕ := ?_
  let RHS : ℕ := ?_
  change LHS = RHS at h
  sorry

but it seems to refuse to unify. It works in Lean 3 (the "open in playground" button will open this in a lean3 editor)

import tactic

example (h : 1 + 2 = 2 + 1) : true :=
begin
  let LHS : ℕ := _,
  let RHS : ℕ := _,
  change LHS = RHS at h,
  sorry
end

[Eric Wieser]

This works:

example (h : 1 + 2 = 2 + 1) : true :=
  let LHS : ℕ := _
  let RHS : ℕ := _
  by
    change LHS = RHS at h
    sorry

but the lets have to be outside the by which is pretty weird. Maybe a metaprogramming expert can chime in about why things are behaving in this way.

[Jireh Loreaux]

Here's a really basic tactic to do this as well. It could certainly be written more efficiently.

import Mathlib.Tactic

syntax (name := let_lhs_rhs) "let_lhs_rhs" term "with" ident ident : tactic

open Lean Expr Meta Elab Tactic

@[tactic let_lhs_rhs] def letSidesTac : Tactic := fun stx => do
  match stx with
    | `(tactic| let_lhs_rhs $e:term with $h₁:ident $h₂:ident) => withMainContext do
        let e ← Elab.Term.elabTerm e none
        let t ← inferType e
        if let .some (type, lhs, rhs) := eq? t then
        liftMetaTactic fun mvarId => do
          let mvarIdNew ← mvarId.define h₁.getId type lhs
          let mvarIdNew' ← mvarIdNew.define h₂.getId type rhs
          let (_, mvarIdNew') ← mvarIdNew'.introNP 2
          return [mvarIdNew']
    | _ => throwUnsupportedSyntax

example (x y : Nat) (h : x = y): True := by
  let_lhs_rhs h with lhs rhs
  trivial

[Eric Wieser]

It would be neat if we could do change ?lhs = ?rhs (or maybe change $lhs = $rhs to be a bit closed to the ~q($lhs = $rhs) we already have) and it did all this for us

[Eric Wieser]

Maybe that's a hint that this should be built on top of Qq

[Jireh Loreaux]

That would have the downside of taking change out of core though.

[Alex J. Best]

You can do

example (h : 1 + 2 = 2 + 1) : True :=
  have a : ?lhs = ?rhs := by exact h
  have as : 2*?rhs + ?lhs = 2*?lhs + 3 := by
    sorry
  trivial

fwiw

[Eric Wieser]

Any idea why it didn't work if I created the metavariables on a separate let tactic?

[Eric Wieser]

Or for that matter, why the by exact is needed?

[Eric Wieser]

It feels like we're navigating a mixture of bugs and unintended behaviors here

[Alex J. Best]

Not really, maybe something to do with metavariable contexts, who knows.

import Mathlib

example (h : 1 + 2 = 2 + 1) : true := by
  let LHS : ℕ := ?_
  let RHS : ℕ := ?_
  have : LHS = RHS := by exact h
  sorry

works too with the by exact

[Terence Tao]

Jireh Loreaux said:

But I'm skeptical this is actually something you want. Can you point to your use case?

Here's a typical thing that shows up in a mathematical argument, particularly in analysis. One needs to bound some expression X, and after a lot of manipulation one ends up demonstrating

h : X \leq complicated_expression_1 + complicated_expression_2 + complicated_expression_3.

Then one often happens is that one writes a line like $=: I + II + III$ in the informal proof, which is implicitly defining

let I := complicated_expression_1
let II := complicated_expression_2
let III := complicated_expression_3

and then one works further to estimate the terms I, II, and III separately, and only at the end of the argument return to h to conclude a final bound for X. This can all be done right now in Lean if one is willing to write out complicated_expression_* several times in the proof itself, but it would be conceptually cleaner if the proof didn't explicitly have to do this, and these complicated expressions were only present in the tactic state.

[Shreyas Srinivas]

I think you are looking for the conv mode I linked above.

[Johan Commelin]

Shreyas, I agree that conv mode can be used, but it still doesn't really match the informal steps that are used on paper, the way Terry describes. Having help from some macro (maybe similar in spirit to congrm) would be helpful, I think.

[Jireh Loreaux]

Oh, I completely understand that (I am an analyst after all). I guess more what I was questioning is why you don't start with:

let I := complicated_expression_1
let II := complicated_expression_2
let III := complicated_expression_3

and then derive:

h : X ≤ I + II + III

and proceed from there? In any case, it seems that what Alex suggested above should work.

[Jireh Loreaux]

I will say, calc type proofs that show up in analysis is one area where our current tooling is lacking, so probably this is just something we want to provide direct support for as Johan mentioned.

[Terence Tao]

Jireh Loreaux said:

Oh, I completely understand that (I am an analyst after all). I guess more what I was questioning is why you don't start with:

let I := complicated_expression_1
let II := complicated_expression_2
let III := complicated_expression_3

and then derive:

h : X ≤ I + II + III

and proceed from there? In any case, it seems that what Alex suggested above should work.

The point is that I would prefer not to explicitly write down complicated_expression_* again, as it is only serving as an intermediate quantity in the argument anyway and having too many expressions of this type makes the proof look intimidating.

Here is a more concrete coding problem: can one solve

import Mathlib

example (X complicated_expression_1 complicated_expression_2 complicated_expression_3 bound_1 bound_2 bound_3: ℕ) (h: X ≤ complicated_expression_1 + complicated_expression_2 + complicated_expression_3) (b1 : complicated_expression_1 ≤ bound_1) (b2 : complicated_expression_2 ≤ bound_2) (b3 : complicated_expression_3 ≤ bound_3) : X ≤ bound_1 + bound_2 + bound_3 := by
  sorry

without explicitly writing down complicated_expression_1, complicated_expression_2, and complicated_expression_3 again? (But usually bound_1, bound_2, and bound_3 are pretty civilized and don't make the proof much scarier-looking if they are written down a few more times in the proof.)

[Heather Macbeth]

One way to do this is:

calc X ≤ complicated_expression_1 + complicated_expression_2 + complicated_expression_3 := by sorry
  _ ≤ bound1 + bound2 + bound3 := ?_
gcongr
· [first bound proof]
· [second bound proof]
· [third bound proof]

[Heather Macbeth]

The disadvantage here is a psychological difference: you are thinking of the three sub-proofs as coming before the endgame, and this way the endgame is presented before the three sub-proofs.

[Heather Macbeth]

So, in your more precise example,

import Mathlib

example (X complicated_expression_1 complicated_expression_2 complicated_expression_3 bound_1 bound_2 bound_3: ℕ)
    (h: X ≤ complicated_expression_1 + complicated_expression_2 + complicated_expression_3)
    (b1 : complicated_expression_1 ≤ bound_1)
    (b2 : complicated_expression_2 ≤ bound_2)
    (b3 : complicated_expression_3 ≤ bound_3) :
    X ≤ bound_1 + bound_2 + bound_3 :=
  calc X ≤ _ := h
    _ ≤ bound_1 + bound_2 + bound_3 := by gcongr

[Terence Tao]

OK, that is workable, and reasonably close to the structure of the informal proof. Thanks!

[Heather Macbeth]

(Noting that typically you wouldn't prove b1, b2, b3 ahead of time, you would let Lean/gcongr formulate them for you based on the structure of the computation, so you didn't need to write out the complicated expressions more than once.)

[Terence Tao]

Yeah, that was an artefact in order to get a minimal working example. Ideally one would never write out the complicated expressions ever, they would only be implicitly stored in the tactic state.

[Heather Macbeth]

That would be ideal but is somewhat beyond current tooling. @Patrick Massot has a tool in progress which will let you get such expressions by clicking on the appropriate sub-expression as displayed in the infoview, so you have to click on it but not write it out. I don't think this tool is merged to mathlib yet, though.

[Johan Commelin]

I think it could aid in readability if we could sometimes write proof steps like:

  suffices : %lhs < bound_1 + bound_2 + bound_3

I suppose that macros %lhs and %rhs aren't too difficult to implement, but I wouldn't know how to do it myself.

[Terence Tao]

So there is nothing like (typeof this).1 to reference this? I don't really know how equality types are structured but this is what I would have naively thought would be the syntax (and also I don't know what the correct version of `typeof' is in Lean4)

[Heather Macbeth]

Currently we can write Johan's proposed macro as

calc _ ≤ bound_1 + bound_2 + bound_3 := ?_
  _ < _ := ?_

[Johan Commelin]

@Terence Tao We can make definitions like this:

def Eq.lhs {X : Type*} {x y : X} (h : x = y) := x
-- and then write

... h.lhs

[Johan Commelin]

But the problem is that you will then have h.lhs appearing in all sorts of places, and you have to explicitly unfold the Eq.lhs away.

[Johan Commelin]

So it would be nicer to have a "meta" place holder.

[Jireh Loreaux]

Right, and Eq.lhs would only work for equality, we would need something else for every expression. I think implementing this with Qq makes sense though.

[Sebastien Gouezel]

Note that not writing the complicated expressions even once may make the proof much harder to read without looking at the goal state. Ideally, one should still retain a readability degree which is comparable to a paper proof, so taking too many shortcuts relying on the framework is not always a good idea.

[Terence Tao]

Well one could still make "assertions" as needed to remind the reader. Something like have : I = complicated_expression_1 by rfl or whatever.

[Jireh Loreaux]

This (Sebastien's comment) is in part why I was suggesting writing let I := ..., let II := ..., let III := ... first. The other reason is that Lean can do more when it knows the expected type, so then proving have : X ≤ I + II + III would probably be easier (e.g., in a calc proof).

[Johan Commelin]

@Terence Tao Agreed, although experience tells me that we're a lazy bunch, and quickly stop writing such assertions.

[Johan Commelin]

"After all, the reader should just look at the goal view" :see_no_evil:

[Heather Macbeth]

I hope that the point-and-click version Patrick is working on will let us be lazy while leaving a readable trace in the code.

[Jireh Loreaux]

Heather, I thought that was already merged, no? #7260

[Terence Tao]

Also I would imagine a non-interactive Lean -> LaTeX converter would also have to have enough of the tactic state embedded in the LaTeX output that one would still see the complicated expressions appear once or twice, much as they already do in informal proofs as a natural consequence of applying all the manipulations.

[Heather Macbeth]

Hmm, I thought the Lean core issue lean4#2652 it exposed had not yet had the fix arrive in mathlib ... maybe I'm behind the times?

[Jireh Loreaux]

I think you're right, #7260 doesn't by itself have all the goodies for calc.

[Adam Topaz]

Concerning getting the LHS and RHS, what do people think about introducing elaborators for this a la

import Mathlib.Lean.Expr.Basic

open Lean Meta

elab "lhs%" t:term : term => do
  let t ← Elab.Term.elabTerm t none
  let tp ← inferType t
  match tp.getAppFnArgs with
    | (``Eq, #[_, a, _]) => return a
    | _ => throwError m!"{← ppExpr tp} is not an equality."

elab "rhs%" t:term : term => do
  let t ← Elab.Term.elabTerm t none
  let tp ← inferType t
  match tp.getAppFnArgs with
    | (``Eq, #[_, _, a]) => return a
    | _ => throwError m!"{← ppExpr tp} is not an equality."

example (a b : Nat) (h : a = b) : Nat := lhs% h
example (a b : Nat) (h : a = b) : (lhs% h) = a := rfl
example (a b : Nat) (h : a = b) : (rhs% h) = b := rfl

[Newell Jensen]

@Terence Tao what I often do if I have expressions that I want to abbreviate is to use abbrev. I then can use the shorter notation in the rest of my code and unfold this definition when it is needed in the proof. There isn't much documentation on abbrev but it works basically like this:

abbrev LHS {i : ℤ} := complicated_experession i

where you can pass arguments, explicit or implicit, on the left hand side which you can use for your complicated expression.

[Newell Jensen]

This is similar to def and so forth.

[Newell Jensen]

Additionally, if you add @[simp] in front of abbrev in your proofs to unfold you can use simp only [LHS]

[Eric Wieser]

abbrev is pretty awkward if the expression in question only exists in the middle of the proof

[Patrick Massot]

Heather Macbeth said:

Hmm, I thought the Lean core issue lean4#2652 it exposed had not yet had the fix arrive in mathlib ... maybe I'm behind the times?

This fix arrived in Mathlib last night but it's going away soon (see #7710) because the new Lean version introduced a completely unrelated bug.

[Patrick Massot]

But if you are lucky you won't see the bug that affects calc. It won't show up in a calculation involving real numbers or natural numbers for instance.

[Newell Jensen]

Eric Wieser said:

abbrev is pretty awkward if the expression in question only exists in the middle of the proof

agreed, abbrev is nice if you are using the complicated expressions in multiple lemmas or theorems, which may be of use to Terence if he plans to use the complicated expressions in more than one lemma or theorem.

[Patrick Massot]

So everything that you can see in the gif from this message is currently available in a recent Mathlib. But indeed this does not include all my plans for this, and it would help with Terry's current question (but Adam's elaborator would).

[Jireh Loreaux]

@Adam Topaz I was thinking of something like the following, which I would call letm (for "let match"). It would take a term with some named holes (or maybe antiquotations instead), e.g., 1 + ?x ^ 2 = ?y, and another term e whose type should match the given expression. We then make all the holes into metavariables, run isDefEq (expression with holes) (← inferType e) which should assign these, and then add the assigned ones to the context with let and the provided name.

[Patrick Massot]

A lot of infrastructure should already be here since this rather close to what congrm is doing.

[Jireh Loreaux]

I know, I'm currently trying to simply understand some of that code.

[Patrick Massot]

Note that it will then be very easy to turn into a widget that looks like the congrm? widget.

[Patrick Massot]

And this as definitely on my TODO list.

[Patrick Massot]

So it you do the hard back-end work then I'll be very happy.

[Terence Tao]

Something resembling the following would I think be very readable and usable by working mathematicians (particularly analysts): starting with a statement like h: X \leq complicated_expression_1 + complicated_expression_2 + complicated_expression_3, it would be nice to have a tactic like rewrite h as X \leq I + II + III for some I, II, III (I know this isn't good Lean syntax, but you should get the point) and this will convert h to h: X \leq I + II + III and introduce three new definitions I := complicated_expression_1, II := complicated_expression_2, III := complicated_expression_3 which can then be manipulated separately without ever having to type out the complicated expressions. (I find that just cut and pasting them from the tactic state stops working once the expressions gets too complicated, mostly due to subtle casting operator issues that I don't really have the expertise or patience to diagnose.)

Having lhs and rhs type operations for arbitrary relations (not just equality), as well as the letm proposal of Jireh, also sound good to me.

[Mario Carneiro]

Terence Tao said:

So there is nothing like (typeof this).1 to reference this? I don't really know how equality types are structured but this is what I would have naively thought would be the syntax (and also I don't know what the correct version of `typeof' is in Lean4)

There is actually a typeof operator, it is spelled type_of% this. But you can't use .1 to get the arguments of an equality, because types are values and there is no function which applied to Eq A B returns A because the function A |-> Eq A B is not injective. You would need to use metamathematical mechanisms to do this, which can look at the syntax Eq A B rather than the value, and unification is the normal one you would use in this case, along the lines of @Eric Wieser 's code example.

[Anatole Dedecker]

Eric Wieser said:

It would be neat if we could do change ?lhs = ?rhs (or maybe change $lhs = $rhs to be a bit closed to the ~q($lhs = $rhs) we already have) and it did all this for us

I think this would be essentially what Eric suggests (but not restricted to lhs and rhs of course)

[Jireh Loreaux]

Terry, my letm proposal should handle your use case as letm X ≤ ?I + ?II + ?III using h (exact syntax TBD).

[Anatole Dedecker]

I think building that on top of change is the cleaner syntactically

[Terence Tao]

OK, thanks for the clarification, that makes sense. I guess one can't have one's cake (invariance under definitional equality) and eat it too (be able to directly reference syntax).

[Terence Tao]

Jireh Loreaux said:

Terry, my letm proposal should handle your use case as letm X ≤ ?I + ?II + ?III using h (exact syntax TBD).

That looks pretty good to me - it would be intelligible to a mathematician not expert in Lean, and would match the flow of the informal mathematical version of argument. Basically as long as all the functional programming type stuff is concealed under very suggestively worded tactics, it should be readable.

[Mario Carneiro]

yeah, you would normally put these metaprograms inside some other file and import it

[Anatole Dedecker]

Some context about change for Terence Tao: currently you can do change _ + _ = _ to reformulate the goal as a definitionally equal form. The change Eric suggested would be to allow naming the underscores, which has the benefit of not really adding "new" syntax for users.

[Anatole Dedecker]

I think it's essentially the same as Jireh's proposal, but I think it would be better to keep the current syntax

[Mario Carneiro]

You "can" name the underscores, this is just an issue with metavariable depths which seems fixable

[Jireh Loreaux]

Can we do that without moving change out of core?

[Mario Carneiro]

(change isn't in core btw)

[Mario Carneiro]

same thing for the issue with let in Eric Wieser 's original version

[Eric Wieser]

Mario, if you have a basic understanding of what's going wrong but don't intend to work on it right now, could you open a Lean4 issue?

[Eric Wieser]

(of course a fix would be great, but I don't want to snipe you!)

[Mario Carneiro]

for change or for let?

[Eric Wieser]

Either/both

[Miguel Marco]

Maybe I am missing the point, but... wouldn't linarith just do this automatically?

[Jireh Loreaux]

linarith is just for proving inequalities. The discussion here is about convenient syntax for assigning names to subexpressions of the type of a given hypothesis, and then introducing those with let myName := subexpression.

[Terence Tao]

For the minimal code example I provided, yes. But in a more practical situation, the bounds b1, b2, and b3 would not yet be in place, and one would have to derive them as part of the task of establishing the final conclusion. Without these sorts of metasyntactic tools, one would have to write out b1, b2, and b3 explicitly at some point, which can make the proof look quite complicated.

[Jireh Loreaux]

@Mario Carneiro , for clarity, are you saying that change should already support the desired behavior, but doesn't because of a bug related to MVarDepth? Or am I misunderstanding?

[Mario Carneiro]

modulo some design questions about metavariable depths, yes

[Jireh Loreaux]

Cool, then I guess I won't work on it!

[Eric Wieser]

I think there's still a feature request here; change ?foo = ?bar creates metavariables, but does not show their values in the infoview

[Mario Carneiro]

I'm not sure you want to be seeing all the metavariables in the infoview

[Jireh Loreaux]

I don't think it's metavariables we want. We're trying to get let declarations for subexpressions determined by the named holes in change.

[Eric Wieser]

Mario Carneiro said:

I'm not sure you want to be seeing all the metavariables in the infoview

I think it's reasonable to see any metavariables given explicit names by the user

[Shreyas Srinivas]

So I found a little time on Saturday night and tried out an idea with very helpful feedback and improvements from @Thomas Murrills

import Mathlib.Tactic
import Lean

open Lean

macro "name " x:ident " := " t:term : tactic => do
  let var_name := TSyntax.getId x
  let eq_name := Name.mkStr var_name "eq"
  let identifier := mkIdent eq_name
  `(tactic|(
    let $x := $t
    have $identifier : $x = $t := by trivial
    repeat rewrite[←$identifier]
  ))

example (n m o : Nat) : n + (m + p) = (n + m) + p := by
  name lhs := n + (m + p)
  rw [lhs.eq]
  exact (Nat.add_assoc n m p).symm


example (n m o : Nat) : n + (m + p) = (n + m) + p := by
  name my_subexp := (m + p)
  sorry

[Shreyas Srinivas]

My next step is to implement this inside conv. After that I plan to use the awesome abilities of conv to navigate through subexpressions and match patterns to write a desugar <expression> as <pattern> tactic.

[Shreyas Srinivas]

Part of my reason to want to put a separate name tactic inside conv is that I have found myself exploring expressions with conv and sometimes wished that I could just put a tag on them.

[Shreyas Srinivas]

@Terence Tao : if you find the redundant appearance of the let and have expression annoying, you can use the filter button on top of the infoview in vscode to hide the let definitions. I needed a way to allow rewrite to work with the definition for convenience.

[Alex J. Best]

This looks very similar to the mathlib set x := blah with h tactic, is there a difference I'm not seeing?

[Yaël Dillies]

Yes, that you don't need to write blah because it's automatically inferred from the LHS of the goal/assumption.

[Kyle Miller]

@Yaël Dillies I don't see this name tactic inferring anything from either goals or assumptions. It appears to be that name x := v is roughly the same as set x := v with x.eq.

[Yaël Dillies]

Oh indeed I misread the syntax.

[Shreyas Srinivas]

It isn't different. Nevertheless I just want a blank slate before I start doing further stuff on top of it. Hopefully debugging will be simpler. set doesn't work inside conv btw. I am writing name to eventually work within conv

[Kyle Miller]

There's not much code to set: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Set.lean

It would be a nice small project to split off the code in the elab_rules into a separate function and then add a conv tactic version.

[Kyle Miller]

Though maybe you do need a separate conv version to be sure that you use the conv rewrite rather than the tactic one. (The conv rewrite makes sure to just rw the LHS of the conv goal.)