## 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_gens, 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 Sorts; 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 swaps

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