Stream: general

Topic: can't view multiple goals

Kevin Buzzard (Oct 10 2020 at 21:47):

This came up in teaching:

import tactic

-- First we do the question using Prop (optimised for proving)

variables (P Q R S U : Prop)

theorem trick {Q : Prop} (hQ : Q) : Q ↔ true :=
iff_of_true hQ trivial
theorem trick2 {Q : Prop} (hQ : ¬ Q) : Q ↔ false :=
iff_false_intro hQ
example : ∀ P Q R S U : Prop,
¬ (
(Q ∨ P ∨ U) ∧ (U ∨ ¬Q ∨ S) ∧ (U ∨ Q ∨ ¬R) ∧ (P ∨ R ∨ ¬S) ∧
(P ∨ S ∨ R) ∧ (R ∨ ¬U ∨ Q) ∧ (R ∨ S ∨ ¬U) ∧ (¬S ∨ ¬R ∨ U) ∧
(U ∨ ¬Q ∨ ¬R) ∧ (¬Q ∨ U ∨ ¬S) ∧ (¬P ∨ ¬R ∨ Q) ∧ (S ∨ ¬U ∨ ¬P) ∧
(¬R ∨ ¬P ∨ U) ∧ (S ∨ ¬R ∨ ¬U) ∧ (¬R ∨ ¬Q ∨ ¬S) ∧ (Q ∨ R ∨ S) ∧
(¬U ∨ P ∨ ¬Q) ∧ (R ∨ ¬Q ∨ ¬P) ∧ (P ∨ R ∨ ¬Q) ∧ (S ∨ P ∨ Q) ∧
(R ∨ P ∨ U) ∧ (¬U ∨ Q ∨ R) ∧ (¬U ∨ R ∨ ¬Q) ∧ (¬S ∨ ¬U ∨ ¬Q) ∧
(¬U ∨ ¬S ∨ R) ∧ (¬S ∨ P ∨ U) ∧ (P ∨ Q ∨ ¬R) ∧ (¬S ∨ ¬R ∨ U) ∧
(¬Q ∨ ¬S ∨ U) ∧ (P ∨ R ∨ ¬Q) ∧ (P ∨ Q ∨ ¬S) ∧ (U ∨ ¬S ∨ ¬P) ∧
(¬U ∨ R ∨ ¬P) ∧ (¬U ∨ P ∨ ¬Q) ∧ (¬R ∨ ¬P ∨ S) ∧ (R ∨ S ∨ ¬U) ∧
(P ∨ ¬U ∨ Q) ∧ (¬S ∨ R ∨ P) ∧ (¬P ∨ ¬Q ∨ ¬R) ∧ (¬P ∨ R ∨ ¬S)) :=
begin
intros,
by_cases hP : P;rw trick hP; try {rw iff_false_intro hP}; clear hP; simp;
by_cases hP : Q;rw trick hP; try {rw iff_false_intro hP}; clear hP; simp; -- <- should be 4 goals here
by_cases hP : R;rw trick hP; try {rw iff_false_intro hP}; clear hP; simp;
by_cases hP : S;rw trick hP; try {rw iff_false_intro hP}; clear hP; simp;
by_cases hP : U;rw trick hP; try {rw iff_false_intro hP}; clear hP; simp,
end


I wanted to inspect the goals part way through the proof, but I was surprised to find that changing the semicolon at the end of the second cases line of the proof to a comma still only let me see one goal -- I'm sure I've used this trick in the past to temporarily view multiple goals just to check things aren't going arwy in one of these crazy semicolony proofs.

Kevin Buzzard (Oct 10 2020 at 21:50):

PS one can check that there are four goals after the highlighted semicolon, because you can put sorry four times even though the infoview says there's only one goal.

Bryan Gin-ge Chen (Oct 10 2020 at 22:15):

I think this is discussed at the re-opened lean#201

Last updated: May 12 2021 at 04:19 UTC