# Zulip Chat Archive

## Stream: new members

### Topic: Creating instance and is_commutative

#### Joao Bregunci (Mar 08 2021 at 22:17):

My goal here is given a `set Prop`

, let's say `{s1,s2,⋯,sn}`

to create a `Prop`

`s1 ∧ s2 ∧ ⋯ ∧ sn`

, so to do this I wanted to use:

```
def finset.fold {α : Type u_1} {β : Type u_2} (op : β → β → β)
[hc : is_commutative β op] [ha : is_associative β op] (b : β) (f : α → β) (s : finset α) :
```

So as far as I understand, I need to make two instances for `is_commutative`

and `is_associative`

for the `and`

operator. So I tried the following:

```
instance my_and_comm (A : Prop) :
@is_commutative Prop and := ⟨ and.comm ⟩
```

Where I got the following:

```
type mismatch at application
{comm := and.comm ?m_2}
term
and.comm
has type
?m_1 ∧ ?m_2 ↔ ?m_2 ∧ ?m_1
but is expected to have type
∀ (a b : Prop), (a ∧ b) = (b ∧ a)
```

Is there any way which I can turn this `↔`

into an equality? Or I won't be able to use `finset.fold`

.

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

This works:

```
instance my_and_comm (A : Prop) :
@is_commutative Prop and := ⟨λ a b, by rw [and.comm]⟩
```

#### Joao Bregunci (Mar 08 2021 at 22:26):

Fantastic Bryan, sorry but can you shine a light on this lambda expression? This `rw [and.comm]`

is creating the equality how?

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

I'm not sure of all the details here, but the `by`

keyword enters tactic mode, and then I use the `rw`

tactic, which apparently is able to do some extra cleanup when rewriting with `and.comm`

.

**Edit**: tactic#show_term shows the term that's created by the tactic:

```
import tactic
instance my_and_comm (A : Prop) :
@is_commutative Prop and := ⟨λ a b, by show_term {rw [and.comm]}⟩
/-
Try this: exact (id (eq.rec (eq.refl ((a ∧ b) = (b ∧ a))) (propext and.comm))).mpr (eq.refl (b ∧ a))
-/
```

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

Ah, I see, this is simpler:

```
instance my_and_comm (A : Prop) :
@is_commutative Prop and := ⟨λ a b, propext $ and.comm⟩
```

So `rw`

(and `simp`

) apply `propext`

when necessary to close goals.

#### Kyle Miller (Mar 09 2021 at 00:31):

It turns out that `(∧)`

(which is `and`

but using its notation; this is the "section" of the operator, giving a function of two arguments) already has an `is_commutative`

instance somehow through docs#inf_is_commutative. I can't say I fully understand how this works.

#### Bryan Gin-ge Chen (Mar 09 2021 at 00:33):

Ah, I bet it's from the `boolean_algebra`

structure on `Prop`

: docs#boolean_algebra_Prop

#### Mario Carneiro (Mar 09 2021 at 05:34):

@Joao Bregunci The simplest way to make a conjunction out of an arbitrary set of propositions, not necessarily even finite, is using forall: `\forall p \in s, p`

#### Joao Bregunci (Mar 09 2021 at 14:04):

Thanks Mario, I was overcomplicating thinks, but I at least learned a few little things `:)`

. I have a tendency to always think like functional programming, so whenever I see a problem I try to put `map`

, `fold`

, `filter`

, `zip`

everywhere... This aspect of Lean, so far in most tutorials that I've seen, are a little bit disappointing to say, at least in my view.

#### Kevin Buzzard (Mar 09 2021 at 14:31):

The definitions are the same as in Haskell and the theorems about the definitions are typically proved directly after the definitions in the source code. I agree that they don't come up much in the docs! These kinds of constructions come up much more in things like program verification. I am about to finish 16 hours of lectures on mathematics in lean this week and I never mentioned fold or filter or zip once, but we did talk about things like filter.map (but never list.map).

Last updated: May 08 2021 at 04:14 UTC