From 093051b0d3fc3c63ef36bdbb7711666bd1d16a07 Mon Sep 17 00:00:00 2001 From: Trequetrum Date: Thu, 11 Jan 2024 02:28:02 +0000 Subject: [PATCH] Update lvls --- Game.lean | 19 ++++- Game/Doc/Tactics.lean | 60 +++++++++++++--- Game/Levels/AndIntro.lean | 30 ++++++++ Game/Levels/AndIntro/L01.lean | 12 ++-- Game/Levels/AndIntro/L02.lean | 17 ++--- Game/Levels/AndIntro/L03.lean | 21 ++---- Game/Levels/AndIntro/L04.lean | 28 ++++---- Game/Levels/AndIntro/L05.lean | 5 +- Game/Levels/AndIntro/L06.lean | 35 +++++++--- Game/Levels/AndIntro/L07.lean | 4 ++ Game/Levels/AndIntro/L08.lean | 20 +++--- Game/Levels/AndTactic.lean | 18 +++++ Game/Levels/AndTactic/L01.lean | 20 ++++++ Game/Levels/AndTactic/L02.lean | 26 +++++++ Game/Levels/AndTactic/L03.lean | 31 +++++++++ Game/Levels/AndTactic/L04.lean | 25 +++++++ Game/Levels/AndTactic/L05.lean | 21 ++++++ Game/Levels/AndTactic/L06.lean | 25 +++++++ Game/Levels/AndTactic/L07.lean | 25 +++++++ Game/Levels/AndTactic/L08.lean | 37 ++++++++++ Game/Levels/IffIntro.lean | 2 + Game/Levels/IffIntro/L01.lean | 9 ++- Game/Levels/IffIntro/L02.lean | 10 ++- Game/Levels/IffIntro/L03.lean | 109 +++++------------------------ Game/Levels/IffIntro/L04.lean | 56 ++++----------- Game/Levels/IffIntro/L05.lean | 122 +++++++++++++++++++++++++++++++++ Game/Levels/IffIntro/L06.lean | 77 +++++++++++++++++++++ Game/Levels/IffTactic.lean | 16 +++++ Game/Levels/IffTactic/L01.lean | 47 +++++++++++++ Game/Levels/IffTactic/L02.lean | 35 ++++++++++ Game/Levels/IffTactic/L03.lean | 27 ++++++++ Game/Levels/IffTactic/L04.lean | 27 ++++++++ Game/Levels/IffTactic/L05.lean | 122 +++++++++++++++++++++++++++++++++ Game/Levels/IffTactic/L06.lean | 77 +++++++++++++++++++++ Game/Levels/ImpIntro.lean | 6 +- Game/Levels/ImpIntro/L01.lean | 3 + Game/Levels/ImpIntro/L02.lean | 3 + Game/Levels/ImpIntro/L03.lean | 5 +- Game/Levels/ImpIntro/L04.lean | 7 +- Game/Levels/ImpIntro/L05.lean | 7 +- Game/Levels/ImpIntro/L06.lean | 13 +++- Game/Levels/ImpIntro/L07.lean | 13 +++- Game/Levels/ImpIntro/L08.lean | 13 ++-- Game/Levels/ImpIntro/L09.lean | 13 +++- Game/Levels/ImpTactic.lean | 19 +++++ Game/Levels/ImpTactic/L01.lean | 25 +++++++ Game/Levels/ImpTactic/L02.lean | 24 +++++++ Game/Levels/ImpTactic/L03.lean | 26 +++++++ Game/Levels/ImpTactic/L04.lean | 24 +++++++ Game/Levels/ImpTactic/L05.lean | 31 +++++++++ Game/Levels/ImpTactic/L06.lean | 57 +++++++++++++++ Game/Levels/ImpTactic/L07.lean | 37 ++++++++++ Game/Levels/ImpTactic/L08.lean | 37 ++++++++++ Game/Levels/ImpTactic/L09.lean | 28 ++++++++ Game/Levels/NotIntro.lean | 4 +- Game/Levels/NotIntro/L01.lean | 3 + Game/Levels/NotIntro/L02.lean | 3 + Game/Levels/NotIntro/L03.lean | 4 ++ Game/Levels/NotIntro/L04.lean | 4 ++ Game/Levels/NotIntro/L05.lean | 8 ++- Game/Levels/NotIntro/L06.lean | 3 + Game/Levels/NotIntro/L07.lean | 4 ++ Game/Levels/NotIntro/L08.lean | 4 ++ Game/Levels/NotIntro/L09.lean | 4 ++ Game/Levels/NotIntro/L10.lean | 4 ++ Game/Levels/NotIntro/L11.lean | 4 ++ Game/Levels/NotIntro/L12.lean | 8 ++- Game/Levels/NotTactic.lean | 22 ++++++ Game/Levels/NotTactic/L01.lean | 22 ++++++ Game/Levels/NotTactic/L02.lean | 32 +++++++++ Game/Levels/NotTactic/L03.lean | 32 +++++++++ Game/Levels/NotTactic/L04.lean | 29 ++++++++ Game/Levels/NotTactic/L05.lean | 24 +++++++ Game/Levels/NotTactic/L06.lean | 29 ++++++++ Game/Levels/NotTactic/L07.lean | 23 +++++++ Game/Levels/NotTactic/L08.lean | 30 ++++++++ Game/Levels/NotTactic/L09.lean | 34 +++++++++ Game/Levels/NotTactic/L10.lean | 38 ++++++++++ Game/Levels/NotTactic/L11.lean | 25 +++++++ Game/Levels/NotTactic/L12.lean | 32 +++++++++ Game/Levels/OrIntro/L01.lean | 3 + Game/Levels/OrIntro/L02.lean | 3 + Game/Levels/OrIntro/L03.lean | 7 +- Game/Levels/OrIntro/L04.lean | 4 ++ Game/Levels/OrIntro/L05.lean | 7 +- Game/Levels/OrIntro/L06.lean | 4 ++ Game/Levels/OrIntro/L07.lean | 4 ++ Game/Levels/OrIntro/L08.lean | 4 ++ Game/Levels/OrTactic.lean | 18 +++++ Game/Levels/OrTactic/L01.lean | 22 ++++++ Game/Levels/OrTactic/L02.lean | 22 ++++++ Game/Levels/OrTactic/L03.lean | 25 +++++++ Game/Levels/OrTactic/L04.lean | 26 +++++++ Game/Levels/OrTactic/L05.lean | 28 ++++++++ Game/Levels/OrTactic/L06.lean | 33 +++++++++ Game/Levels/OrTactic/L07.lean | 30 ++++++++ Game/Levels/OrTactic/L08.lean | 31 +++++++++ Game/Metadata.lean | 2 +- images/logic0101.png | Bin 0 -> 40264 bytes 99 files changed, 2064 insertions(+), 244 deletions(-) create mode 100644 Game/Levels/AndTactic.lean create mode 100755 Game/Levels/AndTactic/L01.lean create mode 100755 Game/Levels/AndTactic/L02.lean create mode 100755 Game/Levels/AndTactic/L03.lean create mode 100755 Game/Levels/AndTactic/L04.lean create mode 100755 Game/Levels/AndTactic/L05.lean create mode 100755 Game/Levels/AndTactic/L06.lean create mode 100755 Game/Levels/AndTactic/L07.lean create mode 100755 Game/Levels/AndTactic/L08.lean create mode 100644 Game/Levels/IffIntro/L05.lean create mode 100644 Game/Levels/IffIntro/L06.lean create mode 100644 Game/Levels/IffTactic.lean create mode 100755 Game/Levels/IffTactic/L01.lean create mode 100644 Game/Levels/IffTactic/L02.lean create mode 100644 Game/Levels/IffTactic/L03.lean create mode 100644 Game/Levels/IffTactic/L04.lean create mode 100644 Game/Levels/IffTactic/L05.lean create mode 100644 Game/Levels/IffTactic/L06.lean create mode 100644 Game/Levels/ImpTactic.lean create mode 100755 Game/Levels/ImpTactic/L01.lean create mode 100755 Game/Levels/ImpTactic/L02.lean create mode 100755 Game/Levels/ImpTactic/L03.lean create mode 100755 Game/Levels/ImpTactic/L04.lean create mode 100755 Game/Levels/ImpTactic/L05.lean create mode 100755 Game/Levels/ImpTactic/L06.lean create mode 100755 Game/Levels/ImpTactic/L07.lean create mode 100755 Game/Levels/ImpTactic/L08.lean create mode 100755 Game/Levels/ImpTactic/L09.lean create mode 100644 Game/Levels/NotTactic.lean create mode 100755 Game/Levels/NotTactic/L01.lean create mode 100755 Game/Levels/NotTactic/L02.lean create mode 100755 Game/Levels/NotTactic/L03.lean create mode 100755 Game/Levels/NotTactic/L04.lean create mode 100755 Game/Levels/NotTactic/L05.lean create mode 100755 Game/Levels/NotTactic/L06.lean create mode 100755 Game/Levels/NotTactic/L07.lean create mode 100755 Game/Levels/NotTactic/L08.lean create mode 100755 Game/Levels/NotTactic/L09.lean create mode 100755 Game/Levels/NotTactic/L10.lean create mode 100755 Game/Levels/NotTactic/L11.lean create mode 100755 Game/Levels/NotTactic/L12.lean create mode 100644 Game/Levels/OrTactic.lean create mode 100755 Game/Levels/OrTactic/L01.lean create mode 100755 Game/Levels/OrTactic/L02.lean create mode 100755 Game/Levels/OrTactic/L03.lean create mode 100755 Game/Levels/OrTactic/L04.lean create mode 100755 Game/Levels/OrTactic/L05.lean create mode 100755 Game/Levels/OrTactic/L06.lean create mode 100755 Game/Levels/OrTactic/L07.lean create mode 100755 Game/Levels/OrTactic/L08.lean create mode 100644 images/logic0101.png diff --git a/Game.lean b/Game.lean index 818cab9..e4a45a4 100755 --- a/Game.lean +++ b/Game.lean @@ -5,16 +5,33 @@ import GameServer.Commands -- in this case). Each world consists of a finite number of levels, and levels -- are numbered 1,2,3,4... inside the level files. import Game.Levels.AndIntro +import Game.Levels.AndTactic import Game.Levels.ImpIntro +import Game.Levels.ImpTactic import Game.Levels.NotIntro +import Game.Levels.NotTactic import Game.Levels.OrIntro +import Game.Levels.OrTactic import Game.Levels.IffIntro +import Game.Levels.IffTactic -- Here's where we show how to glue the worlds together +-- Intro World Dependencies Dependency AndIntro → ImpIntro Dependency ImpIntro → NotIntro Dependency ImpIntro → OrIntro Dependency ImpIntro → IffIntro +-- Intro—Tactic Dependencies +Dependency AndIntro → AndTactic +Dependency ImpIntro → ImpTactic +Dependency OrIntro → OrTactic +Dependency NotIntro → NotTactic +Dependency IffIntro → IffTactic +-- Tactic World Dependencies +Dependency AndTactic → ImpTactic +Dependency ImpTactic → OrTactic +Dependency ImpTactic → NotTactic +Dependency ImpTactic → IffTactic -- Here's what we'll put on the title screen Title "A Lean Intro to Logic" @@ -157,7 +174,7 @@ Warning: In most browsers, deleting cookies will also clear the local storage Languages "English" CaptionShort "Lean intro to Logic" CaptionLong "Self-contained friendly introduction to constructive logic" --- CoverImage "images/cover.png" +CoverImage "images/logic0101.png" /-! Build the game. Show's warnings if it found a problem with your game. -/ MakeGame diff --git a/Game/Doc/Tactics.lean b/Game/Doc/Tactics.lean index 2072227..78e4585 100755 --- a/Game/Doc/Tactics.lean +++ b/Game/Doc/Tactics.lean @@ -118,17 +118,7 @@ TacticDoc rw /-- ## Summary - -`repeat t` repeatedly applies the tactic `t` -to the goal. You don't need to use this -tactic, it just speeds things up sometimes. - -## Example - -`repeat rw [add_zero]` will turn the goal -`a + 0 + (0 + (0 + 0)) = b + 0 + 0` -into the goal -`a = b`. +`repeat t` repeatedly applies the tactic `t` to the goal. You don't need to use this tactic, it just speeds things up sometimes. -/ TacticDoc «repeat» @@ -145,3 +135,51 @@ will change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]` will change the goal to `succ 1 + succ 1 = 4`. -/ TacticDoc nth_rewrite + +/-- +assumption tries to solve the main goal by searching your the assumptions in your proof state for a hypothesis with a compatible proposition +-/ +TacticDoc assumption + +/-- +# Constructor +Whenever there's a clear way to create new evidence **that matches the goal**, the constructor tactic will pick that for you. This replaces the current goal with one or more goals that together complete the construction. + +For example, if your goal is `P ∧ Q` then the `constructor` tactic will replace that goal with two separate subgoals. First you'll need to show evidence for `P`, then you'll need to show evidence for `Q`. +-/ +TacticDoc constructor + +/-- +TODO +-/ +TacticDoc cases + +/-- +TODO +-/ +TacticDoc apply + +/-- +TODO +-/ +TacticDoc intro + +/-- +TODO +-/ +TacticDoc contradiction + +/-- +TODO +-/ +TacticDoc exfalso + +/-- +TODO +-/ +TacticDoc left + +/-- +TODO +-/ +TacticDoc right diff --git a/Game/Levels/AndIntro.lean b/Game/Levels/AndIntro.lean index d00054d..bd97411 100755 --- a/Game/Levels/AndIntro.lean +++ b/Game/Levels/AndIntro.lean @@ -24,4 +24,34 @@ The real-world analogues for evidence of `A ∧ B` might be a box with evidence While real-world analogues can be anything, the abstract machinery used in this game will always be the same. In the case of the `∧` operator, the game stores the associated evidence in a tuple data structure.\\ \\ The details aren't important. Each level will be encoded for you into the symbols of a proof state. The puzzle, at its core, will be about symbol manipulation. Much of the text is there for added fun and flair. + +# **Aside**: Expressions +If you're coming at this as a puzzle, part of the goal of the tutotial worlds is to teach you how to form expressions and to think about what they evaluate to. Consider how how these expressions all evaluate to the same number: +``` +4 + 6 +(4) + 6 +(4) + (6) +3 + 1 + 6 +3 + (1 + 6) +4 + 4 + 2 +(4 * 2) + 2 +``` +and how some things which may look like expressions really are not: +``` +4 6 +4 + +4 (++) 6 +(4 +) 6 +``` +The expressions that this game is asking you to form are mostly in prefix form. In context, this means the operation is given a textual name instead of a symbol and the parameters are separated by spaces **after** the name. For example; the above expressions may look like: +``` +add 4 6 +add (4) 6 +add (4) (6) +add (add 3 1) 6 +add 3 (add 1 6) +add (add 4 4) 2 +add (mul 4 2) 2 +``` +We're not using expressions to express numbers, but many of the concepts do carry over. Instead of numbers, we're working with logical inferences. " diff --git a/Game/Levels/AndIntro/L01.lean b/Game/Levels/AndIntro/L01.lean index 86cd269..6487863 100755 --- a/Game/Levels/AndIntro/L01.lean +++ b/Game/Levels/AndIntro/L01.lean @@ -8,23 +8,19 @@ Title "Exactly! It's in the premise" NewTactic exact NewDefinition GameLogic.AsciiTable +OnlyTactic exact Introduction " # Introduction -You've made a todo list, so you've begun to plan your party. Exhibit evidence that you're planning the party. +You've made a todo list, so you've begun to plan your party. ## Proposition Key: `P` — You're **P**lanning a party ## Assumptions `todo_list : P` — Can be read as `todo_list` “is evidence for” `P` # The Exact Tactic -The Exact tactic is — for now — the means through which you give the game your answer. It's your way of declaring that you're done. In this level, you're just going to be using one of the premises directly, but as you learn how to form expressions the `exact` tactic will accept those too.\\ +The Exact tactic is — for now — the means through which you give the game your answer. It's your way of declaring that you're done. In this level, you're just going to be using one of the assumptions directly, but as you learn how to form expressions the `exact` tactic will accept those too.\\ \\ -It's entered like this: -``` -Goal: P -exact <> -``` -You can use the `exact` tactic to give `todo_list` as your answer.\\ +The expression looks like `exact e` were `e` is an expression the game will accept for the current Goal.\\ \\ ⋆Spoilers!⋆ If you enter “`exact todo_list`,” you will have completed this level. diff --git a/Game/Levels/AndIntro/L02.lean b/Game/Levels/AndIntro/L02.lean index cf71a3c..fa61249 100755 --- a/Game/Levels/AndIntro/L02.lean +++ b/Game/Levels/AndIntro/L02.lean @@ -8,8 +8,12 @@ Title "And Introduction" NewTheorem GameLogic.and_intro NewDefinition GameLogic.and_def +OnlyTactic exact Introduction " +# `∧` +The hat symbol “ ∧ ” is how logicians denote a conjunction — a logical “and”. `A ∧ B` means “A and B”. It works the way you would intuitively expect. Like a lot of math operators (`+,-,÷,×`,and others), the `∧` symbol is an infix operator. This means it has a left side and a right side. Looking at `A ∧ B`, you can see that `A` is on the left and `B` is on the right. + # Sending Invitations in a Single Package You have two letters, one extending an invitation to Pippin and the other to Sybeth. Since they share a residence, you'd like to consolidate their invites into a single package for shipping. The box you're using has space for two items, one on the left and one on the right.\\ \\ @@ -17,9 +21,7 @@ You've labelled the box explicitly, specifying that Pippin's invitation is on th # Proposition Key: - P — “**P**ippin is invited to the party” - S — “**S**ybeth is invited to the party” -# `∧` -The hat symbol “ ∧ ” is how logicians denote a conjunction — a logical “and”. `A ∧ B` means “A and B”. It works the way you would intuitively expect. Like a lot of math operators (`+,-,÷,×`,and others), the `∧` symbol is an infix operator. This means it has a left side and a right side. Looking at `A ∧ B`, you can see that `A` is on the left and `B` is on the right.\\ -\\ + In this game, that means anything operating as evidence for `A ∧ B` will have a left part and a right part as well. The box described in the intro works this way. # Assumptions - `p : P` — Your invitation for Pippin is evidence that Pippin is invited to the party @@ -27,16 +29,10 @@ In this game, that means anything operating as evidence for `A ∧ B` will have # Goal Use `p` and `s` to produce evidence that `P ∧ S`. Remember that you use evidence (generally lowercase letters), to deduce new propositions (generally uppercase letters) -# Juxtapose! -Throughout this game, most of the expressions you will learn are expressed with a name juxtaposed in front of some number of parameters. The form is something like `(name_a param1 param2)`\\ -\\ -In general, “params” can themsevles be the result of any expression as well. You'll often see nested expressions like `(name_a (name_b param1 param2) param2)` where `(name_b param1 param2)` is the first parameter to `name_a` in this example. - # Using the `∧` Construtor This level has unlocked “`∧`” under definitions. This has made the `and_intro` constructor available. You can use `and_intro` by giving it the two relevant pieces of evidence. The expression looks like: `and_intro e₁ e₂` where `e₁` and `e₂` are evidence.\\ \\ -The help-page has even more detail about creating conjunctions like this. - +The help-page has even more detail about creating conjunctions like this (There's a common shorthand using angle-brackers `⟨` `⟩`). # A reminder Use the `exact` tactic to exhibit evidence for a goal @@ -54,7 +50,6 @@ You've got evidence that Pippin and Sybeth are invited to the party.\\ Here are some answers the game would have accepted: ``` exact and_intro p s -exact {left := p, right := s} exact ⟨p,s⟩ ``` " diff --git a/Game/Levels/AndIntro/L03.lean b/Game/Levels/AndIntro/L03.lean index f41277a..1ffc881 100755 --- a/Game/Levels/AndIntro/L03.lean +++ b/Game/Levels/AndIntro/L03.lean @@ -8,6 +8,9 @@ Title "The Have Tactic" NewDefinition GameLogic.Precedence NewTactic «have» +OnlyTactic + exact + «have» Introduction " # Too Many Invites @@ -23,7 +26,6 @@ Nesting boxes like this is a way to get around the “two items per box” rule. - O — **O**rin is invited to the party - U — **U**riel is invited to the party - # The `have` Tactic You can complete this level with your knowledge from the previous level without using this new tactic. For example, either of these would work: ``` @@ -32,7 +34,7 @@ exact ⟨⟨a,i⟩,⟨o,u⟩⟩ ``` Instead of nesting this way, you can break the process down into steps using the `have` tactic. Enter “`have ai := and_intro a i`” to create your first box. After it's entered, it will appear under assumptions in the proof state. Now enter “`have ou := and_intro o u`” to create the second box.\\ \\ -Your proof state should now have the following assumptions: +If you followed this suggestion, your proof state should now have the following assumptions: ``` Assumptions: a: A @@ -50,21 +52,12 @@ Finally, now you can place these two boxes — `ai` and `ou` — into a third bo Statement (A I O U : Prop)(a : A)(i : I)(o : O)(u : U) : (A ∧ I) ∧ O ∧ U := by have ai := and_intro a i have ou := and_intro o u + Hint (hidden := true) "exact and_intro {ai} {ou}" exact and_intro ai ou +example (A I O U : Prop)(a : A)(i : I)(o : O)(u : U) : (A ∧ I) ∧ O ∧ U := by + exact ⟨⟨a,i⟩,⟨o,u⟩⟩ Conclusion " Great! Another 4 invites sent out. You're getting the hang of this. - ----- -```` --- 1. Alarfil and Ilyn: A ∧ I -have h₁ := and_intro a i - --- 2. Orin and Uriel: O ∧ U -have h₂ := and_intro o u - --- 3. both boxes in a final box -exact and_intro h₁ h₂ -```` " diff --git a/Game/Levels/AndIntro/L04.lean b/Game/Levels/AndIntro/L04.lean index 135edd4..d2b7112 100755 --- a/Game/Levels/AndIntro/L04.lean +++ b/Game/Levels/AndIntro/L04.lean @@ -7,6 +7,9 @@ Level 4 Title "And Elimination" NewTheorem GameLogic.and_left +OnlyTactic + exact + «have» Introduction " # Using Only What Is Needed @@ -17,34 +20,33 @@ You'd like to convince Cyna to join the party. You know that Cyna is good friend - P — \"**P**ippin is coming to the party\" - S — \"**S**ybeth is coming to the party\" # Assumptions: -- `h : P ∧ S` — The voicemail (`h`) is evidence that `P ∧ S` +- `vm : P ∧ S` — The voicemail (`vm`) is evidence that `P ∧ S` # Convincing Cyna -Cyna is close with Pippin, but you don't know much about his friendship with Sybeth. You want only a relevant part of the voicemail. Fortunately, you know that any evidence with an `∧` has a left part and a right part. You can use this knowledge to pull evidence out of `h`.\\ +Cyna is close with Pippin, but you don't know much about his friendship with Sybeth. You want only a relevant part of the voicemail. Fortunately, you know that any evidence with an `∧` has a left part and a right part. You can use this knowledge to pull evidence out of `vm`.\\ \\ This can be done with either of these two methods: ``` -have p := h.left -have p := and_left h +have p := and_left vm +have p := vm.left ``` Once you've done this, you're very close to level 1 again where the Goal is directly in your assumptions. " /-- Exhibit evidence that Pippin is coming to the party. -/ -Statement (P S : Prop)(h: P ∧ S) : P := by - have p := h.left +Statement (P S : Prop)(vm: P ∧ S) : P := by + have p := and_left vm + exact p + +example (P S : Prop)(vm: P ∧ S) : P := by + have p := vm.left exact p Conclusion " You've got a proof that Pippin is coming to the party! Lets see if Cyna will attend as well. ---- -Which proof did you use? -```lean -have p := h.left -exact p -``` -or +A reminder that expressions work with the `have` and `exact` tactics in much the same way. You can also solve this level without `have`. ```lean -exact h.left +exact vm.left ``` " diff --git a/Game/Levels/AndIntro/L05.lean b/Game/Levels/AndIntro/L05.lean index a5ce211..dbf4e43 100755 --- a/Game/Levels/AndIntro/L05.lean +++ b/Game/Levels/AndIntro/L05.lean @@ -7,6 +7,9 @@ Level 5 Title "And Elimination 2" NewTheorem GameLogic.and_right +OnlyTactic + exact + «have» Introduction " # Another Unlock @@ -16,7 +19,7 @@ Can you figure this one out? /-- Both P and Q entails just Q as well! -/ Statement (P Q : Prop)(h: P ∧ Q) : Q := by Hint (hidden := true) "`exact h.right`" - exact h.right + exact and_right h Conclusion " Nice. Onward! diff --git a/Game/Levels/AndIntro/L06.lean b/Game/Levels/AndIntro/L06.lean index 536ee48..e72c7ac 100755 --- a/Game/Levels/AndIntro/L06.lean +++ b/Game/Levels/AndIntro/L06.lean @@ -6,6 +6,10 @@ World "AndIntro" Level 6 Title "Mix and Match" +OnlyTactic + exact + «have» + Introduction " # Mixed Up Conjunctions Recall when you placed the invites for Alarfil, Ilyn, Orin, and Uriel in separate boxes. There was a mix-up in the arrangement. Can you fix it so that Alarfil and Uriel's invites are together? @@ -14,27 +18,42 @@ Recall when you placed the invites for Alarfil, Ilyn, Orin, and Uriel in separat - I — **I**lyn is invited to the party - O — **O**rin is invited to the party - U — **U**riel is invited to the party -### Quick tip! -You can type h₁ by entering \"h\\1\". There's unicode table for all the unicode shortcuts this game uses. It should be available under **Definitions** in your inventory. " /-- and_intro, and_left, and_right -/ -Statement (A I O U : Prop)(h₁ : A ∧ I)(h₂ : O ∧ U) : A ∧ U := by - have a := h₁.left - have u := h₂.right +Statement (A I O U : Prop)(h1 : A ∧ I)(h2 : O ∧ U) : A ∧ U := by + have a := h1.left + have u := h2.right exact and_intro a u +example (A I O U : Prop)(h1 : A ∧ I)(h2 : O ∧ U) : A ∧ U := by + exact and_intro h1.left h2.right + +example (A I O U : Prop)(h1 : A ∧ I)(h2 : O ∧ U) : A ∧ U := by + exact and_intro (and_left h1) (and_right h2) + +example (A I O U : Prop)(h1 : A ∧ I)(h2 : O ∧ U) : A ∧ U := by + exact ⟨h1.left, h2.right⟩ + Conclusion " That's better, but you'd better send out those invites so you can get some responses! ---- ``` -have a := h₁.left -have u := h₂.right +have a := h1.left +have u := h2.right exact and_intro a u ``` --- ``` -exact and_intro h₁.left h₂.right +exact and_intro h1.left h2.right +``` +---- +``` +exact and_intro (and_left h1) (and_right h2) +``` +--- +``` +exact ⟨h1.left, h2.right⟩ ``` " diff --git a/Game/Levels/AndIntro/L07.lean b/Game/Levels/AndIntro/L07.lean index d677f01..cce1734 100755 --- a/Game/Levels/AndIntro/L07.lean +++ b/Game/Levels/AndIntro/L07.lean @@ -6,6 +6,10 @@ World "AndIntro" Level 7 Title "More Elimination" +OnlyTactic + exact + «have» + Introduction " # An Emergency! Stop with the invites! Coco, your cat is stuck up a tree.\\ diff --git a/Game/Levels/AndIntro/L08.lean b/Game/Levels/AndIntro/L08.lean index 8f3b5a8..d78f8a9 100755 --- a/Game/Levels/AndIntro/L08.lean +++ b/Game/Levels/AndIntro/L08.lean @@ -6,6 +6,10 @@ World "AndIntro" Level 8 Title "Rearranging Boxes" +OnlyTactic + exact + «have» + Introduction " # BOSS LEVEL If you can finish this level, you've certainly mastered the `∧`. There's no deep logical tricks in this boss level, you've just got to know how to work at properly unnesting and then building the right Proposition.\\ @@ -27,8 +31,8 @@ Finally, a bunch of your invites have returned with RSVPs. The mailman has deliv Statement (A C I O P S U : Prop)(h: ((P ∧ S) ∧ A) ∧ ¬I ∧ (C ∧ ¬O) ∧ ¬U) : A ∧ C ∧ P ∧ S := by have psa := h.left have c := h.right.right.left.left - have fps := and_intro c psa.left - exact and_intro psa.right fps + have cps := and_intro c psa.left + exact and_intro psa.right cps Conclusion " Amazing! You've mastered \"AND\". @@ -38,13 +42,13 @@ Amazing! You've mastered \"AND\". -- 3/4 of the things you need are one step away have psa := h.left --- Evidence for L takes some digging -have l := h.right.right.left.left +-- Evidence for C takes some digging +have c := h.right.right.left.left --- build L ∧ P ∧ S -have lps := and_intro l psa.left +-- build C ∧ P ∧ S +have cps := and_intro c psa.left --- exibit A ∧ L ∧ P ∧ S -exact and_intro psa.right lps +-- exibit A ∧ C ∧ P ∧ S +exact and_intro psa.right cps ``` " diff --git a/Game/Levels/AndTactic.lean b/Game/Levels/AndTactic.lean new file mode 100644 index 0000000..718c6cc --- /dev/null +++ b/Game/Levels/AndTactic.lean @@ -0,0 +1,18 @@ +import Game.Levels.AndTactic.L01 +import Game.Levels.AndTactic.L02 +import Game.Levels.AndTactic.L03 +import Game.Levels.AndTactic.L04 +import Game.Levels.AndTactic.L05 +import Game.Levels.AndTactic.L06 +import Game.Levels.AndTactic.L07 +import Game.Levels.AndTactic.L08 + +World "AndTactic" +Title "Redux: ∧ World Tactics" + +Introduction " +# Redux: ∧ World Tactics +Welcome to the redux of the **∧ Tutorial World**. Every level is the same, but instead of solving each level with `have` and `exact`, this world opens up a bunch of custom tactics.\\ +\\ +This world introduces tactics that you can use in lieu of the expressions you've learned so far. +" diff --git a/Game/Levels/AndTactic/L01.lean b/Game/Levels/AndTactic/L01.lean new file mode 100755 index 0000000..64e8eac --- /dev/null +++ b/Game/Levels/AndTactic/L01.lean @@ -0,0 +1,20 @@ +import Game.Metadata + +open GameLogic + +World "AndTactic" +Level 1 +Title "Assumption" + +NewTactic assumption + +OnlyTactic assumption + +Introduction " +# `assumption` +If the evidence you want is in your list of **Assumptions**, the `assumption` tactic will finish the level for you. +" + +/-- Use the assumption tactic -/ +Statement (P : Prop)(h'₁ : P) : P := by + assumption diff --git a/Game/Levels/AndTactic/L02.lean b/Game/Levels/AndTactic/L02.lean new file mode 100755 index 0000000..b669cde --- /dev/null +++ b/Game/Levels/AndTactic/L02.lean @@ -0,0 +1,26 @@ +import Game.Metadata + +open GameLogic + +World "AndTactic" +Level 2 +Title "Constructor" + +NewTactic constructor + +OnlyTactic + assumption + constructor + +Introduction " +# Constructor +Whenever there's a clear way to create new evidence **that matches the goal**, the constructor tactic will pick that for you. This replaces the current goal with one or more goals that together complete the construction.\\ +\\ +For this level, your goal is `P ∧ Q`. The `constructor` tactic will replace that goal with two separate subgoals. This is likely the first time you've seen two goals in your proof state. First you'll need to show evidence for `P`, then you'll need to show evidence for `Q`. +" + +/-- Use the constructor tactic -/ +Statement (P Q : Prop)(h'₁ : P)(h'₂ : Q) : P ∧ Q := by + constructor + assumption + assumption diff --git a/Game/Levels/AndTactic/L03.lean b/Game/Levels/AndTactic/L03.lean new file mode 100755 index 0000000..21cec83 --- /dev/null +++ b/Game/Levels/AndTactic/L03.lean @@ -0,0 +1,31 @@ +import Game.Metadata + +open GameLogic + +World "AndTactic" +Level 3 +Title "Practise Makes Perfect" + +OnlyTactic + assumption + constructor + +Introduction " +# Practise Makes Perfect +You only have `assumption` and `constructor` available to you. Figure out the order you need to enter them in. +" + +/-- Repeat constructor/assumption until you're done -/ +Statement (P Q R S : Prop)(h'₁ : P)(h'₂ : Q)(h'₃ : R)(h'₄ : S) : (P ∧ Q) ∧ R ∧ S := by + constructor + constructor + assumption + assumption + constructor + assumption + assumption + + +/-- Tactic Proof -/ +example (P Q R S : Prop)(h'₁ : P)(h'₂ : Q)(h'₃ : R)(h'₄ : S) : (P ∧ Q) ∧ R ∧ S := by + repeat (first | constructor | assumption) diff --git a/Game/Levels/AndTactic/L04.lean b/Game/Levels/AndTactic/L04.lean new file mode 100755 index 0000000..b44e87e --- /dev/null +++ b/Game/Levels/AndTactic/L04.lean @@ -0,0 +1,25 @@ +import Game.Metadata + +open GameLogic + +World "AndTactic" +Level 4 +Title "Cases for a Conjunction" + +NewTactic cases + +OnlyTactic + assumption + cases + +Introduction " +# `cases` for a Conjunction +Here, we introduce the `cases` tactic in an unstructured context. `cases` takes a name from the local context and either splits it into multiple goals, or deconstructs it into its parts depending on the Proposition.\\ +\\ +In this level, `cases h` will replace `h` with its `left` and `right` parts. Try it out. +" + +/-- P and Q implies P -/ +Statement (P Q : Prop)(h: P ∧ Q) : P := by + cases h + assumption diff --git a/Game/Levels/AndTactic/L05.lean b/Game/Levels/AndTactic/L05.lean new file mode 100755 index 0000000..53e96ba --- /dev/null +++ b/Game/Levels/AndTactic/L05.lean @@ -0,0 +1,21 @@ +import Game.Metadata + +open GameLogic + +World "AndTactic" +Level 5 +Title "Rinse and Repeat" + +OnlyTactic + assumption + cases + +Introduction " +# Rinse and Repeat +When you were writing expressions before, lvl 4 needed `and_left` while level 5 needed `and_right`. Tactics can incorperate an arbitrary amount of automation. In this case, because assumption will do a search through your assumptions for you, your proof for this level can be 100% identical to the one you used last level. +" + +/-- Both P and Q entails just Q as well! -/ +Statement (P Q : Prop)(h: P ∧ Q) : Q := by + cases h + assumption diff --git a/Game/Levels/AndTactic/L06.lean b/Game/Levels/AndTactic/L06.lean new file mode 100755 index 0000000..4008ab4 --- /dev/null +++ b/Game/Levels/AndTactic/L06.lean @@ -0,0 +1,25 @@ +import Game.Metadata + +open GameLogic + +World "AndTactic" +Level 6 +Title "Nothing New" + +OnlyTactic + assumption + constructor + cases + +Introduction " +# Nothing New +Just use what you've been taught. +" + +/-- Combining your new tactics -/ +Statement (P Q R S : Prop)(h1 : P ∧ Q)(h2 : R ∧ S) : P ∧ S := by + cases h1 + cases h2 + constructor + assumption + assumption diff --git a/Game/Levels/AndTactic/L07.lean b/Game/Levels/AndTactic/L07.lean new file mode 100755 index 0000000..b098aa8 --- /dev/null +++ b/Game/Levels/AndTactic/L07.lean @@ -0,0 +1,25 @@ +import Game.Metadata + +open GameLogic + +World "AndTactic" +Level 7 +Title "More Cases" + +OnlyTactic + assumption + cases + +Introduction " +# So Many Cases +Just keep picking the right hypothesis. +" + +/-- Navigate the tree -/ +Statement (P Q : Prop)(h: (Q ∧ (((Q ∧ P) ∧ Q) ∧ Q ∧ Q ∧ Q)) ∧ (Q ∧ Q) ∧ Q) : P := by + cases h + cases left + cases right_1 + cases left + cases left_2 + assumption diff --git a/Game/Levels/AndTactic/L08.lean b/Game/Levels/AndTactic/L08.lean new file mode 100755 index 0000000..2c9d251 --- /dev/null +++ b/Game/Levels/AndTactic/L08.lean @@ -0,0 +1,37 @@ +import Game.Metadata + +open GameLogic + +World "AndTactic" +Level 8 + +Title "And Tactic Boss" + +OnlyTactic + assumption + constructor + cases + +Introduction " +# BOSS LEVEL +The trick for this level is to pull out the relevant info from the assumption `h` before moving on, otherwise you'll need to re-do that work for each sub-goal. + +I use the `cases` tactic 5 times and for me, they're the first five tactics for this level. +" + +/-- Take apart and build evidence -/ +Statement (A C I O P S U : Prop)(h: ((P ∧ S) ∧ A) ∧ ¬I ∧ (C ∧ ¬O) ∧ ¬U) : A ∧ C ∧ P ∧ S := by + cases h + cases left + cases right + cases right_2 + cases left_2 + constructor + assumption + constructor + assumption + assumption + +Conclusion " +Amazing! You've beaten the `∧` world a second time and you've learned some extra tactics in the process. +" diff --git a/Game/Levels/IffIntro.lean b/Game/Levels/IffIntro.lean index dde3540..5d91395 100644 --- a/Game/Levels/IffIntro.lean +++ b/Game/Levels/IffIntro.lean @@ -2,6 +2,8 @@ import Game.Levels.IffIntro.L01 import Game.Levels.IffIntro.L02 import Game.Levels.IffIntro.L03 import Game.Levels.IffIntro.L04 +import Game.Levels.IffIntro.L05 +import Game.Levels.IffIntro.L06 World "IffIntro" Title "↔ Tutorial: Party Games" diff --git a/Game/Levels/IffIntro/L01.lean b/Game/Levels/IffIntro/L01.lean index 67fe33a..17ec2d9 100755 --- a/Game/Levels/IffIntro/L01.lean +++ b/Game/Levels/IffIntro/L01.lean @@ -6,10 +6,11 @@ World "IffIntro" Level 1 Title "Iff_Intro" -NewTactic rw -NewHiddenTactic «repeat» nth_rewrite NewTheorem GameLogic.iff_intro NewDefinition GameLogic.iff_def +OnlyTactic + exact + «have» Introduction " # Coupled Conditionals @@ -41,4 +42,6 @@ exact ⟨hsj, hjs⟩ ``` " --- example (P Q : Prop): (P ∧ Q) ∨ (¬P ∧ ¬Q) → (P → Q) ∧ (Q → P) := by tauto +/-- Tactic Proof -/ +example (J S : Prop) (hsj: S → J) (hjs: J → S) : S ↔ J := by + constructor <;> assumption diff --git a/Game/Levels/IffIntro/L02.lean b/Game/Levels/IffIntro/L02.lean index 858e759..401d240 100644 --- a/Game/Levels/IffIntro/L02.lean +++ b/Game/Levels/IffIntro/L02.lean @@ -9,6 +9,9 @@ Title "Conjuctive Iff" NewTheorem GameLogic.iff_mp GameLogic.iff_mpr +OnlyTactic + exact + «have» Introduction " # Two sides to every coin @@ -26,6 +29,7 @@ For a biconditional like `h : P ↔ Q`, Statement (B P : Prop) (h : B ↔ ¬P) : (B → ¬P) ∧ (¬P → B) := by exact and_intro (iff_mp h) (iff_mpr h) -Conclusion " -Onward and upward -" +/-- Tactic Proof -/ +example (B P : Prop) (h : B ↔ ¬P) : (B → ¬P) ∧ (¬P → B) := by + cases h + constructor <;> assumption diff --git a/Game/Levels/IffIntro/L03.lean b/Game/Levels/IffIntro/L03.lean index 2562840..9503d1f 100644 --- a/Game/Levels/IffIntro/L03.lean +++ b/Game/Levels/IffIntro/L03.lean @@ -4,101 +4,24 @@ open GameLogic World "IffIntro" Level 3 -Title "Rewriting" +Title "Iff_mp" + +OnlyTactic + exact + «have» Introduction " -# Rewrite the goal -## To an extreme -You're playing a round of *The Resistance*. You've been diligently figuring out who is a member of the resistance and who is a spy. It's a bit complicated, but you've reasoned that the current state of affairs is possible if and only if Alarfil and Cyna are members of the resistance and Pippin is a spy. You also know from an earlier reveal that Pippin and Lippa must be on the same team. Therefore, the same argument applies to Lippa as well. -# Proposition Key: -- A — Alarfil is a member of the resistance -- C — Cyna is a member of the resistance -- L — Lippa is a member of the resistance -- P — Pippin is a member of the resistance -# The `rw` tactic -Depending on the order you've chosen to do the tutorial worlds, you may not yet be familiar with all the symbols in the current proof state. In fact, you may not even have unlocked the tools in your inventory necessary to complete this level. Don't worry, the rewrite tactic makes this level a breeze.\\ -\\ -First, take a look at the proof state and notice that `h₂` and the Goal are extremely similar. In fact, if you replace every occurrence of `L` with `P`, then the two would be identical. That's where `rw` comes in. -\\ -If you have `hpq : P ↔ Q` then `rw [hpq]` will change all `P`s in the goal to `Q`s. It's the way to “substitute in”.\\ -\\ -The `rw` tactic is an automation tool. It does the rote work of taking apart an expression, looking for a matching sub-expression, swapping in the equivalent sub-expression and then constructing the new equivalent term from there.\\ -\\ -Try it out! +# Right-Hand Swap +You'll need h1.mp in order to turn evidence for Q into evidence for R " -/-- Who is loyal, who is a spy? -/ -Statement - (A C L P : Prop) - (h₁ : L ↔ P) - (h₂ : ¬((A → C ∨ ¬P) ∧ (P ∨ A → ¬C) → (P → C)) ↔ A ∧ C ∧ ¬P) - : ¬((A → C ∨ ¬L) ∧ (L ∨ A → ¬C) → (L → C)) ↔ A ∧ C ∧ ¬L := by - rw [h₁] - exact h₂ - -example - (A C L P : Prop) - (h₁ : L ↔ P) - (h₂ : ¬((A → C ∨ ¬P) ∧ (P ∨ A → ¬C) → (P → C)) ↔ A ∧ C ∧ ¬P) - : ¬((A → C ∨ ¬L) ∧ (L ∨ A → ¬C) → (L → C)) ↔ A ∧ C ∧ ¬L := by - rw [← h₁] at h₂ - exact h₂ - -example - (A C L P : Prop) (h₁ : L ↔ P) - (h₂ : ¬((A → C ∨ ¬P) ∧ (P ∨ A → ¬C) → (P → C)) ↔ A ∧ C ∧ ¬P) - : ¬((A → C ∨ ¬L) ∧ (L ∨ A → ¬C) → (L → C)) ↔ A ∧ C ∧ ¬L := - ⟨ - λh₃ ↦ have ⟨a,c,np⟩ := h₂.mp ( - λh₄ ↦ h₃ (λ⟨hl₅,hr₅⟩ l ↦ h₄ ⟨ - λa ↦ or_elim - (hl₅ a) - or_inl - (imp_trans h₁.mpr ≫ or_inr) - , - λ_ ↦ hr₅ (or_inl l) - ⟩ (h₁.mp l)) - ) - ⟨a, c, h₁.mp ≫ np⟩ - , - λ⟨a,c,nl⟩ _ ↦ false_elim ( - h₂.mpr - ⟨a, c, h₁.mpr ≫ nl⟩ - λ_ _ ↦ c - ) - ⟩ +/-- Statement -/ +Statement (P Q R : Prop) (h1 : Q ↔ R)(h2 : P → Q) : P → R := by + exact λp ↦ h1.mp (h2 p) -Conclusion " -Oh, how nice! A fast solution to a complex problem. - ----- -If you've read the inventory page for `rw`, you may have seen another solution too. You can use the backwards arrow “`←`” to change `P`s to `L`s instead of `L`s to `P`s. Also, you can change a hypothesis instead of the goal. -``` -rw [← h₁] at h₂ -exact h₂ -``` - -Here's an example of what this looks like without the `rw` tactic — if you want to try this solution, copy & paste the following text to the editor input mode. -``` -exact ⟨ - λh₃ ↦ have ⟨a,c,np⟩ := h₂.mp ( - λh₄ ↦ h₃ (λ⟨hl₅,hr₅⟩ l ↦ h₄ ⟨ - λa ↦ or_elim - (hl₅ a) - or_inl - (imp_trans h₁.mpr ≫ or_inr) - , - λ_ ↦ hr₅ (or_inl l) - ⟩ (h₁.mp l)) - ) - ⟨a, c, h₁.mp ≫ np⟩ -, - λ⟨a,c,nl⟩ _ ↦ false_elim ( - h₂.mpr - ⟨a, c, h₁.mpr ≫ nl⟩ - λ_ _ ↦ c - ) -⟩ -``` -The thing to notice here is that this long-form solution needs both `h₁.mp` and `h₁.mpr`. Keep in mind that though it’s often tempting to try to use conditionals (`→`), rewrite **requires** a biconditional (`↔`) to work. -" +/-- Tactic Proof -/ +example (P Q R : Prop) (h1 : Q ↔ R)(h2 : P → Q) : P → R := by + intro p + apply h1.mp + apply h2 + assumption diff --git a/Game/Levels/IffIntro/L04.lean b/Game/Levels/IffIntro/L04.lean index 8d92b17..b361677 100644 --- a/Game/Levels/IffIntro/L04.lean +++ b/Game/Levels/IffIntro/L04.lean @@ -4,50 +4,24 @@ open GameLogic World "IffIntro" Level 4 -Title "Rewriting" +Title "Iff_Intro" -NewTheorem - GameLogic.and_assoc - GameLogic.or_assoc +OnlyTactic + exact + «have» Introduction " -# Keep rewriting! -It's another round of the resistance! This time you know that if you could prove that Alarfil, Cyna, or Lippa are part of the resistance, then that would be good enough to show that least one of the other two are spies.\\ -\\ -It doesn't really matter how your friends are paired up, the same truth will hold. -# Proposition Key: -- A — Alarfil is a member of the resistance -- C — Cyna is a member of the resistance -- L — Lippa is a member of the resistance -## new theorems -Two new theorems have been unlocked for this level. We'll make you prove them later — though I imagine they make a certain amount of intuitive sense regardless. -1. `or_assoc : P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R` -2. `and_assoc : P ∧ Q ∧ R ↔ (P ∧ Q) ∧ R` +# Left-Hand Swap +You'll need `h1.mpr` in order to turn evidence for R into evidence for P " -/-- Exactly 2 rewrites -/ -Statement (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by - rw [or_assoc, and_assoc] - exact h +/-- Statement -/ +Statement (P Q R : Prop) (h1 : P ↔ R)(h2 : P → Q) : R → Q := by + exact λr ↦ h2 (h1.mpr r) -example (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by - exact imp_trans - (λpvqvr ↦ h (or_elim pvqvr - (λp ↦ or_inl (or_inl p)) - (λqvr ↦ or_elim qvr - (λq ↦ or_inl (or_inr q)) - (λr ↦ or_inr r)) - )) - λnpqr pqr ↦ npqr ( - and_intro ( - and_intro pqr.left pqr.right.left - ) pqr.right.right - ) - -example (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by - exact or_assoc.mp ≫ h ≫ imp_trans and_assoc.mp - - -Conclusion " -Onward and upward -" +/-- Tactic Proof -/ +example (P Q R : Prop) (h1 : P ↔ R)(h2 : P → Q) : R → Q := by + intro r + apply h2 + apply h1.mpr + assumption diff --git a/Game/Levels/IffIntro/L05.lean b/Game/Levels/IffIntro/L05.lean new file mode 100644 index 0000000..8db737c --- /dev/null +++ b/Game/Levels/IffIntro/L05.lean @@ -0,0 +1,122 @@ +import Game.Metadata + +open GameLogic + +World "IffIntro" +Level 5 +Title "Rewriting" + +NewTactic rw +NewHiddenTactic nth_rewrite +OnlyTactic + exact + «have» + rw + «repeat» + nth_rewrite + +Introduction " +# Rewrite the goal +## To an extreme +You're playing a round of *The Resistance*. You've been diligently figuring out who is a member of the resistance and who is a spy. It's a bit complicated, but you've reasoned that the current state of affairs is possible if and only if Alarfil and Cyna are members of the resistance and Pippin is a spy. You also know from an earlier reveal that Pippin and Lippa must be on the same team. Therefore, the same argument applies to Lippa as well. +# Proposition Key: +- A — Alarfil is a member of the resistance +- C — Cyna is a member of the resistance +- L — Lippa is a member of the resistance +- P — Pippin is a member of the resistance +# The `rw` tactic +Depending on the order you've chosen to do the tutorial worlds, you may not yet be familiar with all the symbols in the current proof state. In fact, you may not even have unlocked the tools in your inventory necessary to complete this level. Don't worry, the rewrite tactic makes this level a breeze.\\ +\\ +First, take a look at the proof state and notice that `h₂` and the Goal are extremely similar. In fact, if you replace every occurrence of `L` with `P`, then the two would be identical. That's where `rw` comes in. +\\ +If you have `hpq : P ↔ Q` then `rw [hpq]` will change all `P`s in the goal to `Q`s. It's the way to “substitute in”.\\ +\\ +The `rw` tactic is an automation tool. It does the rote work of taking apart an expression, looking for a matching sub-expression, swapping in the equivalent sub-expression and then constructing the new equivalent term from there.\\ +\\ +Try it out! +" + +/-- Who is loyal, who is a spy? -/ +Statement + (A C L P : Prop) + (h1 : L ↔ P) + (h2 : ¬((A → C ∨ ¬P) ∧ (P ∨ A → ¬C) → (P → C)) ↔ A ∧ C ∧ ¬P) + : ¬((A → C ∨ ¬L) ∧ (L ∨ A → ¬C) → (L → C)) ↔ A ∧ C ∧ ¬L := by + rw [h1] + exact h2 + +example + (A C L P : Prop) + (h1 : L ↔ P) + (h2 : ¬((A → C ∨ ¬P) ∧ (P ∨ A → ¬C) → (P → C)) ↔ A ∧ C ∧ ¬P) + : ¬((A → C ∨ ¬L) ∧ (L ∨ A → ¬C) → (L → C)) ↔ A ∧ C ∧ ¬L := by + rw [← h1] at h2 + exact h2 + +example + (A C L P : Prop) (h1 : L ↔ P) + (h2 : ¬((A → C ∨ ¬P) ∧ (P ∨ A → ¬C) → (P → C)) ↔ A ∧ C ∧ ¬P) + : ¬((A → C ∨ ¬L) ∧ (L ∨ A → ¬C) → (L → C)) ↔ A ∧ C ∧ ¬L := + ⟨ + λh3 ↦ have ⟨a,c,np⟩ := h2.mp ( + λh₄ ↦ h3 (λ⟨hl₅,hr₅⟩ l ↦ h₄ ⟨ + λa ↦ or_elim + (hl₅ a) + or_inl + (imp_trans h1.mpr ≫ or_inr) + , + λ_ ↦ hr₅ (or_inl l) + ⟩ (h1.mp l)) + ) + ⟨a, c, h1.mp ≫ np⟩ + , + λ⟨a,c,nl⟩ _ ↦ false_elim ( + h2.mpr + ⟨a, c, h1.mpr ≫ nl⟩ + λ_ _ ↦ c + ) + ⟩ + +Conclusion " +Oh, how nice! A fast solution to a complex problem. + +---- +If you've read the inventory page for `rw`, you may have seen another solution too. You can use the backwards arrow “`←`” to change `P`s to `L`s instead of `L`s to `P`s. Also, you can change a hypothesis instead of the goal. +``` +rw [← h₁] at h₂ +exact h₂ +``` + +Here's an example of what this looks like without the `rw` tactic — if you want to try this solution, copy & paste the following text to the editor input mode. +``` +exact ⟨ + λh₃ ↦ have ⟨a,c,np⟩ := h₂.mp ( + λh₄ ↦ h₃ (λ⟨hl₅,hr₅⟩ l ↦ h₄ ⟨ + λa ↦ or_elim + (hl₅ a) + or_inl + (imp_trans h₁.mpr ≫ or_inr) + , + λ_ ↦ hr₅ (or_inl l) + ⟩ (h₁.mp l)) + ) + ⟨a, c, h₁.mp ≫ np⟩ +, + λ⟨a,c,nl⟩ _ ↦ false_elim ( + h₂.mpr + ⟨a, c, h₁.mpr ≫ nl⟩ + λ_ _ ↦ c + ) +⟩ +``` +The thing to notice here is that this long-form solution needs both `h₁.mp` and `h₁.mpr`. Keep in mind that though it’s often tempting to try to use conditionals (`→`), rewrite **requires** a biconditional (`↔`) to work. +" + +/-- Tactic Proof -/ +example + (A C L P : Prop) + (h1 : L ↔ P) + (h2 : ¬((A → C ∨ ¬P) ∧ (P ∨ A → ¬C) → (P → C)) ↔ A ∧ C ∧ ¬P) + : ¬((A → C ∨ ¬L) ∧ (L ∨ A → ¬C) → (L → C)) ↔ A ∧ C ∧ ¬L := by + rw [h1] + assumption diff --git a/Game/Levels/IffIntro/L06.lean b/Game/Levels/IffIntro/L06.lean new file mode 100644 index 0000000..cde48cf --- /dev/null +++ b/Game/Levels/IffIntro/L06.lean @@ -0,0 +1,77 @@ +import Game.Metadata + +namespace GameLogic + +World "IffIntro" +Level 6 +Title "Rewriting" + +NewTheorem + GameLogic.and_assoc + GameLogic.or_assoc +OnlyTactic + exact + «have» + rw + «repeat» + nth_rewrite + +Introduction " +# Keep rewriting! +It's another round of the resistance! This time you know that if you could prove that Alarfil, Cyna, or Lippa are part of the resistance, then that would be good enough to show that least one of the other two are spies.\\ +\\ +It doesn't really matter how your friends are paired up, the same truth will hold. +# Proposition Key: +- A — Alarfil is a member of the resistance +- C — Cyna is a member of the resistance +- L — Lippa is a member of the resistance +## new theorems +Two new theorems have been unlocked for this level. We'll make you prove them later — though I imagine they make a certain amount of intuitive sense regardless. +1. `or_assoc : P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R` +2. `and_assoc : P ∧ Q ∧ R ↔ (P ∧ Q) ∧ R` +" + +/-- Exactly 2 rewrites -/ +Statement (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by + rw [or_assoc, and_assoc] + exact h + +example (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by + exact imp_trans + (λpvqvr ↦ h (or_elim pvqvr + (λp ↦ or_inl (or_inl p)) + (λqvr ↦ or_elim qvr + (λq ↦ or_inl (or_inr q)) + (λr ↦ or_inr r)) + )) + λnpqr pqr ↦ npqr ( + and_intro ( + and_intro pqr.left pqr.right.left + ) pqr.right.right + ) + +example (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by + exact or_assoc.mp ≫ h ≫ imp_trans and_assoc.mp + +Conclusion " +``` +rw [or_assoc] +rw [and_assoc] +exact h +``` +---- +``` +rw [or_assoc, and_assoc] +exact h +``` +---- +``` +exact or_assoc.mp ≫ h ≫ imp_trans and_assoc.mp + +``` +" + +/-- Tactic Proof -/ +example (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by + rw [or_assoc, and_assoc] + assumption diff --git a/Game/Levels/IffTactic.lean b/Game/Levels/IffTactic.lean new file mode 100644 index 0000000..28b01ce --- /dev/null +++ b/Game/Levels/IffTactic.lean @@ -0,0 +1,16 @@ +import Game.Levels.IffTactic.L01 +import Game.Levels.IffTactic.L02 +import Game.Levels.IffTactic.L03 +import Game.Levels.IffTactic.L04 +import Game.Levels.IffTactic.L05 +import Game.Levels.IffTactic.L06 + +World "IffTactic" +Title "Redux: ↔ World Tactics" + +Introduction " +# Redux: ↔ World Tactics +Welcome to the redux of the **↔ Tutorial World**. Every level is the same, but instead of solving each level with `have` and `exact`, this world opens up a bunch of custom tactics.\\ +\\ +This world introduces tactics that you can use in lieu of the expressions you've learned so far. +" diff --git a/Game/Levels/IffTactic/L01.lean b/Game/Levels/IffTactic/L01.lean new file mode 100755 index 0000000..2cb5955 --- /dev/null +++ b/Game/Levels/IffTactic/L01.lean @@ -0,0 +1,47 @@ +import Game.Metadata + +open GameLogic + +World "IffTactic" +Level 1 +Title "Iff_Intro" + +NewTheorem GameLogic.iff_intro +NewDefinition GameLogic.iff_def +OnlyTactic + exact + «have» + +Introduction " +# Coupled Conditionals +Sybeth and Alarfil are a couple. In effect, this means that if Sybeth is playing a party game, then Alarfil is playing too and vise versa. Therefore Sybeth is playing Charades if and only if Alarfil playing. +# Proposition Key: +- J — Alarfil is playing Charades +- S — Sybeth is playing Charades +# Unlocked `↔ intro` +Assuming `e₁ : P → Q` and `e₂ : Q → P`, you can introduce a biconditional with `have h := iff_intro e₁ e₂`, though the anonymous constructor syntax works just like it does for conjunctions: `have h : P ↔ Q := ⟨e₁, e₂⟩` +" + +/-- Statement -/ +Statement (J S : Prop) (hsj: S → J) (hjs: J → S) : S ↔ J := by + exact iff_intro hsj hjs + +example (J S : Prop) (hsj: S → J) (hjs: J → S) : S ↔ J := by + exact ⟨hsj, hjs⟩ + +Conclusion " +Onward and upward + +---- +``` +exact iff_intro hsj hjs +``` +--- +``` +exact ⟨hsj, hjs⟩ +``` +" + +/-- Tactic Proof -/ +example (J S : Prop) (hsj: S → J) (hjs: J → S) : S ↔ J := by + constructor <;> assumption diff --git a/Game/Levels/IffTactic/L02.lean b/Game/Levels/IffTactic/L02.lean new file mode 100644 index 0000000..479819d --- /dev/null +++ b/Game/Levels/IffTactic/L02.lean @@ -0,0 +1,35 @@ +import Game.Metadata + +open GameLogic + +World "IffTactic" +Level 2 +Title "Conjuctive Iff" + +NewTheorem + GameLogic.iff_mp + GameLogic.iff_mpr +OnlyTactic + exact + «have» + +Introduction " +# Two sides to every coin +You're flipping a coin to decide which team gets to guess first in *Salad Bowl*. Heads means blue team and tails means purple team. Even though you're on the purple team, you're secretly hoping it comes up heads. +# Proposition Key: +- B — Blue Team goes first +- P — Purple Team goes First +# Unlocked `iff_mp` and `iff_mpr` +For a biconditional like `h : P ↔ Q`, +1. You can extract `P → Q` using `iff_mp h` or `h.mp`. `mp` here is short of modus ponens. +2. You can extra `Q → P` using `iff_mpr h` or `h.mpr`. `mpr` here is short of modus ponens reversed. +" + +/-- Statement -/ +Statement (B P : Prop) (h : B ↔ ¬P) : (B → ¬P) ∧ (¬P → B) := by + exact and_intro (iff_mp h) (iff_mpr h) + +/-- Tactic Proof -/ +example (B P : Prop) (h : B ↔ ¬P) : (B → ¬P) ∧ (¬P → B) := by + cases h + constructor <;> assumption diff --git a/Game/Levels/IffTactic/L03.lean b/Game/Levels/IffTactic/L03.lean new file mode 100644 index 0000000..fb51d3b --- /dev/null +++ b/Game/Levels/IffTactic/L03.lean @@ -0,0 +1,27 @@ +import Game.Metadata + +open GameLogic + +World "IffTactic" +Level 3 +Title "Iff_mp" + +OnlyTactic + exact + «have» + +Introduction " +# Right-Hand Swap +You'll need h1.mp in order to turn evidence for Q into evidence for R +" + +/-- Statement -/ +Statement (P Q R : Prop) (h1 : Q ↔ R)(h2 : P → Q) : P → R := by + exact λp ↦ h1.mp (h2 p) + +/-- Tactic Proof -/ +example (P Q R : Prop) (h1 : Q ↔ R)(h2 : P → Q) : P → R := by + intro p + apply h1.mp + apply h2 + assumption diff --git a/Game/Levels/IffTactic/L04.lean b/Game/Levels/IffTactic/L04.lean new file mode 100644 index 0000000..c58e300 --- /dev/null +++ b/Game/Levels/IffTactic/L04.lean @@ -0,0 +1,27 @@ +import Game.Metadata + +open GameLogic + +World "IffTactic" +Level 4 +Title "Iff_Intro" + +OnlyTactic + exact + «have» + +Introduction " +# Left-Hand Swap +You'll need `h1.mpr` in order to turn evidence for R into evidence for P +" + +/-- Statement -/ +Statement (P Q R : Prop) (h1 : P ↔ R)(h2 : P → Q) : R → Q := by + exact λr ↦ h2 (h1.mpr r) + +/-- Tactic Proof -/ +example (P Q R : Prop) (h1 : P ↔ R)(h2 : P → Q) : R → Q := by + intro r + apply h2 + apply h1.mpr + assumption diff --git a/Game/Levels/IffTactic/L05.lean b/Game/Levels/IffTactic/L05.lean new file mode 100644 index 0000000..f60fa3f --- /dev/null +++ b/Game/Levels/IffTactic/L05.lean @@ -0,0 +1,122 @@ +import Game.Metadata + +open GameLogic + +World "IffTactic" +Level 5 +Title "Rewriting" + +NewTactic rw +NewHiddenTactic nth_rewrite +OnlyTactic + exact + «have» + rw + «repeat» + nth_rewrite + +Introduction " +# Rewrite the goal +## To an extreme +You're playing a round of *The Resistance*. You've been diligently figuring out who is a member of the resistance and who is a spy. It's a bit complicated, but you've reasoned that the current state of affairs is possible if and only if Alarfil and Cyna are members of the resistance and Pippin is a spy. You also know from an earlier reveal that Pippin and Lippa must be on the same team. Therefore, the same argument applies to Lippa as well. +# Proposition Key: +- A — Alarfil is a member of the resistance +- C — Cyna is a member of the resistance +- L — Lippa is a member of the resistance +- P — Pippin is a member of the resistance +# The `rw` tactic +Depending on the order you've chosen to do the tutorial worlds, you may not yet be familiar with all the symbols in the current proof state. In fact, you may not even have unlocked the tools in your inventory necessary to complete this level. Don't worry, the rewrite tactic makes this level a breeze.\\ +\\ +First, take a look at the proof state and notice that `h₂` and the Goal are extremely similar. In fact, if you replace every occurrence of `L` with `P`, then the two would be identical. That's where `rw` comes in. +\\ +If you have `hpq : P ↔ Q` then `rw [hpq]` will change all `P`s in the goal to `Q`s. It's the way to “substitute in”.\\ +\\ +The `rw` tactic is an automation tool. It does the rote work of taking apart an expression, looking for a matching sub-expression, swapping in the equivalent sub-expression and then constructing the new equivalent term from there.\\ +\\ +Try it out! +" + +/-- Who is loyal, who is a spy? -/ +Statement + (A C L P : Prop) + (h1 : L ↔ P) + (h2 : ¬((A → C ∨ ¬P) ∧ (P ∨ A → ¬C) → (P → C)) ↔ A ∧ C ∧ ¬P) + : ¬((A → C ∨ ¬L) ∧ (L ∨ A → ¬C) → (L → C)) ↔ A ∧ C ∧ ¬L := by + rw [h1] + exact h2 + +example + (A C L P : Prop) + (h1 : L ↔ P) + (h2 : ¬((A → C ∨ ¬P) ∧ (P ∨ A → ¬C) → (P → C)) ↔ A ∧ C ∧ ¬P) + : ¬((A → C ∨ ¬L) ∧ (L ∨ A → ¬C) → (L → C)) ↔ A ∧ C ∧ ¬L := by + rw [← h1] at h2 + exact h2 + +example + (A C L P : Prop) (h1 : L ↔ P) + (h2 : ¬((A → C ∨ ¬P) ∧ (P ∨ A → ¬C) → (P → C)) ↔ A ∧ C ∧ ¬P) + : ¬((A → C ∨ ¬L) ∧ (L ∨ A → ¬C) → (L → C)) ↔ A ∧ C ∧ ¬L := + ⟨ + λh3 ↦ have ⟨a,c,np⟩ := h2.mp ( + λh₄ ↦ h3 (λ⟨hl₅,hr₅⟩ l ↦ h₄ ⟨ + λa ↦ or_elim + (hl₅ a) + or_inl + (imp_trans h1.mpr ≫ or_inr) + , + λ_ ↦ hr₅ (or_inl l) + ⟩ (h1.mp l)) + ) + ⟨a, c, h1.mp ≫ np⟩ + , + λ⟨a,c,nl⟩ _ ↦ false_elim ( + h2.mpr + ⟨a, c, h1.mpr ≫ nl⟩ + λ_ _ ↦ c + ) + ⟩ + +Conclusion " +Oh, how nice! A fast solution to a complex problem. + +---- +If you've read the inventory page for `rw`, you may have seen another solution too. You can use the backwards arrow “`←`” to change `P`s to `L`s instead of `L`s to `P`s. Also, you can change a hypothesis instead of the goal. +``` +rw [← h₁] at h₂ +exact h₂ +``` + +Here's an example of what this looks like without the `rw` tactic — if you want to try this solution, copy & paste the following text to the editor input mode. +``` +exact ⟨ + λh₃ ↦ have ⟨a,c,np⟩ := h₂.mp ( + λh₄ ↦ h₃ (λ⟨hl₅,hr₅⟩ l ↦ h₄ ⟨ + λa ↦ or_elim + (hl₅ a) + or_inl + (imp_trans h₁.mpr ≫ or_inr) + , + λ_ ↦ hr₅ (or_inl l) + ⟩ (h₁.mp l)) + ) + ⟨a, c, h₁.mp ≫ np⟩ +, + λ⟨a,c,nl⟩ _ ↦ false_elim ( + h₂.mpr + ⟨a, c, h₁.mpr ≫ nl⟩ + λ_ _ ↦ c + ) +⟩ +``` +The thing to notice here is that this long-form solution needs both `h₁.mp` and `h₁.mpr`. Keep in mind that though it’s often tempting to try to use conditionals (`→`), rewrite **requires** a biconditional (`↔`) to work. +" + +/-- Tactic Proof -/ +example + (A C L P : Prop) + (h1 : L ↔ P) + (h2 : ¬((A → C ∨ ¬P) ∧ (P ∨ A → ¬C) → (P → C)) ↔ A ∧ C ∧ ¬P) + : ¬((A → C ∨ ¬L) ∧ (L ∨ A → ¬C) → (L → C)) ↔ A ∧ C ∧ ¬L := by + rw [h1] + assumption diff --git a/Game/Levels/IffTactic/L06.lean b/Game/Levels/IffTactic/L06.lean new file mode 100644 index 0000000..e20fc20 --- /dev/null +++ b/Game/Levels/IffTactic/L06.lean @@ -0,0 +1,77 @@ +import Game.Metadata + +namespace GameLogic + +World "IffTactic" +Level 6 +Title "Rewriting" + +NewTheorem + GameLogic.and_assoc + GameLogic.or_assoc +OnlyTactic + exact + «have» + rw + «repeat» + nth_rewrite + +Introduction " +# Keep rewriting! +It's another round of the resistance! This time you know that if you could prove that Alarfil, Cyna, or Lippa are part of the resistance, then that would be good enough to show that least one of the other two are spies.\\ +\\ +It doesn't really matter how your friends are paired up, the same truth will hold. +# Proposition Key: +- A — Alarfil is a member of the resistance +- C — Cyna is a member of the resistance +- L — Lippa is a member of the resistance +## new theorems +Two new theorems have been unlocked for this level. We'll make you prove them later — though I imagine they make a certain amount of intuitive sense regardless. +1. `or_assoc : P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R` +2. `and_assoc : P ∧ Q ∧ R ↔ (P ∧ Q) ∧ R` +" + +/-- Exactly 2 rewrites -/ +Statement (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by + rw [or_assoc, and_assoc] + exact h + +example (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by + exact imp_trans + (λpvqvr ↦ h (or_elim pvqvr + (λp ↦ or_inl (or_inl p)) + (λqvr ↦ or_elim qvr + (λq ↦ or_inl (or_inr q)) + (λr ↦ or_inr r)) + )) + λnpqr pqr ↦ npqr ( + and_intro ( + and_intro pqr.left pqr.right.left + ) pqr.right.right + ) + +example (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by + exact or_assoc.mp ≫ h ≫ imp_trans and_assoc.mp + +Conclusion " +``` +rw [or_assoc] +rw [and_assoc] +exact h +``` +---- +``` +rw [or_assoc, and_assoc] +exact h +``` +---- +``` +exact or_assoc.mp ≫ h ≫ imp_trans and_assoc.mp + +``` +" + +/-- Tactic Proof -/ +example (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by + rw [or_assoc, and_assoc] + assumption diff --git a/Game/Levels/ImpIntro.lean b/Game/Levels/ImpIntro.lean index be91119..94c12bb 100755 --- a/Game/Levels/ImpIntro.lean +++ b/Game/Levels/ImpIntro.lean @@ -20,7 +20,9 @@ This world teaches you about conditional statements. In every day sentences, you \\ This game uses the implication arrow “ → ”. “If A, then B” is the same as “A implies B” or “`A → B`”.\\ \\ -So far, we've been giving our evidence and propositions real-world analogues. What would constitute evidence for a conditional statement? For example; “If we have gnocchi, butter, parmesan, and black pepper, then we can cook *gnocchi cacio e pepe*”. What would be evidence of such a statement? An example of evidence of that could be a recipe with cooking instructions. You can think of the recipe as an argument explaining that the given ingredients are sufficient to be able to cook the dish.\\ +So far, we've been giving our evidence and propositions real-world analogues. Doing this is a bit less desirable with conditionals as real-world evidence is often based on our understanding and not some tangible object. For example; the evidence that “If it rained, then the driveway is wet” generally doesn't come in the form of peer-reviewed physics papers. You should be thinking of the flavour text for each level as an unrefined embellishment of the symbols you're actually concerned with.\\ +\\ +That said, at the level the favour text works on, what would constitute evidence for a conditional statement? Well, for example; “If we have gnocchi, butter, parmesan, and black pepper, then we can cook *gnocchi cacio e pepe*”. An example of evidence for such a conditional could be a recipe with cooking instructions. You can think of the recipe as an argument explaining that the given ingredients are sufficient to be able to cook the dish.\\ \\ Another example might be a safe's combination, as evidence that “I can find the hidden safe” → “I can steal the contents of the safe”. Perhaps a certification is evidence that “I won the contract” → “I will renovate the client's yard”.\\ \\ @@ -28,5 +30,5 @@ The concept behind an implication, such as `A → B`, is that there exists an ex \\ Where this game abstracted the idea of `A ∧ B` into a tuple holding evidence for `A` and evidence for `B`. The way we store evidence like `A → B` is with a function that takes evidence for `A` and produces evidence for `B`.\\ \\ -`h : A → B` reads `h` is evidence for `A → B`. While real-world analogues can be anything, the abstract machinery used in this game will always be a function. +`h : A → B` reads `h` is evidence for `A → B`. While real-world analogues can be anything, the formalization used in this game will always be a function. " diff --git a/Game/Levels/ImpIntro/L01.lean b/Game/Levels/ImpIntro/L01.lean index e8574c2..5178ecc 100755 --- a/Game/Levels/ImpIntro/L01.lean +++ b/Game/Levels/ImpIntro/L01.lean @@ -8,6 +8,9 @@ Title "Cake Delivery Service" NewDefinition GameLogic.FunElim NewTheorem GameLogic.modus_ponens +OnlyTactic + exact + «have» Introduction " # Let there be cake! diff --git a/Game/Levels/ImpIntro/L02.lean b/Game/Levels/ImpIntro/L02.lean index b4be6ee..fff06e0 100755 --- a/Game/Levels/ImpIntro/L02.lean +++ b/Game/Levels/ImpIntro/L02.lean @@ -7,6 +7,9 @@ Level 2 Title "Identity" NewDefinition GameLogic.FunIntro +OnlyTactic + exact + «have» Introduction " # Is it Cake!? diff --git a/Game/Levels/ImpIntro/L03.lean b/Game/Levels/ImpIntro/L03.lean index 5ed31de..9059595 100755 --- a/Game/Levels/ImpIntro/L03.lean +++ b/Game/Levels/ImpIntro/L03.lean @@ -7,6 +7,9 @@ Level 3 Title "Cake Form Swap" NewTheorem GameLogic.identity +OnlyTactic + exact + «have» Introduction " # Trouble with the cake @@ -18,7 +21,7 @@ If you assume an arbitrary cake that has icing and that has sprinkles, show that - `S` — The cake has **S**prinkles " -/-- Show that ∧ is commutative --/ +/-- Show that ∧ is commutative -/ Statement (I S: Prop) : I ∧ S → S ∧ I := by Hint (hidden := true) "`λ h : I ∧ S ↦ and_intro (and_right h) h.left`" exact λ(h : I ∧ S) ↦ and_intro (and_right h) h.left diff --git a/Game/Levels/ImpIntro/L04.lean b/Game/Levels/ImpIntro/L04.lean index 933a54c..71b824e 100755 --- a/Game/Levels/ImpIntro/L04.lean +++ b/Game/Levels/ImpIntro/L04.lean @@ -7,6 +7,9 @@ Level 4 Title "Chain Reasoning" NewTheorem GameLogic.and_comm +OnlyTactic + exact + «have» Introduction " # A Chain of Reasoning @@ -25,8 +28,8 @@ This is the transitive property of `<`. You should be able to show that this sam " /-- Show that → is transitive -/ -Statement (C A S: Prop) (h₁ : C → A) (h₂ : A → S) : C → S := by - exact λ(c: C) ↦ h₂ (h₁ c) +Statement (C A S: Prop) (h1 : C → A) (h2 : A → S) : C → S := by + exact λ(c: C) ↦ h2 (h1 c) -- Example using infix application to drop a pair of brackets. example (C A S: Prop) (h₁ : C → A) (h₂ : A → S) : C → S := by diff --git a/Game/Levels/ImpIntro/L05.lean b/Game/Levels/ImpIntro/L05.lean index 83dfc68..1716e31 100755 --- a/Game/Levels/ImpIntro/L05.lean +++ b/Game/Levels/ImpIntro/L05.lean @@ -7,6 +7,9 @@ Level 5 Title "Riffin Snacks" NewTheorem GameLogic.imp_trans +OnlyTactic + exact + «have» Introduction " # Is Riffin bringing something? @@ -45,8 +48,8 @@ The Precedence definition page explains that function application is left-associ " /-- Riffin is bringing a unicorn snack -/ -Statement (P Q R S T U: Prop) (p : P) (h₁ : P → Q) (h₂ : Q → R) (h₃ : Q → T) (h₄ : S → T) (h₅ : T → U) : U := by - exact (h₁ ≫ h₃ ≫ h₅) p +Statement (P Q R S T U: Prop) (p : P) (h1 : P → Q) (h2 : Q → R) (h3 : Q → T) (h4 : S → T) (h5 : T → U) : U := by + exact (h1 ≫ h3 ≫ h5) p -- One application at a time example (P Q R S T U: Prop) (p : P) (h₁ : P → Q) (h₂ : Q → R) (h₃ : Q → T) (h₄ : S → T) (h₅ : T → U) : U := by diff --git a/Game/Levels/ImpIntro/L06.lean b/Game/Levels/ImpIntro/L06.lean index 0a14b4d..6d02306 100755 --- a/Game/Levels/ImpIntro/L06.lean +++ b/Game/Levels/ImpIntro/L06.lean @@ -6,6 +6,10 @@ World "ImpIntro" Level 6 Title "and_imp" +OnlyTactic + exact + «have» + Introduction " # Curry If you've got chips and dip, then you've got a popular party snack! This is undeniable.\\ @@ -17,9 +21,12 @@ Therefore if you've got chips, then if you've got dip, then you've got a popular - `S` — You've got a popular party snack " -/-- Conjunction interacting with implication --/ -Statement (P Q R: Prop) (h : P ∧ Q → R) : P → Q → R := by - exact λp ↦ and_intro p ≫ h +/-- Conjunction interacting with implication -/ +Statement (C D S: Prop) (h : C ∧ D → S) : C → D → S := by + exact λc ↦ and_intro c ≫ h + +example (C D S: Prop) (h : C ∧ D → S) : C → D → S := by + exact λc d ↦ h (and_intro c d) Conclusion " Cool. Chips and Dip! diff --git a/Game/Levels/ImpIntro/L07.lean b/Game/Levels/ImpIntro/L07.lean index d68a4ba..d22b594 100755 --- a/Game/Levels/ImpIntro/L07.lean +++ b/Game/Levels/ImpIntro/L07.lean @@ -6,6 +6,10 @@ World "ImpIntro" Level 7 Title "and_imp 2" +OnlyTactic + exact + «have» + Introduction " # Un-Curry If you've got chips, then if you've got dip, then you've got a popular party snack.\\ @@ -17,9 +21,12 @@ Therefore, if you've got chips and dip, then you've got a popular party snack! - `S` — You've got a popular party snack " -/-- Conjunction interacting with implication --/ -Statement (P Q R: Prop) (h : P → Q → R) : P ∧ Q → R := by - exact λ(pq: P ∧ Q) ↦ h pq.left pq.right +/-- Conjunction interacting with implication -/ +Statement (C D S: Prop) (h : C → D → S) : C ∧ D → S := by + exact λ(cd: C ∧ D) ↦ h cd.left cd.right + +example (C D S: Prop) (h : C → D → S) : C ∧ D → S := by + exact λ⟨c, d⟩ ↦ h c d Conclusion " Cool. Chips and Dip for sure! diff --git a/Game/Levels/ImpIntro/L08.lean b/Game/Levels/ImpIntro/L08.lean index c93fdc4..7a19463 100755 --- a/Game/Levels/ImpIntro/L08.lean +++ b/Game/Levels/ImpIntro/L08.lean @@ -6,6 +6,10 @@ World "ImpIntro" Level 8 Title "Distribute" +OnlyTactic + exact + «have» + Introduction " # Go buy chips and dip! - If you go shopping, then you'll buy chips. @@ -17,13 +21,12 @@ Introduction " - `S` — You go shopping " -/-- → distributes over ∧ --/ -Statement (R S : Prop) (h : (S → C) ∧ (S → D)) : S → C ∧ D := by +/-- → distributes over ∧ -/ +Statement (C D S : Prop) (h : (S → C) ∧ (S → D)) : S → C ∧ D := by exact λ(s : S) ↦ and_intro (h.left s) (h.right s) --- Should this game try to teach destructuring? It's trying --- to accomplish so much already. -example (R S : Prop) (h : (S → C) ∧ (S → D)) : S → C ∧ D := by +-- Should this game try to teach destructuring? +example (C D S : Prop) (h : (S → C) ∧ (S → D)) : S → C ∧ D := by have ⟨l,r⟩ := h exact λs ↦ ⟨l s, r s⟩ diff --git a/Game/Levels/ImpIntro/L09.lean b/Game/Levels/ImpIntro/L09.lean index 8ee7653..fcb0d04 100755 --- a/Game/Levels/ImpIntro/L09.lean +++ b/Game/Levels/ImpIntro/L09.lean @@ -6,6 +6,10 @@ World "ImpIntro" Level 9 Title "Uncertain Snacks" +OnlyTactic + exact + «have» + Introduction " # BOSS LEVEL!!! # Uncertain Snacks @@ -22,7 +26,7 @@ That's a bit convoluted, but you should be able to produce some evidence of this - `S` — Sybeth is bringing a snack " -/-- Write the nessesary nested function(s)! --/ +/-- Write the nessesary nested function(s)! -/ Statement (R S : Prop) : R → (S → R) ∧ (¬S → R) := by exact λ(r : R) ↦ and_intro (λ(_ : S) ↦ r) (λ(_ : ¬S) ↦ r) @@ -51,3 +55,10 @@ exact λ r : R ↦ ⟨λ _ : S ↦ r, λ _ : ¬S ↦ r⟩ exact λr ↦ ⟨λ_ ↦ r, λ_ ↦ r⟩ ``` " + +/-- Tactic Proof -/ +example (R S : Prop) : R → (S → R) ∧ (¬S → R) := by + intro r + constructor + intro; assumption + intro; assumption diff --git a/Game/Levels/ImpTactic.lean b/Game/Levels/ImpTactic.lean new file mode 100644 index 0000000..77582fc --- /dev/null +++ b/Game/Levels/ImpTactic.lean @@ -0,0 +1,19 @@ +import Game.Levels.ImpTactic.L01 +import Game.Levels.ImpTactic.L02 +import Game.Levels.ImpTactic.L03 +import Game.Levels.ImpTactic.L04 +import Game.Levels.ImpTactic.L05 +import Game.Levels.ImpTactic.L06 +import Game.Levels.ImpTactic.L07 +import Game.Levels.ImpTactic.L08 +import Game.Levels.ImpTactic.L09 + +World "ImpTactic" +Title "Redux: → World Tactics" + +Introduction " +# Redux: → World Tactics +Welcome to the redux of the **→ Tutorial World**. Every level is the same, but instead of solving each level with `have` and `exact`, this world opens up a bunch of custom tactics.\\ +\\ +This world introduces tactics that you can use in lieu of the expressions you've learned so far. +" diff --git a/Game/Levels/ImpTactic/L01.lean b/Game/Levels/ImpTactic/L01.lean new file mode 100755 index 0000000..fa59f92 --- /dev/null +++ b/Game/Levels/ImpTactic/L01.lean @@ -0,0 +1,25 @@ +import Game.Metadata + +open GameLogic + +World "ImpTactic" +Level 1 +Title "Apply" + +NewTactic apply + +OnlyTactic + assumption + apply + +Introduction " +# The `apply` Tactic +This tactic can be a bit confusing as it allows you to reason backwards. In this level, `h` gives us a means to get from P to Q. We can reason backwards and say, that because you have the means to turn evidence for P into evidence for Q — it suffices to show evidence for P.\\ +\\ +If you write `apply h`, you'll see that this changes your goal from `Q` to `P`. +" + +/-- `P → (P → Q) → Q` -/ +Statement (P Q: Prop)(h'₁: P)(h : P → Q) : Q := by + apply h + assumption diff --git a/Game/Levels/ImpTactic/L02.lean b/Game/Levels/ImpTactic/L02.lean new file mode 100755 index 0000000..1a95d30 --- /dev/null +++ b/Game/Levels/ImpTactic/L02.lean @@ -0,0 +1,24 @@ +import Game.Metadata + +open GameLogic + +World "ImpTactic" +Level 2 +Title "Identity" + +NewTactic intro + +OnlyTactic + assumption + intro + +Introduction " +# The `intro` Tactic +The `intro` tactic lets you define a function interactively. It introduces one or more hypotheses, optionally naming them.\\ +\\ +In this level, `intro h` does two things. First, it adds an assumption `h : P` and second, it changes your goal from `P → P` to just `P`. In this sense, `intro h` is a bit like `λh ↦ `. +" + +/-- Idenity via tactics -/ +Statement (P: Prop) : P → P := by + intro; assumption diff --git a/Game/Levels/ImpTactic/L03.lean b/Game/Levels/ImpTactic/L03.lean new file mode 100755 index 0000000..d33358b --- /dev/null +++ b/Game/Levels/ImpTactic/L03.lean @@ -0,0 +1,26 @@ +import Game.Metadata + +open GameLogic + +World "ImpTactic" +Level 3 +Title "Swapping" + +OnlyTactic + assumption + constructor + cases + intro + +Introduction " +# Nothing New +Just use what you know. Start with `intro` to give yourself an asusmption to work with +" + +/-- Show that ∧ is commutative -/ +Statement (P Q: Prop) : P ∧ Q → Q ∧ P := by + intro h + cases h + constructor + assumption + assumption diff --git a/Game/Levels/ImpTactic/L04.lean b/Game/Levels/ImpTactic/L04.lean new file mode 100755 index 0000000..c91e2ff --- /dev/null +++ b/Game/Levels/ImpTactic/L04.lean @@ -0,0 +1,24 @@ +import Game.Metadata + +open GameLogic + +World "ImpTactic" +Level 4 +Title "Apply Chain Reasoning" + +OnlyTactic + assumption + apply + intro + +Introduction " +# More practise +This level will require `apply` again. Remember that it lets you reason backwards on the goal. +" + +/-- Show that → is transitive -/ +Statement (C A S: Prop) (h1 : C → A) (h2 : A → S) : C → S := by + intro + apply h2 + apply h1 + assumption diff --git a/Game/Levels/ImpTactic/L05.lean b/Game/Levels/ImpTactic/L05.lean new file mode 100755 index 0000000..ed74666 --- /dev/null +++ b/Game/Levels/ImpTactic/L05.lean @@ -0,0 +1,31 @@ +import Game.Metadata + +open GameLogic + +World "ImpTactic" +Level 5 +Title "Apply Backwards" + +OnlyTactic + assumption + apply + intro + +Introduction " +# Follow the Graph Backwards +$$ +\\begin{CD} + P @>{h₁}>> Q @>{h₂}>> R \\\\ + @. @VV{h₃}V \\\\ + S @>>{h₄}> T @>>{h₅}> U +\\end{CD} +$$ +" + +/-- Think before you act :) -/ +Statement (P Q R S T U: Prop) (h1 : P → Q) (h2 : Q → R) (h3 : Q → T) (h4 : S → T) (h5 : T → U) : P → U := by + intro + apply h5 + apply h3 + apply h1 + assumption diff --git a/Game/Levels/ImpTactic/L06.lean b/Game/Levels/ImpTactic/L06.lean new file mode 100755 index 0000000..28b1e86 --- /dev/null +++ b/Game/Levels/ImpTactic/L06.lean @@ -0,0 +1,57 @@ +import Game.Metadata + +open GameLogic + +World "ImpTactic" +Level 6 +Title "repeat combinator" + +NewTactic «repeat» + +OnlyTactic + assumption + constructor + apply + intro + «repeat» + +Introduction " +# The `repeat` tactic combinator +Sometimes you'll find you need to use the same tactic a few times in a row. Any tactic can be repeated (until it fails) using the `repeat`.\\ +\\ +In this level, it's very like that you'll be building a conjunction from two assumptions already available in your proof state. Once you make it that far, instead of writting +``` +constructor +assumption +assumption +``` +try this instead +``` +constructor +repeat assumption +``` +" + +/-- repeat assumption -/ +Statement (P Q R: Prop) (h : P ∧ Q → R) : P → Q → R := by + intro p + intro q + apply h + constructor + repeat assumption + +/-- Tactic Proofs -/ +example (P Q R: Prop) (h : P ∧ Q → R) : P → Q → R := by + intro p + exact and_intro p ≫ h + +example (P Q R: Prop) (h : P ∧ Q → R) : P → Q → R := by + intro p + have h2 : Q → P ∧ Q := and_intro p + have h3 : Q → R := h2 ≫ h + assumption + +example (P Q R: Prop) (h : P ∧ Q → R) : P → Q → R := by + intro _ _ + apply h + constructor <;> assumption diff --git a/Game/Levels/ImpTactic/L07.lean b/Game/Levels/ImpTactic/L07.lean new file mode 100755 index 0000000..ba498c6 --- /dev/null +++ b/Game/Levels/ImpTactic/L07.lean @@ -0,0 +1,37 @@ +import Game.Metadata + +open GameLogic + +World "ImpTactic" +Level 7 +Title "Another One" + +OnlyTactic + assumption + cases + apply + intro + «repeat» + +Introduction " +# And Another One +Reverse the implication you proved last level. +# More about `apply` +What this level is showing is that you can think about `h` as a function with 2 parameters instead of a function that returns a function. The `apply` tactic implicitly understands this point of view.\\ +\\ +Once your goal is `R`, you can `apply h`. This is like saying “in order to prove R, it suffices to prove `P` and prove `Q`”. You'll notice that `apply` automatically creates the two goals for you in such cases.\\ +\\ +**Aside:** When you've been using `constructor` to build conjunctions, this has been the same thing as if you had used `apply and_intro`. You can try that out next level if you so inclined. +" + +/-- `(P → Q → R) → P ∧ Q → R` -/ +Statement (P Q R: Prop) (h : P → Q → R) : P ∧ Q → R := by + intro pq + cases pq + apply h + repeat assumption + +example (P Q R: Prop) (h : P → Q → R) : P ∧ Q → R := by + intro ⟨_,_⟩ + apply h + repeat assumption diff --git a/Game/Levels/ImpTactic/L08.lean b/Game/Levels/ImpTactic/L08.lean new file mode 100755 index 0000000..ed307b9 --- /dev/null +++ b/Game/Levels/ImpTactic/L08.lean @@ -0,0 +1,37 @@ +import Game.Metadata + +open GameLogic + +World "ImpTactic" +Level 8 +Title "Distribute" + +OnlyTactic + assumption + constructor + cases + apply + intro + +Introduction " +# Keep it up +" + +/-- `(P → Q) ∧ (P → R) → P → Q ∧ R` -/ +Statement (P Q R : Prop) (h : (P → Q) ∧ (P → R)) : P → Q ∧ R := by + intro + cases h + apply and_intro + apply left + assumption + apply right + assumption + +example (P Q R : Prop) (h : (P → Q) ∧ (P → R)) : P → Q ∧ R := by + intro + cases h + constructor + apply left + assumption + apply right + assumption diff --git a/Game/Levels/ImpTactic/L09.lean b/Game/Levels/ImpTactic/L09.lean new file mode 100755 index 0000000..6a872a6 --- /dev/null +++ b/Game/Levels/ImpTactic/L09.lean @@ -0,0 +1,28 @@ +import Game.Metadata + +open GameLogic + +World "ImpTactic" +Level 9 +Title "Implication Tactic Boss" + +OnlyTactic + assumption + constructor + intro + +Introduction " +# World's End +The home stretch, you can do it! +" + +/-- `Q → (P → Q) ∧ (¬P → Q)` -/ +Statement (P Q : Prop) : Q → (P → Q) ∧ (¬P → Q) := by + intro + constructor + intro; assumption + intro; assumption + +Conclusion " +This set of tactic-based levels is complete! +" diff --git a/Game/Levels/NotIntro.lean b/Game/Levels/NotIntro.lean index 1e7abe4..68bdb43 100755 --- a/Game/Levels/NotIntro.lean +++ b/Game/Levels/NotIntro.lean @@ -24,11 +24,11 @@ The new interesting element for this world is `False`. What is `False`? It's a p \\ Consider a real-world analogue like “Tom is an experienced beginner” or “Tom is a married bachelor”, neither can ever be true. For there to exist evidence of either, you need to throw out definitions of the words themselves.\\ \\ -An interesting corollary arises: from the premise of `False`, any proposition becomes permissible. If you're allowed to speak in gobbledygook, then you can say anything!\\ +An interesting corollary arises: from the premise of `False`, any proposition becomes permissible. If you're allowed to speak in gobbledygook, then you can say anything! ### Garbage In, Garbage out Imagine you're signing a contract of utmost importance. The terms stipulate: “Once per day, you will be given a whole number greater than 0. If the number falls below 100, you must gracefully wave your left hand; if it exceeds 90, your right hand should elegantly sway. Lastly, if the number plunges below 0, you must transform into a cucumber.”\\ \\ On casual scrutiny, one might naively conclude that adhering to this contract may involve turning into a cucumber. While that may seem impossible, a subtle loophole exists. By astutely arguing that the contract will never demand the impossible act of becoming a cucumber, you can effectively assure your compliance.\\ \\ -By signing the contract, you're agreeing that “If there appears a number that is both greater than 0 and less 0, then I will transform into a cucumber.” Your grandiose claims remain secure as they hinge on an eventuality that defies logical possibility.\\ +By signing the contract, you're agreeing that “If there appears a number that is both greater than 0 and less 0, then I will transform into a cucumber.” Your grandiose claims remain secure as they hinge on an eventuality that defies logical possibility. " diff --git a/Game/Levels/NotIntro/L01.lean b/Game/Levels/NotIntro/L01.lean index d9ab8e5..77899f9 100755 --- a/Game/Levels/NotIntro/L01.lean +++ b/Game/Levels/NotIntro/L01.lean @@ -7,6 +7,9 @@ Level 1 Title "Not False" NewDefinition GameLogic.false_def +OnlyTactic + exact + «have» Introduction " # Proof State diff --git a/Game/Levels/NotIntro/L02.lean b/Game/Levels/NotIntro/L02.lean index 7de27b9..a4182d0 100755 --- a/Game/Levels/NotIntro/L02.lean +++ b/Game/Levels/NotIntro/L02.lean @@ -7,6 +7,9 @@ Level 2 Title "False implies anything" NewTheorem GameLogic.false_elim +OnlyTactic + exact + «have» Introduction " # Sybeth's Punctuality diff --git a/Game/Levels/NotIntro/L03.lean b/Game/Levels/NotIntro/L03.lean index eab7bed..8a4933e 100755 --- a/Game/Levels/NotIntro/L03.lean +++ b/Game/Levels/NotIntro/L03.lean @@ -6,6 +6,10 @@ World "NotIntro" Level 3 Title "Double False!" +OnlyTactic + exact + «have» + Introduction " # The Ambiguous Celebration Response Your somewhat bothersome cousin just called and is asking if you're throwing your annual soirée this year. You don't want to outright lie, so you say \"I'm not not throwing the party.\" diff --git a/Game/Levels/NotIntro/L04.lean b/Game/Levels/NotIntro/L04.lean index 51275e9..b855887 100755 --- a/Game/Levels/NotIntro/L04.lean +++ b/Game/Levels/NotIntro/L04.lean @@ -6,6 +6,10 @@ World "NotIntro" Level 4 Title "Self Contradictory" +OnlyTactic + exact + «have» + Introduction " # Self Contradictory Alarfil claims Lippa is coming and Cyna claims Lippa is not coming. They can't both be right. diff --git a/Game/Levels/NotIntro/L05.lean b/Game/Levels/NotIntro/L05.lean index 09b5b6d..d94d35d 100755 --- a/Game/Levels/NotIntro/L05.lean +++ b/Game/Levels/NotIntro/L05.lean @@ -6,6 +6,10 @@ World "NotIntro" Level 5 Title "Modus Tollens" +OnlyTactic + exact + «have» + Introduction " # Modus Tollens If Bella comes to the party, she is certain to perform a bawdy song. You've assured Sybeth that there will be no bawdy songs at the event. Sybeth is disappointed to discover that Bella won't be joining. @@ -15,8 +19,8 @@ If Bella comes to the party, she is certain to perform a bawdy song. You've assu " /-- Modus Tollens. -/ -Statement (B S : Prop)(h₁ : B → S)(h₂ : ¬S) : ¬B := by - exact imp_trans h₁ h₂ +Statement (B S : Prop)(h1 : B → S)(h2 : ¬S) : ¬B := by + exact imp_trans h1 h2 Conclusion " Congradulations. Did you recognise this proof? It's actually a slightly less general version of the proof you used in the \"**→ Tutotial world, level 4**\" to show that implication is transitive. diff --git a/Game/Levels/NotIntro/L06.lean b/Game/Levels/NotIntro/L06.lean index 94d479b..3614010 100755 --- a/Game/Levels/NotIntro/L06.lean +++ b/Game/Levels/NotIntro/L06.lean @@ -7,6 +7,9 @@ Level 6 Title "Alarfil" NewTheorem GameLogic.modus_tollens +OnlyTactic + exact + «have» Introduction " # The Alarfil Effect diff --git a/Game/Levels/NotIntro/L07.lean b/Game/Levels/NotIntro/L07.lean index d39f138..8a1f094 100755 --- a/Game/Levels/NotIntro/L07.lean +++ b/Game/Levels/NotIntro/L07.lean @@ -6,6 +6,10 @@ World "NotIntro" Level 7 Title "Negation" +OnlyTactic + exact + «have» + Introduction " # The Power of negation \"Is it possible that if this is the cake you bought, then it's gonna taste horrible?\"\\ diff --git a/Game/Levels/NotIntro/L08.lean b/Game/Levels/NotIntro/L08.lean index 6b8fbb1..1286653 100755 --- a/Game/Levels/NotIntro/L08.lean +++ b/Game/Levels/NotIntro/L08.lean @@ -6,6 +6,10 @@ World "NotIntro" Level 8 Title "Negated Conjunction" +OnlyTactic + exact + «have» + Introduction " # Definitely Not Your cake order definitely has sprinkles, which means it's **not** missing sprinkles and loaded with chocolate chips diff --git a/Game/Levels/NotIntro/L09.lean b/Game/Levels/NotIntro/L09.lean index 6b9fa1a..97fb493 100755 --- a/Game/Levels/NotIntro/L09.lean +++ b/Game/Levels/NotIntro/L09.lean @@ -6,6 +6,10 @@ World "NotIntro" Level 9 Title "Implies a Negation" +OnlyTactic + exact + «have» + Introduction " # Allergy #1 Owing to his allergy, if Pippin is present, there must be no avocado at the party. Which means that we cannot have both Pippin and avacado at the party diff --git a/Game/Levels/NotIntro/L10.lean b/Game/Levels/NotIntro/L10.lean index af75447..691d20d 100755 --- a/Game/Levels/NotIntro/L10.lean +++ b/Game/Levels/NotIntro/L10.lean @@ -6,6 +6,10 @@ World "NotIntro" Level 10 Title "Conjunction Implicaiton" +OnlyTactic + exact + «have» + Introduction " # Allergy #2 We cannot have both Pippin and avacado at the party. Which means that if Pippin is attending, then there will not be any avacado. diff --git a/Game/Levels/NotIntro/L11.lean b/Game/Levels/NotIntro/L11.lean index 8ff1c1b..9d70452 100755 --- a/Game/Levels/NotIntro/L11.lean +++ b/Game/Levels/NotIntro/L11.lean @@ -6,6 +6,10 @@ World "NotIntro" Level 11 Title "not_not_not" +OnlyTactic + exact + «have» + Introduction " # Allergy: Triple Confusion Pippin is allergic to avocado. You tell him you're not *not* **not** bringing avacado!!! Pippin gives you a confused look, but after a moment of contemplation, he responds with, \"Ok, good to know.\" diff --git a/Game/Levels/NotIntro/L12.lean b/Game/Levels/NotIntro/L12.lean index 5544d9c..1423cbe 100755 --- a/Game/Levels/NotIntro/L12.lean +++ b/Game/Levels/NotIntro/L12.lean @@ -7,6 +7,9 @@ Level 12 Title "¬Intro Boss" NewTheorem GameLogic.not_not_not +OnlyTactic + exact + «have» Introduction " # BOSS Level @@ -20,7 +23,10 @@ Introduction " /-- ¬¬\"You bought this cake" -/ Statement (B C : Prop) (h : ¬(B → C)) : ¬¬B := by - exact λnb ↦ h (imp_trans nb false_elim) + exact λnb ↦ h (λb ↦ false_elim (nb b)) + +example (B C : Prop) (h : ¬(B → C)) : ¬¬B := by + exact λnb ↦ h (nb ≫ false_elim) Conclusion " These unintuitive statements highlight the inherent challenge in contemplating the *potential* existence (or definite non-existance) of implications. diff --git a/Game/Levels/NotTactic.lean b/Game/Levels/NotTactic.lean new file mode 100644 index 0000000..39b64e9 --- /dev/null +++ b/Game/Levels/NotTactic.lean @@ -0,0 +1,22 @@ +import Game.Levels.NotTactic.L01 +import Game.Levels.NotTactic.L02 +import Game.Levels.NotTactic.L03 +import Game.Levels.NotTactic.L04 +import Game.Levels.NotTactic.L05 +import Game.Levels.NotTactic.L06 +import Game.Levels.NotTactic.L07 +import Game.Levels.NotTactic.L08 +import Game.Levels.NotTactic.L09 +import Game.Levels.NotTactic.L10 +import Game.Levels.NotTactic.L11 +import Game.Levels.NotTactic.L12 + +World "NotTactic" +Title "Redux: ¬ World Tactics" + +Introduction " +# Redux: ¬ World Tactics +Welcome to the redux of the **→ Tutorial World**. Every level is the same, but instead of solving each level with `have` and `exact`, this world opens up a bunch of custom tactics.\\ +\\ +This world introduces tactics that you can use in lieu of the expressions you've learned so far. +" diff --git a/Game/Levels/NotTactic/L01.lean b/Game/Levels/NotTactic/L01.lean new file mode 100755 index 0000000..8b7a247 --- /dev/null +++ b/Game/Levels/NotTactic/L01.lean @@ -0,0 +1,22 @@ +import Game.Metadata + +open GameLogic + +World "NotTactic" +Level 1 +Title "Not False" + +OnlyTactic + assumption + intro + +Introduction " +Just like before, you need to keep in mind that `¬P` is defined as `P → False`.\\ +\\ +∴ `¬False` is actually asking for `False → False` +" + +/-- `identity` -/ +Statement: ¬False := by + intro + assumption diff --git a/Game/Levels/NotTactic/L02.lean b/Game/Levels/NotTactic/L02.lean new file mode 100755 index 0000000..aa8326f --- /dev/null +++ b/Game/Levels/NotTactic/L02.lean @@ -0,0 +1,32 @@ +import Game.Metadata + +open GameLogic + +World "NotTactic" +Level 2 +Title "Contradiction" + +NewTactic contradiction +OnlyTactic + intro + contradiction + +Introduction " +# Contradiciton +This level introduces a relatively powerful tactic. Contradiction is a finishing tactic that will look through your assumptions and discharge some of the more obvious contradictions in order to solve any goal.\\ +\\ +examples: + 1. `h : False` says `h` is evidence for `False` which is a contradiction + 2. `h₁ : P` and `h₂ : ¬P` says that P is true and not true at the same time. This is also a contradiction. +" + +/-- ¬S is enough to show S → B -/ +Statement (P Q : Prop)(h'₁ : ¬P) : P → Q := by + intro + contradiction + +example (P Q : Prop)(h'₁ : ¬P) : P → Q := by + intro + exfalso + apply h'₁ + assumption diff --git a/Game/Levels/NotTactic/L03.lean b/Game/Levels/NotTactic/L03.lean new file mode 100755 index 0000000..f65a76e --- /dev/null +++ b/Game/Levels/NotTactic/L03.lean @@ -0,0 +1,32 @@ +import Game.Metadata + +open GameLogic + +World "NotTactic" +Level 3 +Title "Double False" + +NewTactic exfalso +OnlyTactic + assumption + apply + intro + exfalso + +Introduction " +# exfalso +`exfalso` is **Contradiction**'s younger brother. Using `exfalso` turns your goal to `False`. This is the same thing as using `apply false_elim`. Using the principle that “from nonsense, follows nonsense,” if you spot a constradiction in your assumptions, you can make progress by changing your goal to `False.`\\ +\\ +Remember that because `¬P` is the same as `P → False`, you can use the `apply` tactic on evidence for `¬P` +" + +/-- not not introduction. -/ +Statement (P : Prop)(h'₁ : P) : ¬¬P := by + intro np + exfalso + apply np + assumption + +example (P : Prop)(h'₁ : P) : ¬¬P := by + intro + contradiction diff --git a/Game/Levels/NotTactic/L04.lean b/Game/Levels/NotTactic/L04.lean new file mode 100755 index 0000000..47755d9 --- /dev/null +++ b/Game/Levels/NotTactic/L04.lean @@ -0,0 +1,29 @@ +import Game.Metadata + +open GameLogic + +World "NotTactic" +Level 4 +Title "Self Contradictory" + +OnlyTactic + intro + cases + apply + assumption + +Introduction " +# Self Contradictory +You start this level with the `intro` tactic. This will add an assumption to your proof state and change your goal to `False`. +" + +/-- The law of non-self-contradiction -/ +Statement (P : Prop) : ¬(P ∧ ¬P) := by + intro pnp + cases pnp + apply right + assumption + +example (P : Prop) : ¬(P ∧ ¬P) := by + intro ⟨p, np⟩ + contradiction diff --git a/Game/Levels/NotTactic/L05.lean b/Game/Levels/NotTactic/L05.lean new file mode 100755 index 0000000..32ec527 --- /dev/null +++ b/Game/Levels/NotTactic/L05.lean @@ -0,0 +1,24 @@ +import Game.Metadata + +open GameLogic + +World "NotTactic" +Level 5 +Title "Modus Tollens" + +OnlyTactic + intro + apply + assumption + +Introduction " +# Modus Tollens +By now you're getting used to using `intro` and `apply` on negated propositions. Keep it up! +" + +/-- Modus Tollens. -/ +Statement (P Q : Prop)(h1 : P → Q)(h2 : ¬Q) : ¬P := by + intro + apply h2 + apply h1 + assumption diff --git a/Game/Levels/NotTactic/L06.lean b/Game/Levels/NotTactic/L06.lean new file mode 100755 index 0000000..99b87ee --- /dev/null +++ b/Game/Levels/NotTactic/L06.lean @@ -0,0 +1,29 @@ +import Game.Metadata + +open GameLogic + +World "NotTactic" +Level 6 +Title "Self Contradictory 2" + +NewTheorem GameLogic.modus_tollens +OnlyTactic + intro + apply + «repeat» + assumption + +Introduction " +# Another self-contradiction +If you try to `apply h` right away, you'll be stuck. You'll have to try something else first.\\ +\\ +Once your goal is to show `False`, then `apply h` seems to do something funny. It asks you to show evidence for the same goal twice. If you try to apply `P → Q → R → S` to a Goal of `S`, then apply will make you prove each parameter separately — resulting is the three sub-goals of showing `P`, showing `Q`, and showing `R`.\\ +\\ +In this level, `apply h` is applying `P → P → False` to a goal of `False`, so it follows that you'll need to show evidence for `P` twice. +" + +/-- Remember `h: P → ¬P` is actually `h : P → P → False` -/ +Statement (P : Prop) (h: P → ¬P) : ¬P := by + intro + apply h + repeat assumption diff --git a/Game/Levels/NotTactic/L07.lean b/Game/Levels/NotTactic/L07.lean new file mode 100755 index 0000000..39c5166 --- /dev/null +++ b/Game/Levels/NotTactic/L07.lean @@ -0,0 +1,23 @@ +import Game.Metadata + +open GameLogic + +World "NotTactic" +Level 7 +Title "Negation" + +OnlyTactic + intro + apply + assumption + +Introduction " +# Anonymous intro +You've likely tried this already, but you can use `intro` without following it with any identifiers. +" + +Statement (P Q : Prop) (h: ¬(P → Q)) : ¬Q := by + intro + apply h + intro + assumption diff --git a/Game/Levels/NotTactic/L08.lean b/Game/Levels/NotTactic/L08.lean new file mode 100755 index 0000000..db9a103 --- /dev/null +++ b/Game/Levels/NotTactic/L08.lean @@ -0,0 +1,30 @@ +import Game.Metadata + +open GameLogic + +World "NotTactic" +Level 8 +Title "Negated Conjunction" + +OnlyTactic + cases + intro + apply + assumption + +Introduction " +# Pattern matching tip +You can solve this level using the knowledge you've aquired so far. If you've used a language with destructuring or pattern matching before, then you can introduce and pattern-match in one step with `intro ⟨nq, p⟩`. Doing so means you won't need the `cases` tactic for this level. +" + +/-- Negation into conjuction. -/ +Statement (P Q : Prop) (h: Q) : ¬(¬Q ∧ P) := by + intro nqp + cases nqp + apply left + assumption + +example (P Q : Prop) (h: Q) : ¬(¬Q ∧ P) := by + intro ⟨nq, _⟩ + apply nq + assumption diff --git a/Game/Levels/NotTactic/L09.lean b/Game/Levels/NotTactic/L09.lean new file mode 100755 index 0000000..5fb6e6f --- /dev/null +++ b/Game/Levels/NotTactic/L09.lean @@ -0,0 +1,34 @@ +import Game.Metadata + +open GameLogic + +World "NotTactic" +Level 9 +Title "Implies a Negation" + +OnlyTactic + assumption + cases + intro + apply + «repeat» + +Introduction " +# Enjoy ⌣ +" + +/-- Show ¬(P ∧ A) -/ +Statement (P Q : Prop) (h : Q → ¬P) : ¬(Q ∧ P) := by + intro qp + cases qp + apply h + repeat assumption + +example (P Q : Prop) (h : Q → ¬P) : ¬(Q ∧ P) := by + intro ⟨_, _⟩ + apply h + repeat assumption + +Conclusion " +Did you use `intro ⟨p, a⟩` this time? +" diff --git a/Game/Levels/NotTactic/L10.lean b/Game/Levels/NotTactic/L10.lean new file mode 100755 index 0000000..83a9ff2 --- /dev/null +++ b/Game/Levels/NotTactic/L10.lean @@ -0,0 +1,38 @@ +import Game.Metadata + +open GameLogic + +World "NotTactic" +Level 10 +Title "Conjunction Implicaiton" + +OnlyTactic + assumption + intro + apply + «repeat» + +Introduction " +# Intro +Remember how `λx y ↦ ...` is just shorthand for `λx ↦ λy ↦ ...`? Well, the `intro` tactic admits the same shorthand: +``` +intro p q +``` +is just shorthand for +``` +intro p +intro q +``` +" + +/-- Show P → ¬A. -/ +Statement (P Q : Prop) (h: ¬(Q ∧ P)) : Q → ¬P := by + intro p q + apply h + constructor + repeat assumption + +example (P Q : Prop) (h: ¬(Q ∧ P)) : Q → ¬P := by + intro _ _ + apply h + constructor <;> assumption diff --git a/Game/Levels/NotTactic/L11.lean b/Game/Levels/NotTactic/L11.lean new file mode 100755 index 0000000..15e43db --- /dev/null +++ b/Game/Levels/NotTactic/L11.lean @@ -0,0 +1,25 @@ +import Game.Metadata + +open GameLogic + +World "NotTactic" +Level 11 +Title "not_not_not" + +OnlyTactic + assumption + intro + apply + +Introduction " +# False +Once your goal is false, then you can `apply h` +" + +/-- ¬A is stable. -/ +Statement (P : Prop)(h : ¬¬¬P) : ¬P := by + intro + apply h + intro np + apply np + assumption diff --git a/Game/Levels/NotTactic/L12.lean b/Game/Levels/NotTactic/L12.lean new file mode 100755 index 0000000..f7be5b3 --- /dev/null +++ b/Game/Levels/NotTactic/L12.lean @@ -0,0 +1,32 @@ +import Game.Metadata + +open GameLogic + +World "NotTactic" +Level 12 +Title "Not Tactics Boss" + +OnlyTactic + assumption + intro + apply + exfalso + contradiction + +Introduction " +# The Final “Redux: ¬ World Tactics” level +" + +Statement (B C : Prop) (h : ¬(B → C)) : ¬¬B := by + intro nb + apply h + intro b + exfalso + apply nb + assumption + +example (B C : Prop) (h : ¬(B → C)) : ¬¬B := by + intro nb + apply h + intro b + contradiction diff --git a/Game/Levels/OrIntro/L01.lean b/Game/Levels/OrIntro/L01.lean index b3960d8..ac44ce3 100755 --- a/Game/Levels/OrIntro/L01.lean +++ b/Game/Levels/OrIntro/L01.lean @@ -8,6 +8,9 @@ Title "Left Evidence" NewTheorem GameLogic.or_inl NewDefinition GameLogic.or_def +OnlyTactic + exact + «have» Introduction " # Or Introduction Left diff --git a/Game/Levels/OrIntro/L02.lean b/Game/Levels/OrIntro/L02.lean index ba41319..87c4aa2 100755 --- a/Game/Levels/OrIntro/L02.lean +++ b/Game/Levels/OrIntro/L02.lean @@ -7,6 +7,9 @@ Level 2 Title "Right Evidence" NewTheorem GameLogic.or_inr +OnlyTactic + exact + «have» Introduction " # Or Introduction Right diff --git a/Game/Levels/OrIntro/L03.lean b/Game/Levels/OrIntro/L03.lean index 72cae3a..dbe038b 100755 --- a/Game/Levels/OrIntro/L03.lean +++ b/Game/Levels/OrIntro/L03.lean @@ -7,6 +7,9 @@ Level 3 Title "Or Elimination" NewTheorem GameLogic.or_elim +OnlyTactic + exact + «have» Introduction " # Party Games @@ -33,8 +36,8 @@ have r : R := or_elim pvq pr qr " /-- `or_elim h₃ ... ...` -/ -Statement (B C I : Prop)(h₁ : C → B)(h₂ : I → B)(h₃ : C ∨ I) : B := by - exact or_elim h₃ h₁ h₂ +Statement (B C I : Prop)(h1 : C → B)(h2 : I → B)(h3 : C ∨ I) : B := by + exact or_elim h3 h1 h2 Conclusion " `or_elim` is your first 3-paramater function. The associated proposition is `or_elim : (P ∨ Q) → (P → R) → (Q → R) → R` diff --git a/Game/Levels/OrIntro/L04.lean b/Game/Levels/OrIntro/L04.lean index e3b7586..6aeaa52 100755 --- a/Game/Levels/OrIntro/L04.lean +++ b/Game/Levels/OrIntro/L04.lean @@ -6,6 +6,10 @@ World "OrIntro" Level 4 Title "Or is Commutative" +OnlyTactic + exact + «have» + Introduction " # Either way. Chocolate chip oatmeal cookies, which ingredient goes first? diff --git a/Game/Levels/OrIntro/L05.lean b/Game/Levels/OrIntro/L05.lean index 38484a2..46be2b7 100755 --- a/Game/Levels/OrIntro/L05.lean +++ b/Game/Levels/OrIntro/L05.lean @@ -7,6 +7,9 @@ Level 5 Title "Carry On Effects" NewTheorem GameLogic.or_comm +OnlyTactic + exact + «have» Introduction " # Carry On Effects @@ -18,8 +21,8 @@ R — You get a refund " /-- Implication across ∨ -/ -Statement (C J R : Prop)(h₁ : C → J)(h₂ : C ∨ R) : J ∨ R := by - exact or_elim h₂ (h₁ ≫ or_inl) or_inr +Statement (C J R : Prop)(h1 : C → J)(h2 : C ∨ R) : J ∨ R := by + exact or_elim h2 (h1 ≫ or_inl) or_inr Conclusion " Well done, you're getting good at this! diff --git a/Game/Levels/OrIntro/L06.lean b/Game/Levels/OrIntro/L06.lean index 3c6fbef..d7784bf 100755 --- a/Game/Levels/OrIntro/L06.lean +++ b/Game/Levels/OrIntro/L06.lean @@ -6,6 +6,10 @@ World "OrIntro" Level 6 Title "or distributes over and" +OnlyTactic + exact + «have» + Introduction " # A distribution of cookies You can tell the cookies are either gingersnap cookies or they're a mix of shortbread cookies and sugar cookies. diff --git a/Game/Levels/OrIntro/L07.lean b/Game/Levels/OrIntro/L07.lean index 12191a6..ffa50e0 100755 --- a/Game/Levels/OrIntro/L07.lean +++ b/Game/Levels/OrIntro/L07.lean @@ -6,6 +6,10 @@ World "OrIntro" Level 7 Title "and distributes over or" +OnlyTactic + exact + «have» + Introduction " # A distribution of cookies You can tell from the aroma that there are are gingersnap cookies. There's another smell there too. Could be shortbread cookies or sugar cookies. diff --git a/Game/Levels/OrIntro/L08.lean b/Game/Levels/OrIntro/L08.lean index d6c52b3..a81fb8d 100755 --- a/Game/Levels/OrIntro/L08.lean +++ b/Game/Levels/OrIntro/L08.lean @@ -6,6 +6,10 @@ World "OrIntro" Level 8 Title "The Implication" +OnlyTactic + exact + «have» + Introduction " # BOSS LEVEL If we summon the Kraken, then we shall assuredly perish. While that might sound ominous, consider this: if we summon the Kraken or **have icecream**, then we shall **have icecream!** or we shall perish. diff --git a/Game/Levels/OrTactic.lean b/Game/Levels/OrTactic.lean new file mode 100644 index 0000000..ec1baf3 --- /dev/null +++ b/Game/Levels/OrTactic.lean @@ -0,0 +1,18 @@ +import Game.Levels.OrTactic.L01 +import Game.Levels.OrTactic.L02 +import Game.Levels.OrTactic.L03 +import Game.Levels.OrTactic.L04 +import Game.Levels.OrTactic.L05 +import Game.Levels.OrTactic.L06 +import Game.Levels.OrTactic.L07 +import Game.Levels.OrTactic.L08 + +World "OrTactic" +Title "Redux: ∨ World Tactics" + +Introduction " +# Redux: ∨ World Tactics +Welcome to the redux of the **∨ Tutorial World**. Every level is the same, but instead of solving each level with `have` and `exact`, this world opens up a bunch of custom tactics.\\ +\\ +This world introduces tactics that you can use in lieu of the expressions you've learned so far. +" diff --git a/Game/Levels/OrTactic/L01.lean b/Game/Levels/OrTactic/L01.lean new file mode 100755 index 0000000..21b43ce --- /dev/null +++ b/Game/Levels/OrTactic/L01.lean @@ -0,0 +1,22 @@ +import Game.Metadata + +open GameLogic + +World "OrTactic" +Level 1 +Title "Left Evidence" + +NewTactic left +OnlyTactic + assumption + left + +Introduction " +# `left` tactic +If your goal is a disjunction, `left` will change your goal to the left of that disjunction, ignoring the right. +" + +/-- Go Left -/ +Statement (P Q : Prop)(h'₁ : P) : P ∨ Q := by + left + assumption diff --git a/Game/Levels/OrTactic/L02.lean b/Game/Levels/OrTactic/L02.lean new file mode 100755 index 0000000..5d9313a --- /dev/null +++ b/Game/Levels/OrTactic/L02.lean @@ -0,0 +1,22 @@ +import Game.Metadata + +open GameLogic + +World "OrTactic" +Level 2 +Title "Right Evidence" + +NewTactic right +OnlyTactic + assumption + right + +Introduction " +# `right` tactic +Can you guess how it works? +" + +/-- Go Right -/ +Statement (P Q : Prop)(h'₁ : Q) : P ∨ Q := by + right + assumption diff --git a/Game/Levels/OrTactic/L03.lean b/Game/Levels/OrTactic/L03.lean new file mode 100755 index 0000000..d27ed0a --- /dev/null +++ b/Game/Levels/OrTactic/L03.lean @@ -0,0 +1,25 @@ +import Game.Metadata + +open GameLogic + +World "OrTactic" +Level 3 +Title "Or Elimination" + +OnlyTactic + assumption + cases + apply + +Introduction " +# A new way to use the `cases` tactic +You've used cases so far as a means to take apart conjunctions like `P ∧ Q`. The same tactic works a bit differently on disjunctions. When you use `cases h3`, you'll need to show `P` assuming Q and show `P` assuming `R`. Then the game will conclude that `P` is the case regardless of which of the disjunctions are true. +" + +/-- `cases h3` -/ +Statement (P Q R : Prop)(h1 : Q → P)(h2 : R → P)(h3 : Q ∨ R) : P := by + cases h3 + apply h1 + assumption + apply h2 + assumption diff --git a/Game/Levels/OrTactic/L04.lean b/Game/Levels/OrTactic/L04.lean new file mode 100755 index 0000000..ebdaaad --- /dev/null +++ b/Game/Levels/OrTactic/L04.lean @@ -0,0 +1,26 @@ +import Game.Metadata + +open GameLogic + +World "OrTactic" +Level 4 +Title "Or is Commutative" + +OnlyTactic + assumption + cases + right + left + +Introduction " +# Cases again +Similar to last level. +" + +/-- Commutativity of “`∨`” -/ +Statement (P Q : Prop)(h : P ∨ Q) : Q ∨ P := by + cases h + right + assumption + left + assumption diff --git a/Game/Levels/OrTactic/L05.lean b/Game/Levels/OrTactic/L05.lean new file mode 100755 index 0000000..8987ace --- /dev/null +++ b/Game/Levels/OrTactic/L05.lean @@ -0,0 +1,28 @@ +import Game.Metadata + +open GameLogic + +World "OrTactic" +Level 5 +Title "Old Hat" + +NewTheorem GameLogic.or_comm +OnlyTactic + assumption + apply + left + right + +Introduction " +# Old Hat +You've got this. +" + +/-- Implication across ∨ -/ +Statement (P Q R : Prop)(h1 : P → Q)(h2 : P ∨ R) : Q ∨ R := by + cases h2 + left + apply h1 + assumption + right + assumption diff --git a/Game/Levels/OrTactic/L06.lean b/Game/Levels/OrTactic/L06.lean new file mode 100755 index 0000000..d476b46 --- /dev/null +++ b/Game/Levels/OrTactic/L06.lean @@ -0,0 +1,33 @@ +import Game.Metadata + +open GameLogic + +World "OrTactic" +Level 6 +Title "or distributes over and" + +OnlyTactic + assumption + constructor + cases + left + right + +Introduction " +# Tactics All Day Long +" + +/-- ∨ over ∧ -/ +Statement (P Q R : Prop)(h : P ∨ Q ∧ R) : (P ∨ Q) ∧ (P ∨ R) := by + cases h + constructor + left + assumption + left + assumption + cases h_1 + constructor + right + assumption + right + assumption diff --git a/Game/Levels/OrTactic/L07.lean b/Game/Levels/OrTactic/L07.lean new file mode 100755 index 0000000..d568b81 --- /dev/null +++ b/Game/Levels/OrTactic/L07.lean @@ -0,0 +1,30 @@ +import Game.Metadata + +open GameLogic + +World "OrTactic" +Level 7 +Title "and distributes over or" + +OnlyTactic + assumption + constructor + cases + left + right + «repeat» + +Introduction " +# Tactics, Tactics, Tactics +" + +/-- ∧ over ∨ -/ +Statement (P Q R : Prop)(h : P ∧ (Q ∨ R)) : (P ∧ Q) ∨ (P ∧ R) := by + cases h + cases right + left + constructor + repeat assumption + right + constructor + repeat assumption diff --git a/Game/Levels/OrTactic/L08.lean b/Game/Levels/OrTactic/L08.lean new file mode 100755 index 0000000..ef39689 --- /dev/null +++ b/Game/Levels/OrTactic/L08.lean @@ -0,0 +1,31 @@ +import Game.Metadata + +open GameLogic + +World "OrTactic" +Level 8 +Title "The Implication" + +OnlyTactic + assumption + constructor + cases + left + right + apply + intro + +Introduction " +# Final `∨` Tactic Level +This level uses most of the tactics you've learned so far. +" + +/-- Implication of ∨ -/ +Statement (P Q R : Prop)(h : Q → R) : Q ∨ P → P ∨ R := by + intro qp + cases qp + right + apply h + assumption + left + assumption diff --git a/Game/Metadata.lean b/Game/Metadata.lean index 922a5c8..ed958ef 100755 --- a/Game/Metadata.lean +++ b/Game/Metadata.lean @@ -4,7 +4,7 @@ import Game.Doc.Definitions import Game.Doc.Tactics import Game.Doc.Lemmas --- import Mathlib.Tactic +import Mathlib.Tactic -- import Game.Tactic.Induction -- import Game.Tactic.Cases diff --git a/images/logic0101.png b/images/logic0101.png new file mode 100644 index 0000000000000000000000000000000000000000..01e582b3ad1ffe753e81cd5e1b76c07264f18683 GIT binary patch literal 40264 zcmcHgg;!PI_dO0@Lb_WTk#3Rh4(X7Vl$LI|ASGP_igc%RcS?76cU`(J@jJZU-_ID& zKky7f#s%*=XYak{nrp7P!c>%G&{2p{Kp+shoUEi82n5Fu{QQW70DN!XpZE>}!30}L zNT|q3NKiUB*_&J0eg%Q(1wzT&pM*1zK9XoB^9HIdr7La-39#q>?`h3UerJZ9&FT-8@-Jbt;aW#Fr#(8Bq^o-jW2r;C?GOTJ&Xmw>ysNTSc~d+BiBDUkyH|M1DlO9~4wcHEi%$av9tC};_p4s}Ck!_@Lv z?~QZl?vYGg!h#pWf)B?^Lf;x=etIW(-qW$l;D*M2_Uoj0H>TbB`;96Oq=m+QczdjBeF5&BcBkf$m zR6w9m=Aq5FKJ#Em>5VlEcnZP8LuOd+* z4p&NMy{~f6u{4GM*vdBV9$StWgy1FarAChyg((e{wnd0S62qD(vN@o1&d}=<_w3S zBTRz|`>5HDW9OBXTy|G8v}KPOBO)GVoD-7Dm~ox@_9Rk1EyNyK$)}&EcC767YB*-O zKXM$YkxM;%;a$IuVS`h^~Nb5YJbqccTYARIB4>tq_f^^YsIzF6^qfBsNxlA zz)nf`bwv)}!SI~!G3xdsmRug2tWo1gtUr4munV)GoIu|#IWzWm#&c!P9!fR;h=_nU zH}CD9R;>hEFPGm9+3{+Kf4S#gvNN2Xk%DD1Y=hbCdK$0522K|WS?<``;_ZUjQzs7P z=UMo`M?q2GjQQx|!9O%eWM&{1a(SKIIK1%;AvQa)=5=Wz;EfKHZk#-HEr<#W{#qYH zR*^T0TC#1nm4!3!l}l=dQVULH#8{7~D|^eXir6Tgb~mv2_!AxRQ>W#>4v9x0|1I96 zSOR3RHgc@>BMdTmvOBM4F`E$LZ4`7;0Yl6*MzR_=ZRMR7T561Edq-(I?M(Mw(Hcng z4hwJzwRx`^v_*khw`vGm#-BGi@!b!RU_(cafYeKLx2J6WR_qHDlJlsr*E5e?H8%b8 zcbhQ0A2~e-6oL~Sm@qHeV5bjjh931jVIKA0o4Tv@>Q6R$a-;VM^G>;FN{QSlPbn*& znz35r4Yn@>hhO8TOc8>%Rwm1Io33T=!-0obztQ4ZczOu>Zjenp+VLDev;E7@zM`Ss z_AV2v!R__E!@lS4fB&*@8|QpovE%SImBpR|$|K;+w9&uN6xrHWB5N4&L7!pd+u+Vp z^k?QJhYI*pU(*PQW2mH~dIoVd69GR$;KZrn=e_SX?|?9swZGpS!`(i|bWbtZ!MM2$ zlB3QxI#_lIMY`GbZ3-Aujzn2kNP|M^Q*|nt%25u#rnR)&98GtqXB_)0`;O7YFcYoV zr*#V5YnpXu;UrxiQ)IeVlpEpkrLDca+rIU=n5Od{mSza_5i%MqB+};R5#nJUXSx(1 zIcZic8@@MQT8K38Obn1U50OVy_NyZlHgr!F^q4C2wOM;Ta=j8X?9c@fQaeNVhhJdB zO4Y}s5;(J?38&S@b_1TsgWpi!Bc0XCo_|OaBybzh0Tr4>|(#Q1h6KC&$#ktLjK7oSJ2{1v1@!6lt^e>A_u$3&GQA zzvV?arY%e!pOG z2)~D$^SBWxQy``h8na(FPp`ErczM4X$@!JVyuGhjYxibhuk$0<$h64*mt~Kxzm>?Z zkS`mJjJM-H^&C4|2$!}IV9L0`JO40RiiNu5ocjoI@6&TKxUKKsCh-`!dFSK3%ZcM^ zJHF=7Mz3EPwO^a3dPWtbY`TUdy*fR4_mnocMCM=D^%jCb6-0*Ysudl9T7$ce&1JXJ z73MWnirH><-nzw_?j7A@)R*9`Hn`&`kZdJ=JZd&a-+BduJ+0#qjG3LP!Rrq+!#>tr z3(wEu1#Sqaj9<;vZ-S?53PhG{t|1}4h@I%TxW?yKRLfK#?bG+|IU>gkIv2B_#R*%_ zT-^QZe<`_XzrCcH!`!<`E2MpSI0Ti`X)3BC4*TA?SKX(*QTn!)Ut~2_K5u^wk$L~4 zV>wLD;d0vSloHh9KgEhd_Ik6}Deitk(w|Qm*V8V~U4q@oQ(<)^$n?xT#C7r9^Z))4 zeAr<9lHRVL<*%b$PV4v7ci%HQwlo&^ib2tH+SSu?FHfi9 zo-XQ-Ez9ezGG%Tae>NDXO&fsK7~sq}*$KOsZbT^qdvPu7n%%5S=Ib`y%Pxc~hRAzs za78I8LJ3B&U#SLCz) zFE1LM`^lDEQNuAc8Nabh{0|rFP=WRK5+|1Dw8rTgx^X>Agxr_2}Ae_*1LE85+>#8kRDQhYhS82PN3Ip}0U-nyRmjJ>5d1K?_yMhQH8JucZ;d-96rU^pre%fs8 z68h2E7`plpFBPx6A&|mIOTOVxru^S-IpV!MUVsYe`*w={{b3)JYyN@x32B3yl$omB z=l6(!;au(yI^mTsu-qCZU;Xu|Yz5yEuOrWy({!XFCncNPr@vf)EL{;+8-aWoY>Z5$ zWc8Z88^6g64WJs5t*5b-p9HnDt%xPIy)rdf$SY8b|MpAc zq{1fna_P;X@YVK^;ed-`@`@h`mHM2$vU&X62sd*RzJPsZ))3%C2*?DH3=u%{DmOnEEi zC8+6LUg>A9Rw{!Ht;pj)`)tDPJ(%)k&Pruorm;1?Xw-|#^)%$F!}7Ah3uxRGXD?Ue9Q)#4RJl6%i%1w~a13RNPb| z>lJ1wNB>=9#9YWDe4-)sIoq!hz9td&_2HML@oAq?Jj7u0tEXTjUPM~m@gHh#Cx8JtRV+07=u1{n==C;~*Q3v9Eq3#7vb0U2?U8h0a>Sq`z2W zu3F;p1Gk72Fz!=%3J>9B9VR4C7AaQVofD~Kmq^;Ab`9qII&!vUSl}?@O}TiR;R96) zJqv{H=HJReeJ!8qSy_j*jMna@(9fRg;w{(yx3KUBn<=^Uo|+~UlNL#R@8eFm)0c|Ink@BAQJ1;6BI;(2x+gh4FBA)NQl#trZeQgO#wV4iI3a=D5jlDh#`T5k2k@6RB96z1j=~%6Vf}5 zdGAUmk{nNTfC-S(hdi(adepX>2^<5o4QuA!2h2(g_dmpX%R61~@-vXm#&gdu{pWJI z-zDtftsF0dLn{2>p&m!^)L3DmJ$2(7^cLs(5u(ZV6K}?~w!Bn4fZbmvvQ$tL=J5aT zq?&!N;4H_941z$HT~FA{L|%3maB<$Wj|IoWf;uq$(!_K2Wsdtx@lsPnXc`TdZUc%K z0@mnuSS4BfB%!Cj8(uMN6N&sDqO`enz_^G?B4%4xl8Ul=UaNx~d#U;IvT{jF)AW%juj-*)PMlucY|6s##pk;5av%n@s z!dI2L#?3O*peXo8iDi0-e`Ahp&-i?ZWFza=JvOaz)72#-mf+vLck|__92)@*P`SWI z3M@uJ|DZ~SjipIc$b zz5EdQeDXhkgr=us_jxv6&fOcZ=9hot*N^P=f5nwt_n1`H>%P#9_L1W+3+1Y?lzEn(c_p&`}Z7RQn!ZY7kfoudPXKduSO+76%%`3050z`e;L)N?AgN`nM=f z5E{j&j$Urk3}ZUW1xCX*6Gr~T_6zLtV&oD=;MfX$UMx7>Teu*&7-j2|-35!p1+&>v zdIqDzEyl4F|3dYW7$GKM8?1evH@XI-Yl%Xryyex@upgY&Ow^e(R3>Zk83CBXJBLX*Ds zP4WR)fe;A8P0s4{;64BUTa2Fa)ammZ0>_%o&)L#w>Gqs))v+Rj4k&QV?AAg6#w#PT z{Pkun=!T^cPm`k-!sEve3su&@ogFir9hbEmt+tU1)VDHOV>S9{X}sbeAZ)Wn!&Q2A zQNO?&_6oW^aqv*D#S`5xbqG+H@ zxX}*(=7_$$#64DvvswtIgcO*>xHZgM!HFmdg>2woCC8v#v1^ zs885y>n8?`D`s-({S)E?FhDL|)WBh*o9cUiB?o0Kx9^r)hJTH`p3`CClzwyyJjMst zTpSGYCI&b}(gXayh?KjVKZI`kn&-w>U3R+^k-YPW1%lArMSG~RtZebqrd7^E;*nz zweG%r=Dls`nUf6OMr&THp22FUGj>PGA@Ai2HvObmOjl)~dm}XQ8e5hL z?z=&6ye#++zmzV!rrQc?pwzckA*0uakP54(7%#%lttg_zPc7sJ&wOO)k9v8WiUgN< zTdonWrn7%XeS-p&Q8>R6H)zpfHfe>gm?jQc31Q-7bB)*!jUmW=x8@T6C4N~7Iw1y9 zDWpw}ZNl>$K4fg)4lfqZ`!N}~1807T+mzZo91LL(Gg^I4b1Xy>Om`9$&f3YvUwaR~`YL2Y>%M{DrXc$9+L0h%6uXMM`(<@0GX zi$zjQ-}oIRuki<3H6>VthS;{cds&V@LUt7fYpUKCC4jb(=dkahICesU)F96;)hxj7 zivCJOSe;rL;@kzn3ZzqG4NNl8 z#^R6tUq#v|>!`>C@zD6N)M|Ewfkc91-5j?2csJ(BJ}EwZS*Fw7@E7Vwo3FVvOJSrp z;(#~v65iYp;}7ybuHNJiu(>7d{8?Z36M)l-hkAGI1;H#U}v+Lgb2%xBwno{%ZYrdF2 zWdXFDon`&|ucb7EL;6FDnkp&_?-pnGfRvib_^s}a2O$UMBLY{Ui~Klo%|5*Dx`*Qy z%9N=)4+FqHKh#356R-|O+YAjp{L2Ok&DGrZtLM@BbvHt^G%b42vTq09!+&u9muHcI zGUNYvWe-L)WvvJu4R`3l-tU>(xI@}EJN^4_{0R4tVCu(+R;dwPp0_(&O#g_Z-%CX) zq*d1h8Ld`YJ?Pr0wyr>MMO}*LJ)NE ztsUazJJ$NhV0~7o=I3x<|6v%UP}>TiWL?JOiB(USt^4VW|Dm7FI%xCobFBMW$xslY zml&WlMUs;ugsH;33i^FmmHkDNv}y~P-+||PWhkW*a2FWpHH;qtiM(TI1^=;SrDJRe z-KTZAV{8dM;7O2*Y7!HN`iY7kuVm!<7cPyDjDv;~{bT>xWwkPD8m%)_<{5gX(Ere2 zk?{wQtYhV|D4{X7dx#!WF)8Cm0wac=E5UU@|V3>;$YG(zOQ z3tvKS6p_u(DQ6#{6-paf$myKs!Nl26^bmeAM!HEe3b>O>*mM)=3&DF&wBXVG1onC7 z7I{keYw6a7%0mo4d-o(xU-o4eO-3{dyunsI7CL$t5DMd0SQw@&Hb1CxYiG`0O0uTMugTxf zWE*79o$+JIa0Nc%%c5x8s!RCvM+OARl;U69Gm~R;WOSy#pCyGKgeV3Nz1D&oTH44~ z4HHqdMCyLFw0}Tc@w`Y&4?2aCIf=xyrWeu(}CrZ5EI|0-oKew+FiaGNA zSovl2>8PxvVIxpnb=~lNeWpKAal$Z&Pl+tQ?J{3Df>^*H>M` z(2P2Mj2foGHb2&L8fYsaUO1l80iaKhpNEV#Dl~wO@aq*L*N7CO|3MD!`c|KLr+>`p zZhG^#cfW~AB5zjU*t4hnwCwu#j+8o1%EQ+zi)-r80U;jt^Is93H*~8~y`ItLU z)0?SLe`doaEe}y!9QD)LTxJ;*;hzY2H#T?tJPNt>ASL?;q}%NhbUNdM=A{!SAppLZ z-0?dG4c<8P*`y4V&gFIi3g_L=Z5EXClG5NeUSbvPd%yn*x98?3G6NiW2MI-8gEsfN z&2ua0qw!WZaG5_h4Poe)!Hn@&yvTHo+x=CMhs=M#p7xUsi0!rfo#^3c-|w~Z0O6G3 z;!G5h$u^!aqNYzxxI9MsBg3z$=Fj6(Y3b)+A8C0=gg3x;@iYttr1JhO$~!55@HFc$ zj+>95Q>b`#;b~`T zPe#chHUsg_qp7p7GYjh&0^=`Cp2 z3@()!+E_7+iSstcY|qHcS-1T1_(17-;yqLf*M}JqR3p~8e)!J+4(TOAyaGSLS_tp+ zkZ07bg4M}*he$g=2;iSGEahRV=_`Ntz3#^XM^qw!@`h8d??EzCexRP z8?64t8P0%5K{wu#4$s4Qq0cYBwm|O!S~};3(0`i3cCIaZ;J!s%X<7w)%^Df=LRQk|=`;sc zx2{Es*FsI);=IQAY|>rp<~}e7&SQ>OXK)sq6o=wH7QexEghp(~%s-#Wu<`;DeI8b1 zyW|AeoOo*9V-owcNnPJvF?n0csj-5S6cCK~J*8hWH`ywDWu$E`dY!)C?ouTUVsA?hSX9^7@cO_GajH52x#ly0V$hl_LN1} z@p5`w_(Ya#P{29;(agSgxBKf#cnTjb&c?%eU_<)f*ptzc_w6T)>)(8jH=(5#8qpmMq*0oFa<+hd<7ksWPWM-$%H-E}py@1X`jXff$pt5mGc+XMo`eT2yBOc?(+51K)LHif?b;|!(k#v4rt6D=A8%QdURl9tTI)_NP?&sW--NO^yJt~&9(wV=n% zh(ks+gEJj%_o2`pXkGkpCwHULVM>$1!QeB_? z|EAP8njDeY-*F^BaY3ssT{i!IoHOx#%_yR=xyA21ZDH(Ob1QT?+f|lXe-$WrPMaAS z#^-Ws%A>x?DKgzd^_DtnHa`)rrk9=FtIu^*1Ywo&Y;0SZZt{Y@1H$R{lV)RpJa357 zTvvc!Ih~;pr%iriVUWD0l4+on&AzJPcGsU| z%6K$LG8FA*qs_!&B5poG z#zGyQ%B+>5E=E&dz6qwC18APfBSb^z`bF`)*7+Umudq_r)B;3 zXUk+d?2zKl<%*cH$IB^%UuTC=@Q=AWL($*czYoxQiaeeEcciUT}-9!X(S2X4p5JzM* zJXt<)^pb>9-G}ZLy3%?B=JwpJ2AjXIFwT?w8h(p$Nk`{=>r1ohE*stG)Ben_tK_@t zsH9?W96(tT09RnW-p%E?eXiGwMqjB8gzsy+hs}jZ#>J9KN+7@rnaW}I$5??@ZX&VJ zM<7m{vTx9iExAC z*V<&zG3p1}5YWkkOY8DGlPt`U0k&pvof& zGbPyxaSK`fP{p}W)Z49Ikuy{dFogy;eG>kAB=j@gk4HsZlKCnruJB`8b?cuNC#^L)~dHh z@%kFT4L#0U$tpPOyAD1r3tv5Bm^7UetatTx8h%Lzw-bQ_tA0p30Z@S21>5Sem!dbr ze)RGgyHPxGA8l)LIse#sOkOXfw`^|7Jv*6Mr)}i;Iln|&vb*kuxnXVMDZY%HY^c=N zmG$jYZ1`?W1W>S1y&8BzpYF`37%oQ4 zH+)l(yK^Y_N(34=!l*C|!_xQ}e=Su!(#nROZKd%LAq&=hc8zI8J)({<)e-cE!I}tC0^68oD}C-K8=pdQh(iE7`sJ&(2(QBcx7qA z9=61L3W-RNWUfd(=tIlp*v^*v?9MV3 zO<|?fL?nkxrPQI=WP5o5@=Ot5ZP#3+c$}fmY9@iUZAu=oJdmU>ku~6~?^X8k3S5!< znd4%|J%a{&0~SY0NTX}qrbs@vS!%zjU!iukg*%2sg!!k}09?z%ld*Pl`S?L<;cF>i zy~W_)f4|#!)IpA2)l&#MJ^ES=zo)lYb9TE!@_8M1y=6PKoQ};eg(b9#whz9`o^9;a z@8LM8Q6Xv=GihNzhLb9yI*H`oQVDSPkyT$dw_*|j`U&iwtIH!jeir@!wIcW*m?+f? z!uw!;bf-G(d8+eA#|;HiG5vG5FU9noL*gz;YD>$;6Kw{$II>}tt&KEfVJ3EKjw>?E zs{cJz#}5gbZISjJ70h=)c>U-Avarjd&x3M$%a0UU*HZ+L$7Ns68FUr4z$yF7!!G6i z)uY_QAH6=5;*qd{{!ZiN>iQ^rUOY{7d5`^ey-@6m#@1@prDd`77pHd7?MR@?G&D@^ zzRr6`dX?P+fsS@(Afi0fPR!Jvk=6EN+1H7OIQ8$>aDB$F=n8CMMq$>=Qr}Xb=9jO< z7(CK*baIl;l8_QMDTG=waVb9Tg{VLZdt|w9$gmX_>LW|RGQoE$&oet#&FZCri{@_@ zc~HnCnU#KhjN|bWgmvld?!J`iR##$nYP#D$KUluva1^h+oKl@nGT6q8@7p_y#+~|M z3Td79>9@=sV16a!6-cz}Au$<8 zcJSl6CAar#7u-E67W#*}8!~(aD3dJs0*GmWYE0&n^i`Hx+0d_5WV zo{)HXUTcisXhdSmgbalV$j1U)tf58Vseo?T1$UrMriK#mWXI#N_?#*R`@H>cok@Rz zD`TcrnF4Sp-)(H%gUcU}pfUO*Kp#e3nm!n?j-ZE(&GHUsJV1)|$JN9y@@Q~L`9B-` zum1V87oACKfGo@R7X`xnSa&J7;8v6B&dNWHDC~Jbd>l0{lR0Gv$R&S#+x{8|1+prM z$+-Mrrtb3%YfVIyC&FIufchioi*{i*D?s*Vla6i#OA_dPjJOxT?A9{ zU+00uc!aEKHU`-= z8EMigQjllxZI^kCCj#l_&%mLVOHZmRqUR#^M}zY+F`4oEpy*62n58GaDmV16 z3*sx-B)h+R4!!Kk)K)o;u7)j9-yo~>16+aV@?QpBT|HB6!ju38;F^4Bq2}_F|KP5O z(9Y|x@hi{=Tel<85i!o8aqXHBORJJp8L?L&$1i{`m(ape5&u! zAo@W2NN}s83%@^cN){i*s5K-jSl2OMtL2SV3pdVjpF8|W9>K!4<)k-}f|@rP;K1Ul zGe-VWP-Wlt^ako3%D8=Cna5@d#mEg(Lfr~gs(1taY;!$6z1WCSiV}>`^*v^GJ8;6o zv+H%AQ*I4r%6&~Ozt3d@j+HYy{Af6>Fs7Er72k<+psOVfm|)LGSG*L9)uU$s3!5FF znfb7%eh17hgG=yC8@wL3Sq!}FU_AcXh_d6JMeN*QjFNDT75;!oYJTjiI|m=Iasli+ zj5-LAP6|HJFEMX3K(nd&k+ESE$^kozos{K*v{^-c2OURVlUya%>kXPv%Z$#(bz2;H z>=78G!A@kgJ=y)c+btR(C6jlLYZA}VM=pQz5S>o!kvt`1b+j!Y4M!Aey0=k+vCOK0~0lUw4>bVUphuAwv>s*;g3|`2`HTAdU&YAv6Mzi z<`3LQ;>T1hl^09aj4cmYPQM}R*Y2P4cH!4vs%QHT7d2j;b@4QcEza(SDYJmj;5ADI z)yS^$5r&}xP0fcGM9Icodx0_ByoU>U!af*gC#Ni+RW)|J5#ZeTChBf|-v5LTKewfA ztAh5Y5IFAMdn`7LWW1zc*?hFMyV5_3y0$r4|O5 zO>kv_C*`yPXX533E(7*#y+6TH%$+BX3k?yCb zN0Sal54BWs z0;r1k7bH$|z|vMN2+v@<8Q2`>Js&+XR?DAgiie`-Ia28=O) zWk>6^KiD#I4g&Egk_)c)ZuFMiLBIdcK?5{M{)%W=I&19NdU6(h+i-`Z3)5ntV;%eg zP=jz%s1)$-DRspiK*vWuuIT3tmm4oS542GC&)#3<4??VK5O&)KQo@P<@CN`B6Cari zurG+^;hU@K?OWscyXzfhu|IjeL`u^IfScXhWn?0e7=Z4DXa&$thwxH!wJ6(0TZ{lU z9MToUuHa^e7N=Xj6cIlj{1If#tAH9YDk6NbrX6?2JQs6w!Ata`P*auS`-y0kULg_E z4WyhICTOvJ?-jr}{Ybh-Lt}pyPhq`$4 zQ(2fB0TSyT)+qu&!&tvhfXCeg=WoT9`yJ350NUbN`9*M}T7w-%A73Xu8supz)(`Q3 zve=%7!$DD+w7f4$V-uD?2je2*Fe|evIJftW;ko-lS|1_*RBulwt-u;&5|BPr7(x&l zae((RGE+m6M1Xdj^{m%R0L5rGU6<#4nxS0!y)6Y~`P&?tzZU5gSl(J!PDxBCmEJC( z>6cP0)5r1EBABqCz)(v2P>gGTG3@79j`yU!7-6C?_9NK2lXg9Y@?S@=BatqQy)u?p zg2W3N6&q7`mN!opz%yJRP@{M&8pwgwxh8h*EVu;|$ZYB*PBYhIe``%PY#p7k4g055 zslUi+cU*A+lO5#?PPvi4>rQqVYlo!w0MQlj(d*2+)sXrwyL~=`(1o*IT@ElGE+Z%SY*9zDAZN@ ze9HX&iO$Ao;uDGIOC5DV_R))h+hzMKTS_W9y7J8yLM1qCWZ@C)3`n;|vOci}5Jls} z$Vbmic)+jx;~$&-@eKrMqBuO8d~JBO1F4f6$mQqCbY~wF#irwh-|L_mH=bL}+jqn|@5MKLq>hX;eFmbJJz3jfanr2^07oLZ1oU_}C z=rCe-_kSi#Mo1xZld-mKjtO}*{qoXj76*(f6J#A@&%8=@-d}P53aHq+(iB!@k@>Fr zV!YlLK)Z}RmODv#HM<4sZrd7PZPlkf-%$T9Yl2*-0j-FBh98(3AwAV;LkGU1fErZB zJDW^Qet%qu-&U%m`WUH7N$&__mZZ)K@mKV|kr*sprG0G!_9y3HRt4yOLvy9!rx-K> zX;CiS?hn7_uvk5i-u<%F2ej&RK#-GXEVMgvE)-_?>-jL%8l<#whz=~X{8)tQ9HY^jHPzTfek1VAm={WhBjk1t!o zPxu6>X~9?|icidfNjTs~xDOuVa>WVSIP6?t?Rce$7P(uMJ&h^!#;HCvSxzfi0zfbV zz^s|=~f;wRI?aO&l?PgXnu&0#C}VrwPnwA~~;j>upC(a^o+?po~5wT}-^0Aqb! z&i5l7Cl_gt(h@uf7!rzHei)?9Oj%4eVLueJpZ1^4gozS^(+xxbyj{TP84`yZbnVIY zFDyZOjpIgL&W@$J1J&Wzflh3aN>VYeomC?<@8;4I<9*SrExf{y2&%z?-?SvR#Yt9t zG2!%}H@WJMyhE@!uj#AnPx1#w=^C5TRdrdwtJ2ufbF>20=8&yhQ8b!Rx5}nn14b!bFpyyGAcum0ZYbI}JxZGW?tA>?zqPSi zzUG9MyOAur;7Z+c*u1jK?1qVe)xvgqFIFUq+Arvgttiu8`1^p<>0J}x{v&MT2LVGc zJ{?O5YRA*$OiUvtd;w}<4R0H-ZUI7mU~L#0c$^Y0hy-8U9~#$We#2+F%rvNLP5a+) z85>}u>=H<)RO6o+_(^+_VHkrvYJ$pG&l_W`-U@(6Cef#fiMH??2Bx{<Vdn9EXhF0hhTRMd1FiF9#s7sF%kw<*y~ zB`)BcJCCLgXfbwB$g~{V1{mq~JwEh}o9TOLl_M`!2WAvYPFQaXI~rzB8>Y8~Mba+T zF|BIfdT=OjoQ8+_hVx5S)977NVZ9*Xh^EHhN_7e}7^5TPWSEhSQ=81qQx#59uG4uW z^($Ix-~dnHHW^(XLYFFbS+%(`mCiHgOMLUBL6fP8E}B`sbXSe)c`PyE@XQc@|4r%# zUY$jxX6JjQb^B(NOrZKtD*0i8sudHxQ}ydvL4n8g6CVRnXx7|;&6`B0)$^c@&Ev6q z-=nt|=a73?nW;%_DA3*9-*zDSLxk}m7$td0LuFzd0pC?Vy+N^%)P(x*2O ztw@g2+6^W-p>y7VP6JyYX+Iq}Yt-na>5<8!pcE5)-knV)yi75P!}>c;*kD!`BfacL z7vo!7K3!PiR$~1;yLHA5fg(UP-q5hR{N6HV&6vG)%6Pg+ktR9zs3f9)8{DmRhXJX7mrV3GhpN3-->uxYsU5<*sdy)iH9x?DIx=Sn8h($uG4OW47GNUs$`(W$+mJb%g*T;RbW@4p)@k>1R*ov?z5@dO!+BF;hyC|zec0-(HQ9|V3 zEbQ9|$I@ilH}?nS)m_0zt@py{fXz*?)kE+v_?p1ZL|38Q*5kCt?6ln7es8tK9mT^- zyX=NX#aM`ecW`5mw+{gf$Uy0U>ymFHyIK}QDJkxbR+hXU-SqkG;mb|_#9;w4=HMf=039ViXcWj*ZfynPA?+e` z4E&-A-c9MnmKN`&tD*0f^>fdrPQpJx{lgzVhp}twZx<$eKuh(;&xer5PMav4Y?0&A<>Yt!r*fXf zYcDcw*O3j&>mT^phTVhYWZnngyfyAQS8{SBvjW8tD@PYl+AdFk8Dz%|Uxk8TK(iAU z_{N`epIB%Adu6<233_yp5l5l^mm5WHMCsrv?S0W6n&U zg4IfTzm96 zWGC2ZVmB>>i){_fG(?gkg<9DALKhf!DOzcp#m07sEz{6*l+|er_)RLd+`XPqu_{wi zTmAhsAbNiuTKR$HT`(Z|H*E;gxb%eX+K!cCxoGn2Nea1LYKLOpLayOuQPTjSi&t;8 z%VqTKFRbAS{Lf9<{Lj#V_b4=y-dw%9V?9j@5($C^ZL?e>Ur)fecCf!~y$RTxTJ~iv3JPRPZzBKk2ank3-&90(gSS1= zsUUeH888R#a2Ml(YgJt*`L0dH)miMe^G~Igl!%NGBpc;pQZg|9au7D2mCC@83NdI* zjQsc)>;Jp}uyLlWnmhiUre*u3yuvKuIqE`gJDML}$j&z&k^9yE@ZBg z^#xbQ>>u-e`6n=oYn)h{TPW&r)*JaH#?>~7jfdIao&uO6J*UD6OU}o5ekYmAD~FR-LGQ0HW_TlSpuTipzsX1qj9(*;L#2O8$;R+W~+Zi&eo84L0ew@IE@)DQ9&6QU?ndlBbL`d>3e7+kv6#JwK(hJ(+hHx204w+ zp{^PO(>6)%WpgKNv@UE2&Q^J^Al2#lHoF-WbBtm{$U~hUi~aj(A!mwP*cH0Pl&Vn` zwK(->Lq>j+B0?%J8tlT4H4Z?|jj@V#9qeJ1te|TTA1?`WSxjy&!8=XkT+ArOHG5e%yBg1GQQ{D@D|% z9(^cz1b{KEp`s^gQn#)3y>$4Lwi~WyL$@eeK)yRLsXYhzV_m=Y9K-kj(e%x6nRegT zHPvKIwkF$}T$9~o+q|WZQnP`M#gu-`!nZ_vxIy*IIk+eU8_~V`QQK z`x@-D$^DyS+^YWU@rbLn7H`MxNKDkzASSe+KxrM9o&!NFH$dH~&}|!!Q;qso7*c#{ zK{>h!{OI>7;Bny4GjsGnutSalf=ImHz&tpSD0g~ciPb_B9Pqvv_m?#Wo#U5>Vc&dq z)tn}T%wnW#k8xpRKeW|zus&M{WS^MA=s-v2r0|w$=s=;3tO16kKJ|2nJgk;+=v(~H ze#c8bE)o09xr)yQZ8D^mLZd|r5UF)mA`$u%};R=Tx-@H<;%yE@nt{4y%xvljONVPOokm3rMP1 z)vg;aI%nE}!ZQ6iJu~2)@Ba!D9oB5hHs>db*D?nMGNo2O2xMz@jv!$=i!4-zlv0ns za(C@HnG>(oFaV7+Hkr65P<_55Mg3oetW(ZW+hQe2+KnQQs*5Uv>=?KGHpiVKl9 zg|Zq|i(qiPz0t;`<6OsEcUA$y;|M=Hk`!iS?nx!P{{4OYh;9SL zy5`iYrL+3~ka$1oJ-wG14NJ;-se=YVmtAB_`xVf|%-XgIbi(4lchUmJ?A1hW(%}e} z^|9o7?3vs^Ik(?fb2SXbaT?B=MKPwVi$LLqyH!!spuh`?UojGsIE@#k;{*reY@)t( z5Wx1rhm&(0yZhU4x0FSB%|{{jNZ}sM;V9g_Ad2RtBZRl*0A1X*FmQKt}tE zHLr-82{R~M)Ed^sIG`OrJw7i{xb*jtB|-7^k2N_yw`y#)c`r6pUUU%QdmbSne{w`VTLQMh?0UEN;iPU z-vFU>`_T4XkaBfAEQ3WalM45{Uj8UYr$#N~N#z@DJVi*!0u=2Q!=u^RSRv~mIm8C& zP=!g?-!ag)Z@#T8ni@8|b6cX~AQ|N)bLjh7E;ed&qHlob?b7VIBfNAUGidTZ^TzjB zr4k?MpoNMjL1wMrN9e!MA;2;iY#PlO!N4La3Bx)2kfvu8nX4O_n-m z2WsqEor5D_f-w83Mu6RpgMzLK>zR!Z4Qu?8Fgt)0IZqq9|B=BUT;dP+OBSv$n+Qi# z3?!o@c=wfTo`V*0cUADb$=*3u@SoSwFkDqr1t|*Ifal*7l(((rs9_OnEFM&$GkDbL zDF0*2P$gLCxXS#eBtEELbL7=J*pe_dba@^Y&&wdU(P8KG06W=3 zl&`_8e=6Pk@V^6&M6pAyNGYWNqo>$l3Mu1dz`u0I4?D!U!J`pkkFWW>+ue#KVPR9I ze~>RCVH8J}qRW~Zj>67Dc-aOx^6w7*s}l(oU3C^NACiG$Lp zYD{PsAq`~fnEdAp=Wn9(MOHZAZJ5Ydj(U-SG?S_uZ;QJ+?v??~0ynCwuBJ^}nS@4m zPd6KZf;O9X{c}0&AG2)Jn-{9#L2f$}@5Qh)D*_tU!uJnbG$cP&BI?CMF6N9chemZ5 z_JGMO-gBvWN|}Z@oYm-OQ!P&d%7(pOshgZ*wq^6|y< z9h_n1u@oCmP$P)N9t0sFMG44Hi#lmbISguPC^(se@1<12;1K(2m=i za|{dzhaR=}-%b}?ata0Fc1#S$G@y)}9N?)gXxlhJ*O7Mu1qxPK5pFcUqH6xd$RH#FS>`XkiPRJc9XXM(w-}Kk z`PvN#*>r2Uk6O=ewGCJvsJ+@-vCPz{kGq-n_~o?p8g(Qh0vks=7vGVt1cRLiB#J!b z?xTxCgHfgbao`MUziES0nFeP|D!p(45}-vd?56FXDW~p1$C^VG-ogjbal7!%#j^ap zV?EU;8&gVU7B#aP%uaD|b!#p2g)pUa5i4tg!g30`Lx6I43Bvz<8FNg~Bcvu9CI%^S zF?R_o-;d0YH!m5oNjXO(AFXNmr%uGam?kIs4M4~)a+R0Vd6hxv0lI9MWTVqinN6cS z-V@211njap`E&DNVCb0%)7Pj=4h3pn{Zubt#O3WkhvOi0#7Nyp6Bg0n%pzv11dIve zH7d9p+8M%zmFQU~M|7#wK-$k17HG&iqDnVjUffJ?GLnarhW=Lj$R7Q{B-sBi{==f` z$uFW3R174`gF@YeDZ4|6EX*&B=|JX+=5ej2aw;>Zd^OVLY|f>k7HUj0lk)QP za1(ZEeiC7V891pz^uVS-fi|0vcM&T=;Uw=n=(H8+$Ali_>JwafMir%n9ZKWs@W@VE zYx7w(G>J}vkI9M_%Wwp0&;?ZC8%aJ-h_A$$z}ciak4Gpx)w9 zt8!ZGnU8i0TnYKvJ@p8w?FhoNoo1=x1=>0Tm%nQNyuwFL<(ce4n$#xDu&5tyWM`4d z-KfT=f-6o2Bj`1cxX!ataSjb@lILr`R9;ykcYYgS#eNjhHVRjpucwPPEFc?qZ2T!Y|J{)p?cD(PY{r`4?_uL`=N~wFxie^)p%`I-H(mH2-;}-uNqZ?uIgb&Zu!#=NUxag*E5>) zYq|q4<9ucuumrTJ%;k^mBvhc6@9Bic+F2b%$HamSZ^oTF3fA>M6$@jnitLleK!tbQJA z1B4CKjt!qFM|+7wBoBhjR2;4Y_Lc1L`MR zCd+R5Nh|B!mCNug2R%XM&SZ-?2ni^tu5^i(V>7I3v8}Ol#~dE(`9`dUF*z&Id-Gy_ z5U+Lt0%k!j!x}|?!B8G1{!j%#z03F`ef%EG!8N{fLglE~88e$mM#l;1$9h5DY7;vN zY--CD_@QEw$aLbeu;0HaR+$JSctk z3!A2QcbjJN{wSQW8FkqOS9q3#WDT13k0NVJ@mk+0xa z*IlK~d7Q3y3EgsvLQ_;v^)y`<9nL^m<*ebV1mC3 zTQ=nK_fQn${mn!!`Db-E2sP8saO(l{<}ORc6?M~BDr%q4T-Wx0B|<(Ix4^_U(S ziBh6#SLJBjf30oiIwnWeYb)Iji)Ygexx^s|S}!F+h6iBHzj*(+qTu=sR=Vz^Mfr+h zC*+YPxu+I6d0h{KYD6Mh`JZ?v4Eg-=0Cqp~)9Ve{fT1YpsJM7pIIGc)c~(Gcm41!0 zure3G4$RaN1rHri59?Rs9;}^AxMFlXWws1E(G~fs%p^kAh3+K~xRnRpJpKW*VDOC?rKWlFLz;AYbOe{R6reYcqBQY{t z+KSOgtvv*(CmWN8;EX`Xpv0txK&T?|bWIMgBg79N98!S!4G= zZDL1WW5SO@N%ph=Ifz)m`r=>Y#q`);o{sUzf#HM=r)~A%btH()lys#G!*(}v>g2y# zm!^A2zZ#_Bk9L6c-hg^H8Nbi1fs!t<0t0glqKT~_lMn;7FRv#3vvpNw3L&dA@%YPu z6V$MM`{EdsR?-0*7(BcnejJK)%2u1?vY^C+xGCdg#>N07de>=-pXIL{ZdwxYD0r>d z;HMybE4+U4c}VG)2Dv>N`;2Y_rO-UX1`j&Q3EUb_y3|w79s{b$?UYl-K9B6^m_+Ut zkpg;Dr!3>lpNoqnD-2wc)I`2SF|RYN`0~~%)i-8ZA;Bdb&+4IoF@UYXrP9!yFGy-V zG`d}};Mzx#m5@TzbIrsk*kmNR7BU5 zsrdAGunS;)iH3lAxPALZKgOM-T)rPkTlK7g$^%#6LNa#B-bh2wuh&R=D%2AU2!h%L zz#h0u;24aLCf14cC|Ts76&*{=x4Nry>GnMR9eUn9ZK8FYDqr5o2YMmXA;oHmW5y^< zs*yAJX1&VZ67`epVa5Ud&L<9#`WuCZhDynX?>sA)u;1xK#0d~03GnSom;I)nF{g6l6sd{I z%PMDNF~Tsmx245E>b&T=;GieX^-&$2X(_RKA$Rjf3xe>rUqEE!Mp z&iQzM;LUkksbbIF?eSyz^1snhja*f$aPMz(PEJ&vc0k%#42(|4INTVN9Fj^4l=@2r z0Ve2K)NCTlTVDQsb^r!axG272I#+G<`@DKn#B^OwvnIn;C>rTIvz~gSnKJp!Xi->4 zW5l%Gmt!2op3MZZDb*u&r+#&DpCH;z>mYGwv@J!BFR1q(p%ubIOFQp%iTb{;KS7Ws zsgY!Kcejki&B3SuWRSSbpk735c!MmXee+#1A3);)NkP2pSbum~_Ws4{IX1`STPzQf zGta?dUwj)X(HYS_nl^Aow$>iJSh@R~Utx_!A`D6EmrNuV&=bnpEhMUpnwfSW*Z5^= zN<^V|Rb{WSo*HKoxwPPC?Bn=6ht_8PZcK^Qq{)^6f5NmuJM_f3=cdZpFveNhl`1FP zBR2FitaSgHFd{oYsQ=qP&jo47{LDi!aYGw zJR~2wQ!`MaT=8mE?E#r&z^FMmsogYMW@~tV47*X(e(sT$Q25)rqv5r;=WQSVa+^6c zN2s<(;&-`3DXu#59h+LaR1*@SlbDAnK$3#daSyxy>TdNsBh|nqEMBPq??Kzon=gSAK4tM$*X zuOQlRa4=0Ap7!BHc!JDL7{ppRoH?;ruqxX_*jBgSHt-};C*J=}dbJ-(Q1T%U1wQ2} za-%Zm@;kopsn7K{zF3C(KCU3rBb>MC?ge#z)hLS8Rbcmz#g+f(ZIximq;5QBj#cU8 zcD?pZ&Y(tphysIA)BJ(Msn4bsku9eKe{;XygT=G?IOnUkFzn)Agjb)&!*pMZbg(O< zrk&53MyeLQJhQmWv}J1p1(u^&*`NL&c5dIyM39vh4}^v;nZM>Arj02|qvo9r;zM44 zK(>+@Ifc)ECsPs|G;sgc_nl%qHnk|v z9O;+vJ@ISx>L}zuCFQ|*3pyZi5PDLm@!%*ir#(fF0U8bb&F0v=qYC;W?iO+GzTIzz zC?lmFXK1f1PoDAIv&;|(MaU6@3CaNA$4o^1&+iKFxyddI(W2rs9s7i6^2b^g1|GbZWOhP;uuk~Kr`~>mImLhFbT@jm~-^MkM6okXGew$O?--sU3S5AlB zTrL9iPR&Mau`)|hI?+Wew=a5HuyewtbS2pkxxQMysJs%x&OabDZx$}1Y+pt|4`pWi zZ{D&-?r=#(&@Zo|L^&;|SSezfeylP<9-Mj<>Pl1IrG5n{WSK+uq+d&b%SW`~atHV0 zR-~xH-Ln~vMI6upLjMaooH*^a{oZd)j;fXODx6~Lh0*8EN-3I$9pZYtuKfixMc8B; zNWSG>VMfRQRUGjieQD!*ceL7O9_T+FM0(GHqJbYWO5FsASV)$#; zFRp;si1Ror8Tub%XbJ;A4#Ll3D}!4k^E^z)o!*t7YDXA$JT_6AA;DbGunFF3%nZx~ zL?55$na*zLYHNd+E3(4t8&JYuNWj0X>u70~U(nBICMmsY(%e;e=F-!v_EYfrOH+*#HPyK9o}%+oUPOS7fw&a1O%cusO1NkSb~OkH?k z+)Yq=D!nN)m9bLXDzqp{Q02xcFMQOhF~Yf$wq&6Fyyrr7KBqr}7-g>sw(obpesQ;M z+SFOme!O^5(UtRlQ^6^zCn(V7*Rp)*J>oEm+gV2@y;w)gcfTPCD$qKWq88;fs?2cM z`3x$dp83`aX%uhZE*KFOyy7Jpc~kp>!`J=n*lCj0u+{OJVc{V$*`sw_nJ^umhOlO~ z590MP#dRbqy=L4d``A{@(g|1*CAhJHi2xW}^C?*AA*t_i2Ly*KHIo?eD#L4p2R7nS zk`d>%s_>gr2KFj32DgRl1Tnro~$JdUfC=Fa79V{Pxf(mwD{U8$R)nUbN zNO5WKW6KF&W+vnR==QE5-8B{re!m&gY`)YqEh#oAP!4W$_$JiAevIg8@rO3{mxR^v z9VGZ>W5(Z=Kqw=@`TH-5TS4}VZO?*C3?0Q|LoxEZkI1T~5c)Q@RGR!kUYg9xuz~3A zAP?w(jfw?|J<_T$tF7Lv=7R@szOuh#Ls$ogp*rSdBpsp?oeRQC!<~{xDCg)rmLx1Y zaGBc>=g-2>_@DV{s#KQHuE&=Ac592hFc(M%q>M^S9_$H8hJ8Wg-thG((QJk&pYEp) zO;T1x2jQ&JL=NoP3mjBWm+pUbzBf=fpjO^gMExKTK=uKLwWw>aOxY9mfaMEp%c(-4 zcyM*EJ~rLh5mbo8u`^hn5L9yz(F)r3iezS=YF*BC40MB`6buS`G=zUXNL=bKrb|g0 zVs!g{r{vu7zL(Hsv1KS;it-)wLdVcZ(VGgX7<0LA+ym>R{CA=q!7zyx>UTt#d;7WK zM|2)xS9Li>p6(#gUKu38A18QW%IT2HRaNHTy)zcYpv~soNq?YGYGq`oFno6gHezxI zc@%%#z|Q2GaD}9HpgWHt?7~4L)^bGFo~p&&Sjl&g2VAZhhveRm%*7vFYOHM^h$tSQ zFYVT%9Up(`3_kp&0#X1qZdNg{mzZ08y;D{lyuRfRmWT>DT#_n^9DXRDB5`^1SFix> zl2K|{f;^pOc$y&eq_8fZpVNYEm;$9(Xij2$YSt_QXQal}0mVb|6BRI+7e)ld4@S1V zRl^hyh8DYDGPohUOZ2Z+j}}JgibWm7&RZ+9cDL%N+s~={bV^7pz~$-Hw!Zv^^_#SO zO`{-<7B8BUK4Q-8BkB(Y4xq;k*M(}YOEk>LYVR~*jnh-$ukXKbY4loGQH%URF z3=+h2%`@6Zdr6>;&LA}80KWcv^};>XdYV0YnXlb5s|jc6Ky;}@8cN*SR+(oDWx=+M zwqI;^caw<@Of3Pj^DhA zl2qlozl?=;JKwu#`n642WcG`$|2j*J8J``3Ah$tE!d)=aByGu09}D*VJ%GNw81nfV-2uu7^F%6)Nb0~u{3r21p;0S8U*1@|G{I34k$E8ob z+KXByN58*kVSl`HrOmx?Z?IuECutNW-j3rAU=2nQb`Pp~yhy3WtiKNQ|9H4wgg=WR z3wu{Ge{NYTh7Cyh?r@6(4d1);cfz!z?OUe{v)@*cCr?_0X6S#G!5)f87|L+jM9#!K zsW<`de=fUxO-unA*Bb63XXv zcA-BBdyAOX4&-?#28x5w*&Z>S!$b7Y^9k_zc$5Vx{?#Vk8%1n9-(T>AnUX@484cWB z{SAKg%*G5q_>1O-I+8R-18W}P2R#%aPAGEo6-xiaGWw9$i=jaaD|jKkaJKWTMGrc^ zdW&mMm`(XO!0HsYyBxrE#o!SA zM|a{3A7RWiI1ks006cn*Yb~vG{~}!H&G?D94Kv8gKUCOkP=ZsjiuZ;`AUVmeB#PBb z+kAuP8;@uR%Al1MS%#$&u|P~dwH+iFX{GZADNT=2AXNhU5=r*f6I#s7H$9$(!%-DZ<_9>Vyu72s!) z7+g#bTJ7l)F?H( z{8CHh>6NXBF&~{fJ`-fB`kMwzIZ6Q)mflC{g(Pf;Bp3wa5#$X|6Zn%djCPL_{!Fe{ z(r(q&kdiN{q-CG3EtJSsKxc3IeAvn>H(#kFWJvi47l;@EFe2DHqS47vzf(!xCVxY? zvYI}~XfO2vCXgZI5f+a5p-6q8pQ*GKzDzxe7+RuP(?N@2KeiL8y+K-qCfGbyL<#J_ zl>ss?G&1i_rdW<7TBLK)r`4V-HVTUyoz1MBh_lJ2OZx1nm>D^H+OwWziIlpE0OPigjjY zj6NLhXzbSJC5ZCh@WswUg0kof^c%Hk67`FV2!iHLxcZ<-&T9bVKmpZSTCp@|yp@Tl z^LmTD)mbrtz&yJoq@soPvyh4%=2>5lvi4FpT-UBu9ijw$3gcyjD7pHjNSO!2ut$>X zsa0b;)*ZZpBb+4bZKcYe<@)yL&leth*Upw0_9~V_%7qZ6Tu~Xvr7^95?GI2R&9XNJ13I;)>HR|qK#GT88BWTHAXTiDbNuXB563aV&g-OwzsE)fk zV|4{^a`sD)1(ejC2TO)Zhc*4cweZJhu1O(0o8-Id5lTu?>^|}!rY>Nd|6~P zTh4_)wtTgrkG$G(6<0SjWiEtlF`Dp3dkNZr<>N_gV9}nUG3vBc&D;3g+qUJxjdgI+ z(z66>k@68yF{^;C&Ltb-^$f}uB%~C=DDt5wz>BwOXaiBo2WCP_aO4-c)Dd0_RLc_2VPjri{jWF!}^%_ zv(a)(H#$jz_?9GhPDdg=NDr3RO=o+!0Ku!8I-}!$dKnWBloLb1X}Zr**pAB3i*3)( zpB#mELU;0er}298$-wTc;&4ckWc#}UGsZ(k=io&KTeI@v+PAds&P~(-fh9=0cJiCL zNNHNz28b_UM2C$=X77CE?!t#>Cg79@kf5l7(Tq%Yn4XmYV(!p zwtc}97A+;9XsO6%0Uj4E%NkH*I~i1XT8_%c(q+X&0g`xX0Y$!(@9_B+vP zkfnYX!GDx8$hVDR(}JEe(89@(Q=-e@$CBjOM}`{*?jdkL%nhqzd+-GLd2~0D3cfBo z(I5f{LhD}eLLhq-v+Fq~Z5RjZzsTp^_L1~C#7Ml8aUA4k_FPA!Z=~vYhq&jL{Ut*U z(m9MXLsPFt^)4|$r&_64ECd(^`+d7j4c64WNnqV(kzt(}-$$SULq=VWLS*OP8u?A9 z7tN69`+ywM{HA!QLIhW|hV14)!=FhOqk1redlCfVj6&+M_n`9Tcpqi)W`|9GL+KaJ z8|2TkoFYxGN$fM*ike90f!s54Pb=l@LsAj$&W_U~?I2VpIrO(0OuK zzujrfufhT@NU7Rjg=3ZsGUp#FWn}N(PcS^=b&8@-<5E|_^WNJPIdfAn4f*()t8$<2 zDqxty7p>j8?=bT-?Ai<~raLWrYJL5HtCBfTmb!0b8G(bm*hYSHaT@X=vAfLYlFrxK zS8v^_BaT#CKzyT&e|E{DK>d)Gs)BmMk*lY)S-3r@eoNiARm(;~FAo{kwxgFm1g#C- z)Gmi{pq*J48*BPLG$zOIfop>$__THi)Wdu-X>dE=#Q$j(YrTb}#t zMf!1wja`Iig`%X*;b9Is^yz2pV`GuAFv?-EGhIO?D0D|6k)1VFfC%2+-K zQ7?`*RJ59*W8L(tW})IrKVJ02Pv@z;8KAxzq`MkKHa=I3W&{Qc@-hQ8*g&R5HMr}R}A4_c{*MBduO zwX3O%JvZD=F9nHLdUyZ3Kx+&DY=C*YE~(oGT&pSeMT};3$(?*XYXXA6SS4FTtn(j5 zMs+KmUD;|{R0^cqD0@aBN2)ZDuvo2UW05z9o|IB$Cl2Hdz>G#r#uc9jbNL2-4Pez1 zrNY>|GR$u;$*M4_6SJ>hf12T;tutHX6f@G4RflgpA9Sih`|HXjRWoz05-)ORzn(NF zR?nK+{dG_Awsu_VIuBteB;&70adt**U>3o@-nh_OdoEy?7-cXD&>k2QN#`7t-smj& zs=$KLxj`^k_tcW9SC)U)bO9BGZ-+tOett7)QX2K9Lk%a)$Un(hkx)((7wEnPNtI3d)426vCGcQLiOQw!y(6LptYupTzgXp5;Lj&C2%u_cyuaxwZ4P;bfa;d zeSAGEBLw~T3xw~ieoB*0TMVZ`3ah+&@Q@Yf&}mQsSxZ;6j)~r7q`&seHI9QGC#~1} zTRp*d$5tW(=e)B#nmu6NEEX?o#hrNk7oC>uhrwFChg;>=UsBYV6)O`D-u2CMhxBx1 zVNa%NpeyOE%;~F|ovRgAA-M7$Rh0rt$qTlQqW)Kc4=y3aYbw`7B3!#AT$oaiU>6I7Dznr}xbT*rMTwm1nEL z9|~L6i|8=0#PE_|(5DC=gdCRc=BveY&po?nS4qTOg9=k9YOK-@*Om-;=S3^Li2#=; ze7nk7{dhHdCfhNqIp^&H?nq!2pro(zr$cmKxp_3xDC z;~!=1g2t)IS+^GZZG~;PCBquGQDWPSV6nZ(yQmtEzL9&I_xBi2qj^yzu<~|37(kHF zJl+qI^iLC}_|kE{=G|T+lIga_JR(L_R{FSj;MwIFOw@FK{!H-EWw_Rjx;TeiP(Qbe=WV>qJ7DTT^yJ7)s(h!0qbsJlsTmMaZ73S=NixH?*7|)qX)7U z+YEGk!1}a`6gx-DAA*?C-iKf+v~WAlGDEkmO*q-khr}#a`570MlC0h8tYy6E+$F+Ijws|>qrwz+YaJ;tGyHpPe)T1|XgX<)1`6o%O zr#*vC)LZv7E2A892LcR{C3vOk?8i4Cs*c0B4AtOmo}U|}MPPW{zp>418A$>I%%Hwp zhASEQM7zMF(xtM%6#Czf@Qj6}Skq;mM0lD$g}tlN;ZC6T^q}K(kuRD3+ua))gFiYR)5Ljv+DY63VpXsNv~E$1i&C56I3<`&CW=C zTECS#$!QbUt868*072$ zt6w$Xmz=4MI_$q{a;@wcT7Bj8gs%wS=e!^yJGpkPSeSH9&oMwZqstN&yRd*^-MF`IR;c#j?_SJ(094jh3v=!RveVJ*`R$t-VP_s>Y zld4#BVN4rE@=b9Mfh)B<-Uu=VaF&*gE;nZe1Mz_0T>)0PFe%4#oM3kV=V*&&qEd-D zP|U32GTKRi%ay9hV1e$M#{)K`C7;jXKi>$lC17FOxz0~$*WK18Xlug48d|nzwl-77 zHaN$KzEyfx1@Hb|qkQ_W>Qk$@;c5}$P#Ma*T6jW>*)|j&M+%ultyn=_H+^=cE1PA# zLF;S{h`rBAO$ScWg$Q4k{IU)oVELDC7Jp2xu3r_aLZ;|v6ev)G`FY2Xzg{q(;G#EY z>5ztdCIm(!G12ymOoPqUd+<}@Dcg=|-8LU4MgDF`HE8>s?3=;Q7GQgDALb zhf7M(seFjVU~w@Y;>|7T({W`Zl9?Yv=ORoU8HR(El|k8Sa29{k1ZX)yb7=PEVU{*J z3^eVo96?{d1W^nV9-VT1q5FKw? z-dyext66LFL0|s(A!qe&uWEpSHrY*^63n0S)xRTY<;!blnnrkeFHObDBi>`oHb-Sv z0H7Lb(QN`<`zidh1nG<83#HzA04cTbAN9c+RsH>n zs&=apnw_r-H30PP-dcU|rS}SxvDkALz_2?zZeA{@;29)zK>*aLw_gxTPRsW5;0){g zhb5d=T?5lk>0er!egBp{{}ie2V1bXPwGd{;7bUn#Oq*6vSCZYSmie5cYIqkOf*UMU zj>Z^ZAgI}@k!3gq#Wo6`OsA6M_D!4t0S(L)2u?j4tZ&WnTVV1tWoJzJ@0rcqRcD6e ziOv&&l`gO0g&AdWqpcW+yEltw=qiHFWFkwm^C-dt!OaFCMN z9^<3t9j2o1jmmlgw9c~8N6pG0&Tv{KucNx0gY*YKCs$oHTqLu0tLE=xvJGa>1n3MK z*_Ka>=gktk1 zcb5zLy&zwfw@1W;=5egTT8!G8!=~N_PE49a#cl^&+u~6J&fG6s%1bxf%1ikRK7Kl& zTCs}!L%G0+ZZGMosxcY7kCkyX} zoq_+h4fc-37<*X81;r2k`bwF)&M1y#)Y2r|$_> zSWmN;>qc5DllNMi2l1cJ+>X(U6z$%=__AknkL~YVU5xYSi$*z=7!|-&dnXwL(6%*w zq}wZpbNo_m5em>ksoZ3zOa@V3ug@q1REWLiH1lGYedz z_W7eJl&8zH_E_P|O=BHgnLPu8_#t#vnrZx$?nuGczhdo~^ewTSZ$TEGG+t3hJ{Q^N zQ+5H@?#)@hRw;vQ{}li}Ar}_e+~@6x?2#F`ib%#>en8bhptgv1)Y94l~B=CZEPlA z)a29`g0hLvwC1q;dPX71yfgn-16$qc;TCaQ13<7n4@cY76u$4vAvpzIa+w8%!#3Bo zFa_Jhye&_88>@!EMHEIw<&PPMKoXgMAAd6B>4^2|1_F@_0@EK3G%$p<=sS8~HKzOT zo&EXMD|3-Mqk0!#jJGIk8XKcza)GObV8>o&`E0o}^vTggBZq&nG;Fmwk^WDxuOGcR z4&dgM{@D3_`q{ExblC!gAH(dNxJ0Fb-{IH1IhB@sUeLp( zx@?idcU>CFbfHa$n73-IW5$qaxQX90o~uIBGfVAb3>4X5Y;KRdK0@{^O{pKU zP}jXOzX{&T?96Wy+BdSJEfkbn6uOil4Q~0i@WtToI`gFh7 zy}Q%4E{<W2U9dVqKgUdDoO{R;$++^1H1oV7YOrE2zs8?d7(JxEV}4Bf?p8CscPb zuCFal2PS+?t(ASvstjWO3LK>A?pligZb0VT?9Bc=PuI;HqZT`B)+}JZPZb4ovv>J@ zbhyN(+{Sm7Cig3o8zX%JsCFp#O@k-N-S5BgS-ZV9;>(Fj$#I8e@<+D;5Ay!*tCP8f zJdppdP{_HZW}soy&-kgceXd-ZfcyF%B_;x;$WguHl>!wp2LIq;ilPxTH`3VQSrkVh^gy1H7=wLH!AzIHXXx9cp5 zY0`mFy$o0|YZLj(Yf*tr0SXwxLQAkom;N?eirTpBpX*KChj~g*G8pyR!(u2~WLV&^FH4@5p?5iaVmDyqb!}io zy~U*wp8luoIJ%N8URBCRX0YMA3;vRqsVpR1r1K93IaTjqQ9Sv`BUG9u#4R7+Ui$1& z_F6`LzUI4n=m>nKXTJ`06DyZ`&Ifp%F}uLHJH0^2Z=l|Vg`s|?-&{9Fblm6$p2ztK zRrYiaAvur$R~i!JQC{6vA6%p{t8+aK3~4dmz4XkN31s+J&*v8+(+z<$G7`IGjD=F9&*Z#pB?W?YX7O|b4tpoe!hFhiD%HuzN zF19cHnq*afIYh-70@Puh+8xzk4$qBy)|yU@zcmI@+^v!vl@iI-0;Q zW^(1Hh)K+Z1;c@&+&h$4E+9cUl6gPp4j9a6aJi9GsI|YM&1lfk(L^-Kk0ju#g%Rx; zM&Xckm^Zc&Ic(AS+NLzo+iiW^mT;kFE?Awt>bv27t_>#OE*;>VSQOodqWS}`|J8~p z8_b*UqwK}h41IFwv9oz)3u&;X+WZ4Li5bIK>KtNP>Lcgw5>UJD=Om>_b#^{$99z%_Fv7 zj_5EmWU$8#tn2)JYtRYEpM`Um{B=2T9W~qat3I-X&agw13xmP3I%~Ad8i1cnl4+^~neKm?wtvdbmSR!M-tCb(TY6uODI#7%;V3Uzzu1@yAzoezGi`e%0jk975z^v-ElBV6IzdkFk#;M4 zo_Gh34U=1wXMl+8D|eiC{4@#3&t&ea6a3(HSuVgz0D*!@TaJ468GHdq5Wr|fQZ^UC zwBDLvWDpR^gYPAv>+Rb)n^aKZ=82VeVq=iW7#h^Are1~%K#fv;;-cp`uvy``p*#7N zx55kIqHh5az_IJeKo+wU$fOil9m!vM4Y?_7GKqI-w)@p#YE_bk58GLa#X zW`cz8A!*R<)Gv$;=4^;An?EHTeXn;dIYT+xbMsZ6^89r>2C3#$!^G>=mgM`~VlVb3 z-;dOPwuD^i_QxYPTSMY5z(W_mJL4RJ>Ruse2Cc#?uWbf^PqnenKeQ&eyu=WE)SJG> zjxoBoC$Hj803}%9osB`ZC`bUP{?baiK(<&WF-Rs?shE#UE(auoI8fHAszHmOx4l&w z7J7Ih{SWbdT%z7Hjr{|`t>2yVjLNmRC2jl;$9rjhyzVn+dR$s@WSG{Bh`lXNsL*3_ zxj*Jg-Z{dy-%fK8squDtQ<^027F_m%MmzOBE+8YMX)%{Mt!6s6e0~eF0LYbRL~TlT z_l>W7;X&a3SrH#$sY7(R%0;x+8COb~M#V9z;4k=p1t$5-(*vzTW}1NXLIVKipEjSs z+20;J-=W`Zb(wQ-v|SS`hOBfZS8gmDT?G@ucUD6QE`_yI8fW)>!Mz=FcbZ~Qt&+pQ z%nTZtdY=GHUrnbc4cRDr6Q~5cr-wyCDQj3+e?p-7xpL6FZ-82xNp3RB{HjMlt&kB$ zsRoH|3P*1|E-yF$+vlgUvdS?Vy?8jFW4yd1D9>Jjol&D)vx0lprfW33+Uo$pOdAMi z4dh8s620BTA%6L@m0K}(A1~h2PCk9Bvd7CYV{~mrZWu108T6}xrSSKnAy2^0ry`l( zrr&a@@hUgG1L=o!FRbFM`*~hY;Ib=5&jem~ZQ>zQQt>r4j(R4icxm07+oukr(tR3Z zv<$LW>ME9LI$jCFIw<52%6`fMg}33}as77l!(@oe*~(x9pym%JkCZDxfj>Olb-Fit zGF}fVh@H^Dz;G`mMTJy?ESRPbnCs{}pV`!%j!(D@~<0KSFdQ=~Z7f z0`fY=UO%=*ag4VBoTX#-Ng2V77XfZ*G`mq0XaBhhab{?!8-rMkq$gw6RJECZy-Q;! zw)fPkx!ZaQ79E>o4|nQi;qv=NSd$Abk0h1FZ9in>ovVR6 zTkm26#niLSM`ZPa{a?k%UlQ*XEU69|6YbR>``J8F193@wqSu$E5*rg>f1yH z-M$0Own`Td>}~3{ikYiZrIsd7uTSi6-fy^t{GXh7`o5gcmvv1?m?YDui0`Ver9 zo4ezT{Y70DW351puJTw3T*PSa3T;ad0G@j;()Xb$(=W>C)K!07cHH*gC)@)sJP6@{ z>nlD0q)}wbRnvZA&kJj9B+uh?CN_D=^3ufZiR>x;`<* zUI5atnWJ-qUA^rnVzc&(6;Y)3pHX_?wJugg;q3GSQn!B9Cn)Xktg6_eI}PvQy>}K> z^L%c!^rWL}3oZWU#+8!CdW(?(CrZ-q!g%X_yz~CWG5-u1{{=+dWPdN0q?dOA4#2kF zuoSxWt_Ltr(`$R6mRz3r_2aSy{o%F8?Z^8-4W@6A&%MYko$=LZ1=-V(c>5`fDOEcRC@T#B0lVg= zj_j-k3LN{qs)MBy_ISYhc3YHAy8{}LWg-CV>!P6_O5VE+jQzG;zcEMUe$P|Yow?}O z=%2=rpVgGX8{FAsMqx*S`9;mFxd4?zO|C&1Qcq-rjj~^p@l}%>JEZLikh^*|a%w(6nj*)S) z6GAe}<`A-u6&Yn5g^Xj1tYc(5;&&aN->1*l&}Zy1^9G94Uj`>E*NkgM0Te?P4j zzr26O=fpG;)n-G)Lfn&zQ?=GAQNTR7)I*Q|3?^7mWvGxH8s-%`i3Cy$XC*EBZ&RGd zEzRLt%<~EAinr2fRwkDYUS=DAN>H=6IV`c0J(|xm3Ng;py8};g)YNppGNOXXkeh!J&=2upru=NZ7$zyZ-}OM;wSoC@lwW_fxPG3-PY(~NRUCly{)r`4(*cAe4cFfl8Bjun-6bJ$U_rgs+DF&A zqUAF_V_N~PowV!hZqLzN79sb31N6S*)YP?Ew6?-N5WSqs3-3-bNs3mcdmrv`n7TjF zf%?D9itU4CtLWS`SM7!1@t#gsT%NNhr4JN2k~C`v8Rz5f6A1^#8o*H*W|570dzcRh z+|_;{wlEy?Osm@{#u_Zo_28VbhPcfX-(J$j0m7kj{Hj za`(8ti{~6y6!yEpExx^ixOAW@0wPnN2L zTk;-#%q3TXk7pr(?FY9R^--f)Xa6{)Q1#@tm~gtitD9dfP!jU13ppCJ3-7qL;6~bi zEQTj@aJ-{|3BIrAN2>Z?)2tAaNzssW310LuHL0Xlu|(SH1hbN)YJ7J(XHR`vRU_KX zk{o2^?ntJ?9b0(Vf>m+-vCh((>BLE?snqvf{s*QHVSnZwdwVM*lqLe$IQ74pqG3Ih z-d%!abSwP`G(0$8La(wIR{Aic*#WIb=2J5tQ2Pk8M$~S4ex`o?>RVUMXBd2UKn#BB zSz7j6q&6d69Oa_*<}Y2hTQ6Jx*(*@26zoV&VWH`s2Cb*NGJAcYEyNl=IDXh{h%kBJ z&%#&(9H>QT?C0vOTP#+nBo#W=9MXaq4nAHsau2Q+UQxIfyYW~58q#U3Cyrho-l$xR z9!g%TzrXz=WXqNGDuiLpF%|?Q{!(WI;&{eY5oFr8ax$%z|WdpAMVHW0Cf5?SHOu&=+E?YyJTC zyqf9#a;kGDgoB>wo&}XO1Zd`=6(_5b)v;xHf{rdZa*=ukx`Enns_I3%5tLf_dYu;R z@+~jqj=MMvMtKnXSrVy54i!W*sBZEOZvLY65d`{maQ+xMALNpLab(D0?GR2Vz{?MQ z(!+F(kxgT*h8n#F6{tfH#iZv;T(p7qf%0Rg0J4zXtSsiWa*3W(S1ZCU^>E;Kn?H_- zADgd7d!+)Oc9`5n1S4 zVnxDZ@Y{%xFg`!4(_;8^=O8?}f%?&dwn^HkfXQbMBWX7#DwUI7nNdKaao%4+8wwhf zro1dO1$7#d6v!#YxFR>oA5u7|Sxoed>dQpDwAaRi*=K81)g)zJ9j)MqQNf$c;cCAw zt-gg~8cbe6eMR!WxXTfDJ*|(bWzIp$4Z}Rfsx`)C+Oj%QN0fREJ?=Ghzhsotp0weF z_H@OQXr$tj6h85s!-xEM9AyIC@)Ni!QH<=Tp!9Kn>-s|dmK8H)_ne7=w6s~qSl17- zLnKMNvL|k1&8*W|)|zy%m;jr@{coEEy2>Ta*8Md_?<5-yy7Bf9XqMGgli)9~M6IO+ zmG{->C@&^3d-apt+_V;ZqLJ!+8A`5ocQWY4Ya`EU>gOO<1A^8rTN&$f zDdx80Wh#_<@bz#d5NAuAf_lp1C4J3EZG)OTng$Jx*H?q{jVb25?50L(O#e)t*lx7# zepx{I*2tIN#MB9kd@j-%Y(L6_OS{i@ct;b-s}d~Sqxlvw*eoPJzRhN6G0X!Fyz8gf z>ByXxg0#(VqM#>yX6HJh)iHc|dSBTI+rz?DzBAZxEnT0JRL|saixVo&eXdc^yxM4m z*1ReLs8ukw3rYTAHRS_w2?t%iQ=&Zm0>xI=LX48kY4OGHgGPSzp-%2teZE5|@MbRd zLGa*I64LZ+nv~doBSSDzj2fKtMp;c?A%eVBsu%c6Nro;~Jr-F#xlgn5FJ`k7{=oTnG6yqK%of#o3QB;fhs7tEq}e~npX2pBi=QU3MQ>V}QcF@I$;};Y-D>j`TF)D5 zIq7mNBT6UDB6;`r-!uGlnx1DY+VWAWSuWrqY&4xm`gYytoY_X&*UiuNNz|umelcqp z8T`(`-4<}Cc9%AF%!M-ko|(}Y``F~}p;ztaek;MOoC%D52pKBiCkaWPGs-1LE5FFG z9aTUH8B32l>ut`p6vCTKJ97GUw{EGIc0`P4av#ooKGt}MUVj`d&pVY0qd^>7atHFY-d@K)?%Inh29n!y5OcF@u5?kJYXX>k7WBKGOov z3G1EfI~$quE`Q>xR=nyIWG`6@t=(dM(F?&!pPP&Ti!t7ZcL#W$H7O<5h)Z(eA@ z1PR&VHQha5eSAkYlx7nY%KutxXDbyqdquui@y6U^NLi35npB^-A3c3OdIqpC&Q^qNyE?L2i?F!kYBNKnN&lqq~8Z zTge>>5TrQ5mCidlBx=soWc#(9R5~cjMoYsGF0snEyOzivaHWBPL~eB*&ZxJr!H?b{ zcH{PuamZs;g4-gj5Rq$mASdIntD+`0$v1xaO23;E{)U!sS}@S|`qjYc}d zYG;4%T(_wV0U&WYc@!KpZ(wdnhq21x;zF)gXkqLLJ#O8CL932&*X&7T>+SG2-@ebR zQR(3n@k4Qhvryey*zt@h9nTj#{rCLVJj$I zSDE}rH9o_aXkL%zSF1)*N<3<>yB4iE1{Z33AC;AeTtsIwE^w?#T@gOItHMM*eN2m( zLJxegB6`jaK6%PiEn%FBsbzxoYHM%Dk9WrnXAVH-x|uGjJHq$@@T#pt-*gB1;v*<7 z4n78&LjK|JrGtCr(_WSipMg0S-He{#4D^Js%U49ySJ<3(aTVwh1MWn>0q5@(5;a?z zB&-j8t9rTyW!kb05mAUjOmuMeedFCrN-(y%a?}XK$%`vNul7t?(?#$J0!|<283@T% zZ{7|*-qNU#&Z2K4m*Jc`9Gc?T_NbV-qf>03km zZwP1+ZXbwrZx6Sc2tYAxuV2FDwzRQEYGmb>HSy}{0t66$erpNyro05~vT1sA1K_Ae zRSZIx1NUMsu)T1I{VD7^?)vJ1a?qyX{w^hJ{hEZfP81vbNDt88J*EygZu~+koga|HtJC{YII|= zkU4Ln{cVGaE3u1}2m}wsJ+8dr&nF=^6Tm2Y`6bnr)%Rr?7l0-nSa8EKl5oh#-xn9B z&YP<8Ix*7}r}3Kp!Q_Vd9BuDJKdlw|X3E^+C6*%xl+T&gfV(V}3vVJ8pZ;DaG@1mo z0lV|XqR5xXQ%ekGpX~XH3U9zB*^8|vS7Uo4Vm_KDv-2XZs!uGj$it$O}8TqO~crqTY^514jTm)58IPtMAZt^LifYSo!GFr&P!&+&8asF9( zH)<2S{#eei9C`@fh^?=%Tgxt8y(YU&*y8hdNu0L>vkNa2i<~eY_EZR#6f2u}z3w*8 ze0`fW7dH2a;wg}#7V9qs**IG_pNzUSodG&&0?3~`kqH`dZ{51@2?k7nGt2Q6fkyh` ztUJC6o|$Li&owF_g}Ca^CDzMdq3CU4Ytxn&#wwsmW@Rl5x#d&%v_=A!*}~|%);(LX zxx6m#mxrzrdnDlukXSudw!e$NZPCuQbhm?@tLW|YpP7(mC<*z@TPcp2@%xo2*eQEq zNmB7nnd(p60E~L5IRO`Mn8#~5k>ws`?8Ss$k;YeCk-tFab6qZN_^Yx%GfKagv8S-(1M8Ok#mpU$_sjTkWYz0{tce(q zlcGbNcr~yj3E2PK15_c9kl4#KOD*0P9FX6LjWzf=O}RzQm3RWOU}(O zDzAoJ{B5G5pXnxrTfYy4Zuh3H&4AxN+uZi7FQ^jxcZ%@yP(iv|0;TR7MQ46 z2vhw#FkWe005kfg9vPH`7e!#-(#_}GS9D@~s%!i|Lr*jfwt37=Y^-}|QgF+IW?z?> zj^GjmfB>g#k>!8K@I<~tufHX%*ZI;$ULpmjTwC=tr{Pq z^^UXX6R>ZY4*>3Lmr<|}e#a$6Gisnje*gZBVRc>Q|3~aZKy--XMC`D&Eyn`MH+)oc zY}|6`%(MSDvQ$tYHHV!t6 zqDetHaY+Qo1(;Q=1MH|`nkM0SwQ0P9u`rii3_*M(A;b!h63yo;G){;A zF3=Ze?QIVFYQ{tZp!_6z2KB6~(EOjOuKnu+Bn`a41T<#wt zL?Hqh8?cYpJudo>eGvbNeV638G0LWWM<;)Fc`HEr%{9BKYmXxuY(W*=3c47(4v&wT z#{{qcoF9tZ10q>h%1d7Ro6C!k_HfTA>wP&I_}>{^Nz)8;dc8>Pz-Q&8NQhGq|ZyTowe>F=bdGkE0@e3sAcuzC#-6cih ziwyzB10V7>zR!luRSs5r+WnRR9MR1i(7@^>&Q};=UJzPMOQ}t*D1QJ#d&#y>b-wuD zFUEf4Lfq0J&Kh@DaiT(a@QOBxTr|xU?MYr89W`BHt`t5l1I-C13TvUPV}+Obwx~Ee#TE5;b4hn_iMerlyx|Xpx^rzxGxJryq@d4GI462j3jB~t0k-?D zZ!WIGKA61Xl0PuI^hB3QdP`B0*!Qv0B`mfpdMutZU%D(wp+!sZ=B$s2mI5rsg-MAD zYiH{?L=pKXi(y!KEhyo*yZN_-+g>srKP0%WgacTBC{Z zMB?P_i_n72mxdBnK#7bq)K7_Gu*czDRkP8ar%5KG&6KWj9NStv5mb)$D*14EE zY|w0q?|%;HQT>>dDUa*+X`J=%nZN^qr?fayZ^B0r2Owrg2oxYR=#*t$=eOKq72!Wd zjQ*JzkflVp>FGVJ&o9)jYpphldLzvkN50RI^z^obc&GtqSWN}vNA-(2B)WVQvNN8X U!D3fs2LXTTcePdEN>aBJpcdz literal 0 HcmV?d00001