When working with datatypes, and writing theorems involving subterms, I often have to carefully expand subterm at precise positions in my proofs, which make them less automated and more fragile. I believe the following things could be really useful for users working with subterms of datatypes:
Having a subterm transitivity lemma for free (in the generated declarations) that goes as follows : subterm_transitivity: LEMMA ∀ e1, e2, e3 : subterm(e1, e2) ∧ subterm(e2, e3) ⇒ subterm(e1, e3). The proof is doable by induction but cumbersome.
Having a set of rewrite lemmas for subterm (that could be used as auto-rewrites) for each of the constructors, to facilitate the proof work. Adding subterm as a rewrite unfolds too much, as the case analysis is not at top level.
Concretely, this would mean that for a given datatype:
my_datatype: DATATYPE
BEGIN
base_case(t:T): base_case
unary_case(u1: my_datatype): unary_case?
binary_case(u1, u2: my_datatype): binary_case?
END my_datatype
One would get for free the following (in addition to all the automatically generated)
When working with datatypes, and writing theorems involving subterms, I often have to carefully expand
subterm
at precise positions in my proofs, which make them less automated and more fragile. I believe the following things could be really useful for users working with subterms of datatypes:subterm_transitivity: LEMMA ∀ e1, e2, e3 : subterm(e1, e2) ∧ subterm(e2, e3) ⇒ subterm(e1, e3)
. The proof is doable by induction but cumbersome.subterm
as a rewrite unfolds too much, as the case analysis is not at top level.Concretely, this would mean that for a given datatype:
One would get for free the following (in addition to all the automatically generated)
And the user could add the rewrites to his theory, saving himself a lot of
expand
s(This might be doable by changing the definition of
subterm
and adding it as rewrite, but it would not be retro-compatible I guess.)I believe that could be a great addition to the (already very rich) datatype feature!