Menu
▾
▴
#397 Improve induction hypothesis
Assume that we have an inductive datatype which recursive argument is based on another parametric datatype, e.g.: NTree(E) = Empty | Node(val : E, children : List(NTree(E)))
When doing an induction on such a tree, there is no induction hypothesis in the Node case and the user is asked to prove P(Node(val, children)) without knowing that P is true on the children.
In that case, the reasoner should generate an hypothesis that says something like: children∈List({e ∣ e ∈ E ∧ P(e)}) instead of children∈List(E).
This was reported by Guillaume Dupont.
It is unclear if the suggested induction hypothesis is actually valid in all cases.
Moreover, even if we could do an induction on such datatypes, they are not very useful in practice since there is currently no plug-in supporting mutually recursive operators on datatypes.
We will reconsider this problem in a future version.