Status of !4#2470 (SetTheory.Ordinal.Notation)

Stream: mathlib4

[Arien Malec]

I've been semi-adopting this file and fixing things on and off, but it's pretty heinous. In particular, the original Lean 3 (ab)uses _match_1 to prove certain invariants that are essential for proofs, and there's a thing that happens here where two match patterns generate three terms in a way that I don't understand (and neither does Lean 4).

theorem repr_inj {a b} [NF a] [NF b] : repr a = repr b ↔ a = b :=
⟨match cmp a b, cmp_compares a b with
 | ordering.lt, (h : repr a < repr b), e := (ne_of_lt h e).elim
 | ordering.gt, (h : repr a > repr b), e := (ne_of_gt h e).elim
 | ordering.eq, h, e := h
 end, congr_arg _⟩

(cmp returns an ordering and cmp_compares returns (cmp a b).compares a b, and there's some magic that's happening there).

I wonder if the right thing here is for someone to refactor on the Lean 3 side then re-start the port. I've been inserting defs that recapitulate the _match_1 on the Lean 3 side (and yes, there's a match construct on Lean 4 but it returns different signatures), and generally cleaning stuff up, but someone's going to have a long review cycle....

[Eric Wieser]

_match_1 can probably be replaced with let rec?

[Eric Wieser]

Can you link to the offending use of _match_1 in mathlib3?

[Arien Malec]

Sure: docs#onote.opow_def docs#onote.oadd_add docs#onote.repr_sub, docs#onote.fast_growing_def

[Eric Wieser]

docs#opow_def is just the equation lemma for docs#opow

[Arien Malec]

Sort of.

[Arien Malec]

opow._match_1 is onote → onote × ℕ → onote and opow is onote → onote → onote, so it's a single step into opow

[Arien Malec]

I find this very confusing:

/-- The ordinal denoted by a notation -/
@[simp]
noncomputable def repr : Onote → Ordinal.{0}
  | 0 => 0
  | oadd e n a => ω ^ repr e * n + repr a
#align onote.repr Onote.repr

variable (e: Onote)
#check (repr e * (5: PNat)) -- OK: repr e * ↑↑5 : Ordinal
theorem oadd_repr: oadd e n a = ω ^ repr e * n + repr a := rfl -- fails
-- failed to synthesize instance
--  HMul Ordinal ℕ+ ?m.12533

This seemingly trivial proof is key to some shennanigans I'd like to try to unlock repr_inj.

[Eric Wieser]

Did you mean to write (oadd e n a).repr and not oadd e n a ?

[Arien Malec]

I just realized that...

[Arien Malec]

Sigh, now I'm in coercion hell.

theorem zere_ne_oadd_repr: (0: Ordinal) ≠  ω ^ repr e * (n: ℕ+) + repr a := by
  have h: ω ^ repr e ≠ 0 := opow_ne_zero _ omega_ne_zero
  have h₂:  ω ^ repr e * (n : ℕ+) ≠ 0 := Ordinal.mul_ne_zero h (PNat.ne_zero n)

gives

argument
  PNat.ne_zero n
has type
  ↑n ≠ 0 : Prop
but is expected to have type
  ↑↑n ≠ 0 : Prop

The plan here is that by cases, I can get repr_inj to a state where if I can prove the above, and can prove

@[simp]
theorem notation_ext_iff:
    ω ^ repr e * n + repr a = ω ^ repr e' * n' + repr a' ↔ e = e' ∧ n = n' ∧ a = a' := sorry

then I'm done

[Eric Wieser]

How does it work in mathlib3?

[Arien Malec]

See above -- first post -- some weird thing where two matches generate three hypotheses.

