(0 : αᵒᵖ) = (0 : αᵒᵖ)

Stream: general

[Benjamin Davidson]

I am trying to prove

lemma unop_ne_zero_iff [has_zero α] (a : αᵒᵖ) : a.unop ≠ (0 : α) ↔ a ≠ (0 : αᵒᵖ) :=

I would imagine that this is true by not_iff_not.mpr (unop_eq_zero_iff α a) or by rw [not_iff_not, unop_eq_zero_iff] but neither work. Digging a bit deeper:

import algebra.opposites
namespace opposite

lemma unop_ne_zero_iff (α : Type u) [has_zero α] (a : αᵒᵖ) : a.unop ≠ (0 : α) ↔ a ≠ (0 : αᵒᵖ) :=
begin
  rw not_iff_not,
  convert unop_eq_zero_iff α a,
end

end opposite

The above yields a goal of 0 = 0. When I click on the infoview it says Prop eq αᵒᵖ 0 0, but nothing involving reflexivity or eq_self_iff_true works; trying exact rfl throws the error message invalid type ascription, term has type ?m_2 = ?m_2 but is expected to have type 0 = 0.

The issue seems to be that the 0 on the LHS has attributes has_zero.zero and opposite.has_zero α, while the one on the RHS only has has_zero.zero. What is causing this, and is there no way to synthesize the two?

[Eric Wieser]

I'd expect iff.rfl to close that goal

[Eric Wieser]

What is docs#opposite.has_zero defined as?

[Benjamin Davidson]

I had tried that as well

[Benjamin Davidson]

instance [has_zero α] : has_zero (opposite α) :=
{ zero := op 0 }

[Benjamin Davidson]

That is opposite.has_zero

[Benjamin Davidson]

But I couldn't get that to reconcile either.

[Eric Wieser]

local attribute [reducible] opposite probably fixed it

[Eric Wieser]

But is also probably not the right solution

[Benjamin Davidson]

I had tried doing that originally since unop_eq_zero_iffhas that attribute, but I get the error message maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

[Floris van Doorn]

The type of docs#opposite.unop_eq_zero_iff is wrong. It uses the instance _inst_1 on the RHS (i.e. the instance has_zero α when it needs has_zero αᵒᵖ, but that doesn't even type-check when opposite is irreducible:

import algebra.opposites

set_option pp.numerals false
set_option pp.implicit true
#print opposite.unop_eq_zero_iff

Here is a fix:

import algebra.opposites

namespace opposite

variables {α : Type*}

local attribute [semireducible] opposite
@[simp] lemma my_unop_eq_zero_iff [has_zero α] (a : αᵒᵖ) : a.unop = (0 : α) ↔ a = (0 : αᵒᵖ) :=
unop_eq_zero_iff α a

lemma unop_ne_zero_iff [has_zero α] (a : αᵒᵖ) : a.unop ≠ (0 : α) ↔ a ≠ (0 : αᵒᵖ) :=
by rw [not_iff_not, my_unop_eq_zero_iff]

end opposite

(this also makes α implicit)

[Floris van Doorn]

#7687

[Floris van Doorn]

I'll make a PR with a linter that type-checks the type of declarations later:

/- The `check_type` linter reports: -/
/- TYPES DO NOT TYPE-CHECK: -/
-- algebra\category\Mon\adjunctions.lean
#print adjoin_zero_map /- failed to type check -/
#print adjoin_one_map /- failed to type check -/

-- algebra\group\with_one.lean
#print with_zero.coe_add_hom_apply /- failed to type check -/
#print with_one.coe_mul_hom_apply /- failed to type check -/

-- algebra\opposites.lean
#print opposite.unop_eq_zero_iff /- failed to type check -/
#print opposite.op_eq_zero_iff /- failed to type check -/
#print opposite.unop_eq_one_iff /- failed to type check -/
#print opposite.op_eq_one_iff /- failed to type check -/

-- category_theory\opposites.lean
#print category_theory.nat_trans.op_app /- failed to type check -/
#print category_theory.nat_trans.remove_left_op_app /- failed to type check -/
#print category_theory.nat_trans.right_op_app /- failed to type check -/

[Kevin Buzzard]

Nice work!

[Floris van Doorn]

In #7694 I added the linter and fixed these declarations in mathlib.
There are still many automatically generated declarations that are ill-typed (Gist).
This is mostly types that are made @[irreducible], but some definitions on it only work if it's not irreducible. There is a question what to do with these in Lean 4, since in Lean 4 we cannot make definitions irreducible, and then locally reducible. In earlier threads (like this one), it seems that it is an open question whether we want to turn them into constant in Lean 4, or whether we want to make them a def (potentially with a new irreducibility setting?).

[Benjamin Davidson]

Thank you Floris!