From 19361f01965920d2d1ba665b8d86ec900ab06453 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 May 2015 15:45:23 -0700 Subject: [PATCH] feat(library/unifier): do not fire type class resolution as last resort when type contains metavariables see discussion at #604 --- hott/algebra/category/functor.hlean | 2 +- hott/algebra/category/iso.hlean | 2 +- hott/algebra/category/nat_trans.hlean | 2 +- hott/algebra/field.hlean | 17 +++++++------- hott/algebra/group.hlean | 4 ++-- hott/algebra/ordered_group.hlean | 2 +- hott/algebra/ordered_ring.hlean | 12 +++++----- hott/algebra/ring.hlean | 2 +- hott/hit/trunc.hlean | 2 +- hott/init/trunc.hlean | 2 +- hott/types/eq.hlean | 2 +- library/algebra/category/basic.lean | 2 +- library/algebra/category/functor.lean | 6 ++--- library/algebra/category/morphism.lean | 7 +++--- .../category/natural_transformation.lean | 6 ++--- library/algebra/field.lean | 22 +++++++++---------- library/algebra/group.lean | 4 ++-- library/algebra/group_bigops.lean | 8 +++---- library/algebra/group_power.lean | 2 +- library/algebra/ordered_group.lean | 2 +- library/algebra/ordered_ring.lean | 16 +++++++------- library/algebra/ring.lean | 4 ++-- library/data/finset/bigops.lean | 4 ++-- library/data/finset/card.lean | 4 ++-- library/data/finset/to_set.lean | 8 +++---- library/data/list/set.lean | 2 +- src/library/unifier.cpp | 2 +- tests/lean/const.lean | 2 +- tests/lean/run/alg_rw.lean | 2 +- tests/lean/run/dec_trivial_loop.lean | 2 ++ tests/lean/run/finset.lean | 2 +- tests/lean/run/num_bug2.lean | 4 ++-- tests/lean/run/rewriter2.lean | 2 +- 33 files changed, 83 insertions(+), 79 deletions(-) create mode 100644 tests/lean/run/dec_trivial_loop.lean diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean index 4fe26039e..51f55d10d 100644 --- a/hott/algebra/category/functor.hlean +++ b/hott/algebra/category/functor.hlean @@ -44,7 +44,7 @@ namespace functor protected definition id [reducible] {C : Precategory} : functor C C := mk (λa, a) (λ a b f, f) (λ a, idp) (λ a b c f g, idp) - protected definition ID [reducible] (C : Precategory) : functor C C := id + protected definition ID [reducible] (C : Precategory) : functor C C := @functor.id C definition functor_mk_eq' {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)} {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index b7511708e..3c067191d 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -231,7 +231,7 @@ namespace iso (λ c g h H, calc g = g ∘ id : by rewrite id_right - ... = g ∘ f ∘ section_of f : by rewrite -comp_section + ... = g ∘ f ∘ section_of f : by rewrite -(comp_section f) ... = h ∘ f ∘ section_of f : by rewrite [assoc, H, -assoc] ... = h ∘ id : by rewrite comp_section ... = h : by rewrite id_right) diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean index 54467abf5..4416968b9 100644 --- a/hott/algebra/category/nat_trans.hlean +++ b/hott/algebra/category/nat_trans.hlean @@ -36,7 +36,7 @@ namespace nat_trans mk (λa, id) (λa b f, !id_right ⬝ !id_left⁻¹) protected definition ID [reducible] {C D : Precategory} (F : functor C D) : nat_trans F F := - id + (@id C D F) definition nat_trans_mk_eq {η₁ η₂ : Π (a : C), hom (F a) (G a)} (nat₁ : Π (a b : C) (f : hom a b), G f ∘ η₁ a = η₁ b ∘ F f) diff --git a/hott/algebra/field.hlean b/hott/algebra/field.hlean index e535babc1..cef97927d 100644 --- a/hott/algebra/field.hlean +++ b/hott/algebra/field.hlean @@ -65,20 +65,21 @@ section division_ring definition div_self (H : a ≠ 0) : a / a = 1 := mul_inv_cancel H - definition one_div_one : 1 / 1 = 1 := div_self (ne.symm zero_ne_one) + definition one_div_one : 1 / 1 = (1:A) := + div_self (ne.symm zero_ne_one) definition mul_div_assoc : (a * b) / c = a * (b / c) := !mul.assoc definition one_div_ne_zero (H : a ≠ 0) : 1 / a ≠ 0 := assume H2 : 1 / a = 0, - have C1 : 0 = 1, from inverse (by rewrite [-(mul_one_div_cancel H), H2, mul_zero]), + have C1 : 0 = (1:A), from inverse (by rewrite [-(mul_one_div_cancel H), H2, mul_zero]), absurd C1 zero_ne_one -- definition ne_zero_of_one_div_ne_zero (H : 1 / a ≠ 0) : a ≠ 0 := -- assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H -- the analogue in group is called inv_one - definition inv_one_is_one : 1⁻¹ = 1 := + definition inv_one_is_one : 1⁻¹ = (1:A) := by rewrite [-mul_one, (inv_mul_cancel (ne.symm zero_ne_one))] definition div_one : a / 1 = a := @@ -100,8 +101,8 @@ section division_ring -- make "left" and "right" versions? definition eq_one_div_of_mul_eq_one (H : a * b = 1) : b = 1 / a := have H2 : a ≠ 0, from - (assume A : a = 0, - have B : 0 = 1, by rewrite [-(zero_mul b), -A, H], + (assume aeq0 : a = 0, + have B : 0 = (1:A), by rewrite [-(zero_mul b), -aeq0, H], absurd B zero_ne_one), show b = 1 / a, from inverse (calc 1 / a = (1 / a) * 1 : mul_one @@ -131,7 +132,7 @@ section division_ring rewrite [mul.assoc, -(mul.assoc a), (mul_one_div_cancel Ha), one_mul, (mul_one_div_cancel Hb)], eq_one_div_of_mul_eq_one H - definition one_div_neg_one_eq_neg_one : 1 / (-1) = -1 := + definition one_div_neg_one_eq_neg_one : (1:A) / (-1) = -1 := have H : (-1) * (-1) = 1, by rewrite [-neg_eq_neg_one_mul, neg_neg], inverse (eq_one_div_of_mul_eq_one H) @@ -140,7 +141,7 @@ section division_ring (assume H2 : -1 = 0, absurd (inverse (calc 1 = -(-1) : neg_neg ... = -0 : H2 - ... = 0 : neg_zero)) zero_ne_one), + ... = (0:A) : neg_zero)) zero_ne_one), calc 1 / (- a) = 1 / ((-1) * a) : neg_eq_neg_one_mul ... = (1 / a) * (1 / (- 1)) : one_div_mul_one_div H H1 @@ -339,7 +340,7 @@ section discrete_field definition inv_zero : 0⁻¹ = (0 : A) := !discrete_field.inv_zero - definition one_div_zero : 1 / 0 = 0 := + definition one_div_zero : 1 / 0 = (0:A) := calc 1 / 0 = 1 * 0⁻¹ : refl ... = 1 * 0 : discrete_field.inv_zero A diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean index 7396c5132..68eb99a53 100644 --- a/hott/algebra/group.hlean +++ b/hott/algebra/group.hlean @@ -163,7 +163,7 @@ section group theorem inv_eq_of_mul_eq_one {a b : A} (H : a * b = 1) : a⁻¹ = b := by rewrite [-mul_one a⁻¹, -H, inv_mul_cancel_left] - theorem inv_one : 1⁻¹ = 1 := inv_eq_of_mul_eq_one (one_mul 1) + theorem inv_one : 1⁻¹ = (1:A) := inv_eq_of_mul_eq_one (one_mul 1) theorem inv_inv (a : A) : (a⁻¹)⁻¹ = a := inv_eq_of_mul_eq_one (mul.left_inv a) @@ -281,7 +281,7 @@ section add_group theorem neg_eq_of_add_eq_zero {a b : A} (H : a + b = 0) : -a = b := by rewrite [-add_zero, -H, neg_add_cancel_left] - theorem neg_zero : -0 = 0 := neg_eq_of_add_eq_zero (zero_add 0) + theorem neg_zero : -0 = (0:A) := neg_eq_of_add_eq_zero (zero_add 0) theorem neg_neg (a : A) : -(-a) = a := neg_eq_of_add_eq_zero (add.left_inv a) diff --git a/hott/algebra/ordered_group.hlean b/hott/algebra/ordered_group.hlean index 85b3cb777..db2f6a027 100644 --- a/hott/algebra/ordered_group.hlean +++ b/hott/algebra/ordered_group.hlean @@ -424,7 +424,7 @@ section definition abs_of_neg (H : a < 0) : abs a = -a := if_neg (not_le_of_lt H) - definition abs_zero : abs 0 = 0 := abs_of_nonneg (le.refl _) + definition abs_zero : abs 0 = (0:A) := abs_of_nonneg (le.refl _) definition abs_of_nonpos (H : a ≤ 0) : abs a = -a := decidable.by_cases diff --git a/hott/algebra/ordered_ring.hlean b/hott/algebra/ordered_ring.hlean index 97df60603..e9a24182d 100644 --- a/hott/algebra/ordered_ring.hlean +++ b/hott/algebra/ordered_ring.hlean @@ -339,8 +339,8 @@ section (assume H : a ≥ 0, mul_nonneg H H) (assume H : a ≤ 0, mul_nonneg_of_nonpos_of_nonpos H H) - definition zero_le_one : 0 ≤ 1 := one_mul 1 ▸ mul_self_nonneg (1 : A) - definition zero_lt_one : 0 < 1 := lt_of_le_of_ne zero_le_one zero_ne_one + definition zero_le_one : 0 ≤ (1:A) := one_mul 1 ▸ mul_self_nonneg (1 : A) + definition zero_lt_one : 0 < (1:A) := lt_of_le_of_ne zero_le_one zero_ne_one definition pos_and_pos_or_neg_and_neg_of_mul_pos {a b : A} (Hab : a * b > 0) : (a > 0 × b > 0) ⊎ (a < 0 × b < 0) := @@ -400,13 +400,13 @@ section definition sign_of_neg (H : a < 0) : sign a = -1 := lt.cases_of_lt H - definition sign_zero : sign 0 = 0 := lt.cases_of_eq rfl + definition sign_zero : sign 0 = (0:A) := lt.cases_of_eq rfl definition sign_of_pos (H : a > 0) : sign a = 1 := lt.cases_of_gt H - definition sign_one : sign 1 = 1 := sign_of_pos zero_lt_one + definition sign_one : sign 1 = (1:A) := sign_of_pos zero_lt_one - definition sign_neg_one : sign (-1) = -1 := sign_of_neg (neg_neg_of_pos zero_lt_one) + definition sign_neg_one : sign (-1) = -(1:A) := sign_of_neg (neg_neg_of_pos zero_lt_one) definition sign_sign (a : A) : sign (sign a) = sign a := lt.by_cases @@ -454,7 +454,7 @@ section have H2 : -1 = 1, from H⁻¹ ⬝ (sign_of_pos H1), absurd ((eq_zero_of_neg_eq H2)⁻¹) zero_ne_one) (assume H1 : 0 = a, - have H2 : 0 = -1, + have H2 : (0:A) = -1, begin rewrite [-H1 at H, sign_zero at H], exact H diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean index b0bbeb352..d42e95de2 100644 --- a/hott/algebra/ring.hlean +++ b/hott/algebra/ring.hlean @@ -230,7 +230,7 @@ section ... = 0 : mul_zero, inverse (neg_eq_of_add_eq_zero H) - definition mul_ne_zero_imp_ne_zero {a b} (H : a * b ≠ 0) : a ≠ 0 × b ≠ 0 := + definition mul_ne_zero_imp_ne_zero {a b : A} (H : a * b ≠ 0) : a ≠ 0 × b ≠ 0 := have Ha : a ≠ 0, from (assume Ha1 : a = 0, have H1 : a * b = 0, by rewrite [Ha1, zero_mul], diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean index 878d1906c..1fb74a09f 100644 --- a/hott/hit/trunc.hlean +++ b/hott/hit/trunc.hlean @@ -47,7 +47,7 @@ namespace trunc equiv.mk tr _ definition is_trunc_of_is_equiv_tr [H : is_equiv (@tr n A)] : is_trunc n A := - is_trunc_is_equiv_closed n tr⁻¹ + is_trunc_is_equiv_closed n (@tr n _)⁻¹ definition untrunc_of_is_trunc [reducible] [H : is_trunc n A] : trunc n A → A := tr⁻¹ diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index c50fccc9d..aed2539a7 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -233,7 +233,7 @@ namespace is_trunc definition is_trunc_is_equiv_closed (n : trunc_index) (f : A → B) [H : is_equiv f] [HA : is_trunc n A] : is_trunc n B := trunc_index.rec_on n - (λA (HA : is_contr A) B f (H : is_equiv f), !is_contr_is_equiv_closed) + (λA (HA : is_contr A) B f (H : is_equiv f), is_contr_is_equiv_closed f) (λn IH A (HA : is_trunc n.+1 A) B f (H : is_equiv f), @is_trunc_succ_intro _ _ (λ x y : B, IH (f⁻¹ x = f⁻¹ y) _ (x = y) (ap f⁻¹)⁻¹ !is_equiv_inv)) A HA B f H diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index a12886907..44b326e6e 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -134,7 +134,7 @@ namespace eq definition equiv_ap (f : A → B) [H : is_equiv f] (a1 a2 : A) : (a1 = a2) ≃ (f a1 = f a2) := - equiv.mk _ _ + equiv.mk (ap f) _ /- Path operations are equivalences -/ diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean index 8775ebbb3..c165a8a67 100644 --- a/library/algebra/category/basic.lean +++ b/library/algebra/category/basic.lean @@ -23,7 +23,7 @@ namespace category variables {a b c d : ob} include C - definition compose := comp + definition compose := @comp ob _ definition id [reducible] {a : ob} : hom a a := ID a diff --git a/library/algebra/category/functor.lean b/library/algebra/category/functor.lean index 43ef2cc09..8d53e2c40 100644 --- a/library/algebra/category/functor.lean +++ b/library/algebra/category/functor.lean @@ -47,11 +47,11 @@ namespace functor protected definition id [reducible] {C : Category} : functor C C := mk (λa, a) (λ a b f, f) (λ a, rfl) (λ a b c f g, rfl) - protected definition ID [reducible] (C : Category) : functor C C := id + protected definition ID [reducible] (C : Category) : functor C C := @id C - protected theorem id_left (F : functor C D) : id ∘f F = F := + protected theorem id_left (F : functor C D) : (@id D) ∘f F = F := functor.rec (λ obF homF idF compF, dcongr_arg4 mk rfl rfl !proof_irrel !proof_irrel) F - protected theorem id_right (F : functor C D) : F ∘f id = F := + protected theorem id_right (F : functor C D) : F ∘f (@id C) = F := functor.rec (λ obF homF idF compF, dcongr_arg4 mk rfl rfl !proof_irrel !proof_irrel) F end functor diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean index bd51703e8..a1f8616a3 100644 --- a/library/algebra/category/morphism.lean +++ b/library/algebra/category/morphism.lean @@ -137,7 +137,8 @@ namespace morphism theorem refl (a : ob) : a ≅ a := mk id theorem symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a := mk (inverse (iso H)) theorem trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c := mk (iso H2 ∘ iso H1) - theorem is_equivalence_eq [instance] (T : Type) : is_equivalence isomorphic := + + theorem is_equivalence_eq [instance] (T : Type) : is_equivalence (isomorphic : ob → ob → Type) := is_equivalence.mk refl symm trans end isomorphic @@ -160,7 +161,7 @@ namespace morphism is_mono.mk (λ c g h H, calc g = id ∘ g : by rewrite id_left - ... = (retraction_of f ∘ f) ∘ g : by rewrite -retraction_compose + ... = (retraction_of f ∘ f) ∘ g : by rewrite -(retraction_compose f) ... = (retraction_of f ∘ f) ∘ h : by rewrite [-assoc, H, -assoc] ... = id ∘ h : by rewrite retraction_compose ... = h : by rewrite id_left) @@ -169,7 +170,7 @@ namespace morphism is_epi.mk (λ c g h H, calc g = g ∘ id : by rewrite id_right - ... = g ∘ f ∘ section_of f : by rewrite -compose_section + ... = g ∘ f ∘ section_of f : by rewrite -(compose_section f) ... = h ∘ f ∘ section_of f : by rewrite [assoc, H, -assoc] ... = h ∘ id : by rewrite compose_section ... = h : by rewrite id_right) diff --git a/library/algebra/category/natural_transformation.lean b/library/algebra/category/natural_transformation.lean index 7610c2722..e47c65b2f 100644 --- a/library/algebra/category/natural_transformation.lean +++ b/library/algebra/category/natural_transformation.lean @@ -43,11 +43,11 @@ namespace natural_transformation protected definition id {C D : Category} {F : functor C D} : natural_transformation F F := mk (λa, id) (λa b f, !id_right ⬝ symm !id_left) - protected definition ID {C D : Category} (F : functor C D) : natural_transformation F F := id + protected definition ID {C D : Category} (F : functor C D) : natural_transformation F F := natural_transformation.id - protected theorem id_left (η : F ⟹ G) : natural_transformation.compose id η = η := + protected theorem id_left (η : F ⟹ G) : natural_transformation.compose natural_transformation.id η = η := natural_transformation.rec (λf H, dcongr_arg2 mk (funext (take x, !id_left)) !proof_irrel) η - protected theorem id_right (η : F ⟹ G) : natural_transformation.compose η id = η := + protected theorem id_right (η : F ⟹ G) : natural_transformation.compose η natural_transformation.id = η := natural_transformation.rec (λf H, dcongr_arg2 mk (funext (take x, !id_right)) !proof_irrel) η end natural_transformation diff --git a/library/algebra/field.lean b/library/algebra/field.lean index ff2fe0ba9..87a1bd26d 100644 --- a/library/algebra/field.lean +++ b/library/algebra/field.lean @@ -64,21 +64,21 @@ section division_ring theorem div_self (H : a ≠ 0) : a / a = 1 := mul_inv_cancel H - theorem one_div_one : 1 / 1 = 1 := div_self (ne.symm zero_ne_one) + theorem one_div_one : 1 / 1 = (1:A) := div_self (ne.symm zero_ne_one) theorem mul_div_assoc : (a * b) / c = a * (b / c) := !mul.assoc theorem one_div_ne_zero (H : a ≠ 0) : 1 / a ≠ 0 := assume H2 : 1 / a = 0, - have C1 : 0 = 1, from symm (by rewrite [-(mul_one_div_cancel H), H2, mul_zero]), + have C1 : 0 = (1:A), from symm (by rewrite [-(mul_one_div_cancel H), H2, mul_zero]), absurd C1 zero_ne_one -- theorem ne_zero_of_one_div_ne_zero (H : 1 / a ≠ 0) : a ≠ 0 := -- assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H -- the analogue in group is called inv_one - theorem inv_one_is_one : 1⁻¹ = 1 := - by rewrite [-mul_one, (inv_mul_cancel (ne.symm zero_ne_one))] + theorem inv_one_is_one : 1⁻¹ = (1:A) := + by rewrite [-mul_one, inv_mul_cancel (ne.symm (@zero_ne_one A _))] theorem div_one : a / 1 = a := by rewrite [↑divide, inv_one_is_one, mul_one] @@ -99,8 +99,8 @@ section division_ring -- make "left" and "right" versions? theorem eq_one_div_of_mul_eq_one (H : a * b = 1) : b = 1 / a := have H2 : a ≠ 0, from - (assume A : a = 0, - have B : 0 = 1, by rewrite [-(zero_mul b), -A, H], + (assume aeq0 : a = 0, + have B : 0 = (1:A), by rewrite [-(zero_mul b), -aeq0, H], absurd B zero_ne_one), show b = 1 / a, from symm (calc 1 / a = (1 / a) * 1 : mul_one @@ -130,8 +130,8 @@ section division_ring rewrite [mul.assoc, -(mul.assoc a), (mul_one_div_cancel Ha), one_mul, (mul_one_div_cancel Hb)], eq_one_div_of_mul_eq_one H - theorem one_div_neg_one_eq_neg_one : 1 / (-1) = -1 := - have H : (-1) * (-1) = 1, by rewrite [-neg_eq_neg_one_mul, neg_neg], + theorem one_div_neg_one_eq_neg_one : (1:A) / (-1) = -1 := + have H : (-1) * (-1) = (1:A), by rewrite [-neg_eq_neg_one_mul, neg_neg], symm (eq_one_div_of_mul_eq_one H) theorem one_div_neg_eq_neg_one_div (H : a ≠ 0) : 1 / (- a) = - (1 / a) := @@ -139,7 +139,7 @@ section division_ring (assume H2 : -1 = 0, absurd (symm (calc 1 = -(-1) : neg_neg ... = -0 : H2 - ... = 0 : neg_zero)) zero_ne_one), + ... = (0:A) : neg_zero)) zero_ne_one), calc 1 / (- a) = 1 / ((-1) * a) : neg_eq_neg_one_mul ... = (1 / a) * (1 / (- 1)) : one_div_mul_one_div H H1 @@ -336,9 +336,9 @@ section discrete_field ⦃ integral_domain, s, eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero⦄ - theorem inv_zero : 0⁻¹ = 0 := !discrete_field.inv_zero + theorem inv_zero : 0⁻¹ = (0:A) := !discrete_field.inv_zero - theorem one_div_zero : 1 / 0 = 0 := + theorem one_div_zero : 1 / 0 = (0:A) := calc 1 / 0 = 1 * 0⁻¹ : refl ... = 1 * 0 : discrete_field.inv_zero A diff --git a/library/algebra/group.lean b/library/algebra/group.lean index 7156af8a5..3551479a7 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -174,7 +174,7 @@ section group theorem inv_eq_of_mul_eq_one {a b : A} (H : a * b = 1) : a⁻¹ = b := by rewrite [-mul_one a⁻¹, -H, inv_mul_cancel_left] - theorem inv_one : 1⁻¹ = 1 := inv_eq_of_mul_eq_one (one_mul 1) + theorem inv_one : 1⁻¹ = (1 : A) := inv_eq_of_mul_eq_one (one_mul 1) theorem inv_inv (a : A) : (a⁻¹)⁻¹ = a := inv_eq_of_mul_eq_one (mul.left_inv a) @@ -292,7 +292,7 @@ section add_group theorem neg_eq_of_add_eq_zero {a b : A} (H : a + b = 0) : -a = b := by rewrite [-add_zero, -H, neg_add_cancel_left] - theorem neg_zero : -0 = 0 := neg_eq_of_add_eq_zero (zero_add 0) + theorem neg_zero : -0 = (0 : A) := neg_eq_of_add_eq_zero (zero_add 0) theorem neg_neg (a : A) : -(-a) = a := neg_eq_of_add_eq_zero (add.left_inv a) diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean index 4ece384a4..456cf0259 100644 --- a/library/algebra/group_bigops.lean +++ b/library/algebra/group_bigops.lean @@ -62,7 +62,7 @@ section monoid by rewrite [union_eq_append d, Prodl_append] end deceqA - theorem Prodl_one : ∀(l : list A), Prodl l (λ x, 1) = 1 + theorem Prodl_one : ∀(l : list A), Prodl l (λ x, 1) = (1:B) | [] := rfl | (a::l) := by rewrite [Prodl_cons, Prodl_one, mul_one] end monoid @@ -139,7 +139,7 @@ section comm_monoid by rewrite [Prod_insert_of_not_mem f H1, Prod_insert_of_not_mem g H1, IH H3, H4]) end deceqA - theorem Prod_one (s : finset A) : Prod s (λ x, 1) = 1 := + theorem Prod_one (s : finset A) : Prod s (λ x, 1) = (1:B) := quot.induction_on s (take u, !Prodl_one) end comm_monoid @@ -169,7 +169,7 @@ section add_monoid Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := Prodl_union f d end deceqA - theorem Suml_zero (l : list A) : Suml l (λ x, 0) = 0 := Prodl_one l + theorem Suml_zero (l : list A) : Suml l (λ x, 0) = (0:B) := Prodl_one l end add_monoid section add_comm_monoid @@ -209,7 +209,7 @@ section add_comm_monoid Sum s f = Sum s g := Prod_ext H end deceqA - theorem Sum_zero (s : finset A) : Sum s (λ x, 0) = 0 := Prod_one s + theorem Sum_zero (s : finset A) : Sum s (λ x, 0) = (0:B) := Prod_one s end add_comm_monoid end algebra diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean index 5915e4e68..3e670ddb0 100644 --- a/library/algebra/group_power.lean +++ b/library/algebra/group_power.lean @@ -37,7 +37,7 @@ theorem pow_succ' (a : A) : ∀n, a^(succ n) = a * a^n | 0 := by rewrite [pow_succ, *pow_zero, one_mul, mul_one] | (succ n) := by rewrite [pow_succ, pow_succ' at {1}, pow_succ, mul.assoc] -theorem one_pow : ∀ n : ℕ, 1^n = 1 +theorem one_pow : ∀ n : ℕ, 1^n = (1:A) | 0 := rfl | (succ n) := by rewrite [pow_succ, mul_one, one_pow] diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index 447d014fd..015dc583c 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -424,7 +424,7 @@ section theorem abs_of_neg (H : a < 0) : abs a = -a := if_neg (not_le_of_lt H) - theorem abs_zero : abs 0 = 0 := abs_of_nonneg (le.refl _) + theorem abs_zero : abs 0 = (0:A) := abs_of_nonneg (le.refl _) theorem abs_of_nonpos (H : a ≤ 0) : abs a = -a := decidable.by_cases diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index 711b147da..a0e1cc12a 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -337,8 +337,8 @@ section (assume H : a ≥ 0, mul_nonneg H H) (assume H : a ≤ 0, mul_nonneg_of_nonpos_of_nonpos H H) - theorem zero_le_one : 0 ≤ 1 := one_mul 1 ▸ mul_self_nonneg 1 - theorem zero_lt_one : 0 < 1 := lt_of_le_of_ne zero_le_one zero_ne_one + theorem zero_le_one : 0 ≤ (1:A) := one_mul 1 ▸ mul_self_nonneg 1 + theorem zero_lt_one : 0 < (1:A) := lt_of_le_of_ne zero_le_one zero_ne_one theorem pos_and_pos_or_neg_and_neg_of_mul_pos {a b : A} (Hab : a * b > 0) : (a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) := @@ -369,7 +369,7 @@ section end) (assume Hb : b < 0, or.inr (and.intro Ha Hb))) - theorem gt_of_mul_lt_mul_neg_left {a b c} (H : c * a < c * b) (Hc : c ≤ 0) : a > b := + theorem gt_of_mul_lt_mul_neg_left {a b c : A} (H : c * a < c * b) (Hc : c ≤ 0) : a > b := have nhc : -c ≥ 0, from neg_nonneg_of_nonpos Hc, have H2 : -(c * b) < -(c * a), from iff.mp' (neg_lt_neg_iff_lt _ _) H, have H3 : (-c) * b < (-c) * a, from calc @@ -378,7 +378,7 @@ section ... = (-c) * a : neg_mul_eq_neg_mul, lt_of_mul_lt_mul_left H3 nhc - theorem zero_gt_neg_one : -1 < 0 := + theorem zero_gt_neg_one : -1 < (0:A) := neg_zero ▸ (neg_lt_neg zero_lt_one) end @@ -398,13 +398,13 @@ section theorem sign_of_neg (H : a < 0) : sign a = -1 := lt.cases_of_lt H - theorem sign_zero : sign 0 = 0 := lt.cases_of_eq rfl + theorem sign_zero : sign 0 = (0:A) := lt.cases_of_eq rfl theorem sign_of_pos (H : a > 0) : sign a = 1 := lt.cases_of_gt H - theorem sign_one : sign 1 = 1 := sign_of_pos zero_lt_one + theorem sign_one : sign 1 = (1:A) := sign_of_pos zero_lt_one - theorem sign_neg_one : sign (-1) = -1 := sign_of_neg (neg_neg_of_pos zero_lt_one) + theorem sign_neg_one : sign (-1) = -(1:A) := sign_of_neg (neg_neg_of_pos zero_lt_one) theorem sign_sign (a : A) : sign (sign a) = sign a := lt.by_cases @@ -452,7 +452,7 @@ section have H2 : -1 = 1, from H⁻¹ ⬝ (sign_of_pos H1), absurd ((eq_zero_of_neg_eq H2)⁻¹) zero_ne_one) (assume H1 : 0 = a, - have H2 : 0 = -1, + have H2 : (0:A) = -1, begin rewrite [-H1 at H, sign_zero at H], exact H diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 2c1569b0e..5988b972e 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -39,7 +39,7 @@ theorem mul_zero [s : mul_zero_class A] (a : A) : a * 0 = 0 := !mul_zero_class.m structure zero_ne_one_class [class] (A : Type) extends has_zero A, has_one A := (zero_ne_one : zero ≠ one) -theorem zero_ne_one [s: zero_ne_one_class A] : 0 ≠ 1 := @zero_ne_one_class.zero_ne_one A s +theorem zero_ne_one [s: zero_ne_one_class A] : 0 ≠ (1:A) := @zero_ne_one_class.zero_ne_one A s /- semiring -/ @@ -229,7 +229,7 @@ section ... = 0 : mul_zero, symm (neg_eq_of_add_eq_zero H) - theorem mul_ne_zero_imp_ne_zero {a b} (H : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 := + theorem mul_ne_zero_imp_ne_zero {a b : A} (H : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 := have Ha : a ≠ 0, from (assume Ha1 : a = 0, have H1 : a * b = 0, by rewrite [Ha1, zero_mul], diff --git a/library/data/finset/bigops.lean b/library/data/finset/bigops.lean index f31a8aed4..60f84051b 100644 --- a/library/data/finset/bigops.lean +++ b/library/data/finset/bigops.lean @@ -54,7 +54,7 @@ section deceqA Unionl (list.insert a l) f = f a ∪ Unionl l f := algebra.Prodl_insert_of_not_mem f H theorem Unionl_union {l₁ l₂ : list A} (f : A → finset B) (d : list.disjoint l₁ l₂) : Unionl (list.union l₁ l₂) f = Unionl l₁ f ∪ Unionl l₂ f := algebra.Prodl_union f d - theorem Unionl_empty (l : list A) : Unionl l (λ x, ∅) = ∅ := algebra.Prodl_one l + theorem Unionl_empty (l : list A) : Unionl l (λ x, ∅) = (∅ : finset B) := algebra.Prodl_one l end deceqA theorem Union_empty (f : A → finset B) : Union ∅ f = ∅ := algebra.Prod_empty f @@ -70,7 +70,7 @@ section deceqA Union (s₁ ∪ s₂) f = Union s₁ f ∪ Union s₂ f := algebra.Prod_union f disj theorem Union_ext {s : finset A} {f g : A → finset B} (H : ∀x, x ∈ s → f x = g x) : Union s f = Union s g := algebra.Prod_ext H - theorem Union_empty' (s : finset A) : Union s (λ x, ∅) = ∅ := algebra.Prod_one s + theorem Union_empty' (s : finset A) : Union s (λ x, ∅) = (∅ : finset B) := algebra.Prod_one s -- this will eventually be an instance of something more general theorem inter_Union (s : finset B) (t : finset A) (f : A → finset B) : diff --git a/library/data/finset/card.lean b/library/data/finset/card.lean index d15fa659e..70ba4cc0e 100644 --- a/library/data/finset/card.lean +++ b/library/data/finset/card.lean @@ -120,8 +120,8 @@ finset.induction_on s H1 !mem_insert (!mem_insert_of_mem xs') anex, assert H8 : f a ∩ (⋃ (x : A) ∈ s', f x) = ∅, from calc - f a ∩ (⋃ (x : A) ∈ s', f x) = (⋃ (x : A) ∈ s', f a ∩ f x) : inter_Union - ... = (⋃ (x : A) ∈ s', ∅) : Union_ext H7 + f a ∩ (⋃ (x : A) ∈ s', f x) = (⋃ (x : A) ∈ s', f a ∩ f x) : inter_Union + ... = (⋃ (x : A) ∈ s', ∅) : Union_ext H7 ... = ∅ : Union_empty', by rewrite [Union_insert_of_not_mem _ H, Sum_insert_of_not_mem _ H, card_union_of_disjoint H8, H6]) diff --git a/library/data/finset/to_set.lean b/library/data/finset/to_set.lean index cd181167a..1bb93061f 100644 --- a/library/data/finset/to_set.lean +++ b/library/data/finset/to_set.lean @@ -15,18 +15,18 @@ variable [deceq : decidable_eq A] include deceq definition to_set (s : finset A) : set A := λx, x ∈ s -abbreviation ts := to_set -- until coercion is working +abbreviation ts := @to_set A _ -- until coercion is working variables (s t : finset A) (x : A) /- operations -/ theorem mem_to_set_empty : (x ∈ ts ∅) = (x ∈ ∅) := rfl -theorem to_set_empty : ts ∅ = ∅ := rfl +theorem to_set_empty : ts ∅ = (∅ : set A) := rfl theorem mem_to_set_univ [h : fintype A] : (x ∈ ts univ) = (x ∈ set.univ) := propext (iff.intro (assume H, trivial) (assume H, !mem_univ)) -theorem to_set_univ [h : fintype A] : ts univ = set.univ := funext (λ x, !mem_to_set_univ) +theorem to_set_univ [h : fintype A] : ts univ = (set.univ : set A) := funext (λ x, !mem_to_set_univ) theorem mem_to_set_union : (x ∈ ts (s ∪ t)) = (x ∈ ts s ∪ ts t) := !finset.mem_union_eq theorem to_set_union : ts (s ∪ t) = ts s ∪ ts t := funext (λ x, !mem_to_set_union) @@ -51,7 +51,7 @@ theorem to_set_image {B : Type} [h : decidable_eq B] (f : A → B) (s : finset A theorem mem_eq_mem_to_set : (x ∈ s) = (x ∈ ts s) := rfl -definition decidable_mem_to_set [instance] (x s) : decidable (x ∈ ts s) := +definition decidable_mem_to_set [instance] (x : A) (s : finset A) : decidable (x ∈ ts s) := decidable_of_decidable_of_eq _ !mem_eq_mem_to_set theorem eq_eq_to_set_eq : (s = t) = (ts s = ts t) := diff --git a/library/data/list/set.lean b/library/data/list/set.lean index 8d9211b7f..55d265162 100644 --- a/library/data/list/set.lean +++ b/library/data/list/set.lean @@ -325,7 +325,7 @@ definition erase_dup [H : decidable_eq A] : list A → list A | [] := [] | (x :: xs) := if x ∈ xs then erase_dup xs else x :: erase_dup xs -theorem erase_dup_nil [H : decidable_eq A] : erase_dup [] = [] +theorem erase_dup_nil [H : decidable_eq A] : erase_dup [] = ([] : list A) theorem erase_dup_cons_of_mem [H : decidable_eq A] {a : A} {l : list A} : a ∈ l → erase_dup (a::l) = erase_dup l := assume ainl, calc diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index c1be0c315..5698d8de1 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -2198,7 +2198,7 @@ struct unifier_fn { constraint c = p->first; unsigned cidx = p->second; if (cidx >= get_group_first_index(cnstr_group::ClassInstance) && - !m_config.m_discard && is_choice_cnstr(c) && cnstr_on_demand(c)) { + is_choice_cnstr(c) && cnstr_on_demand(c)) { // we postpone class-instance constraints whose type still contains metavariables m_cnstrs.erase_min(); postpone(c); diff --git a/tests/lean/const.lean b/tests/lean/const.lean index 98d844398..56057e2fe 100644 --- a/tests/lean/const.lean +++ b/tests/lean/const.lean @@ -11,7 +11,7 @@ set_option pp.implicit true section variable A : Type variable S : inhabited A - variable B : bla + variable B : @bla A _ check B check @foo A _ end diff --git a/tests/lean/run/alg_rw.lean b/tests/lean/run/alg_rw.lean index d911b3e61..0267f3071 100644 --- a/tests/lean/run/alg_rw.lean +++ b/tests/lean/run/alg_rw.lean @@ -6,7 +6,7 @@ section variable [s : comm_monoid A] include s - theorem one_mul_one : 1 * 1 = 1 := + theorem one_mul_one : 1 * 1 = (1:A) := mul_one 1 end diff --git a/tests/lean/run/dec_trivial_loop.lean b/tests/lean/run/dec_trivial_loop.lean new file mode 100644 index 000000000..741716a73 --- /dev/null +++ b/tests/lean/run/dec_trivial_loop.lean @@ -0,0 +1,2 @@ +check @dec_trivial +print dec_trivial diff --git a/tests/lean/run/finset.lean b/tests/lean/run/finset.lean index 9e9f051fe..c2f9e74ae 100644 --- a/tests/lean/run/finset.lean +++ b/tests/lean/run/finset.lean @@ -186,7 +186,7 @@ namespace finset theorem eq_clean {A : Type} [H : decidable_eq A] : ∀ s : finset A, clean s = s := take s, quot.induction_on s (λ l, eq.symm (quot.sound (eqv_norep l))) - theorem eq_of_clean_eq_clean {A : Type} [H : decidable_eq A] : ∀ s₁ s₂, clean s₁ = clean s₂ → s₁ = s₂ := + theorem eq_of_clean_eq_clean {A : Type} [H : decidable_eq A] : ∀ s₁ s₂ : finset A, clean s₁ = clean s₂ → s₁ = s₂ := take s₁ s₂, by rewrite *eq_clean; intro H; apply H example : to_finset [(1:nat), 1, 2, 3] = to_finset [1, 2, 2, 2, 3, 3] := diff --git a/tests/lean/run/num_bug2.lean b/tests/lean/run/num_bug2.lean index b59f2157f..b9c53b3aa 100644 --- a/tests/lean/run/num_bug2.lean +++ b/tests/lean/run/num_bug2.lean @@ -3,8 +3,8 @@ open algebra variable A : Type variable s : ring A -variable H0 : 0 = 0 -- since algebra defines notation '0' it should have precedence over num -variable H1 : 1 = 1 -- since algebra defines notation '1' it should have precedence over num +variable H0 : 0 = (0:A) -- since algebra defines notation '0' it should have precedence over num +variable H1 : 1 = (1:A) -- since algebra defines notation '1' it should have precedence over num example : has_zero.zero A = has_zero.zero A := H0 diff --git a/tests/lean/run/rewriter2.lean b/tests/lean/run/rewriter2.lean index 8ff802d00..2ab8b6cec 100644 --- a/tests/lean/run/rewriter2.lean +++ b/tests/lean/run/rewriter2.lean @@ -13,7 +13,7 @@ check @mul_zero axiom Ax {A : Type} [s₁ : has_mul A] [s₂ : has_zero A] (a : A) : f (a * 0) (a * 0) = 0 -theorem test2 {A : Type} [s : comm_ring A] (a b c : A) : f 0 0 = 0 := +theorem test2 {A : Type} [s : comm_ring A] (a b c : A) : f 0 0 = (0:A) := begin rewrite [ -(mul_zero a) at {1, 2}, -- - means apply symmetry, rewrite 0 ==> a * 0 at 1st and 2nd occurrences