has_add versus add_semigroup

Stream: general

[Martin Dvořák]

In my PR https://github.com/leanprover-community/mathlib/pull/11181 we ran into a weird behavior that we don't understand. I attempted to make a MWE from it.

import algebra.algebra.basic
import data.matrix.notation
import linear_algebra.bilinear_map


variable {α : Type*}

lemma vec3_eq {a₀ a₁ a₂ b₀ b₁ b₂ : α} (h₀ : a₀ = b₀) (h₁ : a₁ = b₁) (h₂ : a₂ = b₂) :
  ![a₀, a₁, a₂] = ![b₀, b₁, b₂] := sorry

--variable [has_add α]
variable [add_semigroup α]

lemma vec3_add {a₀ a₁ a₂ b₀ b₁ b₂ : α} :
  ![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂] := sorry


variables {R : Type*} [comm_ring R]

def cross_product : (fin 3 → R) →ₗ[R] (fin 3 → R) →ₗ[R] (fin 3 → R) :=
begin
  apply linear_map.mk₂ R (λ (a b : fin 3 → R),
    ![a 1 * b 2 - a 2 * b 1,
      a 2 * b 0 - a 0 * b 2,
      a 0 * b 1 - a 1 * b 0]),
  { intros,
    simp only [pi.add_apply],
    rw vec3_add,     -- this fails when [has_add α] is used
    apply vec3_eq;
    ring,
   }, sorry, sorry, sorry,
end

The application of the lemma vec3_add requires associativity. The problem is that it depends on the instance for α. It isn't sufficient to provide a correct instance of R. If we replace [add_semigroup α] by [has_add α] then it fails in the place of application of vec3_add. The proof of vec3_add is all right either way.

Any idea why it happens?

[Martin Dvořák]

It is also worth noting that the bug does not appear when we do the same proof in the following way (separate definition of cross product and lemma for linearity in the first argument).

import algebra.algebra.basic
import data.matrix.notation
import linear_algebra.bilinear_map


variable {α : Type*}

lemma vec3_eq {a₀ a₁ a₂ b₀ b₁ b₂ : α} (h₀ : a₀ = b₀) (h₁ : a₁ = b₁) (h₂ : a₂ = b₂) :
  ![a₀, a₁, a₂] = ![b₀, b₁, b₂] := sorry

variable [has_add α]
--variable [add_semigroup α]

lemma vec3_add {a₀ a₁ a₂ b₀ b₁ b₂ : α} :
  ![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂] := sorry


variables {R : Type*} [comm_ring R]

def foo (a b : fin 3 → R) : (fin 3 → R) :=
    ![a 1 * b 2 - a 2 * b 1,
      a 2 * b 0 - a 0 * b 2,
      a 0 * b 1 - a 1 * b 0]

example (a₁ a₂ b : fin 3 → R) : foo (a₁ + a₂) b = foo a₁ b + foo a₂ b :=
begin
  unfold foo,
  simp only [pi.add_apply],
  rw vec3_add,     -- this works either way
  apply vec3_eq;
  ring,
end

[Kevin Buzzard]

variable [has_add α]
variable [add_semigroup α]

is wrong. It means "assume alpha is an additive semigroup and assume on top of this that alpha has a completely unrelated addition on it which satisfies no axioms". Once you do this then you have no control over what a + b means if a b : alpha; Lean will pick up a random one of the two additions and you don't know which one it is.

add_semigroup extends has_add, which means that you should not put a has_add alpha assumption in if you have an add_semigroup alpha in.

[Martin Dvořák]

We always use only one of them. The bug appears when we comment out one and uncomment the other.

[Kevin Buzzard]

variable [has_add α]
--variable [add_semigroup α]

lemma vec3_add {a₀ a₁ a₂ b₀ b₁ b₂ : α} :
  ![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂] :=
begin
  ext x,
  fin_cases x;
  refl,
end

btw

[Martin Dvořák]

Why did you add a proof of the lemma? Proving the lemma was not an issue; using the lemma was.

[Kevin Buzzard]

