zero_ne_one

Stream: general

[Kenny Lau]

import data.opposite

universe u

variable {α : Type u}

class nonzero (α : Type u) [has_zero α] [has_one α] : Prop :=
(zero_ne_one : 0 ≠ (1:α))

@[simp]
lemma zero_ne_one [has_zero α] [has_one α] [nonzero α] : 0 ≠ (1:α) :=
nonzero.zero_ne_one

namespace opposite

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

instance [has_one α] : has_one (opposite α) :=
{ one := op 1 }

instance [has_zero α] [has_one α] [nonzero α] : nonzero (opposite α) :=
{ zero_ne_one := λ h, @zero_ne_one α _ _ _ $ op_inj h }

end opposite

[Kenny Lau]

why does it throw an error when I replace @zero_ne_one α with @zero_ne_one _?

[Kenny Lau]

type mismatch at application
  op_inj h
term
  h
has type
  0 = 1
but is expected to have type
  op 0 = op 1

[Kenny Lau]

does that mean I should make that parameter explicit?

[Kenny Lau]

I think this is a lean#282 issue

[Mario Carneiro]

I think this is expected behavior

[Mario Carneiro]

I think you should not make the type explicit

[Kenny Lau]

because it didn't exist when nonzero was bundled

[Kenny Lau]

I can also write λ h, zero_ne_one (op_inj h : (0:α) = 1)

[Mario Carneiro]

The type of the goal is op 0 != op 1, right? Since these have type opposite A, when you apply zero_ne_one lean will guess to fill the type with opposite A instead of A

[Kenny Lau]

no, the goal is false because of the fun h

[Mario Carneiro]

what type does op_inj h have?

[Kenny Lau]

it should say (0:\a) = 1

[Mario Carneiro]

it seems from the error message that lean still managed to work it out top down

[Kenny Lau]

but the 0 and 1 in h didn't unfold to op 0 = op 1

[Kenny Lau]

h has type (0 : opposite \a) = 1

[Kenny Lau]

which can be unfolded to op 0 = op 1

[Kenny Lau]

theoretically

[Kenny Lau]

but somehow Lean got confused in zero_ne_one

[Mario Carneiro]

does it work if you put the type ascription on h instead of op_inj h?

[Kenny Lau]

aha

[Mario Carneiro]

you might even be able to change the type of h at the source, in the lambda

[Kenny Lau]

instance [has_zero α] [has_one α] [nonzero α] : nonzero (opposite α) :=
{ zero_ne_one := λ h, zero_ne_one (op_inj (h : op (0 : α) = op 1)) }

[Kenny Lau]

type mismatch at application
  op_inj h
term
  h
has type
  0 = 1
but is expected to have type
  op 0 = op 1

[Kenny Lau]

this works:

instance [has_zero α] [has_one α] [nonzero α] : nonzero (opposite α) :=
{ zero_ne_one := λ h : op (0 : α) = op 1, zero_ne_one (op_inj h) }

[Kenny Lau]

so what's going wrong with the elaboration?

[Mario Carneiro]

well type ascription doesn't actually change the type

[Mario Carneiro]

if you used show op (0 : α) = op 1, from h it would also work

[Kenny Lau]

yeah but why can't Lean do this for me?

[Mario Carneiro]

Do it again with pp.all

[Kenny Lau]

type mismatch at application
  @opposite.op_inj.{?l_1+1} ?m_2 (@has_zero.zero.{?l_1} ?m_2 ?m_3) (@has_one.one.{?l_1} ?m_2 ?m_4) h
term
  h
has type
  @eq.{u+1} (opposite.{u+1} α) (@has_zero.zero.{u} (opposite.{u+1} α) (@opposite.has_zero.{u} α _inst_1))
    (@has_one.one.{u} (opposite.{u+1} α) (@opposite.has_one.{u} α _inst_2))
but is expected to have type
  @eq.{?l_1+1} (opposite.{?l_1+1} ?m_2) (@opposite.op.{?l_1+1} ?m_2 (@has_zero.zero.{?l_1} ?m_2 ?m_3))
    (@opposite.op.{?l_1+1} ?m_2 (@has_one.one.{?l_1} ?m_2 ?m_4))

[Mario Carneiro]

does by exact h work?

[Kenny Lau]

Tactic State
1 goal
α : Type u,
h :
  @eq.{u+1} (opposite.{u+1} α) (@has_zero.zero.{u} (opposite.{u+1} α) (@opposite.has_zero.{u} α _inst_1))
    (@has_one.one.{u} (opposite.{u+1} α) (@opposite.has_one.{u} α _inst_2))
⊢ @eq.{?l_1+1} (opposite.{?l_1+1} ?m_2) (@opposite.op.{?l_1+1} ?m_2 (@has_zero.zero.{?l_1} ?m_2 ?m_3))
    (@opposite.op.{?l_1+1} ?m_2 (@has_one.one.{?l_1} ?m_2 ?m_4))

opposites.lean:114:42: error

