/- Exercise 2.4: Functional Programming — Metaprogramming -/ open expr open tactic /- Question 1: A term exploder -/ /- In this exercise, we develop a string format for the `expr` metatype. By default, there is no `has_repr` instance to print a nice string. For example: -/ #eval (expr.app (expr.var 0) (expr.var 1) : expr) -- result: `[external]` #eval (`(λx : ℕ, x + x) : expr) -- result: `[external]` /- 1.1. Define a metafunction `expr.repr` that converts an `expr` into a `string`. It is acceptable to leave out some fields from the `expr` constructors, such as the level `l` of a sort, the binder information `bi` of a λ- or Π- binder, and the arguments of the `macro` constructor. Hint: Use `name.to_string` to convert a name to a string, and `repr` for other types that belong to the `has_repr` type class. -/ meta def expr.repr : expr → string | (var n) := "(var " ++ repr n ++ ")" | (sort l) := "sort" | (const n ls) := "(const " ++ n.to_string ++ ")" | (mvar n m t) := "(mvar " ++ n.to_string ++ " " ++ m.to_string ++ " " ++ expr.repr t ++ ")" | (local_const n m bi t) := "(local_const " ++ n.to_string ++ " " ++ m.to_string ++ " " ++ expr.repr t ++ ")" | (app e f) := "(app " ++ expr.repr e ++ " " ++ expr.repr f ++ ")" | (lam n bi e t) := "(lam " ++ n.to_string ++ " " ++ expr.repr e ++ " " ++ expr.repr t ++ ")" | (pi n bi e t) := "(pi " ++ n.to_string ++ " " ++ expr.repr e ++ " " ++ expr.repr t ++ ")" | (elet n g e f) := "(elet " ++ n.to_string ++ " " ++ expr.repr g ++ " " ++ expr.repr e ++ " " ++ expr.repr f ++ ")" | (macro d args) := "macro" /- 1.2. Register `expr.repr` in the `has_repr` type class, so that we can use `repr` without qualification in the future, and so that it is available to `#eval`. Hint: You will need the `meta` keyword in front of the command you enter. -/ meta instance : has_repr expr := ⟨expr.repr⟩ /- 1.3. Test your setup. -/ #eval (expr.app (expr.var 0) (expr.var 1) : expr) #eval (`(λx : ℕ, x + x) : expr) /- 1.4. Compare your answer with `expr.to_raw_fmt`. -/ /- Question 2: `destruct_and` on steroids -/ /- Recall from the lecture that `destruct_and` fails on the following easy goal: -/ example {a b c d : Prop} (h : a ∧ (b ∧ c) ∧ d) : b ∧ d := sorry /- We will now address this by developing a new tactic called `destro_and`, which applies both *des*truction and in*tro*duction rules for conjunction. It will also go automatically through the hypotheses instead of taking an argument. We will develop it in three steps. -/ /- 2.1. Develop a tactic `intro_ands` that replaces all goals of the form `a ∧ b` with two new goals `a` and `b` systematically, until all top-level conjunctions are gone. For this, we can use tactics such as `repeat` (which repeatedly applies a tactic on all goals until the tactic fails on each of the goal) and `applyc` (which can be used to apply a rule, in connection with backtick quoting). -/ meta def intro_ands : tactic unit := repeat (applyc `and.intro) example {a b c d : Prop} (h : a ∧ (b ∧ c) ∧ d) : b ∧ d := begin intro_ands, /- The proof state should be as follows: 2 goals a b c d : Prop, h : a ∧ (b ∧ c) ∧ d ⊢ b a b c d : Prop, h : a ∧ (b ∧ c) ∧ d ⊢ d -/ repeat { sorry } end example {a b c d : Prop} (h : a ∧ (b ∧ c) ∧ d) : b ∧ (a ∧ (c ∧ b)) := begin intro_ands, /- The proof state should be as follows: 4 goals a b c d : Prop, h : a ∧ (b ∧ c) ∧ d ⊢ b a b c d : Prop, h : a ∧ (b ∧ c) ∧ d ⊢ a a b c d : Prop, h : a ∧ (b ∧ c) ∧ d ⊢ c a b c d : Prop, h : a ∧ (b ∧ c) ∧ d ⊢ b -/ repeat { sorry } end /- 2.2. Develop a tactic `destruct_ands` that replaces hypotheses of the form `h : a ∧ b` by two new hypotheses `h_left : a` and `h_right : b` systematically, until all top-level conjunctions are gone. Here is imperative-style pseudocode that you can follow: 1. Retrieve the list of hypotheses from the context. This is provided by the metaconstant `local_context`. 2. Find the first hypothesis (= term) with a type (= proposition) of the form `_ ∧ _`. Here, you can use the `list.mfirst` function, in conjunction with pattern matching. You can use `infer_type` to query the type of a term. 3. Perform a case split on the first found hypothesis. This can be achieved using the `cases` metafunction. 4. Go to step 1. The above procedure might fail if there exists no hypotheses of the required form. Make sure to handle this failure gracefully using `<|>`. -/ meta def destruct_ands : tactic unit := (do hs ← local_context, h ← hs.mfirst (λh, do `(_ ∧ _) ← infer_type h, pure h), cases h, destruct_ands) <|> skip -- alternative solution: meta def destruct_ands_v2 : tactic unit := repeat (do hs ← local_context, h ← hs.mfirst (λh, do `(_ ∧ _) ← infer_type h, pure h), cases h, skip) example {a b c d : Prop} (h : a ∧ (b ∧ c) ∧ d) : b ∧ d := begin destruct_ands, /- The proof state should be as follows: a b c d : Prop, h_left : a, h_right_right : d, h_right_left_left : b, h_right_left_right : c ⊢ b ∧ d -/ sorry end /- 2.3. Finally, combine the two tactics developed above and the `assumption` tactic to implement the desired `destro_and` tactic. -/ meta def destro_and : tactic unit := do destruct_ands, intro_ands, all_goals assumption example {a b c d : Prop} (h : a ∧ (b ∧ c) ∧ d) : b ∧ d := by destro_and example {a b c d : Prop} (h : a ∧ (b ∧ c) ∧ d) : b ∧ (a ∧ (c ∧ b)) := by destro_and /- Question 3: A theorem finder -/ /- We will implement a function that allows us to find theorems by constants appearing in their statements. So given a list of constant names, the function will list all theorems in which all these constants appear. You can use the following metaconstants: * `declaration`: contains all data (name, type, value) associated with a declaration, i.e. axiom, theorem, constant, etc. * `tactic.get_env`: gives us access to the `environment`, a metatype thats lists all `declaration`s (especially all theorems) * `environment.fold` allows us to walk through the environment and collect data * `expr.fold` allows us to walk through an expression and collect data. -/ /- 3.1. Write a metafunction that checks whether an expression contains a specific constant. You can use `expr.fold` to walk through the expression, `||` and `ff` for Booleans, and `expr.is_constant_of` to check if an expression is a constant. -/ meta def term_contains (e : expr) (n : name) : bool := expr.fold e ff $ λe' d c, c || expr.is_constant_of e' n /- 3.2. Write a metafunction that checks whether an expression contains _all_ constants in a list. You can use `list.band` (Boolean and). -/ meta def term_contains_all (ns : list name) (e : expr) : bool := list.band $ list.map (term_contains e) ns /- 3.3. Produce the list of all theorems that contain all constants `ns` in their statement. `environment.fold` allows you to walk over the list of declarations. With `declaration.type`, you get the type of a theorem, and with `declaration.to_name` you get the name. -/ meta def list_constants (ns : list name) (e : environment) : list name := environment.fold e [] $ λdecl lst, if term_contains_all ns decl.type then decl.to_name :: lst else lst /- 3.4. Finally, develop a tactic that uses the above metafunctions to log all found theorems. You can use `trace` to log the results. -/ meta def find_constants (ns : list name) : tactic unit := do env ← get_env, list.mmap' trace (list_constants ns env) /- 3.5. Test your solution. -/ run_cmd find_constants [] -- lists all theorems run_cmd find_constants [`list.map, `function.comp]