Merge pull request #98 from lakesare/lakesare_exercises_3

Exercises for Ch.Tactics

Author: hargoniX

README.md

@@ -15,18 +15,19 @@ A PDF is [available here for download](../../releases/download/latest/Metaprogra
     8. [DSLs](md/main/08_dsls.md)
     9. [Tactics](md/main/09_tactics.md)
     10. [Cheat sheet](md/main/10_cheat-sheet.md)
-* Extra
     1. [Options](md/extra/01_options.md)
     2. [Attributes](md/extra/02_attributes.md)
-    1. [Pretty Printing](md/extra/03_pretty-printing.md)
+    3. [Pretty Printing](md/extra/03_pretty-printing.md)
 * Solutions to exercises
-    1. ...
-    2. ...
+    1. Introduction
+    2. Overview
     3. [Expressions](md/solutions/03_expressions.md)
     4. [`MetaM`](md/solutions/04_metam.md)
     5. [`Syntax`](md/solutions/05_syntax.md)
-    6. ...
+    6. Macros
     7. [Elaboration](md/solutions/07_elaboration.md)
+    8. DSLs
+    9. [Tactics](md/solutions/09_tactics.md)
 
 Sources to extract material from:
 * [Material written by Ed](https://github.com/leanprover-community/mathlib4/blob/tutorial/docs/metaprogramming/02_metavariables.md)

lean/main/04_metam.lean

@@ -1214,47 +1214,47 @@ Notice that changing the type of the metavariable from `Nat` to, for example, `S
 2. [**Metavariables**] What would `instantiateMVars (Lean.mkAppN (Expr.const 'Nat.add []) #[mkNatLit 1, mkNatLit 2])` output?
 3. [**Metavariables**] Fill in the missing lines in the following code.
 
-  ```
-  #eval show MetaM Unit from do
-    let oneExpr := Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero [])
-    let twoExpr := Expr.app (Expr.const `Nat.succ []) oneExpr
-
-    -- Create `mvar1` with type `Nat`
-    -- let mvar1 ← ...
-    -- Create `mvar2` with type `Nat`
-    -- let mvar2 ← ...
-    -- Create `mvar3` with type `Nat`
-    -- let mvar3 ← ...
-
-    -- Assign `mvar1` to `2 + ?mvar2 + ?mvar3`
-    -- ...
-
-    -- Assign `mvar3` to `1`
-    -- ...
-
-    -- Instantiate `mvar1`, which should result in expression `2 + ?mvar2 + 1`
-    ...
-  ```
+    ```lean
+    #eval show MetaM Unit from do
+      let oneExpr := Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero [])
+      let twoExpr := Expr.app (Expr.const `Nat.succ []) oneExpr
+
+      -- Create `mvar1` with type `Nat`
+      -- let mvar1 ← ...
+      -- Create `mvar2` with type `Nat`
+      -- let mvar2 ← ...
+      -- Create `mvar3` with type `Nat`
+      -- let mvar3 ← ...
+
+      -- Assign `mvar1` to `2 + ?mvar2 + ?mvar3`
+      -- ...
+
+      -- Assign `mvar3` to `1`
+      -- ...
+
+      -- Instantiate `mvar1`, which should result in expression `2 + ?mvar2 + 1`
+      ...
+    ```
 4. [**Metavariables**] Consider the theorem `red`, and tactic `explore` below.  
-  a) What would be the `type` and `userName` of metavariable `mvarId`?  
-  b) What would be the `type`s and `userName`s of all local declarations in this metavariable's local context?  
+  **a)** What would be the `type` and `userName` of metavariable `mvarId`?  
+  **b)** What would be the `type`s and `userName`s of all local declarations in this metavariable's local context?  
   Print them all out.
 
-  ```
-  elab "explore" : tactic => do
-    let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
-    let metavarDecl : MetavarDecl ← mvarId.getDecl
+    ```lean
+    elab "explore" : tactic => do
+      let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
+      let metavarDecl : MetavarDecl ← mvarId.getDecl
 
-    IO.println "Our metavariable"
-    -- ...
+      IO.println "Our metavariable"
+      -- ...
 
-    IO.println "All of its local declarations"
-    -- ...
+      IO.println "All of its local declarations"
+      -- ...
 
