Zulip Chat Archive

Stream: general

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


Benjamin Davidson (May 21 2021 at 17:46):

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 (May 21 2021 at 17:50):

I'd expect iff.rfl to close that goal

Eric Wieser (May 21 2021 at 17:50):

What is docs#opposite.has_zero defined as?

Benjamin Davidson (May 21 2021 at 17:51):

I had tried that as well

Benjamin Davidson (May 21 2021 at 17:51):

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

Benjamin Davidson (May 21 2021 at 17:52):

That is opposite.has_zero

Benjamin Davidson (May 21 2021 at 17:52):

But I couldn't get that to reconcile either.

Eric Wieser (May 21 2021 at 17:54):

local attribute [reducible] opposite probably fixed it

Eric Wieser (May 21 2021 at 17:54):

But is also probably not the right solution

Benjamin Davidson (May 21 2021 at 17:57):

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 (May 21 2021 at 22:01):

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 (May 21 2021 at 22:09):

#7687

Floris van Doorn (May 21 2021 at 22:23):

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 (May 22 2021 at 09:15):

Nice work!

Floris van Doorn (May 22 2021 at 19:50):

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 (May 23 2021 at 06:44):

Thank you Floris!


Last updated: Dec 20 2023 at 11:08 UTC