(* In the following sections dedicated to logic, you have to prove some basic propositions. Proving a theorem (or a lemma) is like definiting a function: actually, a proof is a proof-tree; a proof of A -> B (read: "A implies B") is a function with takes a proof of A (that is, a proof-tree whise conclusion is A) and returns a proof of B (that is, a proof-tree whise conclusion is B). It is perfectly possible to provide directly the body of such a theorem (e.g., fun a:A => etc.); however it is much more common and convenient to build the proof-tree in the interactive way. *) (** The [Admitted] command tells Coq that we want to give up trying to prove this theorem and just accept it as a given. This can be useful for developing longer proofs, since we can state subsidiary facts that we believe will be useful for making some larger argument, use [Admitted] to accept them on faith for the moment, and continue thinking about the larger argument until we are sure it makes sense; then we can go back and fill in the proofs we skipped. Be careful, though: every time you say [admit] or [Admitted] you are leaving a door open for total nonsense to enter Coq's nice, rigorous, formally checked world! *) Section Minimal_propositional_logic. (* For minimal propositional logic (i.e. logic using only only one connector: implication), you should use only the followig tactics: intro, intros, apply, exact and assumption. *) Variables P Q R S : Prop. Lemma id_P : P -> P. Proof. (* FILL IN HERE *) Admitted. Lemma id_PP : (P -> P) -> P -> P. Proof. (* FILL IN HERE *) Admitted. Lemma imp_dist : (P -> Q -> R) -> (P -> Q) -> P -> R. Proof. (* FILL IN HERE *) Admitted. Lemma imp_trans : (P -> Q) -> (Q -> R) -> P -> R. Proof. (* FILL IN HERE *) Admitted. Lemma imp_perm : (P -> Q -> R) -> Q -> P -> R. Proof. (* FILL IN HERE *) Admitted. Lemma ignore_Q : (P -> R) -> P -> Q -> R. Proof. (* FILL IN HERE *) Admitted. Lemma delta_imp : (P -> P -> Q) -> P -> Q. Proof. (* FILL IN HERE *) Admitted. Lemma delta_impR : (P -> Q) -> P -> P -> Q. Proof. (* FILL IN HERE *) Admitted. Lemma diamond : (P -> Q) -> (P -> R) -> (Q -> R -> S) -> P -> S. Proof. (* FILL IN HERE *) Admitted. Lemma weak_peirce : ((((P -> Q) -> P) -> P) -> Q) -> Q. Proof. (* FILL IN HERE *) Admitted. End Minimal_propositional_logic. Section my_propositional_logic. (* Here we redefine propositional logic over 2 given propositions Q and Q. *) Variables P Q: Prop. (* Conjunctions states that a proof of [P and Q] is a pair made of a proof of [P] and a proof of [Q] *) Inductive P_and_Q: Prop := P_and_Q_intro : forall (p:P) (q:Q), P_and_Q. (* Disjunction states that a proof of [P or Q] is either a proof of [P] or a proof of [Q]. Note that a proof of [P or Q]is tagged by a constructor, saying if we are in the first case or in the second. *) Inductive P_or_Q : Prop:= | P_or_Q_intro_left : forall (p:P), P_or_Q | P_or_Q_intro_right : forall (q:Q), P_or_Q. (* At the moment P and Q are fixed, so we need additional definitions for the symmetric propositions *) Inductive Q_and_P : Prop := Q_and_P_intro : forall (q:Q) (p:P), Q_and_P. Inductive Q_or_P : Prop := | Q_or_P_intro_left : forall (q:Q), Q_or_P | Q_or_P_intro_right : forall (p:P), Q_or_P. Lemma PQ_and_commut: P_and_Q -> Q_and_P. Proof. intro pq. destruct pq as [p q]. apply Q_and_P_intro. exact q. exact p. Show Proof. Qed. Lemma PQ_or_commut: P_or_Q -> Q_or_P. Proof. intro pq. destruct pq as [p | q]. apply Q_or_P_intro_right. exact p. apply Q_or_P_intro_left. exact q. Show Proof. Qed. (* Instead of [apply Q_and_P_intro], you can use the standard tactic [split], which actually means "apply the unique constructor". *) Lemma PQ_and_commut_tactic: P_and_Q -> Q_and_P. Proof. intro pq. destruct pq as [p q]. split; assumption. Show Proof. Qed. (* Instead of [apply Q_or_P_intro_left], you can use the standard tactic [left], which actually means "apply the first constructor", which happens to be the expected one (because [Q_or_P_intro_left] has a proof of [Q] as an argument -- note that [Q] is the left part of "Q or P". Another suitable tactic with the same meaning would be [constructor 1]. Similarly for [right], which stands for [constructor 2]. Tactics such as [split], [left], [right], [constructor i] are quite handy when you don't remember the nams of the constructor. *) Lemma PQ_or_commut_tactic: P_or_Q -> Q_or_P. Proof. intro pq. destruct pq as [p | q]. right. assumption. left. assumption. Show Proof. Qed. (** Standard propositional connectors are defined along the same lines, but with P and Q as parameters for the sake of generality, and infix notation for convenience. *) Print and. Print or. End my_propositional_logic. Section propositional_logic. (** Homework *) (** Hint: the negation of P, denoted by ~P, is a shorthand for P -> False *) (** where [False] is the empty inductive type in Prop *) Print not. (** You may use the tactics [intros], [apply], [assumption], [destruct], [left], [right], [split] and try to use tactic composition *) Variables P Q R S T : Prop. Print and. Lemma and_commut : P /\ Q -> Q /\ P. Proof. (* FILL IN HERE *) Admitted. Lemma or_commut : P \/ Q -> Q \/ P. Proof. (* FILL IN HERE *) Admitted. Lemma and_assoc : P /\ (Q /\ R) -> (P /\ Q) /\ R. Proof. (* FILL IN HERE *) Admitted. Lemma and_imp_dist : (P -> Q) /\ (R -> S) -> P /\ R -> Q /\ S. Proof. (* FILL IN HERE *) Admitted. Lemma not_contrad : ~(P /\ ~P). Proof. red. intro pnp. destruct pnp as [p np]. (* FILL IN HERE *) Admitted. Print or. Lemma or_and_not : (P \/ Q) /\ ~P -> Q. Proof. (* FILL IN HERE *) Admitted. Lemma not_not_exm : ~ ~ (P \/ ~ P). Proof. (* FILL IN HERE *) Admitted. Lemma de_morgan_1 : ~(P \/ Q) -> ~P /\ ~Q. Proof. (* FILL IN HERE *) Admitted. Lemma de_morgan_2 : ~P /\ ~Q -> ~(P \/ Q). Proof. (* FILL IN HERE *) Admitted. Lemma de_morgan_3 : ~P \/ ~Q -> ~(P /\ Q). Proof. (* FILL IN HERE *) Admitted. Lemma or_to_imp : P \/ Q -> ~ P -> Q. (* FILL IN HERE *) Admitted. Lemma imp_to_not_not_or : (P -> Q) -> ~~(~P \/ Q). (* FILL IN HERE *) Admitted. Lemma contraposition : (P -> Q) -> (~Q -> ~P). (* FILL IN HERE *) Admitted. Lemma contraposition' : (~P -> ~Q) <-> (~~Q -> ~~P). (* FILL IN HERE *) Admitted. Lemma contraposition'' : (~P -> ~Q) <-> ~~(Q -> P). (* FILL IN HERE *) Admitted. End propositional_logic. (* Now observe that the section mechanism discharges also the local variables P, Q, R, etc. *) Check and_imp_dist. (* Proofs about predicates. *) Section First_Order_Logic. Variable A : Set. Variables (P Q : A -> Prop) (R : A -> A -> Prop). Lemma forall_imp_dist : (forall x:A, P x -> Q x) -> (forall x:A, P x) -> forall x: A, Q x. Proof. (* FILL IN HERE *) Admitted. (** Equivalence, denoted by <->, is a shorthand for the conjunction of 2 implications *) Locate "_ <-> _". Print iff. Lemma forall_and_dist : (forall x, P x /\ Q x) <-> (forall x, P x) /\ (forall x, Q x). Proof. red. split. (* FILL IN HERE *) Admitted. Lemma forall_perm : (forall x y:A, R x y) -> forall y x, R x y. Proof. (* FILL IN HERE *) Admitted. Lemma forall_delta : (forall x y:A, R x y) -> forall x, R x x. Proof. (* FILL IN HERE *) Admitted. Print ex. (* Inductive ex (A : Type) (P : A -> Prop) : Prop := ex_intro : forall x : A, P x -> ex P *) (* The tactic [exists x] means [apply (ex_intro x)] *) Lemma ex_example : exists n: nat, n + n = 4. Proof. exists 2. reflexivity. Qed. Lemma exists_imp_dist : (exists x: A, P x -> Q x) -> (forall x:A, P x) -> exists x:A, Q x. Proof. (* FILL IN HERE *) Admitted. Lemma not_empty_forall_exists : forall a:A, (forall x:A, P x) -> exists x:A, P x. Proof. (* FILL IN HERE *) Admitted. Lemma not_ex_forall_not : ~(exists x:A, P x) <-> forall x:A, ~P x. Proof. (* FILL IN HERE *) Admitted. End First_Order_Logic. (* ###################################################################### *) (** * Proof by Rewriting *) Theorem plus_id_example : forall n m:nat, n = m -> n + n = m + m. (** Instead of making a completely universal claim about all numbers [n] and [m], this theorem talks about a more specialized property that only holds when [n = m]. The arrow symbol is pronounced "implies". Since [n] and [m] are arbitrary numbers, we can't just use simplification to prove this theorem. Instead, we prove it by observing that, if we are assuming [n = m], then we can replace [n] with [m] in the goal statement and obtain an equality with the same expression on both sides. The tactic that tells Coq to perform this replacement is called [rewrite]. *) Proof. intros n m. (* move both quantifiers into the context *) intros e. (* move the hypothesis into the context *) rewrite -> e. (* Rewrite the goal using the hypothesis *) reflexivity. Qed. (** The first line of the proof moves the universally quantified variables [n] and [m] into the context. The second moves the hypothesis [n = m] into the context and gives it the name [e]. The third tells Coq to rewrite the current goal ([n + n = m + m]) by replacing the left side of the equality hypothesis [e] with the right side. (The arrow symbol in the [rewrite] has nothing to do with implication: it tells Coq to apply the rewrite from left to right. To rewrite from right to left, you can use [rewrite <-]. Try making this change in the above proof and see what difference it makes in Coq's behavior.) *) (** **** Exercise: 1 star *) (** Remove [Admitted.] and fill in the proof. *) Theorem plus_id_exercise : forall n m o : nat, n = m -> m = o -> n + m = m + o. Proof. (* FILL IN HERE *) Admitted. (** [] *) (** We can also use the [rewrite] tactic with a previously proved theorem instead of a hypothesis from the context. *) Theorem mult_0_plus : forall n m : nat, (0 + n) * m = n * m. Proof. intros n m. rewrite -> plus_O_n. reflexivity. Qed. (** **** Exercise: 1 star *) Theorem mult_1_plus : forall n m : nat, (1 + n) * m = m + (n * m). Proof. (* FILL IN HERE *) Admitted. (** [] *) (* ###################################################################### *) (** * Case Analysis *) (** Of course, not everything can be proved by simple calculation: In general, unknown, hypothetical values (arbitrary numbers, booleans, lists, etc.) can show up in the "head position" of functions that we want to reason about, blocking simplification. For example, if we try to prove the following fact using the [simpl] tactic as above, we get stuck. *) Require Import tests_nat. (* beq_nat, ble_nat and evenb are now available *) Theorem plus_1_neq_0_firsttry : forall n : nat, beq_nat (n + 1) 0 = false. Proof. intros n. simpl. (* does nothing! *) Admitted. (** The reason for this is that the definitions of both [beq_nat] and [+] begin by performing a [match] on their first argument. But here, the first argument to [+] is the unknown number [n] and the argument to [beq_nat] is the compound expression [n + 1]; neither can be simplified. What we need is to be able to consider the possible forms of [n] separately. If [n] is [O], then we can calculate the final result of [beq_nat (n + 1) 0] and check that it is, indeed, [false]. And if [n = S n'] for some [n'], then, although we don't know exactly what number [n + 1] yields, we can calculate that, at least, it will begin with one [S], and this is enough to calculate that, again, [beq_nat (n + 1) 0] will yield [false]. The tactic that tells Coq to consider, separately, the cases where [n = O] and where [n = S n'] is called [destruct]. *) Theorem plus_1_neq_0 : forall n : nat, beq_nat (n + 1) 0 = false. Proof. intros n. destruct n as [| n']. reflexivity. reflexivity. Qed. (** The [destruct] generates _two_ subgoals, which we must then prove, separately, in order to get Coq to accept the theorem as proved. (No special command is needed for moving from one subgoal to the other. When the first subgoal has been proved, it just disappears and we are left with the other "in focus.") In this case, each of the subgoals is easily proved by a single use of [reflexivity]. The annotation "[as [| n']]" is called an "intro pattern". It tells Coq what variable names to introduce in each subgoal. In general, what goes between the square brackets is a _list_ of lists of names, separated by [|]. Here, the first component is empty, since the [O] constructor is nullary (it doesn't carry any data). The second component gives a single name, [n'], since [S] is a unary constructor. The [destruct] tactic can be used with any inductively defined datatype. For example, we use it here to prove that boolean negation is involutive -- i.e., that negation is its own inverse. *) Theorem negb_involutive : forall b : bool, negb (negb b) = b. Proof. intros b. destruct b. reflexivity. reflexivity. Qed. (** Note that the [destruct] here has no [as] clause because none of the subcases of the [destruct] need to bind any variables, so there is no need to specify any names. (We could also have written "[as[|]]".) In fact, we can omit the [as] clause from _any_ [destruct] and Coq will fill in variable names automatically. Although this is convenient, it is arguably bad style, since Coq often makes confusing choices of names when left to its own devices. *) (** **** Exercise: 1 star *) Theorem zero_nbeq_plus_1 : forall n : nat, beq_nat 0 (n + 1) = false. Proof. (* FILL IN HERE *) Admitted. (** [] *) (* ###################################################################### *) (* Bullet proofs *) (** It is recommended to organize your proofs using "bullets": whenever a tactic yields several subgoals, each of them will be solved independently. It is good practice to separe them using bullets (dashes) and proper indententation. See next example. The effect of a bullet is to focus the construction of the proof on the first subgoal by hiding the other subgoals at the same level. Remaining subgoals will reappear when the current subgoal is completed. See next example. The structure of a proof with a single bullet level is then: Proof. tactic. tactic tactic.... tactic (* here 2 subgoals are produced *) - (* 1st subgoal *) tactic... tactic... - (* 2nd subgoal *) tactic... tactic... *) Theorem andb_true_elim1 : forall b c : bool, andb b c = true -> b = true. Proof. intros b c e. destruct b. - reflexivity. - rewrite <- e. reflexivity. Qed. (** Another way to provide structure: using brackets. *) Theorem andb_true_elim1_brackets : forall b c : bool, andb b c = true -> b = true. Proof. intros b c e. destruct b. { reflexivity. } { rewrite <- e. reflexivity. } Qed. (** A subgoal can itself be split into several subgoals, then bullets can be nested. Bullets can have different names: -, + , or * Bullets at the same level must have the same name. Bullets at different levels must have diffeerent names. The structure of a proof with two bullet levels is for instance: Proof. tactic. tactic tactic.... tactic (* here 2 subgoals are produced *) - (* 1st subgoal *) tactic... tactic... tactic (* here 3 subgoals are produced *) + (* 1st subsubgoal *) tactic... tactic... tactic + (* 2nd subsubgoal *) tactic... + (* 3rd subsubgoal *) tactic... - (* 2nd subgoal *) tactic... tactic... Another presention with brackets is: Proof. tactic. tactic tactic.... tactic (* here 2 subgoals are produced *) { (* 1st subgoal *) tactic... tactic... tactic (* here 3 subgoals are produced *) { (* 1st subsubgoal *) tactic... tactic... tactic } { (* 2nd subsubgoal *) tactic... } { (* 3rd subsubgoal *) tactic... } } { (* 2nd subgoal *) tactic... tactic... } Bullets and brackets can be used together, for example: Proof. tactic. tactic tactic.... tactic (* here 2 subgoals are produced *) - (* 1st subgoal *) tactic... tactic... tactic (* here 3 subgoals are produced *) { (* 1st subsubgoal *) tactic... tactic... tactic } { (* 2nd subsubgoal *) tactic... } { (* 3rd subsubgoal *) tactic... } - (* 2nd subgoal *) tactic... tactic... *) (** **** Exercise: 2 stars *) (** Prove [andb_true_elim2], marking cases (and subcases) when you use [destruct]. *) Theorem andb_true_elim2 : forall b c : bool, andb b c = true -> c = true. Proof. (* FILL IN HERE *) Admitted. (** [] *) (** There are no hard and fast rules for how proofs should be formatted in Coq -- in particular, where lines should be broken and how sections of the proof should be indented to indicate their nested structure. However, if the places where multiple subgoals are generated are marked with bullets placed at the beginning of lines, then the proof will be readable almost no matter what choices are made about other aspects of layout. This is a good place to mention one other piece of (possibly obvious) advice about line lengths. Beginning Coq users sometimes tend to the extremes, either writing each tactic on its own line or entire proofs on one line. Good style lies somewhere in the middle. In particular, one convention (not just for Coq proofs, but arguably for all programming!) is to limit yourself to 80 character lines. Lines longer than this are hard to read and can be inconvenient to display and print. Many editors have features that help enforce this. *)