How to "deconstruct" ordinal comparison?

Stream: new members

[Bbbbbbbbba]

Basically, I want to prove
lemma oadd_lt_iff [ONote.NF (ONote.oadd e0 n0 a0)] [ONote.NF (ONote.oadd e1 n1 a1)] : e0.oadd n0 a0 < e1.oadd n1 a1 ↔ e0 < e1 ∨ e0 = e1 ∧ n0 < n1 ∨ e0 = e1 ∧ n0 = n1 ∧ a0 < a1 := sorry
so that when I encounter the condition o0 < o1 in the future, I can separately consider those three cases (in addition to the o0 = 0 case).

Is there an easy way to prove this, or a better way to do what I am trying to do?

[Yaël Dillies]

Can you provide a #mwe ?

[Bbbbbbbbba]

I cannot think of a simple realistic example right now, so I'll just show how I would prove the forward direction of this lemma with itself (obviously in real use cases exact Or.inl h etc. will be replaced by more complicated arguments)

import Mathlib

lemma oadd_lt_iff [ONote.NF (ONote.oadd e0 n0 a0)] [ONote.NF (ONote.oadd e1 n1 a1)] : e0.oadd n0 a0 < e1.oadd n1 a1 ↔ e0 < e1 ∨ e0 = e1 ∧ n0 < n1 ∨ e0 = e1 ∧ n0 = n1 ∧ a0 < a1 := sorry

lemma mwe [ONote.NF (ONote.oadd e0 n0 a0)] [ONote.NF (ONote.oadd e1 n1 a1)] : e0.oadd n0 a0 < e1.oadd n1 a1 → e0 < e1 ∨ e0 = e1 ∧ n0 < n1 ∨ e0 = e1 ∧ n0 = n1 ∧ a0 < a1 := by
  intro h
  rw [oadd_lt_iff] at h
  cases h with
  | inl h => exact Or.inl h
  | inr h => cases h with
    | inl h => exact Or.inr (Or.inl h)
    | inr h => exact Or.inr (Or.inr h)

[Yaël Dillies]

Please add the imports

[Bbbbbbbbba]

Like this?

[Yaël Dillies]

If it doesn't work for you, it doesn't work for me!

[Bbbbbbbbba]

What do you mean, is it that I have to capitalize the import Mathlib? (Edited in the snippet above)

[Bbbbbbbbba]

import mathlib seems to be working fine in VSCode, but not on the web playground, and I don't have an idea why

[Ira Fesefeldt]

Could it be because of the operating system? Windows file system is case-insensitive, Linux is case-sensitive

[Bbbbbbbbba]

Oh right it could be, I am on Windows

[Bbbbbbbbba]

Bbbbbbbbba said:

I cannot think of a simple realistic example right now, so I'll just show how I would prove the forward direction of this lemma with itself (obviously in real use cases exact Or.inl h etc. will be replaced by more complicated arguments)

import Mathlib

lemma oadd_lt_iff [ONote.NF (ONote.oadd e0 n0 a0)] [ONote.NF (ONote.oadd e1 n1 a1)] : e0.oadd n0 a0 < e1.oadd n1 a1 ↔ e0 < e1 ∨ e0 = e1 ∧ n0 < n1 ∨ e0 = e1 ∧ n0 = n1 ∧ a0 < a1 := sorry

lemma mwe [ONote.NF (ONote.oadd e0 n0 a0)] [ONote.NF (ONote.oadd e1 n1 a1)] : e0.oadd n0 a0 < e1.oadd n1 a1 → e0 < e1 ∨ e0 = e1 ∧ n0 < n1 ∨ e0 = e1 ∧ n0 = n1 ∧ a0 < a1 := by
  intro h
  rw [oadd_lt_iff] at h
  cases h with
  | inl h => exact Or.inl h
  | inr h => cases h with
    | inl h => exact Or.inr (Or.inl h)
    | inr h => exact Or.inr (Or.inr h)

But anyway now the mwe should be fixed, so does anyone know how to prove this lemma or do what I want to do in a better way?

[Ira Fesefeldt]

nvm

[Ira Fesefeldt]

