The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

It looks to me like substSub is structurally recursive on s', and
substTy is recursive and terminating because t''' is an indirect
subcomponent of t'.  I think you might be able to convince Coq that
these all terminate by defining them in continuation-passing style
instead of by mutual recursion.  I think Coq's mutual recursion "with"
clause is very limited in that all functions involved have to recurse in
a structurally similar way.

If you separate out the "match nth..." component from substTy and turn
that also into continuation-passing style, then I think all of
these functions can be defined to be structurally recursive.

Also, it looks like that "match nth..." part needs a TUnit case.

On Mon, 3 Aug 2020 15:22:22 -0400
Junyoung Clare Jang <jjc9310 AT gmail.com> wrote:

> 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