मैं वर्तमान में लॉजिकल फ़ाउंडेशन बुक के माध्यम से काम कर रहा हूँ और मैं व्यायाम: 4 सितारे, उन्नत (अनुक्रम) (subseq_trans)।

सबसेक के लिए मेरी परिभाषा यहां दी गई है:

Inductive subseq { X : Type } : list X -> list X -> Prop :=
  | s1 : forall l, subseq [] l
  | s2 : forall (x : X) (l l': list X), subseq l l' -> subseq l (x :: l')
  | s3 : forall (x : X) (l l' : list X), subseq l l' -> subseq (x :: l) (x :: l').

और यहाँ subseq_trans के लिए मेरा प्रमाण है:

Theorem subseq_trans : forall (X : Type) (l1 l2 l3 : list X),
   subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3.
Proof.
  intros X l1 l2 l3 H H'.
  generalize dependent H.
  generalize dependent l1.
  induction H'.
  { intros l1 H. inversion H. apply s1. }
  { intros l1 H. apply s2. apply IHH'. apply H. }
  { intros l1 H. apply s2. apply IHH'. apply s2 in H. (* Unable to find an instance for the variable x. *) }

असफल आवेदन से पहले प्रमाण संदर्भ यहां दिया गया है:

1 subgoal
X : Type
x : X
l, l' : list X
H' : subseq l l'
IHH' : forall l1 : list X, subseq l1 l -> subseq l1 l'
l1 : list X
H : subseq l1 (x :: l)
______________________________________(1/1)
subseq l1 l

मैंने इस तरह x को स्पष्ट रूप से तत्काल करने का प्रयास किया है:

apply s2 with (x:=x) in H

लेकिन यह मुझे देता है:

No such bound variable x (possible names are: x0, l0 and l'0).

अग्रिम में धन्यवाद।

coq
1
SDR 11 अक्टूबर 2018, 16:23

2 जवाब

सबसे बढ़िया उत्तर

आपको eapply क्या हो रहा है यह देखने के लिए उपयोगी रणनीति।

...
{ intros l1 H. apply s2. apply IHH'. eapply s2 in H.

subseq l1 (?1 :: x :: l) देता है, जहां आप जो चाहें उसके साथ ?1 को तत्काल कर सकते हैं, लेकिन, जैसा कि आप अब देख सकते हैं, उस धारणा से s2 आगे लागू करना नहीं है सबूत को आगे बढ़ाओ।

एक अन्य संभावना s2 को x पर लागू करना है और फिर धारणा H पर लागू करना है:

apply (s2 x) in H.

मुझे यह भी अजीब लगता है कि apply s2 with (x:=x) काम नहीं करता। ऐसा लगता है कि Coq पर्दे के पीछे कुछ नाम बदल रहा है, शायद सबूत के संदर्भ में x के साथ भ्रम से बचने के लिए। निम्नलिखित अनुक्रम त्रुटि के बिना लागू होता है:

rename x into y. apply s2 with (x:=y) in H.
1
tbrk 12 अक्टूबर 2018, 10:40

जैसा कि @tbrk द्वारा निदान किया गया है, यह Coq द्वारा अधिकतम निहित तर्कों की उपस्थिति में किया गया नामकरण है (देखें यह मुद्दा)। यह subsequence की परिभाषा में {X : Type} की घोषणा के कारण है।

सभी निहित तर्कों को गैर-अंतर्निहित करने के लिए @ का उपयोग करना और इस नामकरण मुद्दे से बचना एक समाधान है। यह देगा:

apply @s2 with (x:=x) in H.
2
eponier 12 अक्टूबर 2018, 11:29