Show tactic failed

Stream: new members

[Gihan Marasingha]

The following gives an error message show tactic failed in the first subgoal of refine. It works fine if I use exact k₁. As far as I can tell, the goal at that point is a → b ∧ a.

What's going on?

variables p q r a b c : Prop

theorem imp_trans1 : (p → q) → (q → r) → (p → r) :=
λ h₁ h₂ h₃, h₂ (h₁ h₃)

example (k₁ : a → b ∧ a) (k₂ : b → c) : a → c :=
begin
  refine imp_trans1 a (b ∧ a) c _ _,
  { show a → b ∧ a, from k₁, },
  { show b ∧ a → c,
    assume k₃ : b ∧ a,
    have k₄ : b, from k₃.left,
    exact k₂ k₄, },
end

[Reid Barton]

lean#437

[Gihan Marasingha]

So the lesson I've learned is not to use a as a variable name!

[Kevin Buzzard]

The a bug is surprisingly rare, at least for me. It's also apparently surprisingly hard to fix. I went through a phase of never using a but now I use it and just change it when I run into the a bug.

[Kevin Buzzard]

Can't we just change things so instead of being an a bug it's an xyzzy bug or something?

[Mario Carneiro]

That would be lean#442, which appears to have stalled somewhere

[Mario Carneiro]

oh, it's currently blocked on lean#447

[Kevin Buzzard]

I thought that this was because we tried to change it to the _a bug. I'm just suggesting xyzzy with no underscore.

[Mario Carneiro]

I'd rather just fix the segfault

[Kevin Buzzard]

That's of course the correct solution.

[Reid Barton]

Even the proposed a -> _x change was going to induce a surprisingly large number of changes h_a -> h__x in mathlib

[Johan Commelin]

But I think it's worth fixing those anyway

[Johan Commelin]

I can spend some time on fixing those, if someone gives me the lean to fix them

[Reid Barton]

but changing them to h_xyzzy probably isn't great, especially if we would change them to something else again later

[Johan Commelin]

But the fix would be to use explicit variable names, right?

[Reid Barton]

I quickly grew tired of trying to do that when I looked at that earlier

[Johan Commelin]

Maybe we can crowdsource it?

[Reid Barton]

What I'm trying to say is it's significantly more annoying than you would think

[Reid Barton]

you can just build Lean with a version of the change in the PR to see

[Johan Commelin]

rg "h_a" | wc -l
241
rg "_a" | wc -l
32547

[Johan Commelin]

I guess it's not only h_a, right?

[Reid Barton]

for example with the xyzzy change

[Reid Barton]

the number is not the issue

[Reid Barton]

if you want to do it the "correct" way of not using an autogenerated name

[Reid Barton]

the issue is some of them are individually hard to deal with

[Johan Commelin]

rg "_a " | wc -l
124

[Reid Barton]

because they are not simple straight-line intro, cases h, exact h_a but complicated stuff involving ; and so on

[Johan Commelin]

Reid Barton said:

if you want to do it the "correct" way of not using an autogenerated name

But we could do it in two stages... first rename everything to h__xyzzy automatically, and then hope that 124 people will each fix one of those issues afterwards.

[Johan Commelin]

I wouldn't mind having h__xyzzy in mathlib if it removes the a bug

[Johan Commelin]

And it will be extra motivation for people to not use autogenerated names in the future

[Reid Barton]

I think the last time I looked Lean 4 did not let you use autogenerated names anyways (by default?)

[Kevin Buzzard]

so it will need to be done at some stage anyway?