Difference between revisions of "Proof:Union computation"

From CS2800 wiki
Line 19: Line 19:
 
}}
 
}}
  
== proof techniques ==
+
== Proof techniques ==
  
 
This proof used only a few proof techniques:
 
This proof used only a few proof techniques:
Line 31: Line 31:
 
We will review these and other techniques more systematically in the following lecture.  It is a good exercise to read through this proof and identify which of these techniques is being applied in each step.
 
We will review these and other techniques more systematically in the following lecture.  It is a good exercise to read through this proof and identify which of these techniques is being applied in each step.
  
== eliding detail ==
+
== Eliding detail ==
  
 
I have expanded the proof above in painstaking detail; most proofs would elide some of this detail.  Here is a more typical proof of the above fact:
 
I have expanded the proof above in painstaking detail; most proofs would elide some of this detail.  Here is a more typical proof of the above fact:
Line 38: Line 38:
 
Let <math>[[LHS]] [[Definition|:=]] \{1,2\} [[∪]] \{2,3\}</math> and <math>[[RHS]] [[Definition|:=]] \{1,2,3\}</math>; we [[want to show]] that <math>LHS [[⊆]] RHS</math> and <math>RHS [[⊆]] LHS</math>.
 
Let <math>[[LHS]] [[Definition|:=]] \{1,2\} [[∪]] \{2,3\}</math> and <math>[[RHS]] [[Definition|:=]] \{1,2,3\}</math>; we [[want to show]] that <math>LHS [[⊆]] RHS</math> and <math>RHS [[⊆]] LHS</math>.
  
[[choose an arbitrary value|Choose]] an <math>x [[∈]] [[LHS]]</math>; then <math>x</math> is either in <math>\{1,2\}</math> or <math>\{2,3\}.  In either case, we readily see that <math>x [[∈]] \{1,2,3\}</math>, so <math>[[LHS]] [[⊆]] [[RHS]]</math>.
+
[[choose an arbitrary value|Choose]] an <math>x [[∈]] [[LHS]]</math>; then <math>x</math> is either in <math>\{1,2\}</math> or <math>\{2,3\}</math>.  In either case, we readily see that <math>x [[∈]] \{1,2,3\}</math>, so <math>[[LHS]] [[⊆]] [[RHS]]</math>.
  
 
On the other hand, if we [[choose an arbitrary value|choose]] an <math>x [[∈]] [[RHS]]</math>, we see that <math>x</math> is either 1, 2, [[or]] 3; in the former two cases, <math>x [[∈]] \{1,2\}</math> and thus in the [[LHS]], while in the third case, <math>x [[∈]] \{2,3\}</math> and is again in the [[LHS]].
 
On the other hand, if we [[choose an arbitrary value|choose]] an <math>x [[∈]] [[RHS]]</math>, we see that <math>x</math> is either 1, 2, [[or]] 3; in the former two cases, <math>x [[∈]] \{1,2\}</math> and thus in the [[LHS]], while in the third case, <math>x [[∈]] \{2,3\}</math> and is again in the [[LHS]].

Revision as of 14:49, 31 August 2018

To demonstrate a few proof techniques, we will do a proof of the following fact, in painstaking detail:

[math]\href{/cs2800/wiki/index.php/Enumerated_set}{\{1,2\}} \href{/cs2800/wiki/index.php/%E2%88%AA}{∪} \href{/cs2800/wiki/index.php/Enumerated_set}{\{2,3\}} = \href{/cs2800/wiki/index.php/Enumerated_set}{\{1,2,3\}} [/math]

We begin with the completed proof; we'll circle back and look at the proof techniques below.

Proof: painstaking version
Let [math]\href{/cs2800/wiki/index.php/LHS}{LHS} \href{/cs2800/wiki/index.php/Definition}{:=} \href{/cs2800/wiki/index.php/Enumerated_set}{\{1,2\}} \href{/cs2800/wiki/index.php/%E2%88%AA}{∪} \href{/cs2800/wiki/index.php/Enumerated_set}{\{2,3\}} [/math] denote the left hand side, and similarly let [math]\href{/cs2800/wiki/index.php/RHS}{RHS} \href{/cs2800/wiki/index.php/Definition}{:=} \href{/cs2800/wiki/index.php/Enumerated_set}{\{1,2,3\}} [/math]. We want to show that [math]\href{/cs2800/wiki/index.php/LHS}{LHS} \href{/cs2800/wiki/index.php/Equality_(sets)}{=} \href{/cs2800/wiki/index.php/RHS}{RHS} [/math], or in other words that [math]\href{/cs2800/wiki/index.php/LHS}{LHS} \href{/cs2800/wiki/index.php/%E2%8A%86}{⊆} \href{/cs2800/wiki/index.php/RHS}{RHS} [/math] and [math]\href{/cs2800/wiki/index.php/RHS}{RHS} \href{/cs2800/wiki/index.php/%E2%8A%86}{⊆} \href{/cs2800/wiki/index.php/LHS}{LHS} [/math].

