From 6dd82c468283f50fef52895c043c12ab3856a19c Mon Sep 17 00:00:00 2001 From: Arien Malec Date: Fri, 27 Jan 2023 15:33:04 -0800 Subject: [PATCH 1/8] feat: port Data.Finsupp.Fin From d31aef181755005667a8af426ebabe13690cff5a Mon Sep 17 00:00:00 2001 From: Arien Malec Date: Fri, 27 Jan 2023 15:33:04 -0800 Subject: [PATCH 2/8] Initial file copy from mathport --- Mathlib/Data/Finsupp/Fin.lean | 102 ++++++++++++++++++++++++++++++++++ 1 file changed, 102 insertions(+) create mode 100644 Mathlib/Data/Finsupp/Fin.lean diff --git a/Mathlib/Data/Finsupp/Fin.lean b/Mathlib/Data/Finsupp/Fin.lean new file mode 100644 index 0000000000000..503d9b8161634 --- /dev/null +++ b/Mathlib/Data/Finsupp/Fin.lean @@ -0,0 +1,102 @@ +/- +Copyright (c) 2021 Ivan Sadofschi Costa. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ivan Sadofschi Costa + +! This file was ported from Lean 3 source module data.finsupp.fin +! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathbin.Data.Finsupp.Defs + +/-! +# `cons` and `tail` for maps `fin n →₀ M` + +We interpret maps `fin n →₀ M` as `n`-tuples of elements of `M`, +We define the following operations: +* `finsupp.tail` : the tail of a map `fin (n + 1) →₀ M`, i.e., its last `n` entries; +* `finsupp.cons` : adding an element at the beginning of an `n`-tuple, to get an `n + 1`-tuple; + +In this context, we prove some usual properties of `tail` and `cons`, analogous to those of +`data.fin.tuple.basic`. +-/ + + +noncomputable section + +namespace Finsupp + +variable {n : ℕ} (i : Fin n) {M : Type _} [Zero M] (y : M) (t : Fin (n + 1) →₀ M) (s : Fin n →₀ M) + +/-- `tail` for maps `fin (n + 1) →₀ M`. See `fin.tail` for more details. -/ +def tail (s : Fin (n + 1) →₀ M) : Fin n →₀ M := + Finsupp.equivFunOnFinite.symm (Fin.tail s) +#align finsupp.tail Finsupp.tail + +/-- `cons` for maps `fin n →₀ M`. See `fin.cons` for more details. -/ +def cons (y : M) (s : Fin n →₀ M) : Fin (n + 1) →₀ M := + Finsupp.equivFunOnFinite.symm (Fin.cons y s : Fin (n + 1) → M) +#align finsupp.cons Finsupp.cons + +theorem tail_apply : tail t i = t i.succ := + rfl +#align finsupp.tail_apply Finsupp.tail_apply + +@[simp] +theorem cons_zero : cons y s 0 = y := + rfl +#align finsupp.cons_zero Finsupp.cons_zero + +@[simp] +theorem cons_succ : cons y s i.succ = s i := + Fin.cons_succ _ _ _ +#align finsupp.cons_succ Finsupp.cons_succ + +@[simp] +theorem tail_cons : tail (cons y s) = s := + ext fun k => by simp only [tail_apply, cons_succ] +#align finsupp.tail_cons Finsupp.tail_cons + +@[simp] +theorem cons_tail : cons (t 0) (tail t) = t := by + ext + by_cases c_a : a = 0 + · rw [c_a, cons_zero] + · rw [← Fin.succ_pred a c_a, cons_succ, ← tail_apply] +#align finsupp.cons_tail Finsupp.cons_tail + +@[simp] +theorem cons_zero_zero : cons 0 (0 : Fin n →₀ M) = 0 := + by + ext + by_cases c : a = 0 + · simp [c] + · rw [← Fin.succ_pred a c, cons_succ] + simp +#align finsupp.cons_zero_zero Finsupp.cons_zero_zero + +variable {s} {y} + +theorem cons_ne_zero_of_left (h : y ≠ 0) : cons y s ≠ 0 := + by + contrapose! h with c + rw [← cons_zero y s, c, Finsupp.coe_zero, Pi.zero_apply] +#align finsupp.cons_ne_zero_of_left Finsupp.cons_ne_zero_of_left + +theorem cons_ne_zero_of_right (h : s ≠ 0) : cons y s ≠ 0 := + by + contrapose! h with c + ext + simp [← cons_succ a y s, c] +#align finsupp.cons_ne_zero_of_right Finsupp.cons_ne_zero_of_right + +theorem cons_ne_zero_iff : cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0 := + by + refine' ⟨fun h => _, fun h => h.casesOn cons_ne_zero_of_left cons_ne_zero_of_right⟩ + refine' imp_iff_not_or.1 fun h' c => h _ + rw [h', c, Finsupp.cons_zero_zero] +#align finsupp.cons_ne_zero_iff Finsupp.cons_ne_zero_iff + +end Finsupp + From 1baa2d573559b08ff4abcf47f3af0f08c0840c86 Mon Sep 17 00:00:00 2001 From: Arien Malec Date: Fri, 27 Jan 2023 15:33:04 -0800 Subject: [PATCH 3/8] automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean --- Mathlib.lean | 1 + Mathlib/Data/Finsupp/Fin.lean | 14 +++++--------- 2 files changed, 6 insertions(+), 9 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index e0ebb6354b6ce..705a460c4c054 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -297,6 +297,7 @@ import Mathlib.Data.Finset.Sigma import Mathlib.Data.Finset.Sort import Mathlib.Data.Finset.Sum import Mathlib.Data.Finsupp.Defs +import Mathlib.Data.Finsupp.Fin import Mathlib.Data.Finsupp.Order import Mathlib.Data.Fintype.Basic import Mathlib.Data.Fintype.BigOperators diff --git a/Mathlib/Data/Finsupp/Fin.lean b/Mathlib/Data/Finsupp/Fin.lean index 503d9b8161634..9b2ddddb9bfd4 100644 --- a/Mathlib/Data/Finsupp/Fin.lean +++ b/Mathlib/Data/Finsupp/Fin.lean @@ -8,7 +8,7 @@ Authors: Ivan Sadofschi Costa ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.Data.Finsupp.Defs +import Mathlib.Data.Finsupp.Defs /-! # `cons` and `tail` for maps `fin n →₀ M` @@ -67,8 +67,7 @@ theorem cons_tail : cons (t 0) (tail t) = t := by #align finsupp.cons_tail Finsupp.cons_tail @[simp] -theorem cons_zero_zero : cons 0 (0 : Fin n →₀ M) = 0 := - by +theorem cons_zero_zero : cons 0 (0 : Fin n →₀ M) = 0 := by ext by_cases c : a = 0 · simp [c] @@ -78,21 +77,18 @@ theorem cons_zero_zero : cons 0 (0 : Fin n →₀ M) = 0 := variable {s} {y} -theorem cons_ne_zero_of_left (h : y ≠ 0) : cons y s ≠ 0 := - by +theorem cons_ne_zero_of_left (h : y ≠ 0) : cons y s ≠ 0 := by contrapose! h with c rw [← cons_zero y s, c, Finsupp.coe_zero, Pi.zero_apply] #align finsupp.cons_ne_zero_of_left Finsupp.cons_ne_zero_of_left -theorem cons_ne_zero_of_right (h : s ≠ 0) : cons y s ≠ 0 := - by +theorem cons_ne_zero_of_right (h : s ≠ 0) : cons y s ≠ 0 := by contrapose! h with c ext simp [← cons_succ a y s, c] #align finsupp.cons_ne_zero_of_right Finsupp.cons_ne_zero_of_right -theorem cons_ne_zero_iff : cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0 := - by +theorem cons_ne_zero_iff : cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0 := by refine' ⟨fun h => _, fun h => h.casesOn cons_ne_zero_of_left cons_ne_zero_of_right⟩ refine' imp_iff_not_or.1 fun h' c => h _ rw [h', c, Finsupp.cons_zero_zero] From d78d65276c723b81125580cebe9e1596d1fdadfe Mon Sep 17 00:00:00 2001 From: Arien Malec Date: Fri, 27 Jan 2023 15:35:40 -0800 Subject: [PATCH 4/8] explicit naming for `ext` --- Mathlib/Data/Finsupp/Fin.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Mathlib/Data/Finsupp/Fin.lean b/Mathlib/Data/Finsupp/Fin.lean index 9b2ddddb9bfd4..c1eb58957709d 100644 --- a/Mathlib/Data/Finsupp/Fin.lean +++ b/Mathlib/Data/Finsupp/Fin.lean @@ -60,7 +60,7 @@ theorem tail_cons : tail (cons y s) = s := @[simp] theorem cons_tail : cons (t 0) (tail t) = t := by - ext + ext a by_cases c_a : a = 0 · rw [c_a, cons_zero] · rw [← Fin.succ_pred a c_a, cons_succ, ← tail_apply] @@ -68,7 +68,7 @@ theorem cons_tail : cons (t 0) (tail t) = t := by @[simp] theorem cons_zero_zero : cons 0 (0 : Fin n →₀ M) = 0 := by - ext + ext a by_cases c : a = 0 · simp [c] · rw [← Fin.succ_pred a c, cons_succ] @@ -84,7 +84,7 @@ theorem cons_ne_zero_of_left (h : y ≠ 0) : cons y s ≠ 0 := by theorem cons_ne_zero_of_right (h : s ≠ 0) : cons y s ≠ 0 := by contrapose! h with c - ext + ext a simp [← cons_succ a y s, c] #align finsupp.cons_ne_zero_of_right Finsupp.cons_ne_zero_of_right @@ -95,4 +95,3 @@ theorem cons_ne_zero_iff : cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0 := by #align finsupp.cons_ne_zero_iff Finsupp.cons_ne_zero_iff end Finsupp - From a92b88c701b1ee5d7c2b214c2bf7815cfd8a7bb4 Mon Sep 17 00:00:00 2001 From: Arien Malec Date: Fri, 27 Jan 2023 15:39:10 -0800 Subject: [PATCH 5/8] fix for cons_succ --- Mathlib/Data/Finsupp/Fin.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/Finsupp/Fin.lean b/Mathlib/Data/Finsupp/Fin.lean index c1eb58957709d..6eb1c7b3e5fd0 100644 --- a/Mathlib/Data/Finsupp/Fin.lean +++ b/Mathlib/Data/Finsupp/Fin.lean @@ -9,6 +9,7 @@ Authors: Ivan Sadofschi Costa ! if you have ported upstream changes. -/ import Mathlib.Data.Finsupp.Defs +import Mathlib.Tactic.LibrarySearch /-! # `cons` and `tail` for maps `fin n →₀ M` @@ -50,7 +51,7 @@ theorem cons_zero : cons y s 0 = y := @[simp] theorem cons_succ : cons y s i.succ = s i := - Fin.cons_succ _ _ _ + namedPattern rfl rfl rfl #align finsupp.cons_succ Finsupp.cons_succ @[simp] From 53a83cc81d592e161973b0f0c4506e9801a38a7d Mon Sep 17 00:00:00 2001 From: Arien Malec Date: Fri, 27 Jan 2023 15:39:59 -0800 Subject: [PATCH 6/8] fix for cons_succ --- Mathlib/Data/Finsupp/Fin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Finsupp/Fin.lean b/Mathlib/Data/Finsupp/Fin.lean index 6eb1c7b3e5fd0..45dd66589863d 100644 --- a/Mathlib/Data/Finsupp/Fin.lean +++ b/Mathlib/Data/Finsupp/Fin.lean @@ -9,7 +9,6 @@ Authors: Ivan Sadofschi Costa ! if you have ported upstream changes. -/ import Mathlib.Data.Finsupp.Defs -import Mathlib.Tactic.LibrarySearch /-! # `cons` and `tail` for maps `fin n →₀ M` @@ -51,6 +50,7 @@ theorem cons_zero : cons y s 0 = y := @[simp] theorem cons_succ : cons y s i.succ = s i := + -- porting notes: was Fin.cons_succ _ _ _ namedPattern rfl rfl rfl #align finsupp.cons_succ Finsupp.cons_succ From ef69de489955420d6862c6bda22fbccccf18d209 Mon Sep 17 00:00:00 2001 From: Arien Malec Date: Fri, 27 Jan 2023 15:41:08 -0800 Subject: [PATCH 7/8] automated docu naming fixes --- Mathlib/Data/Finsupp/Fin.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Data/Finsupp/Fin.lean b/Mathlib/Data/Finsupp/Fin.lean index 45dd66589863d..e1bec28426d72 100644 --- a/Mathlib/Data/Finsupp/Fin.lean +++ b/Mathlib/Data/Finsupp/Fin.lean @@ -15,8 +15,8 @@ import Mathlib.Data.Finsupp.Defs We interpret maps `fin n →₀ M` as `n`-tuples of elements of `M`, We define the following operations: -* `finsupp.tail` : the tail of a map `fin (n + 1) →₀ M`, i.e., its last `n` entries; -* `finsupp.cons` : adding an element at the beginning of an `n`-tuple, to get an `n + 1`-tuple; +* `Finsupp.tail` : the tail of a map `fin (n + 1) →₀ M`, i.e., its last `n` entries; +* `Finsupp.cons` : adding an element at the beginning of an `n`-tuple, to get an `n + 1`-tuple; In this context, we prove some usual properties of `tail` and `cons`, analogous to those of `data.fin.tuple.basic`. @@ -29,12 +29,12 @@ namespace Finsupp variable {n : ℕ} (i : Fin n) {M : Type _} [Zero M] (y : M) (t : Fin (n + 1) →₀ M) (s : Fin n →₀ M) -/-- `tail` for maps `fin (n + 1) →₀ M`. See `fin.tail` for more details. -/ +/-- `tail` for maps `fin (n + 1) →₀ M`. See `Fin.tail` for more details. -/ def tail (s : Fin (n + 1) →₀ M) : Fin n →₀ M := Finsupp.equivFunOnFinite.symm (Fin.tail s) #align finsupp.tail Finsupp.tail -/-- `cons` for maps `fin n →₀ M`. See `fin.cons` for more details. -/ +/-- `cons` for maps `fin n →₀ M`. See `Fin.cons` for more details. -/ def cons (y : M) (s : Fin n →₀ M) : Fin (n + 1) →₀ M := Finsupp.equivFunOnFinite.symm (Fin.cons y s : Fin (n + 1) → M) #align finsupp.cons Finsupp.cons From 3413a6499d0fb06e7ad72c9f188b13ad43147e76 Mon Sep 17 00:00:00 2001 From: Arien Malec Date: Fri, 27 Jan 2023 15:41:54 -0800 Subject: [PATCH 8/8] docu fixes --- Mathlib/Data/Finsupp/Fin.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Data/Finsupp/Fin.lean b/Mathlib/Data/Finsupp/Fin.lean index e1bec28426d72..44588712533a9 100644 --- a/Mathlib/Data/Finsupp/Fin.lean +++ b/Mathlib/Data/Finsupp/Fin.lean @@ -11,15 +11,15 @@ Authors: Ivan Sadofschi Costa import Mathlib.Data.Finsupp.Defs /-! -# `cons` and `tail` for maps `fin n →₀ M` +# `cons` and `tail` for maps `Fin n →₀ M` -We interpret maps `fin n →₀ M` as `n`-tuples of elements of `M`, +We interpret maps `Fin n →₀ M` as `n`-tuples of elements of `M`, We define the following operations: -* `Finsupp.tail` : the tail of a map `fin (n + 1) →₀ M`, i.e., its last `n` entries; +* `Finsupp.tail` : the tail of a map `Fin (n + 1) →₀ M`, i.e., its last `n` entries; * `Finsupp.cons` : adding an element at the beginning of an `n`-tuple, to get an `n + 1`-tuple; In this context, we prove some usual properties of `tail` and `cons`, analogous to those of -`data.fin.tuple.basic`. +`Data.Fin.Tuple.Basic`. -/ @@ -29,12 +29,12 @@ namespace Finsupp variable {n : ℕ} (i : Fin n) {M : Type _} [Zero M] (y : M) (t : Fin (n + 1) →₀ M) (s : Fin n →₀ M) -/-- `tail` for maps `fin (n + 1) →₀ M`. See `Fin.tail` for more details. -/ +/-- `tail` for maps `Fin (n + 1) →₀ M`. See `Fin.tail` for more details. -/ def tail (s : Fin (n + 1) →₀ M) : Fin n →₀ M := Finsupp.equivFunOnFinite.symm (Fin.tail s) #align finsupp.tail Finsupp.tail -/-- `cons` for maps `fin n →₀ M`. See `Fin.cons` for more details. -/ +/-- `cons` for maps `Fin n →₀ M`. See `Fin.cons` for more details. -/ def cons (y : M) (s : Fin n →₀ M) : Fin (n + 1) →₀ M := Finsupp.equivFunOnFinite.symm (Fin.cons y s : Fin (n + 1) → M) #align finsupp.cons Finsupp.cons