coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] how to rewrite, needed to match goal

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] how to rewrite, needed to match goal
Date: Thu, 17 Dec 2020 14:43:34 +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=kemkpK4GC1hcT6dkmKgb4OR/L0AtMdOd++wmCLkmKi4=; b=mtttmClx1C9LlFQ34YSlPuLZcACzpJu8ch6IpTzNUPMMQV+AaIm8NTBPWxXUuVXuLR7oUbnNp30bHvsNQQsJFpGuDLdzpJ5SqeZ7aj153d/xa8HJTrdaR0TKXJJmGZYFP+xK2R3mditzqdjrLEa+cYx8KiUZ6eIidsbp9LUGWRtnJPL22JbMU82hsoOTuNerhmN/IoicwUXI7Z/5Xmambj0IlFrlNXl0hsQYvkHokuvc8gYGG4GOqHn9M39k6GnYNH/oii2yGK1VIsxCFa+LulP8q/7QZho5i3rucOm27g9roBxnk3it2ngoGMWR3WANpa4Lai2394pj4ypXvR2WFQ==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=aJqo2QK+aByFeNfjPMoY34Hk/VERRXBhLfiva9WLaS8vbtCkbnZdR8sk2dfq67kB5/aq87BicPMZmBC32S8aSui2RMuJoLXtN9M3Af19IuQHObtoi1JzT7DRJRX4k9gZ5NYsi7xgUkPR3G2sCApvKvLnxZpVYSmzRs06W9N5w48nP7t22fy06L5YwEobDFQp7pOhALH6FHNPvy4ruPXvaZcQpk6TKCROImZp6W0t21RP5eAE5MrocOgr+4ipQatqwxV1WQ05mgyGBUnsSzVJRkQJlUMjYUbrCpMae4cEEh/q8T8N5YE1M7K4u+CynGoMfOXsevEydi5DrVxbKBt8rw==
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-ME3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:OrCB9h/HgZHL1v9uRHKM819IXTAuvvDOBiVQ1KB20u4cTK2v8tzYMVDF4r011RmVBNqdsqMfwLaI+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhKiTanfL9/KBu7oQreu8QXnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRRn1gykFKjE56nnahNJwgqxGoxyvqRJwzJLbboGUO/VzZb/dcNAASGZdQspcWS5MD4WhZIUPFeoBOuNYopH5qVQQtxuxGwysBePywTFGnHD307Y60+MnEQrb2wEuG8wBsG7Ko9XwNKYeS+67w7PGzDXYaPNW3yzw55LOchA8u/2DQ69/cdfLxUY1CgPIl1OdopHqMD2JzOoCqXSb7/Z+WuK1jW4qswV8rDizy8ojhIfEiY0Yx1/K+Clk3os4OcO0RUx7bNOgEZZeuCCXOoR2TM4gXWxluyQ3xLIEtJO4ciYHyIkqyRHZZveacIaI+gruWemNLTtimX5pZLCyiwyv/US8yeDwTM253VJSoidKltTArG0B2h/P5sSdVPdw8EWs1SyS2w3X9O1JJ10/m7DBJJ472LEwk4IesUTdES/yn0X7lLObeUs59OS09ujre7LoqJCSOoNtjQHxKbohlta4AeQlLggBRG+b+fm61LL+50H5WK9KjvoqkqbHrJ/aOcUbpqm/AwNP1YYj9gq/DzOh0NQfnnkLNk5KeBWCj4TxOlHOJu73DeunjlmjjDtn3e3KMqHjD5nXM3TPjLTscax55kNY0AYzyMpQ55NQCrEPOvLzXUrxucTcABAnKQy73ePnCdVn2o0QQ22ODLSZMKTUsVKT/O0vJfSMaJULtzngNvgp/eThjWIhlV8HYaapxYcXaGy/Hvl+P0qZZmPsjs4dHmcOowoxV/fniEaCUD5Wf3a9Rbgw5jA9CIK8DIfMXJqhgLKb3HTzIpoDLGtBExWHFWriX4SCQfYFLiyIaIc1mTsdELOlVoUJ1Be0tQa8xaAxfcTO/ShNl5/52d1kr8Haigo183QgLcmH3mScCU19gXgPQRc/2r05rEBgjF6eh/sry8dEHMBesqsaGjwxMoTRmrQjVoLCHznZd9LMc26IB9WrBTZtEYAY/uRWOgNYNo7niRrOmS23H7USirqHQoQu9b7R1GTwIMA7zGva0K4mjB8tRc4dbDT61J46zBDaAsvyq2vcj7yjLP5O1SjQsmqP0CyHoRMACV8iYeD+RXkaI3Dug5H870LGQaWpDO19YAJH1IiPJrYMY8C71Fg=

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, Clément Pit-Claudel, 12/30/2020