coq - 反转在 Coq 中产生意外的存在

Question

这是我在数学定理中使用的归纳类型 pc。

Inductive pc ( n : nat ) : Type :=
  | pcs : forall ( m : nat ), m < n -> pc n
  | pcm : pc n -> pc n -> pc n.

而另一种归纳类型 pc_tree ，它基本上是一个包含一个或多个 pc 的二叉树。 pcts 是包含单个 pc 的叶节点构造函数，而 pctm 是包含多个 pc 的内部节点构造函数。

Inductive pc_tree : Type :=
  | pcts : forall ( n : nat ), pc n -> pc_tree
  | pctm : pc_tree -> pc_tree -> pc_tree.

还有一个归纳定义的命题 contains 。 contains n x t 意味着树 t 包含至少一个 x : pc n 的出现。

Inductive contains ( n : nat ) ( x : pc n ) : pc_tree -> Prop :=
  | contain0 : contains n x ( pcts n x )
  | contain1 : forall ( t s : pc_tree ), contains n x t -> contains n x ( pctm t s )
  | contain2 : forall ( t s : pc_tree ), contains n x t -> contains n x ( pctm s t ).

现在，我需要证明的有问题的引理:

Lemma contains_single_eq : forall ( n : nat ) ( x y : pc n ), contains n x ( pcts n y ) -> x = y.

引理的含义非常简单:如果一棵树的单个叶节点包含 y : pc n 包含一些 x : pc n ，那么它遵循 x = y 。我想我应该能够用 inversion 上的简单 contains 来证明这一点。所以当我写

Lemma contains_single_eq : forall ( n : nat ) ( x y : pc n ), contains n x ( pcts n y ) -> x = y.
intros n x y H. inversion H. 

我期望得到 x = y 作为上下文中的假设。这是我得到的:

1 subgoal
n : nat
x : pc n
y : pc n
H : contains n x (pcts n y)
H1 : existT (fun n : nat => pc n) n x = existT (fun n : nat => pc n) n y
====================================================================== (1/1)
x = y

H1 与我预期的完全不同。 (我以前从未见过 existT。)我关心的是我证明 contains_single_eq ，但我不确定如何使用 H1 ，或者它是否可用。

有什么想法吗？

Answer 1

在对涉及依赖类型的事物进行反演时，这是一个反复出现的问题。在 existT 上生成的相等只是意味着 Coq 不能像普通类型那样反转相等 pcts n x = pcts n y。原因是当输入等式 n 时，出现在 x 和 y 类型上的索引 x = y 不能泛化，这是进行反转所必需的。
existT 是依赖对类型的构造函数，它“隐藏”了 nat 索引并允许 Coq 在一般情况下避免这个问题，生成一个与您想要的稍微相似的语句，尽管不完全相同。幸运的是，对于具有可判定相等性的索引(例如 nat )，实际上可以使用 standard library 中的定理 inj_pair2_eq_dec 恢复“通常”相等性。

Require Import Coq.Logic.Eqdep_dec.
Require Import Coq.Arith.Peano_dec.

Lemma contains_single_eq : 
  forall ( n : nat ) ( x y : pc n ),
    contains n x ( pcts n y ) -> x = y.
  intros n x y H. inversion H.
  apply inj_pair2_eq_dec in H1; trivial.
  apply eq_nat_dec.
Qed.