I would like to have an Ltac tactic which does the work of Disjunction Commutavity. Mainly, if I have a subterm P \/ Q somewhere in a hypothesis H, Ltac Com H will add Q \/ Pas another hypothesis to the context.
I have tried supplying the commutavity rule via an axiom and applyit; but it only works for the simple hypotheses, for example fails in R -> (P \/ Q); where it should add to the context R -> (Q \/ P).
You can use the setoid rewrite library, which allows you to rewrite with relations other than equality. The following snippet shows how to replace A \/ B with B \/ A in a hypothesis:
Require Import Setoid.
Variables A B C : Prop.
Goal ~ (A \/ B -> C).
intros H.
rewrite or_comm in H.
Abort.
To implement the tactic you want, we just have to duplicate the hypothesis and rewrite in it. Note the use of the fresh tactic, which generates a new hypothesis name.
Ltac Comm H :=
let H' := fresh "H" in
pose proof H as H';
rewrite or_comm in H'.
Here's a demo of Comm in action.
Goal ~ (A \/ B -> C).
intros H.
Comm H.
Abort.
Edit The Coq manual has a section on setoid rewriting. Roughly, you can rewrite with any relation R in a hypothesis, provided that you prove that the operations that appear in that hypothesis are compatible with the relation. For instance, if we take R to be <->, the above rewriting works because there are lemmas in the standard library showing that logical equivalence is respected by implication.
Note I would generally advise against letting Coq name hypotheses by itself: these names tend to be quite unstable, which often causes proof scripts to break. As a rule of thumb, you should let Coq choose names by itself if you are writing fully automated proof scripts, which never refer to automatically chosen names. Here's another version of Comm that avoids this issue.
Ltac Comm' H H' :=
pose proof H as H';
rewrite or_comm in H'.
Goal ~ (A \/ B -> C).
intros H.
Comm H H'.
Abort.