mutual inductive and def

Stream: lean4

[Sofia]

Hello. I am trying to create a few mutually recursive definitions, but one of the definitions is a def, not an inductive. I think there is some way to translate this such that it'll work but I haven't been able to figure out the magic words.

It might be better to avoid the mutual dependencies...

inductive Cover : (x y z : List α) -> Prop
| done  : Cover [] [] []
| left  : Cover x y z -> Cover (t :: x) y (t :: z)
| right : Cover x y z -> Cover x (t :: y) (t :: z)
| both  : Cover x y z -> Cover (t :: x) (t :: y) (t :: z)

inductive Ty
| unit
| nat
| bool
| func (a b : Ty)
deriving Inhabited

mutual
    inductive Stlc : Ty -> List Ty -> Type
    | lift : t.type -> Stlc t []
    | var : Stlc t [t]
    | lam : Stlc u (t :: Γ) -> Stlc (Ty.func t u) Γ
    | app : Stlc (Ty.func t u) Γ₁ -> Stlc t Γ₂ -> Cover Γ₁ Γ₂ Γ -> Stlc u Γ

    inductive Closure : Ty -> Ty -> Type
    | mk : Stlc b (a :: Γ) -> Env Γ -> Closure a b

    def Ty.type : Ty -> Type
    | unit => Unit
    | nat => Nat
    | bool => Bool
    | func a b => Closure a b

    inductive Env : List Ty -> Type
    | term : Env []
    | cons : t.type -> Env (t :: xs)
end

[Sofia]

Can replace the Closure indirection with Stlc b (a :: Γ) × Env Γ.

[Sofia]

Maybe something like this? But still invalid...

mutual
    inductive Stlc : Ty -> List Ty -> Type
    -- universe level of lift is too big
    | lift : Lift t y -> y -> Stlc t []
    | var : Stlc t [t]
    | lam : Stlc u (t :: Γ) -> Stlc (Ty.func t u) Γ
    | app : Stlc (Ty.func t u) Γ₁ -> Stlc t Γ₂ -> Cover Γ₁ Γ₂ Γ -> Stlc u Γ

    inductive Lift : Ty -> Type -> Type
    | u : Lift .unit Unit
    | n : Lift .nat Nat
    | b : Lift .bool Bool
-- another issue.. unexpected constructor resulting type..?
--  | f : lift (.func a b) (Stlc b (a :: Γ) × Env Γ)

    inductive Env : List Ty -> Type
    | term : Env []
    | cons : Lift t y -> y -> Env (t :: xs)
end

[Sofia]

Universe level problem with Lift. Suspect a Lift.(u) magic but don't see how to apply it here...

[Sofia]

For context I am trying to adapt this Agda to Lean 4. I have previously tried this and had different issues.

https://repository.tudelft.nl/islandora/object/uuid:f0312839-3444-41ee-9313-b07b21b59c11

[Sofia]

I will eventually translate this from STLC to DTLC, so the Ty and Stlc will be merged into Dtlc.

[Jakob von Raumer]

The magic word is "induction-recursion" which Lean unfortunately does not support.

[Sofia]

Hmm. Is that an open issue to fix or a design limitation?

[Jakob von Raumer]

Induction-recursion without "bumping" the universe is a foundational decision, so it's a design limitation. Compiling inductive-recursive down to features Lean supports could be a nice future project.

[Jakob von Raumer]

Your second snippet can be fixed by having all the three type families live in the second universe:

mutual
    inductive Stlc : Ty -> List Ty -> Type 2
    -- universe level of lift is too big
    | lift : Lift t y -> y -> Stlc t []
    | var : Stlc t [t]
    | lam : Stlc u (t :: Γ) -> Stlc (Ty.func t u) Γ
    | app : Stlc (Ty.func t u) Γ₁ -> Stlc t Γ₂ -> Cover Γ₁ Γ₂ Γ -> Stlc u Γ

    inductive Lift : Ty -> Type -> Type 2
    | u : Lift .unit Unit
    | n : Lift .nat Nat
    | b : Lift .bool Bool
