Coq: Cannot guess decreasing argument of fix

Question

I am trying to write a function that executes boolean operations in a stack program. So far I have got the code bellow but, for some reason, executeBool doesn't work. Coq shows the error "Cannot guess decreasing argument of fix" but I'm not quite sure why since it seems a bit "obvious" that is it program.

Require Import ZArith.
Require Import List.
Require Import Recdef.
Require Import Coq.FSets.FMaps.
Require Import Coq.Strings.String.

Module Import M := FMapList.Make(String_as_OT). 

Set Implicit Arguments.
Open Scope Z_scope. 
Open Scope string_scope.

Inductive insStBool : Type :=
  | SBPush    : Z -> insStBool
  | SBLoad    : string -> insStBool
  | SBNeg     : insStBool
  | SBCon     : insStBool
  | SBDis     : insStBool
  | SBEq      : insStBool
  | SBLt      : insStBool
  | SBSkip    : nat -> insStBool.

Definition getVal (s:string) (st:M.t Z) : Z := 
  match (find s st) with 
    | Some val => val
    | None     => 0
  end.

Fixpoint executeBool (state:M.t Z) (stack:list Z) (program:list insStBool) : list Z :=
  match program with 
    | nil              => stack
    | (SBPush n)::l    => executeBool state (n::stack) l
    | (SBLoad x)::l    => executeBool state ((getVal x state)::stack) l
    | (SBNeg)::l       => match stack with 
                            | nil   => nil
                            | 0::st => executeBool state (1::st) l
                            | _::st => executeBool state (0::st) l
                          end
    | (SBCon)::(SBSkip n)::l  => match stack with 
                                      | nil   => nil 
                                      | 0::st => executeBool state (0::st) ((SBSkip n)::l)
                                      | _::st => executeBool state st l
                                 end
    | (SBDis)::(SBSkip n)::l  => match l with 
                                  | nil  => nil
                                  | m::k =>
                                    match stack with 
                                      | nil   => nil 
                                      | 0::st => executeBool state st l
                                      | _::st => executeBool state (1::st) ((SBSkip n)::l)
                                    end
                                 end
    | (SBSkip n)::m::l => match n with 
                            | 0%nat => executeBool state stack (m::l)
                            | (S k) => executeBool state stack ((SBSkip k)::l)
                          end
    | (SBEq)::l        => match stack with 
                            | nil      => nil 
                            | n::nil   => nil 
                            | n::m::st => match (m - n) with 
                                            | 0 => executeBool state (1::st) l
                                            | _ => executeBool state (0::st) l
                                          end
                          end  
    | (SBLt)::l        => match stack with 
                            | nil      => nil 
                            | n::nil   => nil 
                            | n::m::st => match (m - n) with 
                                            | Z.pos x => executeBool state (1::st) l
                                            | _       => executeBool state (0::st) l
                                          end
                          end
    | _ => nil
    end.

Why does this happen? No matter how much I change the function, I keep getting it... Is there any way to fix it? Thank you!

kyo dralliam kyo dralliam · Accepted Answer · 2021-06-13T17:04:24

You have a few recursive calls to executeBool that are not called directly on a subterm of progam but on a term that you rebuilt out of subterms for instance executeBool state (0::st) ((SBSkip n)::l). The solution is to make explicit that (SBSkip n)::l is a subterm of program by writing the corresponding match case with an as clause capturing that subterm

match program with
...
| (SBCon)::(((SBSkip n)::l) as l')  => ... executeBool state (0::st) l'
...

In order to understand where Coq is having troubles, you could also have added an explicit struct clause to your definition to indicate which parameter should be decreasing (it can also lead to better performances with large fixpoints):

Fixpoint executeBool (state:M.t Z) (stack:list Z) (program:list insStBool) {struct program} : list Z := ...

Finally, as a rule of thumb for future questions, please try to minimize the examples that you post and make sure that they have all the necessary imports to reproduce your problem (e.g. M.t is not defined, the imports for Z and for list notations are missing).

Coq: Cannot guess decreasing argument of fix

2 Answers