coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] FMap with abstract data type

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] FMap with abstract data type
Date: Fri, 24 May 2019 11:50:44 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vzaliva AT cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-it1-f177.google.com
Ironport-phdr: 9a23:HdhSChAN1yVpPaI942u2UyQJP3N1i/DPJgcQr6AfoPdwSPvzpMbcNUDSrc9gkEXOFd2Cra4d0qyP6v6rADdZqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5vIBmssAndq8gbjYR/Jqs/1xfCv2dFdflRyW50P1yYggzy5t23/J5t8iRQv+wu+stdWqjkfKo2UKJVAi0+P286+MPkux/DTRCS5nQHSWUZjgBIAwne4x7kWJr6rzb3ufB82CmeOs32UKw0VDG/5KplVBPklCEKPCM//WrKiMJ/kbhbrQquqBJ/zYDaY5ybOuRica7GZ9wWWXBMU9xNWyBdAI6xaZYEAeobPeZfqonwv1QBogGjCgmtAePk1zxHiWXy3a07zeQuCxzN0Qs+H9MPqnvUqNT1NLkIXu2u0KbIyCjDY+lI1jjg9YjFaxYsquyCU7J3dMre00gvFwXdg1WWt4PkMSma1v4Rs2ia9OpvT+Svi3U9pw5tpTivw98gio/TiYIQ1F/I7Dl2wIEvKtKkSE53e8KrEJxVtyycKoB4QdsiTnl2tComzrAKo522cSgQxJg6xhPSauaLf5WK7x/hUuuaPC12i2h/eL2lgha/6UigxfP4VsmzyFtKqzBKktjItnwU1hzT9tWLRuJz/ku82zuC1Rrf6u5DIUAzmqrbL4AuzqQsmZoUtETPBi72mEPog6+Kbkgo5PSk5uD9brjlppKQLZJ4hwD/P6g0h8CyA+Y1PhALX2eB+OS80LPj/Vf+QLVPlvA2jLPWv43bJcQevKK4AhVa0oIi6xahFTiry9oZkmccLFJZYh6Ik43pO0zULP/mEPi/nkygkC13yPDeIr3hHpLNI2Dfn7fmZLZx8lJTyA4uzd9E/J9UEbEAIPfrWkDrrtDYDxk5Mxa1w+n9Etl92JkeCiqzBfqSN7qXuluV7MouJfONbckbomXTMf8gssDngX480W0Ueai31NNDdmKxGvV4Km2SZGeqj9scRzRZ9jEiRfDn3QXRGQVYYGy/Cvplt2MLTbm+BIKGfbiDxbmI3SO1BJpTPzwUFV2XDTHjcpjCVvsROnvLfp1R1wccXL3kcLcPkAm0vV6owL96aOfY539A7M+x5J1O/+TW0CoK23l0AsCaiT/fSmh1miYJW2Zz0vkg/gpyzVCM1aU+iPtdR4Re

I am trying to figure out how to use FMap with abstract data type and
equality. I need a map where the keys are natural numbers, but values belong to an abstract type A. I can assume that this type has an equality Ae which is decidable, and a strict ordering.

I will need to have an Equiv relation between two maps (backed up by
Ae for elements). Finally, I would like to be able to prove Proper
instances for basic operations, like:

Instance MapsTo_A_proper:
  Proper ((eq) ==> (equiv) ==> (equiv) ==> iff) (NM.MapsTo).

Instance find_A_proper:
  Proper ((eq) ==> (equiv) ==> (equiv)) (NM.find (elt:=A)).

It looks like the map needs to be abstracted over A using a module.
This post http://www.newartisans.com/2016/10/using-fmap-in-coq/ gives
some good intro but stop shorts from abstracting values. It also looks
like I will need to use Sord functor from FMapInterface. I feel
like all pieces are there but having difficulty putting it all
together. I have not been able to find any relevant examples. Could
somebody please point me in the right direction? Thanks!

—
Vadim Zaliva
CMU ECE Ph.D. candidate
Mobile/Signal/WhatsApp: +1(510)220-1060

[Coq-Club] FMap with abstract data type, Vadim Zaliva, 05/24/2019
- Re: [Coq-Club] FMap with abstract data type, Jasper Hugunin, 05/24/2019
  - Re: [Coq-Club] FMap with abstract data type, Vadim Zaliva, 05/24/2019
    - Re: [Coq-Club] FMap with abstract data type, Jasper Hugunin, 05/25/2019
      - Re: [Coq-Club] FMap with abstract data type, Vadim Zaliva, 05/25/2019
        
        Re: [Coq-Club] FMap with abstract data type, Jasper Hugunin, 05/25/2019
        
        Re: [Coq-Club] FMap with abstract data type, Vadim Zaliva, 05/25/2019