specifying metavariable

Stream: new members

[Steven Clontz]

In the below #mwe I'm not sure how to supply the metavariable s on line 15 so I can avoid the cludge on lines 21-22:

import Mathlib.Topology.Basic

variable {X : Type u} [TopologicalSpace X]

def IsGδ (s : Set X) : Prop :=
  ∃ T : Set (Set X), (∀ t ∈ T, IsOpen t) ∧ T.Countable ∧ s = ⋂₀ T

class PerfectlyNormalSpace (X : Type u) [TopologicalSpace X] : Prop where
  closed_gdelta : ∀ ⦃h : Set X⦄, IsClosed h → IsGδ h

example (s : Set X) [PerfectlyNormalSpace X] : IsGδ (closure s) := PerfectlyNormalSpace.closed_gdelta isClosed_closure

example (s : Set X) [PerfectlyNormalSpace X] : ∃ T : Set (Set X),
    (∀ t ∈ T, IsOpen t) ∧ T.Countable ∧ closure s = ⋂₀ T := by
  obtain ⟨a, b⟩ := PerfectlyNormalSpace.closed_gdelta isClosed_closure
  -- typeclass instance problem is stuck, it is often due to metavariables
  sorry

example (s : Set X) [PerfectlyNormalSpace X] : ∃ T : Set (Set X),
    (∀ t ∈ T, IsOpen t) ∧ T.Countable ∧ closure s = ⋂₀ T := by
  have : IsGδ (closure s) := PerfectlyNormalSpace.closed_gdelta isClosed_closure
  obtain ⟨a, b⟩ := this
  -- works but gross
  sorry

[Damiano Testa]

Do you like/is obtain ⟨a, b⟩ := PerfectlyNormalSpace.closed_gdelta (h := closure s) isClosed_closure what you want/good enough?

[Steven Clontz]

That works!

[Damiano Testa]

It is not always the case, but it is very unlikely that providing all non-typeclass arguments leaves Lean in a state where it is still not able to synthesize the appropriate instances. This means that very often, you can un-stuck typeclass synthesis by providing non-typeclass arguments.

[Damiano Testa]

(Besides, in situations such as the code above, calling out the implicit argument to be passed results in more readable code.)

[Steven Clontz]

I definitely agree about readability. I was trying variations on PerfectlyNormalSpace.closed_gdelta closure s isClosed_closure. I didn't expect that the literal h would be important.

[Damiano Testa]

The name of the variables became relevant in Lean 4 precisely due to this (awesome) feature of being able to "call out" implicit arguments. It is a little weird and probably means that there may be a little more thought involved in assigning names to hypotheses, but it is a really great feature, in terms of readability and maintainability of code.

[Patrick Massot]

Note the root cause of your trouble here is that docs#isClosed_closure does not have an explicit argument.

[Yaël Dillies]

(I think that's a good thing)

[Patrick Massot]

Unfortunately the golfing addiction pushes people to ignore the rational rules that tell when arguments can be implicit (see here for a recent example).

[Patrick Massot]

What is a good thing?

[Yaël Dillies]

Patrick Massot said:

What is a good thing?

That docs#isClosed_closure does not take an explicit argument since it is not a rewriting lemma and will mostly be used with dot notation where the extra explicit argument would be a bore most of the time.

[Patrick Massot]

Are you sure you are looking at the right lemma? Which dot notation are you talking about?

[Yaël Dillies]

I mean it will be used in dot notation from other lemmas, like docs#IsClosed.union

[Steven Clontz]

(deleted)

[Patrick Massot]

I see. So it is indeed all about golfing.

[Yaël Dillies]

I don't think using dot notation is specific to golfing?

[Yaël Dillies]

... nor is reducing bracket-induced annoyance

[Patrick Massot]

I’m specifically referring to brackets avoidance. Dot notation is often great for readability.