Zulip Chat Archive

Stream: general

Topic: finset.bind without decidable_eq


view this post on Zulip Eric Wieser (Jul 23 2020 at 16:10):

How can I define the following without needing decidable_eq?

def bind_prod {α β : Type} (sa : finset α) (fb : α  finset β): finset (α × β)
  := sa.bind(λ a, (fb a).map prod.mk a, begin
    intros _ _ ha,
    exact (prod.mk.inj ha).right,
  end)

Normally sa.bind needs decidable_eq to remove duplicates, but in this case I already know there are no duplicates.

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 16:25):

You can use something like ⟨sa.1.bind _, multiset.nodup_bind.2 _⟩

view this post on Zulip Eric Wieser (Jul 23 2020 at 16:55):

Yeah, that's the route I went:

universes u v w
def bind_prod {α : Type u} {β : Type v} (sa : finset α) (fb : α  finset β) : finset (α × β)
  := 
    sa.val.bind(λ a, ((fb a).map prod.mk a, begin
      intros _ _ ha,
      exact (prod.mk.inj ha).right,
    end).val),
    begin
      rw multiset.nodup_bind,
      split,
      intros a ha,
      exact finset.nodup _,
      refine multiset.pairwise_of_nodup _ (finset.nodup _),
      intros a ha a2 ha2 heq,
      simp only [finset.map_val],
      rw multiset.disjoint_map_map,
      intros b1 hb1 b2 hb2,
      unfold_coes,
      simp only [],
      intro hanother,
      exact heq (prod.mk.inj hanother).left,
    end
  

lemma mem_bind_prod {α : Type u} {β : Type v} (sa : finset α) (fb : α  finset β) (ab : α × β) :
  ab  bind_prod sa fb  ab.fst  sa  ab.snd  fb ab.fst := begin
  unfold bind_prod,
  rw finset.mem_def,
  simp only [],
  rw multiset.mem_bind,
  simp only [ finset.mem_def, finset.mem_map, function.embedding.coe_fn_mk],
  split,
  {
    rintros a, ha, b, hb, rfl,
    rw  finset.mem_def at ha,
    simp only [ha, hb],
  },
  {
    rintros ha, hb,
    rw finset.mem_def at ha,
    use [ab.fst, ha, ab.snd, hb],
    simp only [prod.mk.eta],
  }
end

view this post on Zulip Eric Wieser (Jul 23 2020 at 16:55):

Would this belong in mathlib?

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 16:59):

I guess yes. I'd also add a bind_nodup (s : finset α) (t : α → finset β) (ht : ∀ (i ∈ s) (j ∈ s), i ≠ j → disjoint (t i) (t j)) : finset β as an intermediate definition.

view this post on Zulip Chris Hughes (Jul 23 2020 at 16:59):

This is very close to finset.sigma, which is slightly more general.

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:00):

Can you show me how to express this using finset.sigma?

view this post on Zulip Chris Hughes (Jul 23 2020 at 17:00):

But it's probably worth having.

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:00):

Is prod_bind a good name?

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:00):

Thanks @Chris Hughes !

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:01):

You can do (s.sigma t).map (equiv.sigma_equiv_prod _ _).to_embedding

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:03):

Sweet, thanks!

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:14):

I end up stuck trying to prove ⊢ (equiv.sigma_equiv_prod α β).to_fun ⟨ab.fst, ab.snd⟩ = ab if I go down that route

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:14):

Which looks like a trivial statement

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:16):

Does simp work?

view this post on Zulip Chris Hughes (Jul 23 2020 at 17:16):

I think this is prod.eta

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:17):

No, it doesn't

view this post on Zulip Chris Hughes (Jul 23 2020 at 17:17):

Or sigma.eta

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:17):

The angle brackets are sigma.mk

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:17):

but ab is a prod

view this post on Zulip Chris Hughes (Jul 23 2020 at 17:17):

So it's prod.eta I think.

view this post on Zulip Chris Hughes (Jul 23 2020 at 17:17):

apply prod.eta should work hopefully.

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:17):

While you're at it, please rewrite equiv.sigma_equiv_prod to avoid λ ⟨a, b⟩

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:18):

Use λ a, (a.1, b.1) instead.

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:18):

