Reduce like operation for finite sets

Stream: Is there code for X?

[Joao Bregunci]

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]

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

[Joao Bregunci]

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]

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]

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]

@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]

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

[Joao Bregunci]

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

[Kyle Miller]

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

[Joao Bregunci]

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]

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]

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]

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]

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]