The Coq mailing list

[Junyoung Clare Jang <jjc9310 AT gmail.com>]

Dear All,

While I am trying to prove some properties of my language, the following functions come up.

Inductive Sub : Set :=
| NullS : Sub
| SnocS : Sub -> Ty -> Sub
with Ty : Set :=
| TUnit : Ty
| TBox : Ty -> Ty
| TUnbox : nat -> nat -> Sub -> Ty
.

Fixpoint nth (s : Sub) (x : nat) : Ty :=
  match s with
  | NullS => TUnit
  | SnocS s' t' =>
    match x with
    | O => t'
    | S x' => nth s' x'
    end
  end
.
Fixpoint substSub (s : Sub) (n : nat) (s' : Sub) : Sub :=
  match s' with
  | NullS => NullS
  | SnocS s'' t'' => SnocS (substSub s n s'') (substTy s n t'')
  end
with substTy (s : Sub) (n : nat) (t' : Ty) : Ty :=
  match t' with
  | TUnit => TUnit
  | TBox t'' => TBox (substTy s n t'')
  | TUnbox x'' d'' s'' =>
    if eq_dec d'' n
    then
      match nth s x'' with
      | TBox t''' => substTy (substSub s n s'') d'' t'''
      | t''' => TUnit
      end
    else
      TUnbox x'' d'' (substSub s n s'')
  end
.

(I simplified the actual version a little)

However, substSub and substTy are clearly not structurally recursive, so I tried several measures in order to define them, but none of those worked. I also attempted to find a looping example, and that was also unsuccessful. Do these functions terminate? I will appreciate any helps to show these functions are terminating or non-terminating...

Thanks,

Clare Jang