Как превратить одну переменную объединения в цель, во время доказательства - PullRequest
Новая
       6

Как превратить одну переменную объединения в цель, во время доказательства

0 голосов
/ 30 ноября 2018

Я хочу построить экзистенциальную переменную в интерактивном режиме.Я не могу использовать Захватить экзистенциальные переменные , потому что мне нужно заполнить экзистенциальные, прежде чем я достигну цели.

Минимальный пример Вот минимальный пример (поскольку он прост, у него есть другие решения, но он иллюстрирует мой вопрос) 

Context (A:Type).
Parameter P Q: A -> Prop.
Definition filter: forall {a}, P a -> A:= fun a Pa=> a.
Lemma my_lemma:
  forall a b, Q b -> (Q b -> P a) ->
         exists a (H: P a), P (filter H).
  Proof.
  intros ?? H H0.
  do 2 eexists.

На данный момент естьдва решения, которые не отвечают на мои вопросы: (1) я могу запустить (eauto), а затем выполнить Grab Existential Variables, но предположим, что eauto не будет успешным, пока я не создам экземпляр переменной объединения;(2) Я мог бы просто явно передать термин доказательства с помощью instantiate(1:= H0 H) (или даже instantiate(1:= ltac:(eauto))), но предположить, что доказательство xistential было утомительным, и мы хотели сделать это в интерактивном режиме.

Что еще можетмы делаем?Мы можем попытаться использовать cut или assert, например, так: 

match goal with
      |[|- P (filter ?x)] =>
       match type of x with
       | ?T => assert (HH:T) by eauto
       end
      end.

Но HH не находится в контексте переменной объединения, поэтому его нельзя создать. 

  instantiate(1:=HH). (* Instance is not well-typed in the environment of ?H. *)

Насколько я могу судить, единственный способ решить эту проблему - использовать Show Existentials, посмотреть тип переменной, скопировать ее вручную, откатить доказательство до того, как объединение было введено, и построить переменную там.,В примере это выглядит так: 

Lemma my_lemma:
  forall a b, Q b -> (Q b -> P a) ->
         exists a (H: P a), P (filter H).
Proof.
  intros ?? H H0.
  do 2 eexists.
  Show Existentials.  
  Restart. (* This command restores the proof editing process to the original goal. *)
  intros ?? H H0.
  assert (HH:P a) by eauto.
  eexists; exists HH.
  auto.
Qed.

Очевидно, я бы хотел избежать этого рабочего процесса.Итак, в любом случае, чтобы превратить экзистенциальные переменные в подцели?

1 Ответ

0 голосов
/ 30 ноября 2018

Лучше всего вам, вероятно, избегать создания экзистенциальной переменной в качестве эвара.Вам не нужно создавать переменную вручную, чтобы сделать это;если вы можете определить, где он был создан, вы можете обернуть оскорбительную тактику с помощью unshelve t, которая превращает все уши, созданные с помощью t, в цели.Это может быть затруднено, если соответствующая тактика глубоко заложена в некоторой автоматизации и ее трудно идентифицировать или изменить.

...