`IndPreBelow.mkBelow` failure

[leodemoura]

The function IndPredBelow.mkBelow fails to generate brecOn for the following inductive predicate.

set_option trace.Meta.IndPredBelow true in
inductive TransClosure (r : α → α → Prop) : α → α → Prop
  | extends : r a b → TransClosure r a b
  | trans_left : r a b → TransClosure r b c → TransClosure r a c

The trace contains

[Meta.IndPredBelow] failed to prove brecOn for TransClosure.below
    couldn't solve by backwards chaining (Lean.Meta.IndPredBelow.maxBackwardChainingDepth = 10): case a
    α : Sort u_1
    r : α → α → Prop
    motive✝ : (a a_1 : α) → TransClosure r a a_1 → Prop
    a✝³ a✝² : α
    : TransClosure r a✝³ a✝²
    : ∀ (a a_1 : α) (x : TransClosure r a a_1), TransClosure.below x → motive✝ a a_1 x
    a b c : α
    : r a b
    a✝ : TransClosure r b c
    a_ih✝ : TransClosure.below a✝
    ⊢ r a a✝³

Thus, we cannot use structural recursion in the following definition

def trans' {a b c} : TransClosure r a b → TransClosure r b c → TransClosure r a c
| .extends h₁       => .trans_left h₁
| .trans_left h₁ h₂ => .trans_left h₁ ∘ trans' h₂

This issue has been reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Recursive.20definition.20fails/near/301780366

[leodemoura]

@DanielFabian Do you have time to take a look? Thanks, Leo

[DanielFabian]

At first glance it looks like unprovable non-sense. So it's possible that it applied a bad tactic some steps earlier or something about the goal is wrong. I'll try to understand a bit better what is going on

[DanielFabian]

here's roughly what's going on:

We first do a few introductions, apply the IH, induction and apply constructors. Up to this point, I think it looks still ok. Thus we create a bunch of goals to solve:

[DanielFabian]

     α : Sort u_1
     r : α → α → Prop
     motive✝ : (a a_1 : α) → Ex.TransClosure r a a_1 → Prop
     a✝² a✝¹ : α
     : Ex.TransClosure r a✝² a✝¹
     : ∀ (a a_1 : α) (x : Ex.TransClosure r a a_1), Ex.TransClosure.below x → motive✝ a a_1 x
     a b : α
     : r a b
     ⊢ r a b

     α : Sort u_1
     r : α → α → Prop
     motive✝ : (a a_1 : α) → Ex.TransClosure r a a_1 → Prop
     a✝³ a✝² : α
     : Ex.TransClosure r a✝³ a✝²
     : ∀ (a a_1 : α) (x : Ex.TransClosure r a a_1), Ex.TransClosure.below x → motive✝ a a_1 x
     a b c : α
     : r a b
     a✝ : Ex.TransClosure r b c
     a_ih✝ : Ex.TransClosure.below a✝
     ⊢ α

     α : Sort u_1
     r : α → α → Prop
     motive✝ : (a a_1 : α) → Ex.TransClosure r a a_1 → Prop
     a✝³ a✝² : α
     : Ex.TransClosure r a✝³ a✝²
     : ∀ (a a_1 : α) (x : Ex.TransClosure r a a_1), Ex.TransClosure.below x → motive✝ a a_1 x
     a b c : α
     : r a b
     a✝ : Ex.TransClosure r b c
     a_ih✝ : Ex.TransClosure.below a✝
     ⊢ r a ?b

     α : Sort u_1
     r : α → α → Prop
     motive✝ : (a a_1 : α) → Ex.TransClosure r a a_1 → Prop
     a✝³ a✝² : α
     : Ex.TransClosure r a✝³ a✝²
     : ∀ (a a_1 : α) (x : Ex.TransClosure r a a_1), Ex.TransClosure.below x → motive✝ a a_1 x
     a b c : α
     : r a b
     a✝ : Ex.TransClosure r b c
     a_ih✝ : Ex.TransClosure.below a✝
     ⊢ Ex.TransClosure r ?b c

     α : Sort u_1
     r : α → α → Prop
     motive✝ : (a a_1 : α) → Ex.TransClosure r a a_1 → Prop
     a✝³ a✝² : α
     : Ex.TransClosure r a✝³ a✝²
     : ∀ (a a_1 : α) (x : Ex.TransClosure r a a_1), Ex.TransClosure.below x → motive✝ a a_1 x
     a b c : α
     : r a b
     a✝ : Ex.TransClosure r b c
     a_ih✝ : Ex.TransClosure.below a✝
     ⊢ Ex.TransClosure.below ?a✝

     α : Sort u_1
     r : α → α → Prop
     motive✝ : (a a_1 : α) → Ex.TransClosure r a a_1 → Prop
     a✝³ a✝² : α
     : Ex.TransClosure r a✝³ a✝²
     : ∀ (a a_1 : α) (x : Ex.TransClosure r a a_1), Ex.TransClosure.below x → motive✝ a a_1 x
     a b c : α
     : r a b
     a✝ : Ex.TransClosure r b c
     a_ih✝ : Ex.TransClosure.below a✝
     ⊢ motive✝ ?b c ?a✝

