The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Thanks.  I've tried the following

instantiate (W := W).
 > ^^^^^^^^^^^^^^^^^^^^
Error:
Ltac call to "instantiate ( (ident) := (lglob) )" failed.
Unknown existential variable.

I've never used the instantiate tactic before, but
instantiate (?W := W).
seems to give a parsing error

What am I doing wrong here?

Thanks

Jeremy

On 07/13/2019 12:14 AM, Matthieu Sozeau wrote:
> Hi Jeremy,
> 
>   It seems your hypotheses contain extistential variables ?W and ?W0 that 
> by default depend on all previous hypotheses. You can try to either 
> instantiate them or cut their dependencies at the time they are introduced 
> (by clearing unnecessary hypotheses for their later instantiation), then 
> the rewrite should work.
> 
> My 2 cents,
> -- Matthieu
> 
>> Le 12 juil. 2019 à 10:02, Jeremy Dawson 
>> <Jeremy.Dawson AT anu.edu.au>
>>  a écrit :
>>
>>
>> Hi,
>>
>> I have the following goal:
>>
>> (earlier hyps, then)
>>    H0 : (Γ1 ++ Γ2) ++ ?W ⊦ A :: Δ
>>    H2 : Gnh_height H0 < n
>>    H : (Γ1 ++ B :: Γ2) ++ ?W0 ⊦ Δ
>>    H1 : Gnh_height H < n
>>
>> To make use of these hypotheses I need them in the form
>>    H0 : Γ1 ++ Γ2 ++ ?W ⊦ A :: Δ
>>    H : Γ1 ++ B :: Γ2 ++ ?W0 ⊦ Δ
>>
>> trying to rewrite with app_assoc_reverse produces the errors
>>
>> Error: Cannot change H0, it is used in hypothesis H2.
>> Error: Cannot change H, it is used in hypothesis H1.
>>
>> Is there any reason why what I'm trying to do should be invalid?
>> How can I get around this problem?
>>
>> Thanks for any help
>>
>> Jeremy
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>