Missing `.brecOn`

Stream: new members

[Jonathan Chan]

I've noticed some inductive predicates don't get a .brecOn generated for them, but not always. What is it about these inductives that they don't have a .brecOn? Is it a feature in progress, or is there something fundamental about them that makes it impossible to have one? I imagine though that it should still theoretically be possible to do strong structural induction on them?
Here's an example of an inductive predicate with no .brecOn:

inductive Ty : Type where
  | unit : Ty
  | arr  : Ty → Ty → Ty

open Ty

inductive Term : Type where
  | var : Nat → Term
  | unit : Term
  | abs : Term → Term
  | app : Term → Term → Term
open Term

set_option hygiene false
notation:40 Γ:41 "⊢" a:41 "∶" A:41 => Wt Γ a A

inductive Wt : List Ty → Term → Ty → Prop where
  | var {Γ x} :
    (h : x < Γ.length) →
    --------------------
    Γ ⊢ var x ∶ Γ[x]
  | unit {Γ} :
    ---------------
    Γ ⊢ unit ∶ unit
  | abs {Γ b A B} :
    A :: Γ ⊢ b ∶ B →
    -------------------
    Γ ⊢ abs b ∶ arr A B
  | app {Γ b a A B} :
    Γ ⊢ b ∶ arr A B →
    Γ ⊢ a ∶ A →
    -----------------
    Γ ⊢ app b a ∶ B

#check Ty.brecOn
#check Term.brecOn
#check Wt.brecOn -- unknown constant 'Wt.brecOn'