-  theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
-    explore
-    sorry
-  ```
+    theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
+      explore
+      sorry
+    ```
 5. [**Metavariables**] Write a tactic `solve` that proves the theorem `red`.
 6. [**Computation**] What is the normal form of the following expressions:  
   **a)** `fun x => x` of type `Bool → Bool`  
@@ -1270,36 +1270,36 @@ Notice that changing the type of the metavariable from `Nat` to, for example, `S
   **f)** `2 + ?a =?= 2 + 1`
 9. [**Computation**] Write down what you expect the following code to output.
 
-```
-@[reducible] def reducibleDef     : Nat := 1 -- same as `abbrev`
-@[instance] def instanceDef       : Nat := 2 -- same as `instance`
-def defaultDef                    : Nat := 3
-@[irreducible] def irreducibleDef : Nat := 4
+    ```lean
+    @[reducible] def reducibleDef     : Nat := 1 -- same as `abbrev`
+    @[instance] def instanceDef       : Nat := 2 -- same as `instance`
+    def defaultDef                    : Nat := 3
+    @[irreducible] def irreducibleDef : Nat := 4
 
-@[reducible] def sum := [reducibleDef, instanceDef, defaultDef, irreducibleDef]
+    @[reducible] def sum := [reducibleDef, instanceDef, defaultDef, irreducibleDef]
 
-#eval show MetaM Unit from do
-  let constantExpr := Expr.const `sum []
+    #eval show MetaM Unit from do
+      let constantExpr := Expr.const `sum []
 
-  Meta.withTransparency Meta.TransparencyMode.reducible do
-    let reducedExpr ← Meta.reduce constantExpr
-    dbg_trace (← ppExpr reducedExpr) -- ...
+      Meta.withTransparency Meta.TransparencyMode.reducible do
+        let reducedExpr ← Meta.reduce constantExpr
+        dbg_trace (← ppExpr reducedExpr) -- ...
 
-  Meta.withTransparency Meta.TransparencyMode.instances do
-    let reducedExpr ← Meta.reduce constantExpr
-    dbg_trace (← ppExpr reducedExpr) -- ...
+      Meta.withTransparency Meta.TransparencyMode.instances do
+        let reducedExpr ← Meta.reduce constantExpr
+        dbg_trace (← ppExpr reducedExpr) -- ...
 
-  Meta.withTransparency Meta.TransparencyMode.default do
-    let reducedExpr ← Meta.reduce constantExpr
-    dbg_trace (← ppExpr reducedExpr) -- ...
+      Meta.withTransparency Meta.TransparencyMode.default do
+        let reducedExpr ← Meta.reduce constantExpr
+        dbg_trace (← ppExpr reducedExpr) -- ...
 
-  Meta.withTransparency Meta.TransparencyMode.all do
-    let reducedExpr ← Meta.reduce constantExpr
-    dbg_trace (← ppExpr reducedExpr) -- ...
+      Meta.withTransparency Meta.TransparencyMode.all do
+        let reducedExpr ← Meta.reduce constantExpr
+        dbg_trace (← ppExpr reducedExpr) -- ...
 
-  let reducedExpr ← Meta.reduce constantExpr
-  dbg_trace (← ppExpr reducedExpr) -- ...
-```
+      let reducedExpr ← Meta.reduce constantExpr
+      dbg_trace (← ppExpr reducedExpr) -- ...
+    ```
 10. [**Constructing Expressions**] Create expression `fun x, 1 + x` in two ways:  
   **a)** not idiomatically, with loose bound variables  
   **b)** idiomatically.  
@@ -1312,20 +1312,20 @@ def defaultDef                    : Nat := 3
 13. [**Constructing Expressions**] Create expression `fun (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1)` idiomatically.
 14. [**Constructing Expressions**] What would you expect the output of the following code to be?
 
-```
-#eval show Lean.Elab.Term.TermElabM _ from do
-  let stx : Syntax ← `(∀ (a : Prop) (b : Prop), a ∨ b → b → a ∧ a)
-  let expr ← Elab.Term.elabTermAndSynthesize stx none
+    ```lean
+    #eval show Lean.Elab.Term.TermElabM _ from do
+      let stx : Syntax ← `(∀ (a : Prop) (b : Prop), a ∨ b → b → a ∧ a)
+      let expr ← Elab.Term.elabTermAndSynthesize stx none
 
-  let (_, _, conclusion) ← forallMetaTelescope expr
-  dbg_trace conclusion -- ...
+      let (_, _, conclusion) ← forallMetaTelescope expr
+      dbg_trace conclusion -- ...
 
-  let (_, _, conclusion) ← forallMetaBoundedTelescope expr 2
-  dbg_trace conclusion -- ...
+      let (_, _, conclusion) ← forallMetaBoundedTelescope expr 2
+      dbg_trace conclusion -- ...
 
-  let (_, _, conclusion) ← lambdaMetaTelescope expr
-  dbg_trace conclusion -- ...
-```
+      let (_, _, conclusion) ← lambdaMetaTelescope expr
+      dbg_trace conclusion -- ...
+    ```
 15. [**Backtracking**] Check that the expressions `?a + Int` and `"hi" + ?b` are definitionally equal with `isDefEq` (make sure to use the proper types or `Option.none` for the types of your metavariables!).
 Use `saveState` and `restoreState` to revert metavariable assignments.
 -/

lean/main/05_syntax.lean

@@ -559,68 +559,68 @@ the bound variables, we refer the reader to the macro chapter.
 
 1. Create an "urgent minus 💀" notation such that `5 * 8 💀 4` returns `20`, and `8 💀 6 💀 1` returns `3`.
 
-**a)** Using `notation` command.  
-**b)** Using `infix` command.  
-**c)** Using `syntax` command.  
+    **a)** Using `notation` command.  
+    **b)** Using `infix` command.  
+    **c)** Using `syntax` command.  
 
-Hint: multiplication in Lean 4 is defined as `infixl:70 " * " => HMul.hMul`.
+    Hint: multiplication in Lean 4 is defined as `infixl:70 " * " => HMul.hMul`.
 
 2. Consider the following syntax categories: `term`, `command`, `tactic`; and 3 syntax rules given below. Make use of each of these newly defined syntaxes.
 
-```
-  syntax "good morning" : term
-  syntax "hello" : command
-  syntax "yellow" : tactic
-```
+    ```
+      syntax "good morning" : term
+      syntax "hello" : command
+      syntax "yellow" : tactic
+    ```
 
 3. Create a `syntax` rule that would accept the following commands:
 
-- `red red red 4`
-- `blue 7`
-- `blue blue blue blue blue 18`
+    - `red red red 4`
+    - `blue 7`
+    - `blue blue blue blue blue 18`
 
-(So, either all `red`s followed by a number; or all `blue`s followed by a number; `red blue blue 5` - shouldn't work.)
+    (So, either all `red`s followed by a number; or all `blue`s followed by a number; `red blue blue 5` - shouldn't work.)
 
-Use the following code template:
+    Use the following code template:
 
-```
-syntax (name := colors) ...
--- our "elaboration function" that infuses syntax with semantics
-@[command_elab colors] def elabColors : CommandElab := λ stx => Lean.logInfo "success!"
-```
+    ```lean
+    syntax (name := colors) ...
+    -- our "elaboration function" that infuses syntax with semantics
+    @[command_elab colors] def elabColors : CommandElab := λ stx => Lean.logInfo "success!"
+    ```
 
 4. Mathlib has a `#help option` command that displays all options available in the current environment, and their descriptions. `#help option pp.r` will display all options starting with a "pp.r" substring.
 
