(** To prove a result, we announce it as a Theorem or Lemma, with a name, as follows:
*)
Lemma Tautology:
forall A B C:Prop, (A -> B -> C) -> (A -> B) -> (A -> C).
(* Then we give the proof using tactics; we are now in "proof mode"
We start with "Proof" but that's not mandatory *)
Proof.
intros.
apply H.
assumption.
apply H0.
assumption.
(*
The proof is now complete. It is saved for future use
with the command Qed. We can refer to this proof by the name we have given: Tautology
This ends the proof mode.
*)
Qed.
(* Here is the same proof with bulleting to improve the structure and make subgoals explicit *)
Lemma Tautology':
forall A B C:Prop, (A -> B -> C) -> (A -> B) -> (A -> C).
Proof.
intros.
apply H.
- assumption.
- apply H0. assumption.
(* See the files by Jules Jacobs on teh webpage for futher explanation *)
Qed.
Section Implication_Logic.
Variable A B C : Prop.
(* It is nicer to not quantify over A B C : Prop all the time but to keep
these global for a Section *)
(* TODO: use just intros apply assumption to prove the following *)
Lemma ex_1b : (A -> B) -> (B -> C) -> (A -> C).
Admitted.
Lemma ex_1c : (A -> A -> B) -> (A -> B).
Admitted.
Lemma ex_1d : (A -> B) -> (A -> A -> B).
Admitted.
End Implication_Logic.
Section And_Or.
Variable A B C : Prop.
Lemma prop_001 : (A /\ B) -> (B /\A).
Proof.
intro H.
destruct H as [H1 H2].
(* Also try
destruct H.
or
elim H.
intros H1 H2.
or
case H.
The primitive tactic is elim.
destruct does an intros immediately after the elim
destruct H as [H1 H2] does the intros with the given names; here [H1 H2]
describes the "intro pattern" for /\: we get two pieces of data,
H1:A and H2:B
*)
split.
- assumption. (* or: exact H2, in case you want to name the assumtion *)
- assumption.
Qed.
Lemma prop_001a : (A \/ B) -> (B \/ A).
Proof.
intro H.
destruct H as [H1 | H2].
(* Also try
destruct H.
or
elim H.
intros H1.
or
case H.
Here [H1 | H2] describes the "intro pattern" for \/: we get a case split,
as we get H1:A or H2:B.
*)
- right. assumption.
- left; assumption.
(* The ; is for "chaining" tactics. The second tactic is applied to _all_ goals
generated by the first tactic *)
Qed.
Lemma prop_001b : (A \/ B)/\C -> (A \/ B)/\(A\/C).
Admitted.
(* use just intros apply assumption destruct (or elim) split left right *)
Lemma prop_001bb : (A \/ B) /\ C -> (A /\ C) \/ (B /\ C).
Admitted.
Lemma prop_001c : (A \/ B -> C) -> (A -> C)/\(B -> C).
Admitted.
Lemma prop_035 : (A -> (B -> C)) /\ (A -> B) -> (A -> C).
Admitted.
End And_Or.
Section Negation.
Variable A B C : Prop.
(* The negation of A, "not A" [with notation ~A] is defined as A -> False,
where from False we can derive anything.
Type "unfold not" to unfold the definition of ~A into A -> False
and then you can apply your usual tactics *)
Lemma ex_2a : (A -> B) -> ~B -> ~A.
Proof.
Admitted.
Theorem prop_026 : (~A /\ ~B) -> ~(A \/ (~A /\ B)).
(* NB Theorem does the same as Lemma, it is just for you if you want to
distinguish between main results and auxiliary results*)
Proof.
intros.
intro H1.
(* Here we exploit that ~(A \/ (~A /\ B)) is just (A \/ (~A /\ B)) -> False
Coq does not automatically unfold this definition,
but when we say "intro H1" it does.
Try: "unfold not" to unfold the definition of ~ *)
destruct H1 as [H2|H3]. (* Note that A \/ ~ A /\ B means A \/ (~ A /\ B) *)
- destruct H as [H4 H5].
apply H4. (* remember that ~A is just A -> False *)
assumption.
- destruct H as [H4 H5].
destruct H3 as [H6 H7].
contradiction.
(* This simplifies things a bit; Coq tries to derive False in the present context and if
it succeeds, the proof is finished, as everything is provable from False *)
Qed.
Lemma ex_2c : ~~~A -> ~A.
Admitted.
Lemma ex_2d : (A -> ~A) -> ~A.
Admitted.
Lemma prop_065 : (A /\ B) \/ ~B -> B -> (A /\ B).
Admitted.
Lemma prop_014 : (~(A /\ A) -> (~A \/ ~A)).
Admitted.
Lemma ex_2e : (A -> B) -> (A -> ~B) -> A -> C.
Proof.
intros H1 H2 H3.
absurd B.
(* This says that B and ~B is derivable, and so we have False, from which anything follows *)
- apply H2.
assumption.
- exact (H1 H3). (* You don't just have to refer to variables,
but you can also destruct/apply/elim larger terms *)
(* Try typing "intuition" immediately after intros H1 H2 H3
intuition does some simple prop logic steps automatically *)
Qed.
End Negation.
Section Classical.
Require Import Classical.
(* It provides the axiom of excluded middle (amoung other things) *)
Check classic.
(* One way of using it in the proofs is by means of the elimination
rule for disjunction:
destruct (classic A)
*)
Variable A B C : Prop.
Theorem dn_law : ~~A -> A.
Proof.
destruct (classic A).
- intros; assumption.
- intros; contradiction.
Qed.
(* Here we "chain tactics". The ; is sequential composition,
t1 ; t2 means that t2 is applied to _all_ goals generated by t1 *)
Lemma prop_002 : (~A -> A) -> A.
Admitted.
Lemma prop_003 : (~A -> A) \/ ~A.
Admitted.
Lemma prop_025 : A -> (~B \/ (A /\ B)).
Admitted.
Lemma prop_021 : ~A \/ (B -> A).
Admitted.
(* This one can also be done without classical logic *)
Lemma prop_104 : (A \/ B) -> ~(~A /\ ~B).
Admitted.
(* This one is found tricky CAN ONLY BE DONE USING CLASSICAL LOGIC *)
Lemma prop_037 : ((A /\ B) -> C) -> ((A -> C) \/ (B -> C)).
Admitted.
End Classical.
Section Assorted.
Variable A B C D: Prop.
(* We do a bit of chaining and tactic combination in the next proof Try for yourself *)
Lemma prop_085 : ~((A -> (B \/ ~C)) /\ (B -> ~A) /\ (A -> C) /\ A).
Proof.
intro H.
destruct H as [H [H1 H2]].
(* Does the same as destruct H. destruct H1. destruct H2. *)
destruct H.
- destruct H2; assumption.
- apply H1.
+ assumption.
+ destruct H2. assumption.
- apply H.
destruct H2.
apply (H0 H2).
Qed.
(* Try the following one without classical logic *)
Lemma prop_104_noc : (A \/ B) -> ~(~A /\ ~B).
Admitted.
(* The following is tricky, but can be done without classical logic;
for now you may use classical logic by typing
Require Import Classical.
*)
Lemma prop_063 : ~~((~A -> B) /\ (~A -> ~B) -> A).
Admitted.
Lemma prop_082 : (A -> B) /\ (C -> D) -> (~B \/ ~D) -> (~A \/ ~C).
Admitted.
(* A variant of De Morgan; you need classical logic here:
Require Import Classical.
*)
Lemma prop_106 : ~(~A /\ ~B) -> (A \/ B).
Admitted.
End Assorted.