(** 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.