The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

On Fri, Mar 15, 2013 at 9:45 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

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)

Yes, but that leaves me with

1 subgoals, subgoal 1 (ID 231)

  

  H : ?227 = {| CO := ?227; HO := HO ?227 |}

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

   ?227 = ?227

Whereas I really want something like

1 subgoals, subgoal 1 (ID 231)

  

  H : {| CO := ?228; HO := ?229 |} = {| CO := {| CO := ?228; HO := ?229 |}; HO := HO {| CO := ?228; HO := ?229 |} |}

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

   {| CO := ?228; HO := ?229 |} = {| CO := ?228; HO := ?229 |}

 

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.

I'm not sure what you mean hear; my [subst] does the same thing as your [unfold].  Anyway, this is a case that I already had working the way I want it to.  The problem is getting it working with dependent types, like in the first example in this email.

Maybe a higher-level remark will clarify what I'm looking for.  Ideally, I would be delighted with a new tactic [transparent_assert], which is like [assert], but allows future goals to see the generated proof tree.  I'm trying to do simpler forms of this manually, with evars.

-Jason