Creating instance and is_commutative

Stream: new members

[Joao Bregunci]

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]

This works:

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

[Joao Bregunci]

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]

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]

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]

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]

Ah, I bet it's from the boolean_algebra structure on Prop: docs#boolean_algebra_Prop

[Mario Carneiro]

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

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]

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