don't know how to synthesize placeholder
context:
α : Type u,
_inst_1 : has_zero.{u} α,
_inst_2 : has_one.{u} α,
_inst_3 : @nonzero.{u} α _inst_1 _inst_2,
h :
  @eq.{u+1} (opposite.{u+1} α) (@has_zero.zero.{u} (opposite.{u+1} α) (@opposite.has_zero.{u} α _inst_1))
    (@has_one.one.{u} (opposite.{u+1} α) (@opposite.has_one.{u} α _inst_2))
⊢ Type ?l_1

opposites.lean:114:53: error

invalid type ascription, term has type
  @eq.{u+1} (opposite.{u+1} α) (@has_zero.zero.{u} (opposite.{u+1} α) (@opposite.has_zero.{u} α _inst_1))
    (@has_one.one.{u} (opposite.{u+1} α) (@opposite.has_one.{u} α _inst_2))
but is expected to have type
  @eq.{?l_1+1} (opposite.{?l_1+1} ?m_2) (@opposite.op.{?l_1+1} ?m_2 (@has_zero.zero.{?l_1} ?m_2 ?m_3))
    (@opposite.op.{?l_1+1} ?m_2 (@has_one.one.{?l_1} ?m_2 ?m_4))
state:
α : Type u,
_inst_1 : has_zero.{u} α,
_inst_2 : has_one.{u} α,
_inst_3 : @nonzero.{u} α _inst_1 _inst_2,
h :
  @eq.{u+1} (opposite.{u+1} α) (@has_zero.zero.{u} (opposite.{u+1} α) (@opposite.has_zero.{u} α _inst_1))
    (@has_one.one.{u} (opposite.{u+1} α) (@opposite.has_one.{u} α _inst_2))
⊢ @eq.{?l_1+1} (opposite.{?l_1+1} ?m_2) (@opposite.op.{?l_1+1} ?m_2 (@has_zero.zero.{?l_1} ?m_2 ?m_3))
    (@opposite.op.{?l_1+1} ?m_2 (@has_one.one.{?l_1} ?m_2 ?m_4))

[Kenny Lau]

I think Lean cannot unify (@opposite.op.{u+1} ?m_1 (@has_zero.zero.{u} ?m_1 ?m_2)) to (@has_zero.zero.{u} (opposite.{u+1} α) (@opposite.has_zero.{u} α _inst_1))

[Kenny Lau]

or is it the other way round

[Mario Carneiro]

well unify is symmetric

[Kenny Lau]

oh is it

[Mario Carneiro]

sure, there could in general be metavariables on both sides

[Kenny Lau]

so what's going on here?

[Mario Carneiro]

I assume that opposite.has_zero is defined as <op 0>?

[Kenny Lau]

right

[Kenny Lau]

as demonstrated in my #mwe

[Kenny Lau]

and for some reason when it's bundled it says op 0 = op 1:

import data.opposite

universe u

variable {α : Type u}

class zero_ne_one_class (α : Type u) extends has_zero α, has_one α :=
(zero_ne_one : 0 ≠ (1:α))

@[simp]
lemma zero_ne_one [zero_ne_one_class α] : 0 ≠ (1:α) :=
zero_ne_one_class.zero_ne_one

namespace opposite

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

instance [has_one α] : has_one (opposite α) :=
{ one := op 1 }

instance [zero_ne_one_class α] : zero_ne_one_class (opposite α) :=
{ zero_ne_one := λ h, _, -- h : op 0 = op 1
  ..opposite.has_zero,
  ..opposite.has_one }

end opposite

[Kenny Lau]

this is a lean#282 issue afterall methinks

[Mario Carneiro]

I can get the error without using structure literals though

[Mario Carneiro]

example [has_zero α] [has_one α] : (0 : opposite α) = 1 → (0:α) = 1 :=
@op_inj _ 0 1

[Mario Carneiro]

Aha:

set_option pp.implicit true
set_option pp.numerals false
set_option trace.type_context.is_def_eq_detail true
example [has_zero α] [has_one α] (h : (0 : opposite α) = 1) : (0:α) = 1 :=
@op_inj _ 0 1 h

...
[type_context.is_def_eq_detail] [2]: @has_zero.zero αᵒᵖ (@opposite.has_zero α _inst_1) =?= @op ?m_1 (@has_zero.zero ?m_1 ?m_2)
[type_context.is_def_eq_detail] unfold right: opposite.op
[type_context.is_def_eq_detail] [3]: @has_zero.zero αᵒᵖ (@opposite.has_zero α _inst_1) =?= @id ?m_1 (@has_zero.zero ?m_1 ?m_2)
[type_context.is_def_eq_detail] unfold right: id
[type_context.is_def_eq_detail] [4]: @has_zero.zero αᵒᵖ (@opposite.has_zero α _inst_1) =?= @has_zero.zero ?m_1 ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := αᵒᵖ
...

[Mario Carneiro]

It decided that it was more worthwhile to unfold op than has_zero.zero

[Mario Carneiro]

resulting in the incorrect assignment ?m_1 := αᵒᵖ

[Kenny Lau]

oh well

[Kenny Lau]

what to do

[Mario Carneiro]

I think this kind of problem can in theory be addressed by adjusting definitional heights, but that's a black magic I don't want to start peddling

[Mario Carneiro]

it seems like the kind of problem that should happen all the time though, so I must be missing some heuristic

[Mario Carneiro]

The short term fix is obvious though: use @ or a type ascription