反演在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

回答

相關問題