From d0987eb3ac4a3deebba49be616575468bafc5a02 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 May 2015 15:44:22 -0700 Subject: [PATCH] feat(library/tactic): add 'subtvars' tactic --- hott/init/tactic.hlean | 1 + library/init/tactic.lean | 1 + src/emacs/lean-syntax.el | 3 +- src/library/tactic/subst_tactic.cpp | 42 +++++++++++++++++++ tests/lean/hott/substvars1.hlean | 52 ++++++++++++++++++++++++ tests/lean/substvars2.hlean | 14 +++++++ tests/lean/substvars2.hlean.expected.out | 8 ++++ 7 files changed, 120 insertions(+), 1 deletion(-) create mode 100644 tests/lean/hott/substvars1.hlean create mode 100644 tests/lean/substvars2.hlean create mode 100644 tests/lean/substvars2.hlean.expected.out diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 7bc6461d3..d08e41df3 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -116,6 +116,7 @@ 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 diff --git a/library/init/tactic.lean b/library/init/tactic.lean index d8f2e70a4..4bfa43182 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -116,6 +116,7 @@ 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 diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 57bd2f39f..e75dfa2d5 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -139,7 +139,8 @@ "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact" "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp" "unfold" "change" "check_expr" "contradiction" "exfalso" "split" "existsi" "constructor" "left" "right" - "injection" "congruence" "reflexivity" "symmetry" "transitivity" "state" "induction" "induction_using")) + "injection" "congruence" "reflexivity" "symmetry" "transitivity" "state" "induction" "induction_using" + "substvars")) word-end) (1 'font-lock-constant-face)) ;; Types diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp index fa727cada..22d57b86d 100644 --- a/src/library/tactic/subst_tactic.cpp +++ b/src/library/tactic/subst_tactic.cpp @@ -181,6 +181,44 @@ tactic mk_subst_tactic(list const & ids) { return tactic(fn); } +tactic mk_subst_vars_tactic(bool first, unsigned start) { + auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { + goals const & gs = s.get_goals(); + if (empty(gs)) { + if (first) + return proof_state_seq(); + else + return proof_state_seq(s); + } + goal const & g = head(gs); + + auto apply_rewrite = [&](expr const & H, bool symm, unsigned i) { + tactic tac = orelse(then(mk_subst_tactic_core(mlocal_name(H), symm), mk_subst_vars_tactic(false, 0)), + mk_subst_vars_tactic(false, i+1)); + return tac(env, ios, s); + }; + + buffer hyps; + g.get_hyps(hyps); + for (unsigned i = start; i < hyps.size(); i++) { + expr const & h = hyps[i]; + expr lhs, rhs; + if (is_eq(mlocal_type(h), lhs, rhs)) { + if (is_local(rhs)) { + return apply_rewrite(h, true, i); + } else if (is_local(lhs)) { + return apply_rewrite(h, false, i); + } + } + } + if (first) + return proof_state_seq(); + else + return proof_state_seq(s); + }; + return tactic(fn); +} + void initialize_subst_tactic() { register_tac(name{"tactic", "subst"}, [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) { @@ -188,6 +226,10 @@ void initialize_subst_tactic() { get_tactic_id_list_elements(app_arg(e), ns, "invalid 'subst' tactic, list of identifiers expected"); return then(mk_subst_tactic(to_list(ns)), try_tactic(refl_tactic(elab))); }); + register_tac(name{"tactic", "substvars"}, + [](type_checker &, elaborate_fn const & elab, expr const &, pos_info_provider const *) { + return then(mk_subst_vars_tactic(true, 0), try_tactic(refl_tactic(elab))); + }); } void finalize_subst_tactic() { } diff --git a/tests/lean/hott/substvars1.hlean b/tests/lean/hott/substvars1.hlean new file mode 100644 index 000000000..8da6f0e1b --- /dev/null +++ b/tests/lean/hott/substvars1.hlean @@ -0,0 +1,52 @@ +open nat + +example (A B : Type) (a : A) (b : B) (h₁ : A = B) (h₂ : eq.rec_on h₁ a = b) : b = eq.rec_on h₁ a := +begin + substvars +end + +example (A B : Type) (a : A) (b : B) (h₁ : A = B) (h₂ : eq.rec_on h₁ a = b) : b = eq.rec_on h₁ a := +begin + substvars +end + +example (a b c : nat) (a0 : a = 0) (b1 : b = 1 + a) (ab : a = b) : empty := +begin + substvars, + contradiction +end + +example (a : nat) : a = 0 → a = 1 → empty := +begin + intro a0 a1, + substvars, + contradiction +end + +example (a b c : nat) : a = 0 → b = 1 + a → a = b → empty := +begin + intro a0 b1 ab, + substvars, + state, + contradiction +end +example (a b c : nat) : a = 0 → b = 1 + a → a = b → empty := +begin + intro a0 b1 ab, + substvars, + contradiction +end + +example (a b c : nat) : a = 0 → 1 + a = b → a = b → empty := +begin + intro a0 b1 ab, + substvars, + contradiction +end + +example (a b c : nat) : a = 0 → 1 + a = b → a = b → empty := +begin + intros, + substvars, + contradiction +end diff --git a/tests/lean/substvars2.hlean b/tests/lean/substvars2.hlean new file mode 100644 index 000000000..6a4165060 --- /dev/null +++ b/tests/lean/substvars2.hlean @@ -0,0 +1,14 @@ +inductive list (A : Type) := +| nil : list A +| cons : A → list A → list A + +open nat prod + +example (A B : Type) (d c : nat) (h₀ : c = 0) (a : A) (b : list B) (h₁ : A = list B) (h₂ : eq.rec_on h₁ a = @list.nil B) (h₃ : d = c) (h₄ : d + 1 = d + 2) + : b = eq.rec_on h₁ a × c = 1:= +begin + substvars, + state, + injection h₄, + contradiction +end diff --git a/tests/lean/substvars2.hlean.expected.out b/tests/lean/substvars2.hlean.expected.out new file mode 100644 index 000000000..71a65e274 --- /dev/null +++ b/tests/lean/substvars2.hlean.expected.out @@ -0,0 +1,8 @@ +substvars2.hlean:11:2: proof state +A B : Type, +a : A, +b : list B, +h₁ : A = list B, +h₂ : eq.rec_on h₁ a = list.nil B, +h₄ : 0 + 1 = 0 + 2 +⊢ b = eq.rec_on h₁ a × 0 = 1