The Coq mailing list

[Colm Bhandal <bhandalc AT tcd.ie>]

Cool! Hand't come across the evar tactic before. V. powerful. Here's a working & tested version of eassert slightly edited from the above. It just cleans up some definitional equalities from the context. The argument Y could be left out if the name of the assertion is unimportant. This solves my problem. Thanks!

(**Adds a hypothesis Y to the context and generates a subgoal of unspecified type such that instantiation of the sub-goal solves it and sets the type of Y in the original proof context.*)
Ltac eassert Y := let T := fresh in evar (T:Type);
  assert T as Y;[unfold T; clear T | unfold T in Y; clear T].

On 15 November 2014 17:43, Jonathan <jonikelee AT gmail.com> wrote:

On 11/15/2014 09:45 AM, Colm Bhandal wrote:

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

There is a way to do your eassert.

In the trunk, eassert would be:

Ltac eassert var := refine (let var := _ in _); [shelve|..].

In 8.4, this should work (untested as I only have a working trunk version):

Ltac eassert var := let T:=fresh in evar(T:Type); evar(var:T); subst T; assert var; [subst var|].

-- Jonathan

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.