The Coq mailing list

[Nathaniel Yazdani <nyazdani AT cs.washington.edu>]

This great, exactly what we were looking for. Thanks for the information!

Best,

Nate

On Dec 19, 2017, at 2:55 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

A typical usage in my experience is illustrated in the following file of the CoRN library:

https://github.com/c-corn/corn/blob/ebe396ace242aebea59a2c831e9780c1d0655383/logic/Stability.v

It shows that double negation (DN) is a monad. 

Also note (in the above file) the following lemma (note that P is an arbitrary (possibly undecidable) proposition):

Lemma DN_decisionT (P: Type): DN (P + (P->False)).

Proof. firstorder. Qed.

Roughly speaking, if we have to prove propositions that are known to be stable (P is stable := (~~P) -> P), we can use the excluded middle principle in our constructive proofs.

Coq.Logic.Decidable.dec_not_not can be used to weaken a goal P to ~~P and thus enter the DN monad where it is possible to make cases on undecidable propositions (e.g. equality of functions of type nat -> nat)

The above file also shows that stability is closed under conjunction and universal quantification.

(Stability is not closed under disjunction or existential quantification. Intuitively, constructive proofs of those propositions have non-trivial extra information.)

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sun, Dec 17, 2017 at 8:17 PM, Nathaniel Yazdani <nyazdani AT cs.washington.edu> wrote:

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