coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Certified insertion

From: David Holland <dholland-coq AT netbsd.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Certified insertion
Date: Wed, 19 Dec 2018 18:08:19 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dholland-coq AT netbsd.org; spf=Pass smtp.mailfrom=dholland AT netbsd.org; spf=None smtp.helo=postmaster AT mail.netbsd.org
Ironport-phdr: 9a23:aN91/RO3GLC42sH37wUl6mtUPXoX/o7sNwtQ0KIMzox0LPXyrarrMEGX3/hxlliBBdydt6oUzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlLiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkJNzA37nzZhM9+jK1UvB2uuh5wzIDPbYGJKPZzZL/Rcc8ASGZfWMtaSixPApm7b4sKF+cPM/xXr5f8p1QTsBCwBw6sBOfryjBSgH/5wLAx3uM8HgHG2wwgG9YOv27SrNroLasdTee1zLDTwDXFcfxWxSzy6JPVfRw7pvGMR71wfNPXxEIyFA3Flk2dpZHhMj6RzOgBrWaW4uR6We6xlmIqqRt9riazysswjITCm5gbxUre9SpjxYY4Pd24R1B/Yd6jCJZQsjuVN4pyQs84RWFnpjo6xaYduZGmZiQKz44nxxHHZ/yGdYiH/A7jWf6MLTp8gH9pYqyzihi8/ES61OHwS8u53ExUoiZZjtXArnUN2AbS6siDRPt95ECh2TOX2g/O6uFEJkQ0la7BJJ4n37E9jZwTvlrfHiDtg0X5kbWadkI++uin8+jneKnppoeAN49ojQHzKrghmsumAeghLgcOW3Wb9v+n2b34/Uz5Ra1KgecsnqnYtpDaP8UbqbSjDw9byIZwoyq4WjyhyZETmWQNBFNDYhOOyYbzaH/UJ/WtIf6hgljksDBvw/nAMvW1DpXKKnzKlrukdrFkw0hR1AAowZZY/Z0CWeJJG+76RkKk7I+QNRQ+KQHhm7+2WuU47ZsXXCe0OoHcNarTtVGS4ed2ebuKaZMfozq7LOIqtae30S0J3GQFdKzs5qM5LWiiF608cUOUfXD3jpEGC2hY5lNjHtyvs0WLVHtoX1j3X6844WhkWoevDIOFQI2xiqeNmiChEc8Oaw==

On Sat, Dec 08, 2018 at 03:22:10PM +0100, Klaus Ostermann wrote:
> Definition sortedOf(l: list nat)(q: list nat) := Sorted q /\ forall m,
> In m l <-> In m q.

Another bit nobody's noted yet: this is not what you want as it allows
dropping or manufacturing duplicate elements. Use Permutation or
count_occ...

--
David A. Holland
dholland AT netbsd.org

[Coq-Club] Certified insertion, Klaus Ostermann, 12/08/2018
- Re: [Coq-Club] Certified insertion, Jason -Zhong Sheng- Hu, 12/08/2018
  - Re: [Coq-Club] Certified insertion, Xuanrui Qi, 12/08/2018
- Re: [Coq-Club] Certified insertion, Adam Chlipala, 12/08/2018
  - Re: [Coq-Club] Certified insertion, Klaus Ostermann, 12/08/2018
    - Re: [Coq-Club] Certified insertion, Xuanrui Qi, 12/08/2018
    - Re: [Coq-Club] Certified insertion, Jonathan Leivent, 12/09/2018
- Re: [Coq-Club] Certified insertion, David Holland, 12/19/2018