Может ли тактика инъекций изменить конечную цель или добавить посторонние предположения?

Question

Рассмотрим следующую разработку, изолированную часть Адама ЧлипалыsimplHyp:

(** Fail if H is in context *)
Ltac notInCtx H := assert H; [ assumption | fail 1 ] || idtac.

Ltac injectionInCtx :=
  match goal with
  (* Is matching on G strictly necessary? *)
  | [ H : ?F ?X = ?F ?Y |- ?G ] =>
    (* fail early if it wouldn't progress *)
    notInCtx (X = Y); 
    injection H;
    match goal with
      (* G is used here *)
      | [ |- X = Y -> G ] =>
        try clear H; intros; try subst
    end
  end.

Goal forall (x y : nat), S x = S y -> x = y.
  intros x y H.
  injectionInCtx.
  exact eq_refl.
Qed.

Смотрите комментарии в строке - G сопоставляется с самого начала и в конечном итоге используется для проверки того, что конечная цель остается прежней. Это исключает возможность того, что injection H может изменить цель или добавить посторонние предположения?

Answer 1

Я не думаю, что вы можете изменить G, но вы можете создать гипотезу, из которой injection будет генерировать более одного равенства.

Мы определяем injectionInCtx2 который идентичен injectionInCtx кроме того, что он не использует G,

Ltac injectionInCtx2 :=
  match goal with
  | [ H : ?F ?X = ?F ?Y |- _ ] =>
    (* fail early if it wouldn't progress *)
    notInCtx (X = Y);
    injection H;
    match goal with
    | [ |- X = Y -> _ ] =>
      try clear H; intros; try subst
    end
  end.

Definition make_pair {A} (n:A) := (n, n).

Goal forall (x y : nat), make_pair x = make_pair y -> x = y.
Proof.
  intros x y H.
  (* [injection H] gives [x = y -> x = y -> x = y] *)
  Fail injectionInCtx.
  injectionInCtx2.
  reflexivity.
Qed.