-Create a `syntax` rule that would accept the following commands:
+    Create a `syntax` rule that would accept the following commands:
 
-- `#better_help option`
-- `#better_help option pp.r`
-- `#better_help option some.other.name`
+    - `#better_help option`
+    - `#better_help option pp.r`
+    - `#better_help option some.other.name`
 
-Use the following template:
+    Use the following template:
 
-```
-syntax (name := help) ...
--- our "elaboration function" that infuses syntax with semantics
-@[command_elab help] def elabHelp : CommandElab := λ stx => Lean.logInfo "success!"
-```
+    ```lean
+    syntax (name := help) ...
+    -- our "elaboration function" that infuses syntax with semantics
+    @[command_elab help] def elabHelp : CommandElab := λ stx => Lean.logInfo "success!"
+    ```
 
 5. Mathlib has a ∑ operator. Create a `syntax` rule that would accept the following terms:
 
-- `∑ x in { 1, 2, 3 }, x^2`
-- `∑ x in { "apple", "banana", "cherry" }, x.length`
+    - `∑ x in { 1, 2, 3 }, x^2`
+    - `∑ x in { "apple", "banana", "cherry" }, x.length`
 
-Use the following template:
+    Use the following template:
 
-```
-import Std.Classes.SetNotation
-import Std.Util.ExtendedBinder
-syntax (name := bigsumin) ...
--- our "elaboration function" that infuses syntax with semantics
-@[term_elab bigsumin] def elabSum : TermElab := λ stx tp => return mkNatLit 666
-```
+    ```lean
+    import Std.Classes.SetNotation
+    import Std.Util.ExtendedBinder
+    syntax (name := bigsumin) ...
+    -- our "elaboration function" that infuses syntax with semantics
+    @[term_elab bigsumin] def elabSum : TermElab := λ stx tp => return mkNatLit 666
+    ```
 
