Есть ли что-то вроде apply lem в *? - PullRequest
Новая
       5

Есть ли что-то вроде apply lem в *?

0 голосов
/ 18 февраля 2019

Есть ли способ позвонить apply lem in H для каждого возможного H в помещении, как rewrite lem in *? 

Axiom P Q : nat -> Prop.
Axiom lem : forall (n : nat), P n -> Q n.
Goal P O -> P (S O) -> True.
  intros. apply lem in H. apply lem in H0.

1 Ответ

0 голосов
/ 18 февраля 2019

Я не смог найти ничего встроенного, но такую ​​тактику можно написать с помощью Ltac.

Во-первых, особый случай. 

Axiom P Q : nat -> Prop.
Axiom lem : forall (n : nat), P n -> Q n.
Goal P O -> P (S O) -> True.
  intros.
  repeat match goal with
    x : _ |- _ => apply lem in x
  end.
Abort.

Теперь мы можем обобщить это 

Ltac apply_in_premises t :=
  repeat match goal with
    x : _ |- _ => apply t in x
  end.

и используйте его так: 

Goal P O -> P (S O) -> True.
  intros.
  apply_in_premises lem.
Abort.

К сожалению, такой способ может вызвать бесконечный цикл, если применение lem приводит к чему-то еще, что lem может быть примененок. 

Axiom P : nat -> Prop.
Axiom lem : forall (n : nat), P n -> P (S n).
Ltac apply_in_premises t :=
  repeat match goal with
    x : _ |- _ => apply t in x
  end.

Goal P O -> P (S O) -> nat -> True.
  intros.
  apply_in_premises lem. (* infinite loop *)
Abort.

Если это вас беспокоит, вы можете использовать вариант, предложенный Ивом в комментариях.Простое изменение apply t in x на apply t in x; revert x гарантирует, что эта гипотеза больше не будет соответствовать.Однако конечный результат будет содержать все гипотезы в цели, например P -> G, вместо p: P в качестве предпосылки и G в качестве цели.

Для автоматического повторного intro вывода этих гипотезмы можем отследить, сколько раз гипотеза была отменена, а затем представить их снова. 

Ltac intro_n n :=
  match n with
  | 0 => idtac
  | S ?n' => intro; intro_n n'
  end.

Ltac apply_in_premises_n t n :=
  match goal with
  | x : _ |- _ => apply t in x; revert x;
                  apply_in_premises_n t (S n)
  | _ => intro_n n (* now intro all the premises that were reverted *)
  end.

Tactic Notation "apply_in_premises" uconstr(t) := apply_in_premises_n t 0.

Axiom P : nat -> Prop.
Axiom lem : forall (n : nat), P n -> P (S n).

Goal P O -> P (S O) -> nat -> True.
  intros.
  apply_in_premises lem. (* only applies `lem` once in each of the premises *)
Abort.

Здесь тактика intro_n n применяется intro n раз.

Я не проверял это в целом, но это работает хорошо в случае выше.Он может потерпеть неудачу, если гипотеза не может быть отменена (например, если от нее зависит какая-то другая гипотеза).Это также может изменить порядок гипотез, поскольку, когда возвращенная гипотеза вновь вводится, она помещается в конец списка гипотез.

...