Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Recursion over indexed/mapped finite data structure

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Recursion over indexed/mapped finite data structure


Chronological Thread 
    < Chronological >      < Thread >
  • From: Christopher Ernest Sally <christopherernestsally AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Recursion over indexed/mapped finite data structure
  • Date: Mon, 24 May 2021 16:21:50 -0700
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=christopherernestsally AT gmail.com; spf=Pass smtp.mailfrom=christopherernestsally AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f173.google.com
  • Ironport-data: A9a23:b9rGI6KBPK4yPlnhFE+RopQlxSXFcZb7ZxGrkP8bfHDr1Wgk3jNRnzdMXDrSOaqDZzbxL9lwbozj8RtQuZWAm6c2QQE+nZ1PZyIT+JCdXbx1DW+pYnjMdpWbJK5fAnR3huDodKjYdVeB4Ef3WlTdhSMkj/jQG+CgULWs1h1ZHGeIdg9x0XqPpMZi2uaEsfDha++8kYuaT//3YDdJ6BYoWo4g0J9vnTs01BjEVJz0iXRlDRxDlAe2e3D4l/vzL4npR5fzatE88uJX24/+IL+FEmPxp3/BC/ugm7f/N0wOG/vcZFfVzHVRXKemj15JoSlaPqQTbqJNLxcKzWzXwZYol44lWZ+YEW/FOoXHmP4cSAVfCyFzJ6Bc/rLcPWO2tciC50LDenrohf5pCSnaOKVForcoWT4frqVwxDclN0jf3Ypa2omTQe51w88nMcPDJ5IaongmzDfDDP9gT4qrfklgzcsAiW122dQXSK6YP95DPGIpNkWROgkUbw9RVYZhyc62olL6VxFYjHOcg5Ytx1bS6RgoiO2xdIvBEjCRbcBcn0Ldp2afumqgXUpcO9uYxj6ItHmrg4fycerAcNp6PNWFGjRC2TV/B1D/CSH6kXO+qPi9z0+6ApdRchNPvCUpqqc2+QqgSdyVs9iQyJKblkZ0ZjaSO7RSBMKxJm787AOQB2xCRTlEADDjnNFjXiQkjzdlgPuwbQGCc9Sppba1+bKdrDf0Mi8QRYPHTUfoUiNdi+TeTEoPYt4jgzqt/GNZTjE4JN0o/w23kQ==
  • Ironport-hdrordr: A9a23:6GNGCqANFprk0QflHemk55DYdb4zR+YMi2TDGXoQdfUzSKClfqGV8cjzuiWatN98Yh8dcLO7UpVoI0msl6KdiLN5VdyftWLdyQiVxe9ZjLcKjweQfxEXpoZmpMJdT5Q=
  • Ironport-phdr: A9a23:FX2tKBTdybbyqslpDdxoat9OG9psohKfAWYlg6HPa5pwe6iut67vIFbYra00ygOQDMOBtKMP0reJ+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhMiTanf79/LhG7oQrMusQWg4ZpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhSwaNTA27XvXh9R/g6xbrhyvpAFxzZDIb4yOLvVyYrnQcMkGSWZdXMtcUTFKDIOmb4sICuoMJfhVr4nnp1sPthu+GQ6sBPvvyjBWnH/9wKI00/4nEQ7YxwwgA88FvmnOo9XxMKcTUf2+wa7UwjXDdfNW2Cz96JTPchA5ofGDQ6hwftTLyUkpCQzFlUmQqZf/MDOR0uQMs3OW7+VlVe21im4nrxt9rSSoxscpk4TEgJ8exV/Y+ytj2ok1OcG4R1BhYd6iCJZcqT+WOoprTs4+QmxlpTs3x7kItJO6cyUHzJYqyRDcZvGZcYWG4hDuWeSRLDp6mX5oe6yyiwus/UW+zuDxVMe53VBXpSRGitnBrm4B2wDX58SdSfZw/l2t1SuO2g3S8O1IPEI5mKTdJpU82LA/jIATvl7GHiLumEX5kquWdkI89+it8evnY7HmqoadN49wlw3yK6oultG9DOk2KAQOUG+b+eOz1L3n40L1WqlFjvozkqXBsZDaI9oUprKhDgNLzoou7wyzAjSm3dgCgHUKLVNIdAiag4XrNVzCOPX4Au2+g1Sonjdr3ffGPrj5D5rRLnjDirbhfa1h605b0Aozzc5Q54hKBbEbJvL8RFTxtMDDDhAjNwy0x+bmBc5y1oMbQ22PA6uZPLnOvl+P4+IjO/OMa5MNuDbhN/gl4ObjgmM+mV8EZKWmwZ8XaG2jEfl9OEWYYX/sgs8bHmsQvwo+SvbqiFyYXjJJaXayRfF02jZuA4W/SIzHW4rl1LeGxWKwGoBcTmFAEFGFV3nyIdaqQfAJPQmSOM56jjscVbW7A6I70xy1qEfBwr5jP6KA8S0CtIn/08B16vfejxc/7iBvBsCZwkmCSmh1miUDQDpgj/M3mlB01lrWifswuPdfD9EGv5uhvS81MJfdy6pxDNWgA2opn/+MQVeiB9SiWHQ/F41qhdAJZEl5FpOpiRWRh0JC5pcakrWKANo/9aeOhxDM
Hi Club

a finite data structure consisting of a map (from keys to elements) and elements that contain (along with their own data) a key to a successor element. Some elements have no successor key, indicating a kind of "endpoint", resulting in DAGs. (actually, control-flow graphs).

I want to write a recursive function over this data structure (but there is no naive/obvious decreasing struct). I could use a fuel based approach (# of elements as the bound) but wonder if that might hinder any proofs I would later want to do over the function. I have not worked much with Program before.

Do people have experience with this, and any insights to the way forward?

Bonus information:
In fact, I am working with RTL from CompCert. (CompCert's pass out of RTL is a validated pass i.e. the compiler code is in Ocaml and thus does not provide an example) and the function is a translation of RTL code.

Cordialement
Chris

Archive powered by MHonArc 2.6.19+.

Top of Page