because I wondered whether that would change things. Sometimes sorrys can confuse Lean.

[Kevin Buzzard]

This works:

def cross_product : (fin 3 → R) →ₗ[R] (fin 3 → R) →ₗ[R] (fin 3 → R) :=
begin
  apply linear_map.mk₂ R (λ (a b : fin 3 → R),
    ![a 1 * b 2 - a 2 * b 1,
      a 2 * b 0 - a 0 * b 2,
      a 0 * b 1 - a 1 * b 0]),
  { intros,
    simp only [pi.add_apply],
    symmetry,
    convert @vec3_add R _ _ _ _ _ _ _;
    ring,
   }, sorry, sorry, sorry,
end

[Martin Dvořák]

In the full file, we have proofs. I omitted them for the sake of MWE.

[Martin Dvořák]

But it seems you eliminated the use of vec3_eq altogether, thanks!

[Eric Wieser]

More minimal:

import data.matrix.notation

variable {α : Type*}

lemma vec2_add [has_add α] {a₀ a₁ b₀ b₁ : α} :
  ![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁] :=
by simp

lemma vec2_add' [add_semigroup α] {a₀ a₁ b₀ b₁ : α} :
  ![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁] := vec2_add

def vec2_id [add_monoid α] : (fin 2 → α) →+ (fin 2 → α) :=
{ to_fun := λ a, ![a 0, a 1],
  map_zero' := sorry,
  map_add' := λ a b,
  begin
    simp only [pi.add_apply],
    rw vec2_add,    -- this fails
    -- rw vec2_add',     -- this works
  end }

[Martin Dvořák]

I will use Kevin's suggestion; nevertheless, I would still like to know why it failed as it was.

[Eric Wieser]

Yes, I think it's worth understanding what's going wrong here

[Kevin Buzzard]

I might be wrong but looking at the (absolutely huge!) terms generated by pp.all I'm wondering whether the issue is that ![a,b,c] generates a 3 which is a different kind of 3 to the 3 in fin 3.

[Kevin Buzzard]

rewrite tactic failed, did not find instance of the pattern in the target expression
  @has_add.add.{u} (fin (nat.succ (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))) → R)
