Skip to content

Instantly share code, notes, and snippets.

@rwbarton

rwbarton/tactic.lean Secret

Created Jul 30, 2018
Embed
What would you like to do?
import analysis.topology.topological_structures
import tidy.tidy
attribute [applicable]
continuous_id
continuous_subtype_val
continuous_fst continuous_snd
continuous_inl continuous_inr continuous_sum_rec
continuous_top continuous_bot
-- 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 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.
@[tidy] meta def apply_continuous.comp :=
`[fail_if_success { exact continuous_const };
refine continuous.comp _ _;
fail_if_success { exact continuous_id }]
-- `apply` is often not smart enough to guess how many auxiliary goals
-- to add when that number is not 1. We add tidy tactics with the
-- correct number of goals specified explicitly.
@[tidy] meta def apply_continuous_subtype_mk := `[refine continuous_subtype_mk _ _]
@[tidy] meta def apply_continuous.prod_mk := `[refine continuous.prod_mk _ _]
@[tidy] meta def apply_continuous_min := `[refine continuous_min _ _]
@[tidy] meta def apply_continuous_max := `[refine continuous_max _ _]
@[tidy] meta def apply_continuous_neg' := `[exact continuous_neg']
@[tidy] meta def apply_continuous_add := `[refine continuous_add _ _]
@[tidy] meta def apply_continuous_sub := `[refine continuous_sub _ _]
@[tidy] meta def apply_continuous_mul := `[refine continuous_mul _ _]
@[tidy] meta def apply_continuous_const := `[exact continuous_const]
open tactic
meta def continuity_tactics : list (tactic string) :=
[
applicable >>= λ n, pure ("apply " ++ n.to_string),
automatic_induction,
tactic.interactive.apply_assumption >> pure "apply_assumption",
run_tidy_tactics
]
meta def continuity (cfg : tidy_cfg := {}) : tactic unit :=
let tactics := continuity_tactics ++ cfg.extra_tactics in
do
results ← chain tactics cfg.to_chain_cfg,
try tactic.interactive.resetI,
when cfg.trace_result $
interaction_monad.trace ("---\n" ++ (",\n".intercalate results) ++ "\n---")
-- For use with auto_param
meta def continuity' : tactic unit := continuity
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment