My function is noncomputable. How do I debug?

Stream: lean4

[Jesse Slater]

I have a function reindexCtx which is failing to compile computably and I don't understand why. The error message I am getting is not very descriptive, and my searching online didn't turn up anything relevant. I'd like some advice on how to debug this. This is the message:

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'reindexCtx.match_1', and it does not have executable code

I'm doing program verification and this is 700 lines in so I'll try to give relevant context without subjecting you to all the gory details. reindexCtx is a function for modifying an AST to work in a different environment. It takes an AST (parametrized by an environment), a partial mapping from variables in the environment to a new environment, and a proof that all variables used in the AST are in the preimage of the mapping, and produces an AST in the new environment. It works by recursing through the AST and replacing each variable occurrence with the result of the mapping. It seems like very basic pattern matching and recursion, so I don't know where to start looking for the cause.

I'm not using any suspicious datatypes like Real. Mostly just List and Nat and a bunch of inductive datatypes I have defined myself. I know that pattern matching on Prop would make things uncomputable, and I do have the proof that all variables in the AST are in the preimage, but I don't think I am pattern matching on it anywhere. What other things can prevent computability? Where should I start looking for the issue and what tools can I use to get better debugging information than that one error message?

I'd be happy to give any more context that would be useful. I can also share the code, but it's quite long.

[Yakov Pechersky]

It's likely the inductive datatypes themselves had not had computable recursors generated for them.

[Kyle Miller]

Could you share the code? Maybe you can minimize it a bit if you're afraid it's too long?

You're not using recursors directly, are you?

[Jesse Slater]

Here's the MWE. I got it down to 150 lines.

inductive HList {α : Type} (β : α → Type) : List α → Type
  | nil : HList β []
  | cons : β a → HList β as → HList β (a::as)
infixr:67 " ::ₕ " => HList.cons

