(* ignore those first two lines *)
Section propositional_logic.
Variables A B C D: Prop.
(* a simple proof that A implies A
(implication is written "->")
*)
Goal A -> A.
Proof.
(* introduce an hypothesis and name it H *)
intro H.
(* use hypothesis named H *)
apply H.
Qed.
Goal A -> A.
Proof.
(* same thing, using name "a" instead of "H" *)
intro a.
apply a.
Qed.
(* more proofs about implications,
you just need the [intro] and [apply] tactics
*)
Goal A -> B -> A.
Admitted. (* TODO *)
Goal (A -> B) -> A -> B.
Admitted. (* TODO *)
Goal (A -> B) -> (B -> C) -> (A -> C).
Admitted. (* TODO *)
Goal (A -> B -> C) -> B -> A -> C.
Admitted. (* TODO *)
Goal (A -> B -> C) -> (A -> B) -> A -> C.
Admitted. (* TODO *)
(* conjunctions ("logical and") are written "/\" *)
Goal A -> B -> A /\ B.
Proof.
intro a.
intro b.
(* use the tactic [split] to prove disjunctions *)
split.
(* now there are two subgoals *)
apply a.
(* second subgoal *)
apply b.
Qed.
Goal A /\ B -> A.
Proof.
intro H.
(* use the tactic [destruct] to exploit disjunctions
H is the existing hypothesis
a and b are new names for its components
*)
destruct H as [a b].
(* only one goal, two hypotheses now *)
apply a.
Qed.
(* exercises about conjunction:
use [intro], [apply], [destruct] and [split]
*)
Goal A /\ B -> B.
Admitted. (* TODO *)
Goal A /\ B -> (B /\ A).
Admitted. (* TODO *)
Goal A /\ (B /\ C) -> (A /\ B) /\ C.
Admitted. (* TODO *)
Goal A /\ (A -> B) -> B.
Admitted. (* TODO *)
Goal (A -> B) /\ (A -> C) -> (A -> B /\ C).
Admitted. (* TODO *)
Goal (A /\ B -> C) /\ A /\ (A -> B) -> C.
Admitted. (* TODO *)
Goal (A /\ B -> C) -> A /\ B -> C.
Admitted. (* TODO *)
(* disjunctions ("logical or") are written "\/" *)
Goal A -> A \/ B.
Proof.
intro HA.
(* tactic [left] makes it possible to
chose the left hand-side branch of a
disjunction *)
left.
apply HA.
Qed.
Goal B -> A \/ B.
Admitted. (* TODO *)
Goal A \/ B -> (A -> C) -> (B -> C) -> C.
Proof.
intro H.
intro HAC.
intro HBC.
(* tactic [destruct] also makes it possible
to exploit disjunctions:
H is the name of the existing assumption
HA and HB are names for the two new components
they are separated by a bar (|) because they
correspond to two alternatives
*)
destruct H as [HA|HB].
(* now there are two subgoals *)
apply HAC, HA.
(* here we just closed the first subgoal,
the second remains *)
apply HBC, HB.
Qed.
Goal A \/ B -> (B \/ A).
Admitted. (* TODO *)
Goal A \/ (B \/ C) -> (A \/ B) \/ C.
Admitted. (* TODO *)
Goal A \/ A -> A.
Admitted.
Goal (A \/ (B -> C)) -> (A -> C) -> B -> C.
Admitted. (* TODO *)
Goal A /\ (B \/ C) <-> (A /\ B) \/ (A /\ C).
Proof.
(* <-> is a conjunction, we can just split it *)
split.
Admitted. (* TODO *)
Goal A \/ (B /\ C) <-> (A \/ B) /\ (A \/ C).
Admitted. (* TODO *)
(* some optimisations *)
Goal A -> B -> C -> (A /\ B).
Proof.
(* several hypotheses can be introduced at once, using [intros] *)
intros a b c.
split.
apply a.
apply b.
Qed.
Goal A -> B -> C -> (A /\ B).
Proof.
intros a b c.
split.
(* [assumption] search for a hypothesis that matches the goal *)
assumption.
assumption.
Qed.
Goal A /\ B -> A.
Proof.
(* destruction patterns can be given using [intros]
(with an 's', doesn't work with [intro]) *)
intros [a b].
assumption.
Qed.
Goal A \/ (B -> A) -> B -> A.
Proof.
(* idem, for disjunctions *)
intros [a|ba] b.
assumption.
apply ba. assumption.
Qed.
Goal A /\ B /\ (B -> C) -> A /\ C.
Proof.
(* patterns can be nested *)
intros [a [b bc]]. split.
assumption.
apply bc. assumption.
Qed.
Goal A -> B -> C -> (A /\ B).
Proof.
intros a b c.
(* semicolon (;) makes it possible to call a tactic on all generated subgoals *)
split; assumption.
Qed.
(* exercise: go back and shorten your proofs using these
possibilities *)
End propositional_logic.