From b790ca980647e708d56abe7f59a24f21e7ad4802 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Apr 2015 12:16:37 -0700 Subject: [PATCH] fix(library/tactic/rewrite_tactic): type check rewriting steps closes #550 --- hott/cubical/square.hlean | 13 ++++-- src/library/tactic/rewrite_tactic.cpp | 59 +++++++++++++++++++-------- tests/lean/550.lean | 45 ++++++++++++++++++++ tests/lean/550.lean.expected.out | 32 +++++++++++++++ 4 files changed, 128 insertions(+), 21 deletions(-) create mode 100644 tests/lean/550.lean create mode 100644 tests/lean/550.lean.expected.out diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean index 8c18f3e01..d43a5e898 100644 --- a/hott/cubical/square.hlean +++ b/hott/cubical/square.hlean @@ -103,15 +103,20 @@ namespace cubical from eq.rec_on p (by cases r; cases t; exact H), left_inv (to_fun !square_equiv_eq) s ▹ !con_inv_cancel_right ▹ H2 - definition rec_on_t {a₁₀ : A} - {P : Π {a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂}, square idp b l r → Type} + definition rec_on_t.{l} {A : Type.{l}} {a₁₀ : A} + {P : Π {a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂}, square idp b l r → Type.{l}} {a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂} (s : square idp b l r) (H : P ids) : P s := let p : l ⬝ b = r := (eq_of_square s)⁻¹ ⬝ !idp_con in assert H2 : P (square_of_eq ((p ⬝ !idp_con⁻¹)⁻¹)), from eq.rec_on p (by cases b; cases l; exact H), - by rewrite [con_inv_cancel_right at H2, inv_inv at H2]; - exact (left_inv (to_fun !square_equiv_eq) s ▹ H2) + assert H3 : P (square_of_eq ((eq_of_square s)⁻¹⁻¹)), + from eq.rec_on !con_inv_cancel_right H2, + assert H4 : P (square_of_eq (eq_of_square s)), + from eq.rec_on !inv_inv H3, + proof + left_inv (to_fun !square_equiv_eq) s ▹ H4 + qed definition rec_on_tb {a : A} {P : Π{b : A} {l : a = b} {r : a = b}, square idp idp l r → Type} diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index a938bc9b0..1a6883f2d 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "kernel/error_msgs.h" #include "kernel/abstract.h" #include "kernel/replace_fn.h" +#include "kernel/kernel_exception.h" #include "kernel/for_each_fn.h" #include "kernel/default_converter.h" #include "kernel/inductive/inductive.h" @@ -1169,6 +1170,10 @@ class rewrite_fn { } } + void check_term(expr const & H) { + type_checker(m_env).check_ignore_undefined_universes(H); + } + bool process_rewrite_hypothesis(expr const & hyp, expr const & orig_elem, expr const & pattern, occurrence const & occ) { add_target(hyp, true); expr Pa = mlocal_type(hyp); @@ -1214,7 +1219,9 @@ class rewrite_fn { expr new_mvar = mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)); expr new_meta = mk_app(new_mvar, new_hyps); goal new_g(new_meta, new_type); - assign(m_subst, m_g, mk_app(new_mvar, args)); + expr V = mk_app(new_mvar, args); + check_term(V); + assign(m_subst, m_g, V); update_goal(new_g); return true; } @@ -1247,7 +1254,7 @@ class rewrite_fn { } else { H = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, b, mk_lambda("x", A, Px), M, a, Heq}); } - + check_term(H); goal new_g(M, Pb); assign(m_subst, m_g, H); update_goal(new_g); @@ -1404,6 +1411,33 @@ class rewrite_fn { } } + void process_failure(expr const & elem, bool type_error) { + if (m_ps.report_failure()) { + proof_state curr_ps(m_ps, cons(m_g, tail(m_ps.get_goals())), m_subst, m_ngen); + if (!m_use_trace || !m_trace_initialized) { + throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps, + [=](formatter const &) { + if (type_error) + return format("invalid 'rewrite' tactic, rewrite step produced type incorrect term"); + else + return format("invalid 'rewrite' tactic, rewrite step failed"); + }); + } else { + trace saved_trace = m_trace; + throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps, + [=](formatter const & fmt) { + format r; + if (type_error) + r += format("invalid 'rewrite' tactic, step produced type incorrect term, details: "); + else + r += format("invalid 'rewrite' tactic, "); + r += saved_trace.pp(fmt); + return r; + }); + } + } + } + public: rewrite_fn(environment const & env, io_state const & ios, elaborate_fn const & elab, proof_state const & ps): m_env(env), m_ios(ios), m_elab(elab), m_ps(ps), m_ngen(ps.get_ngen()), @@ -1423,22 +1457,13 @@ public: proof_state_seq operator()(buffer const & elems) { for (expr const & elem : elems) { flet set1(m_expr_loc, elem); - if (!process_step(elem)) { - if (m_ps.report_failure()) { - proof_state curr_ps(m_ps, cons(m_g, tail(m_ps.get_goals())), m_subst, m_ngen); - if (!m_use_trace || !m_trace_initialized) { - throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps, - [](formatter const &) { return format("invalid 'rewrite' tactic, rewrite step failed"); }); - } else { - trace saved_trace = m_trace; - throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps, - [=](formatter const & fmt) { - format r = format("invalid 'rewrite' tactic, "); - r += saved_trace.pp(fmt); - return r; - }); - } + try { + if (!process_step(elem)) { + process_failure(elem, false); + return proof_state_seq(); } + } catch (kernel_exception &) { + process_failure(elem, true); return proof_state_seq(); } } diff --git a/tests/lean/550.lean b/tests/lean/550.lean new file mode 100644 index 000000000..23db6e7da --- /dev/null +++ b/tests/lean/550.lean @@ -0,0 +1,45 @@ +import algebra.function +import logic.funext + +open function + +structure bijection (A : Type) := +(func finv : A → A) +(linv : finv ∘ func = id) +(rinv : func ∘ finv = id) + +attribute bijection.func [coercion] + +namespace bijection + variable {A : Type} + + definition compose (f g : bijection A) : bijection A := + bijection.mk + (f ∘ g) + (finv g ∘ finv f) + (by rewrite [compose.assoc, -{finv f ∘ _}compose.assoc, linv f, compose.left_id, linv g]) + (by rewrite [-compose.assoc, {_ ∘ finv g}compose.assoc, rinv g, compose.right_id, rinv f]) + + infixr `∘b`:100 := compose + + lemma compose.assoc (f g h : bijection A) : (f ∘b g) ∘b h = f ∘b (g ∘b h) := rfl + + definition id : bijection A := + bijection.mk id id (compose.left_id id) (compose.left_id id) + + lemma id.left_id (f : bijection A) : id ∘b f = f := + bijection.rec_on f (λx x x x, rfl) + + lemma id.right_id (f : bijection A) : f ∘b id = f := + bijection.rec_on f (λx x x x, rfl) + + definition inv (f : bijection A) : bijection A := + bijection.mk + (finv f) + (func f) + (rinv f) + (linv f) + + lemma inv.linv (f : bijection A) : inv f ∘b f = id := + bijection.rec_on f (λfunc finv linv rinv, by rewrite [↑inv, ↑compose, linv]) +end bijection diff --git a/tests/lean/550.lean.expected.out b/tests/lean/550.lean.expected.out new file mode 100644 index 000000000..ab3b4e8c5 --- /dev/null +++ b/tests/lean/550.lean.expected.out @@ -0,0 +1,32 @@ +550.lean:44:72: error:invalid 'rewrite' tactic, step produced type incorrect term, details: rewrite step failed using pattern + finv ∘ func +proof state: +A : Type, +f : bijection A, +func finv : A → A, +linv : finv ∘ func = function.id, +rinv : func ∘ finv = function.id +⊢ mk (finv ∘ func) (finv ∘ func) + (eq.rec + (eq.rec + (eq.rec (eq.rec (eq.rec (eq.refl function.id) (eq.symm linv)) (eq.symm (compose.left_id func))) + (eq.symm rinv)) + (function.compose.assoc func finv func)) + (eq.symm (function.compose.assoc finv func (finv ∘ func)))) + (eq.rec + (eq.rec + (eq.rec (eq.rec (eq.rec (eq.refl function.id) (eq.symm linv)) (eq.symm (compose.right_id finv))) + (eq.symm rinv)) + (eq.symm (function.compose.assoc finv func finv))) + (function.compose.assoc (finv ∘ func) finv func)) = id +550.lean:44:47: error: don't know how to synthesize placeholder +A : Type, +f : bijection A, +func finv : A → A, +linv : finv ∘ func = function.id, +rinv : func ∘ finv = function.id +⊢ inv (mk func finv linv rinv) ∘b mk func finv linv rinv = id +550.lean:44:2: error: failed to add declaration 'bijection.inv.linv' to environment, value has metavariables +remark: set 'formatter.hide_full_terms' to false to see the complete term + λ (A : Type) (f : …), + bijection.rec_on f (λ (func finv : …) (linv : …) (rinv : …), ?M_1)