Zulip Chat Archive

Stream: general

Topic: zero_ne_one


Kenny Lau (May 28 2020 at 09:06):

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 (May 28 2020 at 09:07):

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

Kenny Lau (May 28 2020 at 09:07):

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 (May 28 2020 at 09:10):

does that mean I should make that parameter explicit?

Kenny Lau (May 28 2020 at 09:18):

I think this is a lean#282 issue

Mario Carneiro (May 28 2020 at 09:18):

I think this is expected behavior

Mario Carneiro (May 28 2020 at 09:18):

I think you should not make the type explicit

Kenny Lau (May 28 2020 at 09:18):

because it didn't exist when nonzero was bundled

Kenny Lau (May 28 2020 at 09:19):

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

Mario Carneiro (May 28 2020 at 09:19):

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 (May 28 2020 at 09:20):

no, the goal is false because of the fun h

Mario Carneiro (May 28 2020 at 09:20):

what type does op_inj h have?

Kenny Lau (May 28 2020 at 09:21):

it should say (0:\a) = 1

Mario Carneiro (May 28 2020 at 09:21):

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

Kenny Lau (May 28 2020 at 09:21):

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

Kenny Lau (May 28 2020 at 09:21):

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

Kenny Lau (May 28 2020 at 09:21):

which can be unfolded to op 0 = op 1

Kenny Lau (May 28 2020 at 09:21):

theoretically

Kenny Lau (May 28 2020 at 09:22):

but somehow Lean got confused in zero_ne_one

Mario Carneiro (May 28 2020 at 09:22):

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

Kenny Lau (May 28 2020 at 09:22):

aha

Mario Carneiro (May 28 2020 at 09:22):

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

Kenny Lau (May 28 2020 at 09:22):

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

Kenny Lau (May 28 2020 at 09:23):

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 (May 28 2020 at 09:23):

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 (May 28 2020 at 09:23):

so what's going wrong with the elaboration?

Mario Carneiro (May 28 2020 at 09:23):

well type ascription doesn't actually change the type

Mario Carneiro (May 28 2020 at 09:24):

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

Kenny Lau (May 28 2020 at 09:24):

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

Mario Carneiro (May 28 2020 at 09:24):

Do it again with pp.all

Kenny Lau (May 28 2020 at 09:25):

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 (May 28 2020 at 09:27):

does by exact h work?

Kenny Lau (May 28 2020 at 09:28):

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 (May 28 2020 at 09:29):

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 (May 28 2020 at 09:29):

or is it the other way round

Mario Carneiro (May 28 2020 at 09:29):

well unify is symmetric

Kenny Lau (May 28 2020 at 09:29):

oh is it

Mario Carneiro (May 28 2020 at 09:30):

sure, there could in general be metavariables on both sides

Kenny Lau (May 28 2020 at 09:30):

so what's going on here?

Mario Carneiro (May 28 2020 at 09:31):

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

Kenny Lau (May 28 2020 at 09:31):

right

Kenny Lau (May 28 2020 at 09:31):

as demonstrated in my #mwe

Kenny Lau (May 28 2020 at 09:34):

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 (May 28 2020 at 09:35):

this is a lean#282 issue afterall methinks

Mario Carneiro (May 28 2020 at 09:38):

I can get the error without using structure literals though

Mario Carneiro (May 28 2020 at 09:38):

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

Mario Carneiro (May 28 2020 at 09:44):

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 (May 28 2020 at 09:45):

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

Mario Carneiro (May 28 2020 at 09:45):

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

Kenny Lau (May 28 2020 at 09:51):

oh well

Kenny Lau (May 28 2020 at 09:51):

what to do

Mario Carneiro (May 28 2020 at 09:55):

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 (May 28 2020 at 09:55):

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

Mario Carneiro (May 28 2020 at 09:56):

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


Last updated: Dec 20 2023 at 11:08 UTC