Conversation
|
|
| /-- 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 := |
There was a problem hiding this comment.
l should be explicit to match the multiset version
There was a problem hiding this comment.
In most cases it can be inferred automatically. Is there any disadvantage to making it implicit in multiset.pi.cons?
There was a problem hiding this comment.
Yes, it requires making large changes to multiset.pi.cons which is already a ported file.
eric-wieser
left a comment
There was a problem hiding this comment.
I think we should modify multiset.pi anyway, and implement it as
quotient.rec_on m (λ l, @list.pi.cons _ _ _ _ l b) sorry
|
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 |
|
Which leads to the question: why do you actually need this? |
|
There is no |
It sounds to me like you should add these lemmas first. |
src/data/list/pi.lean
Outdated
| @[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 := |
There was a problem hiding this comment.
This lemma is multiset.pi.cons_ext
src/data/list/pi.lean
Outdated
| 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) |
There was a problem hiding this comment.
with #18429,
| λ j hj, if h : j = i then h.symm.rec a else f j (hj.resolve_left h) | |
| multiset.pi.cons ↑l _ a f |
src/data/list/pi.lean
Outdated
| (λ 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 }, } |
There was a problem hiding this comment.
More lines but fewer tactics:
| (λ 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
There was a problem hiding this comment.
In #18315 I use it for a backward rewrite. Maybe I should swap its sides.
|
|
…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.
|
What is the status of this PR? It's apparently needed for leanprover-community/mathlib4#3971. |
|
I think I'd like to split this PR into:
I think this will make it easier to forward-port. |
There was a problem hiding this comment.
There's still too much going on in this file. I've created #19050 which captures the renames and the more obvious moves.
|
Closing, replaced by leanprover-community/mathlib4#5549. Please reopen and ping me if this is incorrect! |
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 importsfin_enum!)