如何编写 Ltac 以将方程的两侧乘以 Coq 中的组元素

Question

使用组的以下定义：

Structure group :=
  {
    G :> Set;
    id : G;
    op : G -> G -> G;
    inv : G -> G;
    op_assoc_def : forall (x y z : G), op x (op y z) = op (op x y) z;
    op_inv_l : forall (x : G), id = op (inv x) x;
    op_id_l : forall (x : G), x = op id x
  }.
(** Set implicit arguments *)
Arguments id {g}.
Arguments op {g} _ _.
Arguments inv {g} _.
Notation "x # y" := (op x y) (at level 50, left associativity).

并证明了这个定理：

Theorem mult_both_sides (G : group) : forall (a b c : G),
    a = b <-> c # a = c # b.

我如何编写一个 Ltac 来自动将给定的相等式(目标本身或假设(乘以给定项的过程？

理想情况下，在证明中使用此 Ltac 如下所示：

left_mult (arbitrary expression).
left_mult (arbitrary expression) in (hypothesis).

Answer 1

基于larsr给出的答案，你可以用Tactic Notation s来写

Tactic Notation "left_mult" uconstr(arbitrary_expression) :=
  apply (mult_both_sides _ _ _ arbitrary_expression).
Tactic Notation "left_mult" uconstr(arbitrary_expression) "in" hyp(hypothesis) :=
  apply (mult_both_sides _ _ _ arbitrary_expression) in hypothesis.

使用uconstr表示"延迟此术语的类型检查，直到我们将其插入apply"。 (其他选项包括constr("在呼叫站点进行类型检查"(和open_constr("在呼叫站点进行类型检查并用 evars 填充孔"(。

Answer 2

你真的需要特定的策略吗？如果你只是用apply来解决这个问题

Goal forall (G:group) (a b c: G), a = b.
  intros.
  apply (mult_both_sides _ _ _ c).

现在你的目标是

  G0 : group
  a, b, c : G0
  ============================
  c # a = c # b

如果你想修改一个假设H，那么就apply ... in H