quotient, quotienting?

Stream: new members

[Huỳnh Trần Khanh]

What does 'quotient' mean in Lean and its close relative, Coq?

[Huỳnh Trần Khanh]

oh, it's unusual for a question to take this long to receive an answer. guess i need to be more patient

[Johan Commelin]

It's like quotients in maths. Did you search #tpil for "quotient"?

[Huỳnh Trần Khanh]

oh I did a Google search lol and got no results, thanks for the reminder

[Kevin Buzzard]

Just like subsets are ways to make smaller objects Y from a big object X, quotients are another way -- a kind of duel way. A subset of X is an object Y and an injection from Y to X. A quotient of X is an object Y and a surjection from X to Y. For example the even integers are a subset of the integers, but the integers modulo 10 are naturally a quotient of the integers. You can think of them as a subset but this isn't such a cool way of doing it because 7 and 8 are integers mod 10 and their sum in the integers mod 10 is 5, but their sum in the integers is 15, which means that the injection doesn't preserve addition but the surjection (sending every integer to it's reduction modulo 10) does (as 15 gets mapped to 5).

[Kevin Buzzard]

In this mathlib file https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/Zmod37.lean I make the integers mod 37 as a quotient of the integers.

[Kevin Buzzard]

You make subsets of a type by putting a predicate on the type. The corresponding subset is the terms where the predicate is true. You make quotients of a type by putting a relation on the type. The corresponding quotient is the type you get if you regard terms which are related as actually being equal. For example you can put a relation on the naturals saying that a and b are related if they end in the same digit. The corresponding quotient would be the integers modulo 10, and the surjection from the integers sends two integers to the same residue class iff they end in the same digit.

[Chris B]

Logical verification also has a section on quotients with examples/exercises. https://github.com/blanchette/logical_verification_2020

[Andrew Ashworth]

Huỳnh Trần Khanh said:

oh I did a Google search lol and got no results, thanks for the reminder

I was curious and this: https://www.hedonisticlearning.com/posts/quotient-types-for-programmers.html was the second result when I searched for quotient + related words (don't remember)

[Huỳnh Trần Khanh]

ok so now i'm actually playing around with quotients... how do i prove that another_direction is true? or is it actually false?

def relation : ℕ → ℕ → Prop
| a b := a < b

def quotient1 := quot relation

instance coercion : has_coe ℕ quotient1 := ⟨begin
  intro x,
  exact quot.mk relation x,
end⟩

def a1 : quotient1 := ↑5
def a2 : quotient1 := ↑15

lemma one_direction : a1 = a2 := begin
  apply quot.sound,
  rw relation,
  linarith,
end

lemma another_direction : a2 ≠ a1 := begin
  intro h,
  -- what to do here?
end

[Mario Carneiro]

It's false. You proved it is false

[Mario Carneiro]

the key step for eliminating from an equality of quotient elements is have := quot.exact _ h,

[Mario Carneiro]

however quot.exact is a real pain to deal with because it needs eqv_gen. This is one of the reasons why you should always prefer quotient over quot if possible

[Huỳnh Trần Khanh]

but the relation is not an equivalence relation :joy:

[Huỳnh Trần Khanh]

relation is defined as a < b

[Mario Carneiro]

quotient assumes that the relation you give it is an equivalence relation, and quotient.exact h will tell you that the two elements are directly related by the equivalence relation, rather than the equivalence relation generated by the given relation

[Mario Carneiro]

For the example as given, another_direction is false, because it is the negation of one_direction which you proved

[Mario Carneiro]

eqv_gen relation is the total relation

[Mario Carneiro]

example (a b : ℕ) : eqv_gen relation a b :=
let m := max a b + 1 in
have h1 : a < m, from nat.lt_succ_of_le (le_max_left _ _),
have h2 : b < m, from nat.lt_succ_of_le (le_max_right _ _),
(eqv_gen.rel _ _ h1).trans _ _ _ ((eqv_gen.rel _ _ h2).symm _ _)