Created
August 23, 2018 10:39
-
-
Save kbuzzard/53712d672a894d7b158a512f7aa5f836 to your computer and use it in GitHub Desktop.
modelling a level of the game "undead"
This file contains 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
| import data.set.basic tactic.interactive | |
| import data.list.basic | |
| -- todo -- there's some way of deriving decidable eq here I think | |
| inductive square | |
| | vampire : square | |
| | ghost : square | |
| | zombie : square | |
| namespace square | |
| definition nomirror : square β β | |
| | vampire := 1 | |
| | ghost := 0 | |
| | zombie := 1 | |
| definition mirror : square β β | |
| | vampire := 0 | |
| | ghost := 1 | |
| | zombie := 1 | |
| end square | |
| open square | |
| instance XXX : decidable_eq square | |
| | vampire vampire := is_true rfl | |
| | vampire ghost := is_false (Ξ» h,square.no_confusion h) | |
| | vampire zombie := is_false (Ξ» h,square.no_confusion h) | |
| | ghost vampire := is_false (Ξ» h,square.no_confusion h) | |
| | ghost ghost := is_true rfl | |
| | ghost zombie := is_false (Ξ» h,square.no_confusion h) | |
| | zombie vampire := is_false (Ξ» h,square.no_confusion h) | |
| | zombie ghost := is_false (Ξ» h,square.no_confusion h) | |
| | zombie zombie := is_true rfl | |
| variables aβ aβ aβ aβ aβ aβ aβ aβ aβ : square | |
| /- the 16 equations -/ | |
| definition eβ := aβ.nomirror + aβ.nomirror + aβ.nomirror + aβ.nomirror = 3 | |
| definition eβ := aβ.mirror = 0 | |
| definition eβ := aβ.nomirror + aβ.nomirror + aβ.mirror + aβ .mirror = 2 | |
| definition eβ := 0 = 0 | |
| definition eβ := 0 = 0 | |
| definition eβ := aβ .nomirror + aβ.nomirror + aβ.mirror + aβ.mirror = 3 | |
| definition eβ := aβ.nomirror + aβ.mirror + aβ .mirror + aβ.mirror + aβ.mirror = 3 | |
| definition eβ := 0 = 0 | |
| definition eβ := 0 = 0 | |
| definition eββ := aβ.mirror + aβ.mirror = 1 | |
| definition eββ := aβ.nomirror + aβ.mirror = 2 | |
| definition eββ := aβ.nomirror + aβ.nomirror + aβ.nomirror + aβ.nomirror = 3 | |
| definition eββ := aβ.nomirror + aβ.nomirror = 2 | |
| definition eββ := aβ.nomirror + aβ.mirror = 1 | |
| definition eββ := aβ.nomirror + aβ.mirror + aβ .mirror + aβ.mirror + aβ.mirror = 3 | |
| definition eββ := aβ.nomirror = 1 | |
| definition is_solved := (eβ aβ aβ aβ aβ) β§ (eβ aβ) β§ (eβ aβ aβ aβ ) β§ (eβ) β§ (eβ ) β§ (eβ aβ aβ aβ ) β§ (eβ aβ aβ aβ aβ) | |
| β§ (eβ) β§ (eβ) β§ (eββ aβ aβ) β§ (eββ aβ aβ) β§ (eββ aβ aβ aβ aβ) | |
| β§ (eββ aβ aβ) β§ (eββ aβ aβ) β§ (eββ aβ aβ aβ aβ) β§ (eββ aβ) | |
| β§ list.length (list.filter (Ξ» a, a = vampire) [aβ,aβ,aβ,aβ,aβ ,aβ,aβ,aβ,aβ]) = 3 | |
| β§ list.length (list.filter (Ξ» a, a = ghost) [aβ,aβ,aβ,aβ,aβ ,aβ,aβ,aβ,aβ]) = 3 | |
| β§ list.length (list.filter (Ξ» a, a = zombie) [aβ,aβ,aβ,aβ,aβ ,aβ,aβ,aβ,aβ]) = 3 | |
| lemma not_vampire (a : square) : Β¬ (a = vampire) β a.mirror = 1 := | |
| begin | |
| intro H, | |
| cases a,exfalso,apply H,refl,refl,refl | |
| end | |
| lemma not_ghost (a : square) : Β¬ (a = ghost) β a.nomirror = 1 := | |
| begin | |
| intro H, | |
| cases a,refl,exfalso,apply H,refl,refl | |
| end | |
| lemma not_zombie (a : square) : Β¬ (a = zombie) β a.mirror + a.nomirror = 1 := | |
| begin | |
| intro H, | |
| cases a,refl,refl,exfalso,apply H,refl, | |
| end | |
| lemma square_1_is_vampire (Hsolved : is_solved aβ aβ aβ aβ aβ aβ aβ aβ aβ) : aβ = vampire := | |
| begin | |
| rcases Hsolved with β¨hβ,hβ,hβ,hβ,hβ ,hβ,hβ,hβ,hβ,hββ,hββ,hββ,hββ,hββ,hββ ,hββ,HV,HG,HZβ©, | |
| cases aβ, | |
| refl, | |
| cases hβ, | |
| cases hβ | |
| end | |
| lemma square_2_not_vampire (Hsolved : is_solved aβ aβ aβ aβ aβ aβ aβ aβ aβ) : Β¬ aβ = vampire := | |
| begin | |
| rcases Hsolved with β¨hβ,hβ,hβ,hβ,hβ ,hβ,hβ,hβ,hβ,hββ,hββ,hββ,hββ,hββ,hββ ,hββ,HV,HG,HZβ©, | |
| intro H2, | |
| rw H2 at hβ, | |
| rw H2 at hβ, | |
| cases aβ;cases aβ ;cases hβ;cases hβ | |
| end | |
| lemma square_4_not_zombie (Hsolved : is_solved aβ aβ aβ aβ aβ aβ aβ aβ aβ) : Β¬ aβ = zombie := | |
| begin | |
| rcases Hsolved with β¨hβ,hβ,hβ,hβ,hβ ,hβ,hβ,hβ,hβ,hββ,hββ,hββ,hββ,hββ,hββ ,hββ,HV,HG,HZβ©, | |
| intro H4, | |
| rw H4 at hβ, | |
| rw H4 at hβ, | |
| cases aβ;cases aβ ;cases hβ;cases hβ, | |
| end | |
| lemma square_5_not_ghost (Hsolved : is_solved aβ aβ aβ aβ aβ aβ aβ aβ aβ) : Β¬ aβ = ghost := | |
| begin | |
| rcases Hsolved with β¨hβ,hβ,hβ,hβ,hβ ,hβ,hβ,hβ,hβ,hββ,hββ,hββ,hββ,hββ,hββ ,hββ,HV,HG,HZβ©, | |
| intro H5, | |
| rw H5 at hβ, | |
| rw H5 at hβ, | |
| cases aβ;cases aβ;cases hβ;cases hβ, | |
| end | |
| lemma square_6_not_vampire (Hsolved : is_solved aβ aβ aβ aβ aβ aβ aβ aβ aβ) : Β¬ aβ = vampire := | |
| begin | |
| rcases Hsolved with β¨hβ,hβ,hβ,hβ,hβ ,hβ,hβ,hβ,hβ,hββ,hββ,hββ,hββ,hββ,hββ ,hββ,HV,HG,HZβ©, | |
| intro H6, | |
| rw H6 at hββ, | |
| cases aβ;cases hββ, | |
| end | |
| lemma square_8_not_ghost (Hsolved : is_solved aβ aβ aβ aβ aβ aβ aβ aβ aβ) : Β¬ aβ = ghost := | |
| begin | |
| rcases Hsolved with β¨hβ,hβ,hβ,hβ,hβ ,hβ,hβ,hβ,hβ,hββ,hββ,hββ,hββ,hββ,hββ ,hββ,HV,HG,HZβ©, | |
| intro H8, | |
| rw H8 at hββ, | |
| cases aβ;cases hββ, | |
| end | |
| lemma square_9_not_ghost (Hsolved : is_solved aβ aβ aβ aβ aβ aβ aβ aβ aβ) : Β¬ aβ = ghost := | |
| begin | |
| rcases Hsolved with β¨hβ,hβ,hβ,hβ,hβ ,hβ,hβ,hβ,hβ,hββ,hββ,hββ,hββ,hββ,hββ ,hββ,HV,HG,HZβ©, | |
| intro H9, | |
| rw H9 at hββ, | |
| cases aβ;cases hββ, | |
| end | |
| lemma what_i_know (Hsolved : is_solved aβ aβ aβ aβ aβ aβ aβ aβ aβ) : | |
| aβ = vampire | |
| β§ mirror aβ = 1 | |
| β§ mirror aβ + nomirror aβ = 1 | |
| β§ nomirror aβ = 1 | |
| β§ mirror aβ = 1 | |
| β§ nomirror aβ = 1 | |
| β§ nomirror aβ = 1 | |
| := | |
| begin | |
| have H1 : aβ = vampire := square_1_is_vampire aβ aβ aβ aβ aβ aβ aβ aβ aβ Hsolved, | |
| have H2 : Β¬ aβ = vampire := square_2_not_vampire aβ aβ aβ aβ aβ aβ aβ aβ aβ Hsolved, | |
| have H4 : Β¬ aβ = zombie := square_4_not_zombie aβ aβ aβ aβ aβ aβ aβ aβ aβ Hsolved, | |
| have H5 : Β¬ aβ = ghost := square_5_not_ghost aβ aβ aβ aβ aβ aβ aβ aβ aβ Hsolved, | |
| have H6 : Β¬ aβ = vampire := square_6_not_vampire aβ aβ aβ aβ aβ aβ aβ aβ aβ Hsolved, | |
| have H8 : Β¬ aβ = ghost := square_8_not_ghost aβ aβ aβ aβ aβ aβ aβ aβ aβ Hsolved, | |
| have H9 : Β¬ aβ = ghost := square_9_not_ghost aβ aβ aβ aβ aβ aβ aβ aβ aβ Hsolved, | |
| have H2m : aβ.mirror = 1 := not_vampire aβ H2, | |
| have H4z : aβ.mirror + aβ.nomirror = 1 := not_zombie aβ H4, | |
| have H5g : aβ .nomirror = 1 := not_ghost aβ H5, | |
| have H6v : aβ.mirror = 1 := not_vampire aβ H6, | |
| have H8g : aβ.nomirror = 1 := not_ghost aβ H8, | |
| have H9g : aβ.nomirror = 1 := not_ghost aβ H9, | |
| clear H2,clear H4,clear H5,clear H6,clear H8,clear H9, | |
| exact β¨H1,H2m,H4z,H5g,H6v,H8g,H9gβ© | |
| end | |
| -- I want to finish the job now doing some slicker version of this case by case analysis | |
| lemma square_7_not_zombie (Hsolved : is_solved aβ aβ aβ aβ aβ aβ aβ aβ aβ) : Β¬ aβ = zombie := | |
| begin | |
| have H := what_i_know aβ aβ aβ aβ aβ aβ aβ aβ aβ Hsolved, | |
| rcases (what_i_know aβ aβ aβ aβ aβ aβ aβ aβ aβ Hsolved) with β¨H1,H2m,H4z,H5g,H6v,H8g,H9gβ©, | |
| rcases Hsolved with β¨hβ,hβ,hβ,hβ,hβ ,hβ,hβ,hβ,hβ,hββ,hββ,hββ,hββ,hββ,hββ ,hββ,HV,HG,HZβ©, | |
| rw H1 at *,clear H1, | |
| rw H2m at *,clear H2m, | |
| rw H5g at *,clear H5g, | |
| clear hβ, clear hββ, | |
| intro H7, | |
| rw H7 at *,clear H7, | |
| cases aβ;cases aβ;cases aβ ;cases hβ;cases hββ , | |
| cases aβ;cases aβ;cases aβ;cases aβ;revert HV;try {exact dec_trivial};cases hββ;cases hββ; | |
| cases hββ, | |
| end | |
| lemma equations_so_far (aβ aβ aβ aβ aβ aβ aβ aβ aβ : square) | |
| (H1 : aβ = vampire) | |
| (H2 : Β¬ aβ = vampire) | |
| (H4 : Β¬ aβ = zombie) | |
| (H5 : Β¬ aβ = ghost) | |
| (H6 : Β¬ aβ = vampire) | |
| (H7 : Β¬ aβ = zombie) | |
| (H8 : Β¬ aβ = ghost) | |
| (H9 : Β¬ aβ = ghost) : | |
| is_solved aβ aβ aβ aβ aβ aβ aβ aβ aβ := | |
| begin | |
| unfold is_solved, | |
| unfold eβ,unfold eβ,unfold eβ,unfold eβ,unfold eβ ,unfold eβ,unfold eβ,unfold eβ, | |
| unfold eβ,unfold eββ,unfold eββ,unfold eββ,unfold eββ,unfold eββ,unfold eββ ,unfold eββ, | |
| rw H1, | |
| have H2v : aβ.mirror = 1, | |
| cases aβ,exfalso,apply H2,refl,refl,refl, | |
| rw H2v,clear H2v, | |
| have H4z : aβ.mirror + aβ.nomirror = 1, | |
| cases aβ,refl,refl,exfalso,apply H4,refl, | |
| -- unused | |
| have H5g : aβ .nomirror = 1, | |
| cases aβ ,refl,exfalso,apply H5,refl,refl, | |
| rw H5g,clear H5g, | |
| have H6v : aβ.mirror = 1, | |
| cases aβ,exfalso,apply H6,refl,refl,refl, | |
| rw H6v,clear H6v, | |
| have H8g : aβ.nomirror = 1, | |
| cases aβ,refl,exfalso,apply H8,refl,refl, | |
| rw H8g,clear H8g, | |
| have H9g : aβ.nomirror = 1, | |
| cases aβ,refl,exfalso,apply H9,refl,refl, | |
| rw H9g,clear H9g, | |
| unfold mirror,unfold nomirror,simp, | |
| split,swap, | |
| split,swap, | |
| split,rw βadd_assoc,rw H4z, | |
| split,swap, | |
| split,swap, | |
| split,swap, | |
| split,swap, | |
| split,swap, | |
| split,swap, | |
| split,swap, | |
| repeat {sorry}, | |
| end | |
| -- final boss | |
| theorem unique_solution : β! (aβ aβ aβ aβ aβ aβ aβ aβ aβ : square), | |
| is_solved aβ aβ aβ aβ aβ aβ aβ aβ aβ := begin | |
| sorry | |
| end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment