From 84deddcca96779d1fd26da498bff2d63ae7105b7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 5 May 2015 20:03:00 -0700 Subject: [PATCH] feat(library/tactic/rewrite_tactic): apply 'reflexivity' tactic after 'rewrite' instead of hard coded solution --- library/data/fintype.lean | 2 +- library/data/list/perm.lean | 31 +++++++++---------- library/data/uprod.lean | 4 +-- src/library/tactic/equivalence_tactics.cpp | 9 ++++-- src/library/tactic/equivalence_tactics.h | 1 + src/library/tactic/rewrite_tactic.cpp | 35 ++++------------------ src/library/tactic/tactic.h | 1 + tests/lean/revert_fail.lean.expected.out | 6 +--- tests/lean/rewrite_fail.lean.expected.out | 6 +--- 9 files changed, 33 insertions(+), 62 deletions(-) diff --git a/library/data/fintype.lean b/library/data/fintype.lean index 3b6fbe76e..622570b3b 100644 --- a/library/data/fintype.lean +++ b/library/data/fintype.lean @@ -78,7 +78,7 @@ definition decidable_eq_fun [instance] {A B : Type} [h₁ : fintype A] [h₂ : d match h₁ with | fintype.mk e u c := match find_discr f g e with - | some a := λ h : find_discr f g e = some a, inr (λ f_eq_g : f = g, absurd (by rewrite f_eq_g) (ne_of_find_discr_eq_some h)) + | some a := λ h : find_discr f g e = some a, inr (λ f_eq_g : f = g, absurd (by rewrite f_eq_g; reflexivity) (ne_of_find_discr_eq_some h)) | none := λ h : find_discr f g e = none, inl (show f = g, from funext (λ a : A, all_eq_of_find_discr_eq_none h a (c a))) end rfl end diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 3c2a234eb..6f45c388f 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -104,7 +104,7 @@ theorem perm_cons_app (a : A) : ∀ (l : list A), (a::l) ~ (l ++ [a]) theorem perm_app_comm {l₁ l₂ : list A} : (l₁++l₂) ~ (l₂++l₁) := list.induction_on l₁ - (by rewrite [append_nil_right, append_nil_left]; apply refl) + (by rewrite [append_nil_right, append_nil_left]) (λ a t r, calc a::(t++l₂) ~ a::(l₂++t) : skip a r ... ~ l₂++t++[a] : perm_cons_app @@ -166,7 +166,7 @@ theorem perm_erase [H : decidable_eq A] {a : A} : ∀ {l : list A}, a ∈ l → | [] h := absurd h !not_mem_nil | (x::t) h := by_cases - (assume aeqx : a = x, by rewrite [aeqx, erase_cons_head]; exact !perm.refl) + (assume aeqx : a = x, by rewrite [aeqx, erase_cons_head]) (assume naeqx : a ≠ x, have aint : a ∈ t, from mem_of_ne_of_mem naeqx h, have aux : t ~ a :: erase a t, from perm_erase aint, @@ -185,11 +185,11 @@ assume p, perm.induction_on p by_cases (assume aeqx : a = x, by_cases - (assume aeqy : a = y, by rewrite [-aeqx, -aeqy]; exact !perm.refl) - (assume naeqy : a ≠ y, by rewrite [-aeqx, erase_cons_tail _ naeqy, *erase_cons_head]; exact !perm.refl)) + (assume aeqy : a = y, by rewrite [-aeqx, -aeqy]) + (assume naeqy : a ≠ y, by rewrite [-aeqx, erase_cons_tail _ naeqy, *erase_cons_head])) (assume naeqx : a ≠ x, by_cases - (assume aeqy : a = y, by rewrite [-aeqy, erase_cons_tail _ naeqx, *erase_cons_head]; exact !perm.refl) + (assume aeqy : a = y, by rewrite [-aeqy, erase_cons_tail _ naeqx, *erase_cons_head]) (assume naeqy : a ≠ y, by rewrite[erase_cons_tail _ naeqx, *erase_cons_tail _ naeqy, erase_cons_tail _ naeqx]; exact !swap))) (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂, trans r₁ r₂) @@ -595,19 +595,19 @@ include H theorem perm_union_left {l₁ l₂ : list A} (t₁ : list A) : l₁ ~ l₂ → (union l₁ t₁) ~ (union l₂ t₁) := assume p, perm.induction_on p - (by rewrite [nil_union]; exact !refl) + (by rewrite [nil_union]) (λ x l₁ l₂ p₁ r₁, by_cases (λ xint₁ : x ∈ t₁, by rewrite [*union_cons_of_mem _ xint₁]; exact r₁) (λ nxint₁ : x ∉ t₁, by rewrite [*union_cons_of_not_mem _ nxint₁]; exact (skip _ r₁))) (λ x y l, by_cases (λ yint : y ∈ t₁, by_cases (λ xint : x ∈ t₁, - by rewrite [*union_cons_of_mem _ xint, *union_cons_of_mem _ yint, *union_cons_of_mem _ xint]; exact !refl) + by rewrite [*union_cons_of_mem _ xint, *union_cons_of_mem _ yint, *union_cons_of_mem _ xint]) (λ nxint : x ∉ t₁, - by rewrite [*union_cons_of_mem _ yint, *union_cons_of_not_mem _ nxint, union_cons_of_mem _ yint]; exact !refl)) + by rewrite [*union_cons_of_mem _ yint, *union_cons_of_not_mem _ nxint, union_cons_of_mem _ yint])) (λ nyint : y ∉ t₁, by_cases (λ xint : x ∈ t₁, - by rewrite [*union_cons_of_mem _ xint, *union_cons_of_not_mem _ nyint, union_cons_of_mem _ xint]; exact !refl) + by rewrite [*union_cons_of_mem _ xint, *union_cons_of_not_mem _ nyint, union_cons_of_mem _ xint]) (λ nxint : x ∉ t₁, by rewrite [*union_cons_of_not_mem _ nxint, *union_cons_of_not_mem _ nyint, union_cons_of_not_mem _ nxint]; exact !swap))) (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂, trans r₁ r₂) @@ -657,21 +657,18 @@ assume p, perm.induction_on p by rewrite [*inter_cons_of_mem _ xint, *inter_cons_of_mem _ yint, *inter_cons_of_mem _ xint]; exact !swap) (λ nxint : x ∉ t₁, - by rewrite [*inter_cons_of_mem _ yint, *inter_cons_of_not_mem _ nxint, inter_cons_of_mem _ yint]; - exact !refl)) + by rewrite [*inter_cons_of_mem _ yint, *inter_cons_of_not_mem _ nxint, inter_cons_of_mem _ yint])) (λ nyint : y ∉ t₁, by_cases (λ xint : x ∈ t₁, - by rewrite [*inter_cons_of_mem _ xint, *inter_cons_of_not_mem _ nyint, inter_cons_of_mem _ xint]; - exact !refl) + by rewrite [*inter_cons_of_mem _ xint, *inter_cons_of_not_mem _ nyint, inter_cons_of_mem _ xint]) (λ nxint : x ∉ t₁, by rewrite [*inter_cons_of_not_mem _ nxint, *inter_cons_of_not_mem _ nyint, - inter_cons_of_not_mem _ nxint]; - exact !refl))) + inter_cons_of_not_mem _ nxint]))) (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂, trans r₁ r₂) theorem perm_inter_right (l : list A) {t₁ t₂ : list A} : t₁ ~ t₂ → (inter l t₁) ~ (inter l t₂) := list.induction_on l - (λ p, by rewrite [*inter_nil]; exact !refl) + (λ p, by rewrite [*inter_nil]) (λ x xs r p, by_cases (λ xint₁ : x ∈ t₁, assert xint₂ : x ∈ t₂, from mem_perm p xint₁, @@ -748,7 +745,7 @@ assume p : l₁ ~ l₂, perm.induction_on p theorem perm_cross_product_right (l : list A) {t₁ t₂ : list B} : t₁ ~ t₂ → (cross_product l t₁) ~ (cross_product l t₂) := list.induction_on l - (λ p, by rewrite [*nil_cross_product]; exact !perm.refl) + (λ p, by rewrite [*nil_cross_product]) (λ a t r p, perm_app (perm_map _ p) (r p)) diff --git a/library/data/uprod.lean b/library/data/uprod.lean index 1bf8c012f..ee46b9f7c 100644 --- a/library/data/uprod.lean +++ b/library/data/uprod.lean @@ -20,13 +20,13 @@ take p, or.inl rfl private theorem eqv.symm [symm] {A : Type} : ∀ p₁ p₂ : A × A, p₁ ~ p₂ → p₂ ~ p₁ := take p₁ p₂ h, or.elim h - (λ e, by rewrite e; reflexivity) + (λ e, by rewrite e) (λ e, begin esimp [eqv], rewrite [-e, swap_swap], right, reflexivity end) private theorem eqv.trans [trans] {A : Type} : ∀ p₁ p₂ p₃ : A × A, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃ := take p₁ p₂ p₃ h₁ h₂, or.elim h₁ (λ e₁₂, or.elim h₂ - (λ e₂₃, by rewrite [e₁₂, e₂₃]; reflexivity) + (λ e₂₃, by rewrite [e₁₂, e₂₃]) (λ es₂₃, begin esimp [eqv], rewrite -es₂₃, right, congruence, assumption end)) (λ es₁₂, or.elim h₂ (λ e₂₃, begin esimp [eqv], rewrite es₁₂, right, assumption end) diff --git a/src/library/tactic/equivalence_tactics.cpp b/src/library/tactic/equivalence_tactics.cpp index 0b899c06d..26ceaf5e0 100644 --- a/src/library/tactic/equivalence_tactics.cpp +++ b/src/library/tactic/equivalence_tactics.cpp @@ -11,13 +11,16 @@ Author: Leonardo de Moura #include "library/tactic/expr_to_tactic.h" namespace lean { -static optional get_goal_op(proof_state const & s) { +// Remark: if no_meta == true, then return none if goal contains metavariables +static optional get_goal_op(proof_state const & s, bool no_meta = false) { goals const & gs = s.get_goals(); if (empty(gs)) { throw_no_goal_if_enabled(s); return optional(); } goal const & g = head(gs); + if (no_meta && has_metavar(g.get_type())) + return optional(); expr const & op = get_app_fn(g.get_type()); if (is_constant(op)) return optional(const_name(op)); @@ -25,9 +28,9 @@ static optional get_goal_op(proof_state const & s) { return optional(); } -tactic refl_tactic(elaborate_fn const & elab) { +tactic refl_tactic(elaborate_fn const & elab, bool no_meta = false) { auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { - auto op = get_goal_op(s); + auto op = get_goal_op(s, no_meta); if (!op) return proof_state_seq(); if (auto refl = get_refl_info(env, *op)) { diff --git a/src/library/tactic/equivalence_tactics.h b/src/library/tactic/equivalence_tactics.h index bec7c3dc9..a15f394fb 100644 --- a/src/library/tactic/equivalence_tactics.h +++ b/src/library/tactic/equivalence_tactics.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once namespace lean { +tactic refl_tactic(elaborate_fn const & elab, bool no_meta = false); void initialize_equivalence_tactics(); void finalize_equivalence_tactics(); } diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index b9867fe64..1c0891f74 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -35,6 +35,7 @@ Author: Leonardo de Moura #include "library/tactic/rewrite_tactic.h" #include "library/tactic/expr_to_tactic.h" #include "library/tactic/class_instance_synth.h" +#include "library/tactic/equivalence_tactics.h" // #define TRACE_MATCH_PLUGIN @@ -1385,27 +1386,6 @@ class rewrite_fn { } } - bool check_trivial_goal() { - expr type = m_g.get_type(); - if (is_eq(type) || (is_iff(type) && m_env.impredicative())) { - constraint_seq cs; - expr lhs = app_arg(app_fn(type)); - expr rhs = app_arg(type); - if (m_unifier_tc->is_def_eq(lhs, rhs, justification(), cs) && !cs) { - expr H = is_eq(type) ? mk_refl(*m_tc, lhs) : mk_iff_refl(lhs); - assign(m_subst, m_g, H); - return true; - } else { - return false; - } - } else if (type == mk_true()) { - assign(m_subst, m_g, mk_constant(get_eq_intro_name())); - return true; - } else { - return false; - } - } - class match_converter : public unfold_reducible_converter { public: match_converter(environment const & env, bool relax_main_opaque): @@ -1501,11 +1481,7 @@ public: } } - goals new_gs; - if (check_trivial_goal()) - new_gs = tail(m_ps.get_goals()); - else - new_gs = cons(m_g, tail(m_ps.get_goals())); + goals new_gs = cons(m_g, tail(m_ps.get_goals())); proof_state new_ps(m_ps, new_gs, m_subst, m_ngen); return proof_state_seq(new_ps); } @@ -1663,13 +1639,14 @@ void initialize_rewrite_tactic() { !is_rewrite_reduce_step(arg) && !is_rewrite_fold_step(arg)) throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, invalid argument"); } - return mk_rewrite_tactic(elab, args); + bool fail_if_metavars = true; + return then(mk_rewrite_tactic(elab, args), try_tactic(refl_tactic(elab, fail_if_metavars))); }); register_tac(name{"tactic", "subst"}, - [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { + [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) { buffer ns; get_tactic_id_list_elements(app_arg(e), ns, "invalid 'subst' tactic, list of identifiers expected"); - return mk_subst_tactic(to_list(ns)); + return then(mk_subst_tactic(to_list(ns)), try_tactic(refl_tactic(elab))); }); } diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 685fa539f..72d626d68 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -62,6 +62,7 @@ inline tactic operator<<(tactic const & t1, tactic const & t2) { return then(t1, /** \brief Return a tactic that applies \c t1, and if \c t1 returns the empty sequence of states, then applies \c t2. */ tactic orelse(tactic const & t1, tactic const & t2); inline tactic operator||(tactic const & t1, tactic const & t2) { return orelse(t1, t2); } +inline tactic try_tactic(tactic const & t) { return orelse(t, id_tactic()); } /** \brief Return a tactic that appies \c t, but using the additional set of options \c opts. */ tactic using_params(tactic const & t, options const & opts); /** diff --git a/tests/lean/revert_fail.lean.expected.out b/tests/lean/revert_fail.lean.expected.out index 6ac2c7c0d..a27c50060 100644 --- a/tests/lean/revert_fail.lean.expected.out +++ b/tests/lean/revert_fail.lean.expected.out @@ -13,12 +13,8 @@ revert_fail.lean:6:0: error: failed to add declaration '14.0' to environment, va remark: set 'formatter.hide_full_terms' to false to see the complete term λ (A : Type) (n : nat) (v : …), ?M_1 -revert_fail.lean:11:2: error:invalid tactic, there are no goals to be solved -proof state: +revert_fail.lean:11:2: error: tactic failed no goals -revert_fail.lean:12:0: error: don't know how to synthesize placeholder -n : nat -⊢ n = n revert_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables remark: set 'formatter.hide_full_terms' to false to see the complete term λ (n : nat), diff --git a/tests/lean/rewrite_fail.lean.expected.out b/tests/lean/rewrite_fail.lean.expected.out index 2ecd71ab4..0ffde0242 100644 --- a/tests/lean/rewrite_fail.lean.expected.out +++ b/tests/lean/rewrite_fail.lean.expected.out @@ -15,12 +15,8 @@ rewrite_fail.lean:6:0: error: failed to add declaration '14.0' to environment, v remark: set 'formatter.hide_full_terms' to false to see the complete term λ (a b : ℕ) (Ha : …) (Hb : …), ?M_1 -rewrite_fail.lean:11:2: error:invalid tactic, there are no goals to be solved -proof state: +rewrite_fail.lean:11:2: error: tactic failed no goals -rewrite_fail.lean:12:0: error: don't know how to synthesize placeholder -a : ℕ -⊢ a = a rewrite_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables remark: set 'formatter.hide_full_terms' to false to see the complete term λ (a : ℕ),