Zulip Chat Archive

Stream: Is there code for X?

Topic: dfinsupp of product is dfinsupp of dfinsupp


view this post on Zulip Eric Wieser (Jul 21 2020 at 11:39):

Is there anything in mathlib resembling the sorry here?

import data.dfinsupp
import tactic

universes u v w

variables {ii : Type u} {jj : Type v} [decidable_eq ii] [decidable_eq jj]
variables (β : ii  jj  Type w) [Π i j, has_zero (β i j)]

example : (Π (ij : ii × jj), β ij.1 ij.2)  Π i, Π j, β i j := sorry

view this post on Zulip Scott Morrison (Jul 21 2020 at 12:29):

Quite possibly not. dfinsupp is not very well developed.

view this post on Zulip Eric Wieser (Jul 21 2020 at 14:07):

Is the right statement to try to make?

view this post on Zulip Scott Morrison (Jul 21 2020 at 14:10):

Depends what you need it for. Lots of algebra structures are going to be compatible with this equivalence, too.

view this post on Zulip Eric Wieser (Jul 21 2020 at 16:26):

I can make a start on this with:

def prod_to_nested (f : Π (ij : ii × jj), β ij.1 ij.2) : Π i, Π j, β i j := begin
    fapply quotient.lift_on f,
    exact λ fij, {
        to_fun := λ i,  {
            to_fun := λ j, fij.to_fun (i, j),
            pre_support := fij.pre_support.map (λ (ij : ii × jj), ij.snd),
            zero := λ j, begin
                obtain hin | h0 := fij.zero (i, j),
                {apply or.inl, rw multiset.mem_map, use (i, j), simp only [hin, eq_self_iff_true, and_self]},
                {exact or.inr h0},
            end
        } ,
        pre_support := fij.pre_support.map (λ ij, ij.fst),
        zero := λ i, begin
            have h := λ j, fij.zero (i, j),
            rw multiset.mem_map,
            sorry
        end
    },
    exact λ a b H, quotient.sound $ λ i, by {
        simp [H (i, _)],
        exact λ j, by simp [H (i, j)]
    },
end

although this all feels super awkward

view this post on Zulip Eric Wieser (Jul 21 2020 at 18:27):

Updated the above to be sorry-free, would appreciate feedback on whether I'm missing a trick.
In paticular, the λ j, (fij.zero (i, j)).elim proof is repeated twice, and I'm not sure how to remove it.

view this post on Zulip Eric Wieser (Jul 21 2020 at 19:30):

The other direction is proving even more challenging:

def nested_to_prod (f : Π i j, β i j) : Π (ij : ii × jj), β ij.1 ij.2 := begin
    fapply quotient.lift_on f,
    {
        intro fi,
        refine {
            to_fun := λ ij, fi.to_fun ij.fst ij.snd,
            pre_support := fi.pre_support.product (begin
                let j_sets := fi.pre_support.map (λ i, begin
                    let fi_val := (fi.to_fun i),
                    /- This is unprovable, I think lift_on is the wrong approach, or I need to return a clever quotient -/
                    exact quotient.lift_on fi_val
                        dfinsupp.pre.pre_support
                        (λ a b H, begin
                            sorry
                        end)
                end),
                /- should be union of j_sets -/
                exact (sorry : multiset jj),
            end),
            zero := λ ij, begin
                rw multiset.mem_product,
                cases fi.zero ij.fst,
                { left, simp [h], sorry},
                { right, simp [h] }
            end
        },
    },
    exact λ a b H, quotient.sound $ λ ij, by simp [H ij.fst],
end

view this post on Zulip Eric Wieser (Jul 22 2020 at 11:51):

Would this be more suited to #general, now that it's established the answer to "is there code for X in mathlib" is no?

view this post on Zulip Johan Commelin (Jul 22 2020 at 11:52):

Yes, or #maths

view this post on Zulip Eric Wieser (Jul 22 2020 at 11:52):

Shall I repost, or ask someone with the magic bit to move it?

view this post on Zulip Johan Commelin (Jul 22 2020 at 11:52):

I think reposting is easier

view this post on Zulip Johan Commelin (Jul 22 2020 at 11:52):

Just add a link to this thread

view this post on Zulip Eric Wieser (Jul 22 2020 at 12:14):

Posted as https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/dfinsupp.20of.20product.20is.20dfinsupp.20of.20dfinsupp


Last updated: May 07 2021 at 21:10 UTC