Zulip Chat Archive

Stream: new members

Topic: has_zero equality


view this post on Zulip Duckki Oe (Oct 22 2020 at 06:52):

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

view this post on Zulip Johan Commelin (Oct 22 2020 at 06:54):

It might not be provable

view this post on Zulip Johan Commelin (Oct 22 2020 at 06:54):

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

view this post on Zulip Johan Commelin (Oct 22 2020 at 06:55):

So we need more context.

view this post on Zulip Johan Commelin (Oct 22 2020 at 06:56):

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.

view this post on Zulip Jalex Stark (Oct 22 2020 at 13:10):

by the way format your code using #backticks

view this post on Zulip Duckki Oe (Oct 22 2020 at 16:29):

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 α.

view this post on Zulip Mario Carneiro (Oct 22 2020 at 16:30):

[has_zero α] [semiring α]

This is bad, you just put two zeros on α

view this post on Zulip Mario Carneiro (Oct 22 2020 at 16:31):

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

view this post on Zulip Mario Carneiro (Oct 22 2020 at 16:32):

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

view this post on Zulip Duckki Oe (Oct 22 2020 at 16:37):

That was it. Thanks! @Mario Carneiro


Last updated: May 14 2021 at 07:19 UTC