(* Today we discuss AND and OR. *) (* We can check out their definitions. *) Print and. Print or. (* Notice that they're located in the Logic library. *) Locate and. Locate or. (* AND and OR are fundamental enough that hints about them appear in the core database. *) Print Hint and. Print Hint or. (* First we try proving a conjunction. *) Goal (3 <= 5) /\ True. Proof. (* To prove a conjunction, we must prove both subgoals. We'll prove each of the resulting subgoals using auto, since there's nothing new about them. We separate the steps, so we can inspect the intermediat proof. *) apply conj. Show Proof. auto. auto. Qed. (* We can also use a special purpose tactic, split, to prove the same subgoal. *) Goal (3 <= 5) /\ True. Proof. (* split is a slightly general tactic that can be used to break up goals into there components. It works for conjunctions, but also for other inductive definitions with a unique constructor. We'll prove each of the resulting subgoals using auto, since there's nothing new about them. *) (info split); info auto. Qed. (* It turns out we can prove the whole thing using auto, since apply conj is in the core database and the subgoals are easily proved using auto. If the subgoals could not be proved, auto would fail. *) Goal (3 <= 5) /\ True. Proof. auto. Qed. (* Now we try to prove a disjunction using some basic tactics. *) Goal (2 <= 5) \/ False. Proof. (* Clearly we want to prove the left side of the disjuction. We assert our intention using or_introl. *) apply or_introl. Show Proof. (* Here we see that the first argument to or_introl is the type of the goal it is _not_ proving. *) auto. Qed. (* We'll prove this goal again, using slightly more general tactics. *) Goal (2 <= 5) \/ False. Proof. (* The tactic, left, is general, like split. It works for OR, but also for other inductive definitions with two constructors. left chooses the first constructor. The right tactic will always choose the second constructor. *) (info left); auto. Qed. (* We can actually prove the whole thing using auto, since apply or_introl is in the core hint database and the two subgoals are proved with auto. *) Goal (2 <= 5) \/ False. Proof. auto. Qed. (* AND has induction schemes in all three sorts; another exception to the Prop rule. *) Print and_ind. Print and_rect. Print and_rec. (* OR does not have three induction schemes; it's normal. *) Print or_ind. (* Let's check the type of conj. *) Check conj. (* Notice that it has four arguments, and our pattern matching uses only two. Why? *) (* Let's pretend that conj is overloaded. It's a function that builds an expression and it's a label. I don't know if this is true, but it makes the typechecking work so far. *) (* Some of the arguments are implicit, which means they can be inferred from subsequent arguments. *) Print Implicit conj. (* We are prohibited from supplying A and B to conj, because they're implicit. *) Check (conj I (le_n O)). (* Or we can use @. It's a note to Coq that says I'm going to supply all arguments, even if some are implicit. *) Check ( match @conj True (O <= O) I (le_n O) return True with | conj a b => a end). (* We can leave the implicit args out. *) Check ( match conj I (le_n O) return True with | conj a b => a end). (* What does structural induction on AND really mean? AND is not recursively defined. *) (* We take a break here and discuss well-founded induction. In particular, we construct the maximal induction principle. *) (* Our first hint, we can hold A and B constant throughout. *) (* forall (A B : Prop), ... *) (* What's the type of P, the thing that we're trying to prove. *) (* forall (A B : Prop) (P : forall (Z : A /\ B), Prop), .... *) (* OK, how many constructors do we have? *) (* Just one, so there's only one principle premise. *) (* forall (A B : Prop) (P : forall (Z : A /\ B), Prop), (forall (a : A) (b : B), P (conj a b)) -> forall (Z : A /\ B), P Z *) (* OK, let's prove it. *) Goal forall (A B : Prop) (P : forall (Z : A /\ B), Prop), (forall (a : A) (b : B), P (conj a b)) -> forall (Z : A /\ B), P Z. intros. (* We solve the rest explicitly. It's unnecessary to write a fixpoint. But it's necessary to include an as annotation to make sure that the type varies appropriately. *) refine (match Z as Z0 return P Z0 with | conj a b => _ : P (conj a b) end). auto. Qed. (* We use Coq to check that our maximal induction principle is correct. *) Scheme and_rect' := Induction for and Sort Type. Print and_rect'. (* AND is in Prop, so the induction principle we get by default is the minimal one. *) (* Note that type annotations are unnecessary. *) Print and_rect. (* We prove modus ponens. *) Goal forall (A B : Prop), A /\ (A -> B) -> B. intros. (* Note that auto is unsuccesful. *) auto. (* We do induction on the conjunction. *) induction H. auto. Qed. (* We can prove the same goal differently. *) Goal forall (A B : Prop), A /\ (A -> B) -> B. intros. (* We can apply H, relying on the apply to match H with it's one constructor and to select the appropriate argument, the second. *) apply H. Show Proof. (* We can apply H one more time, again relying on the apply tactic to do its own deconstructing. *) apply H. Show Proof. Qed. (* Note that we can rely on the apply tactic to its own destructuring only when the inductive type has only one constructor. The same approach with the following inductive type will fail. *) Inductive and2 (A : Prop) (B : Prop) : Prop := | conj1 : forall (a : A) (b : B), and2 A B | conj2 : forall (a : A) (b : B), and2 A B . Goal forall (A B : Prop), and2 A (A -> B) -> B. intros. (* applying H at this point will fail. However, we can proceed by induction. *) induction H; auto. Qed.