coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Suneel Sarswat <suneel.sarswat AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Mapping of types to new one in a project
- Date: Mon, 24 Jul 2023 23:21:45 +0530
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=suneel.sarswat AT gmail.com; spf=Pass smtp.mailfrom=suneel.sarswat AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f43.google.com
- Ironport-data: A9a23:XRgMWaL75TpBQ/7HFE+RGpElxSXFcZb7ZxGr2PjKsXjdYENS0jBRx 2MXWzjTM/iMMWajc49wOori8UkPu5DQx4VqTwAd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6j+fSLlbFILasEjhrQgN5QzsWhxtmmuoo6qZlmtHR7zml4 LsemOWBfgf8s9JIGjhMsfnb90k05K+aVA4w5zTSW9gb5DcyqFFOVPrzFYnpR1PkT49dGPKNR uqr5NlVKUuEl/uFIorNfofTKiXmcJaKVeS9oiY+t5yZv/R3jndaPpDXmxYrQRw/Zz2hx7idw TjW3HC6YV9B0qbkwIzxX/TEes3X0GIvFLLveBCCXcKvI0LuIlL+na9+J0oPM6YEx7xZJjkQ3 N0XN2VYBvyDr7reLLOTT+BtgoEuIJCuMt9E/H5nyj7dALAtRpWrr6fiv4cJmmdtwJoWTbCCP KL1ahI3BPjESwZSPFoaDNQllf2zmXDjWzJdoVOR46Ew5gA/ySQviuG8b4WJIbRmQ+0MuXu+9 kbM/17YWA85b8a78AeA80uV07qncSTTAdpOTtVU7MVCi1qKg2cXFRc+Tkq+ufD/i0ikWtsZJ VZ8x8Y1ha079UjuQ9WkGhPk+ziLuRkTX9cWGOo/gO2Q9kbKy1ewFDZeXhVKUdINqPJsaxtyi HaokMy8UFSDr4apYX6a876Vqxa7Ni4UMXIOaEc4oe0ts4mLTGYb3kKnczpzLEKmpoaqRmyok lhmuAB71upD15dav0mu1Qmf22rEm3TfcuIiCuzqso+N6wp4YMuoa9Xt5wSAq/lHK4mdQx+Ku 31sdymiAAImXM/leM+lGr1l8FSVCxCtbmC0bblHQcVJythV0yT/Fb28GRknTKuTDu4KeCXyf GjYsh5L6ZlYMROCNPEmO9vqVJxxlPS+TrwJs8w4iPIeMvCdkyfXrElTibK4gggBbWB2wfxhZ cnFGSpSJS9AWPk6pNZJewvt+eZzmnpWKZL7Spf8wBCquYdyl1bEIYrpxGCmN7hjhIvd+Fu92 48Ga6OilU8DOMWgOXK/2dBIfTg3wY0TX8+eRzp/Lb7dfGKL2QgJV5fs/F/WU9c+wP8Kzb6Sp SDVt40x4AOXuEAr4D6iMhhLAI4Dl74mxZ7iFX13ZQSbyDI4bJyx7awSUZIycPN1vKZg1PN4B b1NMcmJHv0FGHyN9iU/fKvNitVoVC2qogaSYAujQjw0JKB7SyLzp9TLQwrI9Qs1NBSRi/cQm bOa617kccIxfDg6VMfyQ9Cz/my1pkkYyb5TXVOXA9x9e3fM0YlNKg73hMAZO8sndBfJnGOb8 y20Ah4og/bHjKFo0dvOhIGC95yIFcknFGVkPmDr15SEHgiEwXiCmKhrT/StUQ3Gcl/N6IGOR Llw3u7tFv8qh3NIuNdMKKlqxqcA+Nffnb9W4QB6FnHtbV7wKLdfDlSZ/MtIpItf76R4vFaoZ 0ex5dVqA7WFF8f7Glo3JgB+TOCi1+kRqwbC/8YOP0T2yy9mzoWpCXwIEUG3txVcC79pPKcO4 +Qr4pcW4jPirCsaCI+NiyQM+lmcKnAFbb4ciagbJ43V2y4L0VBJZKLOBhDmuK+vb8p+CWh0A zu2qpebuZFi6BvjSUcjLVnMwutXuroWsj9o0lIpBgqEi/jFtNANzTxT9jU9cSpNxD4e19BfF 3RZNXRnAaCC4T0yiNNxZD2uEVsZBTmy2E/4+30WnkL3EmiqUW3sKjUmGOCvpUo2zUNVTgJ5z pq5lln3dCnMfd7g+BcyVWpOie3RffYo+iLswMmYTtm4Rb8kaj/bs4qSTGsvqSq/J/guhUfC9 NJYzMwpZYLVbScv8rAGUa+E3rEtSTeBFmxIYddl2IgrRWj8WjWD6QKiGnCLWPFmBqL1qBejK slUOMhweQy013+OohAlFKc8GeJIs8Bz1uUSWIHABDAgg+OEoytLoaDg0HH0pFUWTuVElec/L YLsdAy+LFGAuEsMm0LwqJhrB2npR/gFewz2486t+sorCZ8okb9hYGMy4JSOrlSXNwpVpUuUt Tzcep6MnvBDyJttraToAK5sFwW5EvKtdeWqoSSYkcVCUsPLCujK7zgqk1jAOx9HG4ceQPFlv O2pnOOv+XjarZEadnv8maiRM4VovuKMBPF2NODzJ1lkxRqyYtfmuUY/yjrpOK53n8N4zej5Y hmzd++bV8MfAvVZz11rMxluKQ4XUfnLX/2xtBGGjqq+DzYG2lb6N/Khz3jiaF9begIuO5HTD gzVue6k1utHrbZjVQM1OPV7P6BWeFPTe7MqV9nUhwmqCmOFhlCjuLy7myR5uHuPQjOBHd3h6 J3IegnmeV7g8OvUxdVeqMppsgdREH95hvIqc1kA/8JtzQq3F3MCMf9XJKBu5ku4ScAu/MqQi PDxgGoe5eHVWD1FdVDx7I2mUFvEQOMJPdj9K3oi+Eb8h+Jawm+fKOMJy8uiyy4elvjfICWPJ tQX+3m2NR+0qn2sbfhG/eS12I+L2duDrk/lOinBfwjaDBMXALFM33tkdOaIueorDOmV/Hj2y aMJqayoja11pYMd0SqtRpKNJCwkgQ==
- Ironport-hdrordr: A9a23:C1QwaaAB8rAnEcvlHemV55DYdb4zR+YMi2TDtnoBMCC9F/bzqy nApoV/6faZskdyZJhko6HiBEDiexLhHPxOkO0s1N6ZNWGMhILrFuFfBODZslrd8kPFh4hgPG RbH5SWyuecMbG3t6nHCcCDfeod/A==
- Ironport-phdr: A9a23:9/Os6hQUJbphfOF0YKt15PzygtpsoqyVAWYlg6HPa5pwe6iut67vI FbYra00ygOTA8OGu7kd0rGempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffQRFiCC9bL5xI xm6sBjdu8cLioZ+N6g9zQfErGFVcOpM32NoIlyTnxf45siu+ZNo7jpdtfE8+cNeSKv2Z6s3Q 6BWAzQgKGA1+dbktQLfQguV53sTSXsZnxxVCAXY9h76X5Pxsizntuph3SSRIMP7QawoVTmk8 qxmTgLjhiUaOD4j6GzYhcJwg6BbrhyvpBJx3pDab52OOfVkYq/QZ8kXSXZdUstTUSFKH4Oyb 5EID+oEJetWspT9p10QohSgAQmnGf7hxSVShn/t06w1yfghGhzB0Qw7AtIOtmrbo8vxNKsIS uC61rPIzS7NbvxMxTfw84fIchU7rvGNWbJ8a9beyU4qFw7ciFibtIPqMS+P2OsXr2ib8/RvV fipi2M/tQ1/ojqiy9swh4fGmI8bxUzI+Tl2zoooO9G2R0B2bN+qHZdMtCyXNol7T8cjTmxot ig31qMKtJ6mcCULyJoqxRjSYOGEfYiQ+h/vSvqdLDNiiH9meL+znQi+/VSjx+HmWcS53lBHp TdfnNbWrHACzRnT59CHSvRj+keh3i6C1wXJ5eFFJUA4jLTUJIM8zrIpmJoevkrOEjX5mEXxi 6+WeUEk9fay5+v7ZbXmo4eQN45yig7gLqQjgtKzDfg8PwQUXGWW+f6w2KP/8UD6WrlHgfM7n rHcsJ/AJMQboqC5AxVS0oYm8xu/FCqm0NIGknYZKFJJYgmHgJLzO1HVLvH3F+u/jk+jkDdu3 f/GP7nhDo/RIXjElbftZbB95FVExwop0d9f/45UCq0GIP/rR0P9rMbYAQMhMwyo3+bnD81w2 Z8ZWWKWG6OWLKfSsUKT6e80OOmNZIoVuC7nJPQ/5v7ui2U5mV4HcqWz05sXciPwIvMzKEKAJ HHon90pEGEQvwN4Qva5pkeFVGtoenC/UqZ03TghE52vEc+XXZ2rjbGFmjyyBIZJb3xuBVWFE HOufIKBDaRfIBmOK9Nsx2RXHYOqTJUsgEnGXG7SzrNmKrGR4SgErdf408Az4eTPlBY0/DgyD sKH0mjLQXsn1ngQSWoQ26Zy6Vd41k/FybJx1udFE9Fe47VSWx0hKpfA5+N/AtH2HAnGe4TBU 06oF+2vGip5Vdct25kLakd5Fc+li0XYwiynDrtTjLWRH4M97orT2nHwI4B2zHOVnLI5gQwAR c1CfXajmrY59wXXANvRlF6Fkq+xaakG9CvE9WPGwGbX+U8EC0h/VqLKWX1ZbUzTxTjgzmXFS bLmSbEuMw8ajNWHNrMPcdrxy1NPWPbkPt3aJWO3gWa5QxiSlPuKa8LxdmMR0T+4agBMmh0P/ XuAKQk1Bzuw62PYAjt0EFvzYkTqueBgoXK/R0UwwkmEdUpkn7ay/xcUg7SbRZZxlvofpSEsp jEyB1+nxM3fF/KPogNgeONXZtZ8qFZL2GTFthBsa4S6JvMH5BZWeAB2skXykhRvX98YwI568 TVwlFo0dfnLtTEJPymV1p3xJLDNf2z7/RT0LrXTxkmby9GOvKEG9PU/rVzn+gCvDEsrtXt9g Lw3mzOR4IvHCA0KXNf/SEEyolJhurfXby17/IrOzmJlLYG7tzbD35QiA+5vmXPCN59PdbiJE gP/CZhQHNWoJeEu3UOgdAkbNfx6+6s9PsfgfPyDkv3OXq4ojHetimJJ55p420SH+n9nS+LG6 J0CxumRwgqNUzqUYE6JisnsgsgEYDgTGjH60i34HMtKYbU0e48XCGCoKsnxx9NkhperVWQKv FKkAloH3oeud3/wJxTmwAtd2EBRunW9gjSx0xR7ljgoquyU2ymGz+n5dRUBM3JGXyE41Qaqc dXy1YhKGhTzJwEy8XntrV733a1auLhyIyHITEFEcjK3Z2BuX62st6aTNstG6ZcmqyJSA6y3Z VGXTKK4ogNPiXuyWTsDgmpjJ3f24cac/VQykm+WIXdtoWCMfMhxwUya/9nAXbtK2SJAQiBki D7RD1z6Pt+z/NzSmY2Q14L2H2+nSJBXdjHmiI2asy7ur3Z3BxCym7aok8f8DgEm+SD+3thuE y7PqVyvB+ujn7T/Ku9hckRyURXn9sx3F4U4iYIqn44ZxVAVg5yU+TwMlmK5YrA5keruKXEKQ zAM2dvc5gPojVZiIny+zIX8TnyBw8FlaoryciYM1yk69cwPFLaM4ekOg35uulTh51G0A7A1j nIHxPAp8nJfn+wZpF9n0HCGGr5LVUhAYX63ylLRvoj49vkIIj7oK+T41VIiz479SuvZ+UcFB i6/ItB7TEoSpo1+KA6ejiO1s9m+PoGWNZVJ7lWVi0uS0bYTcs5g0KpSw3IgYzq1vGV5mbFhy 0Uym8jr5s7fbDw9mcDxSh9Aam+qO4VKoGyr1eAG2Z/Il4G3Qsc4QmVNBcS3C6LuSHVI7LzmL 1rcSWJn7C7KRfyHW1fYsRkDzTqHEoj3ZSvPdT9JkJM7HknbfAsG30gVRGloxMdnUF36gpWwK gEhoWlArl/g9kkWk7wubUKuFDyF4l/vM2ZRKtDXOhNS6ksqC179F8uY46ozGihZ+sbktwmRM imAYBwOC2gVW0uCDlSlP7+05NCG/fLKTuy5Z+DDZ7mDs4k8H7+B2I6v3416/j2NKtTHP39sC Oc+01ZCWnYxEtrQmjEGQSga3yzXaMvTqBC58yxx5sexlZajEBro/peKAqBOPM9H/hm3heKOO 7fVinoibzlf0ZwIyDnDz71elF8ehidydiW8RLQNsSmeKcCY0qRTDhMdd2ZyLJ4St/N6jlQLY 5aLzI+uhdsaxrYvBlxIVELsgJSsbM0OeCSmMU/fQV2MLPKALCHKxMf+ZeW9T6dRhaNarU7V2 37THkn9MzCEjzSsWQqoNLQGlzydMRFa/pq0aA1yAHTLQ9fvaxn9O9hyx25To/V8ljbROGgQP CIpOVtKtaGV5DhEj+9XHmVA6j9oIbDBlXrCqebfLZkSvL1gBSE+xIc4qDwqjrBS6i9DXvl8n iDf+8Vvr1+Rme6K0jN7URBKp16jYaqEuExjPePS8ZwSAR4sHToI5GSUThkG/p5rVoaptKdXx dzC0qn0LWUamzo71cQZDsnQbsmANSh4WSc=
- Ironport-sdr: 64beba3e_TZg0sBYNjsVBRk+VtoUeazur+UkvbYvGgAm1fTgq8dA926X H4VpHUppRisYFJKgUMZTg9mGwvso94Mc4HhQ2nA==
Dear Mukesh,
Thanks a lot for this answer. This is natural and I am feeling bad about my laziness.
Also thanks for the last two theorems, this will be anyway needed.
Have a great day.
Regards,
Suneel
On Mon, Jul 24, 2023 at 10:34 PM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:
Hi Suneel,
I am not sure if it's exactly going to help in your case but you can prove a lemma like this:
Theorem same_f_old_new : forall (r : list r_old), f_new r = List.map f (f_old r).
And use it to replace (f_new r) with (List.map f (f_old r), and hopefully, after this you can use the theorems related to f_old. (I must confess that I don't understand coercions (:>) very well so it is quite possible that there might be an easier solution, or this one may not work).
Best,
MukeshRequire Import List. Section Rec. Record r_old : Type := mk_old { a :> nat; b : nat }. Record r_new : Type := mk_new { c : nat; d : nat }. Definition f (u : r_old) : r_new := match u as _ return r_new with | mk_old a b => mk_new a b end. Definition g (u : r_new) : r_old := match u as _ return r_old with | mk_new a b => mk_old a b end.
(* This might come handy *) Theorem first : forall (r : r_old), g (f r) = r. Proof. intro r. refine match r with | mk_old a b => eq_refl end. Qed. Theorem second : forall (r : r_new), f (g r) = r. Proof. intro r. refine match r with | mk_new a b => eq_refl end. Qed.
(* end of handy theorems *) (* Your definition of f_old *) Definition f_old (B: list r_old) : (list r_old). Admitted. (* Your definition of f_new *) Definition f_new (B: list r_old): (list r_new). Admitted. Theorem same_fold_new_old : forall (r : list r_old), f_new r = List.map f (f_old r). Proof. Admitted.(* I don't think you need this but we never know :) *)Theorem same_fold_old_new : forall (r : list r_old), f_old r = List.map g (f_new r). Proof. Admitted. End Rec.On Mon, Jul 24, 2023 at 12:54 PM Suneel Sarswat <suneel.sarswat AT gmail.com> wrote:Dear friends,
I have an old project (large one) in which I have a few functions, their specifications, and their correctness theorem along with their correctness proofs. Now I have redefined some of the functions and even input-output types. Although my new input types have changed, but the actual values and computations are the same. It's the types at each input instance that have changed (not their actual values and computations) and old functions are replaced with more efficient versions now (See a minimum example below.).
Now I want to restate some of the theorems in terms of new input-output types and functions. The goal is to do this with a minimum amount of new proofs or minimum efforts by using old functions and their correctness proofs.
Basically, I want to show a bijection between the outputs of new and old programs and then want to use it to show the correctness of the theorems without redoing the old work again (which means using the old work as a black box). Please suggest some ideas.
Have a great day.
- Suneel
--------------------------------(* Old input type *)Record r_old:Type:= Mk_r{
a:> nat;
b: nat;
}.(* Current input type is *)Record r_new:Type:= Mk_r{
c: nat;
d: nat;
}.(* I have a = c and b = d. *)(* Old function *)Definition f_old (B: list r_old): (list r_old):= f_old ( Sort_old a_dec B).(* New function *)Definition f_new (B: list r_old): (list r_new):= f_new ( Sort_new c_dec B).(* Note:Sort_new is more efficient than Sort_old.The elements of B are all unique.f_new and f_old are the "same" programs in the sense that they do exactly the same calculations. Also is there any way to avoid writing f_new?*)
- [Coq-Club] Mapping of types to new one in a project, Suneel Sarswat, 07/24/2023
- Re: [Coq-Club] Mapping of types to new one in a project, D. Ben Knoble, 07/24/2023
- Re: [Coq-Club] Mapping of types to new one in a project, mukesh tiwari, 07/24/2023
- Re: [Coq-Club] Mapping of types to new one in a project, Suneel Sarswat, 07/24/2023
- Re: [Coq-Club] Mapping of types to new one in a project, mukesh tiwari, 07/24/2023
- Re: [Coq-Club] Mapping of types to new one in a project, Suneel Sarswat, 07/25/2023
- Re: [Coq-Club] Mapping of types to new one in a project, mukesh tiwari, 07/24/2023
- Re: [Coq-Club] Mapping of types to new one in a project, Suneel Sarswat, 07/24/2023
Archive powered by MHonArc 2.6.19+.