https://stackoverflow.com/questions/17297165
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianThere are probably several things you can do to solve this problem. I couldn't really understand what your code is trying to do, so maybe there are more efficient ways of doing this than the ones I'm about to mention.
One thing you can do is to define gameCompare as a (possibly mutually) inductive relation instead of a function. I don't know how familiar you are with Coq, so I won't explain this in detail because the answer will get too big, but inductive relations give you much greater flexibility than functions when defining concepts such as gameCompare. For more information on how to define inductive relations, you can check Benjamin Pierce's book Software Foundations.
One drawback of this approach is that inductive relations, unlike functions, don't really compute anything. This makes them sometimes harder to use. In particular, you can't simplify an inductive proposition like you can simplify a function call.
Another approach, which might be easier to apply to your problem, is to add a "time" number parameter to your functions that decreases with every recursive call. This makes the functions trivially terminating. Then, to make it work, you just have to make sure that you do your initial call with a big enough "time" parameter. Here's an example of how you can do this:
Fixpoint gameSize (g : game) : nat :=
match g with
| gameCons gl1 gl2 => 1 + gameListSize gl1 + gameListSize gl2
end
with gameListSize (gl : gamelist) : nat :=
match gl with
| emptylist => 1
| listCons g gl => 1 + gameSize g + gameListSize gl
end.
Definition gameCompareTime (g1 g2 : game) : nat :=
gameSize g1 + gameSize g2.
Fixpoint gameCompareAux (time : nat) (c : compare_quest) (g1 : game) (g2 : game) : Prop :=
match time with
| O => True
| S time =>
compareCombiner c
(listGameCompare time
(nextCompare c)
(compareCombiner c)
(g1side c g1)
g2)
(gameListCompare time
(nextCompare c)
(compareCombiner c)
g1
(g2side c g2))
end
with listGameCompare (time : nat) (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) : Prop :=
match time with
| 0 => True
| S time =>
match g1s with
| emptylist => cbn_init cbn
| listCons g1s_car g1s_cdr => cbn (gameCompareAux time c g1s_car g2) (listGameCompare time c cbn g1s_cdr g2)
end
end
with gameListCompare (time : nat) (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) : Prop :=
match time with
| 0 => True
| S time =>
match g2s with
| emptylist => cbn_init cbn
| listCons g2s_car g2s_cdr => cbn (gameCompareAux time c g1 g2s_car) (gameListCompare time c cbn g1 g2s_cdr)
end
end.
Definition gameCompare c g1 g2 :=
gameCompareAux (gameCompareTime g1 g2) c g1 g2.
Definition game_eq (g1 : game) (g2 : game) : Prop :=
(gameCompare lessOrEq g1 g2) /\ (gameCompare greatOrEq g1 g2).
The gameCompareTime function computes the sum of the sizes of both games, which seems like a reasonable bound on the depth of the call tree of gameCompareAux. Notice that I've inlined innerGCompare, since that makes the bound a little bit easier to compute. When the time ends (i.e., the 0 branch on the pattern matching), we return an arbitrary value (True, in this case), because we will have given the function enough time for it to finish before reaching that case.
The advantage of this approach is that it is relatively easy to implement. The drawback is that proving anything about gameCompare will require you to reason about gameCompareAux and the termination time explicitly, which can be very fiddly.
