invalid projection

Stream: lean4

[Marcus Rossel]

The following fails with invalid projection g.1:

import Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
import Lean
open Lean Meta

elab "#fails" : term => do
  let info ← getConstInfo ``SimplicialObject.Splitting.πSummand_comp_ιSummand_comp_PInfty_eq_PInfty
  forallTelescopeReducing info.type fun _ body => do
    match body.eq? with
    | none => return .bvar 0
    | some (_, lhs, _) => Meta.reduceAll lhs

#eval #fails

Is this a bug, or am I doing something wrong?

[Jannis Limperg]

You are probably returning Exprs from forallTelescopeReducing which are only valid in the extended LocalContext generated by forallTelescopeReducing. Use Expr.toString to inspect the expressions; they probably contain FVarIds that don't exist outside the forallTelescopeReducing.

[Marcus Rossel]

Then this shouldn't fail though, should it?

import Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
import Lean
open Lean Meta

elab "#fails" : term => do
  let info ← getConstInfo ``SimplicialObject.Splitting.πSummand_comp_ιSummand_comp_PInfty_eq_PInfty
  forallTelescopeReducing info.type fun _ body => do
    match body.eq? with
    | none => return mkNatLit 0
    | some (_, lhs, _) =>
      let _ ← Meta.reduceAll lhs
      return mkNatLit 1

#eval #fails

[Jannis Limperg]

Indeed. The failure happens during reduceAll:

import Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
import Lean
open Lean Meta

elab "#fails" : term => do
  let info ← getConstInfo ``SimplicialObject.Splitting.πSummand_comp_ιSummand_comp_PInfty_eq_PInfty
  forallTelescopeReducing info.type fun _ body => do
    match body.eq? with
    | none => dbg_trace "none"
    | some (_, lhs, _) =>
      dbg_trace "before reduceAll"
      let x ← Meta.reduceAll lhs
      dbg_trace toString x
  return mkNatLit 0

#eval #fails
-- before reduceAll
-- invalid projection
--  g.1

Looks like a bug to me, so I think you should create an issue (after inlining the type of SimplicialObject...., to remove the Mathlib dependency).

[Marcus Rossel]

Jannis Limperg said:

I think you should create an issue (after inlining the type of SimplicialObject...., to remove the Mathlib dependency).

I'm honestly not sure how to inline the type of SimplicalObject... as it's

∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C]
  {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) [inst_2 : CategoryTheory.Preadditive C]
  (n : ℕ),
  CategoryTheory.CategoryStruct.comp
      (SimplicialObject.Splitting.πSummand s
        (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n))))
      (CategoryTheory.CategoryStruct.comp
        (SimplicialObject.Splitting.ιSummand s
          (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n))))
        (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n)) =
    HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n

[Kyle Miller]

In case it helps at all, Meta.reduce lhs (skipTypes := false) (explicitOnly := false) turns up the error, and setting either of these arguments to the opposite value leads to no error, so it's an implicit type argument somewhere that's causing the failure.

[Kyle Miller]

Here's something to help you minimize:

import Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
import Lean
open Lean Meta

elab "reduce'" loc?:(ppSpace Parser.Tactic.location)? : tactic =>
  Mathlib.Tactic.runDefEqTactic (reduceAll ·) loc? "reduce"

example (C: Type*)
    [CategoryTheory.Category C] [CategoryTheory.Limits.HasFiniteCoproducts C]
    (X: CategoryTheory.SimplicialObject C)
    (s: SimplicialObject.Splitting X)
    [CategoryTheory.Preadditive C]
    (n : ℕ) (x) :
    SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n))
      = x := by
  reduce'
  /-
  invalid projection
    g.1
  -/
  sorry

(I started with the original LHS and deleted things to this point.)

[Kyle Miller]

It seems like this error is coming from reducing a proof. After unfolding things for awhile manually, I've got to this:

example (C: Type*)
    [CategoryTheory.Category C] [CategoryTheory.Limits.HasFiniteCoproducts C]
    (X: CategoryTheory.SimplicialObject C)
    (s: SimplicialObject.Splitting X)
    [CategoryTheory.Preadditive C]
    (n : ℕ)
    {Z : SimplexCategory} (g : (Opposite.op (SimplexCategory.mk n)).unop ⟶ Z)
    (x) :
    CategoryTheory.Category.id_comp g
      = x := by
  reduce'
  /-
  invalid projection
    g.1
  -/
  sorry

[Kyle Miller]

I found the source of the problem. First, you can get more information about the primitive projection using

open Lean PrettyPrinter.Delaborator SubExpr in
/-- Delaborator for `Prefunctor.obj` -/
@[delab proj]
def delabPrefunctorObjExp : Delab := do
  let Expr.proj typeName idx _ ← getExpr | unreachable!
  let e ← withProj delab
  `(proj $(quote typeName) $e $(quote idx))

This makes the error message print as

invalid projection
  proj✝ `OrderHom g 0

That's to say, we're trying to do g.1 as if g had type OrderHom ..

However, g has type docs#SimplexCategory.Hom, which is marked irreducible. This means that when inferType does whnf of the type of g, it gets stuck at SimplexCategory.Hom rather than reducing all the way to OrderHom.

example (C: Type*)
    [CategoryTheory.Category C] [CategoryTheory.Limits.HasFiniteCoproducts C]
    (X: CategoryTheory.SimplicialObject C)
    (s: SimplicialObject.Splitting X)
    [CategoryTheory.Preadditive C]
    (n : ℕ)
    {Z : SimplexCategory} (g : (Opposite.op (SimplexCategory.mk n)).unop ⟶ Z)
    (x) :
    CategoryTheory.Category.id_comp g
      = x := by
  --have : _ →o _ := g -- fails
  reduce at g
  unfold SimplexCategory.Hom at g
  have : _ →o _ := g -- succeeds

[Kyle Miller]

@Marcus Rossel I'm not sure this is a bug, though it's inconvenient having a term that you can do inferType on in one context but not in another. (Here's a related issue: lean4#2194)

One question is why you're reducing the lhs, and another is whether Meta.reduce will do instead of Meta.reduceAll.

[Jannis Limperg]

I would at least ask Leo (via an issue) whether he considers this a bug. Imo having reduceAll fail on a well-typed term is not something one should have to expect.

[Joël Riou]

I have no idea what is discussed in this thread! but this file on split simplicial objects is being slightly refactored in PR #8531 (see https://github.com/leanprover-community/mathlib4/pull/8531/files#diff-6aee2331c01c4301ce958e9d779555f8ed04259863471c15c9e38551bbbb0538R137)

[Mario Carneiro]

is there a mathlib-free MWE of this?

[Kyle Miller]

I think this is reasonably representative, but the setup is slightly different from that last example.

import Lean
open Lean Meta

open Elab Term in
elab "#reduce'" t:term : command => Elab.Command.runTermElabM fun _ => do
  let e ← withSynthesize <| elabTerm t none
  let e ← Meta.reduce e
  logInfo m!"{e} : {← inferType e}"

structure S where
  x : Nat

def S' := S
def S'.x (s : S') : Nat := S.x s

attribute [irreducible] S'

variable (s : S')
#reduce' s.x
/-
invalid projection
  s.1
-/

[Kyle Miller]

It's the inferType that prints the error. Everything else is setting up an Expr.proj term.

[Marcus Rossel]

Thanks for all the digging! The issue is #2975. I haven't opened an issue on the repo before, so any feedback on how to improve it is very welcome :)