failed to generate equality theorem when mixing patterns on index and indexed type

[nomeata]

Matches that mix pattern matching on indexed types as well as their indices are notorious tricky. Here is another example:

inductive Parity : Nat -> Type
| even (n) : Parity (n + n)
| odd  (n) : Parity (Nat.succ (n + n))


partial def natToBin3 : (n : Nat) → Parity n →  List Bool
| 0, _             => []
| _, Parity.even j => [false, false]
| _, Parity.odd  j => [true, true]

/--
error: Failed to realize constant natToBin3.match_1.splitter:
  failed to generate equality theorems for `match` expression `natToBin3.match_1`
  motive✝ : (x : Nat) → Parity x → Sort u_1
  j✝ : Nat
  h_1✝ : (x : Parity 0) → motive✝ 0 x
  h_2✝ : (j : Nat) → motive✝ (j + j) (Parity.even j)
  h_3✝ : (j : Nat) → motive✝ (j + j).succ (Parity.odd j)
  x✝ : ∀ (x : Parity 0), j✝ + j✝ = 0 → Parity.even j✝ ≍ x → False
  ⊢ Nat.rec (motive := fun t =>
        (Nat.hasNotBit 1 t.ctorIdx → (fun x => (x_1 : Parity x) → motive✝ x x_1) t) →
          (fun x => (x_1 : Parity x) → motive✝ x x_1) t)
        (fun x x_1 => h_1✝ x_1) (fun n n_ih x => x ⋯) (j✝ + j✝)
        (fun h x =>
          Parity.casesOn (motive := fun a x_1 => j✝ + j✝ = a → x ≍ x_1 → motive✝ (j✝ + j✝) x) x
            (fun n h_1 =>
              Eq.ndrec (motive := fun x =>
                Nat.hasNotBit 1 x.ctorIdx → (x_1 : Parity x) → x_1 ≍ Parity.even n → motive✝ x x_1)
                (fun h x h_2 => ⋯ ▸ h_2✝ n) ⋯ h x)
            (fun n h_1 =>
              Eq.ndrec (motive := fun x =>
                Nat.hasNotBit 1 x.ctorIdx → (x_1 : Parity x) → x_1 ≍ Parity.odd n → motive✝ x x_1)
                (fun h x h_2 => ⋯ ▸ h_3✝ n) ⋯ h x)
            ⋯ ⋯)
        (Parity.even j✝) =
      h_2✝ j✝
---
error: Unknown constant `natToBin3.match_1.splitter`
-/
#guard_msgs in
#print sig natToBin3.match_1.splitter

That the match statement even compiles is somewhat new, a side-effect of #10823. But then the equation theorem calculation goes wrong.

The problem is that the matcher is doing case analysis on (j✝ + j✝) which proveCondEqThm is not able to make progress on.

Maybe it would be able to make progress by generalizing the scrutinee ((j✝ + j✝)), notice that one branch is unreachable (using x✝ : ∀ (x : Parity 0), j✝ + j✝ = 0 → Parity.even j✝ ≍ x → False) and then continuing. But it’s tricky, and this is a somewhat obscure function, so for now just recording this here.

Impact

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

[nomeata]

I investigated a bit and I believe there is a way forward, but it would require rewriting Lean.Meta.Match.proveCondEqThm.

