Logical ConnectivesConjunctionBi-implication (Iff)DisjunctionFalsehoodTruthNegationInequality9 Logical ConnectivesLike its built-in programming language, Coq’s built-in logic is extremelysmall: universal quantification (forall) and implication (→) are primitive,but all the other familiar logical connectives—conjunction, disjunction, nega-tion, existential quantification, even equality—can be defined using just theseand Inductive.9.1 ConjunctionThe logical conjunction of propositions A and B is represented by the follow-ing inductively defined proposition.Inductive and (A B : Prop) : Prop :=conj : A → B → (and A B).Note that, like the definition of ev, this definition is parameterized; however,in this case, the parameters are themselves propositions.The intuition behind this definition is simple: to construct evidence forand A B, we must provide evidence for A and evidence for B. More precisely:1. conj e1 e2 can be taken as evidence for and A B if e1 is evidence for Aand e2 is evidence for B; and2. this is the only way to give evidence for and A B—that is, if someone givesus evidence for and A B, we know it must have the form conj e1 e2,where e1 is evidence for A and e2 is evidence for B.9.1.1 EXERCISE [F]: What does the induction principle and_ind look like?Since we’ll be using conjunction a lot, let’s introduce a more familiar-looking infix notation for it.Notation "A ∨ B" := (and A B) : type_scope.68 9 Logical Connectives(The type_scope annotation tells Coq that this notation will be appearingin propositions, not values.)Besides the elegance of building everything up from a tiny foundation,what’s nice about defining conjunction this way is that we can prove state-ments involving conjunction using the tactics that we already know. For ex-ample, if the goal statement is a conjuction, we can prove it by applying thesingle constructor conj, which (as can be seen from the type of conj) solvesthe current goal and leaves the two parts of the conjunction as subgoals to beproved separately.Lemma and_example :(ev 0) ∨ (ev 4).Proof.apply conj.Case "left". apply ev_0.Case "right". apply ev_SS. apply ev_SS. apply ev_0. 2The split tactic is a convenient shorthand for apply conj.Conversely, the inversion tactic can be used to investigate a conjunctionhypothesis in the context and calculate what evidence must have been usedto build it.9.1.2 EXERCISE [F]: Look at the proof of and_1 and prove and_2 in Logic.v.9.1.3 EXERCISE [FF]: Prove that conjunction is associative.Lemma and_assoc : forall A B C : Prop,A ∨ (B ∨ C) → (A ∨ B) ∨ C.9.1.4 EXERCISE [FFF]: Now we can prove the other direction of the equivalenceof even and ev:Lemma even_ev : forall n : nat,(even n → ev n) ∨ (even (S n) → ev (S n)).Notice that the left-hand conjunct here is the statement we are actually in-terested in; the right-hand conjunct is needed in order to make the inductionhypothesis strong enough that we can carry out the reasoning in the induc-tive step. (To see why this is needed, try proving the left conjunct by itselfand observe where things get stuck.)9.2 Bi-implication (Iff)The familiar logical “if and only if” is just the conjunction of two implica-tions.9.3 Disjunction 69Definition iff (A B : Prop) := (A → B) ∨ (B → A).Notation "A ↔ B" := (iff A B) : type_scope.9.2.1 EXERCISE [F]: Using the proof that ↔ is symmetric (iff_sym) as a guide,prove that it is also reflexive and transitive (iff_refl and iff_trans).Unfortunately, propositions phrased with ↔ are a bit inconvenient to useas hypotheses or lemmas, because they have to be deconstructed into theirtwo directed components in order to be applied. (The basic problem is thatthere’s no way to apply an iff proposition directly. If it’s a hypothesis, youcan invert it, which is tedious; if it’s a lemma, you have to destruct it intohypotheses, which is worse.) Consequently, many Coq developments avoid↔, despite its appealing compactness. It can actually be made much moreconvenient using a Coq feature called “setoid rewriting,” but that is a bitbeyond the scope of this course.9.2.2 EXERCISE [FF]: We have seen that the families of propositions MyProp andev actually characterize the same set of numbers (the even ones). Provethat MyProp n ↔ ev n for all n (MyProp_iff_ev in Logic.v). Just for fun,write your proof as an explicit proof object, rather than using tactics.9.3 DisjunctionDisjunction (“logical or”) can also be defined as an inductive proposition.Inductive or (A B : Prop) : Prop :=| or_introl : A → or A B| or_intror : B → or A B.9.3.1 EXERCISE [F]: What does the induction principle or_ind look like?Since A ∧ B has two constructors, doing inversion on a hypothesis oftype A ∧ B yields two subgoals.Lemma or_commut : forall A B : Prop,A ∧ B → B ∧ A.Proof.intros A B H.inversion H.Case "left". apply or_intror. apply H0.Case "right". apply or_introl. apply H0. 270 9 Logical ConnectivesFrom here on, we’ll use the handy tactics left and right in place ofapply or_introl and apply or_intror:Lemma or_commut0: forall A B : Prop,A ∧ B → B ∧ A.Proof.intros A B H.inversion H.Case "left". right. apply H0.Case "right". left. apply H0. 29.3.2 EXERCISE [FF]: Using the proof of or_distributes_over_and_1 as aguide, prove or_distributes_over_and_2.9.3.3 EXERCISE [F]: Prove the distributivity of ∨ and ∧ as an iff proposition(or_distributes_over_and).We’ve already seen several places where analogous structures can befound in Coq’s computational (Set) and logical (Prop) worlds. Here is onemore: the boolean operators andb and orb are obviously analogs, in somesense, of the logical connectives ∨ and ∧. This analogy can be made moreprecise by the following theorems, which show how to “translate” know-ledge about andb and orb’s behaviors on certain inputs into propositionalfacts about those inputs.Lemma andb_true : forall b c,andb b c = true → b = true ∨ c = true.Lemma andb_false : forall b c,andb b c = false → b = false ∧ c = false.Lemma orb_true : forall b c,orb b c = true → b = true ∧ c = true.Lemma orb_false : forall b c,orb b c = false → b = false ∨ c = false.9.3.4 EXERCISE [FF, OPTIONAL]: The proof of andb_true is given in Logic.v.Fill in the other three.9.4 FalsehoodFalsehood can be represented in Coq as an inductively defined propositionwith no constructors.Inductive False : Prop := .9.5 Truth 719.4.1 EXERCISE [F]: Can you predict what the induction principle