failed to generate equational theorem

Stream: lean4

[Julien Marquet]

(This follows https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Failed.20to.20generate.20equational.20theorem -- but this version of the issue still exists in nightly-2022-03-30, after the patch that is mentioned in the original topic)

I came across the "failed to generate equational theorem" issue in some code of my own.
Details follow in the next message which is very lengthy due to the traces.

Is there a way to work around this other than defining the function myself in terms of WellFounded.fix ?
I can file an issue on lean4 if it seems relevant

[Julien Marquet]

Here's a mwe:

def g (t : Nat) : Nat := match t with
  | (n+1) => match g n with
    | 0 => 0
    | m + 1 => match g (n - m) with
      | 0 => 0
      | m + 1 => g n
  | 0 => 0
termination_by' sorry
decreasing_by sorry

set_option trace.Elab.definition.wf.eqns true
set_option trace.Elab.definition.structural.eqns true

example : (g 0) = 0 := by
  rw [g]
  admit

(It seems like the problem goes away when I fill the holes in termination_by' and decreasing_by, but I actually encounter this issue in another function where I did prove termination by hand, but I didn't use that function for the example because it requires much, much more work to define and to prove its termination. I can provide this function in a branch in the repo where I work, in case anyone wants to see it ;) )

The Elab.definition.structural.eqns traces show what's happening:

[Elab.definition.structural.eqns] mkEqnTypes step
α β : Type u
inst✝ : Monoid α
t : Nat
⊢ g t =
    match t with
    | Nat.succ n =>
      match g n with
      | 0 => 0
      | Nat.succ m =>
        match g (n - m) with
        | 0 => 0
        | Nat.succ m => g n
    | 0 => 0

[Elab.definition.structural.eqns] mkEqnTypes step
case h_1
α β : Type u
inst✝ : Monoid α
t_1 n : Nat
⊢ g (Nat.succ n) =
    match g n with
    | 0 => 0
    | Nat.succ m =>
      match g (n - m) with
      | 0 => 0
      | Nat.succ m => g n

-- Note that, in the following context, there is a new hypothesis, ` : g n = 0`
[Elab.definition.structural.eqns] mkEqnTypes step
case h_1.h_1
α β : Type u
inst✝ : Monoid α
t_1 n x : Nat
 : g n = 0
⊢ g (Nat.succ n) = 0

[...]

The WF equations generator (src/Lean/Elab/PreDefinition/WF/Eqns.lean) is then stuck because it tries to reduce a goal where g n never appears, because it works on a goal where g has been reduced to its definition in terms of WellFounded.fix

[Elab.definition.wf.eqns] step
α β : Type u
inst✝ : Monoid α
n : Nat
h : g n = 0
⊢ ((match (motive := (t : Nat) → ((y : Nat) → (sorryAx (WellFoundedRelation Nat) false).1 y t → Nat) → Nat)
        Nat.succ n with
      | Nat.succ n => fun x =>
        match x n (_ : (sorryAx (WellFoundedRelation Nat) false).1 n (Nat.succ n)) with
        | 0 => 0
        | Nat.succ m =>
          match x (n - m) (_ : (sorryAx (WellFoundedRelation Nat) false).1 (n - m) (Nat.succ n)) with
          | 0 => 0
          | Nat.succ m => x n (_ : (sorryAx (WellFoundedRelation Nat) false).1 n (Nat.succ n))
      | 0 => fun x => 0)
      fun y h =>
      WellFounded.fix g.proof_1
        (fun t a =>
          (match (motive := (t : Nat) → ((y : Nat) → (sorryAx (WellFoundedRelation Nat) false).1 y t → Nat) → Nat)
              t with
            | Nat.succ n => fun x =>
              match x n (_ : (sorryAx (WellFoundedRelation Nat) false).1 n (Nat.succ n)) with
              | 0 => 0
              | Nat.succ m =>
                match x (n - m) (_ : (sorryAx (WellFoundedRelation Nat) false).1 (n - m) (Nat.succ n)) with
                | 0 => 0
                | Nat.succ m => x n (_ : (sorryAx (WellFoundedRelation Nat) false).1 n (Nat.succ n))
            | 0 => fun x => 0)
            a)
        y) =
    0

[Julien Marquet]

Maybe a temporary solution for me would be to have access to a theorem that states g in terms of WellFounded.rec, is there such a theorem that is generated ?

[Leonardo de Moura]

I pushed a fix for this. The issue happens in declarations using nested recursion and overlapping patterns.
I added your example to the test suite.
https://github.com/leanprover/lean4/commit/096e4eb6d0f56ba395bb658bea87518a8baa4b57

(This follows https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Failed.20to.20generate.20equational.20theorem -- but this version of the issue still exists in nightly-2022-03-30, after the patch that is mentioned in the original topic)

The example on this thread has been on our test suite for a while. https://github.com/leanprover/lean4/blob/master/tests/lean/run/splitIssue.lean
Have you tried a variant of this example?
I have also added today another test where we define this example without any unsound sorrys.
https://github.com/leanprover/lean4/blob/master/tests/lean/run/splitList.lean
It requires a bit of "plumbing" by it is doable in the current system.

[Julien Marquet]

Leonardo de Moura said:

I pushed a fix for this. The issue happens in declarations using nested recursion and overlapping patterns.
I added your example to the test suite.
https://github.com/leanprover/lean4/commit/096e4eb6d0f56ba395bb658bea87518a8baa4b57

Great, thanks ! I'm impressed by how fast you fixed it :)
I just switched to the latest nightly and tested, everything works fine now in my code, thanks again !

[Julien Marquet]

Leonardo de Moura said:

The example on this thread has been on our test suite for a while. https://github.com/leanprover/lean4/blob/master/tests/lean/run/splitIssue.lean
Have you tried a variant of this example?

