From 0280281b1cf66df92f815db27eafb766224ec2ba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Jun 2016 14:09:39 -0700 Subject: [PATCH] chore(library): remove old tactic definition --- library/init/default.lean | 2 +- library/init/tactic.lean | 161 ------------------------------ library/tools/helper_tactics.lean | 17 ---- 3 files changed, 1 insertion(+), 179 deletions(-) delete mode 100644 library/init/tactic.lean delete mode 100644 library/tools/helper_tactics.lean diff --git a/library/init/default.lean b/library/init/default.lean index 40eb76d762..17c8c61d58 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -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 diff --git a/library/init/tactic.lean b/library/init/tactic.lean deleted file mode 100644 index fa367f2058..0000000000 --- a/library/init/tactic.lean +++ /dev/null @@ -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 ' -definition with_expr := expr - --- Marker for instructing the parser to parse it as '?(using )' -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 diff --git a/library/tools/helper_tactics.lean b/library/tools/helper_tactics.lean deleted file mode 100644 index 079497a20f..0000000000 --- a/library/tools/helper_tactics.lean +++ /dev/null @@ -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