Zulip Chat Archive

Stream: general

Topic: can't view multiple goals


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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