No, I didn't try this particular example because since you fixed it and I run a recent enough version, I thought I wouldn't be able to make Lean behave incorrectly from this particular example (I'm not sure if that's what you're asking though, sorry if I missed your point...)

[Julien Marquet]

Leonardo de Moura said:

I have also added today another test where we define this example without any unsound sorrys.
https://github.com/leanprover/lean4/blob/master/tests/lean/run/splitList.lean
It requires a bit of "plumbing" by it is doable in the current system.

Would you be interested in an example that has no unsound sorry ? I guess I can build one if you want, modulo the time required by the plumbing

[Notification Bot]

Julien Marquet has marked this topic as resolved.

[Notification Bot]

Julien Marquet has marked this topic as unresolved.

[Julien Marquet]

It seems like I've hit another bug:

def g (t : Nat) : Nat := match t with
  | (n+1) => match g n with
    | 0 => 0
    | m + 1 => match g (n - m) with
      | 0 => 0
      | m + 1 => g n
  | 0 => 0
termination_by' sorry
decreasing_by sorry

theorem ex3 : g (n + 1) = match g n with
    | 0 => 0
    | m + 1 => match g (n - m) with
      | 0 => 0
      | m + 1 => g n := by
  conv => lhs; rw [g]
  admit

convert tactic failed, there are unsolved goals
case h
n : Nat
⊢ g n = 0

The problem arises from the conditions that lie in the generated equations.
My guess is that the equation generator should actually also generate unconditional equations: the theorem ex3 is an example of an unconditional equation that we would like to have.
From the error, it also looks like rw only tries the first equation it finds (I'm not entirely sure though, maybe it only reports the first error ?)

[Julien Marquet]

(I've also hit a "failed to generate unfold theorem", I'm trying to write a MWE)

[Julien Marquet]

Here's a mwe that triggers "failed to generate unfold theorem":

inductive Term
  | Var (i : Nat)
  | Cons (l : Term) (r : Term)

def Subst := Nat → Nat

def depth : Term → Nat
  | .Var _ => 0
  | .Cons l r => 1 + depth l + depth r

def act (f : Subst) (t : Term) := match t with
  | .Var i => Term.Var (f i)
  | .Cons l r => Term.Cons (act f l) (act f r)

def strangers (u v : Term) := ∀ f : Subst, act f u ≠ act f v

abbrev P (c : Option Subst) u v := match c with
  | none => strangers u v
  | some f => act f u = act f v

def rel : WellFoundedRelation (Term × Term) := measure (λ (u, v) => depth u + depth v)

theorem decr_left (l₁ r₁ l₂ r₂ : Term) :
  rel.rel (l₁, l₂) (Term.Cons l₁ r₁, Term.Cons l₂ r₂) := by
  suffices h : depth l₁ + depth l₂ < depth (Term.Cons l₁ r₁) + depth (Term.Cons l₂ r₂) from h
  admit

theorem decr_right (l₁ r₁ l₂ r₂ : Term) (f : Subst) :
  rel.rel (act f r₁, act f r₂) (Term.Cons l₁ r₁, Term.Cons l₂ r₂) := by
  suffices h : depth (act f r₁) + depth (act f r₂) < depth (Term.Cons l₁ r₁) + depth (Term.Cons l₂ r₂) from h
  admit

def robinson (u v : Term) : { f : Option Subst // P f u v } := match u, v with
  | .Cons l₁ r₁, .Cons l₂ r₂ => match robinson l₁ l₂ with
    | ⟨ none, h ⟩ => ⟨ none, sorry ⟩
    | ⟨ some f, h ⟩ => match robinson (act f r₁) (act f r₂) with
      | ⟨ none, h ⟩ => ⟨ none, sorry ⟩
      | ⟨ some g, h ⟩ => ⟨ some (g ∘ f), sorry ⟩
  | .Var i, .Cons l r => ⟨ none, sorry ⟩
  | .Cons l r, .Var i => ⟨ none, sorry ⟩
  | .Var i, .Var j =>
    if i = j then ⟨ some id, sorry ⟩
    else ⟨ some λ n => if n = i then j else n, sorry ⟩
termination_by' invImage (λ ⟨ u, v ⟩ => (u, v)) rel
decreasing_by
  first
    | apply decr_left _ _ _ _
    | apply decr_right _ _ _ _ _

theorem ex : (robinson (Term.Var 0) (Term.Var 0)).1 = some id := by
  unfold robinson -- fails here
  admit

failed to generate unfold theorem for 'robinson'
case h_1.h_1
u_1 v_1 l₁ r₁ l₂ r₂ : Term
x : { f // P f l₁ l₂ }
h : P none l₁ l₂
 : robinson l₁ l₂ = { val := none, property := h }
⊢ robinson (Term.Cons l₁ r₁) (Term.Cons l₂ r₂) =
    { val := none, property := (_ : P none (Term.Cons l₁ r₁) (Term.Cons l₂ r₂))

The hypothesis h : P none l₁ l₂ in this context looks suspicious imho (in my own code, I've seen the context cluttered by lots of such hypotheses that come from recursive calls, but that can't be proven automatically -- because the purpose of my theorem is to prove them)

I've tried to make this example actually provable, but I don't have the patience to fill the sorrys right now :p

[Julien Marquet]

I think this example also triggers the bug I originally mentioned

[Leonardo de Moura]

I pushed fixes for both issues. They were due to different problems.

[Leonardo de Moura]

https://github.com/leanprover/lean4/commit/4a0f68de83995436e59567d235dd05f1e52e84b1
https://github.com/leanprover/lean4/commit/a926cd1698bce3208591a901bd328f2258e0b697