{var%20f='http://v.t.sina.com.cn/share/share.php?appkey=1515056452',u=z||d.location,p=['&url=',e(u),'&title=',e(t||d.title),'&source=',e(r),'&sourceUrl=',e(l),'&content=',c||'gb2312','&pic=',e(p||'')].join('');function%20a(){if(!window.open([f,p].join(''),'mb',['toolbar=0,status=0,resizable=1,width=440,height=430,left=',(s.width-440)/2,',top=',(s.height-430)/2].join('')))u.href=[f,p].join('');};if(/Firefox/.test(navigator.userAgent))setTimeout(a,0);else%20a();})(screen,document,encodeURIComponent,'','','https://www.manongdao.com/data/attach/logo/logo.png', '推荐 老娘就宠你 的问题《How to indicate decreasing in size of two Coq indu》','https://www.manongdao.com/q-364692.html','页面编码gb2312|utf-8默认gb2312'));){kind=link}
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).
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
gameCompareas 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 asgameCompare. 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:
The
gameCompareTimefunction computes the sum of the sizes of both games, which seems like a reasonable bound on the depth of the call tree ofgameCompareAux. Notice that I've inlinedinnerGCompare, 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
gameComparewill require you to reason aboutgameCompareAuxand the termination time explicitly, which can be very fiddly.One way of indicating the decreasing arguments of a function is by using an ad-hoc predicate that describes the domain of that function.
Armed with some inversion lemmas and proof that your function is total you can define the function like this:
The proofs of the inversion lemmas must end with
Defined.instead ofQed.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:
You can use
Extraction Inlineon 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 returnProps instead ofbools.Full development here.