Как мне упростить гипотезу вида True -> P в Coq? - PullRequest
Новая
       15

Как мне упростить гипотезу вида True -> P в Coq?

2 голосов
/ 23 марта 2020

Если в моем доказательственном контексте есть гипотеза, которая выглядит как H: True -> P, и я хочу преобразовать ее в H: P, какой самый простой способ сделать это? Я попробовал simpl in H, но ничего не получилось, и единственный способ, который я нашел, - это крайне неудовлетворительный pose proof (H Coq.Init.Logic.I) as H. Есть ли более простой способ?

1 Ответ

3 голосов
/ 23 марта 2020

Есть два способа работы с этим, кроме использования pose proof.

Использование specialize.

Эта тактика позволяет вам приводить аргументы к вашим гипотезам. В вашем случае вы можете сделать 

specialize (H I).

или даже 

specialize H with (1 := I).

, и вы можете использовать as, если хотите создать копию, а не создавать экземпляр H напрямую.

Использование forward.

Я думаю, это то, что вы хотите здесь. forward H. попросит вас доказать первую гипотезу H. Таким образом, вы будете делать что-то вроде этого: 

forward H.
- auto.
- (* Then resume with H : P *)

, но вы также можете предоставить ему (закрытие цели) tacti c: 

forward H by auto.
(* Now you have one goal, and H has type P *)

forward is - as пока - не является частью стандартной библиотеки. Однако его можно определить довольно легко (вот определение из библиотеки MetaCoq). 

Ltac forward_gen H tac :=
  match type of H with
  | ?X -> _ => let H' := fresh in assert (H':X) ; [tac|specialize (H H'); clear H']
  end.

Tactic Notation "forward" constr(H) := forward_gen H ltac:(idtac).
Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.

Обратите внимание, что simpl здесь не работает, потому что на самом деле это не тактика c для Упростите гипотезы в обычном смысле, это действительно просто тактика c, чтобы применить некоторые правила вычислений, в основном она оценивает цель или гипотезу, к которой вы ее применили. True -> P не уменьшается до P, потому что тогда потребуется меньше аргументов.

...