Stream: Beginner Questions

Topic: A "cases"-like construction that works through a small set

John Hughes (Apr 25 2024 at 21:16):

I'm trying to show something about a small example; I have a set of 4 "points" and 6 "lines" -- each line consists of two of the points. I'd like to prove something about all six lines, and I'd like to do it by considering them one at a time. I haven't found a "cases" variant that lets me do this. Here's the setup and the place where I get stuck, marked with a comment.

theory AffineExample
  imports Complex_Main
    begin

datatype a4pt = Pa | Qa | Ra | Sa
definition  "A4Points = {Pa, Qa, Ra, Sa}"
definition "A4PQ = {Pa, Qa}"
definition "A4PR = {Pa, Ra}"
definition "A4PS = {Pa, Sa}"
definition "A4QR = {Qa, Ra}"
definition "A4QS = {Qa, Sa}"
definition "A4RS = {Ra, Sa}"

definition "A4Lines = {A4PQ, A4PR, A4PS, A4QR, A4QS, A4RS}"

fun parallel::"a4pt set ⇒ a4pt set ⇒ bool" where
"parallel l m  =  (if (l ∈ A4Lines ∧ m ∈ A4Lines)
  then l = m ∨ (l ∩ m = {}) else undefined)"

fun A4complement::"a4pt set ⇒ a4pt set" where
"A4complement n = (if n = A4PQ then A4RS else
(if n = A4RS then A4PQ else
(if n = A4PR then A4QS else
(if n = A4QS then A4PR else
(if n = A4PS then A4QR else
(if n = A4QR then A4PS else
undefined))))))"

lemma A4complement_parallel:
  fixes n
  assumes "n ∈ A4Lines"
  shows "parallel (A4complement n) n"
  sorry
(* I'd like to say "let's consider each possible value of n, namely A4PQ, A4PR, A4PS, etc" and show the conclusion
for each of these, i.e., do a "cases" on the enumerated values in the set A4Lines. *)

end

Any suggestions on a clean way to do such a proof?

NB: There are probably better ways to do the overall proof than by considering cases, but I'm asking about this approach because sometimes, in the work I'm doing, a plug-n-chug kind of approach really does make sense, so I really am interested in the question I asked. If you have a great alternative approach to the proof, I'd love to see it, of course, but my main question is about this kind of case-construction.

Kevin Kappelmann (Apr 26 2024 at 07:33):

You can also make your lines a datatype and give an interpretation function points. Then everything is much simpler:
(and I added proper intro and elim rules for your parallel definition)

datatype a4pt = Pa | Qa | Ra | Sa
datatype a4line = A4PQ | A4PR | A4PS | A4QR | A4QS | A4RS

fun points :: "a4line ⇒ a4pt set" where
  "points A4PQ = {Pa, Qa}"
| "points A4PR = {Pa, Ra}"
| "points A4PS = {Pa, Sa}"
| "points A4QR = {Qa, Ra}"
| "points A4QS = {Qa, Sa}"
| "points A4RS = {Ra, Sa}"

definition "parallel l m ≡ l = m ∨ (points l ∩ points m = {})"

lemma parallel_self [iff]: "parallel l l"
  unfolding parallel_def by simp

lemma parallel_if_points_inter_eq_emptyI [intro]:
  assumes "points l ∩ points m = {}"
  shows "parallel l m"
  using assms unfolding parallel_def by simp

lemma parallelE [elim]:
  assumes "parallel l m"
  obtains (eq) "l = m" | (disjoint) "points l ∩ points m = {}"
  using assms unfolding parallel_def by auto

fun A4complement::"a4line ⇒ a4line" where
  "A4complement A4PQ = A4RS"
| "A4complement A4RS = A4PQ"
| "A4complement A4PR = A4QS"
| "A4complement A4QS = A4PR"
| "A4complement A4PS = A4QR"
| "A4complement A4QR = A4PS"

lemma A4complement_parallel:
  shows "parallel (A4complement n) n"
  by (cases n) auto

I'd also recommend using something other than sets if points should always return exactly two points.

John Hughes (Apr 26 2024 at 14:08):

You can also make your lines a datatype and give an interpretation function points. Then everything is much simpler:
(and I added proper intro and elim rules for your parallel definition)

Thanks very much. I've been struggling with this for hours.

Indeed, that is a great deal simpler. I'm still interested in the question of how to prove that forall x in S, Q(x) by iterating through the elements s of S showing Q(s) for each one. You've avoided that by shuffling things around to a situation where the set S in fact consists of all items of some type, at which point a nice "cases" approach works.

datatype a4pt = Pa | Qa | Ra | Sa
datatype a4line = A4PQ | A4PR | A4PS | A4QR | A4QS | A4RS

fun points :: "a4line ⇒ a4pt set" where
  "points A4PQ = {Pa, Qa}"
| "points A4PR = {Pa, Ra}"
| "points A4PS = {Pa, Sa}"
| "points A4QR = {Qa, Ra}"
| "points A4QS = {Qa, Sa}"
| "points A4RS = {Ra, Sa}"

definition "parallel l m ≡ l = m ∨ (points l ∩ points m = {})"

lemma parallel_self [iff]: "parallel l l"
  unfolding parallel_def by simp

lemma parallel_if_points_inter_eq_emptyI [intro]:
  assumes "points l ∩ points m = {}"
  shows "parallel l m"
  using assms unfolding parallel_def by simp

lemma parallelE [elim]:
  assumes "parallel l m"
  obtains (eq) "l = m" | (disjoint) "points l ∩ points m = {}"
  using assms unfolding parallel_def by auto

fun A4complement::"a4line ⇒ a4line" where
  "A4complement A4PQ = A4RS"