...
(@has_add.add.{u} R
                (@add_zero_class.to_has_add.{u}
                   ((λ (ᾰ : fin (@bit1.{0} nat nat.has_one nat.has_add (@has_one.one.{0} nat nat.has_one))), R)
                      (@has_one.one.{0} (fin (@bit1.{0} nat nat.has_one nat.has_add (@has_one.one.{0} nat nat.has_one)))

but I might be wrong, maybe rw would be expected to unify fin (bit1 1) and fin (succ succ succ 0).

[Eric Wieser]

That's not it

[Eric Wieser]

It's a dependent type problem again

[Eric Wieser]

In my example,

set_option pp.implicit true
set_option pp.notation false

def vec2_id [add_monoid α] : (fin (succ (succ 0)) → α) →+ (fin (succ (succ 0)) → α) :=
{ to_fun := λ a, ![a 0, a 1],
  map_zero' := sorry,
  map_add' := λ a b,
  begin
    simp only [pi.add_apply],
    rw vec2_add,    -- this fails
    -- rw vec2_add',     -- this works
  end }

gives:

rewrite tactic failed, did not find instance of the pattern in the target expression
  @has_add.add (fin 1.succ → ?m_1)
    (@pi.has_add (fin 1.succ) (λ (ᾰ : fin 1.succ), ?m_1) (λ (i : fin 1.succ), ?m_2))
    (@matrix.vec_cons ?m_1 1 ?m_3 (@matrix.vec_cons ?m_1 0 ?m_4 (@matrix.vec_empty ?m_1)))
    (@matrix.vec_cons ?m_1 1 ?m_5 (@matrix.vec_cons ?m_1 0 ?m_6 (@matrix.vec_empty ?m_1)))
state:
α : Type u_1,
_inst_1 : add_monoid α,
a b : fin 1.succ → α
⊢ @eq (fin 1.succ → α)
    (@matrix.vec_cons α 1
       (@has_add.add α
          (@add_zero_class.to_has_add ((λ (ᾰ : fin 1.succ), α) 0)
             ((λ (i : fin 1.succ), @add_monoid.to_add_zero_class α _inst_1) 0))
          (a 0)
          (b 0))
       (@matrix.vec_cons α 0
          (@has_add.add α
             (@add_zero_class.to_has_add ((λ (ᾰ : fin 1.succ), α) 0)
                ((λ (i : fin 1.succ), @add_monoid.to_add_zero_class α _inst_1) 0))
             (a 1)
             (b 1))
          (@matrix.vec_empty α)))
    (@has_add.add (fin 1.succ → α)
       (@add_zero_class.to_has_add (fin 1.succ → α)
          (@pi.add_zero_class (fin 1.succ) (λ (ᾰ : fin 1.succ), α)
             (λ (i : fin 1.succ), @add_monoid.to_add_zero_class α _inst_1)))
       (@matrix.vec_cons α 1 (a 0) (@matrix.vec_cons α 0 (a 1) (@matrix.vec_empty α)))
       (@matrix.vec_cons α 1 (b 0) (@matrix.vec_cons α 0 (b 1) (@matrix.vec_empty α))))

It can't unify pi.add_zero_class.to_has_add with pi.has_add

[Eric Wieser]

rw vec2_add (_ : α) works, if you make the arguments to vec2_add explicit (which they should be anyway)

[Martin Dvořák]

Kevin Buzzard said:

because I wondered whether that would change things. Sometimes sorrys can confuse Lean.

Does sorry in a proof of a lemma have a capacity to change how the lemma works when it is applied??

[Eric Wieser]

I don't think it can in a lemma, but it can in a def or example, because lean doesn't commit to the type of a def until it's seen the whole thing (which is why def x := 1 is allowed even though it doesn't specify the type, but lemma foo := rfl is not)

[Kevin Buzzard]

Since that noncomputable weirdness that Gabriel fixed with force_noncomputable I've been a lot more paranoid about filling in sorries when I see unexpected errors

[Alex J. Best]

I can't think of too many, but here's a slightly niche example of where sorrying a lemma makes it behave differently:

constant X : Type
def f : X → X := id
@[simp]
lemma a (x : X) : f x = x := sorry--rfl
lemma b (x : X) : f x = x :=
begin
  dsimp,
  refl,
end

[Alex J. Best]

When you prove something by rfl Lean tags it with an attribute which makes dsimp try to use it.

[Alex J. Best]

But yeah most of the time sorrying lemmas for MWEs is fine if the proof is long

[Anne Baanen]

Eric Wieser said:

rw vec2_add (_ : α) works, if you make the arguments to vec2_add explicit (which they should be anyway)

More details: normally a unification problem along the lines of has_add.add α ?m_1 =?= add_semigroup.add α ?m_3 will trigger the instances ?m_1 and ?m_3 to be inferred, and then unfolding the definitions should result in equality. Here however, the goal looks like has_add.add α ?m_1 =?= add_semigroup.add ?m_2 ?m_3, so the right-hand side can't be inferred, and unification fails.

This kind of issue also broke a few proofs in #11238, due to an inheritance path that used to result in unifying linear_order.le α ?m_1 =?= linear_order.le ?m_2 ?m_3 (head is the same, so unify α =?= ?m_2, now ?m_3 is inferrable/unifiable, done) to be instead linear_order.le α ?m_1 =?= ordered_ring.le ?m_2 ?m_3.

[Anne Baanen]

So why can't we just use the types of has_add.add and add_semigroup.add to determine α =?= ?m_2? Perhaps because the types might depend on other fields of the class and you get the same problem recursively?

[Eric Wieser]

My guess is that it gets stuck on unifying the dependent types in docs#pi.has_add, and that if we had a separate function.has_add instance without the dependent types then the problem would go away. I can't test that theory because my internet doesn't seem fast enough to support gitpod right now