updates

Game.lean

@@ -27,7 +27,8 @@ Tästä alkaa matkasi logiikan, aritmetiikan ja formaalin todistamisen laajaan u
 Haluan antaa hieman ohjeita matkallesi:
 
 1. Näytön oikeasta reunasta löydät käytössäsi olevat työkalut. Ne on jaettu kolmeen kategoriaan: taktiikat, määritelmät ja lauseet. Saat dokumentaation auki klikkaamalla niistä. Ne joiden vieressä on lukko ovat vielä lukittuja, eli niitä ei saa käyttää todistuksessa.
-2. Universumin kartta
+2. Universumin kartta kertoo missä menet tällä hetkellä. Kartassa voi siirtyä eteenpäin voin sellaisiin maailmoihin ja tasoihin, joiden vaatimukset on ratkaistu.
+3. Kannattaa lukea kaikki ohjeet mitä tasoissa annetaan. Jotkut identtiseltä vaikuttavat tasot on tarkoitettu ratkaistavaksi eri työkaluilla, jotta oppisit mahdollisimman paljon Leanin työkaluja.
 
 ## Kiireisille seikkailijoille
 

Game/Levels/DisjunktioJaKonjunktio/L00.lean

@@ -1,21 +1,14 @@
 import Game.Metadata
 
+
 World "DisjunktioJaKonjunktio"
 Level 1
 
-Title "Hieno otsikko"
-
-Introduction "This text is shown as first message when the level is played.
-You can insert hints in the proof below. They will appear in this side panel
-depending on the proof a user provides."
-
-Statement : 5 * x + 8 * y = 5 * x + 8 * y := by
-  rfl
-
-Conclusion "This last message appears if the level is solved."
-
-/- Use these commands to add items to the game's inventory. -/
+Title "Disjunktio ∧ konjunktio"
 
-NewTactic rfl
--- NewLemma Nat.add_comm Nat.add_assoc
--- NewDefinition Nat Add Eq
+Statement : A ∧ (B ∨ C) ↔ (B ∨ C) ∧ A := by
+  constructor
+  intro h
+  exact ⟨ h.2, h.1 ⟩
+  intro h
+  exact ⟨ h.2, h.1 ⟩

Game/Levels/Ekvivalenssi/L00.lean

@@ -4,7 +4,7 @@ import Game.Metadata
 World "Ekvivalenssi"
 Level 1
 
-Title "Socrates on mies ↔ Socrates on mies"
+Title "Socrates on ihminen ↔ Socrates on ihminen"
 
 Introduction "
 Kun kahden väitteen $P$ ja $Q$ välillä on looginen implikaatio molempiin suuntiin, eli $P → Q$ ja $Q → P$, sanotaan että $P$ _jos ja vain jos_ $Q$. Looginen **ekvivalenssi** tarkoittaa samaa, eli $P$ on ekvivalentti $Q$:n kanssa.
@@ -16,7 +16,7 @@ Kuten yhtäsuuruus, ekvivalenssi on _refleksiivninen_, eli väitteen `A ↔ A` v
 
 -- TheoremDoc MyNat.zero_mul as "zero_mul" in "*"
 
-Statement Iff.rfl (Socrates_is_man : Prop) : Socrates_is_man ↔ Socrates_is_man := by
+Statement Iff.rfl (Socrates_is_human : Prop) : Socrates_is_human ↔ Socrates_is_human := by
   Hint "Todista väite käyttämällä `rfl`-taktiikkaa"
   rfl
 

Game/Levels/Ekvivalenssi/L01.lean

@@ -4,7 +4,7 @@ import Game.Metadata
 World "Ekvivalenssi"
 Level 2
 
-Title "Socrates on mies ↔ Socrates on mies 2"
+Title "Socrates on ihminen ↔ Socrates on ihminen 2"
 
 Introduction "
 Looginen ekvivalenssi, eli 'jos ja vain jos' voidaan todistaa antamalla todistukset sekä 'jos' ja 'vain jos' suunnista.

Game/Levels/Ekvivalenssi/L02.lean

@@ -4,7 +4,7 @@ import Game.Metadata
 World "Ekvivalenssi"
 Level 3
 
-Title "Socrates on mies ↔ Socrates on mies 3"
+Title "Socrates on ihminen ↔ Socrates on ihminen 3"
 
 Introduction "
 Looginen ekvivalenssi `A ↔ B` on ekvivalentti `(A → B) ∧ (B → A)` kanssa, joten voimme käyttää konjunktion taktiikkaa `constructor`. Jäjelle jää todistaa maalit `A → B` ja `B → A`, jotka menevät `exact`-taktiikkaa käyttäen.