First, we prove LHS RHS, i.e. that for all [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/LHS}{LHS} [/math], [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} RHS [/math]. Choose an arbitrary [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/LHS}{LHS} [/math]. Then by definition of , either [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/Enumerated_set}{\{1,2\}} [/math] or [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/Enumerated_set}{\{2,3\}} [/math].

In the first case (when [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \{1,2\} [/math]), by definition of {1,2}, we know that [math]x = 1 [/math] or [math]x = 2 [/math]. If x = 1, then [math]x = 1 [/math] or [math]x = 2 [/math] or [math]x = 3 [/math], so [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/RHS}{RHS} [/math] by definition. Similarly, if x = 2, then [math]x = 1 [/math] or [math]x = 2 [/math] or [math]x = 3 [/math], so [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/RHS}{RHS} [/math] by definition. In either subcase, we have shown [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/RHS}{RHS} [/math], so we are done with the [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \{1,2\} [/math] case.

The second case, when [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \{2,3\} [/math] is similar: since [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \{2,3\} [/math], we know that [math]x = 2 [/math] or [math]x = 3 [/math]; in both of these subcases, we have [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \{1,2,3\} = \href{/cs2800/wiki/index.php/RHS}{RHS} [/math].

In both cases, we have shown that [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/RHS}{RHS} [/math], which concludes the subproof that [math]\href{/cs2800/wiki/index.php/LHS}{LHS} \href{/cs2800/wiki/index.php/%E2%8A%86}{⊆} \href{/cs2800/wiki/index.php/RHS}{RHS} [/math].

Now, we need to show that [math]\href{/cs2800/wiki/index.php/RHS}{RHS} \href{/cs2800/wiki/index.php/%E2%8A%86}{⊆} \href{/cs2800/wiki/index.php/LHS}{LHS} [/math], i.e. that every [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/RHS}{RHS} [/math] is in the LHS. Choose an arbitrary [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/RHS}{RHS} [/math]; then [math]x = 1 [/math] or [math]x = 2 [/math] or [math]x = 3 [/math]. If [math]x = 1 [/math] or [math]x = 2 [/math], then [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/Enumerated_set}{\{1,2\}} [/math], so [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/LHS}{LHS} [/math] (by definition of ). In the third case, when [math]x = 3 [/math], we have [math]x = 2 [/math] or [math]x = 3 [/math], so [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/RHS}{RHS} [/math]. In both cases, we have [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} RHS [/math], which completes the proof.

Proof techniques

This proof used only a few proof techniques:

We will review these and other techniques more systematically in the following lecture. It is a good exercise to read through this proof and identify which of these techniques is being applied in each step.

Eliding detail

I have expanded the proof above in painstaking detail; most proofs would elide some of this detail. Here is a more typical proof of the above fact:

Proof: short version
Let [math]\href{/cs2800/wiki/index.php/LHS}{LHS} \href{/cs2800/wiki/index.php/Definition}{:=} \{1,2\} \href{/cs2800/wiki/index.php/%E2%88%AA}{∪} \{2,3\} [/math] and [math]\href{/cs2800/wiki/index.php/RHS}{RHS} \href{/cs2800/wiki/index.php/Definition}{:=} \{1,2,3\} [/math]; we want to show that [math]LHS \href{/cs2800/wiki/index.php/%E2%8A%86}{⊆} RHS [/math] and [math]RHS \href{/cs2800/wiki/index.php/%E2%8A%86}{⊆} LHS [/math].

Choose an [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/LHS}{LHS} [/math]; then [math]x [/math] is either in [math]\{1,2\} [/math] or [math]\{2,3\} [/math]. In either case, we readily see that [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \{1,2,3\} [/math], so [math]\href{/cs2800/wiki/index.php/LHS}{LHS} \href{/cs2800/wiki/index.php/%E2%8A%86}{⊆} \href{/cs2800/wiki/index.php/RHS}{RHS} [/math].

On the other hand, if we choose an [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/RHS}{RHS} [/math], we see that [math]x [/math] is either 1, 2, or 3; in the former two cases, [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \{1,2\} [/math] and thus in the LHS, while in the third case, [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \{2,3\} [/math] and is again in the LHS.

When you leave out detail, you are implicitly claiming that the steps you skip are obvious; you should prove them to yourself to convince yourself that they are, in fact, obvious.