6:14 PM Placeholder context error in class extends

Stream: new members

[Raphael Appenzeller]

I am trying to implement $\Lambda$-metric spaces which are like metric spaces but $\mathbb{R}$ replaced by an ordered abelian group $\Lambda$. I am running into the following error:

don't know how to synthesize placeholder
context:
α : Type u
⊢ Type uLean

here is a minimal working example:

import algebra.order.group
universe u
namespace algebra.order.group
variables {Λ : Type u} [linear_ordered_add_comm_group Λ]
class has_lambda_dist (α : Type u) :=
(dist : α → α → Λ)
class lambda_metric_space (α : Type u)
  extends has_lambda_dist α :=
(sym : ∀ p q : X, dist p q = dist p q)

Does anyone know what goes wrong?

[Kevin Buzzard]

Lean can't guess Lambda from the information you gave it so it's asking you to supply it

[Raphael Appenzeller]

Aha. And having defined $\Lambda$ as a variable does not allow me to use it in all definitions afterwards? Do I have to give $\Lambda$ as an input to has_lambda_dist and lambda_metric_space?

[Patrick Johnson]

Why not make Λ explicit? This typechecks:

import algebra.order.group
universe u
variables (Λ : Type u) [linear_ordered_add_comm_group Λ]

class has_lambda_dist (α : Type u) :=
(dist : α → α → Λ)

class lambda_metric_space (α : Type u) extends has_lambda_dist Λ α :=
(sym : ∀ (p q : α), dist p q = dist q p)

[Kevin Buzzard]

import algebra.order.group
universe u
namespace algebra.order.group

class has_lambda_dist (α : Type u) (Λ : Type u) [linear_ordered_add_comm_group Λ] :=
(dist : α → α → Λ)

variables (Λ : Type u) [linear_ordered_add_comm_group Λ]

class lambda_metric_space (α : Type u)
  extends has_lambda_dist α Λ :=
(sym : ∀ p q : α, dist p q = dist p q)

end algebra.order.group

might be a way to do it. variable {Lambda...} doesn't mean "Let Lambda be a fixed ordered group", it means "do nothing, but whenever you see a Lambda later on, add {Lambda : Type u} and all the extra stuff which comes with it to the beginning of the theorem or definition"

[Raphael Appenzeller]

Aha. My problem was that I took curly brackets {} when I wanted round ones ( ) . But it might also be better to make the definitions depend on $\Lambda$ explicitly.

Thanks!

[Raphael Appenzeller]

I am running into more problems. I try to define an isometry, but Lean forgot what dist means. Specifying Y.dist and X.dist does not help. Any cues for how to fix it?

import algebra.order.group
universe u
variables (Λ : Type u) [linear_ordered_add_comm_group Λ]

class has_lambda_dist (α : Type u) :=
(dist : α → α → Λ)

class lambda_metric_space (α : Type u) extends has_lambda_dist Λ α :=
(sym : ∀ (p q : α), dist p q = dist q p)
-- more axioms omitted

class lambda_isometry (X Y: Type u) [lambda_metric_space Λ X] [lambda_metric_space Λ Y]  :=
(to_fun : X → Y)
(isom : ∀ x1 x2 : X , dist (to_fun x1) (to_fun x2) = dist x1 x2)

[Alex J. Best]

Does adding open lambda_metric_space before the last class work?

[Raphael Appenzeller]

Thank you for the suggestion. It unfortunately does not work. The error I am getting is:

unknown identifier 'dist'

and here is the Lean state:

don't know how to synthesize placeholder
context:
Λ : Type u,
_inst_1 : linear_ordered_add_comm_group Λ,
Λ : Type u,
_inst_1 : linear_ordered_add_comm_group Λ,
X Y : Type u,
_inst_2 : lambda_metric_space Λ X,
_inst_3 : lambda_metric_space Λ Y,
to_fun : X → Y,
x1 x2 : X
⊢ Sort ?

[Yaël Dillies]

X.dist can't work, right? It is being resolved to Type.dist X because X : Type*.

[Raphael Appenzeller]

Yes. I somehow need Lean to see X as a lambda_metric_space instead of as a Type u.
I would need to be able to access _inst_2 in the class statement. Is there a way to do this?

[Yaël Dillies]

The problem is that dist x y could be of type Λ₁ or Λ₂ if lambda_metric_space Λ₁ X and lambda_metric_space Λ₂ X, so Lean can't decide which one you mean. Instead, you should define

def dist (Λ : Type*) [linear_ordered_add_comm_group Λ] [lambda_metric_space Λ X} :
  X → X → Λ :=
lambda_metric_space.dist

[Raphael Appenzeller]

Thanks. But when I write your definition I get the same error:

unknown identifier 'lambda_metric_space.dist'

Now the problem is that lambda_metric_space is not a constant.

[Yaël Dillies]

Add set_option old_structure_cmd true at the top of the file.

[Raphael Appenzeller]

Thanks. Together with open lambda_metric_space, this fixes the problem with dist. (What does that set_option-incantation do? How could I have found out about it?) However now there is a problem with the equality.

don't know how to synthesize placeholder
context:
Λ : Type u,
_inst_1 : linear_ordered_add_comm_group Λ,
Λ : Type u,
_inst_1 : linear_ordered_add_comm_group Λ,
X Y : Type u,
_inst_2 : lambda_metric_space Λ X,
_inst_3 : lambda_metric_space Λ Y,
to_fun : X → Y,
x1 x2 : X
⊢ Type u

For reference, here is a mwe.

[Yaël Dillies]

It is because, with new structures, extends has_lambda_dist Λ α means "create a field to_has_lambda_dist", not "copy over the fields from has_lambda_dist".

[Yaël Dillies]

So what you think is lambda_metric_space.dist is actually has_lambda_dist.dist ∘ lambda_metric_space.to_has_lambda_dist.