定义一个对类型参数有约束的归纳依赖类型
Define an inductive dependent-type with constraints on the type-parameter
我尝试在 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
。
所以,我想知道如何强制归纳依赖类型的参数严格为正。
欢迎任何提示!
一种方法是确保存储的 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.
为了确保我很好地理解 Arthur Azevedo De Amorim 的评论,我尝试重写我的 Coq 模块,试图删除语法糖和不必要的大小隐藏。
首先,仅通过查看 Coq 中的可用模块,就可以找到与我想要的非常接近的 Coq.Bool.Bvector
模块...但是,缺少了很多(尤其是模运算部分) 而且,我不同意一些规则,例如编码符号或将 true 和 false 作为 size = 1
) 的特定情况。
因此,我的模块几乎是 Coq.Bool.Bvector
的副本,但为了让我高兴而稍作修改(我可能是错的,我们将在未来看到它)。
这里是重写的模块:
Require Import Arith Bool Vector.
(** Unsigned Bitvector type *)
Definition bitvector := Vector.t bool.
Definition nil := @Vector.nil bool.
Definition cons := @Vector.cons bool.
Definition bv_low := @Vector.hd bool.
Definition bv_high := @Vector.tl bool.
(** A bitvector is false if zero and true otherwise. *)
Definition bv_test n (v : bitvector n) := Vector.fold_left orb false v.
(** Bitwise operators *)
Definition bv_neg n (v : bitvector n) := Vector.map negb v.
Definition bv_and n (v w : bitvector n) := Vector.map2 andb v w.
Definition bv_or n (v w : bitvector n) := Vector.map2 orb v w.
Definition bv_xor n (v w : bitvector n) := Vector.map2 xorb v w.
(** Shift/Rotate operators *)
(* TODO *)
(** Arithmetic operators *)
(* TODO *)
然后,我试图借助 Guillaume Allais 的提示(再次)证明双重否定:
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.
Theorem double_neg :
forall (n : nat) (v : bitvector n), bv_neg n (bv_neg n v) = v.
Proof.
intros; unfold bv_neg.
rewrite map_fusion, <- map_id.
apply map_extensional.
- intros []; reflexivity.
Qed.
而且,令我惊讶的是(对我来说),它就像一个魅力。
非常感谢大家,如果您对此代码有任何意见,请随时发表评论。由于我是 Coq 的新手,我真的很想改进。
您可以通过对 v
的归纳来证明定理。
Require Import Vector.
Definition bitvector := Vector.t bool.
Definition bv_neg n (v : bitvector n) := Vector.map negb v.
Theorem double_neg :
forall (n : nat) (v : bitvector n), bv_neg n (bv_neg n v) = v.
Proof.
induction v as [|x]; [|simpl; destruct x; rewrite IHv]; reflexivity.
Qed.
我尝试在 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
。
所以,我想知道如何强制归纳依赖类型的参数严格为正。
欢迎任何提示!
一种方法是确保存储的 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.
为了确保我很好地理解 Arthur Azevedo De Amorim 的评论,我尝试重写我的 Coq 模块,试图删除语法糖和不必要的大小隐藏。
首先,仅通过查看 Coq 中的可用模块,就可以找到与我想要的非常接近的 Coq.Bool.Bvector
模块...但是,缺少了很多(尤其是模运算部分) 而且,我不同意一些规则,例如编码符号或将 true 和 false 作为 size = 1
) 的特定情况。
因此,我的模块几乎是 Coq.Bool.Bvector
的副本,但为了让我高兴而稍作修改(我可能是错的,我们将在未来看到它)。
这里是重写的模块:
Require Import Arith Bool Vector.
(** Unsigned Bitvector type *)
Definition bitvector := Vector.t bool.
Definition nil := @Vector.nil bool.
Definition cons := @Vector.cons bool.
Definition bv_low := @Vector.hd bool.
Definition bv_high := @Vector.tl bool.
(** A bitvector is false if zero and true otherwise. *)
Definition bv_test n (v : bitvector n) := Vector.fold_left orb false v.
(** Bitwise operators *)
Definition bv_neg n (v : bitvector n) := Vector.map negb v.
Definition bv_and n (v w : bitvector n) := Vector.map2 andb v w.
Definition bv_or n (v w : bitvector n) := Vector.map2 orb v w.
Definition bv_xor n (v w : bitvector n) := Vector.map2 xorb v w.
(** Shift/Rotate operators *)
(* TODO *)
(** Arithmetic operators *)
(* TODO *)
然后,我试图借助 Guillaume Allais 的提示(再次)证明双重否定:
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.
Theorem double_neg :
forall (n : nat) (v : bitvector n), bv_neg n (bv_neg n v) = v.
Proof.
intros; unfold bv_neg.
rewrite map_fusion, <- map_id.
apply map_extensional.
- intros []; reflexivity.
Qed.
而且,令我惊讶的是(对我来说),它就像一个魅力。
非常感谢大家,如果您对此代码有任何意见,请随时发表评论。由于我是 Coq 的新手,我真的很想改进。
您可以通过对 v
的归纳来证明定理。
Require Import Vector.
Definition bitvector := Vector.t bool.
Definition bv_neg n (v : bitvector n) := Vector.map negb v.
Theorem double_neg :
forall (n : nat) (v : bitvector n), bv_neg n (bv_neg n v) = v.
Proof.
induction v as [|x]; [|simpl; destruct x; rewrite IHv]; reflexivity.
Qed.