let x = LHS

Stream: general

[Kevin Buzzard]

As sometimes happens, my goal is currently FPTB.res BU _ _ s = si i and my proof that these two things are equal is going to involve showing that they're both the unique object with some property. I am in tactic mode. I need to hence feed both sides into a bunch of machinery (the proofs that each side has the property are quite different). The underscores are proofs. I want to write "now let x be the left hand side" just to make things easier to handle, but the proof terms are probably nightmares. I am hoping there's a cute one-liner which lets me do this, based on the fact that I sometimes use to_lhs in conv mode. But I don't think to_lhs exists in tactic mode.

[Mario Carneiro]

does let x := FPTB.res BU _ _ s work?

[Mario Carneiro]

Here's a cute one-liner: show let x := _ in x = si i, intro x

[Andrew Ashworth]

can you do the same sort of thing with generalize?

[Andrew Ashworth]

i don't have lean on this computer so i can't check myself

[Mario Carneiro]

It's not a bad idea, but no, generalize does not introduce let binders, only regular variables

[Mario Carneiro]

The best part about generalize with let is that it doesn't suffer the same problems with type incorrectness as generalize itself, since the replacement is definitional

[Kevin Buzzard]

does let x := FPTB.res BU _ _ s work?

It works in the sense that no error appears, but all of a sudden I have 4 goals not 1.

[Kevin Buzzard]

Here's a cute one-liner: show let x := _ in x = si i, intro x

show tactic failed

[Kevin Buzzard]

and what if both sides had suppressed-proofs?

[Kevin Buzzard]

This is hardly a serious issue, I mean I could turn proofs on and just copy what it said I guess...

[Mario Carneiro]

What order are the goals? let x := FPTB.res BU _ _ s, show x = si i should kill most of the auxiliary goals

[Mario Carneiro]

you should be able to do this by unification, no need to copy down those proofs

[Mario Carneiro]

does change give a better error message than show in the one-liner?

[Kevin Buzzard]

wooah one of my proofs is cool

[Kevin Buzzard]

sheaf_property._proof_6 U β Ui Hcover i

[Kevin Buzzard]

you should be able to do this by unification, no need to copy down those proofs

I like your way of thinking

[Mario Carneiro]

This seems to work in my mockup example:

example (LHS RHS : nat) : LHS = RHS :=
begin
  let x, show x = RHS,
end

[Kevin Buzzard]

change let x := _ in x = si i -> don't know how to synthesize placeholder [some term involving all the proofs = si i]

[Kevin Buzzard]

let x := FPTB.res BU _ _ s, show x = si i -- this is the answer

[Mario Carneiro]

The whole definition of the let is optional since it is inferred by the show

[Kevin Buzzard]

Sorry so slow, one of my monitors just died, so it's like I'm back in 2015 with only one screen

[Kevin Buzzard]

I might steal one of the kids' monitors, they're all still in bed

[Kevin Buzzard]

let x := _, show x = si i -- this is the best answer

[Kevin Buzzard]

but it's a hack because what if the RHS had also been full of implicit proofs?

[Kevin Buzzard]

but it'll do for now -- thanks :-)

[Mario Carneiro]

I bet even let x, show x = _ works

[Kevin Buzzard]

Indeed it does.

[Kevin Buzzard]

let x,

[Kevin Buzzard]

wtf?

[Mario Carneiro]

All parts of a let or have are optional

[Mario Carneiro]

you can even just have,

[Kevin Buzzard]

It's the := being optional I didn't know about :-)

[Mario Carneiro]

I'm sure you are familiar with omitting := in a have x : property, tactic

[Kevin Buzzard]

I guess so

[Kevin Buzzard]

thanks!

[Mario Carneiro]

Note that this only works in tactic mode, in term mode it's not so flexible

[Kevin Buzzard]

I was tempted to go into conv mode and use to_lhs

[Kevin Buzzard]

but was scared that if I had to do anything at all in conv mode then I would fail

[Kevin Buzzard]

e.g. prove something

[Kevin Buzzard]

This way is a much better way.

[Mario Carneiro]

Show is super useful, don't underestimate the power of unification with _

[Kevin Buzzard]

Yes, that was the insight.

[Kevin Buzzard]

That I could use unification to fill in the holes.

[Kevin Buzzard]

I just wanted to copy them

[Sebastian Ullrich]

Only thing missing is allowing metavariables instead of _ that can be referenced afterwards :)

[Mario Carneiro]

You can still achieve most of this with unification

[Kevin Buzzard]

Summary for casual readers: let x, show x = _ works for me and answers the original question -- it lets x be the left hand side of a goal of the form X = Y. It looks powerful enough to work in great generality.

[Mario Carneiro]

Do you know why my show let solution failed? Looks like the type checking complained too early

[Kevin Buzzard]

Hmm -- change let x := _ in x = si i actually gives don't know how to synthesize placeholder; context = blah blah blah, ⊢ ?m_1

[Sebastian Ullrich]

I think let checking the value independent from the body is a feature

[Mario Carneiro]

fair enough - I forgot that change doesn't create metavariables but only unifies. let x, has the behavior I intended and also unifies properly in the show line, so I guess it's fine

[Chris Hughes]

I bet even let x, show x = _ works

Is there a version of this trick for term mode, when I want to rw something in a hypothesis and not my goal?

[Mario Carneiro]

You can rw in a hypothesis in term mode by using eqn ▸ h in place of h wherever it gets used. (You may need eqn or eqn.symm depending on orientation of the equation.)

[Kevin Buzzard]

This came up with me specifically because I could not use rw because I only wanted to rewrite a certain term on the LHS, and it showed up on both sides.

[Chris Hughes]

conv!

[Kevin Buzzard]

Actually I am lying, I remember now, it was because there were suppressed proofs everywhere.

[Kevin Buzzard]

Although in the unfolding carefully thread the issue is raised about what happens when conv mode doesn't have the tactics you want.

[Kevin Buzzard]

Conversely, did you see the transitive trick?

[Kevin Buzzard]

Maybe you can let y := RHS, then rewrite in the hypothesis to get LHS = y and then just rw on the hypothesis (rw ... at H works)

[Kevin Buzzard]

(or the triangle business)

[Patrick Massot]

All this discussion is probably worth a new tips and tricks file in mathlib/docs/extras/