-
Notifications
You must be signed in to change notification settings - Fork 307
/
SimpRw.lean
72 lines (64 loc) · 2.84 KB
/
SimpRw.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
/-
Copyright (c) 2020 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anne Baanen, Mario Carneiro, Alex J. Best
-/
import Lean
namespace Mathlib.Tactic
open Lean Parser.Tactic Elab.Tactic
/-- A version of `withRWRulesSeq` (in core) that doesn't attempt to find equation lemmas, and simply
passes the rw rules on to `x`. -/
def withSimpRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax)
(x : (symm : Bool) → (term : Syntax) → TacticM Unit) : TacticM Unit := do
let lbrak := rwRulesSeqStx[0]
let rules := rwRulesSeqStx[1].getArgs
-- show initial state up to (incl.) `[`
withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ())
let numRules := (rules.size + 1) / 2
for i in [:numRules] do
let rule := rules[i * 2]!
let sep := rules.getD (i * 2 + 1) Syntax.missing
-- show rule state up to (incl.) next `,`
withTacticInfoContext (mkNullNode #[rule, sep]) do
-- show errors on rule
withRef rule do
let symm := !rule[0].isNone
let term := rule[1]
-- let processId (id : Syntax) : TacticM Unit := do
x symm term
/--
`simp_rw` functions as a mix of `simp` and `rw`. Like `rw`, it applies each
rewrite rule in the given order, but like `simp` it repeatedly applies these
rules and also under binders like `∀ x, ...`, `∃ x, ...` and `fun x ↦...`.
Usage:
- `simp_rw [lemma_1, ..., lemma_n]` will rewrite the goal by applying the
lemmas in that order. A lemma preceded by `←` is applied in the reverse direction.
- `simp_rw [lemma_1, ..., lemma_n] at h₁ ... hₙ` will rewrite the given hypotheses.
- `simp_rw [...] at *` rewrites in the whole context: all hypotheses and the goal.
Lemmas passed to `simp_rw` must be expressions that are valid arguments to `simp`.
For example, neither `simp` nor `rw` can solve the following, but `simp_rw` can:
```lean
example {a : ℕ}
(h1 : ∀ a b : ℕ, a - 1 ≤ b ↔ a ≤ b + 1)
(h2 : ∀ a b : ℕ, a ≤ b ↔ ∀ c, c < a → c < b) :
(∀ b, a - 1 ≤ b) = ∀ b c : ℕ, c < a → c < b + 1 :=
by simp_rw [h1, h2]
```
-/
elab s:"simp_rw " cfg:(config)? rws:rwRuleSeq g:(location)? : tactic => do
let cfg' : TSyntax `Lean.Parser.Tactic.config ← do
match cfg with
| Option.none =>
`(config| (config := ({ failIfUnchanged := false } : Lean.Meta.Simp.Config)))
| Option.some c => match c with
| `(config| (config := $cfg)) =>
`(config| (config := ({ ($cfg : Lean.Meta.Simp.Config) with failIfUnchanged := false })))
| _ => throwError "malformed cfg"
evalTactic (← `(tactic| simp%$s $cfg' only $g ?))
withSimpRWRulesSeq s rws fun symm term => do
evalTactic (← match term with
| `(term| $e:term) =>
if symm then
`(tactic| simp%$e $[$cfg]? only [← $e:term] $g ?)
else
`(tactic| simp%$e $[$cfg]? only [$e:term] $g ?))