The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 04/02/2017 08:29 PM, Jason Gross wrote:
> 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?

I think that's a bug in unify, maybe related to 
https://coq.inria.fr/bugs/show_bug.cgi?id=4957.

Try this:

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.
  let unused := constr:(eq_refl:(a = proj1 pf)) in idtac.

-- Jonathan