coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Experiences using double-negation elimination (dec_not_not)

From: Nathaniel Yazdani <nyazdani AT cs.washington.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Experiences using double-negation elimination (dec_not_not)
Date: Sun, 17 Dec 2017 17:17:21 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=nyazdani AT cs.washington.edu; spf=None smtp.mailfrom=nyazdani AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-pg0-f54.google.com
Ironport-phdr: 9a23:wcI+yBEVYrWL0nmOLEybEp1GYnF86YWxBRYc798ds5kLTJ78osSwAkXT6L1XgUPTWs2DsrQY07OQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmCexbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT4l/27Yl8J+j6xVrgymqRFk2YHYfISVOeB+fq/Bf94XQ3dKUMZLVyxGB4Oxd5MBAPAdPeZYtYb9oVoOogW6BQKxBuzg0D5JiWLs0q080uQqDAbL3AogHt0UsXXbsc/6NKETUe2u0KbI1i/Pbv1M1jfm6IjIcxYhof6QXbJ3d8rd01cgGB7YjliJr4HuIjCb1vwVvmWZ4OdsT/+jh3Anpg1roTWiyN0gh4nGi44NyF3J9T91zJs3KNC4UkJ2YdGpHIFUuiyZMYZ9X9ksTHtyuCkgz70LoZ67czYOyJQg3xPfbuaIc4mM4h76TOaRLit0iGtreL+/iBu+60egyur7Vsm71FZFsDBJncXLtnAIzxDT686HReVh/kq52zuC2Brf5vxaLU00j6bWKJAszqQwm5ccqUjDGzX5mETyjK+YbEUk/e2o5vzhYrTmvJCdNpJ7hRv4MqQvgcGwHf84PhIAXmeB4uS81Lzj/Uv2QLVWif02lLPVv47HKsQGvqK5GRNa0p4/6xajCDeryMgXnX4eLF5cZB2Hi5XpNErVLfDjDfa/hkysny1xy/DHOL3hGJTNIWLZnLfvZ7Yuo3JbnQE01JVU449eIrAHOvP6HEHr5/LCCRpsFQWow+/hCdh5nrIXS26GBK7RZKXDuE2E7+QuC+KXIpAcozb8Lfc54PiogHMkzwxONZK11IcaPSjrVs9tJF+UNCLh

Hi,

Would anyone mind sharing past instances in which they’ve used constructive double-negation elimination (i.e., Coq.Logic.Decidable.dec_not_not) in a Coq proof? Either experience summaries or examples of proofs themselves (if you don’t mind sharing) would be much appreciated.

I’m working with several colleagues on an automated tool to assist with proof evolution. The tool works by analyzing proof terms, and we’ve noticed that the analysis is ineffective on terms produced by the omega tactic, due to its use of dec_not_not. We would like to gather examples of how dec_not_not is used in other kinds of proofs, so that we can design a more robust approach to handling it.

Thanks,

Nate Yazdani

[Coq-Club] Experiences using double-negation elimination (dec_not_not), Nathaniel Yazdani, 12/18/2017
- Re: [Coq-Club] Experiences using double-negation elimination (dec_not_not), Abhishek Anand, 12/19/2017
  - Re: [Coq-Club] Experiences using double-negation elimination (dec_not_not), Nathaniel Yazdani, 12/20/2017