我怎样才能写出一种既适用于目标又适用于假设的战术？

Question

我试图写一种策略，可以在目标和假设上工作，类似于symmetry，但也适用于不等式。现在，有一些关于广义重写的文档，但是这是非常高级的，也许应该是另一个问题。这就是说，这里是我的实现，它为我的用例工作(虽然很尴尬)：

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本身上匹配(因为它将是一个变量)。

对于内置对称策略是否有什么特别之处，允许它与in关键字一起使用，还是我只需要以特定的方式编写Ltac才能在其中使用？

战术的in变体可以定义为Tactic Notation (也就是说，它实际上是一个独立于原始策略的东西)。

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