From 5ceac83b6ad96a761a583e1208521c6f798f06dc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Nov 2015 12:37:19 -0800 Subject: [PATCH] feat(frontends/lean/elaborator): restrict the number of places where coercions are considered We do not consider coercions around meta-variables anymore. --- hott/algebra/category/functor/yoneda.hlean | 2 +- library/data/rat/basic.lean | 4 ++-- library/data/real/basic.lean | 18 ++++++++-------- src/frontends/lean/elaborator.cpp | 2 +- tests/lean/run/coe_issue2.lean | 8 ++++++++ tests/lean/run/coe_issue3.lean | 24 ++++++++++++++++++++++ 6 files changed, 45 insertions(+), 13 deletions(-) create mode 100644 tests/lean/run/coe_issue2.lean create mode 100644 tests/lean/run/coe_issue3.lean diff --git a/hott/algebra/category/functor/yoneda.hlean b/hott/algebra/category/functor/yoneda.hlean index 871898c35..4aa03008d 100644 --- a/hott/algebra/category/functor/yoneda.hlean +++ b/hott/algebra/category/functor/yoneda.hlean @@ -50,7 +50,7 @@ namespace yoneda end definition yoneda_lemma_equiv [constructor] {C : Precategory} (c : C) - (F : Cᵒᵖ ⇒ cset) : hom (ɏ c) F ≃ lift (F c) := + (F : Cᵒᵖ ⇒ cset) : hom (ɏ c) F ≃ lift (trunctype.carrier (to_fun_ob F c)) := begin fapply equiv.MK, { intro η, exact up (η c id)}, diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index 0f5c30900..bf9c2dab2 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -360,10 +360,10 @@ definition of_num [coercion] [reducible] (n : num) : ℚ := num.to.rat n protected definition prio := num.pred int.prio definition rat_has_zero [reducible] [instance] [priority rat.prio] : has_zero rat := -has_zero.mk (0:int) +has_zero.mk (of_int 0) definition rat_has_one [reducible] [instance] [priority rat.prio] : has_one rat := -has_one.mk (1:int) +has_one.mk (of_int 1) theorem of_int_zero : of_int (0:int) = (0:rat) := rfl diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index a2d6f7c79..4acabb989 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -33,7 +33,7 @@ private theorem s_mul_assoc_lemma_3 (a b n : ℕ+) (p : ℚ) : p * ((a * n)⁻¹ + (b * n)⁻¹) = p * (a⁻¹ + b⁻¹) * n⁻¹ := by rewrite [rat.mul_assoc, right_distrib, *pnat.inv_mul_eq_mul_inv] -private theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : q > 0) +private theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : q > 0) (H : n ≥ pceil (q / ε)) : q * n⁻¹ ≤ ε := begin @@ -188,7 +188,7 @@ theorem eq_of_bdd {s t : seq} (Hs : regular s) (Ht : regular t) have Hj : (∀ j : ℕ+, abs (s n - t n) ≤ n⁻¹ + n⁻¹ + j⁻¹ + j⁻¹ + j⁻¹), begin intros, cases H j with [Nj, HNj], - rewrite [-(sub_add_cancel (s n) (s (max j Nj))), +sub_eq_add_neg, + rewrite [-(sub_add_cancel (s n) (s (max j Nj))), +sub_eq_add_neg, add.assoc (s n + -s (max j Nj)), ↑regular at *], apply rat.le_trans, apply abs_add_le_abs_add_abs, @@ -207,7 +207,7 @@ theorem eq_of_bdd {s t : seq} (Hs : regular s) (Ht : regular t) n⁻¹ + m⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) = n⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) + m⁻¹ : add.right_comm ... = n⁻¹ + (j⁻¹ + m⁻¹ + n⁻¹) + m⁻¹ : add.assoc ... = n⁻¹ + (n⁻¹ + (j⁻¹ + m⁻¹)) + m⁻¹ : add.comm - ... = n⁻¹ + n⁻¹ + j⁻¹ + (m⁻¹ + m⁻¹) : + ... = n⁻¹ + n⁻¹ + j⁻¹ + (m⁻¹ + m⁻¹) : by rewrite[-*add.assoc], rewrite hsimp, have Hms : (max j Nj)⁻¹ + (max j Nj)⁻¹ ≤ j⁻¹ + j⁻¹, begin @@ -482,7 +482,7 @@ private theorem s_mul_assoc_lemma_5 {s t u : seq} (Hs : regular s) (Ht : regular apply Kq_bound_nonneg Hu, end -private theorem s_mul_assoc_lemma_2 {s t u : seq} (Hs : regular s) (Ht : regular t) +private theorem s_mul_assoc_lemma_2 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) (a b c d : ℕ+) : abs (t a) * abs (u b) * abs (s a - s c) + abs (s c) * abs (t a) * abs (u b - u d) + abs (s c) * abs (u d) * abs (t a - t d) ≤ @@ -614,7 +614,7 @@ theorem add_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu : end set_option tactic.goal_names false -private theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c : ℕ+) +private theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c : ℕ+) (j : ℕ+) : ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → abs (s (a * n) * t (b * n) - s (c * n) * t (c * n)) ≤ j⁻¹ := begin @@ -815,7 +815,7 @@ theorem diff_equiv_zero_of_equiv {s t : seq} (Hs : regular s) (Ht : regular t) ( repeat (assumption | apply reg_add_reg | apply reg_neg_reg) end -private theorem mul_well_defined_half1 {s t u : seq} (Hs : regular s) (Ht : regular t) +private theorem mul_well_defined_half1 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) (Etu : t ≡ u) : smul s t ≡ smul s u := begin apply equiv_of_diff_equiv_zero, @@ -839,7 +839,7 @@ private theorem mul_well_defined_half1 {s t u : seq} (Hs : regular s) (Ht : regu apply zero_is_reg) end -private theorem mul_well_defined_half2 {s t u : seq} (Hs : regular s) (Ht : regular t) +private theorem mul_well_defined_half2 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) (Est : s ≡ t) : smul s u ≡ smul t u := begin apply equiv.trans, @@ -1098,10 +1098,10 @@ definition of_nat [coercion] (n : ℕ) : ℝ := nat.to.real 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 := -has_zero.mk (0:rat) +has_zero.mk (of_rat 0) definition real_has_one [reducible] [instance] [priority real.prio] : has_one real := -has_one.mk (1:rat) +has_one.mk (of_rat 1) theorem real_zero_eq_rat_zero : (0:real) = of_rat (0:rat) := rfl diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index ad8cf5095..8dd76e1e1 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -616,7 +616,7 @@ pair elaborator::mk_delayed_coercion( pair elaborator::ensure_has_type_core( expr const & a, expr const & a_type, expr const & expected_type, bool use_expensive_coercions, justification const & j) { bool lifted_coe = false; - if (m_ctx.m_coercions) { + if (m_ctx.m_coercions && !is_meta(a)) { if (use_expensive_coercions && has_coercions_from(a_type, lifted_coe) && ((!lifted_coe && is_meta(expected_type)) || (lifted_coe && is_pi_meta(expected_type)))) { return mk_delayed_coercion(a, a_type, expected_type, j); diff --git a/tests/lean/run/coe_issue2.lean b/tests/lean/run/coe_issue2.lean new file mode 100644 index 000000000..56ed2c24b --- /dev/null +++ b/tests/lean/run/coe_issue2.lean @@ -0,0 +1,8 @@ +import data.int data.real +open int real + +example : (1 : ℤ) * (1 : ℤ) = (1 : ℤ) := +sorry + +example : (1 : ℤ) * 1 = 1 := +sorry diff --git a/tests/lean/run/coe_issue3.lean b/tests/lean/run/coe_issue3.lean new file mode 100644 index 000000000..3030d7c50 --- /dev/null +++ b/tests/lean/run/coe_issue3.lean @@ -0,0 +1,24 @@ +import data.int data.real +open algebra nat int rat real + +example : (1 : ℤ) * (1 : ℤ) = (1 : ℤ) := +sorry + +example : (1 : ℤ) * 1 = 1 := +sorry + +example : (1 : ℝ) * (1 : ℝ) = (1 : ℝ) := +sorry + +example : (1 : ℝ) * 1 = 1 := +sorry + +variable x : ℝ +variable a : ℤ +variable n : ℕ + +example : x + a + n + 1 = 1 := +sorry + +example : x + 1 = 1 + x := +sorry