我怎样才能写出既适用于目标又适用于假设的策略？

Question

我正在尝试编写一种策略，它可以对类似于 symmetry 的目标和假设起作用，但也适用于不等式。现在，有一些关于通用重写的 documentation，但这是非常先进的，也许应该是一个不同的问题。也就是说，这是我的实现，它适用于我的用例（尽管很笨拙）：

Require Import Coq.PArith.BinPos.

Ltac symmetry' :=
  lazymatch goal with
  | [ |- ?x <> ?y ] => unfold not; intros NQ; symmetry in NQ; revert NQ
  | [ |- _ ] => symmetry
  end.

Lemma succ_discr' : forall p : positive,
  Pos.succ p <> p.
Proof.
  intros p.
  symmetry'.
  apply Pos.succ_discr.
Qed.

这很好，但是如果我们希望应用 symmetry' 的假设不等式怎么办？


Lemma succ_discr' : forall p : positive,
  Pos.succ p <> p -> (2 * p <> Pos.succ (2 * p))%positive.
Proof.
  intros p H.
  Fail symmetry' in H.
  (* Fails with Error:
Syntax error: [tactic:ltac_use_default] expected after [tactic:tactic] (in [vernac:tactic_command]). *)

我试着写

Ltac symmetry'' H :=
  lazymatch H with
   | ?x <> ?y => unfold not; intros NQ; symmetry in NQ; revert NQ
   | _ => symmetry
   end.

然后通过 symmetry'' H 申请，但因另一个错误而失败，

Error:
Tactic failure:  The relation (fun x y : positive => x <> y) is not a
declared symmetric relation. Maybe you need to require the
Coq.Classes.RelationClasses library.

所以，我的问题是，内置的 symmetry 策略是否有一些特殊之处，允许它与 in 关键字一起使用，或者我只需要将我的 Ltac 写在能够使用 in?

的特定方式

Answer 1

Ltac symmetry' :=
  lazymatch goal with
  | [ |- ?x <> ?y ] => apply not_eq_sym
  | [ |- _ ] => symmetry
  end.

Ltac symmetry'' H :=
  lazymatch type of H with
   | ?x <> ?y => apply not_eq_sym in H
   | _ => symmetry in H
   end.

请注意，您需要匹配 type of H，而不是 H 本身（因为它将成为一个变量）。

is there something special about the builtin symmetry tactic which allows it to be used with the in keyword, or do I just need to write my Ltac in a particular way to be able to use in?

策略的 in 变体可以定义为 Tactic Notation（即，它实际上与原始策略不同）。

Tactic Notation "symmetry'" "in" ident(H) := symmetry'' H.
(* symmetry' in H *)

我怎样才能写出既适用于目标又适用于假设的策略？

How can I write a tactic which works both in a goal and a hypothesis?

coq

coq-tactic