Zulip Chat Archive

type mismatch at application
  quotient.lift ?m_4 {sorry}
term
  {sorry}
has type
  ?m_1 : Type ?
but is expected to have type
  ∀ (a b : ?m_1), a ≈ b → ?m_4 a = ?m_4 b : Prop
Additional information:
/home/buzzard/lean-projects/lean-stacks-project/src/tag007N.lean:21:21: context: 'eliminator' elaboration is not used for 'quotient.lift' because resulting type is not of the expected form

state:
X : Type u,
_inst_1 : topological_space X,
B : set (set X),
HB : topological_space.is_topological_basis B,
FPRB : presheaf_of_rings_on_basis HB,
x : X,
Hstandard : ∀ (U V : set X), U ∈ B → V ∈ B → U ∩ V ∈ B
⊢ aux (FPRB.to_presheaf_of_types_on_basis) x → stalk FPRB x → stalk FPRB x

Kevin Buzzard (May 18 2018 at 23:07):

'eliminator' elaboration is not used for 'quotient.lift' because resulting type is not of the expected form

Kevin Buzzard (May 18 2018 at 23:07):

I'd never seen that one until today and now I've seen it a lot :-/

Kevin Buzzard (May 18 2018 at 23:08):

It must change the order things are elaborated?

Kevin Buzzard (May 18 2018 at 23:08):

There is more than one sorry in this definition

Kevin Buzzard (May 18 2018 at 23:13):

(deleted)

Kevin Buzzard (May 18 2018 at 23:14):

(deleted)

Kevin Buzzard (May 18 2018 at 23:16):

So by sorry is also an error (the same error)

Mario Carneiro (May 19 2018 at 01:17):

I think this is a "dependent sorry" issue, similar to one that came up earlier with sorry in structure fields. If you write quotient.lift _ sorry, then the sorry has a metavariable type and this is not allowed (gives an error at the sorry application). Whereas if you write quotient.lift sorry sorry then the metavariable is replaced with sorry which is an actual term, so it should work. (You can still get these kinds of errors if you put too many sorries around because this can cause implicit variables that are normally solved by unification fail to be resolved because of sorry's unhelpful type.)

Mario Carneiro (May 19 2018 at 01:23):

And quotient.lift (by admit) sorry causes the same error since the tactic causes a delay in elaboration of the first sorry, so it tries to make sense of quotient.lift _ sorry first before getting to the tactic, and this is what causes the error.

Kevin Buzzard (May 19 2018 at 13:53):

init_quotient: initialize quotient type computational rules

Kevin Buzzard (May 19 2018 at 13:53):

Just found that with #help commands

Kevin Buzzard (May 19 2018 at 13:53):

What does that do?

Kenny Lau (May 19 2018 at 13:54):

that gives you the quot.lift axioms etc

Kenny Lau (May 19 2018 at 13:54):

it appears in core

Kevin Buzzard (May 19 2018 at 13:54):

documentation for that command is better than for coinductive:

Kevin Buzzard (May 19 2018 at 13:54):

coinductive: description

Kevin Buzzard (May 19 2018 at 13:55):

Oh I see -- so I don't really need to run init_quotient myself?

Kenny Lau (May 19 2018 at 13:55):

no, you don't

Kevin Buzzard (May 19 2018 at 13:57):

Anyway, my next quotient type woe is that if I have an object defined as a quotient type and I want to put, say, a group structure on it, then my definition of the multiplication should presumably be done in term mode and should avoid idioms such as \lam \<U,BU,Hx,s\>

Kevin Buzzard (May 19 2018 at 13:57):

which makes the code look horrible.

Kevin Buzzard (May 19 2018 at 13:58):

Is there any way around this? I tried writing a definition of a ring structure on a stalk of a sheaf of rings and the moment I started using \lam \<U,BU,...\> I ran into what I think are standard issues of things not being refl because they are something._match1.something or something

Mario Carneiro (May 19 2018 at 14:02):

use projections instead of a lambda match

Kevin Buzzard (May 19 2018 at 14:11):

Right, so \lam X and then X.U, X.BU etc.

Kevin Buzzard (May 19 2018 at 14:13):

I am a bit surprised that Lean won't do something this simple internally. Presumably what's going on is that the matching machinery is sophisticated and does not guarantee unravelling to something simple even if ultimately I am doing nothing more than a simple match on the components of a structure.

Last updated: Dec 20 2023 at 11:08 UTC