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
IndPreBelow.mkBelow
failure
#1672
Comments
@DanielFabian Do you have time to take a look? |
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 |
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: |
α : 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✝ |
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 [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 |
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 |
+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? |
The function
IndPredBelow.mkBelow
fails to generatebrecOn
for the following inductive predicate.The trace contains
Thus, we cannot use structural recursion in the following definition
This issue has been reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Recursive.20definition.20fails/near/301780366
The text was updated successfully, but these errors were encountered: