David Wang (Dec 04 2023 at 23:50): David Wang (Dec 04 2023 at 23:50):I have spent way too much time attempting to prove the following lemma without using an induction, i.e. directly or by contradiction. Could someone help me out?
datatype 'a tree = Leaf | Node "'a tree" 'a "'a tree"
fun tree_set where
"tree_set Leaf = {}"
| "tree_set (Node l a r) = insert a (tree_set l) ∪ (tree_set r)"
fun bst where
"bst Leaf = True"
| "bst (Node l a r) = ((∀x∈tree_set l. x < a) ∧ bst l ∧ (∀x∈tree_set r. a < x) ∧ bst r)"
fun add_tree:: "nat tree ⇒ nat" where
"add_tree Leaf = 0" |
"add_tree (Node l n r) = add_tree l + n + add_tree r"
lemma
shows "⟦bst t; add_tree t = 0⟧ ⟹ t = Leaf ∨ t = Node Leaf 0 Leaf"
proof (rule ccontr)
assume b: "bst t"
assume a: "add_tree t = 0"
assume as: "¬ (t = Leaf ∨ t = Node Leaf 0 Leaf)"
then obtain l n r where
s: "t = Node l n r" and
t: "l ≠ Leaf ∨ r ≠ Leaf ∨ n ≠ 0" (* does this step necessarily need an induction? *)
by (induction t, auto)
(* the rest of this attempt consists of a few applications of (cases ...) *)
it seems to me that one reason you will need induction is that it's not immediately obvious add_tree t = 0 implies all elements in the tree_set are 0
ah I'm wrong, this works as a direct proof by case splitting, not sure if it's what you want:
lemma
shows "⟦bst t; add_tree t = 0⟧ ⟹ t = Leaf ∨ t = Node Leaf 0 Leaf"
apply (cases t; simp)
subgoal for x y
apply (cases x)
apply (cases y)
by auto
Thank you
Last updated: Apr 28 2024 at 01:11 UTC