10 - "And" Goal

Here we look at a proof goal that is a conjunction.

Task

For integer $x$, given that $x=-1$, show that

$$(x^2=1)\wedge (x^3=-1)$$

Maths

Recall that $P\wedge Q$ being true means both $P$ and $Q$ must be true. 

That means we have to prove both $x^2=1$ and $x^3=-1$ are true, given the hypothesis $x=-1$. 

Let's write a step by step proof.

$$\begin{array}{rlrl}\text{(1)}& x& =-1& & \text{given fact}(x^2=1)& \wedge (x^3=-1)& & \text{proof objective }\\ & & & \\ x^2& =(-1{)}^2& & \text{using fact }(\text{1})\\ \text{(2)}& & =1& & \text{using arithmetic }& & & \\ x^3& =(-1{)}^3& & \text{using fact }(\text{1})\\ \text{(3)}& & =-1& & \text{using arithmetic }& & & \\ ◻& (x^2=1)& \wedge (x^3=-1)& & \text{using results }(\text{2},\text{3})\end{array}$$

We have shown both $x^2=1$ and $x^3=-1$, and so the proof goal $(x^2=1)\wedge (x^3=-1)$ is true.

Code

The following Lean program proves $(x^2=1)\vee (x^3=1)$ follows from $x=-1$.

-- 10 - Conjunctive "and" Goal

import Mathlib.Tactic

example {x : ℤ} (h : x = -1) : x^2 = 1 ∧ x^3 = -1 := by
  constructor
  · calc
      x^2 = (-1)^2 := by rw [h]
      _ = 1 := by norm_num
  · calc
      x^3 = (-1)^3 := by rw [h]
      _ = -1 := by norm_num

As is very familiar now, the proof header declares the variable types, establishes the hypothesis, and defines the overall proof objective. The objective here is a conjunction, and uses the symbol ∧ to denote “logical and”. 

The next step is to split the two parts of the conjunctive proof goal into two separate goals, each to be proven one after another. The instruction constructor does precisely this.

The Infoview will confirm that constructor replaces the single goal x^2 = 1 ∧ x^3 = 1 with two new goals, x^2 = 1 and x^3 = -1.

The rest of the proof has two calc structures, one after the other, to show x^2 = 1 and x^3 = -1. Focussing dots are used to make clear there are two sub-proofs to support the overall proof.

Infoview

Placing the cursor before the constructor instruction shows the original proof goal.

x : ℤ
h : x = -1
⊢ x ^ 2 = 1 ∧ x ^ 3 = -1

Placing the cursor on the next line after constructor confirms the proof goal has been replaced by two smaller goals.

x : ℤ
h : x = -1
⊢ x ^ 2 = 1

x : ℤ
h : x = -1
⊢ x ^ 3 = -1

This is another example of manipulating the proof goal into a form that is easier to prove.

---

Easy Exercise

A longer conjunction could be $P\wedge Q\wedge R\wedge S$. The instruction constructor splits this into two goals, $P$ and $Q\wedge R\wedge S$.

For integer $x$, given that $x=-1$, write a Lean program to show that 

$$(x^3=-1)\wedge (x^4=1)\wedge (x^5=-1)$$

The proof will require two uses of constructor.