Ssreflect Users Discussion List

[Beta Ziliani <>]

Hi list,

Someone asked me in the #coq irc channel how to build some particular algorithm using canonical structures, and besides some particular problems with the original formulation, I found out that apply: is not succeeding where refine is.

The full code can be downloaded from here: http://paste.awesom.eu/98m

Right now it is using "refine" instead of apply:, and it's working. But if I change refine to apply:, it complains with "Error: Could not fill dependent hole in "apply"".

In short, I want to apply

getPos : forall (T : Type) (position : nat) (h : T) (f : find_seq position h)
         (default : T), h = nth default (untag_seq (seq_of f)) position

to the goal

 1 = nth n mySeq ?229 (* [] *)

(notice the existential). What I was expecting is apply: to unify (in this order)

T with nat

h with 1

default with n

untag_seq (seq_of f) with mySeq (defined as [:: 1; 2; 3])

this last step should trigger the canonical structures resolution and obtain a value for position, which should in turn be unified with ?229.

Why is apply: not allowing such applications?

Thanks,
Beta