title: How to indicate decreasing in size of two Coq inductive types
body: <p>I'm trying to define the <code>game</code> inductive type for combinatorial games.  I want a comparison method which tells if two games are <code>lessOrEq</code>, <code>greatOrEq</code>, <code>lessOrConf</code> or <code>greatOrConf</code>.  Then I can check if two games are equal if they are both <code>lessOrEq</code> and <code>greatOrEq</code>.</p>
  
  <p>But when I try defining the mutually recursive methods for making this check, I get:</p>
  
  <blockquote>
    <p>Error: Cannot guess decreasing argument of <code>fix</code>.</p>
  </blockquote>
  
  <p>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?</p>
  
  <p>Here's my code.  The part that fails is the mutually recursive definition of <code>gameCompare</code>, <code>innerGCompare</code>, <code>listGameCompare</code>, <code>gameListCompare</code>.</p>
  
  <pre><code>Inductive game : Set :=
   | gameCons : gamelist -&gt; gamelist -&gt; game
  with gamelist : Set :=
   | emptylist : gamelist
   | listCons : game -&gt; gamelist -&gt; gamelist.
  
  Definition side :=
   game -&gt; gamelist.
  
  Definition leftSide (g : game) : gamelist :=
   match g with
    | gameCons gll glr =&gt; gll
   end.
  
  Definition rightSide (g : game) : gamelist :=
   match g with
    | gameCons gll glr =&gt; 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 =&gt; leftSide
    | greatOrEq =&gt; rightSide
    | lessOrConf =&gt; rightSide
    | greatOrConf =&gt; leftSide
   end.
  
  Definition g2side (c : compare_quest) : side :=
   match c with 
    | lessOrEq =&gt; rightSide
    | greatOrEq =&gt; leftSide
    | lessOrConf =&gt; leftSide
    | greatOrConf =&gt; rightSide
   end.
  
  Definition combiner :=
   Prop -&gt; Prop -&gt; Prop.
  
  Definition compareCombiner (c : compare_quest) : combiner :=
   match c with
    | lessOrEq =&gt; and
    | greatOrEq =&gt; and
    | lessOrConf =&gt; or
    | greatOrConf =&gt; or
   end.
  
  Definition nextCompare (c : compare_quest) : compare_quest :=
   match c with
    | lessOrEq =&gt; lessOrConf
    | greatOrEq =&gt; greatOrConf
    | lessOrConf =&gt; lessOrEq
    | greatOrConf =&gt; 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 =&gt; cbn_init cbn
    | listCons g1s_car g1s_cdr =&gt; 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 =&gt; cbn_init cbn
    | listCons g2s_car g2s_cdr =&gt; 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).
  </code></pre>