代码之家 › 专栏 › 技术社区 › Carl Patenaude Poulin

注入策略是否可以修改最终目标,或添加无关的假设?

ltac coq

0

Carl Patenaude Poulin · 技术社区 · 8 年前

考虑以下开发,这是 Adam Chlipala's 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 回复 | 直到 8 年前

1

eponier 8 年前

我认为你不能修改 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.