How to indicate decreasing in size of two Coq indu

问题:

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

回答1:

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.

回答2:

One way of indicating the decreasing arguments of a function is by using an ad-hoc predicate that describes the domain of that function.

Inductive gameCompareDom : compare_quest ->  game -> game -> Prop :=
  | gameCompareDom1 : forall c g1 g2, innerGCompareDom (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2) -> gameCompareDom c g1 g2

with innerGCompareDom : compare_quest -> combiner -> game -> gamelist -> game -> gamelist -> Prop :=
  | innerGCompareDom1 : forall next_c cbn g1 g1s g2 g2s, listGameCompareDom next_c cbn g1s g2 -> gameListCompareDom next_c cbn g1 g2s -> innerGCompareDom next_c cbn g1 g1s g2 g2s

with listGameCompareDom : compare_quest -> combiner -> gamelist -> game -> Prop :=
  | listGameCompareDom1 : forall c cbn g1s g2, g1s = emptylist -> listGameCompareDom c cbn g1s g2
  | listGameCompareDom2 : forall c cbn g1s g2 g1s_car g1s_cdr, g1s = listCons g1s_car g1s_cdr -> gameCompareDom c g1s_car g2 -> listGameCompareDom c cbn g1s_cdr g2 -> listGameCompareDom c cbn g1s g2

with gameListCompareDom : compare_quest -> combiner -> game -> gamelist -> Prop :=
  | gameListCompareDom1 : forall c cbn g1 g2s, g2s = emptylist -> gameListCompareDom c cbn g1 g2s
  | gameListCompareDom2 : forall c cbn g1 g2s g2s_car g2s_cdr, g2s = listCons g2s_car g2s_cdr -> gameCompareDom c g1 g2s_car -> gameListCompareDom c cbn g1 g2s_cdr -> gameListCompareDom c cbn g1 g2s.

Armed with some inversion lemmas and proof that your function is total you can define the function like this:

Lemma gameCompareDom1Inv : forall c g1 g2, gameCompareDom c g1 g2 ->
  innerGCompareDom (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2).

Lemma innerGCompareDom1Inv1 : forall next_c cbn g1 g1s g2 g2s,
  innerGCompareDom next_c cbn g1 g1s g2 g2s ->
  listGameCompareDom next_c cbn g1s g2.

Lemma innerGCompareDom1Inv2 : forall next_c cbn g1 g1s g2 g2s,
  innerGCompareDom next_c cbn g1 g1s g2 g2s ->
  gameListCompareDom next_c cbn g1 g2s.

Lemma listGameCompareDom2Inv1 : forall c cbn g1s g2 g1s_car g1s_cdr,
  listGameCompareDom c cbn g1s g2 -> g1s = listCons g1s_car g1s_cdr ->
  gameCompareDom c g1s_car g2.

Lemma listGameCompareDom2Inv2 : forall c cbn g1s g2 g1s_car g1s_cdr,
  listGameCompareDom c cbn g1s g2 -> g1s = listCons g1s_car g1s_cdr ->
  listGameCompareDom c cbn g1s_cdr g2.

Lemma gameListCompareDom2Inv1 : forall c cbn g1 g2s g2s_car g2s_cdr,
  gameListCompareDom c cbn g1 g2s -> g2s = listCons g2s_car g2s_cdr ->
  gameCompareDom c g1 g2s_car.

Lemma gameListCompareDom2Inv2 : forall c cbn g1 g2s g2s_car g2s_cdr,
  gameListCompareDom c cbn g1 g2s -> g2s = listCons g2s_car g2s_cdr ->
  gameListCompareDom c cbn g1 g2s_cdr.

Fixpoint gameCompareAux (c : compare_quest) (g1 : game) (g2 : game) (H1 : gameCompareDom c g1 g2) : Prop :=
  innerGCompareAux (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2) (gameCompareDom1Inv _ _ _ H1)

with innerGCompareAux (next_c : compare_quest) (cbn : combiner) (g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) (H1 : innerGCompareDom next_c cbn g1 g1s g2 g2s) : Prop :=
  cbn (listGameCompareAux next_c cbn g1s g2 (innerGCompareDom1Inv1 _ _ _ _ _ _ H1)) (gameListCompareAux next_c cbn g1 g2s (innerGCompareDom1Inv2 _ _ _ _ _ _ H1))

with listGameCompareAux (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) (H1 : listGameCompareDom c cbn g1s g2) : Prop :=
  match g1s as gl1 return g1s = gl1 -> Prop with
  | emptylist                => fun H2 => cbn_init cbn
  | listCons g1s_car g1s_cdr => fun H2 => cbn (gameCompareAux c g1s_car g2 (listGameCompareDom2Inv1 _ _ _ _ _ _ H1 H2)) (listGameCompareAux c cbn g1s_cdr g2 (listGameCompareDom2Inv2 _ _ _ _ _ _ H1 H2))
  end eq_refl

with gameListCompareAux (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) (H1 : gameListCompareDom c cbn g1 g2s) : Prop :=
  match g2s as gl1 return g2s = gl1 -> Prop with
  | emptylist                => fun H2 => cbn_init cbn
  | listCons g2s_car g2s_cdr => fun H2 => cbn (gameCompareAux c g1 g2s_car (gameListCompareDom2Inv1 _ _ _ _ _ _ H1 H2)) (gameListCompareAux c cbn g1 g2s_cdr (gameListCompareDom2Inv2 _ _ _ _ _ _ H1 H2))
  end eq_refl.

Lemma gameCompareTot : forall c g1 g2, gameCompareDom c g1 g2.

Lemma innerGCompareTot : forall next_c cbn g1 g1s g2 g2s,
  innerGCompareDom next_c cbn g1 g1s g2 g2s.

Lemma listGameCompareTot : forall g2 g1s c cbn,
  listGameCompareDom c cbn g1s g2.

Lemma gameListCompareTot : forall g1 g2s c cbn,
  gameListCompareDom c cbn g1 g2s.

Definition gameCompare (c : compare_quest) (g1 : game) (g2 : game) : Prop :=
  gameCompareAux c g1 g2 (gameCompareTot _ _ _).

Definition innerGCompare (next_c : compare_quest) (cbn : combiner) (g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) : Prop :=
  innerGCompareAux next_c cbn g1 g1s g2 g2s (innerGCompareTot _ _ _ _ _ _).

Definition listGameCompare (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) : Prop :=
  listGameCompareAux c cbn g1s g2 (listGameCompareTot _ _ _ _).

Definition gameListCompare (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) : Prop :=
  gameListCompareAux c cbn g1 g2s (gameListCompareTot _ _ _ _).

The proofs of the inversion lemmas must end with Defined. instead of Qed. so that their content is transparent and available for computation. They must also not reference any opaque theorems.

Afterwards, you should be able to define the following equation lemmas by resorting to the axiom of proof irrelevance:

Lemma gameCompareEq : forall c g1 g2, gameCompare c g1 g2 =
  innerGCompare (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2).

Lemma innerGCompareEq : forall next_c cbn g1 g1s g2 g2s, innerGCompare next_c cbn g1 g1s g2 g2s =
  cbn (listGameCompare next_c cbn g1s g2) (gameListCompare next_c cbn g1 g2s).

Lemma listGameCompareEq : forall c cbn g1s g2, listGameCompare c cbn g1s g2 =
  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.

Lemma gameListCompareEq : forall c cbn g1 g2s, gameListCompare c cbn g1 g2s =
  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.

You can use Extraction Inline on the auxiliary functions so that your main functions look like you would expect them to when extracted. But that doesn't apply here because your functions return Props instead of bools.

Full development here.