Currently, reasoners support on inductive types is basically limited to induction and distinct case.
Several other ones would be very useful, such as:
- injectivity of constructors (e.g., C(x)=C(y) implies x=y)
- constructors form a partition of the datatype (and therefore Nil∈List(T) and Nil≠Cons(h, t) for example, for the usual List datatype)
- set membership of constructors arguments (e.g., Cons(h, t)∈List(ℕ) implies h∈ℕ and t∈List(ℕ), which is currently provable through some clever use of ah and distinct case, but is cumbersome)
The last case could also be part of the generalized modus ponens reasoner, as it is quite necessary to perform inductive proofs.
The suggested rules have either been directly implemented or are now easily provable. The changes have been merged in commit [160fb8].
Related
Commit: [160fb8]