I think the proof is rather cumbersome tho. I started it and required for the left-to-right-direction quite some cases or induction for every variable. The other direction can be proven easily with oadd_lt_oadd_1/2/3. But regarding the question of your title:
You can 'destruct' the ordinal comparison using ONote.lt_def and ONote.repr. This will transform it into its ordinal representative. Often this will give you contradictions in the inequality and finish your proof this way. I have not done the proof to its end though.

[Bbbbbbbbba]

Thanks for the advice, I'll try later

[Ira Fesefeldt]

i.e. like this:

import Mathlib

open ONote

lemma oadd_lt_iff [nf0 : (oadd e0 n0 a0).NF] [nf1 : (oadd e1 n1 a1).NF] :
    e0.oadd n0 a0 < e1.oadd n1 a1 ↔ e0 < e1 ∨ e0 = e1 ∧ n0 < n1 ∨ e0 = e1 ∧ n0 = n1 ∧ a0 < a1 := by
  apply Iff.intro
  · intro h
    simp only [lt_def, ONote.repr] at h
    sorry
  · rintro (h_e | ⟨h_e, h_n⟩ | ⟨h_e, h_n, h_a⟩)
    · exact ONote.oadd_lt_oadd_1 nf0 h_e
    · rw [← h_e]; exact ONote.oadd_lt_oadd_2 nf0 h_n
    · rw [← h_e, ← h_n]; exact ONote.oadd_lt_oadd_3 h_a

where the sorry part is what I believe is rather cumbersome.

[Bbbbbbbbba]

I have actually done this using just the trichotomy of ordinal comparison and the oadd_lt_oadd_* theorems. Thanks for showing me how to use rintro (whose documentation pointed me to rcases)! And please tell me if there are ways to improve the proof :stuck_out_tongue_wink:

import Mathlib

open ONote

lemma oadd_lt_iff [hnf0 : (oadd e0 n0 a0).NF] [hnf1 : (oadd e1 n1 a1).NF] :
    e0.oadd n0 a0 < e1.oadd n1 a1 ↔ e0 < e1 ∨ e0 = e1 ∧ n0 < n1 ∨ e0 = e1 ∧ n0 = n1 ∧ a0 < a1 := by
  apply Iff.intro
  · rw [← not_imp_not, not_or, not_or]
    intro ⟨he, hn, ha⟩
    rw [lt_def]
    rcases lt_trichotomy e0.repr e1.repr with he1 | he1 | he1
    . apply lt_def.mpr at he1
      contradiction
    . have _ := hnf0.fst
      have _ := hnf1.fst
      apply repr_inj.mp at he1
      rcases lt_trichotomy n0 n1 with hn1 | hn1 | hn1
      . have : e0 = e1 ∧ n0 < n1 := ⟨he1, hn1⟩
        contradiction
      . rcases lt_trichotomy a0.repr a1.repr with ha1 | ha1 | ha1
        . apply lt_def.mpr at ha1
          have : e0 = e1 ∧ n0 = n1 ∧ a0 < a1 := ⟨he1, hn1, ha1⟩
          contradiction
        . have _ := hnf0.snd
          have _ := hnf1.snd
          apply repr_inj.mp at ha1
          rw [he1, hn1, ha1]
          exact gt_irrefl (e1.oadd n1 a1).repr
        . apply not_lt_of_gt
          apply lt_def.mp
          rw [he1, hn1]
          exact oadd_lt_oadd_3 ha1
      . apply not_lt_of_gt
        apply lt_def.mp
        rw [he1]
        exact oadd_lt_oadd_2 hnf1 hn1
    . apply lt_def.mpr at he1
      apply not_lt_of_gt
      apply lt_def.mp
      exact oadd_lt_oadd_1 hnf1 he1
  · rintro (he | ⟨he, hn⟩ | ⟨he, hn, ha⟩)
    · exact oadd_lt_oadd_1 hnf0 he
    · rw [← he]; exact oadd_lt_oadd_2 hnf0 hn
    · rw [← he, ← hn]; exact oadd_lt_oadd_3 ha

[Bbbbbbbbba]

One thing I'm wondering in particular is if there is a more concise way to fill in the implicit inputs [a.NF] [b.NF] to repr_inj than have _ := hnf0.fst; have _ := hnf1.fst etc.