-- another issue.. unexpected constructor resulting type..?
--  | f : lift (.func a b) (Stlc b (a :: Γ) × Env Γ)

    inductive Env : List Ty -> Type 2
    | term : Env []
    | cons : Lift t y -> y -> Env (t :: xs)
end

[Jakob von Raumer]

I also get an Error: index out of bounds in your example though, which is definitely a bug in Lean /cc @Leonardo de Moura

[Jakob von Raumer]

And the constructor you commented out seems to be harder to realize, since the universe bump prevents the circular dependency.

[Sofia]

Which version of lean did you use? I do not get such an error. nightly-2022-03-21.

[Sofia]

Thanks for the patch. Any idea about the commented line?

[Sofia]

(Disconnected -> messages out of order.)

Harder indeed... not just me. :)

[Jakob von Raumer]

Sofia said:

Which version of lean did you use? I do not get such an error. nightly-2022-03-21.

nightly-2022-04-12

[Sebastian Ullrich]

Sofia said:

Thanks for the patch. Any idea about the commented line?

There is nothing to lift in this case, so it looks like you should use a separate constructor

    inductive Env : List Ty -> Type 2
    | term : Env []
    | cons : Lift t y -> y -> Env (t :: xs)
    | cons_f : Stlc b (a :: Γ) → Env Γ → Env (.func a b :: Γ)

[Sofia]

Hmm. Interesting suggestion.

[Sofia]

Thanks.

[Jakob von Raumer]

Jakob von Raumer said:

I also get an Error: index out of bounds in your example though, which is definitely a bug in Lean /cc Leonardo de Moura

Filed an issue

[Sebastian Ullrich]

Better still to encapsulate Lift t y -> y -> ... in a new type, I think. But I haven't really thought through your design as a whole yet, e.g. how Stlc.lam and Stlc.val (Val.clo ..) should relate.

mutual
  inductive Stlc : Ty -> List Ty -> Type 2
    | val : Val t -> Stlc t []
    | var : Stlc t [t]
    | lam : Stlc u (t :: Γ) -> Stlc (Ty.func t u) Γ
    | app : Stlc (Ty.func t u) Γ₁ -> Stlc t Γ₂ -> Cover Γ₁ Γ₂ Γ -> Stlc u Γ

  inductive Val : Ty -> Type 2
    | u : Val .unit
    | n : Nat → Val .nat
    | b : Bool → Val .bool
    | clo : Stlc b (a :: Γ) → Env Γ → Val (.func a b)

  inductive Env : List Ty -> Type 2
    | term : Env []
    | cons : Val t -> Env (t :: xs)
end

[Sofia]

When writing the evaluator for the Stlc language, I need to lift the closure as the result of evaluation. So it would be ideal to keep the closure inside Val.

[Sofia]

Hmm.. In the evaluator, I'm reaching for the split contexts. How should I access these?

namespace Stlc
    def eval : Stlc t ctx -> Env ctx -> Val t
    | .val x, .term => x
    | .var, .cons x => x
    | .lam f, xs => .clo f xs
    | .app f x c, xs => sorry
end Stlc

(Edit: Is it idiomatic to use the dot-notation to avoid accidentally binding with a wildcard?)

[Sofia]

The "covering" is the Co-De Bruijn partitioning of the context. Thus values have an empty context, variables have a singleton context, and applications may split or share terms, but each term must be used at least once.

[Sofia]

Ah! The issue I had with the commented out lifting code was lift vs. Lift. !!

[Sebastian Ullrich]

You can use named arguments to bind specific implicit parameters, though you cannot currently mix them with the dot notation

    | app (Γ₁ := Γ₁) f x c, xs => sorry

[Sebastian Ullrich]

Sofia said:

