反演在Coq中产生意外的存在T

这是我在数学定理中使用的归纳型pc。反演在Coq中产生意外的存在T

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。我想我应该可以通过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，或者它是否可用。

有什么想法？

来源

2014-07-13 user287393

'{x：T＆P x}'是一个从属总和，例如'T * P'是一个非相关和。 '@existT T P x H：{x：T＆P x}'比如'@pair T P x H：T * P'。存在x：T，P x'，'{x：T | P x}'和'{x：T＆P x}'非常相似。使用'Print ex.'，'Print sig.'和'Print sigT.'命令。 –

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

existT是依赖对类型，其中“隐藏”了nat指标，并允许勒柯克避免在一般情况下这个问题，产生了声明这是稍微类似于你想要的构造，虽然不太一样。幸运的是，对于具有可判定的相等性的索引（例如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.

来源

2014-07-13 13:55:21

反演在Coq中产生意外的存在T

回答

相关问题