apply bug

Stream: general

[Reid Barton]

So I finally understand the exact reason for the apply bug, and it's trickier than I'd guessed. Here is an illustrative example:

import topology.instances.real

variables {α : Type} [ring α] [topological_space α] [topological_ring α]

def f : α → α := λ x, 2 * x + 1

lemma l1 : continuous (f : α → α) :=
begin
  apply continuous.add,
  sorry, sorry
end

lemma l2 : continuous (f : ℝ → ℝ) :=
begin
  apply continuous.add,         -- invalid apply tactic, failed to unify ...
end

apply unfolds the types of the target and the given expression and uses the number of →s to work out how many _s to insert. So here, apply also unfolds continuous f to its definition ∀s, is_open s → is_open (f ⁻¹' s). However, in the target of l2, is_open (f ⁻¹' s) unfolds even further (to something of the form ∀ x ∈ f ⁻¹' s, ...), while in the target of l1 and in the type of continuous.add, is_open (f ⁻¹' s) is stuck (it's a field extractor from the topology instance, which is α or a metavariable). Therefore, apply inserts two fewer _s in l2 and this causes the familiar "apply bug".

[Patrick Massot]

Does it tell you how to fix this in Lean 3.10? (and tell Sebastian how to make sure this will work in Lean 4)

[Reid Barton]

Unfortunately it is not at all clear to me so far how to fix this

[Reid Barton]

apparently Lean 4 already has an apply tactic, though, so conceivably I could try to reproduce the issue there

[Reid Barton]

there is already a hacky fix apply' in mathlib which apparently just implements "try every number of _s"

[Reid Barton]

Maybe it's acceptable if it can be made to produce the same error messages as the current apply (after all, 99% of the errors when using apply interactively will not be due to the apply bug)

[Sebastien Gouezel]

The bug is easy to fix, we just have to make continuous irreducible :) Joke aside, I think this would be a good idea. What do you think?

[Kevin Buzzard]

I thought the fix was refine?

[Reid Barton]

the workaround is refine

[Reid Barton]

I agree making continuous irreducible would be good, or probably better yet a structure.

[Reid Barton]

However, I thought I'd first try to solve the problem at its source

[Yury G. Kudryashov]

Can we make topological_space real instance irreducible?

[Reid Barton]

I don't really like making things irreducible, it makes the library more complex and harder to understand.

[Reid Barton]

There actually isn't a topological_space real instance, it gets created in a rather complicated way

[Reid Barton]

(By "making things irreducible", I mean specifically using attribute [irreducible].)

[Kevin Buzzard]

I think that making real irreducible was a good idea though, because there are two definitions at least, and the user should not be allowed to care about which one we used (I think...)

[Reid Barton]

What I mean is, since real is a Type, we could just make it a structure (with one field), and then it could never be unfolded by anything, without any need for fiddling about with [irreducible].

[Reid Barton]

Unfortunately we can't use the same method for things like real.add which we also want to be irreducible

[Simon Hudon]

Wouldn't it be sufficient to define it as:

def read.add : real -> real -> real
| \< x \> \< y \> := \< ... \>

It would only reduce if you already had \< x \>

[Reid Barton]

That would often help, but you would still be able to prove, for example, 2 + 2 = 4 by rfl

[Reid Barton]

Which I think is quite slow

[Mario Carneiro]

Once upon a time I thought that was a good thing

[Mario Carneiro]

Also, I recall when playing with the apply bug that @[irreducible] made no difference, it would unfold everything