coq - 定义一个对类型参数有约束的归纳依赖类型

Question

我尝试在 Coq 中定义一个归纳依赖类型来表示位向量逻辑中的位向量变量。

我读了 Xavier Leroy 的 blog post，他在其中定义了这样一个结构:

Require Import Vector.

Inductive bitvector : Type := Bitvector (n: nat) (v: Vector.t bool n).

然后，为了测试这种方式，我尝试定义按位否定运算符如下:

Definition bv_neg (v : bitvector) :=
    match v with
        Bitvector n w => Bitvector n (Vector.map negb w)
    end.

并且，开始证明应用两次否定等价于恒等式:

Lemma double_neg :
   forall (v : bitvector), (bv_neg (bv_neg v) = v).

但是，当我试图做证明时，我意识到在每个证明中使用一个零大小的位向量是没有意义的并且强制处理特殊情况 n = 0。

所以，我想知道如何强制归纳依赖型的参数严格为正。

欢迎任何提示!

Answer 1

一种方法是确保存储的 Vector 的大小为 S n 。

Inductive bitvector : Type := Bitvector (n: nat) (v: Vector.t bool (S n)).

但是，鉴于引理是完全可证明的，我不明白您为什么要在这种特殊情况下这样做:它是您稍后可能需要的更一般引理的相当简单的推论。

您的定义(没有 S n 更改):

Require Import Vector.

Inductive bitvector : Type := Bitvector (n: nat) (v: Vector.t bool n).

Definition bv_neg (v : bitvector) :=
    match v with
        Bitvector n w => Bitvector n (Vector.map negb w)
    end.

Vector.map 的一些结果:

Lemma map_fusion : 
  forall {A B C} {g : B -> C} {f : A -> B} {n : nat} (v : Vector.t A n),
    Vector.map g (Vector.map f v) = Vector.map (fun x => g (f x)) v.
Proof.
intros A B C g f n v ; induction v.
  - reflexivity.
  - simpl; f_equal; assumption.
Qed.

Lemma map_id : 
  forall {A} {n : nat} (v : Vector.t A n), Vector.map (@id A) v = v.
Proof.
intros A n v ; induction v.
  - reflexivity.
  - simpl; f_equal; assumption.
Qed.

Lemma map_extensional : 
  forall {A B} {f1 f2 : A -> B} 
         (feq : forall a, f1 a = f2 a) {n : nat} (v : Vector.t A n),
    Vector.map f1 v = Vector.map f2 v.
Proof.
intros A B f1 f2 feq n v ; induction v.
  - reflexivity.
  - simpl; f_equal; [apply feq | assumption].
Qed.

最后，你的结果:

Lemma double_neg :
   forall (v : bitvector), (bv_neg (bv_neg v) = v).
Proof.
intros (n, v).
 simpl; f_equal.
 rewrite map_fusion, <- map_id.
 apply map_extensional.
 - intros []; reflexivity.
Qed.