Невозможно найти экземпляр для переменной x, даже с явным созданием - PullRequest
Новая
       8

Невозможно найти экземпляр для переменной x, даже с явным созданием

0 голосов
/ 11 октября 2018

В настоящее время я работаю с книгой Logical Foundations и застрял в последней части Упражнение: 4 звезды, продвинутый уровень (подпоследовательность) (subseq_trans).

Вот мое определение для subseq: 

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

Заранее спасибо.

Ответы [ 2 ]

0 голосов
/ 12 октября 2018

Как установлено @tbrk, это переименование, выполненное Coq при наличии максимальных неявных аргументов (см. , эта проблема ).Это связано с объявлением {X : Type} в определении subsequence.

. Одним из решений является использование @, чтобы превратить все неявные аргументы в неявные и избежать этой проблемы переименования.Это даст: 

apply @s2 with (x:=x) in H.
0 голосов
/ 11 октября 2018

Вы можете найти тактику 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.
...