Coq 中 push/pop 求值器产生的奇怪证明义务

Question

我正在尝试在 Coq 中定义一种简单的基于堆栈的语言。目前，指令集包含压入 nat 的 push 和弹出一个的指令 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

我看不到 link k 的方法，它是 Prog 的类型参数，以及 n0，它是类型参数对于矢量类型 t.

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

Answer 1

我无法 Program Fixpoint 记住适当的相等性，但这里有一个使用策略的定义，我们可以在其中使用 remember 围绕相等性证明创建护航模式。证明项中的两个子证明是由abstract生成的；它们都是关于构造函数的非常简单的证明。

Fixpoint eval (n : nat) (p : Prog n) : t nat n.
  refine (match p with
          | push n' v p' => cons _ v _ (eval _ p')
          | pop' n' p' => _
          end).
  set (x := eval _ p').
  remember (S (S n')).
  destruct x.
  abstract congruence. (* nil case *)
  assert (n0 = S n') by (abstract congruence).
  rewrite H in x.
  exact x.
Defined.

Print eval.
(*
eval =
fix eval (n : nat) (p : Prog n) {struct p} :
t nat n :=
  match p in (Prog n0) return (t nat n0) with
  | push n' v p' => cons nat v n' (eval n' p')
  | pop' n' p' =>
      let x := eval (S (S n')) p' in
      let n0 := S (S n') in
      let Heqn0 : n0 = S (S n') := eq_refl in
      match
        x in (t _ n1)
        return (n1 = S (S n') -> Prog n1 -> t nat (S n'))
      with
      | nil _ =>
          fun (Heqn1 : 0 = S (S n')) (_ : Prog 0) =>
          eval_subproof n' Heqn1
      | cons _ _ n1 x0 =>
          fun (Heqn1 : S n1 = S (S n')) (_ : Prog (S n1)) =>
          let H : n1 = S n' := eval_subproof0 n' n1 Heqn1 in
          let x1 :=
            eq_rec n1 (fun n2 : nat => t nat n2) x0 (S n') H in
          x1
      end Heqn0 p'
  end
     : forall n : nat, Prog n -> t nat n
*)

Answer 2

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

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 插件，它为依赖模式匹配提供了更好的支持。

Answer 3

这里是使用方程式的尝试。

From Coq Require Import Vector.
From Equations Require Import Equations.

Equations eval (n : nat) (p : Prog n) : t nat n :=
  eval _ (push _ n p) := cons n (eval _ p);
  eval _ (pop' _ p) <= eval _ p => {
    eval _ (pop' _ p) (cons _ stack) := stack }.

但请注意，我并不完全确定自己在做什么。

Coq 中 push/pop 求值器产生的奇怪证明义务

Weird proof obligations resulting from a push/pop evaluator in Coq

proof

coq

dependent-type

proof-obligation