Создание экзистенциального с конкретным доказательством

В настоящее время я пытаюсь написать тактику, которая создает экземпляр экзистенциального квантификатора, используя термин, который может быть сгенерирован легко (в этом конкретном примере, из tauto). Моя первая попытка:

Ltac mytac :=
  match goal with
  | |- (exists (_ : ?X), _) => cut X; 
                             [ let t := fresh "t" in intro t ; exists t; firstorder 
                               | tauto ]
  end.

Эта тактика будет работать над такой простой проблемой, как

Lemma obv1(X : Set) : exists f : X -> X, f = f.
  mytac.
Qed.

Однако это не будет работать на цель, как

Lemma obv2(X : Set) : exists f : X -> X, forall x, f x = x.
  mytac. (* goal becomes t x = x for arbitrary t,x *)

Здесь я хотел бы использовать эту тактику, полагая, что f который tauto находки будут просто fun x => x, таким образом, подпункт в конкретном доказательстве (которое должно быть тождественной функцией), а не только в общем t из моего текущего сценария. Как я могу написать такую ​​тактику?

2 ответа

Решение

Ты можешь использовать eexists ввести экзистенциальную переменную, и пусть tauto инстанцирует это.

Это дает следующий простой код.

Lemma obv2(X : Set) : exists f : X -> X, forall x, f x = x.
  eexists; tauto.
Qed.

Гораздо чаще встречается создание экзистенциальной переменной и использование некоторой тактики (eauto или же tauto например) создать экземпляр переменной путем объединения.

С другой стороны, вы также можете буквально использовать тактику, чтобы обеспечить свидетеля с помощью тактики в терминах:

Ltac mytac :=
  match goal with
  | [ |- exists (_:?T), _ ] =>
    exists (ltac:(tauto) : T)
  end.

Lemma obv1(X : Set) : exists f : X -> X, f = f.
Proof.
  mytac.
  auto.
Qed.

Вам нужен тип надписи : T так что тактика в перспективе ltac:(tauto) имеет правильную цель (типа exists надеется).

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

Другие вопросы по тегам