prod.eta doesn't exist

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:19):

prod.mk.eta does the trick though!

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:19):

sigma_equiv_prod is missing simp lemmas.

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:20):

Goign the other way, how can I extract (a, b) = ab from h: ⇑(equiv.sigma_equiv_prod α β) ⟨a, b⟩ = ab?

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:21):

The whole sigma/psigma section of data/equiv/basic should be fixed to (a) don't use λ ⟨a, b⟩; (b) have simp lemmas.

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:21):

Is λ ⟨a, b⟩ always an antipattern?

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:22):

Using λ ⟨a, b⟩, _ is a bad idea whenever you care about definitional equality of the result.

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:22):

I.e., when you define a function. It's OK in a proof.

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:24):

The main problem with def f : α × β → α := λ ⟨a, b⟩, a is that f p is not defeq p.1.

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:24):

But f (a, b) is defeq f a.

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:29):

Ok, my end result is

universes u v w
def bind_prod {α : Type u} {β : Type v} (sa : finset α) (fb : α  finset β) : finset (α × β)
  := (sa.sigma fb).map (equiv.sigma_equiv_prod _ _).to_embedding

lemma mem_bind_prod {α : Type u} {β : Type v} (sa : finset α) (fb : α  finset β) (ab : α × β) :
  ab  bind_prod sa fb  ab.fst  sa  ab.snd  fb ab.fst
:= begin
  unfold bind_prod,
  rw finset.mem_map,
  simp only [exists_prop, sigma.exists, finset.mem_sigma, equiv.to_embedding_coe_fn, equiv.sigma_equiv_prod, equiv.coe_fn_mk],
  split,
  {
    rintros a, b, ha, hb, h,
    simp only [ h],
    exact ha, hb,
  },
  {
    rintros ha, hb,
    use [ab.fst, ab.snd],
    simp only [ha, hb, true_and, prod.mk.eta],
  },
end

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:42):

It seems like I ought to be able to use the reverse equivalence to simplify the lemma there, but I don't see how.

view this post on Zulip Eric Wieser (Jul 23 2020 at 17:49):

Yury G. Kudryashov said:

While you're at it, please rewrite equiv.sigma_equiv_prod to avoid λ ⟨a, b⟩

I don't feel confident doing this - perhaps worth opening a github issue so that it's not forgotten about?

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 18:14):

It was easier to PR it: #3530

view this post on Zulip Jannis Limperg (Jul 23 2020 at 18:58):

Yury G. Kudryashov said:

The main problem with def f : α × β → α := λ ⟨a, b⟩, a is that f p is not defeq p.1.

Do we have an issue for this? Is there any reason (except effort) not to redefine pattern-matching lambdas so that they desugar to projections?

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 19:25):

@Gabriel Ebner :up: Do I understand correctly that this should be possible if the source type has only one constructor?

view this post on Zulip Mario Carneiro (Jul 24 2020 at 03:48):

also the type has to be large eliminating (i.e. not Exists)

view this post on Zulip Mario Carneiro (Jul 24 2020 at 03:48):

in fact it should probably be restricted to structures anyway since one-constructor inductives don't have standard projections

view this post on Zulip Mario Carneiro (Jul 24 2020 at 03:50):

This is not the desired behavior for programming uses though, I'm not sure how I feel about destructuring let doing this all the time

view this post on Zulip Mario Carneiro (Jul 24 2020 at 03:52):

actually I take it back, as long as let (x, y) := s in t x y expands to (\lam p, t p.1 p.2) sit should have the right VM-computational behavior

view this post on Zulip Gabriel Ebner (Jul 24 2020 at 08:48):

I think the VM generates special instructions for projections (i.e. access one field) that are different from the ones generated by pattern-matching (i.e. destruct the object and put all fields on the stack).

view this post on Zulip Gabriel Ebner (Jul 24 2020 at 08:49):

But I'm still open to a PR that turns λ ⟨a,b⟩, a into a projection, given the nicer definitional reduction.

view this post on Zulip Reid Barton (Jul 25 2020 at 02:10):

I've also requested this feature in the past but at this point my main concern with it is a migration plan for Lean 4


Last updated: May 06 2021 at 22:13 UTC