## Stream: general

### Topic: Lean assertion violation

#### Kevin Buzzard (Mar 05 2018 at 09:05):

universes u v

theorem set.subset.trans {α : Type*} {a b c : set α} (ab : a ⊆ b) (bc : b ⊆ c) : a ⊆ c :=
assume x h, bc (ab h)

def set.preimage {α : Type u} {β : Type v} (f : α → β) (s : set β) : set α := {x | f x ∈ s}
infix  ⁻¹' :80 := set.preimage

structure presheaf_of_types (α : Type*) :=
(F : Π U : set α,  Type*)
(res : ∀ (U V : set α) (H : V ⊆ U),
(F U) → (F V))
(Hcomp : ∀ (U V W : set α)
(HUV : V ⊆ U) (HVW : W ⊆ V),
(res U W (set.subset.trans HVW HUV)) = (res V W HVW) ∘ (res U V HUV) )

definition presheaf_of_types_pushforward
{α : Type*}
{β : Type*}
(f : α → β)
(FPT : presheaf_of_types α)
: presheaf_of_types β :=
{ F := λ V : set β, FPT.F (set.preimage f V),
res := λ V₁ V₂ H,
FPT.res (set.preimage f V₁) (set.preimage f V₂)(λ x Hx,H Hx),
Hcomp := λ Uβ Vβ Wβ HUV HVW,rfl -- assertion violation
}


#### Kevin Buzzard (Mar 05 2018 at 09:05):

LEAN ASSERTION VIOLATION
File: /home/travis/build/leanprover/lean/src/frontends/lean/elaborator.cpp
Line: 3167
m_ctx.match(e, *val2)


#### Kevin Buzzard (Mar 05 2018 at 09:06):

Here's a (mathlib-free) assertion violation. Is this a known issue? If not, is my MWE minimal enough? If so, shall I file a bug report? I'd be happy to hear advice before working on this any more

#### Sebastian Ullrich (Mar 05 2018 at 09:06):

I'm looking into it

#### Kevin Buzzard (Mar 05 2018 at 09:06):

Lean (version 3.3.1, commit d6d44a19947e, Release) Ubuntu 16.04

Can reproduce

Thanks.

#### Sebastian Ullrich (Mar 05 2018 at 09:08):