Instead of proving the equational theorem, we could first prove the “congruence equational theorem” (Added in #8284). There, the LHS is the matcher applied to variables, and the concrete values are added as assumptions. In that form, it should be possible to reliably do a complete case split into the leaves.

Only when we are at the leaf we then substitute all the equations.

In the correct branch, this should turn the HEq into a Eq and we can solve it.

In the other branches, that either leads to a contradiction, or the overlap assumption will take care of it.

I dabbled a bit in that direction; we would be faced with tricky goals like

motive✝ : (x : Nat) → Parity x → Sort u_1
h_1✝ : (x : Parity 0) → motive✝ 0 x
h_2✝ : (j : Nat) → motive✝ (j + j) (Parity.even j)
h_3✝ : (x : Parity (Nat.succ 0)) → motive✝ 1 x
h_4✝ : (j : Nat) → motive✝ (j + j).succ (Parity.odd j)
h_5✝ : (x : Nat) → (x_1 : Parity x) → motive✝ x x_1
j✝ : Nat
x✝¹ : ∀ (x : Parity 0), j✝ + j✝ = 0 → Parity.even j✝ ≍ x → False
x✝ : Parity Nat.zero
heq_1✝ : Nat.zero = j✝ + j✝
heq_2✝ : x✝ ≍ Parity.even j✝
⊢ h_1✝ x✝ ≍ h_2✝ j✝

(where we of course can use the overlap assumption x✝¹ – but how to reliably do so) or

motive✝ : (x : Nat) → Parity x → Sort u_1
h_1✝ : (x : Parity 0) → motive✝ 0 x
h_2✝ : (x : Parity (Nat.succ 0)) → motive✝ 1 x
h_3✝ : (j : Nat) → motive✝ (j + j) (Parity.even j)
h_4✝ : (j : Nat) → motive✝ (j + j).succ (Parity.odd j)
h_5✝ : (x : Nat) → (x_1 : Parity x) → motive✝ x x_1
x✝¹ : Parity (Nat.succ 0)
n✝ : Nat
x✝ : Parity n✝.succ.succ
heq_1✝ : n✝.succ.succ = 1
heq_2✝ : x✝ ≍ x✝¹
⊢ Parity.rec (motive := fun a x => n✝.succ.succ = a → x✝ ≍ x → motive✝ n✝.succ.succ x✝)
    (fun n =>
      (fun n h =>
          Eq.ndrec (motive := fun x => (x_1 : Parity x) → x_1 ≍ Parity.even n → motive✝ x x_1)
            (fun x h => Eq.symm (eq_of_heq h) ▸ h_3✝ n) (Eq.symm h) x✝)
        n)
    (fun n =>
      (fun n h =>
          Eq.ndrec (motive := fun x => (x_1 : Parity x) → x_1 ≍ Parity.odd n → motive✝ x x_1)
            (fun x h => Eq.symm (eq_of_heq h) ▸ h_4✝ n) (Eq.symm h) x✝)
        n)
    x✝ (Eq.refl n✝.succ.succ) (HEq.refl x✝) ≍
  h_2✝ x✝¹

where contradiction does not look deeply into n✝.succ.succ = 1 to see the contradiction.

---

Noting more thoughts:

• Maybe the latter can be handled systematically if we keep track of which assumptions come from the congruence equality setup, and apply injectivity on them eagerly, and/or substitute them if they are of the form x = ctor and we are just about to do cases on x.

• The former still seems hard. We could try to orient them consistently, and use assumption, but I worry that this is not reliable enough, they may look different. Maybe using a congruence-closure-only variant of grind? But that’s a big hammer.

[nomeata]

Ok, here is a plan of attack that might work:

• Prove the congruence rewrite rules. It’s important that the goal starts with match_1 x y … so that all case splits done by the matcher can be followed, and are not blocked because some scrutinee isn't a variable.

• Do not just whnfCore on the left, but make sure that, for example, sparse caseson applications are preserved and then more carefully split. We don’t want to do the catch-call of a sparse case more than once, and we don’t want variables to be instantiated there.

• (Maybe): Before a case split on x, if we have x = ctor e in the context, set y = e and substitute ctor y for x. This way we can reduce the case split without handling all cases.

  Ah, but we should not do that when facing a sparse case and the ctor is in the catch-all, as we don't want to change the goal. So maybe not do this.

• Once we reach a leaf, we can tell from the goal whether this should be a solvable or unsolvable goal.

• If it is solvable, we should be able to subst all the equations from the congruence equation lemma, turn the HEq into an Eq, and solve it by rfl.

• If it is unsolvable, there are two cases:

  • we have an overlap assumption for that branch. Then contradition +genDiseq should handle that fine (if we kep the goal exactly as general as in the matcher).

  • else one of the equations from the congruence equation should be a contradiction. Unfortunately, it may be a nested contradiction like above (n✝.succ.succ = 1), so some work needs to be done here.

    maybe what should be done: Whenever we do a case split on x, and we had x = ctor1 … in scope, so we get ctor … = ctor1 … (with different same constructors), we we run injectivity. But if we get ctor … = non-ctor-expr, we leave it alone. By running injectivity only after a case that was forced by the matcher code, we avoid the problem of dealing with 1001 = 1000 that’s the reason why contradiction does not just handle this.

This is a sizeable change to how match equation are calculated, and not a cheap one in some cases. But maybe the way forward.

[nomeata]

Still not easy.

The tricky bit is when the context has

heq_1✝ : x✝² = j✝ + j✝
heq_2✝ : x✝¹ ≍ Parity.even j✝
x✝ : ∀ (x : Parity 0), j✝ + j✝ = 0 → Parity.even j✝ ≍ x → False
⊢ natToBin3._sparseCasesOn_1 (motive := fun x => (x_1 : Parity x) → motive✝ x x_1) x✝² …

and we are just about to split the _sparseCasesOn_1. Then we get

j✝ : Nat
x✝¹ : ∀ (x : Parity 0), j✝ + j✝ = 0 → Parity.even j✝ ≍ x → False
x✝ : Parity Nat.zero
heq_1✝ : Nat.zero = j✝ + j✝
heq_2✝ : x✝ ≍ Parity.even j✝
⊢ …

and we have lost; this is beyond contradiction even with substVars.

(Granted, I was hoping to see ∀ (x : Parity 0), x✝² = 0 → x✝¹ = x → False here, but not sure if that would make a difference…)

(Hmm, it actually might. So do we need to work the pre-simpH overlap here?)

[nomeata]

Ah, progress. That seems to help. But now I am stuck at

case else.even
motive✝ : (x : Nat) → Parity x → Sort u_1
h_1✝ : (x : Parity 0) → motive✝ 0 x
h_2✝ : (j : Nat) → motive✝ (j + j) (Parity.even j)
h_3✝ : (j : Nat) → motive✝ (j + j).succ (Parity.odd j)
j✝ n✝ : Nat
h✝ : Nat.hasNotBit 1 (n✝ + n✝).ctorIdx
heq_1✝ : n✝ + n✝ = j✝ + j✝
heq_2✝ : Parity.even n✝ ≍ Parity.even j✝
x✝ : ∀ (x : Parity 0), n✝ + n✝ = 0 → Parity.even n✝ ≍ x → False
⊢ h_2✝ n✝ ≍ h_2✝ j✝

Clearly we have taken a wrong turn if we see n✝ + n✝ = j✝ + j✝ here. Probably we should have substituted

heq_1✝ : x✝² = j✝ + j✝
heq_2✝ : x✝¹ ≍ Parity.even j✝

just before splitting Parity.casesOn. But how to tell when to substitute what?