Metaprogramming.md (3092B)
1 +++ 2 title = 'Metaprogramming' 3 +++ 4 # Metaprogramming 5 You can extend Lean with custom tactics/tools; this is metaprogramming. 6 7 ## Tactics, tactic combinators 8 Combinators help if you have to do the same thing multiple times, or recover from failures. 9 10 - `repeat`: applies argument repeatedly on all goals until it can't be applied any further 11 - `iterate`: applies argument repeatedly on first goal until it fails, and then stops 12 - `<|>` ('orelse'): tries first argument, and if it fails, applies second argument 13 - `all_goals`: applies argument once to each goal, succeeds only if succeeds on all goals 14 - `any_goals`: applies argument once to each goal, succeeds if succeeds on any goal 15 - `try`: transforms argument into tactic that never fails (i.e. try it and if you fail it's ok) 16 - `solve1`: if argument doesn't prove the goal, fail 17 18 ## The metaprogramming monad 19 `meta` lets a function call other metafunctions. 20 Tactics have access to: 21 - list of goals as metavariables (`tactic.target`, `tactic.get_goals`) 22 - the elaborator to elaborate expressions and find their type 23 - the environment with all declarations and inductive types (`tactic.local_context`, `tactic.get_local ``hypothesis`) 24 - the attributes (e.g. the list of `@[simp]` rules) 25 26 You can print stuff with `tactic.trace`. 27 `run_cmd` can run a tactic. 28 29 For example, we can rewrite `assumption` which looks through all hypotheses in the context and succeeds if it finds one that works with the goal. 30 31 ```lean 32 meta def exact_list : list expr → tactic unit 33 | [] := tactic.fail "no matching hypothesis in environment" 34 | (h :: hs) := 35 do { tactic.trace "trying", 36 tactic.trace h, 37 tactic.exact h } 38 <|> exact_list hs 39 40 meta def my_assumption : tactic unit := 41 do 42 hs ← tactic.local_context, 43 exact_list hs 44 ``` 45 46 The framework revolves around five main types: 47 - `tactic`: manages proof state, global context, etc 48 - `name`: represents structured name 49 - `expr`: represents expression (term) as abstract syntax tree 50 - `expr.var` gets variables based on De Bruijn indices 51 - `expr.lam` is a lambda expression 52 - `expr.sort` are 'universes' (`Sort 0` is `Prop`, `Sort 1` is `Type`, etc) 53 - `expr.local_const` is hypothesis 54 - `expr.pi` is used for pi binders (e.g. ∀) 55 - `declaration`: represents constant declaration, definition, axiom, or lemma 56 - `environment`: stores all declarations and notations that make up global context 57 58 Unelaborated expressions (pre-expressions) omit some information, elaborated expressions have everything. 59 60 We can create literal expressions: 61 - expressions with single backtick must be fully elaborated 62 - expressions with two backticks are pre-expressions 63 - expressions with three backticks are pre-expressions without name checking 64 65 Similar for names: 66 - names with single backtick are not checked for existence 67 - names with two backticks are resolved and checked 68 69 Antiquotation lets you embed existing expression into larger expression, using prefix `%%` and name from current context. 70 You can also use them in pattern matching, like `(%%a + %%b = %%c) ← tactic.target`