is this a use case for quotient?

Stream: new members

[Vaibhav Karve]

I want to write a function that takes as input an argument of type list ℤ and whenever it finds that an integer n and -n are both in the list, it removes both of them and replaces them with a 0 (so in some sense the n and -n annihilate each other). Repeat process till the list is "completely reduced".

My only thoughts so far have been to define an equivalence relation on list ℤ and then use that to create a quotient type. Is that right? Is there a simpler way I am missing.

In case it is relevant to the answer, there are two other things I have in mind --

• at some point I might decide to change it from list ℤ to multiset ℤ or even set ℤ. So an answer that would let me switch between these would be preferable (that way I am not tied to some particular property of list).
• i then want to be able to prove other theorems about this "reduced/quotiented" object. I am somewhat scared of the quot API. So the easier the final type is to handle, the better.

[Mario Carneiro]

The easiest way I can see to define something like that is

import data.multiset

inductive rel : multiset ℤ → multiset ℤ → Prop
| mk (n l) : rel (n :: -n :: l) (0 :: l)

def quotset : Type := quot rel

[Mario Carneiro]

This definition doesn't work for list because it relies on being able to permute stuff. You would have to change the relation to allow permutation

[Mario Carneiro]

It's also not clear what to do with a set or finset because you can accumulate multiple copies of 0 here

[Vaibhav Karve]

Thanks Mario, you really blew my mind with that. :astonished: Till now I was using inductive only to write nonfunction? types. I had not realized I can define relations using inductive.

[Mario Carneiro]

This does not define what "completely reduced" means, there is a proof obligation there quite similar to what we are doing in free groups