How to indicate decreasing in size of two Coq inductive types

Question

I'm trying to define the game inductive type for combinatorial games. I want a comparison method which tells if two games are lessOrEq, greatOrEq, lessOrConf or greatOrConf. Then I can check if two games are equal if they are both lessOrEq and greatOrEq.

But when I try defining the mutually recursive methods for making this check, I get:

Error: Cannot guess decreasing argument of fix.

I think this is because only one game or the other decreases in size with each recursive call (but not both). How can I indicate this to Coq?

Here's my code. The part that fails is the mutually recursive definition of gameCompare, innerGCompare, listGameCompare, gameListCompare.

Inductive game : Set :=
 | gameCons : gamelist -> gamelist -> game
with gamelist : Set :=
 | emptylist : gamelist
 | listCons : game -> gamelist -> gamelist.

Definition side :=
 game -> gamelist.

Definition leftSide (g : game) : gamelist :=
 match g with
  | gameCons gll glr => gll
 end.

Definition rightSide (g : game) : gamelist :=
 match g with
  | gameCons gll glr => glr
 end.

Inductive compare_quest : Set :=
 | lessOrEq : compare_quest
 | greatOrEq : compare_quest
 | lessOrConf : compare_quest
 | greatOrConf : compare_quest.

Definition g1side (c : compare_quest) : side :=
 match c with
  | lessOrEq => leftSide
  | greatOrEq => rightSide
  | lessOrConf => rightSide
  | greatOrConf => leftSide
 end.

Definition g2side (c : compare_quest) : side :=
 match c with 
  | lessOrEq => rightSide
  | greatOrEq => leftSide
  | lessOrConf => leftSide
  | greatOrConf => rightSide
 end.

Definition combiner :=
 Prop -> Prop -> Prop.

Definition compareCombiner (c : compare_quest) : combiner :=
 match c with
  | lessOrEq => and
  | greatOrEq => and
  | lessOrConf => or
  | greatOrConf => or
 end.

Definition nextCompare (c : compare_quest) : compare_quest :=
 match c with
  | lessOrEq => lessOrConf
  | greatOrEq => greatOrConf
  | lessOrConf => lessOrEq
  | greatOrConf => greatOrEq
 end.

Definition cbn_init (cbn : combiner) : Prop :=
 ~ (cbn False True).

Fixpoint gameCompare (c : compare_quest) (g1 : game) (g2 : game) : Prop :=
 innerGCompare (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2)
with innerGCompare (next_c : compare_quest) (cbn : combiner)
      (g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) : Prop :=
 cbn (listGameCompare next_c cbn g1s g2) (gameListCompare next_c cbn g1 g2s)
with listGameCompare (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) : Prop :=
 match g1s with
  | emptylist => cbn_init cbn
  | listCons g1s_car g1s_cdr => cbn (gameCompare c g1s_car g2) (listGameCompare c cbn g1s_cdr g2)
 end
with gameListCompare (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) : Prop :=
 match g2s with
  | emptylist => cbn_init cbn
  | listCons g2s_car g2s_cdr => cbn (gameCompare c g1 g2s_car) (gameListCompare c cbn g1 g2s_cdr)
 end.

Definition game_eq (g1 : game) (g2 : game) : Prop :=
 (gameCompare lessOrEq g1 g2) /\ (gameCompare greatOrEq g1 g2).

I've given an answer below, but if you could explain in more detail what your code is trying to do, I can try to improve it! — Arthur Azevedo De Amorim

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2013-06-25T17:52:57

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

How to indicate decreasing in size of two Coq inductive types

2 Answers