Ltac, How to intro a fresh variable which may already have a good estiblished name given by a universal quantifier?

Question

Context

I am currently self studying Coq following the Software Foundations book series which I am finding very approachable.

I have finally gotten round to understanding how to write match goal clauses properly in ltac. Because of this and playing around with automation in some of the exercises in the book and I am beginning to understand just how powerful and non-brittle one can make ltac proof scripts by combining a few well chosen match goals / bespoke tacticals together with auto.

To this end I have been examining proofs that I have written prior and producing tacticals to abstract away certain strategies in a piecemeal fashion.

One such case amenable to tacticals I have discovered that crops up a-lot is proving inductive proofs of the form:

forall (t1:T1) ... (ti:Ti) ... (tn:Tn), L <-> R

with (L R : Prop). Specifically the cases when going from L -> R involves induction on ti, R -> L inducting on tj and yet both directions may be solved or very much reduced by application of the same tacticals for i ≠ j. In such cases one wants to apply split underneath the quantifier and be left with the two unshelved goals:

1. forall (t1:T1) ... (ti:Ti) ... (tn:Tn), L -> R
2. forall (t1:T1) ... (ti:Ti) ... (tn:Tn), R -> L

I have enough skill to naively develop a recursive tactical which can perform the application of a tactical underneath quantification (and then re-generalize), but I can't seem to refactor it so that it respects any chosen names for universal variables. On the surface that is only slightly annoying, but it quickly becomes counterproductive when I cant then use those variable names later on in the proof (for example to succinctly begin induction by say calling something like [> induction ti | induction tj]). At also makes reading and debugging produced scripts tedious as the auto-genned names are poorly chosen for readability.

Solving this issue with term-renaming is what I am asking for help with.

---

Question

Consider the following ltac tactical tactical_under_uq :

Ltac tactical_under_uq payload :=
             let W := fresh in
             (tryif (intro W) then (tactical_under_uq payload ;generalize dependent W) else (payload)).

tactical_under_uq tackes a tactical payload, and applies it under all of the outer universal quantification of the goal. Because I need to refer to the introduced variable (W in intro W) to re-generalize it later (by generalize dependent W) I need to introduce W explicitly as opposed to just say calling intro without a given variable-name. Thus, to do this in complete generality I need to ensure that the variables it instantiates are always fresh (hence the use of the tactic fresh). I want to modify this tactical to preserve pre-established quantifier names where they exist.

To me, the Coq manual (whilst a great reference) is (at least for things I am not already familiar with) (esp. when it comes to ltac) dense at the best of times and completely impenetrable to me at the worse. Thusly even though I have looked it up I can't figure out properly how to achieve this. What I can gleam though is that I need to somehow capture the identifier v of the variable I desire and pass it through as an argument to fresh.

---

Attempt

the only way I know how to capture identifiers in the goal / hypothesis of a proof state is to use match goal. However, match goal does not seem well equipped to handle forall clauses (as far as I am aware) in the sense that I cant get something like match goal with [|- forall ?x,?y] to run. I have now exhausted all the resources I know about in order to research how to solve this problem and so would appreciate some help from this community.

---

Example

Her is an example of my tactical working, but not respecting established names:

Ltac tactical_under_uq payload :=
             let W := fresh in
             (tryif (intro W) then (tactical_under_uq payload ;generalize dependent W) else (payload)).
Remark myexample : forall (f:Prop) (A:Type) (a:A) , (f=f<->f=f).
Proof.
tactical_under_uq split.
all: auto.
Qed.

Answer 1

Solution

The problem with your attempt is that you miss-understand how to match for a universally quantified goal-case. Instead of writing match goal with [|- forall ?x,?y] you should write match goal with[ |- forall x : ?T, ?P] or match goal with [ |- forall x, ?P] if one does not care about capturing the type of the quantified variable: That is to say one does not put a ? before the variable.

With the goal-matching problem fixed one can directly extract the correct hint to give to fresh to produce the required tactical as follows:

Ltac tactical_under_uq payload :=
              match goal with
                | [ |- forall x : ?T, ?P]
                  =>  let W := fresh x in
                       (intro W;tactical_under_uq payload ;generalize dependent W)
                | _ 
                  => payload
              end.

Note also that being to match in this way makes tactical_under_uq less brittle as the tryif clause is no longer required as we can infer the branch due to the case that we have matched!