coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] FMap with abstract data type

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] FMap with abstract data type
Date: Fri, 24 May 2019 17:35:41 -0700
Authentication-results: mail2-smtp-roc.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-io1-f54.google.com
Ironport-phdr: 9a23:5rZKGx0Jyht8FyP1smDT+DRfVm0co7zxezQtwd8Zse0SLPad9pjvdHbS+e9qxAeQG9mCsrQd0rWd6PuocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmSexbalvIBmrrwjduccbjIV/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF/g6xbrxChqRJxwIDafZ+bO+Zlc6zHYd8XX3BMUtpNWyFDBI63cosBD/AGPeZdt4TyqEEBoga/BQmpGejgySVHhnv33a0kyesqDAbL3BIhHt0UtHTUrcv1O70JXO+pyanI0C/PYO1L1jfg8YXFdA0qr/+LXbJ1a8XRyE8vGhvDjlqKrIzqISqZ2fgKs2eB8+VgVfijhHIgqwF0pDWk28QiipHRi44L1lzJ8T91zYU1KNGiVUJ2YN+pHIFQuiyVMYZ9X9ksTHtyuCkgz70LoZ67czYOyJQg3xPfbuaIc4mM4h76VeaRJip0iGtreL+/iBu+60egyur7Vsm71FZFsDBJncXLtnAIzxDT686HReVh/kq5xzqDywTe5vtHLE00j6bXNp8sz78qmpcTvknPBir2l1/3jK+SeEUk4O+o6+H/b7X4vJCTKo50igTkPqUvgMO/BeU4MhYUUGWA9+Wzyqbj/VHjTLpWi/02j7PVv47HKsQGvqK5GRNa0p4/6xajCDeryMgXnX4eLF5cZB2Hi5XpNErVLfDjDfa/hkysny1xy/DHOL3hGJTNIWLZnLfvZ7Yuo3JbnQE01JVU449eIrAHOvP6HEHr5/LCCRpsDQW4wuOvOtx5150XETaREKadMb3bmVSN+6QiL/TaN9xdgyr0N/Vwv62mtnQ+g1JIJfD1j6tSU2ixG7FdG2vceWDl04UKFHpMswYjHrSz1Q+yFAVLbnP3ZJoSozE2DIX8UNXGT4Gpxb2GhWK1Q8EQaWdBBVSBV3zvctfcAqZeWGepOsZk1wc8e/2kQo4l2wupsVammaVqNfaS8SgF85/vyYos6g==

Thanks! I will try that. Meanwhile, I was experimenting with a different approach.

I was able to define:

Module A_as_OT <: OrderedType.
  Definition t := A.
  Definition eq := Ae.
  ....

Using it I was able to do:

Module NM := FMapAVL.Make_ord(Nat_as_OT)(A_as_OT).
Definition NatMap := NM.MapS.t.

I was motived by the following comment from FMapInterface.v:

Finally, [Sord] extends [S] with a complete comparison function. For that, the data type should have a decidable total ordering as well.

Not sure if this would help me though.

Vadim

Vadim Zaliva

A button for name playback in email signature

CMU ECE Ph.D. candidate

Mobile/Signal/WhatsApp: +1(510)220-1060

On Fri, May 24, 2019 at 4:44 PM Jasper Hugunin <jasperh AT cs.washington.edu> wrote:

Here is how you can prove MapsTo'_A_proper:

[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