cool assertion violation

Stream: general

[Kevin Buzzard]

My favourite assertion violation -- the only bug I ever really see in Lean nowadays in fact -- is the 'unreachable' code was reached bug which we occasionally get when making structures. A typical situation is this: I want to make an instance of some fancy algebraic structure, put def foo (G V R) : perfectoid_algebra := {! !}, click on the lightbulb and then "generate a skeleton for the structure under construction", fill in the first field and bam, unreachable code was reached.

My usual workaround: switch VS Code from "checking visible files" to "checking nothing", fill in all the remaining underscores as best I can (e.g. sorry is fine, but the more fields I can fill in the better), and then turn Lean back on and we're usually back up and running, the violation has gone and I can fill in the remaining fields and muddle on.

I found it hard to reproduce these errors at first. Often restarting Lean would fix the problem. But I managed to catch a reliable one and opened an issue lean#123, just so we had a record of this.

A few days ago, Scott found another one -- in some non-master branch of mathlib -- and added it to the issue. But this one was worse than mine. Scott had filled in all the underscores of the structure with sorry and the assertion violation was still there. This is now a more serious problem, because filling in those sorrys is going to be nigh-on impossible. Thanks to leanproject and the azure oleans :heart: it was easy for me to reproduce Scott's error. I decided to make the effort to minimise, and now I have a version with no mathlib imports at all (below).

It is pretty weird. The innocent-looking change from x • y • b to y • b in distrib_mul_action' changes the error completely and stops the violation.

I have no idea how easy it is to continue from here, I feel like I've gone as far as I can go. The key ingredients seem to be the structure, the coercion to sort, and the fact that the instance foo seems to need to produce a term of type Ring from nowhere. Changing x • y • b to y • b gives a more expected error.

Can I tempt anyone to look further?

/-- notation typeclass not in core.  -/
class has_scalar (G : Type) (V : Type) := (smul : G → V → V)

infixr ` • `:73 := has_scalar.smul

structure Ring : Type.

instance : has_coe_to_sort Ring :=
{
  S := Type,
  coe := λ R, unit
}

variables {G : Type}  {R : Ring}

class distrib_mul_action' (G : Type) (V : Type) extends has_scalar G V :=
(foo : ∀ (x y : G) (b : V), x • b = x • y • b) -- note that changing x • y • b to y • b fixes the violation
                                               -- and instead we get a different error.

structure finsupp' (β : Type) : Type :=
(to_fun             : β → β)

def mas (r : R) : finsupp' ↥R  :=
{
  to_fun := id,
}

variables (V : Type)

instance foo : distrib_mul_action' G V :=
{
  smul := λ g v, (mas ()) • v, -- note that changing () to 37 also causes an assertion violation
  foo := λ g g' v, sorry
}

[edit: remove superfluous has_mul G]

[Kevin Buzzard]

PS @Scott Morrison this minimisation revealed how to fix the assertion violation you found in lean#123: you have a mas g 1 which needs to be mas g (1 : R) -- Lean cannot figure out that the CommRing you want is R otherwise. One would expect an error about being unable to synthesize a CommRing but you get the assertion violation instead.

[Chris Hughes]

smul isn't a field of distrib_mul_action'

[Kevin Buzzard]

It extends has_scalar. Did I screw up?

[Chris Hughes]

new structure command

[Chris Hughes]

So, to_has_scalar is a field

[Gabriel Ebner]

After removing the assertion I get the following error, is this what you expected:

/home/gebner/lean/kevinbug.lean:34:18: error: don't know how to synthesize placeholder
context:
G : Type,
_inst_1 : has_mul G,
V : Type
⊢ G → V → Ring

[Kevin Buzzard]

Right -- Lean is supposed to be magically coming up with a term of type Ring so mas () makes sense.

[Kevin Buzzard]

If I am not even supposed to be supplying a smul field -- perhaps Lean is trying to interpret λ g v, (mas ()) • v before it even decides what to do with it.

[Chris Hughes]

Actually I think this notation works with the new structure command as well. If I type begin end it expects the right type.

[Kevin Buzzard]

The code I posted above does not really typecheck at all. I think Scott was in a situation where more has_scalar instances were defined. As I mentioned, you can change () to 37 and you still get the violation, and the type of mas forces 37 : unit which isn't OK because unit doesn't have a 1.

[Kevin Buzzard]

@Gabriel Ebner what's the error after the assertion is removed in the other code in the issue:

import ring_theory.algebra

open function

