Non-regular inductive type and universes

Stream: lean4

[ohhaimark]

Is it possible to give appropriate universe levels to the following inductive type

inductive term : Type → Type :=
  | var : {v : Type} → v → term v
  | app : term v → term v → term v
  | lam : term (Option v) → term v

or is it inheritly untypeable in lean?

[Chris Bailey]

No, you can't have (_ : Type) in the constructor args if your inductive is also in Type. You can make it a parameter, but then you won't be able to change it to Option _.

[Kyle Miller]

One way around this is to make your own type universe:

inductive MyType : Type :=
  | MyUnit
  | MyOption : MyType → MyType

def MyType.toType : MyType → Type
  | .MyUnit => Unit
  | .MyOption t => Option t.toType

instance : CoeSort MyType Type where
  coe := MyType.toType

inductive term : MyType → Type :=
  | var : {v : MyType} → v → term v
  | app : term v → term v → term v
  | lam : term (.MyOption v) → term v

[James Gallicchio]

Or you can just put it in Type 1

inductive term : Type → Type :=
  | var : {v : Type} → v → term v
  | app : term v → term v → term v
  | lam : term (Option v) → term v

a value a : A : Sort u cannot contain a B : Sort v unless u > v. In your def, each of the constructors takes a parameter v : Type 0, so the type must live in at least Type 1

[James Gallicchio]

But if you're building a Type 1 you should have pretty good justification for doing so -- types inhabiting higher universes are kinda annoying to work with sometimes

[ohhaimark]

Awesome. I am now stuck on a termination proof for bind

inductive Ty (v : Type) : Type :=
  | base : Ty v
  | option : Ty v → Ty v

def Ty.pure (v : Type) : Ty v := Ty.base (v:=v)

@[simp] def Ty.type : Ty v → Type
  | base => v
  | option ty => Option ty.type


instance : CoeSort (Ty v) Type where
  coe := Ty.type

inductive Term' : Ty v → Type
  | var : {a : Ty v} → a → Term' a
  | app : Term' a → Term' a → Term' a
  | lam : Term' (Ty.option a) → Term' a

def Term a := Term' $ Ty.pure a

namespace Term
@[matchPattern] def var := @Term'.var
@[matchPattern] def app := @Term'.app
@[matchPattern] def lam := @Term'.lam

def liftTermEq {ty : Ty v} {ty' : Ty w} (eq : ty.type = ty'.type) : Term' ty → Term' ty'
  | .var a => .var $ eq ▸ a
  | .app t₁ t₂ => .app (liftTermEq eq t₁) (liftTermEq eq t₂)
  | .lam t => .lam (liftTermEq (by simp; rw [eq]) t)

def liftTerm' {ty : Ty v} : Term' ty → Term ty := liftTermEq (by rfl)

instance {ty : Ty v} : Coe (Term' ty) (Term ty) where
  coe := liftTerm'
instance {a : Type} : Coe (Term' (Ty.pure a).option) (Term (Option a)) where
  coe := liftTermEq (by rfl)
instance {a : Type} : Coe (Term (Option a)) (Term' (Ty.pure a).option) where
  coe := liftTermEq (by rfl)


def fvars : Term' ty → List ty
  | .var a => [a]
  | .app t₁ t₂ => fvars t₁ ++ fvars t₂
  | .lam t => (fvars t).bind (fun
    | none => []
    | some v => List.pure v)

@[simp] def depth : Term' ty → Nat
  | .var _ => 0
  | .app t₁ t₂ => max (depth t₁) (depth t₂) + 1
  | .lam t => depth t + 1

#check List

inductive TermHas {a} : {ty : Ty a} → ty → Term' ty → Prop :=
  | var : TermHas v (var v)
  | app₁ :  TermHas v t₁ → TermHas v (app t₁ t₂)
  | app₂ :  TermHas v t₂ → TermHas v (app t₁ t₂)
  | lam : {ty : Ty a} → {v : ty} → {t' : Term' ty.option} → TermHas (some v) t' → TermHas v (lam t')

@[simp] private def sizeBind (t : Term' ty) (f : (v : ty) → TermHas v t → Nat) : Nat := match t with
  | .var a => f a .var
  | .app t₁ t₂ => (sizeBind t₁ $ fun v h => f v $ .app₁ h) + (sizeBind t₂ $ fun v h => f v $ .app₂ h) + 1
  | .lam t' => sizeBind t' (fun v h => match v with
    | none => 0
    | some v => f v $ .lam h) + 1

@[simp] noncomputable def bindAuxSize (t : Term' ty) (f : (a : ty) → TermHas a t → Term' ty') : Nat := sizeBind t (fun v h => sizeOf $ f v h)

-- private def size_term_has_lt_bind
--   {ty : Ty v}
--   {ty' : Ty w}
--   (t' : Term' ty.option)
--   (b : ty)
--   (h : TermHas b (lam t'))
--   (f : (a : ty) → TermHas a (lam t') → Term' ty') :
--   sizeOf (f b h) < sizeBind t' (fun v h => match v with | none => 0 | some v => sizeOf $ f v $ .lam h) + 1
--   := by sorry

mutual
private def bindAux {ty : Ty v} {ty' : Ty w} (t : Term' ty) (f : (a : ty) → TermHas a t → Term' ty') : Term' ty' := match t with
  | .var a => f a .var
  | .app t₁ t₂ =>
      -- have : depth t₁ < max (depth t₁) (depth t₂) + 1 := by sorry
      -- have : depth t₂ < max (depth t₁) (depth t₂) + 1 := by sorry
      .app (bindAux t₁ $ fun v h => f v $ .app₁ h) (bindAux t₂ $ fun v h => f v $ .app₂ h)
  | .lam t' => .lam $ bindAux t' $ fun t h => match t with
      | none => var none
      | some v =>
          mapAux some (f v $ .lam h)
private def mapAux {ty : Ty v} {ty' : Ty w} (f : (ty → ty')) (t : Term' ty) : Term' ty' := bindAux t (fun v _ => .var $ f v)
end
termination_by
  bindAux t f => bindAuxSize t f + 1
  mapAux f t => sizeOf t
decreasing_by sorry

def pure (a : α) : Term α := Term.var a
def bind (t : Term α) (f : α → Term β) : Term β := bindAux t (fun v _ => f v)

instance : Monad Term where
  pure := pure
  bind := bind

end Term

I guess I can just apologize to lean for my lack of skills with `sorry'. Am I missing an easy WF relation to use, or tactics that can help me in the decreasing_by tactic?