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
- Subject: Re: [Coq-Club] how to rewrite, needed to match goal
- Date: Thu, 17 Dec 2020 15:42:35 +1100
- 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=GyycCSR4dpzPhSrIhw6Cke1IZYhyQ9Ktx98vtpzuyRg=; b=fUmtOQXgJT4SPeVe0m2XQ2bacYN+mud6iHEWm/A6w+eaApS6mCC4sq2/EUgvbzAPZYW+iar6eT/QLEW9PXUOcBOaJTok3JfXL9yRDLum2pfWFZdxDYkKjmO0YyBro8LNN15wvj6b95AFCPJf/WyPwfcnLeeAgbN7ikyff3r9JJB3t34iR0SmuEYa5CPprqCwPJhLLBlhz6fv8rWNQeY3Vxo3f16umdgstG64Iuy7yoRyt2lDT6dfHsracQyQ4ogx/dbnlMcZnWxbDE+47HCTakRBbecLR3Np58KLNmveuk1bp4wklYB6LSUhQf1jmYX2EbRdD0QmXMyIUMFXB3kGRw==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=fZqSs4yXkGE9K8cr/4zlXy/MwhS1LzAB7jAt/KwiNIq9F0vCnYdsONNeI4sMBbTiixtPmgKnO+B1HvkFJS2ebR33eZ14qpctlg4g9lR0QsQofJ7JQlQy2cZQLJ9Kub7Prl7/ZvAr6sM4skK1PWoWLddSmX0utdm6TVsqF8WMQz+Y3JbzC8+3xbcD/tqivpBOzGpOlPzdjoOTGfPy4UH7laN2H702BpAZmH9RtLtdBhYVcH0JqmbvTN4ZZ3HuRlIa7icEjIAeIrs/HWef+O4FdbMeyjXHFMBjswAmVu+ywiIgkOozraVihS61xuDpwzRo796F8rk9Gvgvs0Q0Wz5zvw==
- 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-ME3-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:hkdD0xHPar6cM5L89FQ8ZJ1GYnF86YWxBRYc798ds5kLTJ7yp8ywAkXT6L1XgUPTWs2DsrQY0rWQ6vG7EjBeqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5wIRmssAncsscbjYRtJ6sw1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrg+/qRxxw4DaY4+bO/R8cazBct0aRGVOU91NVyFCGI6wc5cDAuQDMOtesoLzp0EOrRy7BQS0AO3g1CVIiWHz3aw6zu8vHxvJ3QI7H9IJtnTfsdL4OqMMXuCv0qbIyDXCY+lY1zjn5onIaRchofeXUL1qd8rR1FMjGB3YgVWNs4DqJS6V2/0LvmOG4OVuSfihhHQ7qwFtvDev3MEsh5HHiI4J1lzK+jl0zYUpKNCkSEB3fMCoHIVOuy2HKoZ4TN0vTWFrtSsk17ELtpG1cScFxZkoxhPTdfOKfoqG7B/jUuuaPDR2hGp9db+wmxq+61WsxvH+W8WuzVpGsilInsPRunwQyRDf8seKR/9n8ku82juDyxrf5v9KLE02j6bXNposzqA2m5EOq0rMBDX2l1/zjKKOdkUr5Oyo6+P/b7j6qJCSKpN4hhznPqoplcKyD/00Mg8VUGeF4+i806Dj/VHiT7VNk/02lLTWvIrCJcQBoa65HxFa3Zo/6xa+CDem1s4UnX4aLFJZfBKHiI/pO1LULP/kCve/hkygkDZtx//YIr3sGprAImTZnLv8Ybpw6VRQxBcvwd1c/Z5YF6wNLOzrVk/0rtPYDxs5MwKuw+bgDdVwzocQVnyVAqCHNaPTsUWE6Ow1LOiCf48VvzD9JuM/6P7okH81g0EScrS03ZcNcn+4A+xqI1+Fbnr0ntcBDWAKsxIiQ+ztkV2OSCJcZ3KvX60n/Tw7E4KnDYLbRo+3mrCB3SG7HodXZm9cEFyMH23oJM24XKIHbzvXKct8mBQFU6KgQskvz0KArgj/nphqNOfR62U0vI340949s8/ejxw35HpYBtuG1GelRmdp2G4EWnk/wfYs8gRG1l6f3P0g0LRjHttJ6qYRC1poBdvn1+V/TuvKdEfBc9OOFAn0a+idWWh0a/9qhtgEbgB6BsmoiQ3F02yyGbgJmreXBZsytKXBw3z2IMU7wHHDhvB43gsWB/BXPGjjvZZRsg3aBorHiUKczvz4fKIBmiPB6SGK0DjX5R0KYEtLSazAGEsnSA7Ot92gvBHLSaLoBLg6dAJcm5aP
curiouser and curiouser -
in investigating how I got to this situation I found that
Coq would substitute (using subst.) the following equality in l and d1
Γ0 = Γ1 ++ []
So doing rewrite app_nil_r before substituting solves my problem in this particular case.
But in general - (1) why can you do subst but not rewrite in d1
(2) in general, how do you handle this problem
Jeremy
On 17/12/20 2:43 pm, Jeremy Dawson wrote:
Hi,
I have the following goal (only key parts included)
l : LJArules (map (apfst (fmlsext (Γ1 ++ []) Γ2)) ps1)
(fmlsext Γ1 Γ2 [Imp (Var p) B], Var p)
d1 : dersrec LJArules prems (map (apfst (fmlsext (Γ1 ++ []) Γ2)) ps1)
apd : allDT (no_rpt_same seq_ord (prems:=prems))
(derI (fmlsext Γ1 Γ2 [Imp (Var p) B], Var p) l d1)
============================
allDT (no_rpt_same seq_ord (prems:=prems))
(derI (fmlsext Γ1 Γ2 [Imp (Var p) B], Var p) ?l ?d1)
Now the goal doesn't match apd because the types are wrong,
?l and ?d1 have types which would match those of l and d1 if
l and d1 had (Γ1 ++ []) rewritten to Γ1
But rewrite app_nil_r in d1. rewrite app_nil_r in l.
fails because
Ltac call to "rewrite (ssrrwargs) (ssrclauses)" failed.
d1 is used in hypothesis apd.
Ltac call to "rewrite (ssrrwargs) (ssrclauses)" failed.
l is used in hypothesis apd.
How can I handle this situation?
Thanks
Jeremy
- [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/17/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/28/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/30/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/17/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
Archive powered by MHonArc 2.6.19+.