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

Posted 2023-03-29

【中文标题】反转在 Coq 中产生意外的存在

【英文标题】：Inversion produces unexpected existT in Coq

【发布时间】：2014-07-13 06:27:56

【问题描述】：

这是我在数学定理中使用的归纳类型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 是内部节点构造函数，包含多个pcs。

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。我想我应该能够在contains 上用一个简单的inversion 来证明这一点。所以当我写的时候

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，或者它是否可用。

有什么想法吗？

【问题讨论】：

x : T & P x 是一个依赖总和，就像 T * P 是一个非依赖总和。 @existT T P x H : x : T & P x 喜欢 @pair T P x H : T * P。 exists x : T, P x、x : T | P x 和 x : T & P x 非常相似。使用Print ex.、Print sig. 和Print sigT. 命令。

【参考方案1】：

在对涉及依赖类型的事物进行反转时，这是一个反复出现的问题。在existT 上生成的相等性仅仅意味着Coq 不能像普通类型那样反转相等性pcts n x = pcts n y。其原因是，在输入相等 x = y 时，出现在 x 和 y 类型上的索引 n 无法泛化，这是进行反转所必需的。

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.