(** To prove a result, we announce it as a Theorem or Lemma, with a name, as follows:
*)
Lemma Tautology1:
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 the 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).
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).
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.
intros H H0.
intro H1. (* or unfold not. intro H1 *)
apply H0.
apply H.
assumption.
Qed.
Theorem prop_026 : (~A /\ ~B) -> ~(A \/ (~A /\ B)).
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 definitioj 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; it checks if False is derivable
from the context and then closes *)
Qed.
Lemma ex_2c : ~~~A -> ~A.
Proof.
intros.
unfold not.
intros.
apply H. (* ~~~A is just (~~A) -> False *)
intro H1. (* forces Coq to consider ~~A as (~A) -> False; intros does not do this *)
contradiction. (* or apply H1 etc *)
Qed.
Lemma ex_2d : (A -> ~A) -> ~A.
Admitted.
Lemma prop_065 : (A /\ B) \/ ~B -> B -> (A /\ B).
Proof.
intros.
destruct H as [H1|H2].
- exact H1.
- contradiction.
Qed.
Lemma prop_014 : (~(A /\ A) -> (~A \/ ~A)).
Admitted.
Lemma ex_2e : (A -> B) -> (A -> ~B) -> A -> C.
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.
destruct (classic A).
- intros; assumption.
- intros; contradiction.
Qed.
(* Here we "chain tactics" ; 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_065b : (A /\ B) \/ ~B -> B -> (A /\ B).
Proof.
intros H H1.
split.
- destruct H as [Hl | Hr].
* destruct Hl; assumption.
* contradiction.
- assumption.
Qed.
(* 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)).
Proof.
intro H.
destruct (classic B); destruct (classic A).
- left. (* or right. also works *)
intros Ha. apply H. split; assumption.
- left.
intro Ha. contradiction.
- right.
intro Hb. contradiction.
- left. (* or right. also works *)
intro Ha. contradiction.
Qed.
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.
(* prop_104 without classical logic *)
Lemma prop_104_noc : (A \/ B) -> ~(~A /\ ~B).
Proof.
intros.
intro H0.
destruct H as [H1|H2].
- destruct H0 as [H3 H4].
contradiction.
- destruct H0 as [H3 H4].
contradiction.
Qed.
(* tricky; 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).
Proof.
(* We do the proof without classical *)
intro H.
(* Note that the only we we can prove false is by applying H.
This looks weird because then we have the prove the "stronger"
result, the one without the ~~. The point is that one can prove it from
its negation, which is now in the context as H *)
apply H.
intro H0.
destruct H0.
(* USING ASSERT, but I try to avoid assert, as Coq is a goal directed prover
assert (~A).
- intros H4. apply H. intros. assumption.
- assert False.
+ apply H1.
* assumption.
* apply H0. assumption.
+ contradiction.
*)
destruct H1. (* !! This says: we derive the goal from the False at the end of
~A -> ~ B. This leaves us with the goals to prove ~A and B *)
- intro H2. apply H.
intros;assumption.
- apply H0.
intro H2; apply H; intros; assumption.
Qed.
Lemma prop_082 : (A -> B) /\ (C -> D) -> (~B \/ ~D) -> (~A \/ ~C).
Proof.
(* As a matter of fact: you don't need Classical here *)
intros H H0.
destruct H as [Hl Hr]. (* you need to split the /\ in all cases *)
destruct H0 as [H1 | H2].
(* Now, ~ A follows from ~B and A-> B so we can choose *)
- left. intro Ha; apply H1. apply Hl; assumption.
- right. intro Hc; apply H2. apply Hr; assumption.
Qed.
(* A variant of De Morgan; you need classical logic here:
Require Import Classical.
*)
Lemma prop_106 : ~(~A /\ ~B) -> (A \/ B).
Proof.
destruct (classic A).
- left; assumption.
- intros.
destruct (classic B).
* right; assumption.
* destruct H0.
split; assumption.
Qed.
End Assorted.