Error in intros

Stream: lean4

[Mukesh Tiwari]

Hi everyone, I have this very simple piece of code, but intro h in monoid_cancel_left theorem leads to the error shown below.

tactic 'introN' failed, insufficient number of binders
α : Type u
H : Monoid α
z iz x y : α
⊢ Op.op iz z = One.one → Op.op z x = Op.op z y ↔ x = y

Source Code

class One (α : Type u) where
  one : α

class Op (α : Type u) where
  op : α → α → α

class Associative (α : Type u) extends (One α), (Op α) where
  op_associative : ∀ (x y z : α), op x (op y z) = op (op x y) z

class LeftOne (α : Type u) extends (One α), (Op α) where
  left_one : ∀ x : α, op one x = x

class RightOne (α : Type u) extends (One α), (Op α) where
  right_one : ∀ x : α, op x one = x

class Monoid (α : Type u) extends
  (One α), (Op α), (Associative α),
  (LeftOne α), (RightOne α)

class Inv (α : Type u) where
   inv : α → α

class Group (α : Type u) extends (Monoid α), (Inv α) where
  left_inv : forall x : α, op (inv x) x = one
  right_inv : forall x : α, op x (inv x) = one


theorem monoid_cancel_left
  {α : Type u}
  [H : Monoid α]
  (z iz x y : α) :
  (H.op iz z = H.one) →
  (H.op z x) = (H.op z y) ↔ x = y := by
  intro h   (* MOVE YOUR CURSOR HERE TO SEE THE ERROR *)

[Adam Topaz]

Are you sure it's not missing parens?

[Adam Topaz]

E.g. does split make progress?

[Mukesh Tiwari]

Adam Topaz said:

Are you sure it's not missing parens?

I don't think so because I have checked it couple of time. No, split is also not making any progress. I have posted the whole file, just in case you want to run it locally.

[Adam Topaz]

hmmm....

class One (α : Type u) where
  one : α

class Op (α : Type u) where
  op : α → α → α

class Associative (α : Type u) extends (One α), (Op α) where
  op_associative : ∀ (x y z : α), op x (op y z) = op (op x y) z

class LeftOne (α : Type u) extends (One α), (Op α) where
  left_one : ∀ x : α, op one x = x

class RightOne (α : Type u) extends (One α), (Op α) where
  right_one : ∀ x : α, op x one = x

class Monoid (α : Type u) extends
  (One α), (Op α), (Associative α),
  (LeftOne α), (RightOne α)

class Inv (α : Type u) where
   inv : α → α

class Group (α : Type u) extends (Monoid α), (Inv α) where
  left_inv : forall x : α, op (inv x) x = one
  right_inv : forall x : α, op x (inv x) = one


theorem monoid_cancel_left
  {α : Type u}
  [H : Monoid α]
  (z iz x y : α) :
  (H.op iz z = H.one) →
  ((H.op z x) = (H.op z y) ↔ x = y) := by
  intros h
  sorry

[Adam Topaz]

lean is happy with that on my end...

[Mukesh Tiwari]

Wow! I see the problem is solved by this extra bracket :) ((H.op z x) = (H.op z y) ↔ x = y) which is not present in my code. Thank you!

[Mukesh Tiwari]

Now, I have another question: what is the difference between these two typeclasses? What are the pros and cons of these two styles, one in which you extend every thing (first) and one in which you put the axioms inside the body of typeclass?

class Monoid (α : Type u) extends
  (One α), (Op α), (Associative α),
  (LeftOne α), (RightOne α)

class MonoidNew (α : Type u) extends
  (One α), (Op α) where
  op_associative : ∀ (x y z : α), op x (op y z) = op (op x y) z
  left_one : ∀ x : α, op one x = x
  right_one : ∀ x : α, op x one = x

[Mukesh Tiwari]

Is there a way to get rid of one of the rewrite? (some kind of repeat rewrite)

rewrite [H.op_associative, ha, H.left_one] at Hcut
rewrite [H.op_associative, ha, H.left_one] at Hcut

theorem monoid_cancel_left
  {α : Type u}
  [H : Monoid α]
  (z iz x y : α) :
  H.op iz z = H.one →
  (H.op z x = H.op z y ↔ x = y) := by
  intro ha
  apply Iff.intro
  focus
    intro hb
    have Hcut : (H.op iz  (H.op z x))  = (H.op iz (H.op z  y)) := by
      rewrite [hb]; exact rfl
    rewrite [H.op_associative, ha, H.left_one] at Hcut
    rewrite [H.op_associative, ha, H.left_one] at Hcut
    exact Hcut
  focus
    intro hb
    rewrite [hb]
    exact rfl