Structural recursion unfold theorems

Stream: lean4

[Sky Wilshaw]

I'm trying to generate an equational lemma for a function defined by structural recursion, but I can't work out how to prove the required equalities. #mwe:

inductive Foo
| zero : Foo
| succ : Foo → Foo

def replace (f : Foo → Option Foo) (t : Foo) : Foo :=
  match f t with
  | some u => u
  | none =>
      match t with
      | .zero => .zero
      | .succ t => .succ (replace f t)

#print replace
/-
def replace : (Foo → Option Foo) → Foo → Foo :=
fun f t =>
  Foo.brecOn t fun t f_1 =>
    match f t with
    | some u => u
    | none =>
      (match (motive := (t : Foo) → Foo.below t → Foo) t with
        | Foo.zero => fun x => Foo.zero
        | Foo.succ t => fun x => Foo.succ x.fst.fst)
        f_1

-/

theorem replace_eq (f : Foo → Option Foo) (t : Foo) :
    replace f t = (match f t with
      | some u => u
      | none =>
          match t with
          | .zero => .zero
          | .succ t => .succ (replace f t)) := by
  unfold replace -- failed to generate unfold theorem for 'replace'

[Sky Wilshaw]

Even copy-pasting the #print-ed definition doesn't check as defeq to replace f t:

theorem replace_eq (f : Foo → Option Foo) (t : Foo) :
    replace f t = (Foo.brecOn t fun t f_1 =>
    match f t with
    | some u => u
    | none =>
      (match (motive := (t : Foo) → Foo.below t → Foo) t with
        | Foo.zero => fun x => Foo.zero
        | Foo.succ t => fun x => Foo.succ x.fst.fst)
        f_1) := by
  rfl
/- tactic 'rfl' failed, equality lhs
  replace f t
is not definitionally equal to rhs
  Foo.brecOn t fun t f_1 =>
    match f t with
    | some u => u
    | none =>
      (match (motive := (t : Foo) → Foo.below t → Foo) t with
        | Foo.zero => fun x => Foo.zero
        | Foo.succ t => fun x => Foo.succ x.fst.fst)
        f_1
-/

[James Gallicchio]

this seems like a bug in the equation generator?

[Kyle Miller]

I'm not sure exactly what unfold theorems are and how the relate to equation theorems, but simp can handle this.

theorem replace_eq (f : Foo → Option Foo) (t : Foo) :
    replace f t = (match f t with
      | some u => u
      | none =>
          match t with
          | .zero => .zero
          | .succ t => .succ (replace f t)) := by
  cases t <;> simp [replace]

This cases t is important because the definition of replace proceeds by cases on t, so it's not unreasonable for it to decide to generate equation lemmas specialized for the different cases.

[Kyle Miller]

("failed to generate unfold theorem for 'replace'" does seem like a potential bug)

[Sky Wilshaw]

That fix also works in my real case, thanks!

[Sky Wilshaw]

I'd assumed that the equational lemmas would only be specialised to cases when the entire function was defined by pattern-matching - in this case, the match expression is internal so I assumed it wouldn't.

[James Gallicchio]

Even when it's defined by pattern matching you can unfold the definition to a match. See:

inductive Foo
| zero : Foo
| succ : Foo → Foo

def nonrecCasing (f : Foo → Option Foo) (t : Foo) : Foo :=
  match f t with
  | some u => u
  | none =>
    match t with
    | .zero => .zero
    | .succ t' => t'

example : nonrecCasing f t = .zero := by
  unfold nonrecCasing
  sorry

def recursive (t : Foo) : Foo :=
  match t with
  | .zero => .zero
  | .succ t => .succ (recursive t)

example : recursive t = .zero := by
  unfold recursive
  sorry

def recCasing (f : Foo → Option Foo) (t : Foo) : Foo :=
  match f t with
  | some u => u
  | none =>
    match t with
    | .zero => .zero
    | .succ t' => recCasing f t'

example : recCasing f t = .zero := by
  unfold recCasing
  sorry

def recCasing2 (f : Foo → Option Foo) (t1 t2 : Foo) : Foo :=
  match f t1 with
  | some u => u
  | none =>
    match t2 with
    | .zero => .zero
    | .succ t' => recCasing f t'

example : recCasing2 f t1 t2 = .zero := by
  unfold recCasing2
  sorry

Let me look for related issues on the lean4 repo

[Sky Wilshaw]

Those unfolds don't work for me: failed to generate unfold theorem for 'recCasing'

[James Gallicchio]

Yep, that's the bug. It should work fine.

[James Gallicchio]

(recCasing is your original replace function)

[James Gallicchio]

and swapping the order of the matches also proceeds through the equation generator fine:

def recCasing' (f : Foo → Option Foo) (t : Foo) : Foo :=
  match t with
  | .zero =>
    match f t with
    | some u => u
    | none => .zero
  | .succ t' =>
    match f t with
    | some u => u
    | none => recCasing' f t'

example : recCasing' f t = .zero := by
  unfold recCasing'
  sorry

--note this is the same function as before
example : recCasing = recCasing' := by
  apply funext; intro f; apply funext; intro t
  induction t <;> simp [recCasing, recCasing']
  split <;> simp [*]

[James Gallicchio]

https://github.com/leanprover/lean4/issues/2962

[Sky Wilshaw]

Thanks for submitting the issue!