Mutual inductive + abbrev

Stream: lean4

[Yuri de Wit]

I am trying to create a mutual declaration involving an abbrev and an inductive (through a structure, but that is an irrelevant detail).

However, it seems that I can't. Consider the following code snippet.

mutual -- ERROR: invalid mutual block

abbrev Env := Array Val

structure Closure where
  e : Env
  t : Tm

inductive Val : Type
| VVar (l : Lvl)
| VApp (l : Val) (a : Val)  -- dont eval 'a' until needed
| VLam (x : Name) (c : Closure)
| VPi  (x : Name) (A: Val) (c : closure) -- dont eval 'A' if not typechecking
| VU
deriving Inhabited

end

Is there a way around this?

[Yuri de Wit]

Based on the Declaration.lean, only mutual of inductives or mutual of definitions are supported, not even a mutual mixing definitions and inductives.

@[builtinCommandElab «mutual»]
def elabMutual : CommandElab := fun stx => do
  let hints := { terminationBy? := stx[3].getOptional?, decreasingBy? := stx[4].getOptional? }
  if isMutualInductive stx then
    if let some bad := hints.terminationBy? then
      throwErrorAt bad "invalid 'termination_by' in mutually inductive datatype declaration"
    if let some bad := hints.decreasingBy? then
      throwErrorAt bad "invalid 'decreasing_by' in mutually inductive datatype declaration"
    elabMutualInductive stx[1].getArgs
  else if isMutualDef stx then
    for arg in stx[1].getArgs do
      let argHints := getTerminationHints arg
      if let some bad := argHints.terminationBy? then
        throwErrorAt bad "invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword"
      if let some bad := argHints.decreasingBy? then
        throwErrorAt bad "invalid 'decreasing_by' in 'mutual' block, it must be used after the 'end' keyword"
    elabMutualDef stx[1].getArgs hints
  else
    throwError "invalid mutual block"

[Yuri de Wit]

Ok, I guess the workaround is obvious:

mutual

inductive Closure where
  | mk (env : Array Val) (t: Tm)

inductive Val : Type
| VVar (l : Lvl)
| VApp (l : Val) (a : Val) -- call-by-need: dont eval 'a' until needed
| VLam (x : Name) (c : Closure)
| VPi  (x : Name) (A: Val) (c : closure) -- dont eval 'A' if not typechecking
| VU
deriving Inhabited

end

[David Thrane Christiansen]

This is probably a conservative check to rule out induction-recursion, which vastly increases the power of the theory. I suspect that this would make elaborating recursive functions to eliminators much more tricky, and I don't know if I-R is compatible with all the other features of Lean, however.

[Mario Carneiro]

Another workaround is to use a notation to define Env. You have to turn off quot.precheck to make the notation go through though

[Mario Carneiro]

Here's an example from mathport: it starts with a local notation "Binders" => Array #Binder, then uses that in the mutual induction, then ends with def Binders := Array #Binder after the induction so you can use that as a real definition. The only downside is that the inductive constructors themselves have fields using Array #Binder instead of the Binders declaration.