Reverse cancelling/'same thing on both sides'

Stream: general

[Robert Maxton]

What's the idiomatic way to, for example, multiply both sides of an equation by the same object (in contexts where that makes sense)? @mul_left_cancel works, technically, but there doesn't seem to be a good way to tell Lean what to 'un-cancel' without first working my way through the rest of the implicit arguments. I'm almost tempted to just put an alias at the top of my code to make just the first parameter non-implicit; is there a better way?

[Kevin Buzzard]

By "equation" do you mean a goal or a hypothesis? If the goal then I sometimes just write suffices : a*b=a*c, exact mul_left_cancel this.

[Robert Maxton]

Goal in this case, though I'm curious about hypotheses as well.

That works, thanks!

[Kevin Buzzard]

For hypotheses of course you need the argument the other way. If you have h : a*b=a*c you can replace h := mul_left_cancel h and if you have h : b = c then you don't need mul_left_cancel, you can do something like apply_fun (λ x, a * x) at h.

[Robert Maxton]

... How did I manage to work through all the tutorials I could find without meeting apply_fun? >.>

Thanks, that's really helpful.

[Johan Commelin]

Because it's a tactic that isn't actually that old

[Mario Carneiro]

I still think the name is terrible, because it doesn't apply a function

[Mario Carneiro]

it should be congr at h

[Robert Maxton]

does it not?

[Reid Barton]

How would it know what function to, uh, definitely not apply?

[Mario Carneiro]

congr f at h?

[Kevin Lacker]

mul_left a at h

[Mario Carneiro]

apply f at h should do the equivalent of replace h := f h

[Bryan Gin-ge Chen]

Robert Maxton said:

... How did I manage to work through all the tutorials I could find without meeting apply_fun? >.>

Thanks, that's really helpful.

Here's the info about apply_fun on our tactic docs page: tactic#apply_fun

The list of tactics there is much more complete.

[Mario Carneiro]

congr f at h should do the equivalent of replace h := congr_arg f h

[Mario Carneiro]

@Kevin Lacker That would balloon the number of named tactics, which would make navigating the documentation much harder

[Mario Carneiro]

I think Johan has a plan for a tactic along those lines though

[Kevin Lacker]

lol. so basically you are saying 1. if we do this then the documentation will be impossible to understand, 2. and it's already in progress! excellent :grinning_face_with_smiling_eyes:

[Mario Carneiro]

the difference is that johan's tactic is more like calc_step a * h IIRC

[Kevin Buzzard]

I remember there being some kerfuffle when @Patrick Massot suggested apply_fun; the main objections from the CS people were that all the tools were there already to do this. The argument from the maths people were that there was a constant stream of undergrads asking how to apply a function to both sides of an equality!

[Kevin Buzzard]

I haven't fully understood what Johan's plans are, but it's interesting to note that IIRC Patrick's first foray into tactic-writing was apply_fun (or at least one of the first), and now Johan is taking his first steps. Me, I'm still terrified :-)

[Mario Carneiro]

Oh, I just had a great idea for a sufficiently flexible interface:

example (a b c d : ℕ) (h1 : a = b) (h2 : c = d) : a * b + a = c * d + c :=
by bikeshed λ h1 h2, h1 * h2 + h1

or

example (a b c d : ℕ) (h1 : a = b) (h2 : c = d) : a * b + a = c * d + c :=
by bikeshed h1 h2 in h1 * h2 + h1

The trick is that the expression h1 * h2 + h1 is elaborated with h1 h2 : nat and then they are lambda abstracted to produce the motive for the congr application

[Johan Commelin]

Mario Carneiro said:

the difference is that johan's tactic is more like calc_step a * h IIRC

yup... though it's very much wip. atm it only handles the goal.

[Johan Commelin]

And the name is terrible. Suggestions very welcome!

[Kevin Buzzard]

I like bikeshed.