coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] rewriting something used in a subsequent hypothesis
- Date: Fri, 12 Jul 2019 14:02:51 +0000
- Accept-language: en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1;spf=pass smtp.mailfrom=anu.edu.au;dmarc=pass action=none header.from=anu.edu.au;dkim=pass header.d=anu.edu.au;arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=xTcK0aTWRa3dbRhL4n5l+aA0ZshooLh6xeePMJM3RKk=; b=OYImG3RxyXiusBkp0/5MiKralEoO/U6QbfCbSDaQ9+ndg/TypSqyK+1MK8M4YHx2JC/AzLPwX3SZf822ZhPsE5NJdvRS3uUG5KzBOutUcwRvpUVN6rwmGYDGIW5oIIVrqQhgA0+yKrt8kHXnO7bCfhnYrJXRp5NO9UXfRakUAOaRimROaAVZZf1SW8aQ6q2KxCwqkliWT8W/m2USeqrsJSbNOUfSvFiSj2H1OBKYCpBw2jE2bL+3WUYNjC+otmCuyToDn7XPC3pVsuXq5V63X0tR6L/Rw1BXcd9eCC1zmPXur7YZgy7J7MH7EY1YG4XNrgbAUIKEPUXS3d5aSlyWew==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=eOHBu0UnCZZTdR55oBylYPtYSvd/mak+fGo95TlrBjZz9McnvrzHZesJitzPkPlvqCTvOnD/GpmaDnhWTId2DrJm9qtqEV6Gki7RcRhBLZ0bR5y4pAziO0492KVm63Lrikceephbhww8H3DaAnk58A3PKbUIo3u0zJ+fnc/VSNB/DO1e7bSQLMhp5HjOuzcRsd1yiZ9Y1wNojTKHcscG3Olv3amYpvhxIV8chbjzTGqCydE4TfPrvtYnuovT7DBVcA3Bi9gb/6tCIznJC7yJIvco+K8z7VMvY29qZdn4zuCMP6eRO98p/oyzRUW1ugS/H4cmOmpNrcda6ojHYx7tqQ==
- Authentication-results: mail2-smtp-roc.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:qxx2Jxf+tmZakCXVedXkA2HwlGMj4u6mDksu8pMizoh2WeGdxcS9Yx7h7PlgxGXEQZ/co6odzbaP6ea9ASdesN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vMhm6twXcutUZjYZjLqs61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9Zwgbpbrhy/uhJ/34DaboKUNPVica3ScsgXRXZaUctLSyBNHp+wYokJAuEcPehYtY79p14WoBW6GwasHv3gyjpIh3Tr06M1yeogERrB3AwmAtkDt3Dao8vvNKgMVOC0zLPEwzvZYPJYwjf9747Ifws7rvGKQLJ8a9TexlQyFw/flFqQtJXoMjWI3eoOq2iW9+VtWf61h2I6tw18oCKjytoih4TInI4YzlTJ+T1kzIopK9C0UlN3bcK5HJdKqi2XNZZ6Ttk/T2xrpio20rMGtoC4cSQWzZkqwh7SZvyZf4WL5x/sT+mcLixmi39gfL+yiAy9/Eilx+HiTca7y01FoyxYmdfWrH8NzQbc6s2fR/t94Eih3TGP2hjP5+5KPE44ibfXJ4cmzLA/i5YfqEPDETTol0nsi6+Wa1kk9fOv6+T6ZLXpu4WQN5duigH5LqQhhNCwAfg5MggJWWiX4+O81KD//U39R7VKif42nrPFv5DdIMQXvq+5AwlL3YY/8xuyACuq3M4FkXUbLl9JYg+LgoboNl3UJP31Ce+zg1G2nzdqw/DGMKfhApLILnXblLnuY6x95FBZyAsz19xR6YhbC78aIPL0XE/8r8bXDhkkMwCu3enoFch92pkEVmKSGqOZKr/dsUeU5uIzJOmBfJMauDHkK/Q8+/HuiWI5lkQGcKmy3ZoXbWi4Ee58L0WYZ3rsmNYBHn0QsgowVuy5wGGFBHRYYG/3VKYh7Bk6DpinBMHNXMrl1LeGxWKwGoBcTmFAEFGFV3nyIdaqQfAJPQCfOMJkg3QoXKe6TIlpgTOjrgL/2vxLJ/XP/SswvJT+ktV5+qvaiEdhpnRPE82B3jTVHClPlWQSSmpuhfEtkQlG0l6GlJNArbldHN1X6elOV15gZ5fa0qp3B820Ux+TJ47VGmbjec2vBHQKdvx028UHOhwvEtO/yB3PwmyjHu1NzuHZNNkP6qvZmkPJCYN9xnLBiPZzpmQdGpIKEED/w6l1+k7UGpLDlFifm+Cyb6MA0SXR9WCFi22ToEVfVw02WqLADykS
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
- Re: [Coq-Club] rewriting something used in a subsequent hypothesis, Dominique Larchey-Wendling, 07/12/2019
Archive powered by MHonArc 2.6.18.