feat(data/list/pi): new file #18417

negiizhao · 2023-02-10T06:09:06Z

This file is an analog of data.multiset.pi. ~~But this PR only adds some basic lemmas for #18315.~~

Move fin_enum.pi.* into this file. (nothing imports fin_enum!)

src/data/list/pi.lean

eric-wieser

Can you add a lemma in multiset.pi that links list.pi.cons with multiset.pi.cons when m = coe l?

negiizhao · 2023-02-11T00:21:05Z

multiset.pi has already been ported to mathlib4.

eric-wieser · 2023-02-11T11:58:11Z

src/data/list/pi.lean

+/-- Given `α : ι → Sort*`, a list `l` and a term `i`, as well as a term `a : α i` and a
+function `f` such that `f j : α j` for all `i'` in `m`, `pi.cons a f` is a function `g` such
+that `g i'' : α i''` for all `i''` in `i :: l`. -/
+def cons (a : α i) (f : Π j ∈ l, α j) : Π j ∈ (i :: l), α j :=


l should be explicit to match the multiset version

In most cases it can be inferred automatically. Is there any disadvantage to making it implicit in multiset.pi.cons?

Yes, it requires making large changes to multiset.pi.cons which is already a ported file.

eric-wieser

I think we should modify multiset.pi anyway, and implement it as

quotient.rec_on m (λ l, @list.pi.cons _ _ _ _ l b) sorry

eric-wieser · 2023-02-11T12:16:23Z

Or perhaps an easier option,

def list.pi.cons (l : list ι) {i : ι} (a : α i) (f : Π j ∈ l, α j) : Π j ∈ (i :: l), α j :=
multiset.pi.cons ↑l _ a f

eric-wieser · 2023-02-11T12:18:08Z

Which leads to the question: why do you actually need this?

negiizhao · 2023-02-11T23:03:07Z

There is no multiset.pi.map_cons and multiset.pi.forall_rel_cons_ext in mathlib. We need to add some similar lemmas in any case, and I'm not sure it is a good idea to use multiset lemmas for lists. BTW it seems difficult to build APIs directly for multiset in subsequent PR (multiset.rec_on introduces annoying heq).

eric-wieser · 2023-02-11T23:36:52Z

There is no multiset.pi.map_cons and multiset.pi.forall_rel_cons_ext in mathlib.

It sounds to me like you should add these lemmas first.

eric-wieser · 2023-02-11T23:41:17Z

src/data/list/pi.lean

+@[simp] lemma cons_eta (f : Π j ∈ (i :: l), α j) :
+  cons (f i (mem_cons_self _ _)) (λ j hj, f j (mem_cons_of_mem _ hj)) = f :=


This lemma is multiset.pi.cons_ext

eric-wieser · 2023-02-11T23:51:24Z

src/data/list/pi.lean

+function `f` such that `f j : α j` for all `i'` in `m`, `pi.cons a f` is a function `g` such
+that `g i'' : α i''` for all `i''` in `i :: l`. -/
+def cons (a : α i) (f : Π j ∈ l, α j) : Π j ∈ (i :: l), α j :=
+λ j hj, if h : j = i then h.symm.rec a else f j (hj.resolve_left h)


with #18429,

Suggested change

λ j hj, if h : j = i then h.symm.rec a else f j (hj.resolve_left h)

multiset.pi.cons ↑l _ a f

eric-wieser · 2023-02-12T00:12:30Z

src/data/list/pi.lean

+  (λ j hj, f ((cons h t) j hj)) = cons (f h) (λ j hj, f (t j hj)) :=
+by { ext j hj, dsimp [cons], split_ifs with H, { cases H, refl }, { refl }, }


More lines but fewer tactics:

Suggested change

(λ j hj, f ((cons h t) j hj)) = cons (f h) (λ j hj, f (t j hj)) :=

by { ext j hj, dsimp [cons], split_ifs with H, { cases H, refl }, { refl }, }

(λ j hj, f ((cons h t) j hj)) = cons (f h) (λ j hj, f (t j hj)) :=

begin

ext j hj,

refine (apply_dite (@f _) _ _ _).trans (congr_arg2 _ _ rfl),

ext rfl,

refl,

end

Is there a reason you don't state it as

f ((cons h t) j hj) = cons (f h) (λ j hj, f (t j hj)) j hj :=

which looks better for forward rewrites

In #18315 I use it for a backward rewrite. Maybe I should swap its sides.

eric-wieser · 2023-02-12T00:57:08Z

list.pi.cons already exists, it's fin_enum.pi.cons.

…18429) Everything in this file about `multiset.pi.cons` generalizes to `Sort`. The parts of the file which don't generalize now use `β` instead. This is motivated by #18417, though I do not know if supporting `Sort` is actually important there. Forward-ported as leanprover-community/mathlib4#2220

This discard the changes from #18429, as these are already present in the new version.

Parcly-Taxel · 2023-05-14T08:18:57Z

What is the status of this PR? It's apparently needed for leanprover-community/mathlib4#3971.

eric-wieser · 2023-05-14T13:05:21Z

I think I'd like to split this PR into:

Move the existing definitions into a new file, with no modifications
Do the API cleanups

I think this will make it easier to forward-port.

eric-wieser · 2023-05-19T18:09:45Z

src/data/multiset/pi.lean

