As minimal example for my general question, suppose we have the following:
Parameter C: Prop.
Definition blah := C.
I would like to implement a tactic that automatically unfolds blah in all hypotheses of the goal.
I tried this:
Ltac my_auto_unfold := repeat match goal with
| [ H: ?P |- ?P ] => unfold blah in H
end.
Theorem g: blah -> blah -> blah.
Proof.
intros.
my_auto_unfold.
But only one hypothesis had blah unfolded.
I think you may be looking for the progress tactical. If you do this:
Ltac my_auto_unfold := repeat match goal with
| [ H: ?P |- ?P ] => progress unfold blah in H
end.
then it will unfold blah in both hypotheses. You can even do:
Ltac in_all_hyps tac :=
repeat match goal with
| [ H : _ |- _ ] => progress tac H
end.
to generalize this pattern. Note that this may run the tactic in each hypothesis multiple times.
If you want to run over all the hypotheses once, in order, this is significantly harder (especially if you want to preserve evar contexts and not add dumb stuff to the proof term). Here is the quick-and-dirty way to do that (assuming your tactic doesn't mess with the goal):
Parameter C: Prop.
Definition blah := C.
Definition BLOCK := True.
Ltac repeat_until_block tac :=
lazymatch goal with
| [ |- BLOCK -> _ ] => intros _
| [ |- _ ] => tac (); repeat_until_block tac
end.
Ltac on_each_hyp_once tac :=
generalize (I : BLOCK);
repeat match goal with
| [ H : _ |- _ ] => revert H
end;
repeat_until_block
ltac:(fun _
=> intro;
lazymatch goal with
| [ H : _ |- _ ] => tac H
end).
Theorem g: blah -> blah -> fst (id blah, True).
Proof.
intros.
on_each_hyp_once ltac:(fun H => unfold blah in H).
The idea is that you insert a dummy identifier to mark where you are in the goal (i.e., to mark how many variables can be introduced), and then you revert all of the context into the goal, so that you can reintroduce the context one hypothesis at a time, running the tactic on each hypothesis you just introduced.
The problem with your snippet is that [ H: ?P |- ?P ] will always match in this case. The first time it will match H : blah, and the second time it will match H : C -- as C and blah are convertible in Coq -- and the unfold will not change anything, thus aborting the repeat.
I would write
Ltac my_auto_unfold nam := repeat lazymatch goal with
| [ H : nam |- _ ] => unfold nam in H
end.
Theorem g: blah -> blah -> blah.
Proof.
intros.
my_auto_unfold blah. auto. Qed.
You can even write
Theorem g: blah -> blah -> blah.
Proof.
intros.
match goal with
| [ |- ?p] => my_auto_unfold p
end.
auto. Qed.
if you prefer so.
