代码之家 › 专栏 › 技术社区 › user1544337

Coq中推送/弹出评估器产生的奇怪证明义务

proof-obligation dependent-type proof coq

user1544337 · 技术社区 · 8 年前

我试图用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 如上所述(更改 流行音乐 到 弹出' )我得到了错误

术语“stack”的类型为“t nat n0”,而预期的类型为“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 。

为什么会这样 程序 产生这个奇怪的义务,我如何编写绕过这个问题的求值函数?

3 回复 | 直到 8 年前

Arthur Azevedo De Amorim 8 年前

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

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

Tej Chajed 8 年前

我找不到 Program Fixpoint 记住适当的平等,但这里有一个使用策略的定义,我们可以使用 remember 围绕等式证明创建护航模式。证明项中的两个子OF由生成 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
*)

Anton Trunov 8 年前

下面是一个使用公式的尝试。

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 }.

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