This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 299
/
tactic.lean
123 lines (99 loc) · 4.09 KB
/
tactic.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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
/-
Copyright (c) 2020 Reid Barton. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Reid Barton
-/
import tactic.auto_cases
import tactic.tidy
import tactic.with_local_reducibility
import tactic.show_term
import topology.basic
/-!
# Tactics for topology
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
Currently we have one domain-specific tactic for topology: `continuity`.
-/
/-!
### `continuity` tactic
Automatically solve goals of the form `continuous f`.
Mark lemmas with `@[continuity]` to add them to the set of lemmas
used by `continuity`.
-/
/-- User attribute used to mark tactics used by `continuity`. -/
@[user_attribute]
meta def continuity : user_attribute :=
{ name := `continuity,
descr := "lemmas usable to prove continuity" }
-- Mark some continuity lemmas already defined in `topology.basic`
attribute [continuity]
continuous_id
continuous_const
-- As we will be using `apply_rules` with `md := semireducible`,
-- we need another version of `continuous_id`.
@[continuity] lemma continuous_id' {α : Type*} [topological_space α] : continuous (λ a : α, a) :=
continuous_id
namespace tactic
/--
Tactic to apply `continuous.comp` when appropriate.
Applying `continuous.comp` is not always a good idea, so we have some
extra logic here to try to avoid bad cases.
* If the function we're trying to prove continuous is actually
constant, and that constant is a function application `f z`, then
continuous.comp would produce new goals `continuous f`, `continuous
(λ _, z)`, which is silly. We avoid this by failing if we could
apply continuous_const.
* continuous.comp will always succeed on `continuous (λ x, f x)` and
produce new goals `continuous (λ x, x)`, `continuous f`. We detect
this by failing if a new goal can be closed by applying
continuous_id.
-/
meta def apply_continuous.comp : tactic unit :=
`[fail_if_success { exact continuous_const };
refine continuous.comp _ _;
fail_if_success { exact continuous_id }]
/-- List of tactics used by `continuity` internally. -/
meta def continuity_tactics (md : transparency := reducible) : list (tactic string) :=
[
intros1 >>= λ ns, pure ("intros " ++ (" ".intercalate (ns.map (λ e, e.to_string)))),
apply_rules [] [``continuity] 50 { md := md }
>> pure "apply_rules with continuity",
apply_continuous.comp >> pure "refine continuous.comp _ _"
]
namespace interactive
setup_tactic_parser
/--
Solve goals of the form `continuous f`. `continuity?` reports back the proof term it found.
-/
meta def continuity
(bang : parse $ optional (tk "!")) (trace : parse $ optional (tk "?")) (cfg : tidy.cfg := {}) :
tactic unit :=
let md := if bang.is_some then semireducible else reducible,
continuity_core := tactic.tidy { tactics := continuity_tactics md, ..cfg },
trace_fn := if trace.is_some then show_term else id in
trace_fn continuity_core
/-- Version of `continuity` for use with auto_param. -/
meta def continuity' : tactic unit := continuity none none {}
/--
`continuity` solves goals of the form `continuous f` by applying lemmas tagged with the
`continuity` user attribute.
```
example {X Y : Type*} [topological_space X] [topological_space Y]
(f₁ f₂ : X → Y) (hf₁ : continuous f₁) (hf₂ : continuous f₂)
(g : Y → ℝ) (hg : continuous g) : continuous (λ x, (max (g (f₁ x)) (g (f₂ x))) + 1) :=
by continuity
```
will discharge the goal, generating a proof term like
`((continuous.comp hg hf₁).max (continuous.comp hg hf₂)).add continuous_const`
You can also use `continuity!`, which applies lemmas with `{ md := semireducible }`.
The default behaviour is more conservative, and only unfolds `reducible` definitions
when attempting to match lemmas with the goal.
`continuity?` reports back the proof term it found.
-/
add_tactic_doc
{ name := "continuity / continuity'",
category := doc_category.tactic,
decl_names := [`tactic.interactive.continuity, `tactic.interactive.continuity'],
tags := ["lemma application"] }
end interactive
end tactic