Zulip Chat Archive

Stream: new members

Topic: is this a use case for quotient?


view this post on Zulip Vaibhav Karve (Feb 10 2020 at 15:19):

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.

view this post on Zulip Mario Carneiro (Feb 10 2020 at 15:23):

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

view this post on Zulip Mario Carneiro (Feb 10 2020 at 15:24):

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

view this post on Zulip Mario Carneiro (Feb 10 2020 at 15:25):

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

view this post on Zulip Vaibhav Karve (Feb 10 2020 at 15:35):

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.

view this post on Zulip Mario Carneiro (Feb 10 2020 at 15:41):

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


Last updated: May 13 2021 at 23:16 UTC