Avoid duplicating code for applying tactics in both hypothesis and goal

Question

I find my self (sort of) duplicating code because I want to the same tactics in the goal and in a hypothesis when they match. For example:

match goal with
| H : PATTERN |- _ => simpl in H; rewrite X in H; ... ; other_tactic in H
| |- PATTERN       => simpl     ; rewrite       ; ... ; other_tactic
end.

If the tactics in the match cases becomes long, I essentially duplicate it, with some in clauses added, and this seem very unsatisfactory, in particular if I have many match clauses, so that I duplicate a lot of code.

Sometimes it is not because that I am matching, but simply that I have defined a custom tactic, but depending on the context I would like to apply it either to the goal or to a named hypothesis. For example:

Ltac my_tac      H := simpl in H; rewrite X in H; ... ; other_tactic in H.
Ltac my_tac_goal   := simpl     ; rewrite X     ; ... ; other_tactic.

Then I am again "duplicating" code.

Are there any ways of avoiding this kind of duplication?

At some point I wondered of the goal had a name, say GOAL, like hypothesis, so that simpl in GOAL was equivalent to simpl, but I suspect this is not the case. In that case I could drop the definition of my_tac_goal and then just call my_tac GOAL instead.

Any suggestions on how to avoid this kind of duplication would be appreciated.

PS I had a hard time coming up with a good title, so if somebody thinks of one that fits well, do not hesitate to change it.

Wampler

Answer 1

The "name" of the goal in an in clause is |- *, but somehow I can't find a reference in the manual for this. E.g. the following works:

Goal 2+2=4 -> 2+2=4 -> 2+2=4.
intros H1 H2.
simpl in H1 |- *.

This applies simpl in H1 and the goal, but not in H2.

Alexandria

I see, that seems to work sometimes, however, I cannot get it to work when I define tactics myself :/ Any tips to how this can be done, either with Ltac or Tactic Notation? I managed to find something about |- * in the documentation, namely, under Occurrence clauses. – Wampler

I am using this in tactics. Can you post a minimal example where it does not work? – Alexandria

I have tried something like this: Ltac foo H := simpl in H. Lemma bar: forall n : nat, 0 + n = n. Proof. foo |- *., but I get a syntax error at foo |- *. – Wampler

OK, you can't pass "|- *" as argument to a tactic - that's what I meant with the quotes around "name" above. I don't see an elegant way to solve this in Ltac1. It might be easier in Ltac2, where you have access to the low level machinery without using the notations. – Alexandria

Answer 2

Indeed, the DRY principle is often a useful pattern, including for Coq developments!

Regarding the particular use case you describe, it seems you could benefit from the SSReflect tactical in?

Proof-of-concept:

Require Import ssreflect.

Section SomeTest.

Variables (T : Type) (a b : T).

Hypothesis L : a = b.

Ltac my_tac := simpl; rewrite L.

Lemma test (c : T) (H : let _t := tt in (* dummy let-in to exemplify [simpl] *)
                        (a, c) = (c, b)) :
  let _t := tt in (b, c) = (c, a).

  do [ my_tac ] in H.
  my_tac.

  exact: H.
Qed.

End SomeTest.

Obviously, the do [ … ] in H form won't be applicable for any tactic (e.g., an apply/view. tactic should be manually ported to some move/view. tactic), but nothing prevents you from extending the my_tac tactic (e.g., with some if-then-else…), so that relevant parts are adapted manually (or removed) to address both kinds of contexts.

Mislike