| "A4complement A4RS = A4PQ"
| "A4complement A4PR = A4QS"
| "A4complement A4QS = A4PR"
| "A4complement A4PS = A4QR"
| "A4complement A4QR = A4PS"

lemma A4complement_parallel:
  shows "parallel (A4complement n) n"
  by (cases n) auto

I'd also recommend using something other than sets if points should always return exactly two points.

I confess that as a mathematician, being told "Oh, don't use sets" is a little offputting, since they are literally my bread and butter. But I certainly see the point in this particular case. On the other hand, this particular theory file is working out the details of the only example of a finite affine plane in a textbook, so generalizing further doesn't make any sense.

Can I ask one more related question? You've used "unfolding" in multiple places where I would have used "using". Thinking that I should learn the distinction, I looked at "Programming and Proving" ... where the word "unfolding" appears only twice, neither time with a clear description. For functions that are not recursive, am I right in thinking that the effect is more or less the same? Also: is it stylistically considered more appropriate to use "unfolding" for function-definitions, but just "using" in a case like my attempt where I might say "using A4PQ_def" to get the details of some defined constant?

Lukas Stevens (Apr 27 2024 at 13:30):

using adds the fact as an assumption for the following following proof method(s). unfolding is meant to be used to unfold definitions but can be used for any equations. If you use the simplifier after using, you might get the impression that they behave similarly but the effect is quite different.

John Hughes (Apr 27 2024 at 15:09):

Lukas Stevens said:

using adds the fact as an assumption for the following following proof method(s). unfolding is meant to be used to unfold definitions but can be used for any equations. If you use the simplifier after using, you might get the impression that they behave similarly but the effect is quite different.

I appreciate your answering, but to be honest, I don't really feel that I understand anything more after reading your answer. Can you perhaps elucidate a bit with an example?

I have to confess, I don't entirely know what 'unfold' means, so saying that "unfolding is mean to be used to unfold..." isn't shedding any light. (I'd be quite happy with a pointer to read about this use of 'unfold'; it's just something I'm not familiar with.)

Mathias Fleury (Apr 27 2024 at 17:14):

Maybe look at the goal before and after the using/ unfolding but before you apply the tactic. Then you will see the difference

Mathias Fleury (Apr 27 2024 at 17:15):

unfold manipulates the goal and directly unpeals definitions

Mathias Fleury (Apr 27 2024 at 17:15):

using just gives the information that the definition exists to the next tactic and that tactic must do things

Mathias Fleury (Apr 27 2024 at 17:16):

for simp this is rarely different, but blast does not know about equality so it does nothing with the definitions

John Hughes (Apr 27 2024 at 23:28):

Thanks --- that's just what I needed.

Kevin Kappelmann (Apr 30 2024 at 11:02):

John Hughes said:

I confess that as a mathematician, being told "Oh, don't use sets" is a little offputting, since they are literally my bread and butter. But I certainly see the point in this particular case. On the other hand, this particular theory file is working out the details of the only example of a finite affine plane in a textbook, so generalizing further doesn't make any sense.

If you really want to stick with sets, you can apply the elimination rule insertE repeatedly on your assumption $n \in A4Lines$ since finite set notation $\{x,y,z\}$ is nothing more but fancy notation for insert x (insert y (insert z {})).
That's actually quite OK, as you can see in the proof below, looking at the state after applying the elimination rule. However, the next proof step is quite ugly: you need to unfold all definitions and supply another rule that breaks down an equality on finite sets into an equality on its members (+ a case distinction), as shown by rule doubleton_eq_iff:

lemma A4complement_parallel:
  fixes n
  assumes "n ∈ A4Lines"
  shows "parallel (A4complement n) n"
  using assms unfolding A4Lines_def
  apply (elim insertE)
  apply (simp_all add: A4PQ_def A4PR_def A4PS_def A4QR_def A4QS_def A4RS_def A4Lines_def
    doubleton_eq_iff)
  done

John Hughes (Apr 30 2024 at 12:43):

Kevin Kappelmann said:

John Hughes said:

I confess that as a mathematician, being told "Oh, don't use sets" is a little offputting, since they are literally my bread and butter. But I certainly see the point in this particular case. On the other hand, this particular theory file is working out the details of the only example of a finite affine plane in a textbook, so generalizing further doesn't make any sense.

If you really want to stick with sets, you can apply the elimination rule insertE repeatedly on your assumption $n \in A4Lines$ since finite set notation $\{x,y,z\}$ is nothing more but fancy notation for insert x (insert y (insert z {})).
That's actually quite OK, as you can see in the proof below, looking at the state after applying the elimination rule. However, the next proof step is quite ugly: you need to unfold all definitions and supply another rule that breaks down an equality on finite sets into an equality on its members (+ a case distinction), as shown by rule doubleton_eq_iff:

lemma A4complement_parallel:
  fixes n
  assumes "n ∈ A4Lines"
  shows "parallel (A4complement n) n"
  using assms unfolding A4Lines_def
  apply (elim insertE)
  apply (simp_all add: A4PQ_def A4PR_def A4PS_def A4QR_def A4QS_def A4RS_def A4Lines_def
    doubleton_eq_iff)
  done

Thanks again. This explanation of finite-set notation helps explain why even proving {a, b} = {b, a} is nontrivial: Isabelle needs to know that composition of insertions is commutative. For an 8-element set, for instance, that could take some real work.

Manuel Eberl (May 01 2024 at 16:43):

Proving that two finite sets written down fully explicitly is fortunately not that difficult in Isabelle. You can just give the commutativity rule for insert to the simplifier:

lemma "{a,b,c,d,e,f} = {e,c,f,d,b,a}"
  by (simp add: insert_commute)

Of course that only works if the automation can already simplify the elements in the set into a unique normal form.

Last updated: Dec 21 2024 at 16:20 UTC