The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 03/14/2013 04:51 PM, Jason Gross wrote:
> 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].

In this case, the assertion is proved easily if you add after [assert]:
    by (destruct e; reflexivity)

> 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.

This looks like exactly the problem I was describing earlier in the 
thread, and the solution I proposed works:

  match goal with
    | [ |- appcontext[?e] ] => is_evar e;
      evar (n : nat);
      evar (n' : nat);
      let n0 := eval unfold n in n in
      let n'0 := eval unfold n' in n' in
        clear n n'; assert (e = f n0 n'0) by (apply f_equal2; reflexivity)
  end.