时间戳

首页 > 解决方案 > Coq：无法猜测修复的递减参数

coq - Coq：无法猜测修复的递减参数

问题描述

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

为什么会这样？不管我改变多少功能，我都会得到它......有什么办法可以解决它吗？谢谢！

标签： coqcoqide

解决方案

您有一些递归调用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，未定义，导入 forZ和 for 列表符号丢失） .

推荐阅读