Замените гипотезу импликацией, не добавляя ее предпосылку в качестве подцели - PullRequest
Новая
       8

Замените гипотезу импликацией, не добавляя ее предпосылку в качестве подцели

0 голосов
/ 29 сентября 2019

Это часть автоматизации, которую я пытаюсь построить для работы с Is_true. У меня есть это Lemma Is_true_implb_impl : (Is_true x -> Is_true y) <-> Is_true (implb x y)., и у меня есть гипотеза H в форме Is_true (implb ?x ?y), которую я сопоставляю, используя Ltac elim_Is_true := match goal with .... Когда я применяю Is_true_implb_impl x y в H (если я не создаю экземпляр с x и y, он не соответствует), тогда гипотеза изменяется на Is_true y, и я получаю Is_true x как новую подцель. (Я попытался обойти это, написав тактику, которая утверждает Is_true x -> Is_true y, но это также не удается, потому что я не мог понять, как доказать утверждение, используя assumption после того, как утверждение не работает). Есть ли способ, которым я могу изменить H на Is_true x -> Is_true y? Другая проблема, связанная с выполнением этого в цикле с другими исключениями Is_true, заключается в том, что новая подцель формы Is_true _ соответствует match goal with, но тактика не может применять к ней какие-либо правила.

Пример фрагментадемонстрируя то, что я пытаюсь сделать: 

From Coq Require Export Init.Datatypes.
From Coq Require Export Bool.Bool.

Lemma Is_true_implb_impl x y :
  (Is_true x -> Is_true y) <-> Is_true (implb x y).
Proof.
  destruct x; simpl; split; intros H.
  - apply H. apply I.
  - intros H'. assumption.
  - apply I.
  - intros H'. exfalso. assumption.
Qed.

Ltac elim_Is_true :=
  match goal with
  (* FAILS: *)
  (* | [H : Is_true (implb ?x ?y) |- _] => apply Is_true_implb_impl in H *)
  | [H : Is_true (implb ?x ?y) |- _] => apply (Is_true_implb_impl x y) in H
  | _ => idtac
  end.

Example test x y :
  Is_true x -> Is_true (implb x y) -> Is_true y.
Proof.
  intros H1 H2. elim_Is_true.
  (* In this case this is useful but in other cases I do not yet want to add
     the premise as a subgoal *)
Abort.

1 Ответ

1 голос
/ 30 сентября 2019

apply не то, что вы хотите. Цитирование из документации ,

Применяемая тактика пытается сопоставить текущую цель с выводом типа термина. Если это удастся, то эта тактика возвращает столько подцелей, сколько и числа независимых объектов типа термина.

Применить создаст подцели для каждого (независимого) аргумента, который в вашемКейс включает в себя Is_true x (в дополнение к цели, которая у вас уже есть: Is_true y).

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


Ltac elim_Is_true :=
  match goal with
  | H : Is_true (implb ?x ?y) |- _ =>
          (* Generate a new name for a temporary hypothesis *)
          let H' := fresh in
          (* rename the old hypothesis to this new name *)
          rename H into H';
          (* replace the goal with (Is_true x -> Is_true y) -> ?Goal *)
          generalize (proj2 (Is_true_implb_impl x y) H');
          (* intro (Is_true x -> Is_true y) with the old name *)
          intro H;
          (* Get rid of the old hypothesis *)
          clear H'
  | _ => idtac
  end.

Мы используем proj2 (Is_true_implb_impl x y) H', потому что мы хотим <- часть тогда и только тогда, когда.

Это можно абстрагировать с помощью тактики, подобнойэто: 

Tactic Notation "ng_apply" constr(X) "in" constr(H) :=
  let H' := fresh in
  rename H into H';
  generalize (X H'); intro H;
  clear H'.

Теперь elim_Is_true можно переписать как 

Ltac elim_Is_true :=
  lazymatch goal with
  | H : Is_true (implb ?x ?y) |- _ =>
          ng_apply (proj2 (Is_true_implb_impl x y)) in H
  end.

(«ng» в ng_apply означает отсутствие дополнительных целей)

Вы можете эмулировать некоторые действия apply, используя более сложные ltacs. Например, эта версия дублирует поведение apply с типами кортежей (например, <->). Это означает, что мы можем упростить до ng_apply (Is_true_implb_impl x y) in H. 

Ltac ng_apply X H :=
  first [
    let X' := fresh in let Y := fresh in let Z := fresh in
    set (X' := X);
    destruct X' as [Y Z] in X';
    first [ng_apply Y H | ng_apply Z H];
    clear Y; clear Z
  | let H' := fresh in
    rename H into H';
    generalize (X H');
    intro H;
    clear H'
  ].

Возможно, можно ng_apply предоставить некоторые аргументы, но я не смог заставить его работать с деструктуризацией кортежей.

...