finset.bind without decidable_eq

Stream: general

[Eric Wieser]

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.

[Yury G. Kudryashov]

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

[Eric Wieser]

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

[Eric Wieser]

Would this belong in mathlib?

[Yury G. Kudryashov]

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.

[Chris Hughes]

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

[Eric Wieser]

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

[Chris Hughes]

But it's probably worth having.

[Eric Wieser]

Is prod_bind a good name?

[Yury G. Kudryashov]

Thanks @Chris Hughes !

[Yury G. Kudryashov]

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

[Eric Wieser]

Sweet, thanks!

[Eric Wieser]

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

[Eric Wieser]

Which looks like a trivial statement

[Yury G. Kudryashov]

Does simp work?

[Chris Hughes]

I think this is prod.eta

[Eric Wieser]

No, it doesn't

[Chris Hughes]

Or sigma.eta

[Eric Wieser]

The angle brackets are sigma.mk

[Eric Wieser]

but ab is a prod

[Chris Hughes]

So it's prod.eta I think.

[Chris Hughes]

apply prod.eta should work hopefully.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Eric Wieser]

prod.eta doesn't exist

[Eric Wieser]

prod.mk.eta does the trick though!

[Yury G. Kudryashov]

sigma_equiv_prod is missing simp lemmas.

[Eric Wieser]

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

[Yury G. Kudryashov]

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

[Eric Wieser]

Is λ ⟨a, b⟩ always an antipattern?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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?

[Yury G. Kudryashov]

It was easier to PR it: #3530

[Jannis Limperg]

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?

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Gabriel Ebner]

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).

[Gabriel Ebner]

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

[Reid Barton]

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