Coq использовать уточнение с двойным подтекстом - PullRequest
Новая
       68

Coq использовать уточнение с двойным подтекстом

0 голосов
/ 04 марта 2020

Я не знаю, как сформулировать свой вопрос, потому что я новичок в coq. Я хочу использовать уточнение с теоремой, которая включает би-импликацию. Пример кода: 

Parameters A B C : Prop.

Theorem t1:
  A -> B -> C.
Admitted.

Theorem t2:
  A -> B <-> C.
Admitted.

Theorem test1:
  A -> B -> C.
Proof.
  intros.
  refine (t1 _ _).
  assumption.
  assumption.
Qed.

Theorem test2:
  A -> B -> C.
Proof.
  intros A B.
  refine (t2 _ _).

t1 и t2 - теоремы, которые я хочу использовать в уточнении. t1 работает так, как я ожидаю (показано в test1). Но у меня проблема с т2. Я получаю сообщение об ошибке: 

Ltac call to "refine (uconstr)" failed.
Error: Illegal application (Non-functional construction): 
The expression "t2 ?a" of type "Top.B <-> C"
cannot be applied to the term
 "?y" : "?T"
Not in proof mode.

Я пробовал что-то вроде этого: 

Theorem test3:
  A -> B -> C.
Proof.
  intros.
  cut (B <-> C).
  firstorder.
  refine (t2 _).
  assumption.
Qed.

Но с более длинными доказательствами и доказательствами это становится немного грязным. (Также я должен доказать двойное значение сам). Могу ли я использовать t2 и получить его подзадачи более простым способом?

Спасибо

1 Ответ

1 голос
/ 05 марта 2020

A <-> B определяется как (A -> B) /\ (B -> A), поэтому вы можете проецировать с proj1, proj2: 

Theorem test2:
  A -> B -> C.
Proof.
  intros A B.
  refine (proj1 (t2 _) _).
...