Pattern matching on quotient types

Stream: new members

[Brandon Harad]

I am trying to define the integers with a quotient (of pairs of naturals) instead of with an inductive type as an exercise. I would like to make a function which pattern matches inputs based on my defined constants and then proceeds recursively. For example, consider the following function on my quotient type Z:

def mult2 : Z → Z
  | 0 => 0
  | z + 1 => 2 + mult2 z
  | z - 1 => -2 + mult2 z

I have already implemented addition, ofNat, etc in a sensible manner. How can I do this?

[Kevin Buzzard]

You'll have to ask someone more CS-oriented about how to get the notation working (if indeed it's even possible) but there's nothing stopping you defining MyInt.pos_neg_rec or whatever you want to call it, which eats a type X, a term x0 : X and two functions Nat x X -> X, and spits out a function Int -> X satisfying the identities you want; you can then define functions recursively using this.

[Kevin Buzzard]

import Mathlib

abbrev MyInt := ℤ

universe u -- we want to allow `Prop` and `Type` so we can do induction and recursion.
-- So we let the "motive" of the recursor take values in `Sort u`, because `Sort 0 = Prop`
-- and `Sort 1 = Type`.

def MyInt.pos_neg_rec_on {M : MyInt → Sort u} (m0 : M 0) (mpos : ∀ (n : ℕ), M ↑n → M (↑n + 1))
  (mneg : ∀ n : ℕ, M (-↑n) → M (-↑n - 1)) (z : MyInt) : M z := sorry -- hard exercise!

-- specification

variable {M : MyInt → Sort u} (m0 : M 0) (mpos : ∀ (n : ℕ), M ↑n → M (↑n + 1))
  (mneg : ∀ n : ℕ, M (-↑n) → M (-↑n - 1))

lemma pos_neg_rec_on_zero : MyInt.pos_neg_rec_on m0 mpos mneg 0 = m0 := sorry

lemma pos_neg_rec_on_pos (n : ℕ) :
  MyInt.pos_neg_rec_on m0 mpos mneg (↑n + 1) = mpos n (MyInt.pos_neg_rec_on m0 mpos mneg ↑n) := sorry

lemma pos_neg_rec_on_neg (n : ℕ) :
  MyInt.pos_neg_rec_on m0 mpos mneg (-↑n - 1) = mneg n (MyInt.pos_neg_rec_on m0 mpos mneg (-↑n)) := sorry

[Chris Bailey]

There is a match_pattern attribute, I don't remember exactly what the restrictions and capabilities are. The top answer here looks reasonable: https://proofassistants.stackexchange.com/questions/2438/why-can-addition-be-used-in-pattern-matching-nats-but-not-multiplication

I don't recall them using pattern matching, but this definition of the integers is a section in Logical Verification (chapter 12) if you're interested in seeing how others did it at some point (https://github.com/blanchette/logical_verification_2023/tree/main).

[Kevin Buzzard]

I guess the way to define this in your situation is first to define an analogous function on Nat x Nat and then prove it descends (or "lifts", as the computer scientists call it) to Int. These things are quite tricky :-)

[Kevin Buzzard]

I don't think they make the recursor in LV though (and neither do I in my treatment here ).

[Kyle Miller]

@Chris Bailey match_pattern won't work here -- a way to think about that attribute is that it could also be called pattern_inline. In matches, definitions with this attribute get inlined, and it has to be a valid pattern involving constructors of inductive types in th eend.

[Kyle Miller]

@Brandon Harad A lot of times it's better to define something as a quotient by not using Quot, but instead by realizing there is a normal form. Then, you define the Quot API for this. The point is that quotients should be thought of in terms of their universal properties, so you don't need to literally work with Quot itself.

This doesn't help with your match question (I'm not sure there's a way to do that), but I thought I'd mention it.

For example, rather than a quotient on pairs, you can define a subtype on pairs:

