From c1fe20aa5737d07d1afd2d00a3a30734bfcb6f6e Mon Sep 17 00:00:00 2001 From: ChrisHughes24 Date: Fri, 6 Jan 2023 15:21:05 +0000 Subject: [PATCH 1/5] chore(data/multiset): move has_repr into its own file to remove data.string.basic import --- src/data/finset/default.lean | 1 + src/data/finset/repr.lean | 13 +++++++++++++ src/data/finset/sort.lean | 2 -- src/data/multiset/default.lean | 1 + src/data/multiset/repr.lean | 14 ++++++++++++++ src/data/multiset/sort.lean | 3 --- 6 files changed, 29 insertions(+), 5 deletions(-) create mode 100644 src/data/finset/repr.lean create mode 100644 src/data/multiset/repr.lean diff --git a/src/data/finset/default.lean b/src/data/finset/default.lean index b8d3d55dabbaf..3f9b319618671 100644 --- a/src/data/finset/default.lean +++ b/src/data/finset/default.lean @@ -8,3 +8,4 @@ import data.finset.pi import data.finset.powerset import data.finset.sort import data.finset.preimage +import data.finset.repr diff --git a/src/data/finset/repr.lean b/src/data/finset/repr.lean new file mode 100644 index 0000000000000..a9c00f2df4afd --- /dev/null +++ b/src/data/finset/repr.lean @@ -0,0 +1,13 @@ +/- +Copyright (c) 2017 Mario Carneiro. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro +-/ +import data.multiset.repr +import data.finset.sort + +/-! +# Representing a finset as a string +-/ + +instance {α : Type*} [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩ diff --git a/src/data/finset/sort.lean b/src/data/finset/sort.lean index 1ced1d74ff4f2..ef925278e56a5 100644 --- a/src/data/finset/sort.lean +++ b/src/data/finset/sort.lean @@ -211,6 +211,4 @@ by simp only [order_emb_of_card_le, rel_embedding.coe_trans, finset.order_emb_of end sort_linear_order -instance [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩ - end finset diff --git a/src/data/multiset/default.lean b/src/data/multiset/default.lean index e73adf88fc396..89048c8d8b8b2 100644 --- a/src/data/multiset/default.lean +++ b/src/data/multiset/default.lean @@ -12,3 +12,4 @@ import data.multiset.pi import data.multiset.powerset import data.multiset.sections import data.multiset.sort +import data.multset.repr diff --git a/src/data/multiset/repr.lean b/src/data/multiset/repr.lean new file mode 100644 index 0000000000000..dcfa41e7df9f6 --- /dev/null +++ b/src/data/multiset/repr.lean @@ -0,0 +1,14 @@ +/- +Copyright (c) 2017 Mario Carneiro. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro +-/ +import data.multiset.sort +import data.string.basic + +/-! +# Representing a multiset as a string +-/ + +instance {α : Type*} [has_repr α] : has_repr (multiset α) := +⟨λ s, "{" ++ string.intercalate ", " ((s.map repr).sort (≤)) ++ "}"⟩ diff --git a/src/data/multiset/sort.lean b/src/data/multiset/sort.lean index df8ecbe0d9e4b..75f51c51287da 100644 --- a/src/data/multiset/sort.lean +++ b/src/data/multiset/sort.lean @@ -50,7 +50,4 @@ list.merge_sort_singleton r a end sort -instance [has_repr α] : has_repr (multiset α) := -⟨λ s, "{" ++ string.intercalate ", " ((s.map repr).sort (≤)) ++ "}"⟩ - end multiset From 674c72a6cef396b4b4a9cc05551977c5e8449ef5 Mon Sep 17 00:00:00 2001 From: ChrisHughes24 Date: Fri, 6 Jan 2023 15:29:16 +0000 Subject: [PATCH 2/5] oops, forgot to remove the import --- src/data/multiset/sort.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/data/multiset/sort.lean b/src/data/multiset/sort.lean index 75f51c51287da..46d74e6c8c3ed 100644 --- a/src/data/multiset/sort.lean +++ b/src/data/multiset/sort.lean @@ -5,7 +5,6 @@ Authors: Mario Carneiro -/ import data.list.sort import data.multiset.basic -import data.string.basic /-! # Construct a sorted list from a multiset. From 6f48bd68843cf34e23a5f7c21ef8e68c02112784 Mon Sep 17 00:00:00 2001 From: ChrisHughes24 Date: Fri, 6 Jan 2023 15:33:37 +0000 Subject: [PATCH 3/5] move repr for cycles --- .../list/{cycle.lean => cycle/basic.lean} | 9 --------- src/data/list/cycle/default.lean | 1 + src/data/list/cycle/repr.lean | 20 +++++++++++++++++++ 3 files changed, 21 insertions(+), 9 deletions(-) rename src/data/list/{cycle.lean => cycle/basic.lean} (98%) create mode 100644 src/data/list/cycle/default.lean create mode 100644 src/data/list/cycle/repr.lean diff --git a/src/data/list/cycle.lean b/src/data/list/cycle/basic.lean similarity index 98% rename from src/data/list/cycle.lean rename to src/data/list/cycle/basic.lean index 60dc82c3a7e7b..47d95dba058a7 100644 --- a/src/data/list/cycle.lean +++ b/src/data/list/cycle/basic.lean @@ -726,15 +726,6 @@ by { rw [←next_reverse_eq_prev, ←mem_reverse_iff], apply next_mem } end decidable -/-- -We define a representation of concrete cycles, available when viewing them in a goal state or -via `#eval`, when over representatble types. For example, the cycle `(2 1 4 3)` will be shown -as `c[1, 4, 3, 2]`. The representation of the cycle sorts the elements by the string value of the -underlying element. This representation also supports cycles that can contain duplicates. --/ -instance [has_repr α] : has_repr (cycle α) := -⟨λ s, "c[" ++ string.intercalate ", " ((s.map repr).lists.sort (≤)).head ++ "]"⟩ - /-- `chain R s` means that `R` holds between adjacent elements of `s`. `chain R ([a, b, c] : cycle α) ↔ R a b ∧ R b c ∧ R c a` -/ diff --git a/src/data/list/cycle/default.lean b/src/data/list/cycle/default.lean new file mode 100644 index 0000000000000..c3f393cabedd3 --- /dev/null +++ b/src/data/list/cycle/default.lean @@ -0,0 +1 @@ +import data.list.cycle.repr diff --git a/src/data/list/cycle/repr.lean b/src/data/list/cycle/repr.lean new file mode 100644 index 0000000000000..83dfe970e2378 --- /dev/null +++ b/src/data/list/cycle/repr.lean @@ -0,0 +1,20 @@ +/- +Copyright (c) 2021 Yakov Pechersky. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yakov Pechersky +-/ +import data.list.cycle.basic +import data.multiset.repr + +/-! +# Representing a cycle as a string +-/ + +/-- +We define a representation of concrete cycles, available when viewing them in a goal state or +via `#eval`, when over representatble types. For example, the cycle `(2 1 4 3)` will be shown +as `c[1, 4, 3, 2]`. The representation of the cycle sorts the elements by the string value of the +underlying element. This representation also supports cycles that can contain duplicates. +-/ +instance {α : Type*} [has_repr α] : has_repr (cycle α) := +⟨λ s, "c[" ++ string.intercalate ", " ((s.map repr).lists.sort (≤)).head ++ "]"⟩ From c36ca578e4f05e984b8095391f0dce61c1b893a2 Mon Sep 17 00:00:00 2001 From: ChrisHughes24 Date: Fri, 6 Jan 2023 15:37:16 +0000 Subject: [PATCH 4/5] repr for prime_multiset --- src/data/pnat/factors.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/data/pnat/factors.lean b/src/data/pnat/factors.lean index 40fd6f53fc58c..8beb547237009 100644 --- a/src/data/pnat/factors.lean +++ b/src/data/pnat/factors.lean @@ -24,10 +24,14 @@ the multiplicity of `p` in this factors multiset being the p-adic valuation of ` /-- The type of multisets of prime numbers. Unique factorization gives an equivalence between this set and ℕ+, as we will formalize below. -/ - @[derive [inhabited, has_repr, canonically_ordered_add_monoid, distrib_lattice, + @[derive [inhabited, canonically_ordered_add_monoid, distrib_lattice, semilattice_sup, order_bot, has_sub, has_ordered_sub]] def prime_multiset := multiset nat.primes +-- We could use the `repr` for multisets here, but we want to reduce imports +instance : has_repr prime_multiset := +⟨λ m, repr ((m.map (coe : nat.primes → nat)).sort (≤))⟩ + namespace prime_multiset /-- The multiset consisting of a single prime -/ From 95856be831b6aaf30260f10d37e1d5e7c1026432 Mon Sep 17 00:00:00 2001 From: ChrisHughes24 Date: Fri, 6 Jan 2023 15:37:57 +0000 Subject: [PATCH 5/5] typo --- src/data/multiset/default.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/multiset/default.lean b/src/data/multiset/default.lean index 89048c8d8b8b2..393b7c1b89825 100644 --- a/src/data/multiset/default.lean +++ b/src/data/multiset/default.lean @@ -12,4 +12,4 @@ import data.multiset.pi import data.multiset.powerset import data.multiset.sections import data.multiset.sort -import data.multset.repr +import data.multiset.repr