inductive Member : α → List α → Type
  | head : Member a (a :: as)
  | tail : Member a as → Member a (a' :: as)

def HList.get : HList β as → Member a as → β a
  | b ::ₕ _, .head => b
  | _ ::ₕ bs, .tail mem => bs.get mem

abbrev HList.tail : HList β (a :: as) → HList β as
  | _ ::ₕ bs => bs

def HList.map
  {las : List α}
  (bf : {a : α} → β a → β' a)
  : HList β las → HList β' las
  | .nil => .nil
  | b ::ₕ bs => bf b ::ₕ bs.map bf

abbrev Mask (as : List α) : Type :=
  HList (λ _ => Bool) as

def Mask.const : Bool → {as : List α} → Mask as
  | _, [] => .nil
  | b, _ :: _ => b ::ₕ (const b)

def Mask.union
  : Mask as → Mask as → Mask as
  | .nil, .nil => .nil
  | b₁ ::ₕ bs₁, b₂ ::ₕ bs₂ => (b₁ || b₂) ::ₕ union bs₁ bs₂

def Mask.Submask
  : Mask as → Mask as → Prop
  | .nil, .nil => True
  | b₁ ::ₕ mask₁, b₂ ::ₕ mask₂ => (b₁ → b₂) ∧ Submask mask₁ mask₂

theorem Mask.Submask.union_left
  {mask₁ mask₂ mask₁₂ : Mask as} (sub : (mask₁.union mask₂).Submask mask₁₂)
  : mask₁.Submask mask₁₂ := by
  match as, mask₁, mask₂, mask₁₂ with
  | [], .nil, .nil, .nil => trivial
  | scma :: ctx', m₁ ::ₕ ms₁, m₂ ::ₕ ms₂, m₁₂ ::ₕ ms₁₂ =>
    unfold Submask union at *
    simp at sub
    simp_all only [true_or, implies_true, true_and]
    exact union_left sub.right

inductive CellType
  | nat
  deriving Repr, DecidableEq

abbrev CellType.asType : CellType → Type
  | nat => Nat

abbrev Schema := List CellType

abbrev Row scma := HList CellType.asType scma

abbrev Table scma := List (Row scma)

abbrev InCtx (t : CellType) (ctx : List Schema) :=
  (scma : Schema) × Member scma ctx × Member t scma

abbrev CtxMask (ctx : List Schema) := HList Mask ctx

def CtxMask.get
  (mem : InCtx t ctx) (mask : CtxMask ctx) : Bool :=
  (HList.get mask mem.2.1).get mem.2.2

def CtxEmbedding
  (mask : CtxMask ctx) (ctx' : List Schema)
  := {t : CellType} → (inCtx : InCtx t ctx) → mask.get inCtx → InCtx t ctx'

def CtxMask.const
  : Bool → {ctx : List Schema} → CtxMask ctx
  | _, [] => .nil
  | b, _ :: _ => Mask.const b ::ₕ const b

def CtxMask.union
  : CtxMask ctx → CtxMask ctx → CtxMask ctx
  | .nil, .nil => .nil
  | b₁ ::ₕ bs₁, b₂ ::ₕ bs₂ => Mask.union b₁ b₂ ::ₕ union bs₁ bs₂

def CtxMask.Submask
  : CtxMask ctx → CtxMask ctx → Prop
  | .nil, .nil => True
  | m ::ₕ ms, m' ::ₕ ms' => m.Submask m' ∧ CtxMask.Submask ms ms'

theorem CtxMask.Submask.union_left
  {mask₁ mask₂ mask₁₂ : CtxMask ctx} (sub : (mask₁.union mask₂).Submask mask₁₂)
  : mask₁.Submask mask₁₂ := by
  match ctx, mask₁, mask₂, mask₁₂ with
  | [], .nil, .nil, .nil => trivial
  | scma :: ctx', m₁ ::ₕ ms₁, m₂ ::ₕ ms₂, m₁₂ ::ₕ ms₁₂ =>
    unfold Submask CtxMask.union at *
    simp at sub
    constructor
    · exact Mask.Submask.union_left sub.left
    · exact union_left sub.right

inductive CellExpr
  : List Schema → CellType → Type
  | const : ty.asType → CellExpr ctx ty

abbrev RowExpr (ctx : List Schema) (scma : Schema) := HList (CellExpr ctx) scma

inductive TableExpr
  : List Schema → Schema → Type
  | seq_project :
    TableExpr ctx scma
      → RowExpr (scma :: ctx) scma'
      → TableExpr ctx scma'

def CellExpr.maskCtx :
  CellExpr ctx ty → CtxMask ctx
  | .const _ => .const false

def RowExpr.maskCtx :
  RowExpr ctx ty → CtxMask ctx
  | .nil => .const false
  | .cons cellExpr rowExpr' =>
    cellExpr.maskCtx.union (maskCtx rowExpr')

abbrev TableExpr.maskCtx
  : TableExpr ctx scma → CtxMask ctx
  | .seq_project expr rowExpr =>
    .union expr.maskCtx rowExpr.maskCtx.tail

--This actually takes mask, sub, and embedding parameters but I removed them for the MWE
def CellExpr.reindexCtx
  (expr : CellExpr ctx ty)
  : CellExpr ctx' ty :=
  match expr with
  | .const v => .const v

--This actually takes mask, sub, and embedding parameters but I removed them for the MWE
def RowExpr.reindexCtx
  (expr : RowExpr ctx ty)
  : RowExpr ctx' ty :=
  expr.map CellExpr.reindexCtx

def TableExpr.reindexCtx
  (expr : TableExpr ctx scma)
  (mask : CtxMask ctx)
  (sub : expr.maskCtx.Submask mask)
  (embedding : CtxEmbedding mask ctx')
  : TableExpr ctx' scma :=
  match expr with
  | .seq_project expr rowExpr =>
    .seq_project
      (expr.reindexCtx mask sub.union_left embedding)
      rowExpr.reindexCtx

[Jesse Slater]

I'm not using recursors directly.

The function at issue is at the bottom. I removed all but one constructor of the inductive type, and did a whole bunch of other pruning, so hopefully it won't be too hard to follow what is going on.

[Kyle Miller]

(Lean Zulip tip: if you put the code in triple backticks like

```
code
```

then there's a link in the upper right corner to live.lean-lang.org, and it's easy to look at without leaving Zulip. 150 lines is perfectly fine. Long zulip messages are folded. There's also the trick of putting code inside of ````spoiler tags, with one more backtick than the code block, though you have to write ```lean for the inner code block I think.)

[Kyle Miller]

(Somehow live.lean-lang.org wasn't loading for me but it just loaded.)

[Kyle Miller]

That's an odd error.

I notice though that

inductive TableExpr
  : List Schema → Schema → Type
  | seq_project :
    TableExpr ctx scma
      → RowExpr (scma :: ctx) scma'
      → TableExpr ctx scma'

doesn't seem to be an inhabited type. Probably it's the result of your pruning, but in your actual case is it inhabited?

[Kyle Miller]

(Yeah, it's not inhabited:

example (x : TableExpr ctx scma) : False := by
  induction x
  assumption

)

[Jesse Slater]

Yeah I removed the const constructor because it didn't change the error message. I can put some stuff back if you want it to be a bit more realistic. Not sure what is most helpful.

[Jesse Slater]

I may have gone overboard on the pruning

[Robin Arnez]

This is a bug in the old compiler. The new compiler doesn't seem to have this problem.

[Robin Arnez]

For clarification: There are currently two compiler frontends, one written in C++ (the old compiler) and another written in Lean (the new compiler). The old compiler is still currently used by default with the new one being actively in development.

[Robin Arnez]

For your purposes, this works:

def TableExpr.reindexCtx
    (expr : TableExpr ctx scma)
    (mask : CtxMask ctx)
    (sub : expr.maskCtx.Submask mask)
    (embedding : CtxEmbedding mask ctx') :
    TableExpr ctx' scma :=
  match (generalizing := false) h : expr with
  | .seq_project expr rowExpr =>
    .seq_project
      (expr.reindexCtx mask (h ▸ sub).union_left embedding)
      rowExpr.reindexCtx

It just seems like the compiler couldn't handle the substitution in sub

[Jesse Slater]

Thank you!
In my full example there is an extra inductive parameter that I've omitted in the MWE so h becomes HEq instead of Eq, so this doesn't directly work. I've been messing around with it a bit but I haven't gotten it working yet. Here's an updated example with enough added back to make it HEq.

inductive HList {α : Type} (β : α → Type) : List α → Type
  | nil : HList β []
  | cons : β a → HList β as → HList β (a::as)
infixr:67 " ::ₕ " => HList.cons

inductive Member : α → List α → Type
  | head : Member a (a :: as)
  | tail : Member a as → Member a (a' :: as)

def HList.get : HList β as → Member a as → β a
  | b ::ₕ _, .head => b
  | _ ::ₕ bs, .tail mem => bs.get mem

abbrev HList.tail : HList β (a :: as) → HList β as
  | _ ::ₕ bs => bs

def HList.map
  {las : List α}
  (bf : {a : α} → β a → β' a)
  : HList β las → HList β' las
  | .nil => .nil
  | b ::ₕ bs => bf b ::ₕ bs.map bf

abbrev Mask (as : List α) : Type :=
  HList (λ _ => Bool) as

def Mask.const : Bool → {as : List α} → Mask as
  | _, [] => .nil
  | b, _ :: _ => b ::ₕ (const b)

def Mask.union
  : Mask as → Mask as → Mask as
  | .nil, .nil => .nil
  | b₁ ::ₕ bs₁, b₂ ::ₕ bs₂ => (b₁ || b₂) ::ₕ union bs₁ bs₂

def Mask.Submask
  : Mask as → Mask as → Prop
  | .nil, .nil => True
  | b₁ ::ₕ mask₁, b₂ ::ₕ mask₂ => (b₁ → b₂) ∧ Submask mask₁ mask₂

theorem Mask.Submask.union_left
  {mask₁ mask₂ mask₁₂ : Mask as} (sub : (mask₁.union mask₂).Submask mask₁₂)
  : mask₁.Submask mask₁₂ := by
  match as, mask₁, mask₂, mask₁₂ with
  | [], .nil, .nil, .nil => trivial
  | scma :: ctx', m₁ ::ₕ ms₁, m₂ ::ₕ ms₂, m₁₂ ::ₕ ms₁₂ =>
    unfold Submask union at *
    simp at sub
    simp_all only [true_or, implies_true, true_and]
    exact union_left sub.right

inductive CellType
  | nat
  deriving Repr, DecidableEq

abbrev CellType.asType : CellType → Type
  | nat => Nat

abbrev Schema := List CellType

abbrev Row scma := HList CellType.asType scma

abbrev Table scma := List (Row scma)

abbrev InCtx (t : CellType) (ctx : List Schema) :=
  (scma : Schema) × Member scma ctx × Member t scma

abbrev CtxMask (ctx : List Schema) := HList Mask ctx

def CtxMask.get
  (mem : InCtx t ctx) (mask : CtxMask ctx) : Bool :=
  (HList.get mask mem.2.1).get mem.2.2

def CtxEmbedding
  (mask : CtxMask ctx) (ctx' : List Schema)
  := {t : CellType} → (inCtx : InCtx t ctx) → mask.get inCtx → InCtx t ctx'

def CtxMask.const
  : Bool → {ctx : List Schema} → CtxMask ctx
  | _, [] => .nil
  | b, _ :: _ => Mask.const b ::ₕ const b

def CtxMask.union
  : CtxMask ctx → CtxMask ctx → CtxMask ctx
  | .nil, .nil => .nil
  | b₁ ::ₕ bs₁, b₂ ::ₕ bs₂ => Mask.union b₁ b₂ ::ₕ union bs₁ bs₂

def CtxMask.Submask
  : CtxMask ctx → CtxMask ctx → Prop
  | .nil, .nil => True
  | m ::ₕ ms, m' ::ₕ ms' => m.Submask m' ∧ CtxMask.Submask ms ms'

theorem CtxMask.Submask.union_left
  {mask₁ mask₂ mask₁₂ : CtxMask ctx} (sub : (mask₁.union mask₂).Submask mask₁₂)
  : mask₁.Submask mask₁₂ := by
  match ctx, mask₁, mask₂, mask₁₂ with
  | [], .nil, .nil, .nil => trivial
  | scma :: ctx', m₁ ::ₕ ms₁, m₂ ::ₕ ms₂, m₁₂ ::ₕ ms₁₂ =>
    unfold Submask CtxMask.union at *
    simp at sub
    constructor
    · exact Mask.Submask.union_left sub.left
    · exact union_left sub.right

inductive CellExpr
  : List Schema → CellType → Type
  | const : ty.asType → CellExpr ctx ty

abbrev RowExpr (ctx : List Schema) (scma : Schema) := HList (CellExpr ctx) scma

inductive TableExpr
  : Bool → List Schema → Schema → Type
  | scan :
    Table scma → TableExpr false ctx scma
  | seq_project :
    TableExpr b ctx scma
      → RowExpr (scma :: ctx) scma'
      → TableExpr b ctx scma'

def CellExpr.maskCtx :
  CellExpr ctx ty → CtxMask ctx
  | .const _ => .const false

def RowExpr.maskCtx :
  RowExpr ctx ty → CtxMask ctx
  | .nil => .const false
  | .cons cellExpr rowExpr' =>
    cellExpr.maskCtx.union (maskCtx rowExpr')

abbrev TableExpr.maskCtx
  : TableExpr b ctx scma → CtxMask ctx
  | .scan _ => .const false
  | .seq_project expr rowExpr =>
    .union expr.maskCtx rowExpr.maskCtx.tail

--This actually takes mask, sub, and embedding parameters but I removed them for the MWE
def CellExpr.reindexCtx
  (expr : CellExpr ctx ty)
  : CellExpr ctx' ty :=
  match expr with
  | .const v => .const v

--This actually takes mask, sub, and embedding parameters but I removed them for the MWE
def RowExpr.reindexCtx
  (expr : RowExpr ctx ty)
  : RowExpr ctx' ty :=
  expr.map CellExpr.reindexCtx

def TableExpr.reindexCtx
  (expr : TableExpr b ctx scma)
  (mask : CtxMask ctx)
  (sub : expr.maskCtx.Submask mask)
  (embedding : CtxEmbedding mask ctx')
  : TableExpr b ctx' scma :=
  match (generalizing := false) h : expr with
  | .scan t => .scan t
  | .seq_project expr rowExpr =>
    .seq_project
      (expr.reindexCtx mask (h ▸ sub).union_left embedding)
      rowExpr.reindexCtx

[Robin Arnez]

not pretty but (by cases ‹_ = b›; cases h; exact sub.union_left) should do the trick

[Jesse Slater]

Thank you again!
I think I see what is going on there.