Блог

Главная - Вопросы по программированию - Возьмите соединение двух гипотез и создайте новую гипотезу в Coq

Возьмите соединение двух гипотез и создайте новую гипотезу в Coq

#coq #coq-tactic

#coq #coq-тактика

Вопрос:

Мне интересно, как destruct H as (H1 amp; H2). гипотеза H : p / q создает две гипотезы H1 : p и H2 : q , если есть какая-либо тактика, которая работает наоборот. То есть возьмите две гипотезы и создайте одну с их соединением.

Ответ №1:

Вот две возможности, использующие assert тактику:

 Goal forall A B : Prop, A -> B -> A / B.
Proof.
intros A B HA HB.
assert (H1 : A / B). { now split. }
assert (H2 := conj HA HB).
Abort.

Комментарии:

1. Спасибо, @Артур Азеведо Де Аморим

2. Я надеюсь, вы не возражаете, если я добавлю сюда еще один вопрос. Возможно ли создать экземпляр переменной, которую я ввел в свой контекст, используя exists для определенного значения? Я знаю, что для экзистенциальных переменных, имена которых начинаются с ? , вы можете использовать instantiate tactic, но я не знаю, как это сделать в случае, о котором я упоминал.

3. @DanJohnson Я с радостью постараюсь ответить на это, когда у меня будет возможность, но пока вам, вероятно, лучше задать отдельный вопрос. Кто-то другой может прийти первым и ответить вам! 😉