The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 15 May 2013 22:20:27 -0400,
Jason Gross 
<jasongross9 AT gmail.com>
 a écrit :

> Hi,
> Can someone explain to me the error message in the following code,
> and why the bottom snippet causes it, but the top snipped does not?
> 
> Record Foo := { foo : forall A : Set, True }.
> 
> Goal Foo.
> pose (fun pf : Set -> True => @Build_Foo (fun A => pf A)) as H.
> apply H.
> Abort.
> 
> Goal Foo.
> apply (fun pf : Set -> True => @Build_Foo (fun A => pf A)).
> (* Toplevel input, characters 22-72:
> Error: in : Application of lemmas whose beta-iota normal form contains
> metavariables deep inside the term is not supported; try "refine"
> instead. *)
> 
> Thanks,
> Jason

I am not sure of this, but in the second case,
"apply (fun pf : Set -> True => @Build_Foo (fun A => pf A))."
the returned type is not Foo, so it probably tries to use internally
something like:
"apply ((fun pf : Set -> True => @Build_Foo (fun A => pf A)) _).",
performs simplification to have:
"apply (@Build_Foo (fun A => _ A)).",
which cannot be solved, due to existentials.

eapply does not give better result though.

In the pose (H := …) version (it is the same as pose (…) as H.), you
introduce a definition, and this cannot be reduced, so
"apply H." does not work, but "apply (H _)." does since H is not
unfolded, and the form where existentials are on top of the term seem
to be managed by apply, unlike those which are deep (like the error
said).

Let H := fun pf : Set -> True => @Build_Foo (fun A => pf A).
Eval simpl in (H _).
Eval simpl in ((fun pf : Set -> True => @Build_Foo (fun A => pf A)) _).

I think that is the reason, but I am all but certain on it.