Coq 中归纳集的归纳子集答案

【问题标题】：Inductive subset of an inductive set in CoqCoq 中归纳集的归纳子集
【发布时间】：2016-02-09 10:47:24
【问题描述】：

我有一个由三个构造函数构建的归纳集：

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 中的元素互换。这给我在进一步的开发中带来了很多问题，我必须不断添加 Axioms 以获得预期的行为。

【问题讨论】：

标签： coq

【解决方案1】：

请注意，您必须证明 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 库对布尔谓词的子类型提供了强大而系统的支持，如果您发现自己要处理许多子类型，可能需要尝试一下。

【讨论】：

抱歉这么晚才回复。我已经离线一段时间了。谢谢你的详细回答。我想我必须阅读更多关于证明无关性的内容，因为我不太熟悉它。我什至没有想到。
不客气！证明无关性的想法很简单：想象一个证明p : exists k, P k。在 Coq 中，证明是程序，所以实际上，我们可以在这里有不同的程序 p 来实现所需的引理 exists k, P k。然而，这意味着给定我们引理p1 p2 : exists... 的两个证明，我们不能证明p1 = p2。然而，在很多情况下，我们想要这样做，因为我们不关心证明本身，只关心属性。这就是证明无关性发挥作用的时候。对于某些类的证明，比如上面的，它可以推导出来，对于其他的，你需要使用一个公理。
再次感谢！这听起来像是一个有趣的话题。我会记住这一点。

【解决方案2】：

您可以将B 定义为将MF 元素与仅使用D 和dn 构建的证明一起包装的记录。为此，您需要首先定义一个谓词isB : MF -> Prop，描述MF 的元素Bs。

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.

【讨论】：