-
Notifications
You must be signed in to change notification settings - Fork 369
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
fix: IndPred: track function's motive in a let binding, use withoutProofIrrelevance #4827
Conversation
…oofIrrelevance this improves support for structural recursion over inductive *predicates* when there are reflexive arguments. Consider ```lean 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 ``` motive : F → Prop := fun x => True x✝ : x✝¹.below f : Nat → F a✝¹ : ∀ (a : Nat), (f a).below a✝ : ∀ (a : Nat), motive (f a) ⊢ motive (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
Mathlib CI status (docs):
|
@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
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). |
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 |
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? |
That's true for constructing |
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. |
No worries! I tend to get hazy about details more quickly than that :-) |
this improves support for structural recursion over inductive
predicates when there are reflexive arguments.
Consider
Previously the search for the right induction hypothesis would fail with
The backchaining process will try to use
a✝ : Nat → True
, but then hasno idea what to use for
Nat
.There are three steps to fix this.
We let-bind the function's type before the whole process. Now the
goal is
Next we do more aggressive unification when seeing if an assumption
matches: Given
it continues with
a =?= c
andb =?= d
, even ifg
is a let-boundvariable.
This gives us
f 0 =?= f ?a
. In order to make progress here, we usewithoutProofIrrelevance
, because elseisDefEq
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