The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

proof_admitted is just a proof of [False] that is used to implement the [admit] tactic.  You can only use it to get around "Instance is not well-typed" when your instance came from [admit]; in this case, you're essentially just running [admit] again.

On Thu, Jul 24, 2014 at 7:35 PM, Jonathan <jonikelee AT gmail.com> wrote:

On 07/24/2014 02:06 PM, Jonathan wrote:

However, I guess the criticism here is that this is the all-to-common (for me, at least) case of needing to fill in an existential when it's too late to do so (getting the "Instance is not well-typed in the environment of" error) - and instead (hopefully) knowing in advance what to do to set up for a successful instantiation.

Trying this out:

Goal exists n, n=0.

refine (ex_intro _ _ _).

(*normally, it would be too late to fill in that evar with newly-introduces things, like:*)
assert  {m:nat|m=0} as H by admit.
destruct H as [x H].
exact x. (*No "Instance is not well-typed" error!  Cool!*)

But, what on earth is happening in that second subgoal?:

  ============================
   (fun H : {m : nat | m = 0} => let (x, _) := H in x)
     match proof_admitted return {m : nat | m = 0} with
     end = 0

Hmmm... let's try pushing the red button marked danger:

destruct proof_admitted.

Boom!  It worked!

OK - so now I want to know more about this proof_admitted mumbo-jumbo.  What is going on there?  How can I use this to get around other cases of "Instance is not well-typed" related to lateness of instantiation?

-- Jonathan