chore(library): remove old tactic definition
This commit is contained in:
Leonardo de Moura
parent
2eafe66240
commit
0280281b1c
3 changed files with 1 additions and 179 deletions
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.datatypes init.reserved_notation init.tactic init.logic
|
||||
import init.datatypes init.reserved_notation init.logic
|
||||
import init.relation init.wf init.nat init.wf_k init.prod
|
||||
import init.bool init.num init.sigma init.measurable init.setoid init.quot
|
||||
import init.funext init.function init.subtype init.classical init.simplifier
|
||||
|
|
|
|||
|
|
@ -1,161 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Leonardo de Moura
|
||||
|
||||
This is just a trick to embed the 'tactic language' as a Lean
|
||||
expression. We should view 'tactic' as automation that when execute
|
||||
produces a term. tactic.builtin is just a "dummy" for creating the
|
||||
definitions that are actually implemented in C++
|
||||
-/
|
||||
prelude
|
||||
import init.datatypes init.reserved_notation init.num
|
||||
|
||||
inductive tactic :
|
||||
Type := builtin : tactic
|
||||
|
||||
namespace tactic
|
||||
-- Remark the following names are not arbitrary, the tactic module
|
||||
-- uses them when converting Lean expressions into actual tactic objects.
|
||||
-- The bultin 'by' construct triggers the process of converting a
|
||||
-- a term of type 'tactic' into a tactic that sythesizes a term
|
||||
definition and_then (t1 t2 : tactic) : tactic := builtin
|
||||
definition or_else (t1 t2 : tactic) : tactic := builtin
|
||||
definition par (t1 t2 : tactic) : tactic := builtin
|
||||
definition fixpoint (f : tactic → tactic) : tactic := builtin
|
||||
definition repeat (t : tactic) : tactic := builtin
|
||||
definition at_most (t : tactic) (k : num) : tactic := builtin
|
||||
definition discard (t : tactic) (k : num) : tactic := builtin
|
||||
definition focus_at (t : tactic) (i : num) : tactic := builtin
|
||||
definition try_for (t : tactic) (ms : num) : tactic := builtin
|
||||
definition all_goals (t : tactic) : tactic := builtin
|
||||
definition now : tactic := builtin
|
||||
definition assumption : tactic := builtin
|
||||
definition eassumption : tactic := builtin
|
||||
definition state : tactic := builtin
|
||||
definition fail : tactic := builtin
|
||||
definition id : tactic := builtin
|
||||
definition info : tactic := builtin
|
||||
definition contradiction : tactic := builtin
|
||||
definition exfalso : tactic := builtin
|
||||
definition congruence : tactic := builtin
|
||||
definition rotate_left (k : num) := builtin
|
||||
definition rotate_right (k : num) := builtin
|
||||
definition rotate (k : num) := rotate_left k
|
||||
definition norm_num : tactic := builtin
|
||||
|
||||
-- This is just a trick to embed expressions into tactics.
|
||||
-- The nested expressions are "raw". They tactic should
|
||||
-- elaborate them when it is executed.
|
||||
inductive expr : Type :=
|
||||
builtin : expr
|
||||
|
||||
inductive expr_list : Type :=
|
||||
| nil : expr_list
|
||||
| cons : expr → expr_list → expr_list
|
||||
|
||||
-- auxiliary type used to mark optional list of arguments
|
||||
definition opt_expr_list := expr_list
|
||||
|
||||
-- auxiliary types used to mark that the expression is suppose to be an identifier, optional, or a list.
|
||||
definition identifier := expr
|
||||
definition identifier_list := expr_list
|
||||
definition opt_identifier_list := expr_list
|
||||
-- Remark: the parser has special support for tactics containing `location` parameters.
|
||||
-- It will parse the optional `at ...` modifier.
|
||||
definition location := expr
|
||||
-- Marker for instructing the parser to parse it as 'with <expr>'
|
||||
definition with_expr := expr
|
||||
|
||||
-- Marker for instructing the parser to parse it as '?(using <expr>)'
|
||||
definition using_expr := expr
|
||||
-- Constant used to denote the case were no expression was provided
|
||||
definition none_expr : expr := expr.builtin
|
||||
|
||||
definition apply (e : expr) : tactic := builtin
|
||||
definition eapply (e : expr) : tactic := builtin
|
||||
definition fapply (e : expr) : tactic := builtin
|
||||
definition rename (a b : identifier) : tactic := builtin
|
||||
definition intro (e : opt_identifier_list) : tactic := builtin
|
||||
definition generalize_tac (e : expr) (id : identifier) : tactic := builtin
|
||||
definition clear (e : identifier_list) : tactic := builtin
|
||||
definition revert (e : identifier_list) : tactic := builtin
|
||||
definition refine (e : expr) : tactic := builtin
|
||||
definition exact (e : expr) : tactic := builtin
|
||||
-- Relaxed version of exact that does not enforce goal type
|
||||
definition rexact (e : expr) : tactic := builtin
|
||||
definition check_expr (e : expr) : tactic := builtin
|
||||
-- definition trace (s : string) : tactic := builtin
|
||||
|
||||
-- rewrite_tac is just a marker for the builtin 'rewrite' notation
|
||||
-- used to create instances of this tactic.
|
||||
definition rewrite_tac (e : expr_list) : tactic := builtin
|
||||
definition xrewrite_tac (e : expr_list) : tactic := builtin
|
||||
definition krewrite_tac (e : expr_list) : tactic := builtin
|
||||
definition replace (old : expr) (new : with_expr) (loc : location) : tactic := builtin
|
||||
|
||||
-- Arguments:
|
||||
-- - ls : lemmas to be used (if not provided, then blast will choose them)
|
||||
-- - ds : definitions that can be unfolded (if not provided, then blast will choose them)
|
||||
definition blast (ls : opt_identifier_list) (ds : opt_identifier_list) : tactic := builtin
|
||||
|
||||
-- with_options_tac is just a marker for the builtin 'with_options' notation
|
||||
definition with_options_tac (o : expr) (t : tactic) : tactic := builtin
|
||||
-- with_options_tac is just a marker for the builtin 'with_attributes' notation
|
||||
definition with_attributes_tac (o : expr) (n : identifier_list) (t : tactic) : tactic := builtin
|
||||
|
||||
/-
|
||||
definition simp : tactic := #tactic with_options [blast.strategy "simp"] blast
|
||||
definition simp_nohyps : tactic := #tactic with_options [blast.strategy "simp_nohyps"] blast
|
||||
definition simp_topdown : tactic := #tactic with_options [blast.strategy "simp", simplify.top_down true] blast
|
||||
definition inst_simp : tactic := #tactic with_options [blast.strategy "ematch_simp"] blast
|
||||
definition rec_simp : tactic := #tactic with_options [blast.strategy "rec_simp"] blast
|
||||
definition rec_inst_simp : tactic := #tactic with_options [blast.strategy "rec_ematch_simp"] blast
|
||||
definition grind : tactic := #tactic with_options [blast.strategy "grind"] blast
|
||||
definition grind_simp : tactic := #tactic with_options [blast.strategy "grind_simp"] blast
|
||||
-/
|
||||
|
||||
definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin
|
||||
|
||||
definition induction (h : expr) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin
|
||||
|
||||
definition intros (ids : opt_identifier_list) : tactic := builtin
|
||||
|
||||
definition generalizes (es : expr_list) : tactic := builtin
|
||||
|
||||
definition clears (ids : identifier_list) : tactic := builtin
|
||||
|
||||
definition reverts (ids : identifier_list) : tactic := builtin
|
||||
|
||||
definition change (e : expr) : tactic := builtin
|
||||
|
||||
definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin
|
||||
|
||||
definition note_tac (id : identifier) (e : expr) : tactic := builtin
|
||||
|
||||
definition constructor (k : option num) : tactic := builtin
|
||||
definition fconstructor (k : option num) : tactic := builtin
|
||||
definition existsi (e : expr) : tactic := builtin
|
||||
definition split : tactic := builtin
|
||||
definition left : tactic := builtin
|
||||
definition right : tactic := builtin
|
||||
|
||||
definition injection (e : expr) (ids : opt_identifier_list) : tactic := builtin
|
||||
|
||||
definition subst (ids : identifier_list) : tactic := builtin
|
||||
definition substvars : tactic := builtin
|
||||
|
||||
definition reflexivity : tactic := builtin
|
||||
definition symmetry : tactic := builtin
|
||||
definition transitivity (e : expr) : tactic := builtin
|
||||
|
||||
definition try (t : tactic) : tactic := or_else t id
|
||||
definition repeat1 (t : tactic) : tactic := and_then t (repeat t)
|
||||
definition focus (t : tactic) : tactic := focus_at t 0
|
||||
definition determ (t : tactic) : tactic := at_most t 1
|
||||
-- definition trivial : tactic := or_else (or_else (apply eq.refl) (apply true.intro)) assumption
|
||||
end tactic
|
||||
-- tactic_infixl `;`:15 := tactic.and_then
|
||||
-- tactic_notation T1 `:`:15 T2 := tactic.focus (tactic.and_then T1 (tactic.all_goals T2))
|
||||
tactic_notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
|
||||
--tactic_notation `replace` s `with` t := tactic.replace_tac s t
|
||||
|
|
@ -1,17 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
|
||||
-- tools.helper_tactics
|
||||
-- ====================
|
||||
|
||||
-- Useful tactics.
|
||||
|
||||
import logic.eq
|
||||
|
||||
open tactic
|
||||
|
||||
namespace helper_tactics
|
||||
-- definition apply_refl := apply eq.refl
|
||||
-- tactic_hint apply_refl
|
||||
end helper_tactics
|
||||
Loading…
Add table
Reference in a new issue