coq – 定义具有类型参数约束的归纳依赖类型
发布时间:2020-12-14 04:59:55 所属栏目:百科 来源:网络整理
导读:我尝试在Coq中定义一个归纳依赖类型来表示位向量逻辑中的位向量变量. 我读了Xavier Leroy的blog post,他在其中定义了如下结构: Require Import Vector.Inductive bitvector : Type := Bitvector (n: nat) (v: Vector.t bool n). 然后,为了测试这种做法,我尝
我尝试在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)). 但是,我不明白为什么你想要在这种特殊情况下做到这一点,因为引理是完全可证明的:它是一个相当简单的推论,你可能会在以后需要更一般的引理. 你的定义(没有改变): 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. (编辑:李大同) 【声明】本站内容均来自网络,其相关言论仅代表作者个人观点,不代表本站立场。若无意侵犯到您的权利,请及时与联系站长删除相关内容! |