Created
November 21, 2019 12:01
-
-
Save larsr/d9089da9e1b6b9962e36c370bf05dd98 to your computer and use it in GitHub Desktop.
Logic puzzle: which answer is correct?
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** | |
Which answer is correct? | |
1. All of the below. | |
2. None of the below. | |
3. All of the above. | |
4. At least one of the above. | |
5. None of the above. | |
6. None of the above. | |
**) | |
Require Import Bool. | |
Notation "-- a" := (negb a) (at level 10). | |
Notation " a <--> b" := (eqb a b) (at level 100). | |
Definition puzzle a1 a2 a3 a4 a5 a6 := | |
(a1 <--> (a2 && a3 && a4 && a5 && a6)) && | |
(a2 <--> --(a3||a4||a5||a6)) && | |
(a3 <--> (a1&&a2)) && | |
(a4 <--> (a1||a2||a3)) && | |
(a5 <--> -- (a1||a2||a3||a4)) && | |
(a6 <--> -- (a1||a2||a3||a4||a5)). | |
Goal exists a1 a2 a3 a4 a5 a6, puzzle a1 a2 a3 a4 a5 a6 = true. | |
assert ( forall a1 a2 a3 a4 a5 a6, puzzle a1 a2 a3 a4 a5 a6 = false). | |
(* to get rid of all the failed cases with auto, and only keep the good ones *) | |
intros a1 a2 a3 a4 a5 a6; | |
remember (a1,a2,a3,a4,a5,a6) as Q; | |
destruct a1,a2,a3,a4,a5,a6; simpl; auto. | |
(* now we have the good ones left. see what we have in Q and use that *) | |
Restart. | |
now exists false, false, false, false, true, false. | |
Qed. | |
(* show it is the only answer *) | |
Goal forall a1 a2 a3 a4 a5 a6, | |
puzzle a1 a2 a3 a4 a5 a6 = true <-> | |
( a1, a2, a3, a4, a5, a6) = (false, false, false, false, true, false). | |
split. | |
now destruct a1,a2,a3,a4,a5,a6; compute; inversion 1. | |
now inversion 1. | |
Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment