Zulip Chat Archive

Stream: Is there code for X?

Topic: Copying projections through a definition


view this post on Zulip Eric Wieser (Sep 17 2020 at 18:31):

In congruence.lean, there are definitions like

  /-- Defining the quotient by a ring congruence relation of a type with a multiplication. -/
  protected def quotient := quotient $ c.to_setoid

  /-- The function on the quotient by a congruence relation `c` induced by a function that is
      constant on `c`'s equivalence classes. -/
  @[elab_as_eliminator]
  protected def lift_on {β} {c : ring_con M} (q : c.quotient) (f : M  β)
    (h :  a b, c a b  f a = f b) : β := quotient.lift_on' q f h

  /-- The binary function on the quotient by a ring congruence relation `c` induced by a binary function
      that is constant on `c`'s equivalence classes. -/
  @[elab_as_eliminator]
  protected def lift_on₂ {β} {c : ring_con M} (q r : c.quotient) (f : M  M  β)
    (h :  a₁ a₂ b₁ b₂, c a₁ b₁  c a₂ b₂  f a₁ a₂ = f b₁ b₂) : β := quotient.lift_on₂' q r f h

This seems awfully verbose. Is there a way of telling lean that when I write def quotient := quotient $ c.to_setoid I also want to copy over a bunch of the projections?

view this post on Zulip Eric Wieser (Sep 17 2020 at 18:31):

And if not, is there a way I can at least avoid writing out the full lemma each time?


Last updated: May 16 2021 at 05:21 UTC