Создание экзистенциального с конкретным доказательством
В настоящее время я пытаюсь написать тактику, которая создает экземпляр экзистенциального квантификатора, используя термин, который может быть сгенерирован легко (в этом конкретном примере, из 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
надеется).
Я не уверен, что это все, что полезно (обычно тип свидетеля не очень информативен, и вы хотите использовать остальную часть цели, чтобы выбрать его), но это здорово, что вы можете сделать это, тем не менее.