3

For example, coq has in its standard library a Classical package with lemmas in classical logic such as ones that relate forall and exists (https://coq.inria.fr/library/Coq.Logic.Classical_Pred_Type.html).

My question is if there is any support like that in mathcomp or ssreflect itself. All I have found so far is a few definitions and lemmas in https://github.com/coq/stdlib2/blob/master/src/bool.v#L548

Thanks

Christian Altamirano
  • 31
  • 2

1 Answers1

5

I don't think there is anything along those lines in the basic mathcomp libraries. The closest might be the classically operator in ssrbool, which mimics classical reasoning in intuitionistic logic. However, the experimental mathcomp analysis library assumes classical axioms and has results like the ones you mentioned (https://github.com/math-comp/analysis/blob/master/theories/boolp.v).

Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39