The Coq mailing list

[Jasper Hugunin <jasper AT hugunin.net>]

Hi Ashish,

I'm not an expert on Ltac programming, so hopefully someone else will chime in here, but here is how I would solve your two issues.

(1) The first tactic lets you define `Ltac symmetric_apply H := first [ apply H | symmetry in H; apply H ].` which I believe has exactly the behavior you describe. You can also replace first with solve if you want to require that `symmetric_apply H''` finishes the proof.

(2) Consider using the form `assert (H'' : S1) by (apply L1; assumption);` This avoids the use of `{` which is causing you trouble when chaining with `;`.

Sincerely,

- Jasper Hugunin

On Sun, Sep 13, 2020 at 8:10 AM Kumar, Ashish <azk640 AT psu.edu> wrote:

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