Coq：无法猜测 fix

问题描述

我正在尝试编写一个在堆栈程序中执行布尔运算的函数。到目前为止，我已经得到了下面的代码，但是由于某种原因，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.

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

解决方法

您有几个对 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 := ...

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

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

coq coqide