(Edit: Is it idiomatic to use the dot-notation to avoid accidentally binding with a wildcard?)

The notation is still quite new, but that sounds reasonable to me (except in the case I just mentioned). But it really only matters for parameter-less constructors, all others should lead to an error when typoed.

[Sofia]

Makes sense. Thanks. <3

[Sofia]

Actually I don't think I need the Γ1/Γ2, I need to split the environment based on c. Either way that is nice to know. :)

[Sofia]

Hmm. Seem to have an issue with Prop vs. Type now. Cover was a Prop, but I guess I need to make it a Type but... I get universe level troubles again.

namespace Env
    def partition : Env Γ -> Cover Γ1 Γ2 Γ -> Env Γ1 × Env Γ2
    -- Cover.casesOn can only eliminate into Prop.
    | term, .done => (term, term)
    | cons v xs, .left c =>
        let (l, r) := partition xs c
        (cons v l, r)
    | cons v xs, .right c =>
        let (l, r) := partition xs c
        (l, cons v r)
    | cons v xs, .both c =>
        let (l, r) := partition xs c
        (cons v l, cons v r)
end Env

[Sofia]

Nevermind, seems I typo'd a for α when elaborating the type for Cover when converting it to Type with universe levels.

[Sofia]

Okay... I think I have everything except for.... the termination proof.

universe u

inductive Cover : (x y z : List.{u} α) -> Type u
  | done  : Cover [] [] []
  | left  : Cover x y z -> Cover (t :: x) y (t :: z)
  | right : Cover x y z -> Cover x (t :: y) (t :: z)
  | both  : Cover x y z -> Cover (t :: x) (t :: y) (t :: z)

inductive Ty
  | unit
  | nat
  | bool
  | func (a b : Ty)
deriving Inhabited

mutual
  inductive Stlc : Ty -> List Ty -> Type 2
    | val : Val t -> Stlc t []
    | var : Stlc t [t]
    | lam : Stlc u (t :: Γ) -> Stlc (Ty.func t u) Γ
    | app : Stlc (Ty.func t u) Γ₁ -> Stlc t Γ₂ -> Cover Γ₁ Γ₂ Γ -> Stlc u Γ

  inductive Val : Ty -> Type 2
    | u : Val .unit
    | n : Nat -> Val .nat
    | b : Bool -> Val .bool
    | clo : Stlc b (a :: Γ) -> Env Γ -> Val (.func a b)

  inductive Env : List Ty -> Type 2
    | term : Env []
    | cons : Val t -> Env xs -> Env (t :: xs)
end

namespace Env
    def partition : Env Γ -> Cover Γ₁ Γ₂ Γ -> Env Γ₁ × Env Γ₂
    | term, .done => (term, term)
    | cons v xs, .left  c => let (l, r) := partition xs c; (cons v l, r)
    | cons v xs, .right c => let (l, r) := partition xs c; (l, cons v r)
    | cons v xs, .both  c => let (l, r) := partition xs c; (cons v l, cons v r)
end Env

namespace Stlc
  def eval : Stlc t ctx -> Env ctx -> Val t
    | val x, .term => x
    | .var, .cons x .term => x
    | lam f, xs => .clo f xs
    | app f x c, xs =>
        let (l, r) := xs.partition c
        let .clo f l := eval f l
        eval f (l.cons (eval x r))
end Stlc

[Sofia]

Actually no, not just termination proof. Type mismatch in .. something in eval. o.o

[Leonardo de Moura]

Jakob von Raumer said:

Jakob von Raumer said:

I also get an Error: index out of bounds in your example though, which is definitely a bug in Lean /cc Leonardo de Moura

Filed an issue

Pushed a fix for this.

[Sofia]

././Stlc.lean:51:6: error: fail to show termination for
  Stlc.eval
