Zulip Chat Archive

Stream: Is there code for X?

Topic: quotient by product relation


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 24 2020 at 04:42):

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

view this post on Zulip Mario Carneiro (Aug 24 2020 at 04:44):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 24 2020 at 04:50):

You should start the proof with fconstructor to skip the swaps

view this post on Zulip Mario Carneiro (Aug 24 2020 at 04:53):

also the hr hypothesis should be two hypotheses

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 24 2020 at 04:55):

you can remove the dsimp on the last line though

view this post on Zulip 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?

view this post on Zulip 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 }

view this post on Zulip Mario Carneiro (Aug 24 2020 at 05:11):

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

view this post on Zulip Mario Carneiro (Aug 24 2020 at 05:11):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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