coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] rewriting something used in a subsequent hypothesis

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] rewriting something used in a subsequent hypothesis
Date: Fri, 12 Jul 2019 22:44:41 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:oD5hxhF62PzO2Fa4KSZ2bp1GYnF86YWxBRYc798ds5kLTJ7zr8mwAkXT6L1XgUPTWs2DsrQY0rCQ7vmrADZIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfK1+IA+2oAnMucUanJVuIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1jioMKjw3/3zNisFojKxVvg+vpwBxzYDXboGaNvt+cb/Sc9wVXmdBQt1eWjZdDo+gc4cCDewMNvtYoYnnoFsOqAOzCw2yC+P11DBIg3/31rA03es7HwDGxwsgH9QTu3nTqNv6Kr0SXv6wzKjI1znNYelZ2Dnm6IjPdBAsuuuDXbRtccbL10YgCh7Fgk+Kpoz4Jj6Y0PkGvWuD7+d4Wu+jl3QrpxxtrjWt3Msgl4fEi4MPxlzZ6Cl13p45KcCkREN1e9KoDYdcuzyAO4drQM4uXntktDs5x7EYoZK7cjYFxZc7yxPabvGKc4iF7gzgWeuUOjh1i2lqd6y6ihu2/kWv0O3xW8yq3FlRtSVKid/BvW0X2RPJ8MiIUP5981+h2TmR0wDT7flJLFw6mqTGN5It36c8mJ0cv0jeByP2n175g7GMekUj5+io9//oYrL7pp+aKoB4kBn+Mr4pmsyjH+s3LhQOX2mc+eS6zrHj+lD5QKlOjv0xlanZs4rWKtgcpq68GwNV04Aj5AijDzq+39kUgWMLIE9ZdB+FlYTlJl/DLfHiAfuinligji9nx/XcMb3gBpXNIGLDkLDkfbtl70BT1hAzws5a55NUEL0PLuj8W0HqtNzfCB80KBa7w+D6CNlnyIwRRH+PDrWDP6PPqVOI/P4gI/GQZI8JvzbwM+Qq5/n3jXMghVAdebSp0oAMZXCjHvVmJl2ZbmD2jtcAF2cKpAs+Q/bwhF2MSz4AL0q1Cug34Sh+A4a7B6/CQJqsifqPxm3zSpZRfyVNDk2GOXbubYSNHfkWPnG8OMhkxx4JT7WkWscN3A61swmyn5hqNOfR62s0vI34095d7uvO0xw+6Hp9EpLOgCm2U2hokzZQFHcN16dlrBklkwvR4e1Dm/VdUOdrybZRSA5jb8zVyfE8BtzvHAvcLI/QFQSWB+6+CDR0deofht8DZ0EhRIeLsyubhm+PLuZQkLaGQpsp7qjbwn79Yd5nzGrL37UgiF9gRdZTMWqhheh08A2BXteYwXXcrL6jcOEn5ACI8W6CyWSUu0QBClx5V7iDUHwCIELL/430

thanks very much, this worked fine

Jeremy

On 07/13/2019 12:07 AM, Dominique Larchey-Wendling wrote:
> 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
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>

[Coq-Club] rewriting something used in a subsequent hypothesis, Jeremy Dawson, 07/12/2019
- Re: [Coq-Club] rewriting something used in a subsequent hypothesis, Dominique Larchey-Wendling, 07/12/2019
  - Re: [Coq-Club] rewriting something used in a subsequent hypothesis, Jeremy Dawson, 07/13/2019
- Re: [Coq-Club] rewriting something used in a subsequent hypothesis, Matthieu Sozeau, 07/12/2019
  - Re: [Coq-Club] rewriting something used in a subsequent hypothesis, Jeremy Dawson, 07/13/2019