The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Oops.  Sorry, I forgot to clean up my code from a previous version of what I tried.  I meant to paste

    Record NT := Build_NT { CO :> forall x : nat, x = x;

                              HO : CO = CO }.

    Goal exists x : NT, x = x.

      clear.

      esplit.

      match goal with

        | [ |- appcontext[?e] ] => is_evar e;

                                  assert (e = @Build_NT (CO e) (HO e))

      end.

      apply f_equal2.

What I want to do is be able to say that [e] should start with [@Build_NT].  Here's an example that works the way I want it to:

Goal forall f : nat -> nat -> nat, exists x : nat, x = x.

    clear.

    intro f.

    esplit.

    match goal with

      | [ |- appcontext[?e] ] => is_evar e;

                                evar (n : nat);

                                evar (n' : nat);

                                assert (e = @f n n') by (apply f_equal2; subst; reflexivity)

    end.

(note that [n] and [n'] are dummy evars, which get instantiated by [reflexivity], but aren't used there-after.)

I think the problem I'm having has to do with dependent typing.

-Jason

On Thu, Mar 14, 2013 at 4:36 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

Maybe the problem has to do with choosing an evar instantiation that refers to new local variables created since the birth of that evar?  I'm a bit confused by the code below, which defines [t] and [t'] but doesn't seem to refer to them.  If they were used somehow to instantiate [e], then you would have an instance of the problem I suggested, in which you'd want to do something like [let t0 := eval unfold t in t ...] and refer to [t0] instead of [t].

On 03/14/2013 04:31 PM, Jason Gross wrote:

Is there a systematic way to partially instantiate an evar?  That is, if I have an evar [e] and I want to instantiate [e] as [f _ _] for a known [f] (and get the two holes as new evars), is there a way to do that?

I feel like I should be able to do it with something like the following, but I haven't managed to make it work.

Record NT := Build_NT { CO :> forall x : nat, x = x;
                              HO : CO = CO }.
      Goal exists x : NT, x = x.
      clear.
      esplit.
      match goal with
        | [ |- appcontext[?e] ] => is_evar e;
                                  let T := fresh in let t := fresh in evar (T : Type); evar (t : T); subst T;
                                  let T' := fresh in let t' := fresh in evar (T' : Type); evar (t' : T'); subst T';
                                                                        assert (e = @Build_NT (CO e) (HO e))
      end.
      apply f_equal2.

Thanks,
Jason