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

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

0 голосов
/ 14 октября 2018

Рассмотрим следующую разработку, изолированную часть Адама Чипалы 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 может изменить цель или добавить посторонние предположения?

1 Ответ

0 голосов
/ 17 октября 2018

Я не думаю, что вы можете изменить 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.
...