Yannick Stade (Jul 13 2023 at 06:19): Yannick Stade (Jul 13 2023 at 06:19):In our theory, we encountered some differences between using by (cases …; auto) and by (cases …) auto to prove a statement. In many cases, the former option is considerably slower and in one case, the first option even fails to terminate. From the specification (p. 145 and p. 148), we understood that, in this case, they should do the same; apparently, we are wrong. Can you tell us the difference and why the second option is faster? Below we created a minimal working example demonstrating this issue.
theory MWE
imports Main
begin
datatype ('a) t = A 'a
fun set_of_list where
"set_of_list [] = {}"
| "set_of_list (A x # xs) = insert x (set_of_list xs)"
lemma
assumes "xs = ys @ zs"
shows "set_of_list xs = set_of_list ys ∪ set_of_list zs"
using assms
proof (induction ys arbitrary: xs zs)
case Nil
then show ?case by simp
next
case (Cons y ys)
then show ?case by (cases y) auto
(* Why can the proof method not be replaced with `(cases y; auto)`? *)
qed
end
Weird. simp_trace_new tells you exactly why it behaves differently… but I have no idea why
Mathias Fleury (Jul 13 2023 at 06:27):Ah nothing magic here: the issue is that you are relying on the order in which the simplification happens
Mathias Fleury (Jul 13 2023 at 06:28):And the user is responsible of taking care that the rewrite system is confluent
Mathias Fleury (Jul 13 2023 at 06:29):Other examples are differences between simp add: XXX and marking XXX as [simp].
Yannick Stade (Jul 13 2023 at 06:31):Ah, okay, this explains the differences. Thank you!
Hanno Becker (Aug 08 2023 at 06:02):(EDIT: I posted something as an answer here which was meant as a new topic)
Last updated: May 04 2024 at 16:18 UTC