The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I can't seem to get it to work, even if they are skolemized.  Here's a toy example that works, but when I do the same thing in my actual example, [Defined] takes over 30 hours and over 10 GB of RAM after the refine:

Axioms A B : Prop.

Goal exists a : A, B.

  clear; intros; evar (a:A); exists a.

  (*

  a := ?a : A

  ============================

  B

*)

  revert a.

  refine (let pf : A /\ B := _ in (proj2 pf : let f' := proj1 pf in B)).

  (*

  ============================

  A /\ B

*)

Here are my failed attempts using the strategy I think you're proposing:

Axioms A B : Prop.

Goal exists a : A, B.

  clear; intros; evar (a:A); exists a.

  revert a.

  instantiate (1:=ltac:(refine (proj1 ?[a']))).

  simple refine (let pf : A /\ B := ?[pf] in _); cycle 1.

  intro a.

  Fail unify a (proj1 pf).

  Fail unify (proj1 pf) a.

  Fail all: [ > unify ?pf ?a' | ]; [ | ].

  Fail all: [ > unify ?a' ?pf | ]; [ | ].

Do you have any ideas?

If you want to play with the actual example, see https://coq.inria.fr/bugs/show_bug.cgi?id=5437.

On Sat, Apr 1, 2017 at 2:48 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

You first need to skolemize x before doing that unification, so that it
has no hyps.  You can also then set up the new goal with no hyps as well
- so they will then both have no hyps at the point of the unification.

To skolemize, do something like "instantiate (1 := ltac:(revert_all))",
where revert_all is the obvious:

Ltac revert_all := repeat lazymatch goal with H : _ |- _ => revert H end.

-- Jonathan


On 04/01/2017 02:20 PM, Jason Gross wrote:
> Say I have an Ltac variable x such that [is_evar x] succeeds.  How do I get
> a goal corresponding to x, in an Ltac script (without vernaculars)?  I
> tried making a new goal and unifying the evar of that goal with x, but that
> fails with a "not well typed in the context of x" message, because I have
> different hypotheses.
>
> Thanks,
> Jason
>