In contrast, here is one that does (and it's mutual!)

mutual
inductive Even : Nat → Prop where
  | zero : Even 0
  | succ n : Odd n → Even (n + 1)

inductive Odd : Nat → Prop where
  | succ n : Even n → Odd (n + 1)
end
open Even Odd

#check Even.brecOn
#check Odd.brecOn

[Aaron Liu]

Inductives which get a .brecOn are recursive.

[Jonathan Chan]

Aren't they all recursive?

[Aaron Liu]

It's because Wt is a Prop, so it's not eligible for a Wt.below.

[Jonathan Chan]

Wt does have a .below, and so do Even and Odd, which are also Props, and which also have .brecOns

[Aaron Liu]

Here's another guess: maybe since Wt has a definition (getElem for List) in the conclusion of some of its constructors

[Jonathan Chan]

Deleting the Wt.var constructor entirely doesn't change anything, so looks like it's not that either

[Jonathan Chan]

Okay looking at what .brecOn actually says, it's actually possible to prove it for Wt, assuming Wt.below is correct:

theorem brecOn {motive : ∀ Γ a A, Γ ⊢ a ∶ A → Prop} {Γ a A} (h : Γ ⊢ a ∶ A) :
  (∀ Γ a A (h : Γ ⊢ a ∶ A), @Wt.below motive Γ a A h → motive Γ a A h) →
  motive Γ a A h := by
    refine λ ih ↦ ih Γ a A h ?_
    induction h using Wt.rec
    all_goals constructor <;> apply_rules

so I think it's whatever's generating .brecOn that's incomplete

[Joachim Breitner]

This trace option reveals the issue:

/--
info: [Meta.IndPredBelow] added [Wt.below]
[Meta.IndPredBelow] failed to prove brecOn for Wt.below
    couldn't solve by backwards chaining (Lean.Meta.IndPredBelow.maxBackwardChainingDepth = 10): case a
    motive✝ : (a : List Ty) → (a_1 : Term) → (a_2 : Ty) → Wt a a_1 a_2 → Prop
    a✝⁴ : List Ty
    a✝³ : Term
    a✝² : Ty
    x✝ : Wt a✝⁴ a✝³ a✝²
    ih✝ : ∀ (a : List Ty) (a_1 : Term) (a_2 : Ty) (x : Wt a a_1 a_2), x.below → motive✝ a a_1 a_2 x
    Γ : List Ty
    b a : Term
    A B : Ty
    a✝¹ : Wt Γ b (A.arr B)
    a✝ : Wt Γ a A
    a_ih✝¹ : a✝¹.below
    a_ih✝ : a✝.below
    ⊢ Wt Γ b (a✝².arr B)
-/
#guard_msgs in
inductive Wt : List Ty → Term → Ty → Prop where
  | var {Γ x} :
    (h : x < Γ.length) →
    --------------------
    Γ ⊢ var x ∶ Γ[x]
  | unit {Γ} :
    ---------------
    Γ ⊢ unit ∶ unit
  | abs {Γ b A B} :
    A :: Γ ⊢ b ∶ B →
    -------------------
    Γ ⊢ abs b ∶ arr A B
  | app {Γ b a A B} :
    Γ ⊢ b ∶ arr A B →
    Γ ⊢ a ∶ A →
    -----------------
    Γ ⊢ app b a ∶ B

Possibly the same issue as https://github.com/leanprover/lean4/issues/1672

[Robin Arnez]

I actually also have a bit of a question/RFC/whatever regarding brecOns:
Acc has a recursor that can eliminate into anything, but Acc.brecOn can only eliminate to Prop!
There doesn't seem to be anything preventing it from eliminating into anything though:

inductive Acc.below'.{u} {α : Sort u} {r : α → α → Prop} {motive : (a : α) → Acc r a → Sort u} : {a : α} → Acc r a → Sort _ where
  | intro (x : α) {h : ∀ (y : α), r y x → Acc r y} (h' : ∀ (y : α) (a : r y x), Acc.below' (motive := motive) (h y a))
    (h'' : ∀ (y : α) (a : r y x), motive y (h y a)) : Acc.below' (Acc.intro x h)

noncomputable def Acc.brecOn' {α : Sort u} {r : α → α → Prop} {motive : (a : α) → Acc r a → Sort u} {a : α} (x : Acc r a)
    (h : ∀ (a : α) (x : Acc r a), x.below' (motive := motive) → motive a x) : motive a x := by
  apply h
  induction x with
  | intro a h' ih =>
    constructor
    · exact ih
    · intro y rel
      exact h y _ (ih y rel)

[Robin Arnez]

This would be nice because then you could write recursive functions by structural recursion on a predicate instead of writing out a whole well-founded relation and what not

[Robin Arnez]

(this applies to any predicate being able to eliminate to anything, not just Acc)

[Jonathan Chan]

I don't know how structural recursion gets turned into brecOn, but it would be nice to be able to provide a custom below recursor for situations like this, something like termination_by structural using brecOn' => ...

[Joachim Breitner]

Robin Arnez said:

(this applies to any predicate being able to eliminate to anything, not just Acc)

Do you have practical examples of predicates besides Acc that have this property?

[Robin Arnez]

For example something like a no-cycles predicate: A while back, I worked on doubly-linked-lists (backed by an array) and there was a property that a particular node id was valid. That predicate was an inductive to (along other things) ensure that there are no cycles. In order to iterate through the list, it would've been helpful to use that predicate to do recursion. Instead, I ended up making a weird well-founded relation on the subtype of node ids that are valid. It's not really necessary to have it work directly but it would definitely be nice.

[Joachim Breitner]

Above we were talking about Acc, which is a rather peculiar beast that allows its recursor to eliminiate into Type, and I think only in the context of those special predicates we were wondering if .brecOn could be more general. Is your no-cycle-predicate one of those that can eliminate into Type?

[Jonathan Chan]

Joachim Breitner said:

Possibly the same issue as https://github.com/leanprover/lean4/issues/1672

Coming back to this, I tried out the patch in #4840 and it does succeed in generating .brecOn for Wt! This was the same issue I was having with structural mutual recursion for a similar inductive so it'll be great to be able to use mutual recursion for my proofs once that's merged in

[Joachim Breitner]

Im not sure when I'll get back to that experiment, it did break other things. But in any case it's helpful to collect regression tests, so if you have a mwe that is fixed by this, feel free to add it to the issue, with a comment that the fix fixes it.