Zulip Chat Archive

Stream: Is there code for X?

Topic: Reduce like operation for finite sets


view this post on Zulip Joao Bregunci (Mar 08 2021 at 15:12):

I was thinking if there is a reduce type like operation as in functional programming for finite sets. What I mean by this is if I have a finite set of a certain type and an operation that is associative and commutative if I can apply a reduce like operation. A simple example of this would be if I have a finite set of Prop if I could create the and of all of them. I would prefer to not work with lists if possible, even thought these already have fold operations...

view this post on Zulip Bryan Gin-ge Chen (Mar 08 2021 at 15:15):

Is docs#finset.fold what you're looking for?

view this post on Zulip Joao Bregunci (Mar 08 2021 at 15:20):

Exactly that. Thanks, just a question about mathlib. I was searching for this is data.set.finite, but didn't find. Is there a better way to search in mathlib? Sorry if this seems silly, but often I find myself a little bit lost on where to search...

view this post on Zulip Kevin Buzzard (Mar 08 2021 at 15:26):

data.set.finite is nonconstructive -- a possibly nonconstructive proof that a set is finite. Finset is more likely to reduce, you might want to look at the file where finset is defined.

view this post on Zulip Bryan Gin-ge Chen (Mar 08 2021 at 15:27):

I don't know think we have any great solutions for searching mathlib now (that's why we have this Zulip stream).

There's a search box in the top right of our docs page. Confusingly, it has two different modes. The more obvious behavior is that it searches declaration names as you type and displays them in a clickable dropdown (the VS Code extension's "symbol search" does this too, but only for declarations in files you've imported, you can access this by hitting Ctrl+T (Cmd+T on macOS)). The second mode is if you hit the search button, it directs you to a site-specific google search (which sadly is often out of date) (locally, I just use VS Code's search on mathlib; if you're working on a dependency, note that you may have to tell VS Code to include the _target/deps/mathlib directory in the search).

view this post on Zulip Johan Commelin (Mar 08 2021 at 15:29):

@Kevin Buzzard in some programming languages reduce is the name for fold. I think that this is the kind of reduce that Joao means.

view this post on Zulip Johan Commelin (Mar 08 2021 at 15:30):

We can certainly have a nonconstructive fold for data.set.finite

view this post on Zulip Joao Bregunci (Mar 08 2021 at 16:57):

Thanks for all the assistance, it has been extremely helpful.

view this post on Zulip Kyle Miller (Mar 08 2021 at 19:08):

@Joao Bregunci Is the non-duplication important for the Props? If not, you might consider mulitset. Implementation-wise, a finset is a multiset with no duplication, and a multiset is a list up to permutation. The fold operation for finset is defined in terms of foldr for multiset, which is defined in terms of foldr for list.

view this post on Zulip Joao Bregunci (Mar 08 2021 at 21:49):

Kyle Miller, I think that explaining my goal would be a little bit easier. I have a set of Propositions which I will call Theory and I want to show that given some Interpretation of these Prop, that is a way in which I evaluate these Prop, then I can arrive at a certain conclusion. So what I am thinking of is the following in a simple pseudocode:

 interp,  interp s1  interp s2   interp sn  interp dn

I can assume that I won't have duplicates, so I am going to take a look at multiset. My goal was to be able to concisely build the and above with n terms. Just a small question, to use this fold operation do I need to create any instance for the and operator? Because with Bryan suggestion, sorry if I am wrong, I would need to create a instance is_commutative and instance is_associative for the and operator...

view this post on Zulip Kyle Miller (Mar 08 2021 at 22:42):

Could you say a bit more about what a Theory is? Is Prop the usual kind of Prop? Or is it a data type representing some logical expression? Is there any specific reason you want to avoid list?

view this post on Zulip Kyle Miller (Mar 08 2021 at 22:46):

In case it's useful, there's list.all, which is a bool version of sort of what you want. A Prop-valued version is easy to write:

import data.list

def list.all' {α : Sort*} (l : list α) (p : α  Prop) : Prop :=
list.foldr (λ a r, p a  r) true l

You could use it with l.all' interp where l is a list of things to be interpreted, and interp takes a proposition and yields a Prop.

view this post on Zulip Kyle Miller (Mar 08 2021 at 22:50):

Here's a multiset version:

import data.multiset.fold

def multiset.and (l : multiset Prop) : Prop :=
multiset.fold () true l

def multiset.all {α : Sort*} (l : multiset α) (p : α  Prop) : Prop :=
(l.map p).and

view this post on Zulip Kyle Miller (Mar 08 2021 at 22:58):

A quick example of how it might be used:

inductive MyProp
| P : MyProp
| Or (p q : MyProp) : MyProp
| Not (p : MyProp) : MyProp

open MyProp

def interp_with (p' : Prop) : MyProp  Prop
| P := p'
| (Or p q) := interp_with p  interp_with q
| (Not p) := ¬ interp_with p

example : ({P, Or (Not P) P, Not (Not P)} : multiset MyProp).all (interp_with true) :=
by simp [multiset.all, interp_with, multiset.and]

Last updated: May 19 2021 at 02:10 UTC