The Coq mailing list

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

On Mon, 3 Aug 2020 16:32:05 -0400
"jonikelee AT gmail.com" <jonikelee AT gmail.com> wrote:

> 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.

No - it isn't missing a TUnit case - I was just parsing all those
primes in t''' as a pattern instead of a binding. Sorry.

> 
> 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  
>