quotient by product relation

Stream: Is there code for X?

[Junyan Xu]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

You should start the proof with fconstructor to skip the swaps

[Mario Carneiro]

also the hr hypothesis should be two hypotheses

[Mario Carneiro]

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]

you can remove the dsimp on the last line though

[Mario Carneiro]

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]

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]

ext ⟨a₂⟩,, also brought to you by rcases

[Mario Carneiro]

abbreviating apply funext, apply quot.ind, intro a₂, from the original proof

[Scott Morrison]

I really like ext ⟨a₂⟩. It is really useful. Another place that parser would be helpful is in choose.

[Mario Carneiro]

I actually thought about adding it when I was working on choose!, but it conflicts with the current syntax a bit

[Junyan Xu]

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