## Stream: Beginner Questions

### Topic: prove a formulae on a finite set

#### 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
``````

Last updated: Jul 15 2022 at 23:21 UTC