|
| 1 | +/- |
| 2 | +Copyright (c) 2020 Dany Fabian. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Dany Fabian |
| 5 | +-/ |
| 6 | + |
| 7 | +import tactic.split_ifs |
| 8 | +/-! |
| 9 | + # Unfold cases tactic |
| 10 | +
|
| 11 | + In Lean, pattern matching expressions are not atomic parts of the syntax, but |
| 12 | + rather they are compiled down into simpler terms that are later checked by the kernel. |
| 13 | +
|
| 14 | + This allows Lean to have a minimalistic kernel but can occasionally lead an explosion |
| 15 | + of cases that need to be considered. What looks like one case in the `match` expression |
| 16 | + can in fact be compiled into many different cases that all need to proved by case analysis. |
| 17 | +
|
| 18 | + This tactic automates the process by allowing us to write down an equation `f x = y` |
| 19 | + where we know that `f x = y` is provably true, but does not hold definitionally. In that |
| 20 | + case the `unfold_cases` tactic will continue unfolding `f` and introducing `cases` where |
| 21 | + necessary until the left hand side becomes definitionally equal to the right hand side. |
| 22 | +
|
| 23 | + Consider a definition as follows: |
| 24 | +
|
| 25 | + ```lean |
| 26 | + def myand : bool → bool → bool |
| 27 | + | ff _ := ff |
| 28 | + | _ ff := ff |
| 29 | + | _ _ := tt |
| 30 | + ``` |
| 31 | +
|
| 32 | + The equation compiler generates 4 equation lemmas for us: |
| 33 | + ```lean |
| 34 | + myand ff ff = ff |
| 35 | + myand ff tt = ff |
| 36 | + myand tt ff = ff |
| 37 | + myand tt tt = tt |
| 38 | + ``` |
| 39 | +
|
| 40 | + This is not in line with what one might expect looking at the definition. |
| 41 | + Whilst it is provably true, that `∀ x, myand ff x = ff` and `∀ x, myand x ff = ff`, |
| 42 | + we do not get these stronger lemmas from the compiler for free but must in fact |
| 43 | + prove them using `cases` or some other local reasoning. |
| 44 | +
|
| 45 | + In other words, the following does not constitute a proof that lean accepts. |
| 46 | + ```lean |
| 47 | + example : ∀ x, myand ff x = ff := |
| 48 | + begin |
| 49 | + intros, refl |
| 50 | + end |
| 51 | + ``` |
| 52 | +
|
| 53 | + However, you can use `unfold_cases { refl }` to prove `∀ x, myand ff x = ff` and |
| 54 | + `∀ x, myand x ff = ff`. For definitions with many cases, the savings can be very |
| 55 | + significant. |
| 56 | +
|
| 57 | + The term that gets generated for the above definition looks like this: |
| 58 | + ```lean |
| 59 | + λ (a a_1 : bool), |
| 60 | + a.cases_on |
| 61 | + (a_1.cases_on (id_rhs bool ff) (id_rhs bool ff)) |
| 62 | + (a_1.cases_on (id_rhs bool ff) (id_rhs bool tt)) |
| 63 | + ``` |
| 64 | +
|
| 65 | + When the tactic tries to prove the goal `∀ x, myand ff x = ff`, it starts by `intros`, |
| 66 | + followed by unfolding the definition: |
| 67 | + ```lean |
| 68 | + ⊢ ff.cases_on |
| 69 | + (x.cases_on (id_rhs bool ff) (id_rhs bool ff)) |
| 70 | + (x.cases_on (id_rhs bool ff) (id_rhs bool tt)) = ff |
| 71 | + ``` |
| 72 | +
|
| 73 | + At this point, it can make progress using `dsimp`. But then it gets stuck: |
| 74 | + ```lean |
| 75 | + ⊢ bool.rec (id_rhs bool ff) (id_rhs bool ff) x = ff |
| 76 | + ``` |
| 77 | +
|
| 78 | + Next, it can introduce a case split on `x`. At this point, it has to prove two |
| 79 | + goals: |
| 80 | + ```lean |
| 81 | + ⊢ bool.rec (id_rhs bool ff) (id_rhs bool ff) ff = ff |
| 82 | + ⊢ bool.rec (id_rhs bool ff) (id_rhs bool ff) tt = ff |
| 83 | + ``` |
| 84 | +
|
| 85 | + Now, however, both goals can be discharged using `refl`. |
| 86 | +-/ |
| 87 | +namespace tactic |
| 88 | +open expr |
| 89 | +namespace unfold_cases |
| 90 | +/-- |
| 91 | + Given an equation `f x = y`, this tactic tries to infer an expression that can be |
| 92 | + used to do distinction by cases on to make progress. |
| 93 | +
|
| 94 | + Pre-condition: assumes that the outer-most application cannot be beta-reduced |
| 95 | + (e.g. `whnf` or `dsimp`). |
| 96 | +-/ |
| 97 | +meta def find_splitting_expr : expr → tactic expr |
| 98 | +| `(@ite %%cond %%dec_inst _ _ _ = _) := pure `(@decidable.em %%cond %%dec_inst) |
| 99 | +| `(%%(app x y) = _) := pure y |
| 100 | +| e := fail!"expected an expression of the form: f x = y. Got:\n{e}" |
| 101 | + |
| 102 | +/-- |
| 103 | + Tries to finish the current goal using the `inner` tactic. If the tactic |
| 104 | + fails, it tries to find an expression on which to do a distinction by |
| 105 | + cases and calls itself recursively. |
| 106 | +
|
| 107 | + The order of operations is significant. Because the unfolding can potentially |
| 108 | + be infinite, it is important to apply the `inner` tactic at every step. |
| 109 | +
|
| 110 | + Notice, that if the `inner` tactic succeeds, the recursive unfolding is stopped. |
| 111 | +-/ |
| 112 | +meta def unfold_cases_core (inner : interactive.itactic) : tactic unit := |
| 113 | +inner <|> |
| 114 | +(do split_ifs [], all_goals unfold_cases_core, skip) <|> |
| 115 | +do |
| 116 | + tgt ← target, |
| 117 | + e ← find_splitting_expr tgt, |
| 118 | + focus1 $ do |
| 119 | + cases e, |
| 120 | + all_goals $ (dsimp_target >> unfold_cases_core) <|> skip, |
| 121 | + skip |
| 122 | + |
| 123 | +/-- |
| 124 | + Given a target of the form `⊢ f x₁ ... xₙ = y`, unfolds `f` using a delta reduction. |
| 125 | +-/ |
| 126 | +meta def unfold_tgt : expr → tactic unit |
| 127 | +| `(%%l@(app _ _) = %%r) := |
| 128 | + match l.get_app_fn with |
| 129 | + | const n ls := delta_target [n] |
| 130 | + | e := fail!"couldn't unfold:\n{e}" |
| 131 | + end |
| 132 | +| e := fail!"expected an expression of the form: f x = y. Got:\n{e}" |
| 133 | +end unfold_cases |
| 134 | + |
| 135 | +namespace interactive |
| 136 | +open unfold_cases |
| 137 | + |
| 138 | +/-- |
| 139 | + This tactic unfolds the definition of a function or `match` expression. |
| 140 | + Then it recursively introduces a distinction by cases. The decision what expression |
| 141 | + to do the distinction on is driven by the pattern matching expression. |
| 142 | +
|
| 143 | + A typical use case is using `unfold_cases { refl }` to collapse cases that need to be |
| 144 | + considered in a pattern matching. |
| 145 | +
|
| 146 | + ```lean |
| 147 | + have h : foo x = y, by unfold_cases { refl }, |
| 148 | + rw h, |
| 149 | + ``` |
| 150 | +
|
| 151 | + The tactic expects a goal in the form of an equation, possibly universally quantified. |
| 152 | +
|
| 153 | + We can prove a theorem, even if the various case do not directly correspond to the |
| 154 | + function definition. Here is an example application of the tactic: |
| 155 | +
|
| 156 | + ```lean |
| 157 | + def foo : ℕ → ℕ → ℕ |
| 158 | + | 0 0 := 17 |
| 159 | + | (n+2) 17 := 17 |
| 160 | + | 1 0 := 23 |
| 161 | + | 0 (n+18) := 15 |
| 162 | + | 0 17 := 17 |
| 163 | + | 1 17 := 17 |
| 164 | + | _ (n+18) := 27 |
| 165 | + | _ _ := 15 |
| 166 | +
|
| 167 | + example : ∀ x, foo x 17 = 17 := |
| 168 | + begin |
| 169 | + unfold_cases { refl }, |
| 170 | + end |
| 171 | + ``` |
| 172 | +
|
| 173 | + The compiler generates 57 cases for `foo`. However, when we look at the definition, we see |
| 174 | + that whenever the function is applied to `17` in the second argument, it returns `17`. |
| 175 | +
|
| 176 | + Proving this property consists of merely considering all the cases, eliminating invalid ones |
| 177 | + and applying `refl` on the ones which remain. |
| 178 | +
|
| 179 | + Further examples can be found in `test/unfold_cases.lean`. |
| 180 | +-/ |
| 181 | +meta def unfold_cases (inner : itactic) : tactic unit := focus1 $ do |
| 182 | + tactic.intros, |
| 183 | + tgt ← target, |
| 184 | + unfold_tgt tgt, |
| 185 | + try dsimp_target, |
| 186 | + unfold_cases_core inner |
| 187 | + |
| 188 | +add_tactic_doc |
| 189 | +{ name := "unfold_cases", |
| 190 | + category := doc_category.tactic, |
| 191 | + decl_names := [`tactic.interactive.unfold_cases], |
| 192 | + tags := ["induction", "case bashing"] } |
| 193 | + |
| 194 | +end interactive |
| 195 | +end tactic |
0 commit comments