def Z := {p : Nat × Nat // p.1 = 0 ∨ p.2 = 0}

And then the constructor can be defined using normalization:

def Z.mk : Nat → Nat → Z
  | a, 0 => ⟨(a, 0), Or.inr rfl⟩
  | 0, b => ⟨(0, b), Or.inl rfl⟩
  | a+1, b+1 => Z.mk a b

theorem Z.mk_zero_snd (a : Nat) : Z.mk a 0 = ⟨(a, 0), Or.inr rfl⟩ := by cases a <;> rfl
theorem Z.mk_zero_fst (b : Nat) : Z.mk 0 b = ⟨(0, b), Or.inl rfl⟩ := by cases b <;> rfl

@[elab_as_elim]
theorem Z.ind {β : Z → Prop} (mk : ∀ (a b : Nat), β (Z.mk a b)) (q : Z) : β q := by
  obtain ⟨⟨a, b⟩, h | h⟩ := q <;> dsimp at h <;> subst_vars
  · simpa [Z.mk_zero_fst] using mk 0 b
  · simpa [Z.mk_zero_snd] using mk a 0

def Z.lift {β : Sort _} (f : Nat → Nat → β)
    (_ : ∀ (a b a' b' : Nat), a + b' = a' + b → f a b = f a' b')
    (n : Z) : β :=
  f n.1.1 n.1.2

theorem Z.mk_eq_of_ge {a b : Nat} (h : a ≥ b) : Z.mk a b = ⟨(a - b, 0), Or.inr rfl⟩ := by
  induction a generalizing b
  · simp at h; subst_vars; rfl
  next n ih =>
    cases b
    · rw [Z.mk_zero_snd]; rfl
    · rw [Z.mk, ih]; simp; omega

theorem Z.mk_eq_of_le {a b : Nat} (h : a ≤ b) : Z.mk a b = ⟨(0, b - a), Or.inl rfl⟩ := by
  induction b generalizing a
  · simp at h; subst_vars; rfl
  next n ih =>
    cases a
    · rw [Z.mk_zero_fst]; rfl
    · rw [Z.mk, ih]; simp; omega

@[simp]
theorem Z.lift_mk {β : Sort _} (f : Nat → Nat → β)
    (h : ∀ (a b a' b' : Nat), a + b' = a' + b → f a b = f a' b')
    (a b : Nat) : Z.lift f h (Z.mk a b) = f a b := by
  unfold Z.lift
  obtain hab|hab := le_or_gt a b
  · rw [Z.mk_eq_of_le hab, h]
    dsimp
    omega
  · rw [Z.mk_eq_of_ge hab.le, h]
    dsimp
    omega

theorem Z.sound (a b a' b' : Nat) (h : a + b' = a' + b) : Z.mk a b = Z.mk a' b' := by
  obtain hab|hab := le_or_gt a b <;>
  obtain hab'|hab' := le_or_gt a' b' <;>
  · apply Subtype.ext
    simp [Z.mk_eq_of_le, Z.mk_eq_of_ge, hab, hab', LT.lt.le]
    omega

For example, here's how you could define addition using this API:

def Z.add (x y : Z) : Z :=
  x.lift (fun a b => y.lift (fun c d => Z.mk (a + c) (b + d)) <| by
    intros a b c d h
    dsimp
    apply Z.sound
    omega) <| by
  intros a b c d h
  dsimp
  congr! 3
  apply Z.sound
  omega

theorem Z.add_mk (a b c d : Nat) :
    Z.add (Z.mk a b) (Z.mk c d) = Z.mk (a + c) (b + d) := by
  simp [Z.add]

[Kevin Buzzard]

@Kyle Miller did you just tag the wrong Brando(n)? (If so, note that at least a few years ago, editing your post doesn't tag the new person)

[Kevin Buzzard]

Note that the disadvantage of the subtype definition is that the API for the algebra structure on the integers becomes more fiddly to write (you're constantly having to break into cases when defining and proving). But it's a one time cost.

[Eric Wieser]

Kevin Buzzard said:

... there's nothing stopping you defining MyInt.pos_neg_rec or whatever you want to call it, ...

When you do this, you should tag it @[elab_as_elim] to make it a little easier to use

[Kyle Miller]

(Oops, yes, I tagged the wrong Brandon. Edited it.)

[Kyle Miller]

@Kevin Buzzard With what I wrote, now you never have to open up the definition ever again. You use the universal property of the quotient.

[Kyle Miller]

I extended the code in the message, and it includes this example of how to then define addition without breaking Z open:

def Z.add (x y : Z) : Z :=
  x.lift (fun a b => y.lift (fun c d => Z.mk (a + c) (b + d)) <| by
    intros a b c d h
    dsimp
    apply Z.sound
    omega) <| by
  intros a b c d h
  dsimp
  congr! 3
  apply Z.sound
  omega

theorem Z.add_mk (a b c d : Nat) :
    Z.add (Z.mk a b) (Z.mk c d) = Z.mk (a + c) (b + d) := by
  simp [Z.add]

[Kyle Miller]

The theorem Z.sound is sort of "responsible" for doing the case analysis you're talking about. That's now wrapped up in a theorem though, so you never have to do it again.

[Brandon Harad]

Interesting implementation. I hadn't thought of that. Thank you all.

[Eric Wieser]

One small advantage of working with literal quotients instead of a normal form is that they allow lift_mk to be true by definition

[Eric Wieser]

Perhaps there should be something like csimp for associating a normal form to a quotient, as the normal form is more efficient for actual computation

[Kyle Miller]

Well, you could always write an identity function that normalizes the underlying term of a quotient, and then use @[csimp] lemmas to swap the operations out for ones that insert this normalizer.

If you don't combine normalization with operations, I'm not sure where the compiler would insert normalization.

Or maybe you mean it could be @[csimp] for quotient types themselves? Where you can tell the compiler to use another type that implements the whole interface and universal property of being a quotient?