0

考虑以下发展， Adam Chlipala 的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可能修改目标或添加无关假设的可能性吗？

4

1 回答 1

1

我不认为你可以修改G，但你可以制定一个假设，从中injection产生多个相等。

我们定义injectionInCtx2which 与 相同，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.
于 2018-10-17T12:36:41.270 回答