The Coq mailing list

[Anders Lundstedt <anders AT anderslundstedt.se>]

On Sun, Feb 16, 2014 at 5:31 PM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> Does replacing [forall b : A, r (a*b) (P b) _] with [(fun x => forall b : A,
> r (a*b) (P b) (x b)) _] work (possibly with some additional type
> annotations)?
>
> -Jason

Yes, it does, thank you! The drawback is that it is not very elegant.
Example (pastebin: http://pastebin.com/nzet8G8i) below.


Parameter P : True -> Prop.

Definition Q : Prop.
(* will fail due to "metas in product" *)
try refine (forall n : nat, P _).
(* solution: lambda abstraction on the blank *)
refine ((fun x : True => forall n : nat, P x) _).
apply I.
Defined.

Parameter P' : nat -> Prop.
Axiom pf : forall n, P' n.
Parameter P'' : forall n : nat, P' n -> Prop.

Definition Q' : Prop.
(* will fail due to "metas in product" *)
try refine (forall n : nat, P'' n _).
(* solution: lambda abstraction on the blank. this time we need to abstract a
   dependent product *)
refine ((fun x : (forall n, P' n) => forall n : nat, P'' n (x n)) _).
apply pf.
Defined.