From 5cbdd77ad039e3ab1ff06dafca4b94589d3aabe3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Feb 2015 12:40:55 -0800 Subject: [PATCH] feat(library/tactic/rewrite_tactic): improve matcher in rewrite_tactic closes #433 --- src/library/tactic/rewrite_tactic.cpp | 19 ++-- tests/lean/hott/433.hlean | 122 ++++++++++++++++++++++++++ 2 files changed, 135 insertions(+), 6 deletions(-) create mode 100644 tests/lean/hott/433.hlean diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 561ce1788..5be59c35a 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include "util/interrupt.h" #include "util/list_fn.h" +#include "util/rb_map.h" #include "util/sexpr/option_declarations.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" @@ -19,6 +20,7 @@ Author: Leonardo de Moura #include "library/kernel_serializer.h" #include "library/reducible.h" #include "library/util.h" +#include "library/expr_lt.h" #include "library/match.h" #include "library/projection.h" #include "library/local_context.h" @@ -730,7 +732,7 @@ class rewrite_fn { expr to_meta_idx(expr const & e) { m_lsubst.clear(); m_esubst.clear(); - name_map emap; + rb_map emap; name_map lmap; auto to_meta_idx = [&](level const & l) { @@ -753,22 +755,27 @@ class rewrite_fn { }); }; + // return true if the arguments of e are not metavar applications + auto no_meta_args = [&](expr const & e) { + buffer args; + get_app_args(e, args); + return !std::any_of(args.begin(), args.end(), [&](expr const & e) { return is_meta(e); }); + }; + return replace(e, [&](expr const & e, unsigned) { if (!has_metavar(e)) { return some_expr(e); // done } else if (is_binding(e)) { throw_rewrite_exception("invalid rewrite tactic, pattern contains binders"); } else if (is_meta(e)) { - expr const & fn = get_app_fn(e); - lean_assert(is_metavar(fn)); - name const & n = mlocal_name(fn); - if (auto it = emap.find(n)) { + if (auto it = emap.find(e)) { return some_expr(*it); } else { unsigned next_idx = m_esubst.size(); expr r = mk_idx_meta(next_idx, m_tc->infer(e).first); m_esubst.push_back(none_expr()); - emap.insert(n, r); + if (no_meta_args(e)) + emap.insert(e, r); // cache only if arguments of e are not metavariables return some_expr(r); } } else if (is_constant(e)) { diff --git a/tests/lean/hott/433.hlean b/tests/lean/hott/433.hlean new file mode 100644 index 000000000..78a3eaa55 --- /dev/null +++ b/tests/lean/hott/433.hlean @@ -0,0 +1,122 @@ +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Floris van Doorn +Ported from Coq HoTT + +Theorems about pi-types (dependent function spaces) +-/ +import types.sigma + +open eq equiv is_equiv funext + +namespace pi + universe variables l k + variables {A A' : Type.{l}} {B : A → Type.{k}} {B' : A' → Type.{k}} {C : Πa, B a → Type} + {D : Πa b, C a b → Type} + {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {f g : Πa, B a} + + /- Paths -/ + + /- Paths [p : f ≈ g] in a function type [Πx:X, P x] are equivalent to functions taking values in path types, [H : Πx:X, f x ≈ g x], or concisely, [H : f ∼ g]. + + This equivalence, however, is just the combination of [apD10] and function extensionality [funext], and as such, [path_forall], et seq. are given in axioms.funext and path: -/ + + /- Now we show how these things compute. -/ + + definition apD10_path_pi [H : funext] (h : f ∼ g) : apD10 (path_pi h) ∼ h := + apD10 (retr apD10 h) + + definition path_pi_eta [H : funext] (p : f = g) : path_pi (apD10 p) = p := + sect apD10 p + + definition path_pi_idp [H : funext] : path_pi (λx : A, refl (f x)) = refl f := + !path_pi_eta + + /- The identification of the path space of a dependent function space, up to equivalence, is of course just funext. -/ + + definition path_equiv_homotopy [H : funext] (f g : Πx, B x) : (f = g) ≃ (f ∼ g) := + equiv.mk _ !funext.ap + + definition is_equiv_path_pi [instance] [H : funext] (f g : Πx, B x) + : is_equiv (@path_pi _ _ _ f g) := + inv_closed apD10 + + definition homotopy_equiv_path [H : funext] (f g : Πx, B x) : (f ∼ g) ≃ (f = g) := + equiv.mk _ !is_equiv_path_pi + + + /- Transport -/ + + protected definition transport (p : a = a') (f : Π(b : B a), C a b) + : (transport (λa, Π(b : B a), C a b) p f) + ∼ (λb, transport (C a') !transport_pV (transportD _ _ p _ (f (p⁻¹ ▹ b)))) := + eq.rec_on p (λx, idp) + + /- A special case of [transport_pi] where the type [B] does not depend on [A], + and so it is just a fixed type [B]. -/ + definition transport_constant {C : A → A' → Type} (p : a = a') (f : Π(b : A'), C a b) + : (eq.transport (λa, Π(b : A'), C a b) p f) ∼ (λb, eq.transport (λa, C a b) p (f b)) := + eq.rec_on p (λx, idp) + + /- Maps on paths -/ + + /- The action of maps given by lambda. -/ + definition ap_lambdaD [H : funext] {C : A' → Type} (p : a = a') (f : Πa b, C b) : + ap (λa b, f a b) p = path_pi (λb, ap (λa, f a b) p) := + begin + apply (eq.rec_on p), + apply inverse, + apply path_pi_idp + end + + /- Dependent paths -/ + + /- with more implicit arguments the conclusion of the following theorem is + (Π(b : B a), transportD B C p b (f b) = g (eq.transport B p b)) ≃ + (eq.transport (λa, Π(b : B a), C a b) p f = g) -/ + definition dpath_pi [H : funext] (p : a = a') (f : Π(b : B a), C a b) (g : Π(b' : B a'), C a' b') + : (Π(b : B a), p ▹D (f b) = g (p ▹ b)) ≃ (p ▹ f = g) := + eq.rec_on p (λg, !homotopy_equiv_path) g + + section open sigma sigma.ops + /- more implicit arguments: + (Π(b : B a), eq.transport C (sigma.path p idp) (f b) = g (p ▹ b)) ≃ + (Π(b : B a), transportD B (λ(a : A) (b : B a), C ⟨a, b⟩) p b (f b) = g (eq.transport B p b)) -/ + definition dpath_pi_sigma {C : (Σa, B a) → Type} (p : a = a') + (f : Π(b : B a), C ⟨a, b⟩) (g : Π(b' : B a'), C ⟨a', b'⟩) : + (Π(b : B a), (sigma.path p idp) ▹ (f b) = g (p ▹ b)) ≃ (Π(b : B a), p ▹D (f b) = g (p ▹ b)) := + eq.rec_on p (λg, !equiv.refl) g + end + + variables (f0 : A' → A) (f1 : Π(a':A'), B (f0 a') → B' a') + + definition transport_V [reducible] (P : A → Type) {x y : A} (p : x = y) (u : P y) : P x := + p⁻¹ ▹ u + + protected definition functor_pi : (Π(a:A), B a) → (Π(a':A'), B' a') := (λg a', f1 a' (g (f0 a'))) + /- Equivalences -/ + definition isequiv_functor_pi [instance] (f0 : A' → A) (f1 : Π(a':A'), B (f0 a') → B' a') + [H0 : is_equiv f0] [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')] + : is_equiv (functor_pi f0 f1) := + begin + apply (adjointify (functor_pi f0 f1) (functor_pi (f0⁻¹) + (λ(a : A) (b' : B' (f0⁻¹ a)), transport B (retr f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))), + intro h, apply path_pi, + esimp {functor_pi, function.compose}, -- simplify (and unfold function_pi and function.compose) + --first subgoal + intro a', esimp, + rewrite adj, + rewrite -transport_compose, + rewrite {f1 a' _}(ap_transport _ f1 _), + apply (transport_V (λx, sect f0 a' ▹ x = h a') (retr (f1 _) _)), + -- retr cannot be used as rewrite rule, the resulting type is not an equality + apply apD, + intro h, beta, + apply path_pi, intro a, esimp, + apply (transport_V (λx, retr f0 a ▹ x = h a) (sect (f1 _) _)), + esimp {function.id}, + apply apD + end + +end pi