The Coq mailing list

[Colm Bhandal <bhandalc AT tcd.ie>]

Apologies! The middle example is wrong. Should have been:


[H : _ |- P], eassert as Q ->
[H : _ |- P; H : _ |- ?], inversion H->
[H : _ |- P; H1 : T |- ?; H2 : T' |- ?], some tactic that converts H2 type to H1 type->
[H : _ |- P; H1 : T |- ?; H2 : T |- ?], exact H2 -> //this now binds the goal of eassert to T
[H : _ |- P; H1 : T |-  T], exact H1
[H, Q : T |- P], clear H //just to be thorough
[Q : T |- P] //and we end up with only one occurrence of the goal

On 15 November 2014 14:41, Colm Bhandal <bhandalc AT tcd.ie> wrote:

Thanks for the responses guys. I think I should probably have provided a bit of context in the original question to demonstrate the need for such a specialised tactic. Say I want to write a general tactic for splitting a hypothesis H into H1 and H2 (by inversion) and then converting H2 to H1 (by some other tactic). Then I get the annoying duplication of the goal with H1 as hypothesis e.g.

[H : _ |- P], inversion H->
[H1 : _ |- P; H2 : _ |- P], some tactic that converts H2 to H1->

[H1 : _ |- P; H1 : _ |- P]

I agree with Cedric that a forward proof is generally nicer in this context, but because this is a general tactic rather than a specific proof we don't know exactly what H1 is. A solution would be a tactic eassert, allowing you to assert something whose type you don't know yet, and then instantiate it and add it to the hypotheses. In the above example it could be used as follows:

[H : _ |- P], eassert as Q ->
[H : _ |- P; H : _ |- ?], inversion H->
[H : _ |- P; H1 : _ |- ?; H2 : _ |- ?], some tactic that converts H2 to H1->
[H : _ |- P; H1 : _ |- ?; H1 : _ |- ?], exact H1 -> //this now binds the goal of eassert to H1
[H : _ |- P; H1 : _ |- H1], exact H1
[H, H1 : _ |- P], clear H //just to be thorough
[H1 : _ |- P] //and we end up with only one occurrence of the goal

Maybe eassert (or an equivalent tactic) already exists? I just haven't found any tactic like this!

@Pierre yes I think that tactic would be interesting. Maybe even it would be possible to develop a general tactic to merge any two subgoals? This would be different to Pierre's suggestion of wlog, but wlog could probably be used to implement such a tactic:

Say we have: [ g1 : Γ1 ⊢ A1 ; gi : Γi ⊢ Ai... gk : Γk ⊢ Ak... ]

Then we could say [merge i k] to give: [ g1 : Γ1 ⊢ A1 ; gik : Γi U Γk ⊢ Ai /\ Ak ...] and gik is then the nice easy trivial case of conjunction first proposed by Jonathan. Note that by Γi U Γk is some sort of union (unification?) of the hypotheses of goals i and k. This could be simply the concatenation of the two hypotheses lists but then there might be duplication...

Hopefully some of that was clear! Thanks again for the responses.

On 15 November 2014 12:47, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 15/11/2014 10:06, Enrico Tassi wrote:
> In trunk goals can be named.  I did not test that, but I guess you can:
>
>   refine ?[theothergoal]. (* or maybe even exact *)
>
> to merge the ongoing goal with another one named "theothergoal".

Yep, I even proposed a generalized version of this some time ago, under
the form of a [wlog] tactic. If you have some goals

[ g1 : Γ1 ⊢ A1 ; ... ; gn : Γn ⊢ An ]

then [wlog gi] results in the state

[ g1 : (forall Γi : Ai), Γ1 ⊢ A1 ; ... ; gn : Γn ⊢ An ]

with some occur check to prevent loops.

This would allow to do a lot of proof by symmetry in a very simple way.
This is very easy to implement, but at the penultimate Coq WG, nobody
seemed really interested so I just forgot about it. But if people here
on Coq-club are interested, I can write it out.

PMP