Day 10: Taking apart and building “and”
Follow constructor, h.1/h.2, obtain and bullets on ∧ and ↔.
To prove P ∧ Q you must prove P and prove Q. The tactic constructor splits the goal into those two:
P Q : Prop hp : P hq : Q ⊢ P ∧ Q
After constructor there are two goals, named case left and case right:
case left P Q : Prop hp : P hq : Q ⊢ P case right P Q : Prop hp : P hq : Q ⊢ Q
Both must be closed before the proof is done.
With several goals, a proof uses bullets, ·, to work on one goal at a time:
theorem both (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := P:PropQ:Prophp:Phq:Q⊢ P ∧ Q
P:PropQ:Prophp:Phq:Q⊢ PP:PropQ:Prophp:Phq:Q⊢ Q
P:PropQ:Prophp:Phq:Q⊢ P All goals completed! 🐙
P:PropQ:Prophp:Phq:Q⊢ Q All goals completed! 🐙
The first bullet handles case left (goal P), the second handles case right (goal Q). Each bullet must close its goal completely. Hover over the tactics to watch the goals disappear one by one.
↔ is two implications, so constructor also splits it, into case mp (left to right) and case mpr (right to left):
theorem shift (n : Nat) : n + 1 > 5 ↔ n > 4 := n:Nat⊢ n + 1 > 5 ↔ n > 4
n:Nat⊢ n + 1 > 5 → n > 4n:Nat⊢ n > 4 → n + 1 > 5
n:Nat⊢ n + 1 > 5 → n > 4 n:Nath:n + 1 > 5⊢ n > 4
All goals completed! 🐙
n:Nat⊢ n > 4 → n + 1 > 5 n:Nath:n > 4⊢ n + 1 > 5
All goals completed! 🐙
After constructor:
case mp n : Nat ⊢ n + 1 > 5 → n > 4 case mpr n : Nat ⊢ n > 4 → n + 1 > 5
Now the other side: using a hypothesis h : P ∧ Q. It holds two facts. h.1 is the first (P) and h.2 the second (Q). Or obtain unpacks it into two named hypotheses:
theorem swap (P Q : Prop) (h : P ∧ Q) : Q ∧ P := P:PropQ:Proph:P ∧ Q⊢ Q ∧ P
P:PropQ:Prophp:Phq:Q⊢ Q ∧ P
P:PropQ:Prophp:Phq:Q⊢ QP:PropQ:Prophp:Phq:Q⊢ P
P:PropQ:Prophp:Phq:Q⊢ Q All goals completed! 🐙
P:PropQ:Prophp:Phq:Q⊢ P All goals completed! 🐙
After obtain ⟨hp, hq⟩ := h, the display shows hp : P and hq : Q in place of h.
For an auditor: a hypothesis with
∧is several assumptions at once. Unpack it and check each part.