The Coq mailing list

["Kumar, Ashish" <azk640 AT psu.edu>]

Hi,

I am trying to prove a theorem (proof code given below). The issue is there is a lot of repeated code in the proof, which I would like to avoid. Is there a way to do so?


Proof has been summarized below to show only relevant details - In below proof,
(1) Let T1 and T2 denote a sequence of tactics of the form t1 ; t2 ; t3 ... ; tn.
(2) Let S1 be some lemma statement, which has type Prop.
(3) Let L1 be a lemma proved earlier.

Proof.
intros. split; intros H'; inversion_clear H'; T1.
+ assert (H" : S1). { apply L1; assumption. }
    T2 ; apply H''.
+ assert (H" : S1). { apply L1; assumption. }
    T2;  symmetry in H''; apply H''.
Qed.

After the intros, we have a goal of the form (A -> B) /\ (B -> A).
The inversion_clear H' statement generates a total of 4 subgoals from the 2 subgoals generated by split, and T1 solves 2 of these 4 subgoals. 
As you can see the proof code for the remaining 2 subgoals is almost identical (excluding the symmetry tactic). Note that I cannot push the assert statement earlier in the proof, as inversion_clear H' generates a variable st'0 which is used in the assert statements.
I have 2 issues:
(1) Is there a way I can write a customized tactic 'symmetric_apply H' which applies either H or the reversed version of H, and fails if both fail.
(2) Once (1) is done, the proof statement of the remaining 2 subgoals becomes exactly identical (using 'symmetric_apply' instead of apply).
     Then is there a way, I could use the tactical ';' with the assert statement - Coq doesn't seem to be allowing me to do so?

Or if there is some other way of avoiding the code duplication, that would be great.

With regards,
Ashish