## Stream: general

### Topic: finset.bind without decidable_eq

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

#### Yury G. Kudryashov (Jul 23 2020 at 16:25):

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

#### 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


#### Eric Wieser (Jul 23 2020 at 16:55):

Would this belong in mathlib?

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

#### Chris Hughes (Jul 23 2020 at 16:59):

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

#### Eric Wieser (Jul 23 2020 at 17:00):

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

#### Chris Hughes (Jul 23 2020 at 17:00):

But it's probably worth having.

#### Eric Wieser (Jul 23 2020 at 17:00):

Is prod_bind a good name?

#### Yury G. Kudryashov (Jul 23 2020 at 17:00):

Thanks @Chris Hughes !

#### Yury G. Kudryashov (Jul 23 2020 at 17:01):

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

Sweet, thanks!

#### 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

#### Eric Wieser (Jul 23 2020 at 17:14):

Which looks like a trivial statement

#### Yury G. Kudryashov (Jul 23 2020 at 17:16):

Does simp work?

#### Chris Hughes (Jul 23 2020 at 17:16):

I think this is prod.eta

No, it doesn't

#### Chris Hughes (Jul 23 2020 at 17:17):

Or sigma.eta

#### Eric Wieser (Jul 23 2020 at 17:17):

The angle brackets are sigma.mk

#### Eric Wieser (Jul 23 2020 at 17:17):

but ab is a prod

#### Chris Hughes (Jul 23 2020 at 17:17):

So it's prod.eta I think.

#### Chris Hughes (Jul 23 2020 at 17:17):

apply prod.eta should work hopefully.

#### Yury G. Kudryashov (Jul 23 2020 at 17:17):

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

#### Yury G. Kudryashov (Jul 23 2020 at 17:18):

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

#### Eric Wieser (Jul 23 2020 at 17:18):

prod.eta doesn't exist

#### Eric Wieser (Jul 23 2020 at 17:19):

prod.mk.eta does the trick though!

#### Yury G. Kudryashov (Jul 23 2020 at 17:19):

sigma_equiv_prod is missing simp lemmas.

#### 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?

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

#### Eric Wieser (Jul 23 2020 at 17:21):

Is λ ⟨a, b⟩ always an antipattern?

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

#### Yury G. Kudryashov (Jul 23 2020 at 17:22):

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

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

#### Yury G. Kudryashov (Jul 23 2020 at 17:24):

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

#### 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


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

#### 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?

#### Yury G. Kudryashov (Jul 23 2020 at 18:14):

It was easier to PR it: #3530

#### 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?

#### 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?

#### Mario Carneiro (Jul 24 2020 at 03:48):

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

#### 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

#### 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

#### 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

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

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

#### 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