# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: quotient by product relation

#### Junyan Xu (Aug 24 2020 at 04:40):

Is this anywhere in the Lean library? I managed to prove it using only `quot.sound`

without `propext`

. If r₁ and r₂ are setoids, there is a simpler proof using `quotient.exact`

, which however depends on `propext`

. The setoid version for Pi types also holds (requires `quotient.choice`

; is this in the library?), but if the relations are only reflexive, the kernels of the quotients are the equivalence relations generated by the respective relations (`eqv_gen`

), but the `eqv_gen`

of the product relation doesn't necessarily equal the product of the `eqv_gen`

s, because it can take any number of steps to reach a pair of elements in the transitive closure, and across different coordinates, these numbers may well be unbounded.

```
import tactic
def rprod {α₁: Sort u} {α₂: Sort v} (r₁: α₁ → α₁ → Prop) (r₂: α₂ → α₂ → Prop)
:= λa a': pprod α₁ α₂, r₁ a.1 a'.1 ∧ r₂ a.2 a'.2
lemma prod_quot {α₁: Sort u} {α₂: Sort v} (r₁: α₁ → α₁ → Prop) (r₂: α₂ → α₂ → Prop)
(hr: reflexive r₁ ∧ reflexive r₂): quot (rprod r₁ r₂) ≃ pprod (quot r₁) (quot r₂) :=
begin
constructor, swap 3,
{ set f := λa: pprod α₁ α₂, pprod.mk (quot.mk r₁ a.1) (quot.mk r₂ a.2) with hf,
refine quot.lift f _, intros a b h, simp [hf],
congr' 1; apply quot.sound, exacts [h.1, h.2] },
swap 3, { set g := λa₁ a₂, quot.mk (rprod r₁ r₂) (pprod.mk a₁ a₂) with hg,
set g' := λa₁, @quot.lift _ r₂ _ (g a₁) _ with hg',
refine λa, (@quot.lift _ r₁ _ g' _) a.1 a.2, rw hg', swap,
intros a a' h, apply quot.sound, exact ⟨hr.1 a₁, h⟩,
intros a a' h, apply funext, apply quot.ind, intro a₂,
simp [hg], exact quot.sound ⟨h, hr.2 a₂⟩ },
{ apply quot.ind, simp, intro a, cases a, triv },
{ intro a, cases a, revert a_fst, apply quot.ind, intro a,
revert a_snd, simp, apply quot.ind, dsimp, intro a, refl }
end
#print axioms prod_quot -- quot.sound
```

I appreciate any simplification of the proof. Moreover, if I replace the last line with `revert a_snd, apply quot.ind, simp }`

the proof still works but will then depend on `propext`

. I am not experienced enough to track down the problem, so help is appreciated.

#### Mario Carneiro (Aug 24 2020 at 04:42):

No, I don't think this has been proved in mathlib

#### Mario Carneiro (Aug 24 2020 at 04:44):

What's your #mwe header? I can't find `rprod`

#### Mario Carneiro (Aug 24 2020 at 04:47):

I found `prod.rprod`

but it doesn't work on `Sort`

s; it looks like you are using `pprod`

but there is no `pprod.rprod`

that has been proved AFAICT

#### Junyan Xu (Aug 24 2020 at 04:49):

Sorry,

```
def rprod {α₁: Sort u} {α₂: Sort v} (r₁: α₁ → α₁ → Prop) (r₂: α₂ → α₂ → Prop)
:= λa a': pprod α₁ α₂, r₁ a.1 a'.1 ∧ r₂ a.2 a'.2
```

#### Mario Carneiro (Aug 24 2020 at 04:50):

You should start the proof with `fconstructor`

to skip the `swap`

s

#### Mario Carneiro (Aug 24 2020 at 04:53):

also the `hr`

hypothesis should be two hypotheses

#### Mario Carneiro (Aug 24 2020 at 04:54):

As for avoiding propext, tactics use it all the time. You will have a bad day trying to avoid it unless you rewrite some of the core algorithms

#### Mario Carneiro (Aug 24 2020 at 04:55):

you can remove the `dsimp`

on the last line though

#### Mario Carneiro (Aug 24 2020 at 04:57):

you can replace the coherence proofs at the end with

```
{ rintro ⟨⟨a, b⟩⟩, refl },
{ rintro ⟨⟨a⟩, ⟨b⟩⟩, refl }
```

Did I mention that `rcases`

(or `rintro`

in this guise) is awesome?

#### Mario Carneiro (Aug 24 2020 at 05:10):

Here's a compression pass:

```
def prod_quot {α₁ α₂} (r₁ : α₁ → α₁ → Prop) (r₂ : α₂ → α₂ → Prop)
(hr₁: reflexive r₁) (hr₂ : reflexive r₂) : quot (rprod r₁ r₂) ≃ pprod (quot r₁) (quot r₂) :=
{ to_fun := quot.lift (λa: pprod α₁ α₂, pprod.mk (quot.mk r₁ a.1) (quot.mk r₂ a.2)) $
by intros a b h; dsimp only; rw [quot.sound h.1, quot.sound h.2],
inv_fun := λ ⟨a, b⟩, begin
refine (quot.lift (λa₁, quot.lift (λ a₂, quot.mk _ (pprod.mk a₁ a₂)) _) _) a b,
{ exact λ a a' h, quot.sound ⟨hr₁ a₁, h⟩ },
{ intros a a' h, ext ⟨a₂⟩, exact quot.sound ⟨h, hr₂ a₂⟩ }
end,
left_inv := by rintro ⟨⟨a, b⟩⟩; refl,
right_inv := by rintro ⟨⟨a⟩, ⟨b⟩⟩; refl }
```

#### Mario Carneiro (Aug 24 2020 at 05:11):

`ext ⟨a₂⟩,`

, also brought to you by rcases

#### Mario Carneiro (Aug 24 2020 at 05:11):

abbreviating `apply funext, apply quot.ind, intro a₂,`

from the original proof

#### Scott Morrison (Aug 24 2020 at 10:10):

I really like `ext ⟨a₂⟩`

. It is really useful. Another place that parser would be helpful is in `choose`

.

#### Mario Carneiro (Aug 24 2020 at 19:23):

I actually thought about adding it when I was working on `choose!`

, but it conflicts with the current syntax a bit

#### Junyan Xu (Aug 24 2020 at 19:58):

Pi type version

```
import tactic
universes u v
noncomputable def pi_setoid_quot {α : Sort u} {β : α → Sort v} [S : Π a, setoid (β a)] :
@quotient (Π a, β a) pi_setoid ≃ Π a, quotient (S a) :=
{ to_fun := quotient.lift (λ (f : Π a, β a) a, ⟦f a⟧) (λ_ _ h, funext (λa, quot.sound (h a))),
inv_fun := λf, ⟦λa, (f a).out⟧,
left_inv := by rintro ⟨f⟩; exact quot.sound (λa, quotient.mk_out _),
right_inv := by intro; ext; simp }
#print axioms pi_setoid_quot -- all three
#print axioms quotient.mk_out -- choice, propext; incorporates exactness
```

Last updated: May 07 2021 at 22:14 UTC