Lemma ex_6_19 P : (~~P) <-> P. Universal_Intros. Split_Eq. P_with_CP. For P Use IP. For False Use (Contr H1 H2). P_with_CP. P_with_CP. For False Use (Contr H1 H2). Qed.
Hopefully this proof is easily read, but I'll walk through it anyway. We begin by introducing our universally quantified variable [P]. (Its good to note that even though I am doing Propositional logic, there is an implicit [forall] in the goal state.) After the introduction, we divide the bi-conditional, [<->], into two implications and begin the main body of the proof. For [~~P -> P], we'll need to use a conditional proof technique. The matching tactical is [P_with_CP]. From there the [For Use] syntax allows use to write a new hypotheses [~P] for [P] using the Indirect Proof [IP] tactical. Finally we'll show [False] using a contradiction between our two hypotheses, [~~P, ~P]. The other direction is immediate from the implication.
Ideally, a new student will be able to understand this language since it is very close to the language in their books. One area I am not a fan of is the lack of explication for some of the tacticals, [Univeral_Intros, Split_Eq, P_with_CP]. It might be a worthwhile addition to have the student also write out what those tactics are producing; this would be a similar behavior to the other tactics.
Well that's it for now, happy proving!
