Ssreflect Users Discussion List

[Laurent Théry <>]

On 08/08/13 14:05, Beta Ziliani wrote:
> 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
I think this has nothing to do with the canonical structure:

Goal exists n : nat, 0 = n.
eexists.
apply: (eq_refl 0).

does not work either. I think apply: does not instantiate existential 
variables but the standard apply does.

Goal exists n : nat, 0 = n.
eexists.
apply eq_refl.
Qed.