isauser (Nov 20 2025 at 05:21): isauser (Nov 20 2025 at 05:21):While working through "Concrete Semantics", I discovered a very confusing scenario where automation works well or breaks completely depending on how you arrange the arguments. To demonstrate, given these definitions:
datatype alpha = a | b
inductive T :: "alpha list ⇒ bool" where
"T []" |
"T w⇩1 ⟹ T w⇩2 ⟹ T (w⇩1 @ a # w⇩2 @ [b])"
The following lemma cannot be proven automatically:
lemma "T w⇩1 ⟹ T w⇩2 ⟹ T (w⇩1 @ w⇩2)"
try (* "No proof found, Tried in vain" *)
Whereas if you swap the order of arguments in the conclusion, sledgehammer finds the solution instantly, and the previous lemma can now be trivially proved as well:
lemma T_append: "T w⇩1 ⟹ T w⇩2 ⟹ T (w⇩2 @ w⇩1)"
apply(induction rule: T.induct)
apply simp
apply(metis T.intros(2) append_assoc)
done
lemma "T w⇩1 ⟹ T w⇩2 ⟹ T (w⇩1 @ w⇩2)"
by(simp add: T_append)
Why does this happen? Is there some sort of a rule I should follow to avoid this in the future?
Mathias Fleury (Nov 20 2025 at 05:40):Neither version can be proven without T_append
Mathias Fleury (Nov 20 2025 at 05:40):And proving T_append is very hard, because the solvers do not do induction
isauser (Nov 20 2025 at 05:59):Neither version can be proven without
T_append
I'm not sure I understand. This is T_append:
lemma T_append: "T w⇩1 ⟹ T w⇩2 ⟹ T (w⇩2 @ w⇩1)"
apply(induction rule: T.induct)
apply simp
try
The try statement immediately finds several proofs. But then if you state this lemma slightly differently:
lemma T_append: "T w⇩1 ⟹ T w⇩2 ⟹ T (w⇩1 @ w⇩2)"
apply(induction rule: T.induct)
apply simp
try
The automation breaks completely. The order of the arguments shouldn't matter, but for some reason it does, and I don't understand why.
Mathias Fleury (Nov 20 2025 at 06:11):The order matters
Mathias Fleury (Nov 20 2025 at 06:11):you are not doing induction on the same variable
isauser (Nov 20 2025 at 06:13):Ah, thank you - it's clear to me now.
Mathias Fleury (Nov 20 2025 at 06:15):BTW: I briefly tried to do a proof by hand, but I failed because the induction principle does not apply
Mathias Fleury (Nov 20 2025 at 06:15):It might be possible but I don't see it
Last updated: Dec 08 2025 at 08:34 UTC