The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Jeremy,

You cannot rewrite in hypotheses on which other hypotheses depend.
You have to rewrite simultaneously in them.

You can try

revert H0 H2; rewrite <rew. eq>; intros H0 H2

If you can use subst, it generally does not suffer
from that problem.

Best,

Dominique

Le 12/07/2019 à 16:02, Jeremy Dawson 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
> 
> 
> 
> 
> 
> 
> 
> 
> 
> 
> 
> 
>