On Negation

Prove the following propositions:

~ False

forall P:Prop, ~ ~ ~ P -> ~ P

forall P Q:Prop, ~ ~ ~ P -> P -> Q

forall P Q:Prop, (P -> Q) -> ~ Q -> ~ P.

forall P Q R:Prop, (P -> Q) -> (P -> ~ Q) -> P -> R.

Some of these propositions don't need False-elimination; in these situations, show that these theorems are derived from some theorems of the minimal propositional logic.

Solution

See on_negation.v

Notes

Whenever False-elimination is not needed, we first proved some lemma in minimal propositional logic, then apply it to derive the statement we wanted to prove.
Please notice that all these results could be proved in one step : either by "unfold not; auto" if False-elimination is not needed, or by tauto in the other case.

Going home

Pierre Castéran