From d0559472438026950fc8d32799fa878eec09ff7e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Apr 2015 12:51:33 -0700 Subject: [PATCH] feat(library/tactic/rewrite_tactic): ignore implicit argument when matching at rewrite tactic --- src/library/tactic/rewrite_tactic.cpp | 8 +- tests/lean/531.hlean | 151 ++++++++++++++++++++++++++ tests/lean/531.hlean.expected.out | 7 ++ 3 files changed, 162 insertions(+), 4 deletions(-) create mode 100644 tests/lean/531.hlean create mode 100644 tests/lean/531.hlean.expected.out diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 3a85c9bf3..79a960d14 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -459,11 +459,11 @@ public: } // Return true iff the given declaration contains inst_implicit arguments - bool has_inst_implicit_args(name const & d) const { + bool has_implicit_args(name const & d) const { if (auto decl = m_tc.env().find(d)) { expr const * it = &decl->get_type(); while (is_pi(*it)) { - if (binding_info(*it).is_inst_implicit()) + if (!is_explicit(binding_info(*it))) return true; it = &binding_body(*it); } @@ -500,7 +500,7 @@ public: } return l_true; } - if (has_inst_implicit_args(const_name(p_fn))) { + if (has_implicit_args(const_name(p_fn))) { // Special support for declarations that contains inst_implicit arguments. // The idea is to skip them during matching. buffer p_args, t_args; @@ -510,7 +510,7 @@ public: return l_false; expr const * it = &m_tc.env().get(const_name(p_fn)).get_type(); for (unsigned i = 0; i < p_args.size(); i++) { - if (is_pi(*it) && binding_info(*it).is_inst_implicit()) { + if (is_pi(*it) && !is_explicit(binding_info(*it))) { it = &binding_body(*it); continue; // skip argument } diff --git a/tests/lean/531.hlean b/tests/lean/531.hlean new file mode 100644 index 000000000..769ec483d --- /dev/null +++ b/tests/lean/531.hlean @@ -0,0 +1,151 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: init.hit +Authors: Floris van Doorn + +Declaration of hits +-/ + +structure diagram [class] := + (Iob : Type) + (Ihom : Type) + (ob : Iob → Type) + (dom cod : Ihom → Iob) + (hom : Π(j : Ihom), ob (dom j) → ob (cod j)) + +open eq diagram + +-- structure col (D : diagram) := +-- (incl : Π{i : Iob}, ob i) +-- (eq_endpoint : Π{j : Ihom} (x : ob (dom j)), ob (cod j)) +-- set_option pp.universes true +-- check @diagram +-- check @col + +constant colimit.{u v w} : diagram.{u v w} → Type.{max u v w} + +namespace colimit + + constant inclusion : Π [D : diagram] {i : Iob}, ob i → colimit D + abbreviation ι := @inclusion + + constant cglue : Π [D : diagram] (j : Ihom) (x : ob (dom j)), ι (hom j x) = ι x + + /-protected-/ constant rec : Π [D : diagram] {P : colimit D → Type} + (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x)) + (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) + (y : colimit D), P y + + -- {P : my_colim f → Type} (Hinc : Π⦃n : ℕ⦄ (a : A n), P (inc f a)) + -- (Heq : Π(n : ℕ) (a : A n), inc_eq f a ▹ Hinc (f a) = Hinc a) : Πaa, P aa + -- init_hit + + definition comp_incl [D : diagram] {P : colimit D → Type} + (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x)) + (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) + {i : Iob} (x : ob i) : rec Pincl Pglue (ι x) = Pincl x := + sorry --idp + + --set_option pp.notation false + definition comp_cglue [D : diagram] {P : colimit D → Type} + (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x)) + (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) + {j : Ihom} (x : ob (dom j)) : apd (rec Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry := + --the sorry's in the statement can be removed when comp_incl is definitional + sorry --idp + + protected definition rec_on [D : diagram] {P : colimit D → Type} (y : colimit D) + (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x)) + (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) : P y := + colimit.rec Pincl Pglue y + +end colimit + +open colimit bool + +namespace pushout +section + +universe u +parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR) + + inductive pushout_ob := + | tl : pushout_ob + | bl : pushout_ob + | tr : pushout_ob + + open pushout_ob + + definition pushout_diag [reducible] : diagram := + diagram.mk pushout_ob + bool + (λi, pushout_ob.rec_on i TL BL TR) + (λj, bool.rec_on j tl tl) + (λj, bool.rec_on j bl tr) + (λj, bool.rec_on j f g) + + local notation `D` := pushout_diag + -- open bool + -- definition pushout_diag : diagram := + -- diagram.mk pushout_ob + -- bool + -- (λi, match i with | tl := TL | tr := TR | bl := BL end) + -- (λj, match j with | tt := tl | ff := tl end) + -- (λj, match j with | tt := bl | ff := tr end) + -- (λj, match j with | tt := f | ff := g end) + + definition pushout := colimit pushout_diag + local attribute pushout_diag [instance] + + definition inl (x : BL) : pushout := + @ι _ _ x + + definition inr (x : TR) : pushout := + @ι _ _ x + + definition coherence (x : TL) : inl (f x) = @ι _ _ x := + @cglue _ _ x + + definition glue (x : TL) : inl (f x) = inr (g x) := + @cglue _ _ x ⬝ (@cglue _ _ x)⁻¹ + + set_option pp.notation false + protected theorem rec {P : pushout → Type} --make def + (Pinl : Π(x : BL), P (inl x)) + (Pinr : Π(x : TR), P (inr x)) + (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x)) + (y : pushout) : P y := + begin + fapply (@colimit.rec_on _ _ y), + { intros [i, x], cases i, + exact (coherence x ▹ Pinl (f x)), + apply Pinl, + apply Pinr}, + { intros [j, x], cases j, + exact idp, + esimp [pushout_ob.cases_on], + apply concat, rotate 1, apply (idpath (coherence x ▹ Pinl (f x))), + apply concat, apply (ap (transport _ _)), apply (idpath (Pinr (g x))), + apply eq_tr_of_inv_tr_eq, + rewrite -{(transport (λ (x : pushout), P x) (inverse (coherence x)) (transport P (@cglue _ tt x) (Pinr (g x))))}con_tr, + apply sorry + } + end + +example +{P : pushout → Type} +{Pinl : Π (x : BL), P (inl x)} +{Pinr : Π (x : TR), P (inr x)} +{Pglue : Π (x : TL), eq (transport (λ (x : pushout), P x) (glue x) (Pinl (f x))) (Pinr (g x))} +{y : pushout} +{x : @ob _ (@dom _ tt)} +: eq (transport (λ (x : pushout), P x) (inverse (coherence x)) (transport P (@cglue _ tt x) (Pinr (g x)))) + (Pinl (f x)) := +begin +rewrite -{(transport (λ (x : pushout), P x) (inverse (coherence x)) (transport P (@cglue _ tt x) (Pinr (g x))))}con_tr, +apply sorry +end + +exit diff --git a/tests/lean/531.hlean.expected.out b/tests/lean/531.hlean.expected.out new file mode 100644 index 000000000..59c5ad3cd --- /dev/null +++ b/tests/lean/531.hlean.expected.out @@ -0,0 +1,7 @@ +531.hlean:49:2: warning: using 'sorry' +531.hlean:55:72: warning: using 'sorry' +531.hlean:55:92: warning: using 'sorry' +531.hlean:57:2: warning: using 'sorry' +531.hlean:133:12: warning: using 'sorry' +531.hlean:148:6: warning: using 'sorry' +531.hlean:151:0: warning: using 'exit' to interrupt Lean