Coq：无法猜测 fix 的递减参数

Question

我正在尝试编写一个在堆栈程序中执行布尔运算的函数。到目前为止，我已经得到了下面的代码，但是由于某种原因，executeBool 不起作用。 Coq 显示错误“无法猜测修复的递减参数”，但我不太确定为什么，因为它看起来有点“明显” 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.

为什么会这样？无论我如何更改功能，我都会得到它......有什么办法可以解决它吗？谢谢！

Answer 1

program 在技术上是递减的，但你在语法上使用它时添加了一个构造函数，Coq 的递减检查不是很聪明。尝试为匹配中的子元素命名 as 并使用此名称：

    | (SBCon)::((SBSkip n)::l as l') => match stack with 
                                      | nil   => nil 
                                      | 0::st => executeBool state (0::st) (l')
                                      | _::st => executeBool state st l

Answer 2

您有一些对 executeBool 的递归调用，它们不是直接在程序的子项上调用，而是在您从子项重建的项上调用，例如 executeBool state (0::st) ((SBSkip n)::l)。解决方案是明确 (SBSkip n)::l 是程序的一个子项，方法是用 as 子句捕获相应的匹配案例

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

为了了解 Coq 哪里有问题，您还可以在定义中添加一个明确的 struct 子句以指示应该减少哪个参数（它还可以通过较大的固定点带来更好的性能） :

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

最后，作为未来问题的经验法则，请尽量减少您 post 的示例，并确保它们具有重现您的问题所需的所有导入（例如 M.t未定义，缺少 Z 和列表符号的导入）。

Coq：无法猜测 fix 的递减参数

Coq: Cannot guess decreasing argument of fix

coq

coqide