Coq中sig类型元素的相等性

Question

Coq中sig类型元素的相等性

4

有一个如下的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？请问我在这里错过了什么？谢谢。

- Zheng Cheng

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Arthur Azevedo De Amorim · Accepted Answer

在你卡住的那一点，你的目标大致如下：

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标准库已经为您完成了这项工作）。

顺便说一下，mathcomp库已经有一个泛型引理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.