Skip to content
{{ message }}

Instantly share code, notes, and snippets.

# rwbarton/tactic.lean Secret

Created Jul 30, 2018
 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
to join this conversation on GitHub. Already have an account? Sign in to comment