Lemmas for Levels.

Stream: Is there code for X?

[Robert Maxton]

It would be nice if I could provide a proper proof that e.g. isLevelDefEq (Level.max u v) (Level.max v u). (Specifically, I want to prove that if Level.dec u matches .some u', then Level.dec u |>.succ = u, so I can subst in that proof when working with Qq typed expressions). Unfortunately, I don't see any relevant existing lemmas, and all the relevant definitions are opaque and/or external so it's hard to prove them myself by induction on Level. Is there an existing workaround?

[Eric Rodriguez]

How would you expect the proof to be stated?

[Robert Maxton]

Well, that is sort of part of the question; I'm aware of the BEq instance for Levels and of QL= and of Level.geq and Level.normLt, but I wouldn't feel comfortable assertitng that that's all there is for Levels. Consider it a dependent goal :p
Marginally more seriously, I did in fact try and write a couple of proofs...

  lemma Level.max_symm (u v : Level) : Level.max u v = Level.max v u := by
    induction u with
    | zero =>
        induction v with
        | zero => rfl
        | succ v ih => -- ??

  -- If I had `Level.max_symm`, I could make a decent attempt at writing something like...
  lemma Level.succ_get_dec (u : Level) (h : u.dec.isSome = true): (u.dec.get h |>.succ) = u := by
    cases u with
    | zero => simp [Level.dec] at h
    | succ u => rfl
    | max u v =>
        wlog h' : Level.geq u v
        next =>
          specialize this v u h -- fails because `Level.max u v` is not obviously convertible to a `Level.max v u`

[Robert Maxton]

but I see no way of proving the subgoal that Level.max 0 (.succ v) = Level.succ (Level.max 0 v), either

[Robert Maxton]

(For whatever definition of = you care to use here; so far all the options I've seen either don't unfold or unfold to opaques.)

[Robert Maxton]

At best, maybe I could try and prove that the mapping from Nats is surjective, and then just work with Level.ofNat...?

[Robert Maxton]

But that feels like it'd pretty much run into the same problem of "everything to do with Levels is opaque meta code".

[Robert Maxton]

I don't even see a way of proving that a u : Level is valid iff there's a matching Sort u, so.

[Robert Maxton]

... Hm. Actually, now that I look at that code again, I can get a good bit closer by working with Level.geq; I can probably prove that, _if_ Level.geq defines by antisymmetry a valid equivalence relation, _then_ all the expected things about Levels are true up to that equivalence

[Robert Maxton]

But I still don't see a good way of turning that equivalence into something I can subst or rw or the like.

[Eric Wieser]

max_symm is false

[Eric Rodriguez]

Eric Wieser said:

max_symm is false

what?!

[Eric Wieser]

docs#Level.max is a constructor, isn't it? So it's axiomatically unique

[Damiano Testa]

Indeed:

import Lean
open Lean Level

example (u : Level) (h : max u (u.succ) = max (u.succ) u) : False := by
  cases h

[Damiano Testa]

Once you have this, proving Level.succ_get_dec will be a breeze.

[Eric Rodriguez]

but I mean within the context of actual universes, we do have that max u v = max v u? so what's going on here?

[Robert Maxton]

Something like, Sort is actually the quotient of Level by Level.geq a b && Level.geq b a? Except you can't actually write that in Lean because you'd be quantifying over Sorts and the resulting thing would live in Sort ω or something.

[Mario Carneiro]

for typechecking purposes, levels which are geq in both directions are equal, at least in theory. In practice level comparison is done by normalization, which is known to be incomplete in some cases

[Mario Carneiro]

It's not that weird that Level contains equivalent things in it that are not = (which is basically what we would call "syntactically equal"). Level has a defeq relation on it just like Expr, it's just significantly simpler. Obviously we don't expect Expr.const `foo [] = mkNumLit 1 to be true (assuming def foo := 1), but isDefEq (.const `foo []) (mkNumLit 1) is true

[Mario Carneiro]

The (assuming) part of the above sentence should give you a hint as to why we can't just make it true: the defeq relation depends on the environment, but = obviously cannot depend on anything but the structure of the Expr itself

[Notification Bot]

9 messages were moved here from #Is there code for X? > Lemmas for Levels by Ivan Gonzalez.

[Notification Bot]

10 messages were moved here from #Is there code for X? > Lemmas for Levels by Ivan Gonzalez.