I get the feeling structure notation is too sophisticated for our (the implementers') own good :sweat_smile:

ha ha

#### Kevin Buzzard (Mar 05 2018 at 09:08):

so it's my fault? :-)

#### Kevin Buzzard (Mar 05 2018 at 09:08):

I wasn't expecting rfl to work, it's just sometimes worth a try

#### Sebastian Ullrich (Mar 05 2018 at 09:09):

It's obviously our fault for enabling you to do weird things :)

#### Kevin Buzzard (Mar 05 2018 at 09:09):

I would be interested to know what the first thing you do in this situation is. If it's to fire up some C++ debugger then fair enough, you've lost me already, but if it's to just set some options and watch more carefully then I would be interested to follow along for a while

#### Kevin Buzzard (Mar 05 2018 at 09:10):

What do I do that is weird?

#### Kevin Buzzard (Mar 05 2018 at 09:14):

actually I wonder whether I am now grown up enough to fire up a C++ debugger myself

#### Sebastian Ullrich (Mar 05 2018 at 09:16):

It's a unification error, so I'm now looking at the is_def_eq_detail trace. The terms are still quite big - if you find a way to minimize them, that would be great.

#### Kevin Buzzard (Mar 05 2018 at 09:17):

OK I will try and minimise more

#### Kevin Buzzard (Mar 05 2018 at 09:29):

definition presheaf_of_types_pushforward
{β : Type*}
: presheaf_of_types β :=
{ F := sorry,
res := sorry,
Hcomp := λ Uβ Vβ Wβ HUV HVW,rfl -- assertion violation
}


#### Kevin Buzzard (Mar 05 2018 at 09:29):

No idea if that helps

#### Kevin Buzzard (Mar 05 2018 at 09:30):

I just replaced some stuff with sorry

#### Kevin Buzzard (Mar 05 2018 at 09:32):

definition presheaf_of_types_pushforward
{β : Type*}
: presheaf_of_types β :=
{ Hcomp := λ Uβ Vβ Wβ HUV HVW,rfl -- assertion violation
}


#### Kevin Buzzard (Mar 05 2018 at 09:34):

oh I have made it smaller

#### Kevin Buzzard (Mar 05 2018 at 09:34):

universes u v

structure presheaf_of_types (α : Type*) :=
(F : Π U : set α,  Type*)
(res : ∀ (U V : set α) ,
(F U) → (F V))
(Hcomp : ∀ (U V W : set α),
(res U W  = (res V W) ∘ (res U V) ))

set_option trace.type_context.is_def_eq_detail true

definition presheaf_of_types_pushforward
{β : Type*}
: presheaf_of_types β :=
{ Hcomp := λ Uβ Vβ Wβ,rfl -- assertion violation
}


#### Kevin Buzzard (Mar 05 2018 at 09:46):

structure presheaf_of_types (α : Type*) :=
(F : Π U : set α,  Type*)
(res : ∀ (U V : set α) ,
(F U) → (F V))
(Hidem : ∀ U : set α, res U U = (res U U) ∘ (res U U))

set_option trace.type_context.is_def_eq_detail true

definition presheaf_of_types_pushforward
{β : Type*}
: presheaf_of_types β :=
{ Hidem := λ U, rfl,
}


#### Kevin Buzzard (Mar 05 2018 at 09:57):

structure presheaf_of_types (α : Type) :=
(res : ∀ (U V : set α) ,
{x : α // U x} → {x : α // V x})
(Hidem : ∀ U : set α, res U U = (res U U) ∘ (res U U))

definition presheaf_of_types_pushforward
{β : Type}
: presheaf_of_types β :=
{ Hidem := λ U, rfl,
}


#### Kevin Buzzard (Mar 05 2018 at 09:58):

I'm going to stop there because all I am doing now is taking things like my general F from set alpha to Type and replacing it with an arbitrary explicit F (in this case the map sending U to the subtype corresponding to U)

#### Kevin Buzzard (Mar 05 2018 at 09:59):

oh here's an even better one, I can just use some random map unit to unit

#### Kevin Buzzard (Mar 05 2018 at 09:59):

structure presheaf_of_types (α : Type) :=
(res : ∀ (U V : set α) ,
unit → unit)
(Hidem : ∀ U : set α, res U U = (res U U) ∘ (res U U))

definition presheaf_of_types_pushforward
{β : Type}
: presheaf_of_types β :=
{ Hidem := λ U, rfl,
}


Still simpler:

#### Kevin Buzzard (Mar 05 2018 at 10:01):

structure presheaf_of_types (α : Type) :=
(res : ∀ (U : set α) ,
unit → unit)
(Hidem : ∀ U : set α, res U = (res U) ∘ (res U))

definition presheaf_of_types_pushforward
{β : Type}
: presheaf_of_types β :=
{ Hidem := λ U, rfl,
}


#### Kevin Buzzard (Mar 05 2018 at 10:02):

structure presheaf_of_types (α : Type) :=
(res : unit → unit)
(Hidem : ∀ U : set α, res = (res) ∘ (res))

definition presheaf_of_types_pushforward
{β : Type}
: presheaf_of_types β :=
{ Hidem := λ U, rfl,
}


#### Sebastian Ullrich (Mar 05 2018 at 10:04):

Thanks! That should do hopefully.

#### Kevin Buzzard (Mar 05 2018 at 10:04):

structure presheaf_of_types :=
(res : unit → unit)
(Hidem : ∀ U : unit, res = res ∘ res)

set_option trace.type_context.is_def_eq_detail true

definition presheaf_of_types_pushforward
: presheaf_of_types :=
{ Hidem := λ U, rfl,
}


#### Kevin Buzzard (Mar 05 2018 at 10:05):

Thanks for asking for more minimisation -- in some sense that was quite instructive. Initially I just removed everything not directly related to the violation in the form I had it, but after you asked more I realised there was nothing stopping me trying to find simpler violations

#### Kevin Buzzard (Mar 05 2018 at 10:07):

Adding the field res := id makes the problem go away

#### Kevin Buzzard (Mar 05 2018 at 10:10):

Hey, is it doing a prolog-like search?

#### Patrick Massot (Mar 05 2018 at 10:11):

Poor Kevin was deprived of a prolog-like search yesterday

#### Kevin Buzzard (Mar 05 2018 at 10:11):

I should never have equated this phrase with "random thing I don't understand"

#### Kevin Buzzard (Mar 05 2018 at 10:12):

but looking at the debugging output it looks like it might be backtracking...

#### Patrick Massot (Mar 05 2018 at 10:13):

I'm picturing you asking to Scholze: "are you doing a a prolog-like search" at the end of a really tough talk.

#### Kevin Buzzard (Mar 05 2018 at 10:17):

Maybe I don't even know what backtracking means. I guess I look at these debugging outputs and think "oh look it's trying lots of things in what looks like a systematic manner"

It's not enough

#### Kevin Buzzard (Mar 05 2018 at 10:17):

but I probably need to look more closely to distinguish the difference between "if this fails, discard it and try something else"

#### Kevin Buzzard (Mar 05 2018 at 10:17):

and "let's actually backtrack here"

#### Patrick Massot (Mar 05 2018 at 10:17):

You want to start following a path and then come back to an earlier branch point

#### Kevin Buzzard (Mar 05 2018 at 10:17):

yes this is just dawning on me now

#### Sebastian Ullrich (Mar 05 2018 at 11:51):

@Kevin Buzzard Congrats, I think you found a bug where definitional equality is not idempotent

#### Kevin Buzzard (Mar 05 2018 at 11:51):

Is that a good thing?

#### Kevin Buzzard (Mar 05 2018 at 11:51):

Do I get an achievement?

I'm jalous

#### Patrick Massot (Mar 05 2018 at 11:52):

My conv bug seems much less cool

#### Gabriel Ebner (Mar 05 2018 at 11:57):

@Sebastian Ullrich "Idempotent"?? Do you mean is_def_eq(t, t) returns false?

#### Sebastian Ullrich (Mar 05 2018 at 11:57):

On the first run it returns true for two terms, then false on any subsequent runs

#### Kevin Buzzard (Mar 05 2018 at 12:00):

ooh can I prove false??

#### Kevin Buzzard (Mar 05 2018 at 12:00):

I would definitely get an achievement for that

#### Sebastian Ullrich (Mar 05 2018 at 12:00):

Nah, it's just the elaborator

aah well

#### Sebastian Ullrich (Mar 05 2018 at 12:01):

Apparently elim_delayed_abstractions accidentally supports backtracking assignments to a metavar... not the correct place for a Prolog-like search

#### Kevin Buzzard (Mar 05 2018 at 12:01):

you lost me at the prolog-like search bit

#### Sebastian Ullrich (Mar 05 2018 at 12:02):

That was mostly a joke :)

#### Gabriel Ebner (Mar 05 2018 at 12:03):

Wow, this is unexpected.

#### Kevin Buzzard (Mar 05 2018 at 12:04):

Kenny posted this about a week ago

#### Kevin Buzzard (Mar 05 2018 at 12:04):

instance error (α : Type) : group α := { mul_assoc := λ x y z, rfl } 

#### Kevin Buzzard (Mar 05 2018 at 12:04):

without any further comment

#### Kevin Buzzard (Mar 05 2018 at 12:05):

and it might be the same thing

#### Sebastian Ullrich (Mar 05 2018 at 12:06):

Yep, same assertion

#### Patrick Massot (Mar 05 2018 at 12:17):

users.png
One little bug and everybody flies out, except devs. So sad...

Last updated: Dec 20 2023 at 11:08 UTC