Stream: Beginner Questions

Topic: Improving Binary Decision Diagram Proof

view this post on Zulip o7 (Dec 13 2024 at 15:54):

I have the following isabelle code below

theory sec24
  imports Main
begin
datatype bdd = Leaf bool | Branch bdd bdd

primrec eval :: "(nat ⇒ bool) ⇒ nat ⇒ bdd ⇒ bool" where
"eval f n (Leaf x) = x" |
"eval f n (Branch left right) = (if f n then eval f (Suc n) right else eval f (Suc n) left)"

primrec bdd_unop :: "(bool ⇒ bool) ⇒ bdd ⇒ bdd" where
"bdd_unop f (Leaf x) = Leaf (f x)" |
"bdd_unop f (Branch left right) = Branch (bdd_unop f left) (bdd_unop f right)"

primrec bdd_binop :: "(bool ⇒ bool ⇒ bool) ⇒ bdd ⇒ bdd ⇒ bdd" where
"bdd_binop f (Leaf x) t2 = bdd_unop (f x) t2" |
"bdd_binop f (Branch left right) t2 = (case t2 of
  Leaf x ⇒ Branch (bdd_binop f left t2) (bdd_binop f right t2)
| Branch left2 right2 ⇒ Branch (bdd_binop f left left2) (bdd_binop f right right2))"

theorem t1: "g (eval f n t) = eval f n (bdd_unop g t)"
  apply (induct t arbitrary: n)
   apply auto
  done

lemma l1: "eval f n (bdd_unop ((=) (eval f n t)) t)"
  apply (induct t arbitrary: n)
   apply auto
  done

lemma l2: "bdd_binop g t (Leaf y) = bdd_unop (λ x. g x y) t"
  apply (induct t)
   apply auto
  done

lemma l3: "If True (eval e (Suc i) b12) = (λ _. (eval e (Suc i) b12))"
  apply auto
  done

theorem t2: "∀ i b2. eval e i (bdd_binop f b1 b2) = f (eval e i b1) (eval e i b2)"
  apply (induct b1)
   apply (auto simp: t1 l1)
  apply (case_tac b2)
   apply (auto simp: If_def l2)
    apply (case_tac "e i")
     apply (auto simp: l3)
  using t1 apply auto
   apply (case_tac "e i")
  by (auto simp: the_equality)
end

Context: I'm working through some exercises on binary decision trees and I saw that the solution for theorem t2 was much simpler than mine, but it doesn't work, possibly due to changes in isabelle since 2012.

I would like to know if I can optimise the proof of theorem t2 such that less lines are used, and less time is taken to process each application.

As for my thought process, I mainly observed each subgoal in order to define each lemma above, then used sledgehammer in places where I believed the goal could be intuitively achieved without introducing additional lemmas. I then simplified the sledgehammer lines. Could I please also have some advice on this too?

view this post on Zulip Mathias Fleury (Dec 13 2024 at 16:00):

theorem t2: "eval e i (bdd_binop f b1 b2) = f (eval e i b1) (eval e i b2)"
  apply (induct b1 arbitrary:  i b2)
   using t1 apply (auto simp: l1 split: bdd.splits if_splits)
  done

view this post on Zulip o7 (Dec 13 2024 at 16:02):

Thanks Mathias. Since I haven't seen the split argument in the auto tactic yet, could you lmk how it works?
lmao it's in prog-prove, please disregard. Sorry. Will ask further if necessary.

view this post on Zulip Mathias Fleury (Dec 13 2024 at 16:05):

theorem t2: "eval e i (bdd_binop f b1 b2) = f (eval e i b1) (eval e i b2)"
by (induct b1 arbitrary: i b2)
(use t1 in ‹auto simp: l1 split: bdd.splits if_splits›

view this post on Zulip Mathias Fleury (Dec 13 2024 at 16:09):

but it is a bit of magic

view this post on Zulip o7 (Dec 13 2024 at 16:33):

Turns out you don't need if_splits

theorem t2'': "eval e i (bdd_binop f b1 b2) = f (eval e i b1) (eval e i b2)"
  apply (induct b1 arbitrary: i b2)
  using t1 apply (auto simp: l1 split: bdd.splits)
   done

very interesting.

Last updated: Dec 21 2024 at 16:20 UTC