Stream: Beginner Questions

Topic: prove a formulae on a finite set

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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