(* Eduardo Hermo Reyes *)
(* Coq built-in Logic *)
(* Example *)
(* Coq's built-in logic is very small.We will see how to use some tactics
to carry out standard forms of logical reasoning. *)
Example E1 : forall A : Prop, A /\ ~ A -> False.
Proof.
intros.
destruct H.
apply H0.
assumption.
Qed.
Check E1.
Example E2: 0*3 = 0 /\ 1+1 = 2.
Proof.
split.
reflexivity.
reflexivity.
Qed.
(* In Coq a proposition P is inhabited by its proofs. We will refer to such
inhabitants as proof term or proof object or evidence for the truth of P. *)
Check forall A : Prop, A /\ ~ A -> False.
Check E1.
(* The proof term for an implication P → Q is a function that takes evidence
for P as input and produces evidence for Q as its output. *)
Example E3: forall A B : Prop, A -> A \/ B.
Proof.
intros.
left.
assumption.
Qed.
Print E3.
Example Construct1: forall A : Prop, A -> ~~A.
Proof.
intros.
intro.
apply H0; assumption.
Qed.
Example Construct2: forall A : Prop, ~~~A -> ~A.
Proof.
intros.
intro.
apply H.
apply Construct1; assumption.
Qed.
(*
Example E4: forall A : Prop, ~~A -> A.
Proof.
intros.
*)
(* To prove a conjunction P /\ Q we must provide evidence for P and
evidence for Q *)
(* If conjunction is in our goals *)
Example E4 : forall A B : Prop, A -> B -> A /\ B.
Proof.
intros.
split.
assumption.
assumption.
Qed.
(* If conjunction is in our hypothesis *)
Example E5: forall A B : Prop, A /\ B -> B.
Proof.
intros.
destruct H.
assumption.
Qed.
(* To prove a disjunction P \/ Q, we must provide an evidence for
P and say that it is P you are giving evidence for, or an evidence
for Q *)
(* See Example E3 *)
Example E6: forall A B : Prop, A \/ B -> B \/ A.
Proof.
intros.
destruct H.
right.
assumption.
left.
assumption.
Qed.
(* Falsehood: False is a proposition for which there is no way to
give evidence. Which are the inhabitants of False? *)
Theorem False_implies_nonsense : False -> 2 + 2 = 5.
Proof.
intros.
inversion H.
Qed.
Theorem Ex_Falso_Loquequieras : forall A : Prop, False -> A.
Proof.
intros.
inversion H.
Qed.
(* inversion H breaks H nto each of its possible cases, and yields a subgoal
for each case. However, False has no inhabitant, so therefore there possible
subgoal *)
(* We can use False and -> for negation. The intuition for ~P is
that if we assume to have a proof of P then anything at all, even
False, follows from that. *)
Example E7: 2 + 2 <> 5.
Proof.
intro.
inversion H.
Qed.
(* True is rarely used. The intuition is that is trivial to give
an evidence *)
Example E8 : forall A : Prop, A -> True.
Proof.
intros.
trivial.
Qed.
Theorem T1 : ~ False <-> True.
Proof.
split.
intro.
trivial.
intro.
intro.
inversion H0. (* / assumption *)
Qed.
Theorem T2 : ~~False <-> False.
Proof.
split.
intro.
apply H.
apply T1.
trivial.
intro.
intro.
apply H0.
assumption.
Qed.