Add classic logic operators

[NotBad4U]

Hi!

This PR adds the classic logic operators and some basic lemma.

However, I have a little problem with this lemma:

opaque symbol ∀ᶜᵢ p : (Π x, πᶜ (p x)) → πᶜ (∀ᶜ p) ≔
begin
  assume p Hnnpx Hnnnpx;
  apply Hnnnpx;
  assume x Hnnp;
  apply Hnnpx x;
  assume Hnp;
  apply Hnnp;
  apply Hnp
end;

I got the warning below when I ran make preventing creating the Classic.lpo

Writing "/Users/alessiocoltellacci/Projects/Inria/lambdapi-stdlib/Classic.lpo" ...
Uncaught [File "src/core/sign.ml", line 182, characters 16-22: Assertion failed].

[fblanqui]

Because of the use of the opaque command, this PR can only work with the next release of lambdapi. This should be reflected in the opam file.

[fblanqui]

I am wondering: why not having 2 files:

1. one file stating the axiom of excluded middle and the properties of connectors in this context (De Morgan laws), so not using the ᶜ exponent.
2. one file showing that classical logic can be encoded in intuitionistic logic using double negation?

[NotBad4U]

I am wondering: why not having 2 files:

1. one file stating the axiom of excluded middle and the properties of connectors in this context (De Morgan laws), so not using the ᶜ exponent.
2. one file showing that classical logic can be encoded in intuitionistic logic using double negation?

The file 1 will be the one used by the user ? Will this file contain only axiom symbols?
The problem that I discovered with my approach is that I can not use the rewriting rule on _ᶜ operator because they have a definition.
For example, a rule like rule πᶜ ($p ⇒ᶜ $q) ↪ πᶜ $p → πᶜ $q; could not be defined because ⇒ᶜ and πᶜ are defined symbols. So it makes proof in classical logic more verbose than the intuitionistic one with tactic because we need to use a combination of apply ⇒ᶜᵢ; assume h; where assume h; is enough for the intuitionistic ⇒ (similar problem with ∃ₑ that can act like an exists tactic 😄 ).

[fblanqui]

The file 1 will be the one used by the user ? Will this file contain only axiom symbols?

Yes.

Classic.lp:

require open Stdlib.Prop;
require open Stdlib.FOL;
require open Stdlib.Set;
symbol classic [p] : π (p ∨ ¬ p);
opaque symbol nnpp [p] : π (¬ ¬ p) → π p ≔ begin ... end;
opaque symbol pierce [p] : π ((p ⇒ ⊥) ⇒ p) → π p ≔ begin ... end;
opaque symbol imply_to_or [p q] : π (p ⇒ q) → π (¬ p ∨ q) ≔ begin ... end;
...

[fblanqui]

Hi @NotBad4U . This PR is not going to be merged as it is. Shouldn't I close it?

[NotBad4U]

Should we reopen a PR with the new version of the std-lib? Rebasing this work should not be hard but maybe not necessary.

[fblanqui]

I currently do not see the point of introducing the c-indexed versions of connectives in the stdlib.
If you require Classic, you can simply use the usual connectives.