Cannot derive unfold equation addpre._unary.eq_def

Stream: new members

[Op From The Start]

I have the following definition of addition on the games:

def addpre : PreNo → PreNo → PreNo := by
  intro x y
  cases x with
  | mk xL xR xLS xRS =>
    cases y with
    | mk yL yR yLS yRS =>
      apply PreNo.mk
      rotate_left 2
      exact Sum xL yL
      exact Sum xR yR
      intro xyl
      cases xyl with
      | inl xl => exact addpre (xLS xl) (PreNo.mk yL yR yLS yRS)
      | inr yl => exact addpre (PreNo.mk xL xR xLS xRS) (yLS yl)
      intro xyr
      cases xyr with
      | inl xr => exact addpre (xRS xr) (PreNo.mk yL yR yLS yRS)
      | inr yr => exact addpre (PreNo.mk xL xR xLS xRS) (yRS yr)
termination_by x y => Ordinal.nadd (birthday x) (birthday y)
decreasing_by
. simp
  apply birthday_left_child_lt
. simp
  apply birthday_left_child_lt
. simp
  apply birthday_right_child_lt
. simp
  apply birthday_right_child_lt

But I am getting a strange error on the first line:

Cannot derive unfold equation addpre._unary.eq_def
  failed to finish proof for equational theorem for 'addpre._unary'
    Tactic `rfl` failed: equality lhs
      PSigma.rec
        (fun fst snd =>
          PreNo.rec (motive := fun t => fst = t → PreNo)
            (fun L R a a_1 a_ih a_ih h =>
              PreNo.rec (motive := fun t =>
                ((y : (_ : PreNo) ×' PreNo) →
                    (invImage (fun x => PSigma.casesOn x fun a a_2 => (birthday a).nadd (birthday a_2))
                            Ordinal.wellFoundedRelation).1
                        y ⟨PreNo.mk L R a a_1, t⟩ →
                      PreNo) →
                  snd = t → PreNo)
                (fun L_1 R_1 a_2 a_3 a_ih a_ih x h =>
                  PreNo.mk (L ⊕ L_1) (R ⊕ R_1)
                    (fun xyl =>
                      Sum.rec (motive := fun t => xyl = t → PreNo) (fun val h => x ⟨a val, PreNo.mk L_1 R_1 a_2 a_3⟩ ⋯)
                        (fun val h => x ⟨PreNo.mk L R a a_1, a_2 val⟩ ⋯) xyl ⋯)
                    fun xyr =>
                    Sum.rec (motive := fun t => xyr = t → PreNo) (fun val h => x ⟨a_1 val, PreNo.mk L_1 R_1 a_2 a_3⟩ ⋯)
                      (fun val h => x ⟨PreNo.mk L R a a_1, a_3 val⟩ ⋯) xyr ⋯)
                snd (fun y h => addpre._unary y) ⋯)
            fst ⋯)
        _x
    is not definitionally equal to rhs
      PSigma.rec
        (fun fst snd =>
          PreNo.rec (motive := fun t => fst = t → PreNo)
            (fun L R a a_1 a_ih a_ih h =>
              PreNo.rec (motive := fun t => snd = t → PreNo)
                (fun L_1 R_1 a_2 a_3 a_ih a_ih h =>
                  PreNo.mk (L ⊕ L_1) (R ⊕ R_1)
                    (fun xyl =>
                      Sum.rec (motive := fun t => xyl = t → PreNo)
                        (fun val h => addpre._unary ⟨a val, PreNo.mk L_1 R_1 a_2 a_3⟩)
                        (fun val h => addpre._unary ⟨PreNo.mk L R a a_1, a_2 val⟩) xyl ⋯)
                    fun xyr =>
                    Sum.rec (motive := fun t => xyr = t → PreNo)
                      (fun val h => addpre._unary ⟨a_1 val, PreNo.mk L_1 R_1 a_2 a_3⟩)
                      (fun val h => addpre._unary ⟨PreNo.mk L R a a_1, a_3 val⟩) xyr ⋯)
                snd ⋯)
            fst ⋯)
        _x


_x : (_ : PreNo) ×' PreNo
⊢ PSigma.rec
    (fun fst snd =>
      PreNo.rec (motive := fun t => fst = t → PreNo)
        (fun L R a a_1 a_ih a_ih h =>
          PreNo.rec (motive := fun t =>
            ((y : (_ : PreNo) ×' PreNo) →
                (invImage (fun x => PSigma.casesOn x fun a a_2 => (birthday a).nadd (birthday a_2))
                        Ordinal.wellFoundedRelation).1
                    y ⟨PreNo.mk L R a a_1, t⟩ →
                  PreNo) →
              snd = t → PreNo)
            (fun L_1 R_1 a_2 a_3 a_ih a_ih x h =>
              PreNo.mk (L ⊕ L_1) (R ⊕ R_1)
                (fun xyl =>
                  Sum.rec (motive := fun t => xyl = t → PreNo) (fun val h => x ⟨a val, PreNo.mk L_1 R_1 a_2 a_3⟩ ⋯)
                    (fun val h => x ⟨PreNo.mk L R a a_1, a_2 val⟩ ⋯) xyl ⋯)
                fun xyr =>
                Sum.rec (motive := fun t => xyr = t → PreNo) (fun val h => x ⟨a_1 val, PreNo.mk L_1 R_1 a_2 a_3⟩ ⋯)
                  (fun val h => x ⟨PreNo.mk L R a a_1, a_3 val⟩ ⋯) xyr ⋯)
            snd (fun y h => addpre._unary y) ⋯)
        fst ⋯)
    _x =
  PSigma.rec
    (fun fst snd =>
      PreNo.rec (motive := fun t => fst = t → PreNo)
        (fun L R a a_1 a_ih a_ih h =>
          PreNo.rec (motive := fun t => snd = t → PreNo)
            (fun L_1 R_1 a_2 a_3 a_ih a_ih h =>
              PreNo.mk (L ⊕ L_1) (R ⊕ R_1)
                (fun xyl =>
                  Sum.rec (motive := fun t => xyl = t → PreNo)
                    (fun val h => addpre._unary ⟨a val, PreNo.mk L_1 R_1 a_2 a_3⟩)
                    (fun val h => addpre._unary ⟨PreNo.mk L R a a_1, a_2 val⟩) xyl ⋯)
                fun xyr =>
                Sum.rec (motive := fun t => xyr = t → PreNo)
                  (fun val h => addpre._unary ⟨a_1 val, PreNo.mk L_1 R_1 a_2 a_3⟩)
                  (fun val h => addpre._unary ⟨PreNo.mk L R a a_1, a_3 val⟩) xyr ⋯)
            snd ⋯)
        fst ⋯)
    _x

I don't know what addpre._unary.eq_def or addpre._unary actually are or what they should be. How can I fix this?

[Aaron Liu]

Those are auxiliary definitions created when you perform mutual recursion I think

[Aaron Liu]

can you provide a #mwe

[Op From The Start]

I will try, theres about 300 lines of code before the add function so it might take a bit of testing.

[Aaron Liu]

oh no the mutual recursion auxiliary definitions are have the word mutual in them, I think this is actually the well-founded recursion auxiliary definition for well-founded recursion

[Op From The Start]

Here is a minimal example. It isnt proven but it still gives the error:

import Mathlib.SetTheory.Ordinal.Family
import Mathlib.SetTheory.Ordinal.NaturalOps

inductive NewOrd
| oversup : (T: Type) → (T → NewOrd) → NewOrd

noncomputable
def new_to_old : NewOrd → Ordinal.{0} := by
  intro n
  cases h:n
  rename_i I n_i
  exact iSup (λi:I => new_to_old (n_i i) + 1)

def ordnadd : NewOrd → NewOrd → NewOrd := by
  intro x y
  cases hx:x with
  | oversup xI x_i =>
    cases hy:y with
    | oversup yI y_i =>
      apply NewOrd.oversup
      rotate_left 1
      exact Sum xI yI
      intro xyi
      cases xyi with
      | inl xi => exact ordnadd (x_i xi) (NewOrd.oversup yI y_i)
      | inr yi => exact ordnadd (NewOrd.oversup xI x_i) (y_i yi)
termination_by x y => Ordinal.nadd (new_to_old x) (new_to_old y)
decreasing_by
  sorry
  sorry

gives:

Cannot derive unfold equation ordnadd._unary.eq_def
  failed to finish proof for equational theorem for 'ordnadd._unary'
    Tactic `rfl` failed: equality lhs
      PSigma.rec
        (fun fst snd =>
          NewOrd.rec (motive := fun t => fst = t → NewOrd)
            (fun T a a_ih h =>
              (⋯ ▸ fun hx =>
                  NewOrd.rec (motive := fun t =>
                    ((y : (_ : NewOrd) ×' NewOrd) →
                        (invImage (fun x => PSigma.casesOn x fun a a_1 => (new_to_old a).nadd (new_to_old a_1))
                                Ordinal.wellFoundedRelation).1
                            y ⟨NewOrd.oversup T a, t⟩ →
                          NewOrd) →
                      snd = t → NewOrd)
                    (fun T_1 a_1 a_ih x h =>
                      (⋯ ▸ fun hy =>
                          NewOrd.oversup (T ⊕ T_1) fun xyi =>
                            Sum.rec (motive := fun t => xyi = t → NewOrd)
                              (fun val h => x ⟨a val, NewOrd.oversup T_1 a_1⟩ ⋯)
                              (fun val h => x ⟨NewOrd.oversup T a, a_1 val⟩ ⋯) xyi ⋯)
                        ⋯)
                    snd (fun y h => ordnadd._unary y) ⋯)
                ⋯)
            fst ⋯)
        _x
    is not definitionally equal to rhs
      PSigma.rec
        (fun fst snd =>
          NewOrd.rec (motive := fun t => fst = t → NewOrd)
            (fun T a a_ih h =>
              (⋯ ▸ fun hx =>
                  NewOrd.rec (motive := fun t => snd = t → NewOrd)
                    (fun T_1 a_1 a_ih h =>
                      (⋯ ▸ fun hy =>
                          NewOrd.oversup (T ⊕ T_1) fun xyi =>
                            Sum.rec (motive := fun t => xyi = t → NewOrd)
                              (fun val h => ordnadd._unary ⟨a val, NewOrd.oversup T_1 a_1⟩)
                              (fun val h => ordnadd._unary ⟨NewOrd.oversup T a, a_1 val⟩) xyi ⋯)
                        ⋯)
                    snd ⋯)
                ⋯)
            fst ⋯)
        _x


_x : (_ : NewOrd) ×' NewOrd
⊢ PSigma.rec
    (fun fst snd =>
      NewOrd.rec (motive := fun t => fst = t → NewOrd)
        (fun T a a_ih h =>
          (⋯ ▸ fun hx =>
              NewOrd.rec (motive := fun t =>
                ((y : (_ : NewOrd) ×' NewOrd) →
                    (invImage (fun x => PSigma.casesOn x fun a a_1 => (new_to_old a).nadd (new_to_old a_1))
                            Ordinal.wellFoundedRelation).1
                        y ⟨NewOrd.oversup T a, t⟩ →
                      NewOrd) →
                  snd = t → NewOrd)
                (fun T_1 a_1 a_ih x h =>
                  (⋯ ▸ fun hy =>
                      NewOrd.oversup (T ⊕ T_1) fun xyi =>
                        Sum.rec (motive := fun t => xyi = t → NewOrd) (fun val h => x ⟨a val, NewOrd.oversup T_1 a_1⟩ ⋯)
                          (fun val h => x ⟨NewOrd.oversup T a, a_1 val⟩ ⋯) xyi ⋯)
                    ⋯)
                snd (fun y h => ordnadd._unary y) ⋯)
            ⋯)
        fst ⋯)
    _x =
  PSigma.rec
    (fun fst snd =>
      NewOrd.rec (motive := fun t => fst = t → NewOrd)
        (fun T a a_ih h =>
          (⋯ ▸ fun hx =>
              NewOrd.rec (motive := fun t => snd = t → NewOrd)
                (fun T_1 a_1 a_ih h =>
                  (⋯ ▸ fun hy =>
                      NewOrd.oversup (T ⊕ T_1) fun xyi =>
                        Sum.rec (motive := fun t => xyi = t → NewOrd)
                          (fun val h => ordnadd._unary ⟨a val, NewOrd.oversup T_1 a_1⟩)
                          (fun val h => ordnadd._unary ⟨NewOrd.oversup T a, a_1 val⟩) xyi ⋯)
                    ⋯)
                snd ⋯)
            ⋯)
        fst ⋯)
    _x

[Op From The Start]

I think the binary nature is required as I have a similar unary function that does not give that error.

[Aaron Liu]

maybe don't define your function using tactics

[Op From The Start]

Huh, this:

def ordnadd2 : NewOrd → NewOrd → NewOrd :=
  λ x y =>
  match hx:x with
  | NewOrd.oversup xI x_i =>
    match hy:y with
    | NewOrd.oversup yI y_i =>
      NewOrd.oversup (Sum xI yI) (λ xyi => match xyi with
      | Sum.inl xi => ordnadd2 (x_i xi) (NewOrd.oversup yI y_i)
      | Sum.inr yi => ordnadd2 (NewOrd.oversup xI x_i) (y_i yi) )
termination_by x y => Ordinal.nadd (new_to_old x) (new_to_old y)
decreasing_by
  sorry
  sorry

so i guess tactics get in the way of something