Как написать 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с писать

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,