The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi all,

Marko, I did not know about this library. I've added it to the list at https://github.com/coq/stdlib2/wiki/Other-%22standard%22-libraries. If someone could complete the new bullet point with some more info about it, that would be nice.

Li-yao, your solution

match type of H with
| ?A -> _ =>
   assert (I : A); [| apply H in I ]
end.

can be written (equivalently I think) as:

eassert _ as I%H.

For some reason, this also works (since 8.7) with assert (no need for eassert), but I wonder if this change of semantics is not a bug that was introduced at the time of adding eassert...

Finally, note the related issue https://github.com/coq/coq/issues/7412 requesting a new “especialize” tactic.

Théo

Le mar. 8 janv. 2019 à 15:41, Marko Doko <mdoko AT mpi-sws.org> a écrit :

On 2019-01-08 07:17 UTC+0100 Jeremy Dawson wrote:
>
> given a hypothesis, such as
> H : A -> B
> how do I get this to two subgoals, one with B as a hypothesis,
> and the other with A as the conclusion
> (where either A and B are too long to type in, or where I want to do
> this inside an Ltac tactic, where A and B may vary)
>

Here a tactic from Hahn library (https://github.com/vafeiadis/hahn) that
achieves the above (and a bit more):

Tactic Notation "specialize_full" ident(H) :=
  let foo := fresh in
  evar (foo : Prop); cut (foo); subst foo; cycle 1;
  [eapply H|try clear H; intro H].


If you call

  specialize_full H

you will get two goals. The first one will require you to prove A, and the
second one will contain hupothesis H: B.


--
Marko