# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Reduce like operation for finite sets

#### 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...

#### Bryan Gin-ge Chen (Mar 08 2021 at 15:15):

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

#### 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...

#### 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.

#### 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).

#### 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.

#### Johan Commelin (Mar 08 2021 at 15:30):

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

#### Joao Bregunci (Mar 08 2021 at 16:57):

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

#### Kyle Miller (Mar 08 2021 at 19:08):

@Joao Bregunci Is the non-duplication important for the `Prop`

s? 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`

.

#### 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...

#### 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`

?

#### 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`

.

#### 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
```

#### 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