Bool MulComm sanity check

Stream: lean4

[Scott Viteri]

In both cases boolean multiplication is logical and.
In lean 3:

class has_mulcomm (α : Type u) [has_mul α] : Prop :=
    (mulComm : Π {a b : α}, a * b = b * a)
instance : has_mulcomm bool :=
  ⟨λ a b, bool.cases_on a (bool.cases_on b (eq.refl _) (eq.refl _))
                          (bool.cases_on b (eq.refl _) (eq.refl _))⟩

In lean 4:

class MulComm (α : Type u) [Mul α] : Prop where
    mulComm : {a b : α} → a * b = b * a
instance : MulComm Bool :=
  ⟨λ a b => Bool.casesOn a (Bool.casesOn b _ _)
                           (Bool.casesOn b _ _)⟩

Lean 4 error:

Messages (2)
148:3:
type mismatch
  fun (a b : Bool) => Bool.casesOn a (?m.14758 a b) (?m.14759 a b)
has type
  (a b : Bool) → ?m.14757 a b a : Sort (imax 1 1 ?u.14676)
but is expected to have type
  a * b = b * a : Prop
148:12:
application type mismatch
  Bool.casesOn a ?m.14718 (Bool.casesOn b ?m.14721 ?m.14722)
argument
  Bool.casesOn b ?m.14721 ?m.14722
has type
  ?m.14757 a b b : Sort ?u.14676
but is expected to have type
  ?m.14757 a b true : Sort ?u.14676
(10 more messages above...)

to be honest, I am having trouble even reading this error message, and don't know how to proceed.

[Scott Viteri]

(deleted)

[Sebastian Ullrich]

The important part of the error message is that you are using fun on something not of a function type (anymore). See https://leanprover.github.io/lean4/doc/lean3changes.html#lambda-expressions, "implicit lambdas".

[Scott Viteri]

If I leave off the λ a b => then even though the context shows a and b of type Bool, I cannot case on them.
If I use @fun instead of λ , then it says that Bool.casesOn a is trying to prove a * b = a.

[Leonardo de Moura]

Here are a few ways to do it in Lean 4

class MulComm (α : Type u) [Mul α] : Prop where
    mulComm : {a b : α} → a * b = b * a

instance : Mul Bool where
  mul := and

instance : MulComm Bool where
  mulComm {a b} :=
    match a, b with
    | true, true   => rfl
    | true, false  => rfl
    | false, true  => rfl
    | false, false => rfl

instance : MulComm Bool where
  mulComm {a b} := by cases a <;> cases b <;> rfl

instance : MulComm Bool :=
  ⟨by intro a b; cases a <;> cases b <;> rfl⟩

instance : MulComm Bool :=
  ⟨fun {a b} => by cases a <;> cases b <;> rfl⟩

instance : MulComm Bool :=
  ⟨fun {a b} =>
    match a, b with
    | true, true   => rfl
    | true, false  => rfl
    | false, true  => rfl
    | false, false => rfl⟩

[Scott Viteri]

If I write

instance : MulComm Bool where
 mulComm a b := by {}

I get

Messages (1)
137:17:
invalid 'by' tactic, expected type has not been provided
(10 more messages above...)

If I try to define

instance : MulComm Bool where
 mulComm := (by {cases a with
                 | true => _
                 | false => _})

I get

Messages (1)
137:23:
unknown identifier 'a'

[Leonardo de Moura]

We will try to improve the error message.

[Scott Viteri]

oh just saw your response, looking now

[Scott Viteri]

ok, I understand, thank you