Zulip Chat Archive

Stream: new members

Topic: extract part of goal into separate variable


Eric Rodriguez (Apr 06 2022 at 01:02):

I can only find this being used in mathlib in docs#polynomial.gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, it definitely should be in the tips and tricks page

Adam Topaz (Apr 06 2022 at 01:05):

We use it quite frequently in LTE.

Matt Diamond (Apr 06 2022 at 02:27):

I'm running into one other roadblock with the above code... trying to prove this:

example :  (o : ordinal), beth o  aleph o := begin

end

and Lean isn't happy about universes:

type mismatch at application
  aleph o
term
  o
has type
  ordinal.{?l_1} : Type (?l_1+1)
but is expected to have type
  ordinal.{(max (?l_1+1) ?l_2)} : Type ((max (?l_1+1) ?l_2)+1)

I tried changing ordinal to ordinal.{max (u+1) v} but that just led to this new error:

type mismatch at application
  aleph o
term
  o
has type
  ordinal.{(max (u+1) v)} : Type ((max (u+1) v)+1)
but is expected to have type
  ordinal.{(max ((max (u+1) v)+1) ?l_1)} : Type ((max ((max (u+1) v)+1) ?l_1)+1)

Is there any way I can get past this? Do I need to modify my definition of beth to explicitly declare universe variables?

Notification Bot (Apr 06 2022 at 02:27):

Matt Diamond has marked this topic as unresolved.

Junyan Xu (Apr 06 2022 at 05:43):

I think you won't get the universe issue with the definition beth':

noncomputable
def beth' (o: ordinal) : cardinal :=
  ordinal.limit_rec_on o
  (cardinal.aleph 0)
  (λ _ b, 2 ^ b)
  (λ lim _ IH, Sup (lim.brange IH))

set_option pp.universes true
#check beth
#check beth'
beth.{u_1 u_2} : ordinal.{u_1}  cardinal.{(max (u_1+1) u_2)}
beth'.{u_1 u_2} : ordinal.{u_1}  cardinal.{u_2}

(Notice that you need bdd_above(using the disjoint union / Sigma type) for Sup to be well behaved: docs#le_cSup )

I think it's good in this case to specify explicit universes like

universe u
def beth' (o: ordinal.{u}) : cardinal.{u} :=

Junyan Xu (Apr 06 2022 at 05:53):

The universe issue with your approach is that the indexing type ι in

noncomputable def cardinal.sup {ι : Type u} (f : ι  cardinal.{max u v}) : cardinal :=

is { o // o < lim } : Type (u_1+1).


Last updated: Dec 20 2023 at 11:08 UTC