There's still too much going on in this file. I've created #19050 which captures the renames and the more obvious moves.

semorrison · 2023-07-27T08:54:21Z

Closing, replaced by leanprover-community/mathlib4#5549. Please reopen and ping me if this is incorrect!

negiizhao added 2 commits February 10, 2023 14:03

feat(data/list/pi): new file

62ed6b5

golf

7a4901c

negiizhao added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Feb 10, 2023

negiizhao mentioned this pull request Feb 10, 2023

feat(data/*/quot): quotient_lift on a finite family #18315

Closed

2 tasks

negiizhao removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Feb 10, 2023

eric-wieser reviewed Feb 10, 2023

View reviewed changes

src/data/list/pi.lean Show resolved Hide resolved

eric-wieser reviewed Feb 10, 2023

View reviewed changes

eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Feb 10, 2023

add list.pi.nil

70b3170

negiizhao added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Feb 11, 2023

eric-wieser reviewed Feb 11, 2023

View reviewed changes

eric-wieser reviewed Feb 12, 2023

View reviewed changes

eric-wieser mentioned this pull request Feb 12, 2023

[Merged by Bors] - chore(data/{multiset,finset}/pi): generalize from Type to Sort #18429

Closed

negiizhao added 2 commits February 12, 2023 10:19

a lot of changes...

15b6f72

lemmas & golf

fb680cb

eric-wieser added 2 commits March 1, 2023 19:30

Merge remote-tracking branch 'origin/master' into FR_list_pi

1ffd02e

This discard the changes from #18429, as these are already present in the new version.

move lemma

bae13ee

Merge remote-tracking branch 'origin/master' into FR_list_pi

ccc7985

github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label May 19, 2023

eric-wieser reviewed May 19, 2023

View reviewed changes

eric-wieser mentioned this pull request May 19, 2023

[Merged by Bors] - chore(data/multiset/pi): correct names and reorder #19050

Closed

Merge remote-tracking branch 'origin/master' into FR_list_pi

cc69f4e

collares mentioned this pull request May 22, 2023

[Merged by Bors] - feat: port Data.Fintype.Quotient leanprover-community/mathlib4#3971

Closed

eric-wieser added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 15, 2023

semorrison closed this Jul 27, 2023

YaelDillies deleted the FR_list_pi branch November 18, 2023 11:29

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(data/list/pi): new file #18417

feat(data/list/pi): new file #18417

negiizhao commented Feb 10, 2023 •

edited

eric-wieser left a comment •

edited

negiizhao commented Feb 11, 2023

eric-wieser Feb 11, 2023

negiizhao Feb 12, 2023

eric-wieser Mar 1, 2023 •

edited

eric-wieser left a comment

eric-wieser commented Feb 11, 2023 •

edited

eric-wieser commented Feb 11, 2023

negiizhao commented Feb 11, 2023

eric-wieser commented Feb 11, 2023

eric-wieser Feb 11, 2023

eric-wieser Feb 11, 2023

eric-wieser Feb 12, 2023

negiizhao Feb 12, 2023

eric-wieser commented Feb 12, 2023 •

edited

Parcly-Taxel commented May 14, 2023

eric-wieser commented May 14, 2023

eric-wieser May 19, 2023

semorrison commented Jul 27, 2023

		@[simp] lemma cons_eta (f : Π j ∈ (i :: l), α j) :
		cons (f i (mem_cons_self _ _)) (λ j hj, f j (mem_cons_of_mem _ hj)) = f :=

	λ j hj, if h : j = i then h.symm.rec a else f j (hj.resolve_left h)
	multiset.pi.cons ↑l _ a f

		(λ j hj, f ((cons h t) j hj)) = cons (f h) (λ j hj, f (t j hj)) :=
		by { ext j hj, dsimp [cons], split_ifs with H, { cases H, refl }, { refl }, }

feat(data/list/pi): new file #18417

feat(data/list/pi): new file #18417

Conversation

negiizhao commented Feb 10, 2023 • edited

eric-wieser left a comment • edited

Choose a reason for hiding this comment

negiizhao commented Feb 11, 2023

eric-wieser Feb 11, 2023

Choose a reason for hiding this comment

negiizhao Feb 12, 2023

Choose a reason for hiding this comment

eric-wieser Mar 1, 2023 • edited

Choose a reason for hiding this comment

eric-wieser left a comment

Choose a reason for hiding this comment

eric-wieser commented Feb 11, 2023 • edited

eric-wieser commented Feb 11, 2023

negiizhao commented Feb 11, 2023

eric-wieser commented Feb 11, 2023

eric-wieser Feb 11, 2023

Choose a reason for hiding this comment

eric-wieser Feb 11, 2023

Choose a reason for hiding this comment

eric-wieser Feb 12, 2023

Choose a reason for hiding this comment

negiizhao Feb 12, 2023

Choose a reason for hiding this comment

eric-wieser commented Feb 12, 2023 • edited

Parcly-Taxel commented May 14, 2023

eric-wieser commented May 14, 2023

eric-wieser May 19, 2023

Choose a reason for hiding this comment

semorrison commented Jul 27, 2023

negiizhao commented Feb 10, 2023 •

edited

eric-wieser left a comment •

edited

eric-wieser Mar 1, 2023 •

edited

eric-wieser commented Feb 11, 2023 •

edited

eric-wieser commented Feb 12, 2023 •

edited