by { }

Stream: mathlib4

[Yaël Dillies]

What's the equivalent of one-line by { } proofs?

[Scott Morrison]

just leave out the braces?

[Scott Morrison]

by X; Y <;> Z

[Jireh Loreaux]

And use ;

[Yaël Dillies]

Not a MWE but is

refine' ⟨fun h ↦ _, by rintro ⟨rfl, rfl⟩; refl⟩

supposed to work?

[Jireh Loreaux]

Seems syntactically valid.

[Yaël Dillies]

Fails in mathlib4#840 but you're welcome to prove me wrong!

[Scott Morrison]

It was a different problem.

[Scott Morrison]

simpa has changed behaviour slightly, I've pushed a fix

[Scott Morrison]

Note A; B no longer means "do B to all goals from A"

[Scott Morrison]

for that you need <;>

[Scott Morrison]

Then, the other change is that simpa using h will fail it if simplifies h to False. You have to change this just to simp at h.

[Yaël Dillies]

Yeah, I thought so too, so I tried ; ... <:>, but you did <;> ... ; instead?

[Yaël Dillies]

Wait sorry, why does simplifying it to False make it fail?

[Scott Morrison]

In your case, the simpa using h was doing something pretty weird: there were two goals open. It killed the first one during the simp at h stage, and then tried exact h on the second goal, but by then h wasn't in scope anymore (rather: there was an h in scope, but a different one)

[Scott Morrison]

Because if simp at h reduces h to False it will immediately close the goal.

[Scott Morrison]

and simpa is currently not smart enough to realise it shouldn't try assumption.

[Scott Morrison]

This should be fixed; someone needs to make a PR to std, where simpa now lives.

[Scott Morrison]

(The reason I knew something weird was happening with the goals was that the error message had a tombstone next to the h, indicating it wasn't the h I thought it was.)

[Yaël Dillies]

That calls for more questions than it answers :^)

1. Haven't we fixed the fact that simpa doesn't focus on one goal?
2. Can't we use the same name for different hypotheses through goals anymore? I thought it was a great, if not hacky, feature, as that means you can run the same proof in parallel when doing a case bash.

[Yaël Dillies]

Oh I guess that answers 1 actually no, we are talking about different things. But I still don't see why the h in the second goal was a different h. It was introduced with the same lambda.

[Scott Morrison]

sort of... :-) There are two different hs here. When you use <;> it correctly uses the correct h in each branch of the proof (see the fix I pushed). However when simpa using h did something wonky switching from one goal to another, Lean correctly detected that it was talking about the wrong h!

[Scott Morrison]

There's certainly a problem in simpa, but Lean 4 handled the bad instructions it received well.

[Mario Carneiro]

Oh, I had some recent fixes to simpa but apparently they weren't pushed. Is there a MWE for the issue you folks are talking about so I can see if this issue has already been fixed?

[Mario Carneiro]

(It appears I can't even look at the original PR, since it was force-pushed away. Please don't do that to issues which have been permalinked to zulip.)

[Yaël Dillies]

Yes you can. I just force-pushed over Ruben's fix as I had a better fix in local, but the first commit still has the error mentioned here.

[Mario Carneiro]

can you please MWE it?

[Mario Carneiro]

I don't even see simpa in the code

[Mario Carneiro]

Actually, reading Scott's description of the issue I'm pretty sure it's exactly what I was trying to fix, so I think I'll just leave it at that.

[Yaël Dillies]

Ah sorry, actually Scott answered #839 on this thread that was about #840. #839 is where the failing simpa is.