with errors
argument #3 was not used for structural recursion
  application type mismatch
    @Stlc.brecOn (fun {t} {Γ} x => Env Γ → Val t) t
  argument
    t
  has type
    Ty : Type
  but is expected to have type
    (a : Ty) → Val a → Type u_1 : Type (u_1 + 1)

argument #4 was not used for structural recursion
  application type mismatch
    @Env.brecOn fun {Γ} x => {t : Ty} → Stlc t Γ → Val t
  argument
    fun {Γ} x => {t : Ty} → Stlc t Γ → Val t
  has type
    {Γ : List Ty} → Env Γ → Type u_1 : Type (u_1 + 1)
  but is expected to have type
    (a : Ty) → (a_1 : List Ty) → Stlc a a_1 → Type u_1 : Type (u_1 + 1)

argument #1 was not used for structural recursion
  failed to eliminate recursive application
    eval f l

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    eval f l

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

error: Error: index out of bounds

[Sofia]

Looking over the types. It seems that everything returns Val t except for the lambda case, which returns Val (Ty.func a b). Is this the problem? If so, how do I unify the type with Val t?

[Sofia]

Replacing its result with sorry does not resolve the type mismatch. shrugs

[Sofia]

Very confused with this error.

[Leonardo de Moura]

@Sofia We will try to clarify the error message in the future. The application type mismatches are not in your code. They were generated when Lean tried different ways to prove termination by structural recursion. If you use the termination_by annotation, you will get a better error message. Example:

  def eval : (s : Stlc t Γ) -> Env Γ -> Val t
    | val x, .term => x
    | .var, .cons x .term => x
    | lam f, xs => .clo f xs
    | app f x c, xs =>
        let (l, r) := xs.partition c
        let .clo f l := eval f l
        eval f (l.cons (eval x r))
  termination_by eval s env => sizeOf s

You can make the error message clearer by avoiding the variable shadowing at let .clo f l := eval f l.

[Leonardo de Moura]

BTW, I defined an arbitrary well-founded relation in the example above (i.e., sizeOf s), but you will not be able to prove termination using it. The goal was just to get a better error message.

[Sofia]

Noted. I had later renamed those and applied a few other similar cleanups. I first tried to add partial to skip the termination proof, but Lean wasn't happy with that either.

[Sofia]

Due to the lack of Inhabited instance on Val. Which I could add. Would be better to prove the termination of course.

[Sofia]

The tricky bit is the inhabited instance for Val.clo.

[Sofia]

I really need to figure out the details of the termination proofs... Tend to get stuck here a lot. :/

[Sofia]

Thanks @Leonardo de Moura . I should call the night here. Take care. o/

[Leonardo de Moura]

Sofia said:

The tricky bit is the inhabited instance for Val.clo.

You can simplify the problem a bit by writing the Stlc.val constructor as

    | val : Val t -> Stlc t Γ

Then, you can show that Val ty is inhabited using

def Ty.someValue : (ty : Ty) → Val ty
   | .unit     => .u
   | .nat      => .n 0
   | .bool     => .b false
   | .func a b => .clo (Γ := []) (.val (someValue b)) .term

instance : Inhabited (Val ty) where
  default := ty.someValue

You will also have to change the | val x, .term => x case at eval to | val x, _ => x.
After these changes partial will work.
If you hit similar issues in the future where it is not feasible to show the type is inhabited, then another option is to use

  def eval : (s : Stlc t Γ) -> Env Γ -> Val t
    | val x, _ => x
    | .var, .cons x .term => x
    | lam f, xs => .clo f xs
    | app f x c, xs =>
        let (l, r) := xs.partition c
        let .clo f l := eval f l
        eval f (l.cons (eval x r))
  decreasing_by sorry

This is equivalent to telling Lean "trust me this function does terminate, and I am willing to compromise soundness if it does not".

[Sofia]

That val needs to be empty, not arbitrary. Otherwise a helpful tip. I guess I will have to lie about the decreasing proof for now. Thanks again. I'm off for the night for real this time. :)