"failed to generate equational theorem" when matching on not only recursive call

[nomeata]

This could be a duplicate of #3219 or #2962. Still reporting it separately, so when a fix is applied each example can be checked and closed separately, and nothing falls through the cracks.

Here is a minimized version of the issue that's currently biting me:

inductive Expr where
  | const (i : BitVec 32)
  | op (op : Unit) (e1 : Expr)

-- fails:

def optimize : Expr → Expr
  | .const i => .const i
  | .op bop e1 =>
    match bop, optimize e1 with
    | _, .const _ => .op bop (.const 0)
    | _, _ => .const 0

#check optimize.eq_1

-- works:

def optimize2 : Expr → Expr
  | .const i => .const i
  | .op bop e1 =>
    match optimize2 e1 with
    | .const _ => .op bop (.const 0)
    | _ => .const 0

#check optimize2.eq_1

-- also works:

def optimize3 : Expr → Expr
  | .const i => .const i
  | .op bop e1 =>
    match bop, e1 with
    | _, .const _ => .op bop (optimize3 e1)
    | _, _ => .const 0

#check optimize3.eq_1

Note it seems crucial to have a match that matches on both the recursive call, and some other parameter.

Switching to well-founded recursion does not help.

Versions

"4.13.0-rc3"

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

The error message gives a glimpse: The recursive function is unfolded to its internal guts, and then contradiction (or whatever tactic is involved here) fails to see the contradiction:

Failed to realize constant optimize.eq_1:
  failed to generate equational theorem for 'optimize'
  
case h_2
e1 : Expr
i : BitVec 32
heq : optimize e1 = Expr.const i
bop✝ bop_1 : Unit
x : Expr
x_3 : ∀ (i : BitVec 32),
  (Expr.rec (fun i => ⟨Expr.const i, PUnit.unit⟩)
          (fun op e1 e1_ih =>
            ⟨match op, e1_ih.1 with
              | x, Expr.const i => Expr.op op (Expr.const 0)
              | x, x_1 => Expr.const 0,
              e1_ih⟩)
          e1).1 =
      Expr.const i →
    False
⊢ Expr.const 0 = Expr.op bop✝ (Expr.const 0)

[nomeata]

Ah, and with well-founded recursion we see the different guts. The plot thickens.

case h_2
e1 : Expr
i : BitVec 32
heq : optimize e1 = Expr.const i
bop✝ bop_1 : Unit
x : Expr
x_3 : ∀ (i : BitVec 32),
  optimize.proof_1.fix
        (fun a a_1 =>
          (match (motive :=
              (x : Expr) → ((y : Expr) → (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 y x → Expr) → Expr)
              a with
            | Expr.const i => fun x => Expr.const i
            | Expr.op bop e1 => fun x =>
              match bop, x e1 ⋯ with
              | x, Expr.const i => Expr.op bop (Expr.const 0)
              | x, x_1 => Expr.const 0)
            a_1)
        e1 =
      Expr.const i →
    False
⊢ Expr.const 0 = Expr.op bop✝ (Expr.const 0)

---

This also doesn't fail:

def optimize : Expr → Expr
  | .const i => .const i
  | .op bop e1 =>
    match (bop, optimize e1) with
    | (_, .const _) => .op bop (.const 0)
    | (_, _) => .const 0

---

Tried a few things, but no clear way forward. The deltaLHS in Lean.Elab.Structural.mkProof exposes the guts of the recursive function, and maybe that’s the problem here, because some tactics don’t recognize it’s defeq to the original function?

I assume tryContradiction in Lean.Elab.Structural.mkProof should be the tactic that solves this, but I am not sure. Bumping transparency and disabling smart unfolding does not help…

Hmm, enough investigation for now.

[nomeata]

This issue is at least getting worse due to #5129; before we would generate

optimize2.eq_2 (bop : Unit) (e1 : Expr) :
  optimize2 (Expr.op bop e1) =
    match bop, optimize2 e1 with
    | x, Expr.const i => Expr.op bop (Expr.const 0)
    | x, x_1 => Expr.const

and that works, now we would generate

 ∀ (e1 : Expr) (bop : Unit) (i : Nat),
      optimize2 e1 = Expr.const i → optimize2 (Expr.op bop e1) = Expr.op bop (Expr.const 0)

and that fails.

But that PR did not introduce the issue, it already exists with

def optimize2 : Expr → Expr
  | .const i => .const i
  | .op bop e1 =>
    match bop, optimize2 e1 with
    | _, .const _ => .op bop (.const 0)
    | _, e1' => optimize2 e1'
termination_by e => e
decreasing_by sorry

(we need a recursive calls in the arms for this code path to trigger before.)

[nomeata]

I conjecture that this would be robust if we create the .unfold theorem first (simple for WF rec due to WellFounded.fix_eq. For structural recursion it’s one level of delta and then essentially the same code used for equations now, splitting until it’s rfl).

And then we prove the fine-grained equational lemmas by rfl, if possible, else by unfolding the .unfold on the left and then using the existing code.

This way, the internals don't show up in the second step any more. And it’d be the same code path for structural, wf and non-recursive functions.

[nomeata]

It would at least fix this, partial work in #5669, but shelving it for today (I hope).