def quot.lift
  {R : Type*} [comm_ring R]
  {A : Type*} [comm_ring A] [algebra R A]
  {B : Type*} [comm_ring B] [algebra R B]
  {C : Type*} [comm_ring C] [algebra R C]
  (f : A →ₐ[R] B) (hf : surjective f)
  (g : A →ₐ[R] C) (hfg : ∀ a : A, f a = 0 → g a = 0) :
  B →ₐ[R] C :=
{ to_fun := λ b, _,
  map_one' := _,
  map_mul' := _,
  map_zero' := _,
  map_add' := _,
  commutes' := _ }

Or do you need me to remove the mathlib import? Here is looks like everything is specified. If I could understand a bit better what is causing the violation, it might make it easier to work around.

[Gabriel Ebner]

Please try to remove the mathlib imports.

[Kevin Buzzard]

Now you see it:

import ring_theory.algebra

open function

def quot.lift
  {R : Type} [comm_ring R]
  {A : Type} [comm_ring A] [algebra R A]
  {B : Type*} [comm_ring B] [algebra R B]
  {C : Type} [comm_ring C] [algebra R C]
  (f : alg_hom R A B) (hf : surjective f)
  (g : alg_hom R A C) (hfg : ∀ a : A, f a = 0 → g a = 0) :
  alg_hom R B C :=
{ to_fun := λ b, _,
  map_one' := _,
  map_mul' := _,
  map_zero' := _,
  map_add' := _,
  commutes' := _ }

...now you don't:

import ring_theory.algebra

open function

def quot.lift
  {R : Type} [comm_ring R]
  {A : Type} [comm_ring A] [algebra R A]
  {B : Type} [comm_ring B] [algebra R B]
  {C : Type} [comm_ring C] [algebra R C]
  (f : alg_hom R A B) (hf : surjective f)
  (g : alg_hom R A C) (hfg : ∀ a : A, f a = 0 → g a = 0) :
  alg_hom R B C :=
{ to_fun := λ b, _,
  map_one' := _,
  map_mul' := _,
  map_zero' := _,
  map_add' := _,
  commutes' := _ }

Change is {B : Type*} -> {B : Type}

[Kenny Lau]

yeah there's some issue with Type* so one is recommended to use Type u

[Kevin Buzzard]

Type u you don't see it either. This one is caused by Type*. You see assertion violations with Type* Kenny?

[Kevin Buzzard]

rofl, set_option old_structure_cmd true makes it go away, even though no structures are being defined

[Kenny Lau]

no, I see over-elaboration with Type*

[Kevin Buzzard]

open function

class has_scalar' (R : Type*) (A : Type*) := (smul : R → A → A)

infixr ` • `:73 := has_scalar'.smul

structure ring_hom' (M : Type*) (N : Type*) [semiring M] [semiring N] :=
(to_fun : M → N)
(map_one' : to_fun 1 = 1)
(map_mul' : ∀ x y, to_fun (x * y) = to_fun x * to_fun y)
(map_zero' : to_fun 0 = 0)
(map_add' : ∀ x y, to_fun (x + y) = to_fun x + to_fun y)

instance (α : Type*) (β : Type*) [semiring α] [semiring β] : has_coe_to_fun (ring_hom' α β) :=
⟨_, λ f, ring_hom'.to_fun (f)⟩

class algebra' (R : Type*) (A : Type*) [comm_semiring R] [semiring A]
  extends has_scalar' R A, ring_hom' R A :=
(commutes' : ∀ r x, to_fun r * x = x * to_fun r)
(smul_def' : ∀ r x, r • x = to_fun r * x)

def algebra_map' (R : Type*) (A : Type*) [comm_semiring R] [semiring A] [algebra' R A] : ring_hom' R A :=
algebra'.to_ring_hom'

structure alg_hom' (R : Type*) (A : Type*) (B : Type*)
  [comm_semiring R] [semiring A] [semiring B] [algebra' R A] [algebra' R B] extends ring_hom' A B :=
(commutes' : ∀ r : R, to_fun (algebra_map' R A r) = algebra_map' R B r)

variables {R : Type*} {A : Type*} {B : Type*}
variables [comm_semiring R] [semiring A] [semiring B]
variables [algebra' R A] [algebra' R B]

instance : has_coe_to_fun (alg_hom' R A B) := ⟨_, λ f, f.to_fun⟩

def quot.lift
  {R : Type} [comm_ring R]
  {A : Type} [comm_ring A] [algebra' R A]
  {B : Type*} [comm_ring B] [algebra' R B]
  {C : Type} [comm_ring C] [algebra' R C]
  (f : alg_hom' R A B) (hf : surjective f)
  (g : alg_hom' R A C) (hfg : ∀ a : A, f a = 0 → g a = 0) :
  alg_hom' R B C :=
{ to_fun := λ b, _,
  map_one' := _,
  map_mul' := _,
  map_zero' := _,
  map_add' := _,
  commutes' := _ }

[Kevin Buzzard]

Mathlib-free.

[Kevin Buzzard]

Thanks @Gabriel Ebner for the hack removing line 3174 completely! We can now see that Scott's problem was caused by Lean failing to synthesize a ring (which is correct behaviour -- Scott should explicitly say which ring he's using) and mine was caused by the Lean authors apparently incorrectly assuming that two types should be synthetically equal at some point, whereas there is still an { a := x, b := y}.a which hasn't become x yet (this would explain why we only ever saw the assertion violation when defining structures).