Currently I have to learn Coq and don't know how to deal with an or
:
As an example, as simple as it is, I don't see how to prove:
Theorem T0: x \/ ~x.
I would really appreciate it, if someone could help me.
For reference I use this cheat sheet.
Also an example of a proof I have in mind: Here for double negation:
Require Import Classical_Prop.
Parameters x: Prop.
Theorem T7: (~~x) -> x.
intro H.
apply NNPP.
exact H.
Qed.
NNPP
's type isforall p:Prop, ~ ~ p -> p.
, so it's cheating to use it to proveT7
. When you importClassical_Prop
you getAxiom classic : forall P:Prop, P \/ ~ P.
$\endgroup$apply classic.
solves your goal forT0
. $\endgroup$