反演在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,它基本上是一个包含一个或多个pcs 的二叉树.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),它实际上是可以恢复"正常"使用等价定理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.