has_zero equality

Stream: new members

[Duckki Oe]

How do you prove this?
α: Type
_inst_5: has_zero α
⊢ mul_zero_class.to_has_zero α = _inst_5

[Johan Commelin]

It might not be provable

[Johan Commelin]

If you have to unrelated instances of has_zero, they will be actually different.

[Johan Commelin]

So we need more context.

[Johan Commelin]

I could be evil and write

instance evil_zero : has_zero nat := { zero := 1 }

Now you certainly cannot prove evil_zero = nat.has_zero, even though both have type has_zero nat.

[Jalex Stark]

by the way format your code using #backticks

[Duckki Oe]

I'm trying to prove this:

section std_basis

open matrix

variables {m n: Type*} [fintype m] [fintype n]
variables [decidable_eq m] [decidable_eq n]
variables {α : Type} [has_zero α] [semiring α]

example {i' : m} {j' : n} {v : α}
        : ∀ {i j}, ¬ i = i' ∨ ¬ j = j' → std_basis_matrix i' j' v i j = 0
:= begin
    intros i j h,
    unfold std_basis_matrix,
    rwa if_neg, {
        sorry
    }
end

The zero from std_basis_matrix is not an instance of has_zero α, instead it seems to be mul_zero_class.to_has_zero α.

[Mario Carneiro]

[has_zero α] [semiring α]

This is bad, you just put two zeros on α

[Mario Carneiro]

The error you are getting is because you need one zero and have the other

[Mario Carneiro]

you should just delete [has_zero α] and it should work

[Duckki Oe]

That was it. Thanks! @Mario Carneiro