-Hint: use the `Std.ExtendedBinder.extBinder` parser.
-Hint: you need Std4 installed in your Lean project for these imports to work.
+    Hint: use the `Std.ExtendedBinder.extBinder` parser.
+    Hint: you need Std4 installed in your Lean project for these imports to work.
 
 -/

lean/main/07_elaboration.lean

@@ -348,52 +348,52 @@ elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
 
 1. Consider the following code. Rewrite `syntax` + `@[term_elab hi]... : TermElab` combination using just `elab`.
 
-```
-syntax (name := hi) term " ♥ " " ♥ "? " ♥ "? : term
-
-@[term_elab hi]
-def heartElab : TermElab := fun stx tp =>
-  match stx with
-    | `($l:term ♥) => do
-      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
-      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 1)
-    | `($l:term ♥♥) => do
-      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
-      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 2)
-    | `($l:term ♥♥♥) => do
-      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
-      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 3)
-    | _ =>
-      throwUnsupportedSyntax
-```
+    ```lean
+    syntax (name := hi) term " ♥ " " ♥ "? " ♥ "? : term
+
+    @[term_elab hi]
+    def heartElab : TermElab := fun stx tp =>
+      match stx with
+        | `($l:term ♥) => do
+          let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+          return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 1)
+        | `($l:term ♥♥) => do
+          let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+          return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 2)
+        | `($l:term ♥♥♥) => do
+          let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+          return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 3)
+        | _ =>
+          throwUnsupportedSyntax
+    ```
 
 2. Here is some syntax taken from a real mathlib command `alias`.
 
-```
-syntax (name := our_alias) (docComment)? "our_alias " ident " ← " ident* : command
-```
+    ```
+    syntax (name := our_alias) (docComment)? "our_alias " ident " ← " ident* : command
+    ```
 
-We want `alias hi ← hello yes` to print out the identifiers after `←` - that is, "hello" and "yes".
+    We want `alias hi ← hello yes` to print out the identifiers after `←` - that is, "hello" and "yes".
 
-Please add these semantics:
+    Please add these semantics:
 
-**a)** using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`.  
-**b)** using `syntax` + `elab_rules`.  
-**c)** using `elab`.
+    **a)** using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`.  
+    **b)** using `syntax` + `elab_rules`.  
+    **c)** using `elab`.
 
 3. Here is some syntax taken from a real mathlib tactic `nth_rewrite`.
 
-```
-open Parser.Tactic
-syntax (name := nthRewriteSeq) "nth_rewrite " (config)? num rwRuleSeq (ppSpace location)? : tactic
-```
+    ```lean
+    open Parser.Tactic
+    syntax (name := nthRewriteSeq) "nth_rewrite " (config)? num rwRuleSeq (ppSpace location)? : tactic
+    ```
 
-We want `nth_rewrite 5 [←add_zero a] at h` to print out `"rewrite location!"` if the user provided location, and `"rewrite target!"` if the user didn't provide location.
+    We want `nth_rewrite 5 [←add_zero a] at h` to print out `"rewrite location!"` if the user provided location, and `"rewrite target!"` if the user didn't provide location.
 
-Please add these semantics:
+    Please add these semantics:
 
-**a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.  
-**b)** using `syntax` + `elab_rules`.  
-**c)** using `elab`.
+    **a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.  
+    **b)** using `syntax` + `elab_rules`.  
+    **c)** using `elab`.
 
 -/