The Coq mailing list

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

Thank you, that works.

For the first one, I realized later that we could I could use: 'Tactic Notation' instead of Ltac, which uses the tactical || .

With regards,
Ashish

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Jasper Hugunin <jasper AT hugunin.net>
Sent: Sunday, September 13, 2020 4:02 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How to avoid code-duplication in this proof?

 

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