Proof:Union computation

From CS2800 wiki
Revision as of 14:44, 31 August 2018 by {{GENDER:Mdg39|[math]'"2}} [/math]'"7
(<math>1) </math>2 | <math>3 (</math>4) | <math>5 (</math>6)

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}. Then \href{/cs2800/wiki/index.php/By_definition}{by definition} of \href{/cs2800/wiki/index.php/%E2%88%AA}{∪}, either \lt math\gt 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\}}. \href{/cs2800/wiki/index.php/Case_analysis}{In the first case} (when \lt math\gt 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 case analysis 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\}. In either case, we readily see that \lt math\gt 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.