coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Dual of Well Founded Induction in CoInductive World
- Date: Sun, 14 Aug 2022 16:06:10 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf1-f48.google.com
- Ironport-data: A9a23:NUhYRq2ySRShpW6wN/bD5e13kn2cJEfYwER7XKvMYLTBsI5bpzQHy GJMUTzTbKrZYGKjKNklOY7goxsE7MPUztRlQVBl3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/nOHNIQMcacUsxLbVYMpBwJ1FQywIbVvqYy2YLjW1PU4 oupyyHiEAbNNwBcYjp8B52r80sHUMTa4Fv0aXRjDRzjlAa2e0g9VPrzF4npR5fLatU88tqBe gr25OrRElU1UPsaIojNfr7TKiXmS1NJVOSEoiI+t6OK2nCuqsGuu0o2HKJ0VKtZt9mGt4pj8 toO746cdQYgfaH+hP4mFEkfVC4raMWq+JefSZS+mcmazkmDd3W1hvsyXAc5OooX/usxCmZLn RAaAGpVP1bT2qTvnu39FrkEascLdKEHOKsap3Jt1jHFDOkvW5GFQqTL+dpw0zI5h8QIFvHbD yYcQWA2NkuROEAQUrsRILsDm+LzhWT2SAICg3eZ5pAS4HKP3iUkhdABN/KMIoDQLSlPpW6To XuD9GDkCDkBJdmHwHyE9Gitj6nBh0vGtJk6EbS58rtujgTWyDBDThIRUlS/rL+yjUvWt89jx 1I8oDgUouto5mCXT9C+Uy+kukXD7llbVI8FewEl0z2lxq3R6gefI2ELSD9dddAr3PPaoxR6h jdlePu5VVRSXK2ppWG1rejL8GvjUcQBBSpTOn9eFFptD8zL+dlr1nryosBf/LlZZ+AZ9Bn1y jGO6Sww3vAd0Z5N2KK88lTKxTmro/AlrzLZBC2GBApJDSsjP+ZJgrBED3CFtp6sy67HEjG8U IAswZT20Qz3JcjleNaxaOsMBqq1wP2OLSfRh1Vid7F4qWr1pyf+IdoNvW8vTKuMDiriUW+5C KM0kVMBjKK/wFP3BUOKS9nsVZpynPiI+SrND6CFP4omjmdNmP+vpXkyPyZ8Lkjil08jlaxXB HtoWZfEMJruMow+lGDeb75Fj9cDn3lirUuOG82T50n4idK2OS/NIZ9YYQDmRr1ovMus/l+Jm /4BbJDi40sEAIXDjtz/q9F7waYidihlW/gbaqV/Koa+H+aRMDh7Vq+Onu5/JtUNcmY8vr6gw 0xRk3RwkDLX7UAr4y3TApy6QL+wD5t5s1whOikgYQSh13Q5MNSg6a4ec908erx+rL5vyvt9T v8kfcScA6QXGm6XpWhFNZSt/pZ/cBmLhB6VO3X3bTU6ealmTVOb99LheDzp6yRTXDG8stEzo uH72w6CGcgDSg1uAdz4cvWqy1/t73ERlPgjDUTNK9hXPk7r9dEyeSD2i/Y2JeAKKAnClmPKj VbIXU9AqLCU8YEv8dTPiaSVlKuTErNzThhAAm3WzbeqLi2FrGeuxIl3VuzXLz3QUWXD/rr7O bdYwvT6B/0wnFhQtr16Hbs2n7k14MHipuMDwwlpQCfLYlCsBu8yK3WKx5MU5KhEx7scvQXvH 0zTqp9VPrKGPM6jG1kUfVJ3YuOG3PASuz/T8fVlfxmgtXEvpOKKARdIIh2BqC1BN78pYokr9 uEs5ZwN4Aulhxt2b9uL0nJO+2KXIiBSWqkrrMtBUoriiw5uzl8bJJKAWmn555aAb9gKOU4ve 2fGiK3HjrVa50zDb3tjSiSXjLQF3cwD6EJQ0VsPB1WVgd6Z1PU56xtcrGYsRQNPwxQbju9+N wCH7aGuyXliItupuCRCY4xoMwRIBRnc/kKojlVVxCvWSE6nUmGLJ2o4UQpIEIb17EoEFgW3P pnBoIombdouVM701yo2H0VirpQPiPRvoxbalpnP89utRvEHjPmMvkNqTWUNohrjR8g2gSUrY AWsEPlYMcXGCMLbn0H350R2G1jdpNBo6VGumc1cwZ4=
- Ironport-hdrordr: A9a23:tV9DZ6wFNkjDK6JD/CRWKrPwIb1zdoMgy1knxilNoH1uA6ulfq WV9sjzuiWE6wr5NEtBpTniAsi9qBHnhPxICOAqVN/IYOCMghrMEGgN1/qH/9QiIUHDHyxmuJ uIv5IQNDQ4NzZHsfo=
- Ironport-phdr: A9a23:X89ydxS1/KShMLaoazavCHt/OtpsohmVAWYlg6HPa5pwe6iut67vI FbYra00ygOTBsOBtqoP27GempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffQtFiCCjbb5yM Bm6ogbcu8cLioZ+N6g9zQfErGFVcOpM32NoIlyTnxf45siu+ZNo7jpdtfE8+cNeSKv2Z6s3Q 6BWAzQgKGA1+dbktQLfQguV53sTSXsZnxxVCAXY9h76X5Pxsizntuph3SSRIMP7QawoVTmk8 qxmTgLjhiUaOD4j6GzYhcx+gqxYrhy8uRJw35XZYJ2JOPdkYq/RYc8WSGhHU81MVyJBGIS8b 44XAuoEIOZYrJfyp0AOrRCjGQmsBe3uxSVShn/3wKY31OEhERzF3AM+BNIOsGjUrNT7NagIS +C1zbPEzTTCb/NXxTf97ZPFch8kof6WXLJwddDdxlUoFwPAl1idr5HuMDyJ2OoXqWeb8/ZgW vy1i24hswx/rDehytkshIXUmo4Yy1/K+yt7zYs7K9C1RkF1bMOqHpdOqy2XKpZ7T948T2xqt yg3yrMItJCmcCQUyJkqxh7SZvqaeIaG5RLjUfyeITZ+hH99ebK/gQyy8Um6xeHmWMm0ylBHp TdGnNnUrn0ByQDf58ydRvZ+/kqtwyuD2gHR5+1eLk05lqzWIIM7zLEqjJocq0HDEzf2mEroi K+WcV0p+u2y5OTmZrXqv5ucN4Fphg3nPKQjlc+yDf43MggJWGib9uC826P58ULlR7VKi+U6k qjfsJ/EOcQWvrC1DxNR34o56BuyDy2q3MkZkHQFNl5IdxGKg5DsO17UIfD4Cfm/g06rkDdu3 /3GO6DhApbTIXjYkLfhYbd96kBGxwopzNBT/ZNUCrAAIPLvX0/8r9PYDhojPAy1x+brEsly1 oQbWW6XBK+WK7vdsUWU6eI3P+mMeIgVtS7gJ/Q9/f7hkWc5mUMBfamuxZYYdHe4Hu1/L0qFZ Xrsn8wOHHwRvgs+SezqkEeNXSRSZ3a0RaI85ys0BJioDYfZFciRh+mK2z7+FZlLbEhHDEqNG DHmbdaqQfAJPSePIcJ6knQYVKeoUY5pgRSztwLhy6ZmMePO+2sZtJP/0fB64uTSkVc58jkiX JfV6H2EU2whxjBAfDQxxq0q+SSVq3+G2Kl82LlDEMBLouhOSkE8PILdyOpzD5bzXBjAd5GHU gXuWc2oVBc2SN952NoSewBlAdz3iw3A0jGqH74KnqaKQp01877Z93f0Lsd5jX3B0fpplEEoF /NGLnbunatj707WDo/NnV+ekvOvaKcRxy7R9XiK12vIvUBZTAtYXqDMXHRZbUzT/pzi/k2Xa bioBPw8NxdZj86PLqwfctrykVBPX+vuIvzbamO13mO+XFOGmuPKY43tdGEQmi7aDSDoiig1+ nCLfUg7Dyal+CfFCSB2UEnoewXq+PV/r3WySgk1yRuLZgtvzej9/BldnvGaR/4Ju9BM8C48t zV5Gkq81NPKGpKBoQRmZqBVfdI65h9Oy2vYswV3OpHoIbplgxYSdAF+vkWm0BsSaM0IlNUpo Wgq0AttILiZllJAdi+d9Z/1M7zTbGL1+VHnaqLb3E3fzMfD4r0Gu5Fa4x3ouACkEFZn8m0yi YEElSvBoMyUU0xOAcGUMA5/7RVxqrDEbzNo4orV0SYpKqyoqnrZ3MpvAuI5yxGmdtMZMaWeF Qa0HddJYqrmYOEshVWtaQoJee5I86thdca7dPad2LKqI+96nXSnjGVb5ahy10uN82x3TeuCj PNni7mImxCKUTvxlgLrt930lJtEeTANF3C+jynlBZJUTqJ3dIcPT2ypJofko7c2z46oUHle+ lm5AloA08L8YhueYWv22ghI3FgWq3iq8ceh5wR9iCph7q+W3SiVhv/naAJCIWlTAm9rkVbrJ 4GwydEcRkmhKQYzxlOp4kPzxq4To6oaTSGbRFpLcjP2M2B9W7Gx8LuDYtJKwJwtuCRTFu+7Z BiWR6X8rB0Tzy74VzEGlXZrKnfz5Mq/w0wygXn4Tj47tHfDfMBs2RrTrMfRQ/JcxHtORSV1j yXWGknpOtCo+duOkJKQ+uu6Vm+nSthSaXyxldLG5Hb9vDM1R0HvzJXR0pX9HAM30DH2zYxvX CTM91PnZ5Xzkr+9KaRhd1VpA1n174x7HJt/m80+nsJ1uzBSi5OL8H4AiWq2P89c3Pe0aWcOS CUL39/K6RLknkxiL26M7438X3SZhMBmYpPpBwFekjJ49M1MBKqOufZBgCh4uVqkrB3Ye/k7n zYc1f4G53sTguVPsw0ohHb4YPhaDQxTOirikA6N5ta1ofBMZWqhRrO30VJ3gdGrCLzR6hEZQ nvyfY0uWDNh9sgqekyZy2X9s8u3HbuYJcJWrBCflA3MyvRYOI5k3ORfnjJpYCr8pSF3kLN91 E02m8vm487fbD8xtKOhXkwGanuvPJhVo2+1y/4Zx5fzvcjnH409SGtVGsKwF7TwVmpV76yvN h7SQmNi7C3HSPyPRUnHrx0+53PXT8L0bTfOeD9AnI8kHF7EdCk9yEgVRGlowcJ/T1r3gpSnK AAguHgQ/gKq80McjLs3aF+vFD+Y/l7gay9oGsHAd1wPv10EvwGNdpXAi4A7VyBAos/79F3Le jHdPl4YSzlOAxPMBki/bOP3u5+do67BV7D4d7yXMP2PsbAMDa7Wg8j0g809pXDUcZzeWxsqR +sy3k4JNZxgM+LenThHCykeliaWKtWeuA/54Spv6Ma27PXsXgvro4qJEbpbd9t1qViwhu+YO uiciTwcS34Q344QxXLO1LkU3UIDwyBoeT63FL0ctCnLBKvOk65TBhQfZmt9LsxNp6472wBMP 4bchLaXnvZgieUpDl5eSVH7ssSgZMhPJ2/kcV2bVACEM7OJITCNyMbyIOu9RbBWkORIpkiwt DKcQCqBdnyIkzjkUQzqMPkZ1nnKekwD/tjjLVAxWTuGLpqucBCwPd5pgCdjxLQ1giiPLmsAK X1ndFsLqLSM7CRei/E5Gmpb73MjI/PX/kTRp+TeNJsStuNmRypukOcPqnEnyLZO7D1FW/Vvm W3Tr99ypnmpl+COznxsVx8E+VMpzMqb+F5vP6nU7MwKQXHf4BcE9nmdETwPrtphT9nh4uVel oiJm6X0JzNPtdnT+IFPYqqcYNLCO30nPx3zHTfSBwZQVj+nO1bUgElFme2T/HmYxnDbgp3lm Z5LTrECEVJpRrUVDUNqGNFEK5ByDGtMeVuzg8sB5H74px7UFp0yVn/vWfebAPGpIzGc3+AsW g==
- Ironport-sdr: BXMVCqrkSQvn5PcjDj4WoJ0fnqYfFNl8suNV6pk8gIXzMb9QBMZG+0UEhD9dA5OZf+DEmjAysj /bblYXk+IyUlV3G7I+HjpOBXdKtolrRvEQjsZ3luuI7SYsUj7+792RkQU9oKQqWjqM2KYnE6fY guQvTT//s9dsLMRMY/+P6U6pW+vHGc3/pBC4pa954HxJdK4Xa3qIwqSk1jd/CvelutebDCoz5p Dz9TgZyv3f5XiHzRRyKU+qTISA6P51s/BoYrV46kv/QhX9TImipBGS6gD64m6CMMM/sJaKSksH nlbBBMFwsrDnHN8c/5zWZV9i
Hi everyone,
I am wondering if there is some dual notion of well founded induction
[1] in the coinductive world? If yes, then can you tell me about your
use case and point me towards your Coq code? (Also, it's quite
possible that this question may not make any sense from Coq's logic
perspective, and in that case, apologies for the noise).
Best,
Mukesh
[1] https://coq.inria.fr/library/Coq.Init.Wf.html
- [Coq-Club] Dual of Well Founded Induction in CoInductive World, mukesh tiwari, 08/14/2022
- Re: [Coq-Club] Dual of Well Founded Induction in CoInductive World, Ralf Jung, 08/15/2022
- Re: [Coq-Club] Dual of Well Founded Induction in CoInductive World, mukesh tiwari, 08/16/2022
- Re: [Coq-Club] Dual of Well Founded Induction in CoInductive World, Ralf Jung, 08/15/2022
Archive powered by MHonArc 2.6.19+.