उलटा कोक

Question

में अप्रत्याशित अस्तित्व का उत्पादन करता है यहां एक अपरिवर्तनीय प्रकार pc है जिसे मैं गणितीय प्रमेय में उपयोग कर रहा हूं।

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 में कम से कम एक ocurrence x : pc n है।

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

क्या लेम्मा का मतलब है वास्तव में सरल है::

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

अब, समस्याग्रस्त लेम्मा मैं साबित करने के लिए की जरूरत है एक पेड़ y : pc n वाली एकल पत्ती नोड है कि कुछ x : pc n होता है, यह इस प्रकार है कि x = y। मैंने सोचा कि मुझे inversioncontains पर इसे सरल साबित करने में सक्षम होना चाहिए। तो जब मैं

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 को सामान्य प्रकारों के समान नहीं कर सकता है। इसका कारण यह है कि सूचकांक nx और y के प्रकारों पर दिखाई देने वाले समानता कोटाइप करते समय सामान्यीकृत नहीं किया जा सकता है, जो इनवर्जन करने के लिए आवश्यक है।

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.