Proof of mirrored binary trees · Beginner Questions

Hello again. When proving with Isabelle, I came across an issue of a simplification rule getting in the way of proving my main lemma "mirror_proof". If I delete the bolded code below, I get errors on proofs leading up to mirror_proof but mirror_proof can complete successfully but if I leave it in, apply(auto) at mirror_proof becomes purple and subsequently red (Meaning it's failed I presume?). Is there any way I can prevent Isabelle from using a certain rule when proving a lemma?

fun mirror :: "'a tree ⇒ 'a tree" where
"mirror Tip = Tip" |
"mirror (Node l a r ) = Node (mirror r ) a (mirror l)"

**lemma reverse_simp [simp] : "reverse (snoc ys y) = Cons y (reverse ys)"
apply(induction ys)
apply(auto)
done**

lemma mirror_simp [simp]: "Cons x (reverse xs) = (reverse (snoc xs x))"
apply(induction xs)
apply(auto)
done

lemma mirror_simp__3 [simp]: "snoc ys y = app ys (Cons y Nil)"
apply(induction ys)
apply(auto)
done

lemma app_distributivity [simp]: "app (app ys xs) zs = app ys (app xs zs)"
apply(induction ys)
apply(auto)
done

lemma app_distributivity_v2 [simp]: "xs = app xs Nil"
apply(induction xs)
apply(auto)
done

lemma mirror_simp_distributive [simp]: "reverse (app xs ys) = app (reverse ys) (reverse xs)"
apply(induction xs)
apply(auto)
done

lemma mirror_proof : "pre_order (mirror t) = reverse (post_order t)"
apply(induction t)
apply(auto)
done

Mathias Fleury (Sep 18 2023 at 04:53):

In general: auto applies simp rules from left to right, so the right-hand side should be easier than the left-hand side

Mathias Fleury (Sep 18 2023 at 04:54):

Wolfgang Jeltsch (Sep 18 2023 at 13:06):

Regarding Zulip communication: @Abu, could you please prepend and append a line with three backticks to your code blocks? This way they get typeset as code, even with syntax highlighting. Putting code in posts as mere text makes your posts harder to read.

Alex Weisberger (Sep 19 2023 at 20:28):

Probably the most straightforward answer is to manually remove a rule with del:

apply(simp del: reverse_simp)

Another option is to remove the [simp] declarations from your lemmas. This adds them a simplification rules, and by omitting that they won't automatically be added to the simp set (set of all simplification rules). That effectively will require you to opt in to them.

Another option is to use less powerful tactics. simp and auto are very powerful. This is great for effort, but not so great for control. You can apply inference rules directly with rule, erule, drule etc. Chapter 5 in the Isabelle tutorial has a ton of information there.

Wolfgang Jeltsch (Sep 19 2023 at 20:34):

Disclaimer: The Isabelle tutorial is considered “old”, meaning not everything there is recommended to be followed or even applies still. Generally, the prog-prove tutorial is to be preferred, but it is true that it doesn’t go very much into the lower-level proof methods, those that give you more control.

Alex Weisberger (Sep 19 2023 at 20:46):

Yea unfortunately prog-prove is ~1/4 the size of the tutorial. There's just a lot more info in the tutorial - I wonder if there's any plans to revitalize it.

Stream: Beginner Questions

Topic: Proof of mirrored binary trees