Iff Tactics

Author: Trequetrum

Game/Levels/IffIntro/L01.lean

@@ -41,7 +41,3 @@ 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

Game/Levels/IffIntro/L02.lean

@@ -28,8 +28,3 @@ For a biconditional like `h : P ↔ Q`,
 /-- 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

Game/Levels/IffIntro/L03.lean

@@ -17,11 +17,4 @@ 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
+  exact h2 ≫ h1.mp

Game/Levels/IffIntro/L04.lean

@@ -17,11 +17,4 @@ 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
+  exact h1.mpr ≫ h2

Game/Levels/IffIntro/L05.lean

@@ -111,12 +111,3 @@ exact ⟨
 ```
 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

Game/Levels/IffIntro/L06.lean

@@ -70,8 +70,3 @@ 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

Game/Levels/IffIntro/L07.lean

@@ -9,9 +9,6 @@ Title "IffBoss"
 OnlyTactic
   exact
   «have»
-  rw
-  «repeat»
-  nth_rewrite
 
 Introduction "
 # BOSS LEVEL

Game/Levels/IffTactic/L01.lean

@@ -6,42 +6,16 @@ World "IffTactic"
 Level 1
 Title "Iff_Intro"
 
-NewTheorem GameLogic.iff_intro
-NewDefinition GameLogic.iff_def
 OnlyTactic
-  exact
-  «have»
+  assumption
+  constructor
+  «repeat»
 
 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₂⟩`
+# Using Tactics
+The tactics available to you should provide a hint for what to do. You'll be using a tactic in a context you havn't tried before, but the result should make sense once you try it and see what happens.
 "
 
-/-- 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
+Statement (P Q : Prop) (hsj: Q → P) (hjs: P → Q) : Q ↔ P := by
+  constructor
+  repeat assumption

Game/Levels/IffTactic/L02.lean

@@ -6,30 +6,18 @@ World "IffTactic"
 Level 2
 Title "Conjuctive Iff"
 
-NewTheorem
-  GameLogic.iff_mp
-  GameLogic.iff_mpr
 OnlyTactic
-  exact
-  «have»
+  assumption
+  cases
+  constructor
+  «repeat»
 
 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.
+# Using Tactics
+Last level you learned that `constructor` works for biconditionals in the the same way it works for conjunction. This level demonstrates that `cases` works the way you may expect as well.
 "
 
-/-- 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
+Statement (P Q : Prop) (h : P ↔ ¬Q) : (P → ¬Q) ∧ (¬Q → P) := by
   cases h
-  constructor <;> assumption
+  constructor
+  repeat assumption

Game/Levels/IffTactic/L03.lean

@@ -7,20 +7,15 @@ Level 3
 Title "Iff_mp"
 
 OnlyTactic
-  exact
-  «have»
+  intro
+  apply
+  assumption
 
 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