svarc-milnor

Stream: new members

[Georgi Kocharyan]

Hiya,
I'm doing a summer project on Lean and am working on formalising the Svarc-Milnor lemma - I've finished proving the first part about \a being generated by a specific subset S, and now I want to state the second part of the theorem (that states \a quasi-isometric to the metric space \b it acts on) and am getting a weird error message:

theorem metric_svarcmilnor2 {α : Type*} {β : Type*} [inhabited β] [group α] [inhabited α] (c : ℝ) (b : ℝ) (cpos: c > 0) (bpos: b > 0)  [quasigeodesic_space β c b cpos (le_of_lt bpos)]
  [isom_action α β] (s : set β) (htrans: translates_cover α s) (finitediam : metric.bounded s) (x : β)
   : @is_QI α β (@word_metric α _ (@proper_action_set α β _ _ _ (set_closed_ball s (2*b))) (metric_svarcmilnor1 c b cpos bpos s htrans finitediam)) _ (λ g : α, g • x) :=
   sorry

The error states:

type mismatch at application
word_metric
term
α
has type
Type u_1 : Type (u_1+1)
but is expected to have type
Type : Type 1

I realise this might not be enough information to know what the problem is, I just figured this might be a common error. It uses my definition of the word metric on groups which takes Type* as an argument - let me know if you'd like to see it.
Thanks in advance :)

[Yaël Dillies]

Hey Georgi! The problem is that your definition of word_metric is not universe-polymorphic. That is, it only applies to types in Type (= Type 0), and not all Type u. You can probably just replace Type by Type* and it should work.

[Yaël Dillies]

Note that Type* in lemma statements means "Lean, please make it Type u for whatever u makes sense". So if word_metric uses something that is already not universe-polymorphic, then Lean will think "Oh, u must be 0" and word_metric won't be universe-polymorphic either.

[Yaël Dillies]

Type* in variables declarations means "Lean, this is Type u for some fixed u I am not bothering to declare. Deal with it".

[Georgi Kocharyan]

Yaël Dillies said:

Hey Georgi! The problem is that your definition of word_metric is not universe-polymorphic. That is, it only applies to types in Type (= Type 0), and not all Type u. You can probably just replace Type by Type* and it should work.

amazing!! I forgot to add the *, because I didn't know what it did, but now I do :) Thank you!

[Jim Fowler]

This is great! Is quasigeodesic_space in mathlib? Is isom_action in mathlib...?

[Georgi Kocharyan]

Jim Fowler said:

This is great! Is quasigeodesic_space in mathlib? Is isom_action in mathlib...?

No, this is all stuff I've defined. Check the repo if you want to see the definitions!
https://github.com/GregorSamsa42/svarc-milnor