unknown free variable

Stream: mathlib4

[Yury G. Kudryashov]

I get the following error: unknown free variable '_uniq.56988'. The proof is here:

theorem Tendsto.isCompact_insert_range_of_cofinite {f : ι → α} {a} (hf : Tendsto f cofinite (𝓝 a)) :
    IsCompact (insert a (range f)) := by
  letI : TopologicalSpace ι := ⊥; haveI : DiscreteTopology ι := ⟨rfl⟩
  rw [← cocompact_eq_cofinite] at hf
  exact Tendsto.isCompact_insert_range_of_cocompact hf continuous_of_discreteTopology

It is also here: https://github.com/leanprover-community/mathlib4/pull/1913/files#diff-168d6c7ac4acb6033bfdf68bf30e50796594b04d24beb36a8ad595e729b9a6ecR572

[Yury G. Kudryashov]

Any ideas what can be the reason?

[Yury G. Kudryashov]

I found the reason: rw [← cocompact_eq_cofinite] generates a free var (as rw in Lean 3 sometimes did) but doesn't register it as a goal.

[Yury G. Kudryashov]

Specifying ι solves the problem.

[Kevin Buzzard]

Can you minimise?

[Yury G. Kudryashov]

I'll try to do it tomorrow. I've got a cold, so I'm thinking much slower than usual.

[Reid Barton]

I've also seen the same form of error message in what looks like a totally different situation, where I didn't understand what's going on.

[Reid Barton]

Does recover do anything in this example? It sounds a bit different than a metavariable not getting assigned.

[Yury G. Kudryashov]

You can checkout this branch and have a look.

[Yury G. Kudryashov]

Or I can do it later.

[Mario Carneiro]

This error message usually indicates a missing withContext

[Mario Carneiro]

Why are there letI and haveI calls in this example? The lean 4 way to spell that is let,have; letI and haveI mean something else now

[Yury G. Kudryashov]

What do they mean now?

[Yury G. Kudryashov]

mathport translated letI and haveI as letI and haveI, I didn't touch these lines.

[Mario Carneiro]

?? it should not have

[Yury G. Kudryashov]

I'll double check.

[Mario Carneiro]

the I means "inline" - haveI x := a; b elaborates to b[x/a] while have x := a; b elaborates to (some metadata over) (fun x => b) a

[Yury G. Kudryashov]

https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Topology/SubsetProperties.lean#L639

[Yury G. Kudryashov]

I'm going to try it with have/let

[Mario Carneiro]

Hm, it looks like @Gabriel Ebner changed it to introduce haveI at some point. Why is that?

[Eric Rodriguez]

Mario Carneiro said:

the I means "inline" - haveI x := a; b elaborates to b[x/a] while have x := a; b elaborates to (some metadata over) (fun x => b) a

this is really confusing to us lean3 users - I know instances don't need resetting anymore but I assumed this was just a normal porting thing and for example this could've been just declared as a synonym for ease of use

[Eric Rodriguez]

I think it's really important to flag the difference so even if it's not fixed at mathport end, it's fixed in mathlib4

[Eric Rodriguez]

(also, this can definitely be useful for introducing haves and lets in such a way to just shorten proofs, without causing any weird syntactic difficulties!)

[Mario Carneiro]

Note that have-the-tactic in lean 3 was actually inlining in this sense

[Mario Carneiro]

have-the-term was not

[Mario Carneiro]

in fact, that might be why it is being aligned like that in mathport

[Eric Rodriguez]

i did know that have-the-term did not, but I did not know that have-the-tactic did. neat.

[Yury G. Kudryashov]

Same with let/have.

[Reid Barton]

I'm confused--there's no way that if you wrote have h := blah blah in Lean 3 and then used h multiple times in the rest of the tactic block, that h was getting duplicated into each use site, right?

[Reid Barton]

What's the difference between Lean 4 haveI and letI then?

[Mario Carneiro]

def foo : nat := begin
  have := 1,
  have := this + this,
  have := this + this,
  have := this + this,
  exact this,
end
#print foo
-- def foo : ℕ :=
-- 1 + 1 + (1 + 1) + (1 + 1 + (1 + 1))

[Mario Carneiro]

Note that this isn't as expensive as you might think since the term is deduplicated

[Reid Barton]

Is this why mathlib is slow?

[Mario Carneiro]

Reid Barton said:

What's the difference between Lean 4 haveI and letI then?

Same as the difference between have and let, except the effects are all felt before getting to the kernel term

[Mario Carneiro]

letI inserts a x : t := e into the local context so simp and friends can unfold it

[Gabriel Ebner]

Mario Carneiro said:

Hm, it looks like Gabriel Ebner changed it to introduce haveI at some point. Why is that?

You correctly guessed it. The have ...; exact ... idiom was mainly used in Lean 3 to declare local instances. Those should not produce a have-term in the elaborated expression and are therefore translated to haveI.