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