On Negation
Please consider the propositions automatically
proved in this file .
Some of these propositions do not require False-elimination and
can be considered as instances of theorems of minimal propositional logic.
The other propositions are proved with the help of tauto.
Please replace occurrences of auto with combinations of
intros, apply and assumption.
Proofs made initially with
tauto will be rewritten using unfold not, and
False and negation elimination.
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.