The Coq mailing list

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

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

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

Another way to convince Coq of termination is to add a height param
to Sub and Ty, and use that as the measure.

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