The Coq mailing list

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

Hi,

Thank you for the answer. However, I think the problem is more subtle. In the recursive call

substTy (substSub s n s'') d'' t'''

t''' comes from the first argument, so it's not necessarily smaller than t' (the third argument).

I cannot do anything just with first or third argument as this recursive call uses substSub s n s'' as the first argument where s'' is a subterm of the third, and t''' as the third that is a subterm of the first.

I tried to combine those two, but the first argument is not just s'' but substSub s n s'', so I need some facts that involves substSub.

Even if I can use something like that in my measure, all such sizes I have tried give me less than or equal to, not just less than...

And thank you for the suggestion. Unfortunately, my actual case is more complex, so I cannot use just a list for a sub(stitution). Maybe it's better to have used a list at list for this simplified version.

Best,

Clare Jang

2020년 8월 3일 (월) 오후 4:20, Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>님이 작성:

Hi,

To me the only non-structural case seems to be

the call on the match on the nth sub-term of our

snoc list sub-structure. Its size is smaller though.

It is actually a real sub-term but convincing Coq

that it is so could be very hard indeed.

In such a case, I do not see why a measure based

on the linear size would not work, in each Fixpoint on

the third argument. May be you struggle trying to

define mutual Fixpoints based on measures ?

Also if I may (and if possible), I would suggest that

you implement your type Ty so that snoc lists are

actual list as in eg

Inductive Ty : Set :=
| TUnit : Ty
| TBox : Ty -> Ty
| TUnbox : nat -> nat -> list Ty -> Ty

Definition Sub := list Ty.

Hence you could use the List library on

your type instead of having to recreate one. A snoc

notation could help if you want to see the list reversed.

You would switch mutual inductives with nested inductives

and would have to design a suitable recursor but once

done, you will find it easy to work with.

Best,

Dominique

---

De: "Junyoung Clare Jang" <jjc9310 AT gmail.com>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Lundi 3 Août 2020 21:22:22
Objet: [Coq-Club] Is there a measure for these functions?

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

--

Best,

Junyoung Clare Jang