Coq 中归纳集的归纳子集
Inductive subset of an inductive set in Coq
我有一个用三个构造函数构建的 Inductive Set:
Inductive MF : Set :=
| D : MF
| cn : MF -> MF -> MF
| dn : Z -> MF -> MF.
我想以某种方式定义一个新的归纳集 B,使得 B 是 MF 的子集,仅包含从 D 和 dn 获得的元素。此外,如果需要,B 中的所有内容都应解释为类型 MF。
我尝试先定义 B,然后定义 MF,如下所示:
Inductive B : Set :=
| D : B
| dn : Z -> B -> B.
Inductive MF : Set :=
| m : B -> MF
| cn : MF -> MF -> MF
| Dn : Z -> MF -> MF.
Axiom m_inj : forall (a b : B), m a = m b -> a = b.
Coercion m : B >-> MF.
Axiom dnDn : forall (a : B)(i : Z), (m (dn i a)) = (Dn i (m a)).
这里的问题是我必须构造函数(dn 和 Dn),它们应该可以与 B 中的元素互换。这给我在进一步开发中带来了很多问题,我必须不断添加公理以便获得预期的行为。
您可以将 B
定义为将 MF
元素与仅使用 D
和 dn
构建的证明一起打包的记录。为此,您需要首先定义一个谓词 isB : MF -> Prop
,描述 MF
的元素,即 B
s.
Require Import ZArith.
Inductive MF : Set :=
| D : MF
| cn : MF -> MF -> MF
| dn : Z -> MF -> MF.
Inductive isB : MF -> Prop :=
| DIsOK : isB D
| dnIsOK : forall z mf, isB mf -> isB (dn z mf).
Record B := mkB
{ mf : MF
; prf : isB mf
}.
Coercion mf : B >-> MF.
请注意,您必须证明 isB mf
在您的设置中享有证明无关性,否则 Coq 不会知道投影 mf
是单射的。通常,您希望 MF
中的相等性暗示您的子类型 B
.
中的相等性
我建议以下变体:
Require Import Bool ZArith Eqdep_dec.
Inductive MF : Set :=
| D : MF
| cn : MF -> MF -> MF
| dn : Z -> MF -> MF.
Inductive isB : MF -> Prop :=
| DIsOK : isB D
| dnIsOK : forall z mf, isB mf -> isB (dn z mf).
Fixpoint isBb (mf : MF) : bool :=
match mf with
| D => true
| dn _ mf => isBb mf
| _ => false
end.
Lemma mfP mf : reflect (isB mf) (isBb mf).
Proof.
apply iff_reflect; split.
+ elim mf; auto; simpl; intros mf1 ihmf1 mf2 ihmf2.
- now intros hisB; inversion hisB.
- now inversion ihmf2; rewrite mf2.
+ now elim mf; simpl; try repeat (auto||constructor||congruence).
Qed.
Record B := mkB
{ mf : MF
; prf : isBb mf = true
}.
Coercion mf : B >-> MF.
(* From http://cstheory.stackexchange.com/questions/5158/prove-proof-irrelevance-in-coq *)
Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.
Proof.
intros; apply Eqdep_dec.eq_proofs_unicity; intros.
now destruct (Bool.bool_dec x y); tauto.
Qed.
Lemma valB b1 b2 : mf b1 = mf b2 -> b1 = b2.
Proof.
destruct b1, b2; simpl; intros ->.
now rewrite (bool_pirrel (isBb mf1) prf0 prf1).
Qed.
math-comp 库对布尔谓词的子类型提供了强大而系统的支持,如果您发现自己要处理许多子类型,您可能想试一试。
我有一个用三个构造函数构建的 Inductive Set:
Inductive MF : Set :=
| D : MF
| cn : MF -> MF -> MF
| dn : Z -> MF -> MF.
我想以某种方式定义一个新的归纳集 B,使得 B 是 MF 的子集,仅包含从 D 和 dn 获得的元素。此外,如果需要,B 中的所有内容都应解释为类型 MF。
我尝试先定义 B,然后定义 MF,如下所示:
Inductive B : Set :=
| D : B
| dn : Z -> B -> B.
Inductive MF : Set :=
| m : B -> MF
| cn : MF -> MF -> MF
| Dn : Z -> MF -> MF.
Axiom m_inj : forall (a b : B), m a = m b -> a = b.
Coercion m : B >-> MF.
Axiom dnDn : forall (a : B)(i : Z), (m (dn i a)) = (Dn i (m a)).
这里的问题是我必须构造函数(dn 和 Dn),它们应该可以与 B 中的元素互换。这给我在进一步开发中带来了很多问题,我必须不断添加公理以便获得预期的行为。
您可以将 B
定义为将 MF
元素与仅使用 D
和 dn
构建的证明一起打包的记录。为此,您需要首先定义一个谓词 isB : MF -> Prop
,描述 MF
的元素,即 B
s.
Require Import ZArith.
Inductive MF : Set :=
| D : MF
| cn : MF -> MF -> MF
| dn : Z -> MF -> MF.
Inductive isB : MF -> Prop :=
| DIsOK : isB D
| dnIsOK : forall z mf, isB mf -> isB (dn z mf).
Record B := mkB
{ mf : MF
; prf : isB mf
}.
Coercion mf : B >-> MF.
请注意,您必须证明 isB mf
在您的设置中享有证明无关性,否则 Coq 不会知道投影 mf
是单射的。通常,您希望 MF
中的相等性暗示您的子类型 B
.
我建议以下变体:
Require Import Bool ZArith Eqdep_dec.
Inductive MF : Set :=
| D : MF
| cn : MF -> MF -> MF
| dn : Z -> MF -> MF.
Inductive isB : MF -> Prop :=
| DIsOK : isB D
| dnIsOK : forall z mf, isB mf -> isB (dn z mf).
Fixpoint isBb (mf : MF) : bool :=
match mf with
| D => true
| dn _ mf => isBb mf
| _ => false
end.
Lemma mfP mf : reflect (isB mf) (isBb mf).
Proof.
apply iff_reflect; split.
+ elim mf; auto; simpl; intros mf1 ihmf1 mf2 ihmf2.
- now intros hisB; inversion hisB.
- now inversion ihmf2; rewrite mf2.
+ now elim mf; simpl; try repeat (auto||constructor||congruence).
Qed.
Record B := mkB
{ mf : MF
; prf : isBb mf = true
}.
Coercion mf : B >-> MF.
(* From http://cstheory.stackexchange.com/questions/5158/prove-proof-irrelevance-in-coq *)
Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.
Proof.
intros; apply Eqdep_dec.eq_proofs_unicity; intros.
now destruct (Bool.bool_dec x y); tauto.
Qed.
Lemma valB b1 b2 : mf b1 = mf b2 -> b1 = b2.
Proof.
destruct b1, b2; simpl; intros ->.
now rewrite (bool_pirrel (isBb mf1) prf0 prf1).
Qed.
math-comp 库对布尔谓词的子类型提供了强大而系统的支持,如果您发现自己要处理许多子类型,您可能想试一试。