fix: IndPred: track function's motive in a let binding, use withoutProofIrrelevance

[nomeata]

this improves support for structural recursion over inductive predicates when there are reflexive arguments.

Consider

inductive F: Prop where
  | base
  | step (fn: Nat → F)

-- set_option trace.Meta.IndPredBelow.search true
set_option pp.proofs true

def F.asdf1 : (f : F) → True
  | base => trivial
  | step f => F.asdf1 (f 0)
termination_by structural f => f`

Previously the search for the right induction hypothesis would fail with

could not solve using backwards chaining x✝¹ : F
x✝ : x✝¹.below
f : Nat → F
a✝¹ : ∀ (a : Nat), (f a).below
a✝ : Nat → True
⊢ True

The backchaining process will try to use a✝ : Nat → True, but then has no idea what to use for Nat.

There are three steps to fix this.

1. We let-bind the function's type before the whole process. Now the goal is

   funType : F → Prop := fun x => True
   x✝ : x✝¹.below
   f : Nat → F
   a✝¹ : ∀ (a : Nat), (f a).below
   a✝ : ∀ (a : Nat), funType (f a)
   ⊢ funType (f 0)
   

2. Next we do more aggressive unification when seeing if an assumption matches: Given

   g a b =?= h c d
   

   it continues with a =?= c and b =?= d, even if g is a let-bound variable.

3. This gives us f 0 =?= f ?a. In order to make progress here, we use withoutProofIrrelevance, because else isDefEq is happy to say “they are equal” without actually looking at the terms and thus assigning ?a := 0.

This idea of let-binding the function's motive may also be useful for the other recursion compilers, as it may simplify the FunInd construction. This is to be investigated.

fixes #4751

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 93fa9c8837e071a866b62e2ca73c22a362ccb988 --onto 5938dbbd14145c9b78f7645c4777f62a3fc8212c. (2024-07-25 08:50:27)

[nomeata]

@DanielFabian this the idea that I mentioned, and seems to be able to handle the examples in that bug report.

I wonder whether a full proof search is really needed for replacing the recursive arguments. When would the assumption to use be more complicated than something like

a✝ : ∀ (a : Nat), motive (f a)

i.e. the function’s recursive type, applied to indices, the target, and possibly extra arguments, where the target is a plain variable or a function application (if the constructor has a reflexive parameters).

[DanielFabian]

Iirc, the motive is indeed always simple because it is completely opaque to us. In particular variables neither show up, nor are swallowed.

The only problem I had in the past was that sometimes there were multiple objects of the right type in the local context and it was important to pick the right one

[DanielFabian]

I'm going to mention #1672 again, because since you're changing the backwards-chaining it's possible it'll have an impact over there, too?

[nomeata]

Iirc, the motive is indeed always simple because it is completely opaque to us

That's true for constructing .below, but when compiling a concrete function (like T -> True), the motive is fun _ => True, isn't it?

[DanielFabian]

I'm really sorry, at this point I'm fairly hazy about the details. It's been a few years and the construction is not trivial. To jog my memory, it would be really great if you could share some of the proof states that we're seeing and where the tactics fail. Unless you want to walk me through your steps; that's also an option. At this point, I don't even remember how to run or debug this thing, making understanding it from just source code quite a challenge.

[nomeata]

No worries! I tend to get hazy about details more quickly than that :-)