From 22814d086e1a49ed5523993218a02158861f081b Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 24 Sep 2019 13:35:05 -0400 Subject: [PATCH] cleanup(*): use priority 10 for low priority Now we can locally use priorities lower than this low-priority --- src/analysis/calculus/deriv.lean | 2 +- src/analysis/calculus/times_cont_diff.lean | 2 +- src/category/bifunctor.lean | 4 ++-- src/category/bitraversable/instances.lean | 4 ++-- src/category_theory/adjunction/basic.lean | 8 ++++---- src/computability/primrec.lean | 2 +- src/data/fintype.lean | 4 ++-- src/data/int/basic.lean | 2 +- src/data/nat/cast.lean | 2 +- src/data/num/basic.lean | 6 +++--- src/data/rat/cast.lean | 2 +- src/field_theory/splitting_field.lean | 2 +- src/group_theory/sylow.lean | 2 +- src/linear_algebra/finsupp.lean | 2 +- src/logic/basic.lean | 2 +- src/logic/function.lean | 4 ++-- src/tactic/finish.lean | 18 +++++++++--------- src/tactic/localized.lean | 2 +- src/tactic/push_neg.lean | 2 +- src/topology/algebra/uniform_group.lean | 2 +- .../metric_space/gromov_hausdorff.lean | 6 +++--- .../gromov_hausdorff_realized.lean | 2 +- .../uniform_space/abstract_completion.lean | 2 +- 23 files changed, 42 insertions(+), 42 deletions(-) diff --git a/src/analysis/calculus/deriv.lean b/src/analysis/calculus/deriv.lean index b80f0e421b51d..b74e551d97f8a 100644 --- a/src/analysis/calculus/deriv.lean +++ b/src/analysis/calculus/deriv.lean @@ -53,7 +53,7 @@ import analysis.asymptotics analysis.calculus.tangent_cone open filter asymptotics continuous_linear_map set noncomputable theory -local attribute [instance, priority 0] classical.decidable_inhabited classical.prop_decidable +local attribute [instance, priority 10] classical.decidable_inhabited classical.prop_decidable set_option class.instance_max_depth 90 diff --git a/src/analysis/calculus/times_cont_diff.lean b/src/analysis/calculus/times_cont_diff.lean index 262884527030c..c445560bbd411 100644 --- a/src/analysis/calculus/times_cont_diff.lean +++ b/src/analysis/calculus/times_cont_diff.lean @@ -66,7 +66,7 @@ derivative, differentiability, higher derivative, C^n -/ noncomputable theory -local attribute [instance, priority 0] classical.decidable_inhabited classical.prop_decidable +local attribute [instance, priority 10] classical.decidable_inhabited classical.prop_decidable universes u v w diff --git a/src/category/bifunctor.lean b/src/category/bifunctor.lean index 26ac2b1ab0432..91e103616b982 100644 --- a/src/category/bifunctor.lean +++ b/src/category/bifunctor.lean @@ -108,11 +108,11 @@ by refine { .. }; intros; cases x; refl open bifunctor functor -@[priority 0] +@[priority 10] instance bifunctor.functor {α} : functor (F α) := { map := λ _ _, snd } -@[priority 0] +@[priority 10] instance bifunctor.is_lawful_functor [is_lawful_bifunctor F] {α} : is_lawful_functor (F α) := by refine {..}; intros; simp [functor.map] with functor_norm diff --git a/src/category/bitraversable/instances.lean b/src/category/bitraversable/instances.lean index 8eaad1beedce8..cafd51e404401 100644 --- a/src/category/bitraversable/instances.lean +++ b/src/category/bitraversable/instances.lean @@ -83,11 +83,11 @@ by constructor; introsI; casesm is_lawful_bitraversable t; apply_assumption open bitraversable functor -@[priority 0] +@[priority 10] instance bitraversable.traversable {α} : traversable (t α) := { traverse := @tsnd t _ _ } -@[priority 0] +@[priority 10] instance bitraversable.is_lawful_traversable [is_lawful_bitraversable t] {α} : is_lawful_traversable (t α) := by { constructor; introsI; simp [traverse,comp_tsnd] with functor_norm, diff --git a/src/category_theory/adjunction/basic.lean b/src/category_theory/adjunction/basic.lean index 09ca83c9912a3..f9cbc17a12c78 100644 --- a/src/category_theory/adjunction/basic.lean +++ b/src/category_theory/adjunction/basic.lean @@ -46,13 +46,13 @@ namespace adjunction restate_axiom hom_equiv_unit' restate_axiom hom_equiv_counit' -attribute [simp, priority 1] hom_equiv_unit hom_equiv_counit +attribute [simp, priority 10] hom_equiv_unit hom_equiv_counit section variables {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) {X' X : C} {Y Y' : D} -@[simp, priority 1] lemma hom_equiv_naturality_left_symm (f : X' ⟶ X) (g : X ⟶ G.obj Y) : +@[simp, priority 10] lemma hom_equiv_naturality_left_symm (f : X' ⟶ X) (g : X ⟶ G.obj Y) : (adj.hom_equiv X' Y).symm (f ≫ g) = F.map f ≫ (adj.hom_equiv X Y).symm g := by rw [hom_equiv_counit, F.map_comp, assoc, adj.hom_equiv_counit.symm] @@ -60,7 +60,7 @@ by rw [hom_equiv_counit, F.map_comp, assoc, adj.hom_equiv_counit.symm] (adj.hom_equiv X' Y) (F.map f ≫ g) = f ≫ (adj.hom_equiv X Y) g := by rw [← equiv.eq_symm_apply]; simp [-hom_equiv_unit] -@[simp, priority 1] lemma hom_equiv_naturality_right (f : F.obj X ⟶ Y) (g : Y ⟶ Y') : +@[simp, priority 10] lemma hom_equiv_naturality_right (f : F.obj X ⟶ Y) (g : Y ⟶ Y') : (adj.hom_equiv X Y') (f ≫ g) = (adj.hom_equiv X Y) f ≫ G.map g := by rw [hom_equiv_unit, G.map_comp, ← assoc, ←hom_equiv_unit] @@ -117,7 +117,7 @@ namespace core_hom_equiv restate_axiom hom_equiv_naturality_left_symm' restate_axiom hom_equiv_naturality_right' -attribute [simp, priority 1] hom_equiv_naturality_left_symm hom_equiv_naturality_right +attribute [simp, priority 10] hom_equiv_naturality_left_symm hom_equiv_naturality_right variables {F : C ⥤ D} {G : D ⥤ C} (adj : core_hom_equiv F G) {X' X : C} {Y Y' : D} diff --git a/src/computability/primrec.lean b/src/computability/primrec.lean index 180b2306ca1c2..d0df374ff836c 100644 --- a/src/computability/primrec.lean +++ b/src/computability/primrec.lean @@ -108,7 +108,7 @@ class primcodable (α : Type*) extends encodable α := namespace primcodable open nat.primrec -@[priority 0] instance of_denumerable (α) [denumerable α] : primcodable α := +@[priority 10] instance of_denumerable (α) [denumerable α] : primcodable α := ⟨succ.of_eq $ by simp⟩ def of_equiv (α) {β} [primcodable α] (e : β ≃ α) : primcodable β := diff --git a/src/data/fintype.lean b/src/data/fintype.lean index a79ef68cade1b..f0a3a529b7a9e 100644 --- a/src/data/fintype.lean +++ b/src/data/fintype.lean @@ -196,7 +196,7 @@ instance (n : ℕ) : fintype (fin n) := @[simp] theorem fintype.card_fin (n : ℕ) : fintype.card (fin n) = n := by rw [fin.fintype]; simp [fintype.card, card, univ] -@[instance, priority 0] def unique.fintype {α : Type*} [unique α] : fintype α := +@[instance, priority 10] def unique.fintype {α : Type*} [unique α] : fintype α := ⟨finset.singleton (default α), λ x, by rw [unique.eq_default x]; simp⟩ @[simp] lemma univ_unique {α : Type*} [unique α] [f : fintype α] : @finset.univ α _ = {default α} := @@ -712,7 +712,7 @@ subrelation.wf this (measure_wf _) lemma preorder.well_founded [fintype α] [preorder α] : well_founded ((<) : α → α → Prop) := well_founded_of_trans_of_irrefl _ -@[instance, priority 0] lemma linear_order.is_well_order [fintype α] [linear_order α] : +@[instance, priority 10] lemma linear_order.is_well_order [fintype α] [linear_order α] : is_well_order α (<) := { wf := preorder.well_founded } diff --git a/src/data/int/basic.lean b/src/data/int/basic.lean index b5cf35e030209..b564c9cc9a1bf 100644 --- a/src/data/int/basic.lean +++ b/src/data/int/basic.lean @@ -1048,7 +1048,7 @@ protected def cast : ℤ → α | (n : ℕ) := n | -[1+ n] := -(n+1) -@[priority 0] instance cast_coe : has_coe ℤ α := ⟨int.cast⟩ +@[priority 10] instance cast_coe : has_coe ℤ α := ⟨int.cast⟩ @[simp, squash_cast] theorem cast_zero : ((0 : ℤ) : α) = 0 := rfl diff --git a/src/data/nat/cast.lean b/src/data/nat/cast.lean index 125471e87deda..43cbf99fe4c9e 100644 --- a/src/data/nat/cast.lean +++ b/src/data/nat/cast.lean @@ -19,7 +19,7 @@ protected def cast : ℕ → α | 0 := 0 | (n+1) := cast n + 1 -@[priority 0] instance cast_coe : has_coe ℕ α := ⟨nat.cast⟩ +@[priority 10] instance cast_coe : has_coe ℕ α := ⟨nat.cast⟩ @[simp, squash_cast] theorem cast_zero : ((0 : ℕ) : α) = 0 := rfl diff --git a/src/data/num/basic.lean b/src/data/num/basic.lean index d6f554625cec7..5716699b678e2 100644 --- a/src/data/num/basic.lean +++ b/src/data/num/basic.lean @@ -160,9 +160,9 @@ section | 0 := 0 | (num.pos p) := cast_pos_num p - @[priority 0] instance pos_num_coe : has_coe pos_num α := ⟨cast_pos_num⟩ + @[priority 10] instance pos_num_coe : has_coe pos_num α := ⟨cast_pos_num⟩ - @[priority 0] instance num_nat_coe : has_coe num α := ⟨cast_num⟩ + @[priority 10] instance num_nat_coe : has_coe num α := ⟨cast_num⟩ instance : has_repr pos_num := ⟨λ n, repr (n : ℕ)⟩ instance : has_repr num := ⟨λ n, repr (n : ℕ)⟩ @@ -504,7 +504,7 @@ section | (znum.pos p) := p | (znum.neg p) := -p - @[priority 0] instance znum_coe : has_coe znum α := ⟨cast_znum⟩ + @[priority 10] instance znum_coe : has_coe znum α := ⟨cast_znum⟩ instance : has_repr znum := ⟨λ n, repr (n : ℤ)⟩ end diff --git a/src/data/rat/cast.lean b/src/data/rat/cast.lean index 1dd61ea26144e..1a85c62966672 100644 --- a/src/data/rat/cast.lean +++ b/src/data/rat/cast.lean @@ -35,7 +35,7 @@ variable [division_ring α] protected def cast : ℚ → α | ⟨n, d, h, c⟩ := n / d -@[priority 0] instance cast_coe : has_coe ℚ α := ⟨rat.cast⟩ +@[priority 10] instance cast_coe : has_coe ℚ α := ⟨rat.cast⟩ @[simp] theorem cast_of_int (n : ℤ) : (of_int n : α) = n := show (n / (1:ℕ) : α) = n, by rw [nat.cast_one, div_one] diff --git a/src/field_theory/splitting_field.lean b/src/field_theory/splitting_field.lean index 22eb9184a4ef1..3ac6f08a3b05e 100644 --- a/src/field_theory/splitting_field.lean +++ b/src/field_theory/splitting_field.lean @@ -118,7 +118,7 @@ is_noetherian_ring.irreducible_induction_on (f.map i) section UFD -local attribute [instance, priority 0] principal_ideal_domain.to_unique_factorization_domain +local attribute [instance, priority 10] principal_ideal_domain.to_unique_factorization_domain local infix ` ~ᵤ ` : 50 := associated open unique_factorization_domain associates diff --git a/src/group_theory/sylow.lean b/src/group_theory/sylow.lean index 11fe8861fd530..277067ec433b7 100644 --- a/src/group_theory/sylow.lean +++ b/src/group_theory/sylow.lean @@ -11,7 +11,7 @@ open equiv.perm is_subgroup list quotient_group universes u v w variables {G : Type u} {α : Type v} {β : Type w} [group G] -local attribute [instance, priority 0] subtype.fintype set_fintype classical.prop_decidable +local attribute [instance, priority 10] subtype.fintype set_fintype classical.prop_decidable namespace mul_action variables [mul_action G α] diff --git a/src/linear_algebra/finsupp.lean b/src/linear_algebra/finsupp.lean index 7a9d78c3a5450..980ea54953d25 100644 --- a/src/linear_algebra/finsupp.lean +++ b/src/linear_algebra/finsupp.lean @@ -8,7 +8,7 @@ Linear structures on function with finite support `α →₀ β`. import data.finsupp linear_algebra.basic noncomputable theory -local attribute [instance, priority 0] classical.prop_decidable +local attribute [instance, priority 10] classical.prop_decidable open lattice set linear_map submodule diff --git a/src/logic/basic.lean b/src/logic/basic.lean index 0c9c9d46b5a64..8e822b2c41fd6 100644 --- a/src/logic/basic.lean +++ b/src/logic/basic.lean @@ -31,7 +31,7 @@ instance : subsingleton empty := ⟨λa, a.elim⟩ instance : decidable_eq empty := λa, a.elim -@[priority 0] instance decidable_eq_of_subsingleton +@[priority 10] instance decidable_eq_of_subsingleton {α} [subsingleton α] : decidable_eq α | a b := is_true (subsingleton.elim a b) diff --git a/src/logic/function.lean b/src/logic/function.lean index 45ebe404bd60c..f0535147c0258 100644 --- a/src/logic/function.lean +++ b/src/logic/function.lean @@ -94,7 +94,7 @@ theorem right_inverse.comp {γ} {f : α → β} {g : β → α} {h : β → γ} (hf : right_inverse f g) (hh : right_inverse h i) : right_inverse (h ∘ f) (g ∘ i) := left_inverse.comp hh hf -local attribute [instance, priority 1] classical.prop_decidable +local attribute [instance, priority 10] classical.prop_decidable /-- We can use choice to construct explicitly a partial inverse for a given injective function `f`. -/ @@ -119,7 +119,7 @@ end section inv_fun variables {α : Type u} [inhabited α] {β : Sort v} {f : α → β} {s : set α} {a : α} {b : β} -local attribute [instance, priority 1] classical.prop_decidable +local attribute [instance, priority 10] classical.prop_decidable /-- Construct the inverse for a function `f` on domain `s`. -/ noncomputable def inv_fun_on (f : α → β) (s : set α) (b : β) : α := diff --git a/src/tactic/finish.lean b/src/tactic/finish.lean index 1ef65efbaab54..f40f7b8b81259 100644 --- a/src/tactic/finish.lean +++ b/src/tactic/finish.lean @@ -111,7 +111,7 @@ variable {α : Type u} variables (p q : Prop) variable (s : α → Prop) -local attribute [instance, priority 1] classical.prop_decidable +local attribute [instance, priority 10] classical.prop_decidable theorem not_not_eq : (¬ ¬ p) = p := propext not_not theorem not_and_eq : (¬ (p ∧ q)) = (¬ p ∨ ¬ q) := propext not_and_distrib theorem not_or_eq : (¬ (p ∨ q)) = (¬ p ∧ ¬ q) := propext not_or_distrib @@ -397,7 +397,7 @@ local_context >>= case_some_hyp_aux s cont `safe_core s ps cfg opt` negates the goal, normalizes hypotheses (by splitting conjunctions, eliminating existentials, pushing negations inwards, and calling `simp` with the supplied lemmas `s`), and then tries `contradiction`. - + If this fails, it will create an SMT state and repeatedly use `ematch` (using `ematch` lemmas in the environment, universally quantified assumptions, and the supplied lemmas `ps`) and congruence closure. @@ -432,7 +432,7 @@ do when_tracing `auto.finish (trace "entering safe_core" >> trace_state), /-- `clarify` is `safe_core`, but with the `(opt : case_option)` - parameter fixed at `case_option.at_most_one`. + parameter fixed at `case_option.at_most_one`. -/ meta def clarify (s : simp_lemmas × list name) (ps : list pexpr) (cfg : auto_config := {}) : tactic unit := safe_core s ps cfg case_option.at_most_one @@ -481,13 +481,13 @@ local postfix *:9001 := many `clarify [h1,...,hn] using [e1,...,en]` negates the goal, normalizes hypotheses (by splitting conjunctions, eliminating existentials, pushing negations inwards, and calling `simp` with the supplied lemmas `h1,...,hn`), and then tries `contradiction`. - + If this fails, it will create an SMT state and repeatedly use `ematch` (using `ematch` lemmas in the environment, universally quantified assumptions, and the supplied lemmas `e1,...,en`) and congruence closure. `clarify` is complete for propositional logic. - + Either of the supplied simp lemmas or the supplied ematch lemmas are optional. `clarify` will fail if it produces more than one goal. @@ -501,13 +501,13 @@ do s ← mk_simp_set ff [] hs, `safe [h1,...,hn] using [e1,...,en]` negates the goal, normalizes hypotheses (by splitting conjunctions, eliminating existentials, pushing negations inwards, and calling `simp` with the supplied lemmas `h1,...,hn`), and then tries `contradiction`. - + If this fails, it will create an SMT state and repeatedly use `ematch` (using `ematch` lemmas in the environment, universally quantified assumptions, and the supplied lemmas `e1,...,en`) and congruence closure. `safe` is complete for propositional logic. - + Either of the supplied simp lemmas or the supplied ematch lemmas are optional. `safe` ignores the number of goals it produces, and should never fail. @@ -521,13 +521,13 @@ do s ← mk_simp_set ff [] hs, `finish [h1,...,hn] using [e1,...,en]` negates the goal, normalizes hypotheses (by splitting conjunctions, eliminating existentials, pushing negations inwards, and calling `simp` with the supplied lemmas `h1,...,hn`), and then tries `contradiction`. - + If this fails, it will create an SMT state and repeatedly use `ematch` (using `ematch` lemmas in the environment, universally quantified assumptions, and the supplied lemmas `e1,...,en`) and congruence closure. `finish` is complete for propositional logic. - + Either of the supplied simp lemmas or the supplied ematch lemmas are optional. `finish` will fail if it does not close the goal. diff --git a/src/tactic/localized.lean b/src/tactic/localized.lean index 88f52a32e2ba7..8c2244aa40ac7 100644 --- a/src/tactic/localized.lean +++ b/src/tactic/localized.lean @@ -70,7 +70,7 @@ meta def print_localized_commands (ns : list name) : tactic unit := do cmds ← get_localized ns, cmds.mmap' trace -- you can run `open_locale classical` to get the decidability of all propositions. -localized "attribute [instance, priority 1] classical.prop_decidable" in classical +localized "attribute [instance, priority 9] classical.prop_decidable" in classical localized "postfix `?`:9001 := optional" in parser localized "postfix *:9001 := lean.parser.many" in parser diff --git a/src/tactic/push_neg.lean b/src/tactic/push_neg.lean index d123389a2e8a2..788392f23350d 100644 --- a/src/tactic/push_neg.lean +++ b/src/tactic/push_neg.lean @@ -21,7 +21,7 @@ variable {α : Sort u} variables (p q : Prop) variable (s : α → Prop) -local attribute [instance, priority 1] classical.prop_decidable +local attribute [instance, priority 10] classical.prop_decidable theorem not_not_eq : (¬ ¬ p) = p := propext not_not theorem not_and_eq : (¬ (p ∧ q)) = (¬ p ∨ ¬ q) := propext not_and_distrib theorem not_or_eq : (¬ (p ∨ q)) = (¬ p ∧ ¬ q) := propext not_or_distrib diff --git a/src/topology/algebra/uniform_group.lean b/src/topology/algebra/uniform_group.lean index 214eecbcf4185..e38b175b56792 100644 --- a/src/topology/algebra/uniform_group.lean +++ b/src/topology/algebra/uniform_group.lean @@ -61,7 +61,7 @@ by simp * at * lemma uniform_continuous_add' : uniform_continuous (λp:α×α, p.1 + p.2) := uniform_continuous_add uniform_continuous_fst uniform_continuous_snd -@[priority 0] +@[priority 10] instance uniform_add_group.to_topological_add_group : topological_add_group α := { continuous_add := uniform_continuous_add'.continuous, continuous_neg := uniform_continuous_neg'.continuous } diff --git a/src/topology/metric_space/gromov_hausdorff.lean b/src/topology/metric_space/gromov_hausdorff.lean index 8311c99ec97e3..7f42f266c7213 100644 --- a/src/topology/metric_space/gromov_hausdorff.lean +++ b/src/topology/metric_space/gromov_hausdorff.lean @@ -225,7 +225,7 @@ begin simp [Aα, Bβ] end -local attribute [instance, priority 0] inhabited_of_nonempty' +local attribute [instance, priority 10] inhabited_of_nonempty' /-- The optimal coupling constructed above realizes exactly the Gromov-Hausdorff distance, essentially by design. -/ @@ -371,8 +371,8 @@ end -- without the next two lines, { exact closed_of_compact (range Φ) hΦ } in the next -- proof is very slow, as the t2_space instance is very hard to find -local attribute [instance, priority 0] orderable_topology.t2_space -local attribute [instance, priority 0] ordered_topology.to_t2_space +local attribute [instance, priority 10] orderable_topology.t2_space +local attribute [instance, priority 10] ordered_topology.to_t2_space /-- The Gromov-Hausdorff distance defines a genuine distance on the Gromov-Hausdorff space. -/ instance GH_space_metric_space : metric_space GH_space := diff --git a/src/topology/metric_space/gromov_hausdorff_realized.lean b/src/topology/metric_space/gromov_hausdorff_realized.lean index a1fb2013a4667..539c18c82600d 100644 --- a/src/topology/metric_space/gromov_hausdorff_realized.lean +++ b/src/topology/metric_space/gromov_hausdorff_realized.lean @@ -66,7 +66,7 @@ section constructions variables {α : Type u} {β : Type v} [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] {f : prod_space_fun α β} {x y z t : α ⊕ β} -local attribute [instance, priority 0] inhabited_of_nonempty' +local attribute [instance, priority 10] inhabited_of_nonempty' private lemma max_var_bound : dist x y ≤ max_var α β := calc dist x y ≤ diam (univ : set (α ⊕ β)) : diff --git a/src/topology/uniform_space/abstract_completion.lean b/src/topology/uniform_space/abstract_completion.lean index 30272ac3ce486..19a2150891cba 100644 --- a/src/topology/uniform_space/abstract_completion.lean +++ b/src/topology/uniform_space/abstract_completion.lean @@ -45,7 +45,7 @@ uniform spaces, completion, universal property -/ noncomputable theory -local attribute [instance, priority 0] classical.prop_decidable +local attribute [instance, priority 10] classical.prop_decidable open filter set function