Ssreflect Users Discussion List

[Georges Gonthier <>]

   Indeed, Laurent -- here's the detailed explanation I sent to Beta but 
forgot to cc: to the list.

In general, apply: can't assign to pre-existing unification variables. If I 
recall correctly, this was difficult to achieve in the original 
implementation, which conformed to the general tactic API. It tried to 
minimize evar environments by extending the global proof evar map with just 
the relevant part of the extended evar map that was created by type inference 
and unification, rather than simply threading the map through the entire 
proof construction process; for example this allowed eager garbage collection 
of all the temporary unification variables that were created then assigned to 
during type inference.
I think the function that did this did not deal well with assignments of old 
variables, so for the sake of robustness I put in a test that simply rejected 
all unifications that required assigning pre-existing unification variables 
(essentially, treating them as new constants). Since we are now paying the 
50% slowdown due to the new proof engine threading a huge global evar map 
through the entire proof construction process, this precaution may no longer 
be necessary, however.

   Georges


-----Original Message-----
From: Laurent Théry [] 
Sent: 08 August 2013 14:16
To: Beta Ziliani
Cc: ssreflect
Subject: Re: apply:

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.