The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Apparently, refine doesn't like you to leave holes under a forall. There is probably no good solution in your case. Except moving to the development version of Coq: the refine tactic has been completely reimplemented and accepts holes anywhere.

On 16 February 2014 05:06, Anders Lundstedt <anders AT anderslundstedt.se> wrote:

Dear all,

continuing my attempt to define a realizability relation, I get the
error in the subject line when trying to use the refine tactic.

An example is below (pastebin: http://pastebin.com/acR7xAEy). I know I
can avoid the refine tactic by replacing the blank with "(pf b)", but
this is not a very convenient option for the full definition of
realizability.


Parameter A : Type.

Parameter bin_op : A -> A -> A.
Infix "*" := bin_op.

Inductive is_A_atom : Prop -> Prop :=
| eq_false          : is_A_atom False
| eq_atom (a b : A) : is_A_atom (a = b).

Inductive is_A_formula : Prop -> Type :=
| atom_formula (P : Prop)      : is_A_atom P -> is_A_formula P
| uni_formula  (P : A -> Prop) : (forall a : A, is_A_formula (P a)) ->
                                 is_A_formula (forall a, P a).

Definition helper : A -> forall P, is_A_formula P -> Prop.
refine (fix r a P (pf : is_A_formula P) := match pf with
| atom_formula _ _          => P
| uni_formula P pf          => forall b : A, r (a*b) (P b) _
end).


Best regards,

Anders Lundstedt