Define logic `clProp` for axiom-free classical logic + remove `pure_forall_2` from BI interface
This MR defines a new logic
clProp that embeds classical logic into Coq. It uses essentially the Gödel-Gentzen translation, so the propositions of
clProp are defined as the subset of
Prop propositions that are stable under double negation, and the pure, ∨, ∃ connectives of
clProp are defined using a double negation.
clProp is a BI, so this MR allows one to use the proof mode to carry out proofs in classical logic, without axioms! For example:
Lemma test_excluded_middle P Q : ⊢ P ∨ ¬P. Proof. iApply clProp.dn; iIntros "#H". iApply "H". iRight. iIntros "HP". iApply "H". auto. Qed. Lemma test_peirces_law P Q : ((P → Q) → P) ⊢ P. Proof. iIntros "#H". iApply clProp.dn; iIntros "#HnotP". iApply "HnotP". iApply "H". iIntros "HP". iDestruct ("HnotP" with "HP") as %. Qed.
clProp logic does not enjoy the BI law
(∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝. Therefore, I have removed this law from the BI interface, and factored it into a type class
BiPureForall. This follows the same pattern as we use for other properties that do not hold for all BIs.