From 98a4458cbfa0888d49408763247b669c712cec63 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 20 Jan 2023 15:08:17 +0000 Subject: [PATCH 1/7] feat: port Data.Finite.Basic From 8c6a07adde9cd684544daeb3e1ea79a4c59586f3 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 20 Jan 2023 15:08:17 +0000 Subject: [PATCH 2/7] Initial file copy from mathport --- Mathlib/Data/Finite/Basic.lean | 164 +++++++++++++++++++++++++++++++++ 1 file changed, 164 insertions(+) create mode 100644 Mathlib/Data/Finite/Basic.lean diff --git a/Mathlib/Data/Finite/Basic.lean b/Mathlib/Data/Finite/Basic.lean new file mode 100644 index 0000000000000..a72c9dde5c9d7 --- /dev/null +++ b/Mathlib/Data/Finite/Basic.lean @@ -0,0 +1,164 @@ +/- +Copyright (c) 2022 Kyle Miller. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller + +! This file was ported from Lean 3 source module data.finite.basic +! leanprover-community/mathlib commit 1126441d6bccf98c81214a0780c73d499f6721fe +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathbin.Data.Fintype.Powerset +import Mathbin.Data.Fintype.Prod +import Mathbin.Data.Fintype.Sigma +import Mathbin.Data.Fintype.Sum +import Mathbin.Data.Fintype.Vector + +/-! +# Finite types + +In this file we prove some theorems about `finite` and provide some instances. This typeclass is a +`Prop`-valued counterpart of the typeclass `fintype`. See more details in the file where `finite` is +defined. + +## Main definitions + +* `fintype.finite`, `finite.of_fintype` creates a `finite` instance from a `fintype` instance. The + former lemma takes `fintype α` as an explicit argument while the latter takes it as an instance + argument. +* `fintype.of_finite` noncomputably creates a `fintype` instance from a `finite` instance. + +## Implementation notes + +There is an apparent duplication of many `fintype` instances in this module, +however they follow a pattern: if a `fintype` instance depends on `decidable` +instances or other `fintype` instances, then we need to "lower" the instance +to be a `finite` instance by removing the `decidable` instances and switching +the `fintype` instances to `finite` instances. These are precisely the ones +that cannot be inferred using `finite.of_fintype`. (However, when using +`open_locale classical` or the `classical` tactic the instances relying only +on `decidable` instances will give `finite` instances.) In the future we might +consider writing automation to create these "lowered" instances. + +## Tags + +finiteness, finite types +-/ + + +noncomputable section + +open Classical + +variable {α β γ : Type _} + +namespace Finite + +-- see Note [lower instance priority] +instance (priority := 100) of_subsingleton {α : Sort _} [Subsingleton α] : Finite α := + of_injective (Function.const α ()) <| Function.injective_of_subsingleton _ +#align finite.of_subsingleton Finite.of_subsingleton + +-- Higher priority for `Prop`s +@[nolint instance_priority] +instance prop (p : Prop) : Finite p := + Finite.of_subsingleton +#align finite.prop Finite.prop + +instance [Finite α] [Finite β] : Finite (α × β) := + by + haveI := Fintype.ofFinite α + haveI := Fintype.ofFinite β + infer_instance + +instance {α β : Sort _} [Finite α] [Finite β] : Finite (PProd α β) := + of_equiv _ Equiv.pprodEquivProdPLift.symm + +theorem prod_left (β) [Finite (α × β)] [Nonempty β] : Finite α := + of_surjective (Prod.fst : α × β → α) Prod.fst_surjective +#align finite.prod_left Finite.prod_left + +theorem prod_right (α) [Finite (α × β)] [Nonempty α] : Finite β := + of_surjective (Prod.snd : α × β → β) Prod.snd_surjective +#align finite.prod_right Finite.prod_right + +instance [Finite α] [Finite β] : Finite (Sum α β) := + by + haveI := Fintype.ofFinite α + haveI := Fintype.ofFinite β + infer_instance + +theorem sum_left (β) [Finite (Sum α β)] : Finite α := + of_injective (Sum.inl : α → Sum α β) Sum.inl_injective +#align finite.sum_left Finite.sum_left + +theorem sum_right (α) [Finite (Sum α β)] : Finite β := + of_injective (Sum.inr : β → Sum α β) Sum.inr_injective +#align finite.sum_right Finite.sum_right + +instance {β : α → Type _} [Finite α] [∀ a, Finite (β a)] : Finite (Σa, β a) := + by + letI := Fintype.ofFinite α + letI := fun a => Fintype.ofFinite (β a) + infer_instance + +instance {ι : Sort _} {π : ι → Sort _} [Finite ι] [∀ i, Finite (π i)] : Finite (Σ'i, π i) := + of_equiv _ (Equiv.psigmaEquivSigmaPLift π).symm + +instance [Finite α] : Finite (Set α) := + by + cases nonempty_fintype α + infer_instance + +end Finite + +/-- This instance also provides `[finite s]` for `s : set α`. -/ +instance Subtype.finite {α : Sort _} [Finite α] {p : α → Prop} : Finite { x // p x } := + Finite.of_injective coe Subtype.coe_injective +#align subtype.finite Subtype.finite + +instance Pi.finite {α : Sort _} {β : α → Sort _} [Finite α] [∀ a, Finite (β a)] : + Finite (∀ a, β a) := by + haveI := Fintype.ofFinite (PLift α) + haveI := fun a => Fintype.ofFinite (PLift (β a)) + exact + Finite.of_equiv (∀ a : PLift α, PLift (β (Equiv.plift a))) + (Equiv.piCongr Equiv.plift fun _ => Equiv.plift) +#align pi.finite Pi.finite + +instance Vector.finite {α : Type _} [Finite α] {n : ℕ} : Finite (Vector α n) := + by + haveI := Fintype.ofFinite α + infer_instance +#align vector.finite Vector.finite + +instance Quot.finite {α : Sort _} [Finite α] (r : α → α → Prop) : Finite (Quot r) := + Finite.of_surjective _ (surjective_quot_mk r) +#align quot.finite Quot.finite + +instance Quotient.finite {α : Sort _} [Finite α] (s : Setoid α) : Finite (Quotient s) := + Quot.finite _ +#align quotient.finite Quotient.finite + +instance Function.Embedding.finite {α β : Sort _} [Finite β] : Finite (α ↪ β) := + by + cases' isEmpty_or_nonempty (α ↪ β) with _ h + · infer_instance + · refine' h.elim fun f => _ + haveI : Finite α := Finite.of_injective _ f.injective + exact Finite.of_injective _ FunLike.coe_injective +#align function.embedding.finite Function.Embedding.finite + +instance Equiv.finite_right {α β : Sort _} [Finite β] : Finite (α ≃ β) := + Finite.of_injective Equiv.toEmbedding fun e₁ e₂ h => Equiv.ext <| by convert FunLike.congr_fun h +#align equiv.finite_right Equiv.finite_right + +instance Equiv.finite_left {α β : Sort _} [Finite α] : Finite (α ≃ β) := + Finite.of_equiv _ ⟨Equiv.symm, Equiv.symm, Equiv.symm_symm, Equiv.symm_symm⟩ +#align equiv.finite_left Equiv.finite_left + +instance [Finite α] {n : ℕ} : Finite (Sym α n) := + by + haveI := Fintype.ofFinite α + infer_instance + From ea4bd377e1b92c86f39c461be98df09377339322 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 20 Jan 2023 15:08:17 +0000 Subject: [PATCH 3/7] automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean --- Mathlib.lean | 1 + Mathlib/Data/Finite/Basic.lean | 31 ++++++++++++------------------- 2 files changed, 13 insertions(+), 19 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index eb4a735747e02..0eb9cd501d8e2 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -242,6 +242,7 @@ import Mathlib.Data.Fin.Fin2 import Mathlib.Data.Fin.SuccPred import Mathlib.Data.Fin.Tuple.Basic import Mathlib.Data.FinEnum +import Mathlib.Data.Finite.Basic import Mathlib.Data.Finite.Defs import Mathlib.Data.Finite.Set import Mathlib.Data.Finset.Basic diff --git a/Mathlib/Data/Finite/Basic.lean b/Mathlib/Data/Finite/Basic.lean index a72c9dde5c9d7..42098ae81c389 100644 --- a/Mathlib/Data/Finite/Basic.lean +++ b/Mathlib/Data/Finite/Basic.lean @@ -8,11 +8,11 @@ Authors: Kyle Miller ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.Data.Fintype.Powerset -import Mathbin.Data.Fintype.Prod -import Mathbin.Data.Fintype.Sigma -import Mathbin.Data.Fintype.Sum -import Mathbin.Data.Fintype.Vector +import Mathlib.Data.Fintype.Powerset +import Mathlib.Data.Fintype.Prod +import Mathlib.Data.Fintype.Sigma +import Mathlib.Data.Fintype.Sum +import Mathlib.Data.Fintype.Vector /-! # Finite types @@ -65,8 +65,7 @@ instance prop (p : Prop) : Finite p := Finite.of_subsingleton #align finite.prop Finite.prop -instance [Finite α] [Finite β] : Finite (α × β) := - by +instance [Finite α] [Finite β] : Finite (α × β) := by haveI := Fintype.ofFinite α haveI := Fintype.ofFinite β infer_instance @@ -82,8 +81,7 @@ theorem prod_right (α) [Finite (α × β)] [Nonempty α] : Finite β := of_surjective (Prod.snd : α × β → β) Prod.snd_surjective #align finite.prod_right Finite.prod_right -instance [Finite α] [Finite β] : Finite (Sum α β) := - by +instance [Finite α] [Finite β] : Finite (Sum α β) := by haveI := Fintype.ofFinite α haveI := Fintype.ofFinite β infer_instance @@ -96,8 +94,7 @@ theorem sum_right (α) [Finite (Sum α β)] : Finite β := of_injective (Sum.inr : β → Sum α β) Sum.inr_injective #align finite.sum_right Finite.sum_right -instance {β : α → Type _} [Finite α] [∀ a, Finite (β a)] : Finite (Σa, β a) := - by +instance {β : α → Type _} [Finite α] [∀ a, Finite (β a)] : Finite (Σa, β a) := by letI := Fintype.ofFinite α letI := fun a => Fintype.ofFinite (β a) infer_instance @@ -105,8 +102,7 @@ instance {β : α → Type _} [Finite α] [∀ a, Finite (β a)] : Finite (Σa, instance {ι : Sort _} {π : ι → Sort _} [Finite ι] [∀ i, Finite (π i)] : Finite (Σ'i, π i) := of_equiv _ (Equiv.psigmaEquivSigmaPLift π).symm -instance [Finite α] : Finite (Set α) := - by +instance [Finite α] : Finite (Set α) := by cases nonempty_fintype α infer_instance @@ -126,8 +122,7 @@ instance Pi.finite {α : Sort _} {β : α → Sort _} [Finite α] [∀ a, Finite (Equiv.piCongr Equiv.plift fun _ => Equiv.plift) #align pi.finite Pi.finite -instance Vector.finite {α : Type _} [Finite α] {n : ℕ} : Finite (Vector α n) := - by +instance Vector.finite {α : Type _} [Finite α] {n : ℕ} : Finite (Vector α n) := by haveI := Fintype.ofFinite α infer_instance #align vector.finite Vector.finite @@ -140,8 +135,7 @@ instance Quotient.finite {α : Sort _} [Finite α] (s : Setoid α) : Finite (Quo Quot.finite _ #align quotient.finite Quotient.finite -instance Function.Embedding.finite {α β : Sort _} [Finite β] : Finite (α ↪ β) := - by +instance Function.Embedding.finite {α β : Sort _} [Finite β] : Finite (α ↪ β) := by cases' isEmpty_or_nonempty (α ↪ β) with _ h · infer_instance · refine' h.elim fun f => _ @@ -157,8 +151,7 @@ instance Equiv.finite_left {α β : Sort _} [Finite α] : Finite (α ≃ β) := Finite.of_equiv _ ⟨Equiv.symm, Equiv.symm, Equiv.symm_symm, Equiv.symm_symm⟩ #align equiv.finite_left Equiv.finite_left -instance [Finite α] {n : ℕ} : Finite (Sym α n) := - by +instance [Finite α] {n : ℕ} : Finite (Sym α n) := by haveI := Fintype.ofFinite α infer_instance From 02857c5fbb3fd23de47f0436600594695b982332 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 20 Jan 2023 15:46:46 +0000 Subject: [PATCH 4/7] done --- Mathlib/Data/Finite/Basic.lean | 35 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 18 deletions(-) diff --git a/Mathlib/Data/Finite/Basic.lean b/Mathlib/Data/Finite/Basic.lean index 42098ae81c389..0b9000a7f43a9 100644 --- a/Mathlib/Data/Finite/Basic.lean +++ b/Mathlib/Data/Finite/Basic.lean @@ -17,27 +17,27 @@ import Mathlib.Data.Fintype.Vector /-! # Finite types -In this file we prove some theorems about `finite` and provide some instances. This typeclass is a -`Prop`-valued counterpart of the typeclass `fintype`. See more details in the file where `finite` is +In this file we prove some theorems about `Finite` and provide some instances. This typeclass is a +`Prop`-valued counterpart of the typeclass `Fintype`. See more details in the file where `Finite` is defined. ## Main definitions -* `fintype.finite`, `finite.of_fintype` creates a `finite` instance from a `fintype` instance. The - former lemma takes `fintype α` as an explicit argument while the latter takes it as an instance +* `Fintype.finite`, `Finite.of_fintype` creates a `Finite` instance from a `Fintype` instance. The + former lemma takes `Fintype α` as an explicit argument while the latter takes it as an instance argument. -* `fintype.of_finite` noncomputably creates a `fintype` instance from a `finite` instance. +* `Fintype.of_finite` noncomputably creates a `Fintype` instance from a `Finite` instance. ## Implementation notes -There is an apparent duplication of many `fintype` instances in this module, -however they follow a pattern: if a `fintype` instance depends on `decidable` -instances or other `fintype` instances, then we need to "lower" the instance -to be a `finite` instance by removing the `decidable` instances and switching -the `fintype` instances to `finite` instances. These are precisely the ones -that cannot be inferred using `finite.of_fintype`. (However, when using -`open_locale classical` or the `classical` tactic the instances relying only -on `decidable` instances will give `finite` instances.) In the future we might +There is an apparent duplication of many `Fintype` instances in this module, +however they follow a pattern: if a `Fintype` instance depends on `Decidable` +instances or other `Fintype` instances, then we need to "lower" the instance +to be a `Finite` instance by removing the `decidable` instances and switching +the `Fintype` instances to `Finite` instances. These are precisely the ones +that cannot be inferred using `Finite.of_fintype`. (However, when using +`open Classical` or the `classical` tactic the instances relying only +on `Decidable` instances will give `Finite` instances.) In the future we might consider writing automation to create these "lowered" instances. ## Tags @@ -60,7 +60,7 @@ instance (priority := 100) of_subsingleton {α : Sort _} [Subsingleton α] : Fin #align finite.of_subsingleton Finite.of_subsingleton -- Higher priority for `Prop`s -@[nolint instance_priority] +-- @[nolint instance_priority] -- Porting note: linter not found instance prop (p : Prop) : Finite p := Finite.of_subsingleton #align finite.prop Finite.prop @@ -108,9 +108,9 @@ instance [Finite α] : Finite (Set α) := by end Finite -/-- This instance also provides `[finite s]` for `s : set α`. -/ +/-- This instance also provides `[Finite s]` for `s : Set α`. -/ instance Subtype.finite {α : Sort _} [Finite α] {p : α → Prop} : Finite { x // p x } := - Finite.of_injective coe Subtype.coe_injective + Finite.of_injective (↑) Subtype.coe_injective #align subtype.finite Subtype.finite instance Pi.finite {α : Sort _} {β : α → Sort _} [Finite α] [∀ a, Finite (β a)] : @@ -137,7 +137,7 @@ instance Quotient.finite {α : Sort _} [Finite α] (s : Setoid α) : Finite (Quo instance Function.Embedding.finite {α β : Sort _} [Finite β] : Finite (α ↪ β) := by cases' isEmpty_or_nonempty (α ↪ β) with _ h - · infer_instance + · apply Finite.of_subsingleton · refine' h.elim fun f => _ haveI : Finite α := Finite.of_injective _ f.injective exact Finite.of_injective _ FunLike.coe_injective @@ -154,4 +154,3 @@ instance Equiv.finite_left {α β : Sort _} [Finite α] : Finite (α ≃ β) := instance [Finite α] {n : ℕ} : Finite (Sym α n) := by haveI := Fintype.ofFinite α infer_instance - From b45e120c90a406dbe57ea709179f80273d8fe340 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 20 Jan 2023 16:01:15 +0000 Subject: [PATCH 5/7] Update Mathlib/Data/Finite/Basic.lean --- Mathlib/Data/Finite/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Finite/Basic.lean b/Mathlib/Data/Finite/Basic.lean index 0b9000a7f43a9..a3dc3f39afd68 100644 --- a/Mathlib/Data/Finite/Basic.lean +++ b/Mathlib/Data/Finite/Basic.lean @@ -137,7 +137,7 @@ instance Quotient.finite {α : Sort _} [Finite α] (s : Setoid α) : Finite (Quo instance Function.Embedding.finite {α β : Sort _} [Finite β] : Finite (α ↪ β) := by cases' isEmpty_or_nonempty (α ↪ β) with _ h - · apply Finite.of_subsingleton + · apply Finite.of_subsingleton -- Porting note: inferInstance fails because it applies `Finite.of_fintype`. · refine' h.elim fun f => _ haveI : Finite α := Finite.of_injective _ f.injective exact Finite.of_injective _ FunLike.coe_injective From 15aaa6deb366552dd16769dc4567e02e30e517bd Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 20 Jan 2023 17:21:07 +0100 Subject: [PATCH 6/7] Update Mathlib/Data/Finite/Basic.lean --- Mathlib/Data/Finite/Basic.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/Finite/Basic.lean b/Mathlib/Data/Finite/Basic.lean index a3dc3f39afd68..d088b726e8906 100644 --- a/Mathlib/Data/Finite/Basic.lean +++ b/Mathlib/Data/Finite/Basic.lean @@ -137,7 +137,9 @@ instance Quotient.finite {α : Sort _} [Finite α] (s : Setoid α) : Finite (Quo instance Function.Embedding.finite {α β : Sort _} [Finite β] : Finite (α ↪ β) := by cases' isEmpty_or_nonempty (α ↪ β) with _ h - · apply Finite.of_subsingleton -- Porting note: inferInstance fails because it applies `Finite.of_fintype`. + · -- Porting note: inferInstance fails because it applies `Finite.of_fintype`. + apply Finite.of_subsingleton + · refine' h.elim fun f => _ haveI : Finite α := Finite.of_injective _ f.injective exact Finite.of_injective _ FunLike.coe_injective From 8dd600d431f125ab3d5f6a70dc8b6d9078307d67 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Fri, 20 Jan 2023 19:06:27 +0100 Subject: [PATCH 7/7] Update Mathlib/Data/Finite/Basic.lean Co-authored-by: Eric Wieser --- Mathlib/Data/Finite/Basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/Finite/Basic.lean b/Mathlib/Data/Finite/Basic.lean index d088b726e8906..d6a6a280f4fb9 100644 --- a/Mathlib/Data/Finite/Basic.lean +++ b/Mathlib/Data/Finite/Basic.lean @@ -137,7 +137,8 @@ instance Quotient.finite {α : Sort _} [Finite α] (s : Setoid α) : Finite (Quo instance Function.Embedding.finite {α β : Sort _} [Finite β] : Finite (α ↪ β) := by cases' isEmpty_or_nonempty (α ↪ β) with _ h - · -- Porting note: inferInstance fails because it applies `Finite.of_fintype`. + · -- Porting note: infer_instance fails because it applies `Finite.of_fintype` and produces a + -- "stuck at solving universe constraint" error. apply Finite.of_subsingleton · refine' h.elim fun f => _