obtaining elements of a small set · Beginner Questions

"... The sets H and K overlap, and the overlap contains at least three points. Let A, B, and C denote three points in that overlap, and consider the lines AB and BC..."

I tried saying something like this in Isabelle and had troubles, and trimmed it down to this example:

lemma xx:
  fixes U::"nat set"
  assumes a: "card U ≥ 3"
  shows "True"
proof -
  obtain A B where "A ∈ U ∧ B ∈ U  ∧ A ≠ B" using a ...

(The lemma was just a way to let me get into the middle of a proof; I didn't really need to prove True.)

 by (smt (verit, ccfv_SIG) Suc_le_mono antisym ex_card le_add2 nat.simps(3) numeral_3_eq_3 plus_1_eq_Suc subset_iff)

  obtain A B where "A ∈ U ∧ B ∈ U  ∧ distinct [A, B]" using a by sledgehammer

(* vampire, > 1.0 s *)

  by (metis Suc_le_mono all_not_in_conv antisym bot_least bot_nat_0.extremum card.empty card_Suc_eq distinct_length_2_or_more distinct_singleton insertI1 insert_subset
      numeral_3_eq_3 subsetI zero_neq_numeral)


(* Isar proof, 157 msec *)
proof -
  assume a1: "⋀A B. A ∈ U ∧ B ∈ U ∧ distinct [A, B] ⟹ thesis"
  obtain NN :: "nat set ⇒ nat ⇒ nat set" and NNa :: "nat set ⇒ nat ⇒ nat set" where
    f2: "∀N n. NN N n ⊆ N ∧ card (NN N n) = n ∨ ¬ n ≤ card N"
    by (metis (no_types) ex_card)
  obtain nn :: "nat set ⇒ nat set ⇒ nat" and nna :: "nat set ⇒ nat set ⇒ nat" where
    f3: "∀N Na. ((∀n. n ∈ Na ∨ n ∉ N) ∨ ¬ N ⊆ Na) ∧ (N ⊆ Na ∨ nn N Na ∉ Na ∧ nn N Na ∈ N)"
    by (metis (no_types) subset_iff)
  have f4: "3 ≠ 0"
    by simp
  have f5: "∀n. ¬ 3 ≤ Suc n ∨ Suc (Suc 0) ≤ n"
    by presburger
  have f6: "∀n. ¬ (n::nat) ≤ 0 ∨ 0 = n"
    by blast
  have f7: "∀n. Suc n ≤ 3 ∨ ¬ n ≤ Suc (Suc 0)"
    by (simp add: numeral_3_eq_3)
  have "∀n. ¬ n ≤ 0 ∨ 3 = Suc (Suc (Suc n))"
    by force
  moreover
  { assume "∃N Na. nn U Na ∈ N ∧ ¬ U ⊆ N ∧ ¬ U ⊆ Na"
    then have "∃n na. na ∈ U ∧ n ≠ na ∧ n ∈ U"
      using f3 by (metis (no_types)) }
  moreover
  { assume "∃N n Na. n ∉ Na ∧ ¬ Na ⊆ N ∧ ¬ Na ⊆ N ∧ Na ⊆ U ∧ n ∈ U"
    then have "∃n na. na ∈ U ∧ n ≠ na ∧ n ∈ U"
      using f3 by (metis (full_types)) }
  ultimately show ?thesis
    using f7 f6 f5 f4 f3 f2 a1 by (smt (z3) Suc_le_mono assms bot_nat_0.extremum distinct_length_2_or_more distinct_singleton nat.simps(3) order_antisym_conv)
qed

Not surprisingly, given how long these took, trying to generalize to get three distinct items from U was hopeless -- sledgehammer gave up.

Is there some more idiomatic way to do this kind of thing? I'll soon be doing something with 10 points (although I think I only need to extract 4 of them, and then can construct the others), and it's clear that what I've been doing won't suffice for that task.

Mathias Fleury (Jun 22 2025 at 13:45):

Something like that? It is not exactly pretty… (the lemma helper can for sure be proven better, but I did not care about that lemma)

lemma helper:
  ‹card U > numeral n ⟹ numeral n ≥ (0::nat) ⟹ ∃x U'. U = insert x U' ∧ x ∉ U' ∧ card U' > pred_numeral n›
  ‹card U > Suc 0 ⟹ ∃x U'. U = insert x U' ∧ x ∉ U' ∧ card U' > 0›
  ‹card U > 0 ⟹ ∃x U'. U = insert x U' ∧ x ∉ U'›
  apply (cases U rule: finite.cases)
  using card_ge_0_finite[of U]
  apply (auto dest!: )[]
  apply (auto dest: card_ge_0_finite)[]
  apply (auto dest: card_ge_0_finite)
    apply (metis Set.set_insert card_insert_if finite_insert insertCI less_numeral_Suc)
  apply (metis Suc_less_eq2 card_eq_SucD)
  by (meson card_le_Suc_iff less_eq_Suc_le)



lemma xx:
  fixes U::"nat set"
  assumes a: "card U > 5"
  shows "True"
proof -
  obtain A B C D E where "A ∈ U ∧ B ∈ U  ∧C ∈ U ∧ D ∈ U  ∧ E ∈ U ∧
         distinct [A, B, C, D, E]" using a
    using card_ge_0_finite[of U]
    apply (auto dest!: helper simp: )
    by blast

John Hughes (Jun 22 2025 at 14:49):

Gosh. It took me a while to even parse the theorem statement, as I thought that ‹card U > contained an open-close cartouche pair!

I've been trying to do everything in Isar, and maybe this is one of those places where you really need to move to "assembly language" and write apply scripts, but I'd hate to think so.

Mathias Fleury (Jun 22 2025 at 14:52):

John Hughes (Jun 22 2025 at 14:55):

Hmmm. I wish that I knew of a resource on how to translate apply-scripts to become Isar. I guess I'll spend some time trying to do it myself, but I'm not optimistic :( .

Mathias Fleury (Jun 22 2025 at 15:02):

lemma helper:
  ‹card U > numeral n ⟹ numeral n ≥ (0::nat) ⟹ ∃x U'. U = insert x U' ∧ x ∉ U' ∧ card U' > pred_numeral n›
  ‹card U > Suc 0 ⟹ ∃x U'. U = insert x U' ∧ x ∉ U' ∧ card U' > 0›
  ‹card U > 0 ⟹ ∃x U'. U = insert x U' ∧ x ∉ U'›
proof -
  show p1: ‹∃x U'. U = insert x U' ∧ x ∉ U' ∧ card U' > pred_numeral n›
    if H: ‹card U > numeral n› ‹numeral n ≥ (0::nat)›
    by (metis card_le_Suc_iff less_eq_Suc_le numeral_eq_Suc that(1))
  show
    ‹card U > Suc 0 ⟹ ∃x U'. U = insert x U' ∧ x ∉ U' ∧ card U' > 0›
    by (meson card_le_Suc_iff less_eq_Suc_le)
  show
    ‹card U > 0 ⟹ ∃x U'. U = insert x U' ∧ x ∉ U'›
    by (metis card_gt_0_iff ex_in_conv mk_disjoint_insert)
qed

John Hughes (Jun 22 2025 at 15:55):

Manuel Eberl (Jun 24 2025 at 13:39):

One trick I often do is to go through lists. There is a lemma that tells you that if you have a set A with cardinality n then there exists a list xs of length n with no repeated elements such that set xs ⊆ A.

notepad
begin
  fix A :: "'a set"
  assume card_A: "finite A" "card A ≥ 3"
  obtain xs where xs: "length xs = 3" "distinct xs" "set xs ⊆ A"
    using card_A
    by (metis distinct_card finite_distinct_list obtain_subset_with_card_n)
  obtain a b c where xs_eq: "xs = [a, b, c]"
    using xs by (auto simp: length_Suc_conv eval_nat_numeral)
  have abc: "a ≠ b" "a ≠ c" "b ≠ c" "a ∈ A" "b ∈ A" "c ∈ A"
    using xs xs_eq by auto
end

One could potentially write some automation for this sort of thing. But I'm not sure if it's worth it.

Stream: Beginner Questions

Topic: obtaining elements of a small set