coq - Coq 中推/弹出计算器导致的奇怪的证明义务

Question

我正在尝试在 Coq 中定义一种简单的基于堆栈的语言。目前，指令集包含push，它压入一个nat，还有一个指令pop，它弹出一个。这个想法是程序是依赖类型的； Prog 2 是一个在执行后在堆栈上留下两个元素的程序。

这是通过这个简单的程序实现的:

Require Import Coq.Vectors.VectorDef.

Inductive Prog : nat -> Type :=
  | push : forall n : nat, nat -> Prog n -> Prog (S n)
  | pop  : forall n : nat, Prog (S n) -> Prog n.

Fixpoint eval (n : nat) (p : Prog n) : t nat n :=
  match p with
  | push _ n p => cons _ n _ (eval _ p)
  | pop _ p => match eval _ p with
    | cons _ _ _ stack => stack
    end
  end.

我现在想添加一条指令 pop'，它会弹出堆栈中的一个元素，但只能在堆栈中至少有两个元素时应用。

Inductive Prog : nat -> Type :=
  | push : forall n : nat, nat -> Prog n -> Prog (S n)
  | pop' : forall n : nat, Prog (S (S n)) -> Prog (S n).

当使用与上面相同的 Fixpoint 时(将 pop 更改为 pop')我得到错误

The term "stack" has type "t nat n0" while it is expected to have type "t nat (S k)".

所以我想我可以用 Program 来做到这一点。所以我使用:

Require Import Coq.Program.Tactics Coq.Logic.JMeq.

Program Fixpoint eval (n : nat) (p : Prog n) : t nat n :=
  match p with
  | push _ n p => cons _ n _ (eval _ p)
  | pop' k p => match eval _ p with
    | cons _ l _ stack => stack
    | nil _ => _
    end
  end.

但是，出于某种原因，这会产生奇怪的义务，我认为这是无法解决的。自动尝试后留下的第一个(两个)义务是:

k : nat
p0 : Prog (S k)
p : Prog (S (S k))
Heq_p : JMeq (pop' k p) p0
l, n0 : nat
stack : t nat n0
h : nat
t : t nat n0
Heq_anonymous0 : JMeq (cons nat l n0 stack) (cons nat h n0 t)
______________________________________(1/1)
n0 = S k

我没有找到一种方法来链接 k，它是 Prog 的类型参数，以及 n0，它是向量类型 t 的类型参数。

为什么这个程序会产生这个奇怪的义务，我该如何编写评估函数来规避这个问题？

Answer 1

在回答您的问题之前，请注意不可能用您的语言编写任何程序! (对你描述的问题没有任何影响，但无论如何还是值得指出来...)

From Coq Require Import Vectors.Vector.

Set Implicit Arguments.

Inductive Prog : nat -> Type :=
  | push : forall n : nat, nat -> Prog n -> Prog (S n)
  | pop' : forall n : nat, Prog (S (S n)) -> Prog (S n).

Fixpoint not_Prog n (p : Prog n) : False :=
  match p with
  | push _ p' => not_Prog p'
  | pop'   p' => not_Prog p'
  end.

现在，回答你的问题。正是由于这个和相关问题，许多人更愿意避免在 Coq 中使用这种编程风格。在这种情况下，我发现使用提取向量尾部的 tl 对您的函数进行编程会更容易。

From Coq Require Import Vectors.Vector.

Set Implicit Arguments.

Inductive Prog : nat -> Type :=
  | empty : Prog 0
  | push : forall n : nat, nat -> Prog n -> Prog (S n)
  | pop' : forall n : nat, Prog (S (S n)) -> Prog (S n).

Fixpoint eval (n : nat) (p : Prog n) : t nat n :=
  match p with
  | empty    => nil _
  | push n p => cons _ n _ (eval p)
  | pop'   p => tl (eval p)
  end.

如果您仍然对在 Coq 中使用这种数据类型感兴趣，您可能想看看 Equations插件，为依赖模式匹配提供更好的支持。