The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Huh.  That works in my toy example, but once again causes [Defined] to run ~forever in my actual example.  Closing the proof with

  all:exfalso; clear; admit. Grab Existential Variables. all:exfalso; clear; admit.  Time Defined.

right before the [let unused := ...] line in my actual example gives under .2 seconds, whereas I haven't seen it terminate yet doing it after that line.

On Sun, Apr 2, 2017 at 9:34 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

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