From bc380f540778b65bad8f3a996579426f6e73f7a2 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 20 Apr 2024 10:53:01 +0900 Subject: [PATCH] format code: trim whitespace, add annotation --- lean/main/05_syntax.lean | 8 ++++---- lean/main/06_macros.lean | 10 +++++----- lean/main/07_elaboration.lean | 14 +++++++------- lean/main/09_tactics.lean | 24 ++++++++++++------------ 4 files changed, 28 insertions(+), 28 deletions(-) diff --git a/lean/main/05_syntax.lean b/lean/main/05_syntax.lean index d93868b..a06a0f0 100644 --- a/lean/main/05_syntax.lean +++ b/lean/main/05_syntax.lean @@ -563,15 +563,15 @@ 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`. 2. Consider the following syntax categories: `term`, `command`, `tactic`; and 3 syntax rules given below. Make use of each of these newly defined syntaxes. - ``` + ```lean syntax "good morning" : term syntax "hello" : command syntax "yellow" : tactic diff --git a/lean/main/06_macros.lean b/lean/main/06_macros.lean index 49c9d74..d00d69f 100644 --- a/lean/main/06_macros.lean +++ b/lean/main/06_macros.lean @@ -35,7 +35,7 @@ to indicate that "it doesn't feel responsible for this syntax". In this case it's merely used to fill a wildcard pattern that should never be reached anyways. However we can in fact register multiple macros for the same syntax this way -if we desire, they will be tried one after another (the later registered ones have +if we desire, they will be tried one after another (the later registered ones have higher priority) -- is "higher" correct? until one throws either a real error using `Macro.throwError` or succeeds, that is it does not `Macro.throwUnsupported`. Let's see this in action: @@ -169,7 +169,7 @@ for example macro creating macros, we can escape the anti quotation using: `` `( If we want to specify the syntax kind we wish `x` to be interpreted as we can make this explicit using: `` `($x:term) `` where `term` can be replaced with any other valid syntax category (e.g. `command`) or parser -(e.g. `ident`). +(e.g. `ident`). So far this is only a more formal explanation of the intuitive things we've already seen in the syntax chapter and up to now in this chapter, @@ -198,11 +198,11 @@ For example: -/ -- syntactically cut away the first element of a tuple if possible -syntax "cut_tuple " "(" term ", " term,+ ")" : term +syntax "cut_tuple " "(" term ", " term,+ ")" : term macro_rules -- cutting away one element of a pair isn't possible, it would not result in a tuple - | `(cut_tuple ($x, $y)) => `(($x, $y)) + | `(cut_tuple ($x, $y)) => `(($x, $y)) | `(cut_tuple ($x, $y, $xs,*)) => `(($y, $xs,*)) #check cut_tuple (1, 2) -- (1, 2) : Nat × Nat @@ -225,7 +225,7 @@ we know so far we'd have to write two `macro_rules` now, one for the case with, one for the case without the optional argument. However the rest of the syntactic translation works exactly the same with and without the optional argument so what we can do using a splice here is to essentially -define both cases at once: +define both cases at once: -/ macro_rules diff --git a/lean/main/07_elaboration.lean b/lean/main/07_elaboration.lean index 23f597f..ac904c9 100644 --- a/lean/main/07_elaboration.lean +++ b/lean/main/07_elaboration.lean @@ -173,7 +173,7 @@ elab "#findCElab " c:command : command => do /-! TODO: Maybe we should also add a mini project that demonstrates a non # style command aka a declaration, although nothing comes to mind right now. -TODO: Define a `conjecture` declaration, similar to `lemma/theorem`, except that +TODO: Define a `conjecture` declaration, similar to `lemma/theorem`, except that it is automatically sorried. The `sorry` could be a custom one, to reflect that the "conjecture" might be expected to be true. -/ @@ -316,7 +316,7 @@ def myanonImpl : TermElab := fun stx typ? => do -- Term elaborators can only postpone execution once, so the elaborator -- doesn't end up in an infinite loop. Hence, we only try to postpone it, -- otherwise we may cause an error. - tryPostponeIfNoneOrMVar typ? + tryPostponeIfNoneOrMVar typ? -- If we haven't found the type after postponing just error let some typ := typ? | throwError "expected type must be known" if typ.isMVar then @@ -338,7 +338,7 @@ syntax sugar of the `elab` syntax instead: -/ -- This `t` syntax will effectively perform the first two lines of `myanonImpl` -elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do +elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do sorry @@ -377,8 +377,8 @@ elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do Please add these semantics: - **a)** using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`. - **b)** using `syntax` + `elab_rules`. + **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`. @@ -392,8 +392,8 @@ elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do Please add these semantics: - **a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`. - **b)** using `syntax` + `elab_rules`. + **a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`. + **b)** using `syntax` + `elab_rules`. **c)** using `elab`. -/ diff --git a/lean/main/09_tactics.lean b/lean/main/09_tactics.lean index 2b683c2..2a8f990 100644 --- a/lean/main/09_tactics.lean +++ b/lean/main/09_tactics.lean @@ -593,9 +593,9 @@ tactic infrastructure and the parsing front-end. ## Exercises 1. Consider the theorem `p ∧ q ↔ q ∧ p`. We could either write its proof as a proof term, or construct it using the tactics. - When we are writing the proof of this theorem *as a proof term*, we're gradually filling up `_`s with certain expressions, step by step. Each such step corresponds to a tactic. + When we are writing the proof of this theorem *as a proof term*, we're gradually filling up `_`s with certain expressions, step by step. Each such step corresponds to a tactic. - There are many combinations of steps in which we could write this proof term - but consider the sequence of steps we wrote below. Please write each step as a tactic. + There are many combinations of steps in which we could write this proof term - but consider the sequence of steps we wrote below. Please write each step as a tactic. The tactic `step_1` is filled in, please do the same for the remaining tactics (for the sake of the exercise, try to use lower-level apis, such as `mkFreshExprMVar`, `mvarId.assign` and `modify fun _ => { goals := ~)`. ```lean @@ -653,7 +653,7 @@ tactic infrastructure and the parsing front-end. -- 1. Create new `_`s with appropriate types. let mvarId1 ← mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := "red") - let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue") + let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue") -- 2. Assign the main goal to the expression `Iff.intro _ _`. mvarId.assign (mkAppN (Expr.const `Iff.intro []) #[a, b, mvarId1, mvarId2]) @@ -670,13 +670,13 @@ tactic infrastructure and the parsing front-end. step_4 ``` -2. In the first exercise, we used lower-level `modify` api to update our goals. - `liftMetaTactic`, `setGoals`, `appendGoals`, `replaceMainGoal`, `closeMainGoal`, etc. are all syntax sugars on top of `modify fun s : State => { s with goals := myMvarIds }`. - Please rewrite the `forker` tactic with: +2. In the first exercise, we used lower-level `modify` api to update our goals. + `liftMetaTactic`, `setGoals`, `appendGoals`, `replaceMainGoal`, `closeMainGoal`, etc. are all syntax sugars on top of `modify fun s : State => { s with goals := myMvarIds }`. + Please rewrite the `forker` tactic with: - **a)** `liftMetaTactic` - **b)** `setGoals` - **c)** `replaceMainGoal` + **a)** `liftMetaTactic` + **b)** `setGoals` + **c)** `replaceMainGoal` ```lean elab "forker" : tactic => do @@ -709,9 +709,9 @@ tactic infrastructure and the parsing front-end. For each of the points below, create a tactic `introductor` (one per each point), that turns the goal `(ab: a = b) → (bc: b = c) → (a = c)`: - **a)** into the goal `(a = c)` with hypotheses `(ab✝: a = b)` and `(bc✝: b = c)`. - **b)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(ab: a = b)`. - **c)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(hello: a = b)`. + **a)** into the goal `(a = c)` with hypotheses `(ab✝: a = b)` and `(bc✝: b = c)`. + **b)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(ab: a = b)`. + **c)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(hello: a = b)`. ```lean example (a b c : Nat) : (ab: a = b) → (bc: b = c) → (a = c) := by