## 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: Dec 20 2023 at 11:08 UTC