[DanielFabian]

this all looks solvable to me. I'm not perfectly sure about the last goal, but I think if we apply backwards chaining, we could solve it.

The problem, I believe is the second goal that simply wants an α. And there 5 different objects of type α around. So I think what's happening is that the prove simply picks the first but that then effectively chooses the metavariable and it modifies the other goals rendering some of them unprovable!

When we then subsequently ask closeGoal to prove the goal, things go south:

[Meta.IndPredBelow] closeGoal:
    case a
    α : Sort u_1
    r : α → α → Prop
    motive✝ : (a a_1 : α) → Ex.TransClosure r a a_1 → Prop
    a✝² a✝¹ : α
    : Ex.TransClosure r a✝² a✝¹
    : ∀ (a a_1 : α) (x : Ex.TransClosure r a a_1), Ex.TransClosure.below x → motive✝ a a_1 x
    a b : α
    : r a b
    ⊢ r a b
[Meta.IndPredBelow] closeGoal:
    case b
    α : Sort u_1
    r : α → α → Prop
    motive✝ : (a a_1 : α) → Ex.TransClosure r a a_1 → Prop
    a✝³ a✝² : α
    : Ex.TransClosure r a✝³ a✝²
    : ∀ (a a_1 : α) (x : Ex.TransClosure r a a_1), Ex.TransClosure.below x → motive✝ a a_1 x
    a b c : α
    : r a b
    a✝ : Ex.TransClosure r b c
    a_ih✝ : Ex.TransClosure.below a✝
    ⊢ α
[Meta.IndPredBelow] closeGoal:
    case a
    α : Sort u_1
    r : α → α → Prop
    motive✝ : (a a_1 : α) → Ex.TransClosure r a a_1 → Prop
    a✝³ a✝² : α
    : Ex.TransClosure r a✝³ a✝²
    : ∀ (a a_1 : α) (x : Ex.TransClosure r a a_1), Ex.TransClosure.below x → motive✝ a a_1 x
    a b c : α
    : r a b
    a✝ : Ex.TransClosure r b c
    a_ih✝ : Ex.TransClosure.below a✝
    ⊢ r a a✝³

Notice how the last goal has ⊢ r a a✝³ as goal as opposed to ⊢ r a ?b as before. And now it's unprovable.

[DanielFabian]

So, in other words, I don't think we can greedily apply backwards resolution. I think we need to exhaustively try all possible proofs for each goal.

This may sound terrible, but if we first check for each goal if we can uniquely prove using backwards chaining and delay it otherwise, we wouldn't pay that much most of the time. And, indeed, in this case, we wouldn't pay anything. Because if we first proved the goal ⊢ r a ?b, that would constrain the ?b in such a way, that the other goal would then become uniquely provable, I think.

[watersofoblivion]

+1 on this issue. Ran into the same thing (reported on Zulip as well.)

Any progress?

FWIW, I'm doing a very similar thing (making a recursive call to construct the IH for an inductively-defined proposition) here and other places as well with no problem. The difference in those cases is that the inductive proposition is not polymorphic. Is this issue specifically tied to polymorphic inductively-defined propositions?

[nomeata]

Together with @DanielFabian we looked into this, and it turns out we can solve this by deleting code:

@@ -310,9 +311,6 @@ where
         args.back.withApp fun ctor _ => do
         let ctorName := ctor.constName!.updatePrefix below.constName!
         let ctor := mkConst ctorName below.constLevels!
-        let ctorInfo ← getConstInfoCtor ctorName
-        let (mvars, _, _) ← forallMetaTelescope ctorInfo.type
-        let ctor := mkAppN ctor mvars
         m.apply ctor
     return mss.foldr List.append []

The reason is that the apply tactic by default returns the mvars in a more useful order (non-dependent first), and thus we then get ?b resolved by unification and don't have to search for it.

Not sure if this will solve all problems of this form, but probably a fair number of them.