Coq 中 sig 类型元素的相等性

Question

使用像这样的 sig 类型定义：

Inductive A: Set := mkA : nat-> A.
Function getId (a: A) : nat := match a with mkA n => n end.
Function filter (a: A) : bool := if (beq_nat (getId a) 0) then true else false.
Coercion is_true : bool >-> Sortclass.
Definition subsetA : Set := { a : A | filter a }.

我试图证明它的投影是单射的：

Lemma projection_injective : 
  forall t1 t2: subsetA, proj1_sig t1 = proj1_sig t2 -> t1 = t2.
Proof.
 destruct t1.
 destruct t2.
 simpl.
 intros.
 rewrite -> H. (* <- stuck here *)
Abort.

此时，Coq 知道：

x : A
i : is_true (filter x)
x0 : A
i0 : is_true (filter x0)
H : x = x0

我尝试了一些重写但没有成功。例如，为什么我不能重写 i 和 H 来给 Coq 一个 i0？请问我在这里错过了什么？谢谢。

Answer 1

在你遇到困难的时候，你的目标大概是这样的：

exist x i = exist x0 i0

如果您键入的重写成功，您将获得以下目标：

exist x0 i = exist x0 i0

在这里，您可以了解 Coq 抱怨的原因：重写会产生错误类型的术语。问题是子项 exist x0 i 使用 i 作为类型 filter x0 的项，而实际上它的类型是 filter x。为了让 Coq 相信这不是问题，您需要在重写之前稍微调整一下您的目标：

Lemma projection_injective : 
  forall t1 t2: subsetA, proj1_sig t1 = proj1_sig t2 -> t1 = t2.
Proof.
 destruct t1.
 destruct t2.
 simpl.
 intros.
 revert i. (* <- this is new *)
 rewrite -> H. (* and now the tactic succeeds *)
 intros i.
Abort.

或者，您可以使用 subst 策略，它会尝试删除上下文中的所有冗余变量。这是上述脚本的更紧凑版本：

Lemma projection_injective :
  forall t1 t2: subsetA, proj1_sig t1 = proj1_sig t2 -> t1 = t2.
Proof.
  intros [x1 i1] [x2 i2]; simpl; intros e.
  subst.
Abort.

之后您可能会运行进入另一个问题：证明 filter x0 类型的任意两项相等。通常，您需要证明无关性公理才能证明这一点；但是，由于 filter 被定义为具有可判定相等性的类型的两个项之间的相等性，您可以证明此属性作为定理（Coq standard library 已经为您完成了）。

附带说明一下，包含您的属性的 mathcomp library already has a generic lemma 称为 val_inj。仅举个例子，人们可能会这样使用它：

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.

Inductive A: Set := mkA : nat-> A.
Function getId (a: A) : nat := match a with mkA n => n end.
Function filter (a: A) : bool := if (Nat.eqb (getId a) 0) then true else false.
Definition subsetA : Set := { a : A | filter a }.

Lemma projection_injective :
  forall t1 t2: subsetA, proj1_sig t1 = proj1_sig t2 -> t1 = t2.
Proof.
  intros t1 t2.
  apply val_inj.
Qed.

Coq 中 sig 类型元素的相等性

Equality for elements of sig type in Coq

subtype

coq