Trinh Le Khanh (Jun 19 2022 at 13:01): Trinh Le Khanh (Jun 19 2022 at 13:01):Hi all,
I have a question about proving a formula on finite sets. Isabelle can prove if I define specific sets (sets with particular values) and then write the formula.
definition p_list :: "nat list" where
"p_list = [1::nat,2,3,4]"
definition q_list :: "nat list" where
"q_list = [1::nat,2,3]"
lemma compare_1: "(∀i∈set(p_list).(P(i) ⟶
(∃j∈ set(q_list).
(Q(j) ∧ (∀j1 ∈ set(q_list)-{j}. ¬Q(j1)))
)
)
∧ ((∀i∈ set(p_list). P(i) ⟶ (∀i1 ∈ set(p_list)-{i}. ¬P(i1)))
∧ (∀j∈ set(q_list). Q(j) ⟶ (∀j1 ∈ set(q_list)-{j}. ¬Q(j1)))))
⟷ (∃i∈ set(p_list).∃j∈ set(q_list).((P(i) ⟶ Q(j))
∧ (∀i1∈set(p_list)-{i}.¬P(i1)) ∧ (∀j1∈set(q_list)-{j}.¬Q(j1))))"
unfolding p_list_def q_list_def
by (smt (z3) DiffD1 DiffI insert_iff list.set(2) singletonD)
Isabelle cannot prove if I write the lemma with generic set definitions (even if I limited the cardinality).
lemma test_general:
fixes p_list::"nat list"
fixes q_list::"nat list"
assumes "card (set p_list) < 3" and "card (set q_list) < 3" and "card (set p_list) > 1" and "card (set q_list) > 1"
shows "(∀i∈set(p_list).(P(i) ⟶
(∃j∈ set(q_list).
(Q(j) ∧ (∀j1 ∈ set(q_list)-{j}. ¬Q(j1)))
)
)
∧ ((∀i∈ set(p_list). P(i) ⟶ (∀i1 ∈ set(p_list)-{i}. ¬P(i1)))
∧ (∀j∈ set(q_list). Q(j) ⟶ (∀j1 ∈ set(q_list)-{j}. ¬Q(j1)))))
⟷ (∃i∈ set(p_list).∃j∈ set(q_list).((P(i) ⟶ Q(j))
∧ (∀i1∈set(p_list)-{i}.¬P(i1)) ∧ (∀j1∈set(q_list)-{j}.¬Q(j1))))"
sledgehammer
Could you explain why and give me some advice to deal with it, please?
Wenda Li (Jun 19 2022 at 13:20):To me, the latter lemma is much harder...
With concrete lists (e.g., p_list = [1::nat,2,3,4]), propositions involving ∀i∈set(p_list) ... can be proved by unfolding/enumerating all possible values, which is in general easier for automatic theorem provers. In comparison, card (set p_list) < 3 gives us infinitely many possible p_list even though we know its length is less than 3, which makes the reasoning on "for all" and "exists" much more challenging.
Trinh Le Khanh (Jun 19 2022 at 13:40):So you mean even if I limited the cardinality is 2 but the concrete value would unpredictable (e.g., {1,2}, {200,5000}, etc.)?
Is there any way to guide Isabelle to compute the random values for p_list first, then invoke them from the formula?
Trinh Le Khanh (Jun 19 2022 at 13:51):I created a function to generate a list with concrete values and use it in the lemma, but it's still unprovable
fun finite_set_with_card_eq :: "nat ⇒ nat list" where
"finite_set_with_card_eq 0 = []" |
"finite_set_with_card_eq k = [k] @ finite_set_with_card_eq (k-1)"
value "finite_set_with_card_eq 5"
lemma test_general:
fixes p_list::"nat list"
fixes q_list::"nat list"
assumes "p_list = finite_set_with_card_eq 3" and "q_list = finite_set_with_card_eq 3"
shows "(∀i∈set(p_list).(P(i) ⟶
(∃j∈ set(q_list).
(Q(j) ∧ (∀j1 ∈ set(q_list)-{j}. ¬Q(j1)))
)
)
∧ ((∀i∈ set(p_list). P(i) ⟶ (∀i1 ∈ set(p_list)-{i}. ¬P(i1)))
∧ (∀j∈ set(q_list). Q(j) ⟶ (∀j1 ∈ set(q_list)-{j}. ¬Q(j1)))))
⟷ (∃i∈ set(p_list).∃j∈ set(q_list).((P(i) ⟶ Q(j))
∧ (∀i1∈set(p_list)-{i}.¬P(i1)) ∧ (∀j1∈set(q_list)-{j}.¬Q(j1))))"
sledgehammer
Even in this case, Sledgehammer still needs to figure out a way to prove p_list = [3, 2, 1] first, which itself involves non-trivial rewriting rules. Sledgehammer itself is not yet smart enough to do that right now.
We can try to treat Sledgehammer as a black box, if it fails we can then simplify the problem manually and throw it to Sledgehammer again:
fun finite_set_with_card_eq :: "nat ⇒ nat list" where
"finite_set_with_card_eq 0 = []" |
"finite_set_with_card_eq k = [k] @ finite_set_with_card_eq (k-1)"
lemma test_general:
fixes p_list::"nat list"
fixes q_list::"nat list"
assumes "p_list = finite_set_with_card_eq 3" and "q_list = finite_set_with_card_eq 3"
shows "(∀i∈set(p_list).(P(i) ⟶
(∃j∈ set(q_list).
(Q(j) ∧ (∀j1 ∈ set(q_list)-{j}. ¬Q(j1)))
)
)
∧ ((∀i∈ set(p_list). P(i) ⟶ (∀i1 ∈ set(p_list)-{i}. ¬P(i1)))
∧ (∀j∈ set(q_list). Q(j) ⟶ (∀j1 ∈ set(q_list)-{j}. ¬Q(j1)))))
⟷ (∃i∈ set(p_list).∃j∈ set(q_list).((P(i) ⟶ Q(j))
∧ (∀i1∈set(p_list)-{i}.¬P(i1)) ∧ (∀j1∈set(q_list)-{j}.¬Q(j1))))"
proof -
have *:"p_list = [3, 2, 1]" "q_list = [3, 2, 1]"
unfolding assms by eval+
show ?thesis
unfolding *
by (smt (z3) DiffE DiffI insert_iff list.set(2) singletonD)
qed
I see. Thank you very much for your help.
Notification Bot (Jun 19 2022 at 15:38):Trinh Le Khanh has marked this topic as resolved.
Last updated: Apr 19 2024 at 16:20 UTC