Inversion, Coq

Question

için beklenmeyen bir varoluş ortaya çıkarıyor Burada bir matematiksel teoremde kullandığım bir endüktif tip pc.

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

Ve temel olarak bir veya daha fazla pc ler içeren bir ikili ağaçtır başka endüktif tip pc_tree. pcts, tek bir pc içeren ve pctm birden çok pc s içeren bir iç düğüm kurucusu olan bir yaprak düğümü kurucusudur.

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

Ve indüktif tanımlanan önerme contains. contains n x t, t ağacının x : pc n en az bir oluşumunu içerdiği anlamına gelir. o izler, y : pc n içeren tek yaprak düğümü olan bir ağaç bazı x : pc n içeriyorsa: lemma ne anlama

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

gerçekten basittir:

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). 

Şimdi, sorunlu lemma ben kanıtlamak gerekir x = y. Bunu contains numaralı telefondan basit bir inversion ile kanıtlayabileceğimi düşündüm. Ben

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. 

yazdığımda Yani bağlamında bir hipotez olarak x = y almak için bekliyordum. İşte bunun yerine ne var:

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 beklediğim oldukça farklıdır. (Ben daha önce hiç existT görmedim.) Tek umurumda contains_single_eq olduğunu kanıtlamak, ama bunun için H1 nasıl kullanılacağını veya hiç kullanılıp kullanılamayacağını emin değilim.

Herhangi bir düşünce?

Answer 1

Bu, bağımlı türleri içeren şeyleri tersine çevirirken yinelenen bir sorundur. existT üzerinden üretilen eşitlik, Coq'un normal türlerde olduğu gibi pcts n x = pcts n y eşitliğini tersine çeviremeyeceği anlamına gelir. Bunun nedeni, x ve y türlerinde görünen n dizininin, inversiyon için gereken eşitlik x = y yazarken genelleştirilememesidir.

existT

, her ne kadar tamamen aynı değildir istediğini biraz benzer bir açıklama üreten genel durumda bu sorunu önlemek için Coq "gizler" nat endeks ve izin veren bağımlı çifti türü için yapıcı olduğunu . Neyse ki, eşit bir eşitliğe (örneğin, nat) sahip olan endeksler için, standard library'daki teorem inj_pair2_eq_dec'u kullanarak "olağan" eşitliği kurtarmak mümkündür.

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.