pattern matching quotient

Stream: general

[Bernd Losert]

I'm trying to do the following but it doesn't work:

constant r : nat -> nat -> Prop

def foo (x : quot r) : nat := match x with
| (quot.mk r x') := 0
end

What is the correct way to do this?

[Yakov Pechersky]

The error says, quot.mk is not a pattern. What that means is that you can't use it on as a pattern of deconstruction in a match statement. Here is one option:

-- not constant, so that foo can be computable
def r : nat -> nat -> Prop := sorry

def foo (x : quot r) : nat :=
quot.hrec_on x
  (λ nat_from_my_quot, 0) -- my function from the underlying nat inside the quot
  begin
    -- here we must prove that my function would have given the same output
    -- regardless of what precise nat was inside the quot, as long as
    -- other nats that satisfy `r` would also give the same output
    intros,
    refine heq_of_eq _,
    simp
  end

[Bernd Losert]

So you're saying that I have to use the recursor when dealing with quotients?

[Yakov Pechersky]

No, not necessarily. You could use something like docs#quotient.map or docs#quot.map

[Yakov Pechersky]

There are many helper functions built on top of the recursor.

[Bernd Losert]

Alright. Thanks a lot.

[Yury G. Kudryashov]

When you define a function on a quotient, you can't just say f ⟦x⟧ = g x. You also need to prove x ≈ y → g x = g y. Pattern matching doesn't have syntax for that.

[Yury G. Kudryashov]

You need to use, e.g., docs#quot.lift_on to define f.