Zulip Chat Archive

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
Task: /home/buzzard/Encfs/Computer_languages/Lean/lean/bug.lean: presheaf_of_types_pushforward
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

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

Can reproduce

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

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:

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

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,
}

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

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

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

Please be nice this time

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"