Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Theorems as Fixpoints

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Theorems as Fixpoints


Chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Theorems as Fixpoints
  • Date: Fri, 3 May 2024 09:20:52 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-pj1-f50.google.com
  • Ironport-data: A9a23:Z+3jDqtSnM3hG6hVM2Nyh4lIt+fnVPNaMUV32f8akzHdYApBsoF/q tZmKTyAOvjYZWD1KoojPY+x8R5TvcXUzNYwHVQ5/Hs2Fy4TgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTrSCYEidfCc8IA85kxVvhuUltYBhhNm9Emult Mj7yyHlEAbNNwVcbCRMtMpvlDs15K6u4G5A5ARkDRx2lAa2e0c9XMp3yZ6ZdCOQrrl8RoaSW +vFxbelyWLVlz9F5gSNz94X2mVTKlLjFVDmZkh+A8BOsTAezsAG6ZvXAdJHAathZ5plqPgqo DlFncTYpQ7EpcQgksxFO/VTO3kW0aGrZNYriJVw2CCe5xSuTpfi/xlhJE4oIowxxvRqOGdH5 +YEI2BQTh6f1/3jldpXSsE07igiBMziPYdaonM5iD+EVbApRpfMR6iM7thdtNsyrpoWTLCOO oxDMGQpMUyojx5nYj/7DLomneqynHS5eDpFsk6UqLcf7G3azQg327/oWDbQUoXUGZ4PzhrJ/ woq+Uz4CTwxJsGe8QG7+1aOoePCgTnVCbwNQejQGvlC2wDKnjNCVnX6T2CTqv6gz0W6Rth3M F0R4iNorK4o9UXtQMOVYvGjiHuNvxpZQ9gJVuNnsEeCza3b5wvfDW8BJtJcVDA4nMAoWj0D6 k2UptXgFyZzu+3IaXyBpqjB+FteJhMpBWMFYCYFSy4M7N/ivJw/g3rzojBLQP7dYjrdSW6Y/ tyakBXSkYn/miLi6klW1VXOgjbpvpqQCwBovkPYWWWq6g4/b4mgD2BJ1bQ5xacbRGp6ZgDe1 JThpyR4xL5UZX1qvHLXKNjh5Jnzu5643MT02DaD5aUJ+TW34GKEdotN+jx4L0oBGp9bIGO3P xON51wJvcM70J6WgUlfM9LZ5yMCnfiIKDgZfqmJBjazSsEtKlLao30yDaJu9zuzwBRw+U3AB XtrWZ3xVC5FWPoPIMueSOAa3rsmjiE4ziW7eHwI50XP7FZqX1bMEe1tGALWMIgRtfrYyC2Lq Yo3H5XRkH13DrauChQ7BKZJcjjm21BgVc6owyGWH8bfSjdb9JYJW6WJnu15ItM790mX/8+Rl kyAtoZj4AKXrRX6xc+iMxiPsZu2Bcwh/0EodzchJ0ip0HUFaIOipvVXPZgucLVtsKQpwfdoR rNXM4+NE9ZeeAThoj49VJjaqJA9VRKJgQnVATGpTgJidLFdRivI2OTeQC3RyAc0ABCK6PQO+ 4+b6luDQL4oZRhTM8LNWff+k3KzpSc8ncxxbWvpI/5SWkPmz6ZyIQesjPVte8AoAjfAzwu8y Ay5L0o5p+7Mgolt6/jPp/mOgLmIGttEPHhxPjfk/5fvEgLF7E+P/JRmbN+YWRz8CEbl57SEZ 8hO6vP3bc08g1dBtrRjH4ZRza4R48Xlo5lYxF9GGErnQkuKCLRyBGuvxuhK67Nww4FGtTuMW k6g/sdQPZOLMpjHFH8TPA8UUfSR58oLmzX97eUHH2ui3XVZpIG4aER1OwWArAd/L7EvaYMs/ roHif4ssge6jkInD8aCgiVq7F+zF30nUZg8l5QkEYTu2xsKyFZDXMTmMRXIwqqzMvdCDkp7B QWvpvvmp69dzU/8YXYMBSDz/e5Ct68v5jFO7nE/fmqspPSUp8UZ/hNr9RYPcj901TRCiuJ6B XhqPRZ6JIKI5DZZu/JAVGGNRSBECAGoxUjq714vimfiblKJU1bVJzYXIte9/0E+8kNdcANE/ bqe9n3XbDbycOz13QowQURAqcG/afBU6Sv5h5mBM+meOps1cx7Jo/WLXnUZjQnjDecaplz1l cMz8MleMaTEZDMt+YslAIyk5JEsYRGjJkkZZNp+/akMTFruSBvr1Regc0mOK95wfdrU+kqFC utrFMJFdzK68A2s9jk7J6o9E4VYrc4TxugpW+3UfDYdkr6lsDBWnora9XH+iE8VUtxeq5sBB b2LRQ2SMF67pCVyoHDMnvlmK2DjQNgjZS/A5s6X3tgNNao+tLBLTRlv/Jqy526YISl2zSKy5 QnjXZLb/8Zm6IZrnrbvLJl9OhWJGYvzetiloAGXmPZSXOzLKvbL5l80qEG4HgF4PokxetVQl JaRgeHzx2f1lq8TaDncvaWoCpsTtNuABvpTFsfRMnNhvDCjXfX06EAp4FGIKp1ukfJc6PK4R gC+VtCCSN4NV/pZx1xXcyJ7AT9HL4jWN4DO/TicqdaIATgjiT33FsutryLVXDsKZx02NI3bI S6qnfSXv/RzjplGXT0ADNFYW65IGkfpA/YaRoegpAujLzeah32ZseHfjjsm0zbAD0eEHOvc4 Z7oQhvfdgy4iJrXzeN24pBDgRkKMElT2eUAXFoR29pTuQCICGQrKec8M5JfLrp2lif09o/zZ RCTTW8EJBj+Yw95ckTH0Iy+ZjucO+0ABI6obHhhtUaZcDy/C468EaNsvHUoqWt/fjz4ivqrM 5cC83n3JQK82YxtWf1V3PGgnON73bnP8xrkI6wmfxDaWH7ywInm1UCN2CJIXC3DVtnPzQDFe DBzSmdDT0W2D0X2FK6MvpKT9A4x5FvSI/cANE9jA+ozf62UyeRBzLv0POSbPngrcpERPLBXL Z/obzLl3o1Vs0D/fYMmvtsohel/Dvfj8g1W6kP8bVV6opxcIVjL8y/PceTjgS3iFMNi/4vhq wSR
  • Ironport-hdrordr: A9a23:6P9iPqxAv4MyNumX4SCEKrPwvL1zdoMgy1knxilNoERuA7Slfr OV7Y8mPH7P+UAssR4b6LS90cW7IE80sKQFmLX5Xo3SFTUO2lHYS72KhLGKq1aLdkGQygce79 YHT0EUMqySMbEOt7ee3ODOKadD/DDoysCVbbi09QYkcelPA5sP0+4zMHfgLqQ/fng6OXOSLu vW2iKMzwDQB0j+rayAdwg4t5Konay5qHq8CyR2dSLOrGK1/ESVAHuTKWnp4v/bOwk/tIvLNg D+4njEDqnPiYDG9vbz7R6t06hr
  • Ironport-phdr: A9a23:/5nXNh/IimG2MP9uWfa2ngc9DxPPW53KNwIYoqAql6hJOvz6uci4b QqFvKQm1QeSFazgqNt6yMPu8JrcEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PXbglSmjaxfLd/I BqroQnNuMQdnJdvJLs2xhbVrXREfPhby3lvKVyPgRj3+92+/IRk8yReuvIh89BPXKDndKkmT rJWESorPXkt6MLkqRfMQw2P5mABUmoNiRpHHxLF7BDhUZjvtCbxq/dw1zObPc3ySrA0RCii4 qJ2QxLmlCsLKzg0+3zRh8dtjqxUvQihqgRwzI7aYo6bNPRwcKDAc90EWWVMRdxeWzBbD46mc 4cDE+gMMOBFpIf9vVsOqh6+CBG2CuPu1DBInGX20rMn2Ok/FgHGwRYgH84PsHvKsdX+KaAfU fi0zKbW1zXDde1Z1S3h54jPbxAhu+2MXbNufsrM0kQvGAbFgU+RqYzhJT+ayuMNs22C4udmS OmghHIppRtrrTiz2scjlJPJhoQNx13E6yl3zpg5KNO6RUNmYtOpDIZduiKVOoV2X84sQ25lt Sknx7AYuJO1fDYHxZo7yhLCZfGKbYiF7xzhWeqNJTp1gm9udrGnhxuq70Ss1unxWtO33VtKt CZJjMTAu3EX2xHT9sSKTOZ281ml2TaSzADT9v9LIVopm6raKp8u3KY9moYVvE/eBCH5gl/2g 7WTdkg8+uin9eDnYrL+q5+ZLYB0iwX+Pr02msy9HOg0KwYOUmiH9eim273j+kr5QLpOjvIoi KXWrJfaJcEDqq64BQ9azJoj5g6hAzu61NkUh3oKIVJfdB6ZkoTkOkvCLfDkAfunhlSjijZrx /TIPr37BZXNK2DOkK/gfblj8U5c0hQ8wcpD6JJTF7EBOu7zWk7vu9zFFRI5PAm0zPzmCNV5z I8RRWWPAqqBPKPUqlCH/vgvLPWUZI8JpDb9LOAo6+P2gX8jhVAdZbWp3YcQaH2gAvtmJFyZb WPwjdcFDGcFpREzTPfqiV2HST5cfWy+X6M65jEhCYKpF53PRo63gO/J4CDuFZpPI2tCF1qkE HHydozCVe1fRjiVJ5pZkzEeT7XpYIg8zw2vuRKyn6JmI/DO92sTso/5yNl4+sXckBgz8Xp/C MHLgDLFdH19gm5dH2x+56t4u0Eokj9rsIB9iv1cT5lI4u9RFx09PtjaxvB7DNb7XkTAeM2IQ RCoWIbuGik/G/Q2xdJGeENhA5O6lBmWxyunGaUY0beMGYYo86/B93f0Lsd5jX3B0fpplEEoF /NGLnbunatj707WDo/NnV+ekvOydKkGxiOL/2Ce13aPsVxwXwt5UKGDVncaNQPNtdqswETEQ ve1DKg/dAtMzcnXMqxRdtjglklLXt/mMdXaJnqzwiK+WE7OybSLY47nPW4a2U0xEWAilAYet TaDPAk6XGK6pn7GSSZpHhTpal/t9u93rDW6SFU1xkeEdR8p0b394RMTifGGLpFblrsZpCcsr Sl1F1ehzprXDdSHvQ9oYKRbZ5s0/l5G0WvTswE1MIanKuhugVsXcgI/uE2LtV0/EoRNi9In6 ngt0RBuKK+F+FxEfjKcm5v3P/yfK2X/+gyud7+DwkvXg7P0su8E7PU1rUmmvRn8TBJztSU6l YMMjT3BvsavbkJaS5/6X0cp+gIvorjbZnN4/IbIzTh2NqLytDbe2tUvDe9jyxC6ft4ZPrnXc W26W8AcGcWqL/Qn3lazaRdRdvhT+bQuMoWtcOacxK+mIc5vmTuniSJM54U3gSfuv2JsD/XF2 ZoI2aTSxgqKTS3xylymr9rrmI1ZTT4XF2u7jyPjAcQCA886NZZOAmCoLcqtw9x4jJO4QH9U+ mmoAFYe0dOocx6fB7Dk9TVZzl9f4XmumC/iiidxjylstK2UmirH3+XlchMDfG9NXmhry1n2c 8C4iNUTXU7gaAZM9lPt/Uf33bJW4q94MnPPQEpVVyfzJmBmFKC3s/KObtVO55UhrShMGL7kM BbKF/in+kVcjnurFnA7pnhzbzywv5TlgxF2wHmQKnp+tjuReM19wwve+M2JQPdQ2jQcQywrw TLTB1W6I5yo5YDOz8aF4r34DTv/EMALIkyJhcuauSC25HNnG0i6lvG3wJj8FBQilDX83J9sX DnJqxD1Zs/q0b67OKRpZBoNZhe05sxkF4V5ioZ1iosX3C1QnpSY52AK12z0LM9H2K/jRHUIT D8PhdXS5UK2vS8rZmLM3I//WniHl4F5ZtSgeG5Q0SUg9dxLBbq847lNnC8zqV2951G0A7A1j nIWzv0g72QfiucCtV82zymTNbsVGFFRIS3mkxnbp8D7tqhcY3yjNKShzEcr1870F6mM+0sPP RSxModnByJ76d9zdU7BwGGmoJ+xY8HeNJoSrkHGyEqG1rkNbshtybxSwnA7cWPl4S97l6hh1 kcohM/i+tDAcjQInurxAwYEZGOrIZpLoHe1y/4ZxJ7e3pjzTMs/XG9XDd24FbTwV2hK/fX/a 1TRSntl9jHCSOCZRUjGuCIE5zrOC8z5aC3RfSNEi40kHF7EegRemFxGBW1q2MdmSUb6gpSmK h4x5yhNtAen8V0Vm74ub1+nFT6BwWXgIjYsFMrFdEsQvlwEvh2Fd5TZt707HjkErMf48krQe irCNl4OVSZQCwSFHwyxZODwo4Oboq7DXKzmaKKfBNfG4fpXU/PCrX62+q1h+TvEdsCGP304S uY+xlIGR3dyXcLQhzQITSUT0SPLdc+S4hmmqGVxqYik/fLnVRiKh8PHAqZOMdhp5xG9gLuSf ++WiiFjLD9E15QKjXbWwbkb1VQWhmlgbT6oWbgHsCfMSurXlMo1R1YDbDhvMcJT868m9gxEO MqektGsk7Al1rg6DFBKUVGnkcasJIQLL2y7KFLbFROLObCBdlipi4n8ZaKxT6EVjf0B7UXh/ 2bGVRW6YHLez2qMNVjnK+xHgSCFMQYLvYi8dkwoEm3/VJf8bRb9NtZrjDowyLlyh3XQNGdaP yIvFiEF5rCW8y5che1yXmJb6X8wZ/GFljyD4q/TLYsMrfpmHwx7kutb5DIxzL4fv0QmDLRl3 TDfqNJjuQTsiu6U1j9uSwZDsB5OjYOP+F1gYODXq8EGVnHD8xYAq26XDl5ZwrktQs2qsKdWx N/Vkav1IzoX6NPY8/wXAM3MId6GOn4sWfIMMDHRBQoBCzWsMDOH76S8uPSb93nQtppj75axw NwBTbhUUFFzHfQfWBwN9DMqL5J+Xzdimrme3pdg2A==
  • Ironport-sdr: 66349062_BjhyYs6Z2qTDJ5nXQHfat/Jt3ETpJnX51/fGevDA/ZPbtCf sfqNxDm0H7NVxN8yUA5TmIDw7nibstsil5X7AkA==


Le ven. 3 mai 2024 à 08:29, Elias Castegren <elias.castegren AT it.uu.se> a écrit :


Maybe there are other tricks one can employ to solve the
same problem? My goto solution is using well-founded
induction over some size measure, but it always involves
some boilerplate that would be nice to avoid.

I guess the standard solution would probably be two mutual induction principles: one for rose_tree and one for list of rose_tree. And you prove mutual lemmas too.


Cheers

/Elias




Archive powered by MHonArc 2.6.19+.

Top of Page