Game/Levels/Johdanto/L00.lean

@@ -3,32 +3,33 @@ import Game.Metadata
 World "Johdanto"
 Level 1
 
-Title "Määritelmällisesti tosi"
+Title "Määritelmällisesti yhtäsuuri"
 
 Introduction "
 Ensimmäiset asiat, johon lähes jokainen formalisoija törmää on määritelmät.
 
 Määritelmät ovat aivan formalisoinnin ydin, koska emme voisi sanoa mitään, jos millään sanalla ei olisi merkitystä.
 
-Esimerkiksi yhtäsuuruus on määritetty niin, että kaikki lauseet muotoa $x = x$ on tosi (määritelmällisesti), jossa $x$:n paikalla saa olla mikä tahansa lauseke.
+Esimerkiksi yhtäsuuruus on määritetty niin, että kaikki lauseet muotoa $x = y$ on totta, kun $x$ on määritelmällisesti sama kuin $y$. $x$:n ja $y$:n paikalla saa olla mikä tahansa lauseke. Se milloin asiat ovat määritelmällisesti yhtäsuuria on tärkeä osa [tyyppiteoriaa](https://en.wikipedia.org/wiki/Type_theory) ja monimutkaisempi kysymys kuin kuvittelisikaan.
 
 Seuraavat lauseet ovat määritelmällisesti totta:
 - $x = x$
 - $x + 1 = x + 1$
 - $x * (y + z) = x * (y + z)$
 
-Mutta seuraavat eivät (yleisesti) ole:
+Mutta seuraavat eivät (yleisesti ottaen) ole:
 - $x = y$
 - $x + 1 = 1 + x$
 - $x + y = y + x$
 - $x * 5 = 5 * x$
 
-Kun todistettava väite (Goal) on määritelmällisesti totta, `rfl` taktiikka yleensä todistaa väitteen ja _sulkee_ maalin.
+Kun todistettava väite (Goal) on yhtäsuuruus jonka molemmilla puolilla on määritelmällisesti samat lausekkeet voidaan käyttää `rfl`-taktiikka, eli **refleksiivisyyttä**$^1$, todistamaan lause.
 
-Syötä syötekenttään `rfl` käyttääksesi määritelmällistä totuutta.
+$^1$ Katso [Equality (wikipedia)](<https://en.wikipedia.org/wiki/Equality_(mathematics)>)
 "
 
 Statement : 5 * x + 8 * y = 5 * x + 8 * y := by
+  Hint "Syötä `rfl`"
   rfl
 
 Conclusion "This last message appears if the level is solved."

Game/Levels/Johdanto/L01.lean

@@ -3,31 +3,30 @@ import Game.Metadata
 World "Johdanto"
 Level 2
 
-Title "Socrates on mies"
+Title "Socrates on ihminen 0"
 
 Introduction "
-Tässä kentässä todistamme seuraavan väitteen: Socrates on mies, kun tiedämme, että Socrates on mies.
+Tässä kentässä todistamme seuraavan väitteen: Socrates on ihminen, kun tiedämme, että Socrates on ihminen.
 
-Todistus etenee seuraavasti. Oletuksista tiedämme, että Socrates on mies, joten Socrates on mies. □
+Todistus etenee seuraavasti. Oletuksista tiedämme, että Socrates on ihminen, joten Socrates on ihminen. □
 
 ## Oliot ja oletukset
 
 Lean esittää näytön alareunassa tärkeää tietoa tehtävän tilanteesta.
 
-**Objects**-otsikon alla on listattu tehtävässä annettujen alkioiden tyypit. Alkio `Socrates_is_man` on tyyppiä `Prop`. `Prop` on loogisten väitteiden tyyppi, ja kaikki sen alkiot ovat loogisia väitteitä, eli `Socrates_is_man` on looginen väite. Myös esimerkiksi `1 = 2` on tyyppiä `Prop`.
+**Objects**-otsikon alla on listattu tehtävässä käytettyjen alkioiden tyypit. Alkio `Socrates_is_human` on tyyppiä `Prop`. `Prop` on loogisten väitteiden tyyppi, ja kaikki sen alkiot ovat loogisia väitteitä, eli `Socrates_is_human` on looginen väite. Myös esimerkiksi `1 = 2` on tyyppiä `Prop`.
 
-**Assumptions**-otsikon alla on tehtävänannossa esitetyt oletukset ja niiden tyypit. Oletus `h` on tyyppiä `Socrates_is_man`, eli se on todistus väitteestä Socrates on mies.
+**Assumptions**-otsikon alla on tehtävänannossa esitetyt oletukset ja niiden tyypit. Oletus `h` on tyyppiä `Socrates_is_human`, eli se on todistus väitteestä Socrates on ihminen. Vinkki: sijoittamalla kursori `Socrates_is_human` tyypin päälle, saat lisätietoa tyypistä.
 
-Koska tavoitteena on todistaa se, mille `h` on jo todistus, voimme käyttää `h`:ta todistuksena käyttämällä `exact`-taktiikkaa.
+Koska tavoitteena on todistaa väite, mille `h` on jo todistus, voimme käyttää `h`:ta todistuksena käyttämällä `exact`-taktiikkaa.
 
 ## `exact`-taktiikka
 
 `exact`-taktiikalle syötetään välilyönnillä erotettuna todistus väitteestä. Todistuksen on oltava _täsmälleen_ oikeasta väitteestä, tai Lean antaa virheen.
-
-Ratkaise taso syöttämällä `exact h`
 "
 
-Statement (Socrates_is_man : Prop) (h : Socrates_is_man) : Socrates_is_man := by
+Statement (Socrates_is_human : Prop) (h : Socrates_is_human) : Socrates_is_human := by
+  Hint "Ratkaise taso syöttämällä `exact h`"
   exact h
 
 NewTactic exact

Game/Levels/Johdanto/L02.lean

@@ -3,19 +3,26 @@ import Game.Metadata
 World "Johdanto"
 Level 3
 
-Title "Socrates on mies 1"
+Title "Socrates on ihminen 1"
 
-Introduction "Tässä tasossa tehtävänä on todistaa, että tiedosta 'Socrates on mies' seuraa tieto 'Socrates on mies.'
+Introduction "
+Tässä tasossa tehtävänä on todistaa, että tiedosta 'Socrates on ihminen' seuraa tieto 'Socrates on ihminen.'
 
-Todistus alkaa tällä kertaa olettamalla, että väite 'Socrates on mies' implikaationuolen vasemmalla puolella pitää paikkansa, jolloin saamme sen kontekstiin, ja tavoitteeksi jää osoittaa, että 'Socrates on mies'.
+**Implikaatiosta**, eli loogisesta seurauksesta, käytetään nuolisymbolia $→$.
 
-Lean
+Todistus alkaa tällä kertaa olettamalla, että väite 'Socrates on ihminen' implikaationuolen vasemmalla puolella pitää paikkansa, jolloin saamme 'Socrates_is_human' osaksi oletuksia. Tavoitteeksi jää osoittaa, että 'Socrates on ihminen'. Ollaan siis päädytty täysin identtiseen tilaan, kuin edellisessä kentässä.
 
-Huomataan siis, että ollaan päädytty täysin identtiseen tilan
+Leanissä voidaan siirtää implikaationuolen vasen puoli maalista oletuksiin käyttämällä `intro`-taktiikkaa. `intro`-taktiikalle voi syöttää välilyönnillä nimen, joka tulee oletuksen nimeksi.
 "
 
-Statement (Socrates_is_man : Prop) : Socrates_is_man → Socrates_is_man := by
+Statement (Socrates_is_human : Prop) : Socrates_is_human → Socrates_is_human := by
+  Hint "Aloita kirjoittamalla `intro h`"
   intro h
+  Hint "Käytä juuri muodostamaasi oletusta todistamaan väite"
   exact h
 
+Conclusion "
+Huomaa, että voit navigoida todistusta liikkumalla eri riville, jolloin todistuksen _tila_ muuttuu.
+"
+
 NewTactic intro

Game/Levels/Johdanto/L03.lean

@@ -3,11 +3,22 @@ import Game.Metadata
 World "Johdanto"
 Level 4
 
-Title "Socrates 3"
+Title "Socrates on kuolevainen 0 (Modus Ponens)"
 
-Statement (Socrates_is_man Socrates_is_mortal : Prop) : (Socrates_is_man → Socrates_is_mortal) → Socrates_is_man → Socrates_is_mortal := by
-  intro hmm hm
-  apply hmm
-  exact hm
+Introduction "
+Tässä tasossa sinulla on oletuksissa
+0. Tieto siitä, että 'Socrates on ihminen': `sh`
+1. Tieto siitä, että 'jos Socrates on ihminen, niin Socrates on kuolevainen': `h`
+
+Väitteenä on todistaa, että 'Socrates on kuolevainen'. Loogisesti tämä seuraa selvästi oletuksesta `Socrates_is_human → Socrates_is_mortal`. Haluamme siis ensimmäiseksi _soveltaa_ oletusta `h`.
+
+Leanissa `apply`-taktiikka soveltaa implikaatiomuotoista oletusta. Kirjoittamalla `apply h` muutat maalin `Socrates_is_mortal`:ista `Socrates_is_human`:iksi. Huomaa, että soveltaessa tulee lukea implikaationuolta oikealta vasemmalle.
+"
+
+Statement (Socrates_is_human Socrates_is_mortal : Prop) (h : Socrates_is_human → Socrates_is_mortal) (sh : Socrates_is_human) : Socrates_is_mortal := by
+  Hint "Aloita soveltamalla oletusta `h`: `apply h`"
+  apply h
+  Hint "Maali muuttui väitteeksi `Socrates_is_human`, joka on jo oletuksissa: `sh`"
+  exact sh
 
 NewTactic apply

Game/Levels/Johdanto/L04.lean

@@ -3,11 +3,20 @@ import Game.Metadata
 World "Johdanto"
 Level 5
 
-Title "Socrates 3"
+Title "Socrates on kuolevainen 1"
 
-Statement (Socrates_is_man Socrates_is_mortal : Prop) : (Socrates_is_man → Socrates_is_mortal) → Socrates_is_man → Socrates_is_mortal := by
-  intro hmm hm
-  apply hmm
-  exact hm
+Introduction "
+Tehtävä on sama kuin edellinen, mutta sinulla ei ole käytössä `apply`-taktiikkaa.
 
-NewTactic apply
+Konstruktiivisessa logiikassa implikaatio on sama kuin funktio. `h : Socrates_is_human → Socrates_is_mortal` on funktio joka muuttaa todistuksen väitteestä `Socrates_is_human` todistukseksi `Socrates_is_mortal`.
+
+Funktiokutsu Leanissä kirjoitetaan ilman sulkeita, eli jos `f : A → B` ja `a : A` niin `f a` on tyyppiä `B`.
+
+`exact`-taktiikalle voi syöttää minkä tahansa lausekkeen, jonka tyyppi on oikea, esim. `exact f a` sulkee maalin `B`.
+"
+
+Statement (Socrates_is_human Socrates_is_mortal : Prop) (h : Socrates_is_human → Socrates_is_mortal) (sh : Socrates_is_human) : Socrates_is_mortal := by
+  Hint "Saat todistuksen väitteestä kutsumalla funktiota `h` arvolla `sh`: `exact h sh`"
+  exact h sh
+
+OnlyTactic exact

Game/Levels/Johdanto/L05.lean

@@ -3,11 +3,9 @@ import Game.Metadata
 World "Johdanto"
 Level 6
 
-Title "Socrates 4"
+Title "Socrates on kuolevainen 2"
 
-Statement (Socrates_is_man Socrates_is_mortal : Prop) : Socrates_is_man → (Socrates_is_man → Socrates_is_mortal) → Socrates_is_mortal := by
+Statement (Socrates_is_human Socrates_is_mortal : Prop) : Socrates_is_human → (Socrates_is_human → Socrates_is_mortal) → Socrates_is_mortal := by
   intro hmm hm
   apply hm
   exact hmm
-
-NewTactic apply

Game/Levels/Johdanto/L06.lean

@@ -6,6 +6,6 @@ Level 7
 
 Title "Socrates (extra)"
 
-Statement (Human : Type) (Men Mortal: Set (Human)) (Socrates : Human) (socrates_is_man : Socrates ∈ Men) (mortality_of_men : ∀ man ∈ Men, man ∈ Mortal) : Socrates ∈ Mortal := by
+Statement (Human : Type) (Men Mortal: Set (Human)) (Socrates : Human) (Socrates_is_human : Socrates ∈ Men) (mortality_of_men : ∀ man ∈ Men, man ∈ Mortal) : Socrates ∈ Mortal := by
   apply mortality_of_men
-  exact socrates_is_man
+  exact Socrates_is_human

Game/Levels/Johdanto/L07.lean

@@ -6,6 +6,6 @@ Level 8
 
 Title "Socrates (extra)"
 
-Statement (Human : Type) (Men Mortal : Set (Human)) (Socrates : Human) (socrates_is_man : Socrates ∈ Men) (mortality_of_men : Men ⊆ Mortal) : Socrates ∈ Mortal := by
+Statement (Human : Type) (Men Mortal : Set (Human)) (Socrates : Human) (Socrates_is_human : Socrates ∈ Men) (mortality_of_men : Men ⊆ Mortal) : Socrates ∈ Mortal := by
   apply mortality_of_men
-  exact socrates_is_man
+  exact Socrates_is_human

Game/Levels/Konjunktio.lean

@@ -4,7 +4,6 @@ import Game.Levels.Konjunktio.L02
 import Game.Levels.Konjunktio.L03
 import Game.Levels.Konjunktio.L04
 import Game.Levels.Konjunktio.L05
-import Game.Levels.Konjunktio.L06
 
 
 World "Konjunktio"

Game/Levels/Konjunktio/L05.lean

@@ -4,9 +4,13 @@ import Game.Metadata
 World "Konjunktio"
 Level 6
 
-Title "Konjunktio 5"
+Title "Konjunktio 6"
 
-Statement (A B : Prop) (h : A ∧ B) : B ∧ A := by
+Statement (h : (A ∧ B ∧ C ∧ (D ∧ (E ∧ F)) ∧ G ∧ H ∧ I) ∧ J ∧ (K ∧ L ∧ M ∧ N ∧ (O ∧ P) ∧ Q) ∧ R ∧ (S ∧ T ∧ (U ∧ V)) ∧ ((W ∧ X) ∧ Y) ∧ Z) : L ∧ E ∧ A ∧ N := by
   constructor
-  exact h.2
-  exact h.1
+  exact h.2.2.1.2.1
+  constructor
+  exact h.1.2.2.2.1.2.1
+  constructor
+  exact h.1.1
+  exact h.2.2.1.2.2.2.1

Game/Levels/Negaatio.lean

@@ -7,8 +7,6 @@ import Game.Levels.Negaatio.L05
 import Game.Levels.Negaatio.L06
 import Game.Levels.Negaatio.L07
 import Game.Levels.Negaatio.L08
-import Game.Levels.Negaatio.L09
-
 
 World "Negaatio"
 Title "¬ maailma"

Game/Levels/Negaatio/L02.lean

@@ -3,13 +3,11 @@ import Game.Metadata
 World "Negaatio"
 Level 3
 
-Title "Epätodesta voidaan todistaa mitä tahansa"
+Title "Kaksoisepätosi"
 
-Introduction "Edellisessä tehtävässä huomattiin, että tapauksessa, jossa kontekstista löytyy epätotuus, voidaan todistaa 'False'. Tässä tasossa havainnollistetaan, että tällaisessa tapauksessa voidaan oikeastaan todistaa mitä tahansa, esimerkiksi se, että Socrates syö kenkiä."
+Introduction ""
 
-Statement (socrates_syo_kenkia : Prop) (f : False) : socrates_syo_kenkia := by
-  Hint "Kannattaa kokeilla 'exfalso'-taktiikkaa, jonka avulla todistat väitteen todistamalla sen negaatiosta syntyvän ristiriidan."
-  exfalso
-  exact f
-
-NewTactic exfalso
+Statement (P : Prop) (x : P) : ¬¬P := by
+  intro np
+  apply np
+  exact x

Game/Levels/Negaatio/L03.lean

@@ -3,11 +3,11 @@ import Game.Metadata
 World "Negaatio"
 Level 4
 
-Title "Kaksoisepätosi"
+Title "Modus Tollens"
 
 Introduction ""
 
-Statement (P : Prop) (x : P) : ¬¬P := by
-  intro np
-  apply np
-  exact x
+Statement (P Q : Prop) (h : P → Q) (nq : ¬ Q) : ¬P := by
+  intro p
+  apply nq
+  exact h p

Game/Levels/Negaatio/L04.lean

@@ -3,11 +3,11 @@ import Game.Metadata
 World "Negaatio"
 Level 5
 
-Title "Modus Tollens"
+Title "Itseristiriita"
 
 Introduction ""
 
-Statement (P Q : Prop) (h : P → Q) (nq : ¬ Q) : ¬P := by
+Statement (P : Prop) (h : P → ¬ P) : ¬P := by
   intro p
-  apply nq
-  exact h p
+  apply h p
+  exact p

Game/Levels/Negaatio/L05.lean

@@ -3,11 +3,12 @@ import Game.Metadata
 World "Negaatio"
 Level 6
 
-Title "Itseristiriita"
+Title "Negaatio 6"
 
 Introduction ""
 
-Statement (P : Prop) (h : P → ¬ P) : ¬P := by
-  intro p
-  apply h p
-  exact p
+Statement (P Q : Prop) (h : ¬(P → Q)) : ¬Q := by
+  intro q
+  apply h
+  intro _p
+  exact q