Cannot guess decreasing argument of fix

Using Coq
1

Hi! 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 .

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!

2

There are apparently two difficulties for Coq:

  1. Moving from (SBCon)::(SBSkip n)::l to (SBSkip n)::l is not detected as moving to a sub-list.
    This one can be easily fixed by using a move from (SBCon)::((SBSkip n)::l) as l') to l'.
  2. (SBSkip k)::l with n = S k is not a sub-list of (SBSkip n)::m::l
    This one requires a bit more work to make the recursive call really structurally decreasing. A solution is to introduce an intermediate function which skips all elements to be skipped.
1 Like
3

Thank you for your answer. The first one for SBCon and SBDis solves the problem, but for SBSkip I should make an intermediate function? Then how could I call it so that Coq understands that it is structurally decreasing?

4

I am not sure this is the best solution, but I hope the following is correct:

Fixpoint executeBool (state:M.t Z) (stack:list Z) (program:list insStBool) : list Z :=
  match program with 
  [...]
  | (SBSkip O)::l => executeBool state stack l
  | (SBSkip (S n))::l => executeBool_skip n state stack l
  [...]
  end
with executeBool_skip n (state:M.t Z) (stack:list Z) (program:list insStBool) : list Z :=
  match program with
  | nil => nil
  | _ :: l0 => 
    match n with
    | 0%nat => executeBool state stack l0
    | S n0 => executeBool_skip n0 state stack l0
    end
  end.

with executeBool_skip also structurally decreasing on program.

1 Like
5

It’s perfect! That exactly what I needed, thank you so much!