Struggling with a trivial set equality · Beginner Questions

I am struggling with a function ("cut") where for some reason I cannot use its definition in my proofs.

(* I do not believe this definition is needed but I write it here for completeness *)
definition cols :: "('a * 'b) set set  ⇒ 'a set" where
  "cols R = { n | n r. r ∈ R ∧ (∃ v. (n, v) ∈ r) }"

definition cut :: "('a * 'b) set ⇒ ('a * 'b) set set ⇒ ('a * 'b) set set ⇒ ('a * 'b) set" where
  "cut r1 R1 R2 = { (n, v) | n v. (n, v) ∈ r1 ∧ n ∈ (cols R1 - cols R2) }"

lemma "cut r1 R1 {} = { (n, v) | n v. (n, v) ∈ r1 ∧ n ∈ (cols R1 - cols {}) }"
  apply(simp add: cut_def[of "r1" "R1" "{}"])

"cut r1 R1 {} =
 { (n, v) | n v. (n, v) ∈ r1 ∧ n ∈ (cols R1 - cols {}) }"

"{(n, v). (n, v) ∈ r1 ∧ n ∈ cols R1 ∧ n ∉ cols {}} =
  {(n, v). (n, v) ∈ r1 ∧ n ∈ cols R1 ∧ n ∉ cols {}}"

which to me seems trivial ("a = a"), but I can't make it to work (I am trying blast, fastforce, auto, .. nothing works)
What rule do I need to use to finish this goal? What am I missing?

ZDHKLV (Jan 15 2025 at 09:30):

I just found out that applying the rule "cols {} = {}" (proved by auto) makes my proof succeed. Why is it required when I was clearly dealing with "a = a" to begin with?

Mathias Fleury (Jan 15 2025 at 09:44):

lemma "cut r1 R1 {} = { (n, v) | n v. (n, v) ∈ r1 ∧ n ∈ (cols R1 - cols {}) }"
  apply(simp add: cut_def[of "r1" "R1" "{}"])
  supply [[unify_trace_failure]]
  apply (rule refl)
(*
The following types do not unify:
('a × 'b) set set ⇒ 'a set
('a × 'c) set set ⇒ 'a set
*)

Mathias Fleury (Jan 15 2025 at 09:45):

If you control-hover over the colsin your theory file, you will see where the 'c is

Mathias Fleury (Jan 15 2025 at 09:46):

Kevin Kappelmann (Jan 15 2025 at 09:51):

Your goal isn't a=a if you check the types. The type of the first {} is 'a x 'b set set while the type of the second one is 'a x 'c set set since Isabelle infers the most general types. Unfortunately, Isabelle doesn't print the type of {} even if you use declare [[show_types]]. Mathias showed you a nice way to use the unifier to find the mismatch though.

Now it is up to you to decide whether you actually want the second {} to be of the same type as the first one or you provide the equation cols {} = {} as an additional rule to close the goal while keeping the types as they are.

Kevin Kappelmann (Jan 15 2025 at 09:54):

If you really want to see the complete goal including all types, you can use this:

declare[[show_types,show_sorts,ML_print_depth=10000]]
lemma "cut r1 R1 {} = { (n, v) | n v. (n, v) ∈ r1 ∧ n ∈ (cols R1 - cols {}) }"
  apply(simp add: cut_def[of "r1" "R1" "{}"])
ML_command ‹
  @{Isar.goal} |> #goal |> Thm.full_prop_of |> @{print}
›

ZDHKLV (Jan 15 2025 at 10:01):

It makes perfect sense! Thank you very much to the both of you and thank you for the tips to print the types!

Stream: Beginner Questions

Topic: Struggling with a trivial set equality