From 42fbc63bb64c2055091804e2400f0d2fd15e77b6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Feb 2016 13:15:42 -0800 Subject: [PATCH] fix(library/tc_multigraph): avoid name collisions @avigad, @fpvandoorn, @rlewis1988, @dselsam I changed how transitive instances are named. The motivation is to avoid a naming collision problem found by Daniel. Before this commit, we were getting an error on the following file tests/lean/run/collision_bug.lean. Now, transitive instances contain the prefix "_trans_". It makes it clear this is an internal definition and it should not be used by users. This change also demonstrates (again) how the `rewrite` tactic is fragile. The problem is that the matching procedure used by it has very little support for solving matching constraints that involving type class instances. Eventually, we will need to reimplement `rewrite` using the new unification procedure used in blast. In the meantime, the workaround is to use `krewrite` (as usual). --- hott/algebra/category/functor/yoneda.hlean | 2 +- .../category/limits/functor_preserve.hlean | 2 +- hott/algebra/category/limits/set.hlean | 1 - hott/algebra/hott.hlean | 2 +- hott/types/int/basic.hlean | 3 +- library/algebra/group_power.lean | 6 ++-- library/algebra/ring_power.lean | 12 +++---- library/data/complex.lean | 8 ++--- library/data/int/div.lean | 2 +- library/data/int/power.lean | 2 +- library/data/nat/bigops.lean | 4 +-- library/data/nat/power.lean | 4 +-- library/data/rat/basic.lean | 4 +-- library/data/real/basic.lean | 4 +-- library/theories/analysis/real_limit.lean | 4 +-- library/theories/combinatorics/choose.lean | 4 +-- .../number_theory/prime_factorization.lean | 2 +- src/library/tc_multigraph.cpp | 34 ++++--------------- tests/lean/852.hlean | 2 +- tests/lean/852.hlean.expected.out | 6 ---- tests/lean/binder_overload.lean.expected.out | 13 +++++-- tests/lean/extra/show_goal.lean | 2 +- .../lean/notation_priority.lean.expected.out | 8 ++--- tests/lean/pp_all.lean.expected.out | 9 ++--- tests/lean/run/collision_bug.lean | 2 ++ tests/lean/run/inj_tac.lean | 2 +- 26 files changed, 64 insertions(+), 80 deletions(-) create mode 100644 tests/lean/run/collision_bug.lean diff --git a/hott/algebra/category/functor/yoneda.hlean b/hott/algebra/category/functor/yoneda.hlean index 93b5958ae..8d50af170 100644 --- a/hott/algebra/category/functor/yoneda.hlean +++ b/hott/algebra/category/functor/yoneda.hlean @@ -17,7 +17,7 @@ namespace yoneda However, we don't want to have them globally, because that will unfold the composition g ∘ f in a Category to category.category.comp g f -/ - local attribute Category.to.precategory category.to_precategory [constructor] + local attribute category.to_precategory [constructor] -- should this be defined as "yoneda_embedding Cᵒᵖ"? definition contravariant_yoneda_embedding [constructor] [reducible] diff --git a/hott/algebra/category/limits/functor_preserve.hlean b/hott/algebra/category/limits/functor_preserve.hlean index fd42ebc35..d29f6fb66 100644 --- a/hott/algebra/category/limits/functor_preserve.hlean +++ b/hott/algebra/category/limits/functor_preserve.hlean @@ -50,7 +50,7 @@ namespace category /- yoneda preserves existing limits -/ - local attribute Category.to.precategory category.to_precategory [constructor] + local attribute category.to_precategory [constructor] definition preserves_existing_limits_yoneda_embedding_lemma [constructor] (y : cone_obj F) [H : is_terminal y] {G : Cᵒᵖ ⇒ cset} (η : constant_functor I G ⟹ ɏ ∘f F) : diff --git a/hott/algebra/category/limits/set.hlean b/hott/algebra/category/limits/set.hlean index ac65e8f52..3d2d2c2ea 100644 --- a/hott/algebra/category/limits/set.hlean +++ b/hott/algebra/category/limits/set.hlean @@ -11,7 +11,6 @@ import .colimits ..constructions.set hit.set_quotient open eq functor is_trunc sigma pi sigma.ops trunc set_quotient namespace category - local attribute Category.to.precategory [unfold 1] local attribute category.to_precategory [unfold 2] definition is_complete_set_cone.{u v w} [constructor] diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean index b59b577e7..53bddbf99 100644 --- a/hott/algebra/hott.hlean +++ b/hott/algebra/hott.hlean @@ -27,7 +27,7 @@ namespace algebra -- coercions between them anymore. -- So, an application such as (@mul A G g h) in the following definition -- is type incorrect if the coercion is not added (explicitly or implicitly). - local attribute group.to.has_mul [coercion] + definition group.to_has_mul [coercion] {A : Type} (H : group A) : has_mul A := _ local attribute group.to_has_inv [coercion] universe variable l diff --git a/hott/types/int/basic.hlean b/hott/types/int/basic.hlean index c004028b6..142f3f32d 100644 --- a/hott/types/int/basic.hlean +++ b/hott/types/int/basic.hlean @@ -380,7 +380,8 @@ calc ... = nat_abs a : abstr_repr theorem padd_pneg (p : ℕ × ℕ) : padd p (pneg p) ≡ (0, 0) := -show pr1 p + pr2 p + 0 = pr2 p + pr1 p + 0, from !nat.add_comm ▸ rfl +show pr1 p + pr2 p + 0 = pr2 p + pr1 p + 0, +by rewrite [nat.add_comm (pr1 p)] theorem padd_padd_pneg (p q : ℕ × ℕ) : padd (padd p q) (pneg q) ≡ p := calc pr1 p + pr1 q + pr2 q + pr2 p diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean index 6b11d9627..167bdb609 100644 --- a/library/algebra/group_power.lean +++ b/library/algebra/group_power.lean @@ -71,7 +71,7 @@ theorem one_pow : ∀ n : ℕ, 1^n = (1:A) theorem pow_add (a : A) (m n : ℕ) : a^(m + n) = a^m * a^n := begin induction n with n ih, - {rewrite [nat.add_zero, pow_zero, mul_one]}, + {krewrite [nat.add_zero, pow_zero, mul_one]}, rewrite [add_succ, *pow_succ', ih, mul.assoc] end @@ -171,7 +171,7 @@ include s theorem pow_pos {a : A} (H : a > 0) (n : ℕ) : a ^ n > 0 := begin induction n, - rewrite pow_zero, + krewrite pow_zero, apply zero_lt_one, rewrite pow_succ', apply mul_pos, @@ -181,7 +181,7 @@ theorem pow_pos {a : A} (H : a > 0) (n : ℕ) : a ^ n > 0 := theorem pow_ge_one_of_ge_one {a : A} (H : a ≥ 1) (n : ℕ) : a ^ n ≥ 1 := begin induction n, - rewrite pow_zero, + krewrite pow_zero, apply le.refl, rewrite [pow_succ', -mul_one 1], apply mul_le_mul v_0 H zero_le_one, diff --git a/library/algebra/ring_power.lean b/library/algebra/ring_power.lean index bcde5a2ea..dbf2bf56e 100644 --- a/library/algebra/ring_power.lean +++ b/library/algebra/ring_power.lean @@ -21,7 +21,7 @@ theorem zero_pow {m : ℕ} (mpos : m > 0) : 0^m = (0 : A) := have h₁ : ∀ m : nat, (0 : A)^(succ m) = (0 : A), begin intro m, induction m, - rewrite pow_one, + krewrite pow_one, apply zero_mul end, obtain m' (h₂ : m = succ m'), from exists_eq_succ_of_pos mpos, @@ -45,7 +45,7 @@ or.elim (eq_zero_or_pos m) begin intro m, induction m with m ih, - {rewrite pow_one; intros; assumption}, + {krewrite pow_one; intros; assumption}, rewrite pow_succ, intro H, cases eq_zero_or_eq_zero_of_mul_eq_zero H with h₃ h₄, @@ -73,7 +73,7 @@ or.elim (eq_zero_or_pos m) begin intro m, induction m with m ih, - {rewrite pow_one; assumption}, + { krewrite pow_one; assumption }, rewrite pow_succ, apply division_ring.mul_ne_zero H ih end, @@ -136,7 +136,7 @@ monoid_has_pow_nat theorem abs_pow (a : A) (n : ℕ) : abs (a^n) = abs a^n := begin induction n with n ih, - rewrite [*pow_zero, (abs_of_nonneg zero_le_one : abs (1 : A) = 1)], + krewrite [*pow_zero, (abs_of_nonneg zero_le_one : abs (1 : A) = 1)], rewrite [*pow_succ, abs_mul, ih] end @@ -149,7 +149,7 @@ include s theorem field.div_pow (a : A) {b : A} {n : ℕ} (bnz : b ≠ 0) : (a / b)^n = a^n / b^n := begin induction n with n ih, - rewrite [*pow_zero, div_one], + krewrite [*pow_zero, div_one], have bnnz : b^n ≠ 0, from division_ring.pow_ne_zero_of_ne_zero bnz, rewrite [*pow_succ, ih, !field.div_mul_div bnz bnnz] end @@ -163,7 +163,7 @@ include s theorem div_pow (a : A) {b : A} {n : ℕ} : (a / b)^n = a^n / b^n := begin induction n with n ih, - rewrite [*pow_zero, div_one], + krewrite [*pow_zero, div_one], rewrite [*pow_succ, ih, div_mul_div] end diff --git a/library/data/complex.lean b/library/data/complex.lean index 491544041..1c4e9592f 100644 --- a/library/data/complex.lean +++ b/library/data/complex.lean @@ -30,10 +30,10 @@ protected proposition eta (z : ℂ) : complex.mk (complex.re z) (complex.im z) = by cases z; exact rfl definition of_real [coercion] (x : ℝ) : ℂ := complex.mk x 0 -definition of_rat [coercion] (q : ℚ) : ℂ := rat.to.complex q -definition of_int [coercion] (i : ℤ) : ℂ := int.to.complex i -definition of_nat [coercion] (n : ℕ) : ℂ := nat.to.complex n -definition of_num [coercion] [reducible] (n : num) : ℂ := num.to.complex n +definition of_rat [coercion] (q : ℚ) : ℂ := q +definition of_int [coercion] (i : ℤ) : ℂ := i +definition of_nat [coercion] (n : ℕ) : ℂ := n +definition of_num [coercion] [reducible] (n : num) : ℂ := n protected definition prio : num := num.pred real.prio diff --git a/library/data/int/div.lean b/library/data/int/div.lean index 9b21a8b40..8ea0bef1b 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -99,7 +99,7 @@ calc ... < 0 : neg_neg_of_pos this protected theorem zero_div (b : ℤ) : 0 / b = 0 := -by rewrite [of_nat_div_eq, nat.zero_div, of_nat_zero, mul_zero] +by krewrite [of_nat_div_eq, nat.zero_div, of_nat_zero, mul_zero] protected theorem div_zero (a : ℤ) : a / 0 = 0 := by rewrite [div_def, sign_zero, zero_mul] diff --git a/library/data/int/power.lean b/library/data/int/power.lean index a97d65461..abec75efc 100644 --- a/library/data/int/power.lean +++ b/library/data/int/power.lean @@ -23,7 +23,7 @@ theorem of_nat_pow (a n : ℕ) : of_nat (a^n) = (of_nat a)^n := begin induction n with n ih, apply eq.refl, - rewrite [pow_succ, pow_succ, of_nat_mul, ih] + krewrite [pow_succ, pow_succ, of_nat_mul, ih] end end int diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean index 6784624bf..4307166cf 100644 --- a/library/data/nat/bigops.lean +++ b/library/data/nat/bigops.lean @@ -35,7 +35,7 @@ proposition sum_range_def (m n : ℕ) (f : ℕ → A) : proposition sum_range_self (m : ℕ) (f : ℕ → A) : (∑ i = m...m, f i) = f m := - by rewrite [↑sum_range, succ_sub !le.refl, nat.sub_self, sum_up_to_one, zero_add] + by krewrite [↑sum_range, succ_sub !le.refl, nat.sub_self, sum_up_to_one, zero_add] proposition sum_range_succ {m n : ℕ} (f : ℕ → A) (H : m ≤ succ n) : (∑ i = m...succ n, f i) = (∑ i = m...n, f i) + f (succ n) := @@ -126,7 +126,7 @@ proposition prod_range_def (m n : ℕ) (f : ℕ → A) : proposition prod_range_self (m : ℕ) (f : ℕ → A) : (∏ i = m...m, f i) = f m := -by rewrite [↑prod_range, succ_sub !le.refl, nat.sub_self, prod_up_to_one, zero_add] +by krewrite [↑prod_range, succ_sub !le.refl, nat.sub_self, prod_up_to_one, zero_add] proposition prod_range_succ {m n : ℕ} (f : ℕ → A) (H : m ≤ succ n) : (∏ i = m...succ n, f i) = (∏ i = m...n, f i) * f (succ n) := diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean index 7b093734b..b97ad5c8f 100644 --- a/library/data/nat/power.lean +++ b/library/data/nat/power.lean @@ -24,7 +24,7 @@ or.elim (eq_zero_or_pos m) begin intro m, induction m with m ih, - {rewrite pow_one; intros; assumption}, + {krewrite pow_one; intros; assumption}, rewrite pow_succ, intro H, cases eq_zero_or_eq_zero_of_mul_eq_zero H with h₃ h₄, @@ -53,7 +53,7 @@ theorem le_pow_self {x : ℕ} (H : x > 1) : ∀ i, i ≤ x^i theorem mul_self_eq_pow_2 (a : nat) : a * a = a ^ 2 := show a * a = a ^ (succ (succ zero)), from -by rewrite [*pow_succ, *pow_zero, mul_one] +by krewrite [*pow_succ, *pow_zero, mul_one] theorem pow_cancel_left : ∀ {a b c : nat}, a > 1 → a ^ b = a ^ c → b = c | a 0 0 h₁ h₂ := rfl diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index 837ab5afe..4bf4b982e 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -353,8 +353,8 @@ namespace rat /- operations -/ definition of_int [coercion] (i : ℤ) : ℚ := ⟦prerat.of_int i⟧ -definition of_nat [coercion] (n : ℕ) : ℚ := nat.to.rat n -definition of_num [coercion] [reducible] (n : num) : ℚ := num.to.rat n +definition of_nat [coercion] (n : ℕ) : ℚ := n +definition of_num [coercion] [reducible] (n : num) : ℚ := n protected definition prio := num.pred int.prio diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index 472a7c118..9e6ebbed8 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -1092,8 +1092,8 @@ has_sub.mk real.sub open rat -- no coercions before definition of_rat [coercion] (a : ℚ) : ℝ := quot.mk (r_const a) -definition of_int [coercion] (i : ℤ) : ℝ := int.to.real i -definition of_nat [coercion] (n : ℕ) : ℝ := nat.to.real n +definition of_int [coercion] (i : ℤ) : ℝ := i +definition of_nat [coercion] (n : ℕ) : ℝ := n definition of_num [coercion] [reducible] (n : num) : ℝ := of_rat (rat.of_num n) definition real_has_zero [reducible] [instance] [priority real.prio] : has_zero real := diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index 9f7c9bf0c..45df21ba8 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -367,11 +367,11 @@ proposition mul_converges_to_seq (HX : X ⟶ x in ℕ) (HY : Y ⟶ y in ℕ) : apply converges_to_seq_constant, rewrite -{0}zero_add, apply add_converges_to_seq, - rewrite -(mul_zero K), + krewrite -(mul_zero K), apply mul_left_converges_to_seq, apply abs_sub_converges_to_seq_of_converges_to_seq, exact HY, - rewrite -(mul_zero (abs y)), + krewrite -(mul_zero (abs y)), apply mul_left_converges_to_seq, apply abs_sub_converges_to_seq_of_converges_to_seq, exact HX diff --git a/library/theories/combinatorics/choose.lean b/library/theories/combinatorics/choose.lean index 464de0efc..84eda84b2 100644 --- a/library/theories/combinatorics/choose.lean +++ b/library/theories/combinatorics/choose.lean @@ -58,7 +58,7 @@ begin induction n with [n, ih], {apply rfl}, change choose (succ n) (succ 0) = succ n, - rewrite [choose_succ_succ, ih, choose_zero_right] + krewrite [choose_succ_succ, ih, choose_zero_right] end theorem choose_pos {n : ℕ} : ∀ {k : ℕ}, k ≤ n → choose n k > 0 := @@ -87,7 +87,7 @@ begin krewrite [one_mul, choose_zero_succ, choose_eq_zero_of_lt H, zero_mul]}}, intro k, cases k with k', - {rewrite [choose_zero_right, choose_one_right]}, + {krewrite [choose_zero_right, choose_one_right]}, rewrite [choose_succ_succ (succ n), right_distrib, -ih (succ k')], rewrite [choose_succ_succ at {1}, left_distrib, *succ_mul (succ n), mul_succ, -ih k'], rewrite [*add.assoc, add.left_comm (choose n _)] diff --git a/library/theories/number_theory/prime_factorization.lean b/library/theories/number_theory/prime_factorization.lean index 78625b908..a7a9a4106 100644 --- a/library/theories/number_theory/prime_factorization.lean +++ b/library/theories/number_theory/prime_factorization.lean @@ -246,7 +246,7 @@ theorem mult_pow_eq_zero_of_prime_of_ne {p q : ℕ} (primep : prime p) (primeq : (pneq : p ≠ q) (i : ℕ) : mult p (q^i) = 0 := begin induction i with i ih, - {rewrite [pow_zero, mult_one_right]}, + {krewrite [pow_zero, mult_one_right]}, have qpos : q > 0, from pos_of_prime primeq, have qipos : q^i > 0, from !pow_pos_of_pos qpos, rewrite [pow_succ', mult_mul primep qipos qpos, ih, mult_eq_zero_of_prime_of_ne primep diff --git a/src/library/tc_multigraph.cpp b/src/library/tc_multigraph.cpp index 8b4986711..dec400055 100644 --- a/src/library/tc_multigraph.cpp +++ b/src/library/tc_multigraph.cpp @@ -59,30 +59,8 @@ struct add_edge_fn { m_graph.m_edges.insert(edge, src); } - - static name compose_name_core(name const & src, name const & tgt) { - return src + name("to") + tgt; - } - - static name compose_name(name const & p, name const & src, name const & tgt) { - if (is_prefix_of(p, tgt)) - return compose_name_core(src, tgt.replace_prefix(p, name())); - else if (p.is_atomic()) - return compose_name_core(src, tgt); - else - return compose_name(p.get_prefix(), src, tgt); - } - - static name compose_name(name const & src, name const & tgt) { - if (src.is_atomic()) - return compose_name_core(src, tgt); - else - return compose_name(src.get_prefix(), src, tgt); - } - - name compose(name const & src, name const & e1, name const & e2, name const & tgt) { - name n = compose_name(src, tgt); - pair env_e = ::lean::compose(m_env, *m_tc, e2, e1, optional(n)); + name compose(name const & base_name, name const & e1, name const & e2) { + pair env_e = ::lean::compose(m_env, *m_tc, e2, e1, optional(base_name)); m_env = env_e.first; return env_e.second; } @@ -90,6 +68,7 @@ struct add_edge_fn { pair> operator()(name const & src, name const & edge, name const & tgt) { buffer new_edges; if (auto preds = m_graph.m_predecessors.find(src)) { + name base_name = edge.append_before("_trans_to_"); for (name const & pred : *preds) { if (pred == tgt) continue; // avoid loops @@ -97,7 +76,7 @@ struct add_edge_fn { for (pair const & p : *pred_succ) { if (p.second != src) continue; - name new_e = compose(pred, p.first, edge, tgt); + name new_e = compose(base_name, p.first, edge); new_edges.emplace_back(pred, new_e, tgt); } } @@ -107,15 +86,16 @@ struct add_edge_fn { buffer new_back_edges; new_back_edges.append(new_edges); if (auto succs = m_graph.m_successors.find(tgt)) { + name base_name = edge.append_before("_trans_of_"); for (pair const & p : *succs) { if (src == p.second) continue; // avoid loops - name new_e = compose(src, edge, p.first, p.second); + name new_e = compose(base_name, edge, p.first); new_edges.emplace_back(src, new_e, p.second); for (auto const & back_edge : new_back_edges) { if (back_edge.m_from != p.second) continue; - name new_e = compose(back_edge.m_from, back_edge.m_cnst, p.first, p.second); + name new_e = compose(base_name, back_edge.m_cnst, p.first); new_edges.emplace_back(back_edge.m_from, new_e, p.second); } } diff --git a/tests/lean/852.hlean b/tests/lean/852.hlean index d6954c0b4..7fc17ae67 100644 --- a/tests/lean/852.hlean +++ b/tests/lean/852.hlean @@ -2,4 +2,4 @@ import algebra.category.functor.equivalence -- print prefix category.equivalence -check @category.equivalence.to._Fun +-- check @category.equivalence.to._Fun diff --git a/tests/lean/852.hlean.expected.out b/tests/lean/852.hlean.expected.out index ce53e0e8b..e69de29bb 100644 --- a/tests/lean/852.hlean.expected.out +++ b/tests/lean/852.hlean.expected.out @@ -1,6 +0,0 @@ -category.equivalence.to._Fun : - Π {C : category.Precategory} {D : category.Precategory} (c : category.equivalence C D) - {a b : category.Precategory.carrier C}, - category.hom a b → - category.hom (functor.to_fun_ob (category.equivalence.to_functor c) a) - (functor.to_fun_ob (category.equivalence.to_functor c) b) diff --git a/tests/lean/binder_overload.lean.expected.out b/tests/lean/binder_overload.lean.expected.out index 71813e21b..6adfc8960 100644 --- a/tests/lean/binder_overload.lean.expected.out +++ b/tests/lean/binder_overload.lean.expected.out @@ -1,8 +1,15 @@ {x : ℕ ∈ S | x > 0} : set ℕ {x : ℕ ∈ s | x > 0} : finset ℕ -@set.sep.{1} nat (λ (x : nat), @gt.{1} nat _source.to.has_lt x (@zero.{1} nat _source.to.has_zero)) S : set.{1} nat +@set.sep.{1} nat + (λ (x : nat), + @gt.{1} nat nat._trans_of_decidable_linear_ordered_semiring_13 x + (@zero.{1} nat nat._trans_of_decidable_linear_ordered_semiring_6)) + S : + set.{1} nat @finset.sep.{1} nat (λ (a b : nat), nat.has_decidable_eq a b) - (λ (x : nat), @gt.{1} nat _source.to.has_lt x (@zero.{1} nat _source.to.has_zero)) - (λ (a : nat), nat.decidable_lt (@zero.{1} nat _source.to.has_zero) a) + (λ (x : nat), + @gt.{1} nat nat._trans_of_decidable_linear_ordered_semiring_13 x + (@zero.{1} nat nat._trans_of_decidable_linear_ordered_semiring_6)) + (λ (a : nat), nat.decidable_lt (@zero.{1} nat nat._trans_of_decidable_linear_ordered_semiring_6) a) s : finset.{1} nat diff --git a/tests/lean/extra/show_goal.lean b/tests/lean/extra/show_goal.lean index 5dba4c039..a5489e1a3 100644 --- a/tests/lean/extra/show_goal.lean +++ b/tests/lean/extra/show_goal.lean @@ -13,7 +13,7 @@ begin have ceq : c = 0, begin rewrite aeq0 at h₃, rewrite add_zero at h₃, - rewrite add_succ at h₃, + krewrite add_succ at h₃, krewrite add_zero at h₃, injection h₃, exact a_1 end, diff --git a/tests/lean/notation_priority.lean.expected.out b/tests/lean/notation_priority.lean.expected.out index af4e2ac54..9db0fe887 100644 --- a/tests/lean/notation_priority.lean.expected.out +++ b/tests/lean/notation_priority.lean.expected.out @@ -1,4 +1,4 @@ -@add.{1} nat _source.to.has_add a b : nat -@add.{1} int _source.to.has_add_1 i j : int -@add.{1} nat _source.to.has_add a b : nat -@add.{1} int _source.to.has_add_1 i j : int +@add.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2 a b : nat +@add.{1} int int._trans_of_linear_ordered_comm_ring_16 i j : int +@add.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2 a b : nat +@add.{1} int int._trans_of_linear_ordered_comm_ring_16 i j : int diff --git a/tests/lean/pp_all.lean.expected.out b/tests/lean/pp_all.lean.expected.out index 205e9cc63..d40a12b76 100644 --- a/tests/lean/pp_all.lean.expected.out +++ b/tests/lean/pp_all.lean.expected.out @@ -1,8 +1,9 @@ a + of_num b = 10 : Prop @eq.{1} nat - (@add.{1} nat _source.to.has_add ((λ (x : nat), x) a) + (@add.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2 ((λ (x : nat), x) a) (nat.of_num (@bit0.{1} num num_has_add (@one.{1} num num_has_one)))) - (@bit0.{1} nat _source.to.has_add - (@bit1.{1} nat _source.to.has_one _source.to.has_add - (@bit0.{1} nat _source.to.has_add (@one.{1} nat _source.to.has_one)))) : + (@bit0.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2 + (@bit1.{1} nat nat._trans_of_decidable_linear_ordered_semiring_22 nat._trans_of_decidable_linear_ordered_semiring_2 + (@bit0.{1} nat nat._trans_of_decidable_linear_ordered_semiring_2 + (@one.{1} nat nat._trans_of_decidable_linear_ordered_semiring_22)))) : Prop diff --git a/tests/lean/run/collision_bug.lean b/tests/lean/run/collision_bug.lean new file mode 100644 index 000000000..14c62b62e --- /dev/null +++ b/tests/lean/run/collision_bug.lean @@ -0,0 +1,2 @@ +import theories.measure_theory.sigma_algebra +import data.int.order diff --git a/tests/lean/run/inj_tac.lean b/tests/lean/run/inj_tac.lean index 6d6bdb19e..ac8b1625c 100644 --- a/tests/lean/run/inj_tac.lean +++ b/tests/lean/run/inj_tac.lean @@ -38,6 +38,6 @@ example (a₁ a₂ a₃ b₁ b₂ b₃ : nat) : (a₁+2, a₂+3, a₃+1) = (b₁ begin intro H, injection H with a₁b₁ sa₂b₂ a₃sb₃, esimp at *, - rewrite [a₁b₁, a₃sb₃, sa₂b₂], + krewrite [a₁b₁, a₃sb₃, -sa₂b₂], repeat (split | esimp) end