(Sadly, my ext_iff relies on repr_inj so that's another corner).

[Reid Barton]

I don't understand why that syntax worked but it must have meant something like

fun e => match _, _ with
| _, _ => ...[e]
...

[Reid Barton]

In any case repr_inj should follow easily from cmp_compares

[Reid Barton]

Reid Barton said:

I don't understand why that syntax worked but it must have meant something like

fun e => match _, _ with
| _, _ => ...[e]
...

Because this match expression is appearing where we want a term of type
repr a = repr b -> a = b
and in the branch | ordering.lt, (h : repr a < repr b), e := (ne_of_lt h e).elim we see ne_of_lt h e with h : repr a < repr b, so e : repr a = repr b and there is a call to false.elim

[Arien Malec]

What's so very confusing here, is that we have h,e where h: repr a < repr b and e is a = b

[Reid Barton]

e should be of type repr a = repr b

[Arien Malec]

ne_of_lt

[Reid Barton]

Right, it is being passed h : repr a < repr b, so then the result is not (repr a = repr b), so if we pass e : repr a = repr b now, we get false

[Reid Barton]

This also makes sense, since we are proving the forwards direction so repr a = repr b is what we know.

[Arien Malec]

Sorry, e: repr a = repr b

[Reid Barton]

To be more precise what I mean is that you can rewrite the Lean 3 code equivalently by

• inserting \lam e, between the \< and match
• removing , e from the LHS of each branch

[Reid Barton]

I think whoever wrote this code the first time knows too much about how Lean works.

[Arien Malec]

Look at the copyright statement :rolling_on_the_floor_laughing:

[Reid Barton]

Yes, I was pretty sure I knew who it was without looking!

[Reid Barton]

Now I wonder if you could use match with with no expressions, but with multiple branches, as a lambda-case

[Kevin Buzzard]

Uber-compact/golfed code has turned out to be tricky to port on more than one occasion. For me this was an unexpected bad consequence of the mathlib3 golf-for-your-life policy.

[Eric Wieser]

On the flipside, I think long messy nonterminal-simp proofs would have been worse to port

[Arien Malec]

This is driving me crazy -- has to be an easy fix with a missing coercion somewhere.

import Mathlib.SetTheory.Ordinal.Principal

theorem mul_one' {o: Ordinal}: o * 1 = o := by
  rw [mul_one] -- good

theorem mul_one'' {o: Ordinal}: o * (1: ℕ+) = o := by
  rw [mul_one] -- fails

[Eric Wieser]

I would not expect the second one to work, look at the goal state

[Arien Malec]

Ah....

import Mathlib.SetTheory.Ordinal.Principal

theorem mul_one' {o: Ordinal}: o * 1 = o := by
  rw [mul_one] -- works

theorem mul_one'' {o: Ordinal}: o * (1 : Nat) = o := by
  rw [mul_one] -- doens't

theorem mul_one'''' {o: Ordinal}: o * (1: ℕ+) = o := by
  rw [mul_one] -- doesn't

[Arien Malec]

So in the first case, we use the One machinery, in the other two we use coercion machinery to cast a P/Nat as an Ordinal.

[Arien Malec]

Which, if the cast is to mean anything should be equal to Ordinal.one

[Arien Malec]

So, updating:

import Mathlib.SetTheory.Ordinal.Principal

theorem mul_one' {o: Ordinal}: o * 1 = o := by
  rw [mul_one]

theorem mul_one'' {o: Ordinal}: o * (1 : Nat) = o := by
  simp [mul_one] -- closes goal, below fails due to no goals to be solved
  have h: ↑(1: ℕ) = (1: Ordinal) := Nat.cast_one
  rw [h, mul_one]

theorem mul_one'''' {o: Ordinal}: o * (1: ℕ+) = o := by
  simp [mul_one] -- DOES NOT CLOSE GOAL but below closes goal
  have h: (↑↑(1: ℕ+) : Ordinal) = ↑(1:ℕ) := rfl
  have h₂: ↑(1: ℕ) = (1: Ordinal) := Nat.cast_one
  rw [h, h₂, mul_one]

It seems like there's a simp lemma missing somewhere.

[Eric Wieser]

!4#2989 perhaps?

[Arien Malec]

I don't think that has the right signature, but maybe?

[Arien Malec]

One would like to express "if there's a coercion between ℕ and some time there's also a coercion between ℕ+ and that type"

[Eric Wieser]

Do the proofs above work in Lean 3?

[Arien Malec]

Lean 3 simps just fine

[Eric Wieser]

Then use simp? in Lean 3 vs Lean 4 and see what's different

[Arien Malec]

Ah, the missing bit is docs#coe_coe

[Arien Malec]

Not ported, and no align statement AFAICT?

[Eric Wieser]

coe_coe was a magic lemma in Lean3 which can't really exist in Lean4

[Eric Wieser]

At least, as I understand it; I think it exploited the fact that implicit typeclass arguments are found by unification, so it would apply to things that aren't actually the transitive coercion instance as long as they're defeq to it. There is no coe symbol to match on in Lean 4, so the lemma wouldn't work

[Eric Wieser]

If you add the coe_coe statement locally for the types you need, does it help?

[Arien Malec]

Let me try -- I see a bunch of local coe_coe lemmas that I can try from & obviously I have a hacky solution above that will work.

[Arien Malec]

I did confirm that

@[simp]
theorem PNat_Nat_coe: (↑↑(n: ℕ+) : Ordinal) = ↑(n: ℕ) := rfl

does not work where the local hypothesis does?

[Eric Wieser]

↑↑ is nonsense there

[Eric Wieser]

Lean has no way of knowing which coercion you meant

[Arien Malec]

Ah, because my local type is actually @Nat.cast Ordinal AddMonoidWithOne.toNatCast ↑1 : Ordinal

[Eric Wieser]

What statement are you trying to write? And what is n?

[Arien Malec]

Goal state is ω ^ repr x * ↑↑1 * repr o = ω ^ repr x * repr o

[Arien Malec]

and I want to close the goal with mul_one

[Eric Wieser]

Can you turn off coercion printing?

[Eric Wieser]

Eric Wieser said:

!4#2989 perhaps?

I'm pretty sure this PR will solve your problem

[Arien Malec]

ω ^ repr x * Nat.cast (PNat.val (OfNat.ofNat 1)) * repr o = ω ^ repr x * repr o

[Eric Wieser]

That's docs4#PNat.one_coe I think

[Eric Wieser]

Which like I said, is fixed in !4#2989

[Eric Wieser]

Eric Wieser said:

That's docs4#PNat.one_coe I think

@Henrik Böving, how hard would it be to make ↑ link to PNat.val in that lemma?

[Arien Malec]

OK, merged and building now...

[Henrik Böving]

Eric Wieser said:

Eric Wieser said:

That's docs4#PNat.one_coe I think

Henrik Böving, how hard would it be to make ↑ link to PNat.val in that lemma?

Hmmm, as I understand it the arrow is a Coe.coe call which has an implicit argument with theCoe instnace? And somewhere burried in that should be the call to PNat.val. So certainly not trivial :(

[Eric Wieser]

My understanding was that Coes got inlined, so the arrow is actually a direct call of PNat.val

[Henrik Böving]

Ah indeed it does desugar into PNat.val here I didn't know that cool...and I can directly go to definition on it as well so the InfoTree does seem to have the information even. In that case it should certainly be doable.

In fact I am rather surprise it doesnt just work :tm: out of the box :thinking: