The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

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

Attachment: signature.asc
Description: OpenPGP digital signature