chore: potential nontermination at simp#485
Conversation
Using `simp [forIn]` may cause nontermination with different `simp` reduction strategies. We have the following theorem ``` @[simp] theorem forIn_eq_forIn [Monad m] : @List.forIn α β m _ = forIn := rfl ``` Then, executing `simp [forIn]` in a term containing `forIn` iterating over a `List` may cause nontermination since the theorem above will fold it again. Remark: the reduction strategy implemented leanprover/lean4#3118 triggers nontermination.
|
Why wasn't this already nonterminating before? |
|
In general this seems like it will be a problem with any use of simp lemmas for re-folding an unfolded notation, e.g. |
|
I noticed these lemmas also had non-terminal simp, so I went ahead and cleaned that up. I think there are a ways this could be improved. Ultimately, I think it'd be nice if we had some sort of simp modulo some limited equations so that, for example, |
Using
simp [forIn]may cause nontermination with differentsimpreduction strategies. We have the following theoremThen, executing
simp [forIn]in a term containingforIniterating over aListmay cause nontermination since the theorem above will fold it again.Remark: the reduction strategy implemented
leanprover/lean4#3118 triggers the nontermination.