(* We take the same approach to or_introl and or_intror as with conj; they're tags and they're functions. *) Check or_introl. (* or_introl takes two types as arguments, and then a proof of just one of the types. *) Print Implicit or_introl. (* Since you supply an argument of type A, the type itself is implicit. *) (* or_intror is symmetrical. *) Check or_intror. Print Implicit or_intror. (* We can write a match statement, constructing a proof of True \/ O <= O by proving the right-hand side. *) Check ( match (@or_intror True (O <= O) (le_n O)) with | or_intror r => I | or_introl l => I end). (* Note that we must supply both constructors in the match statement, even though we "know" that the tag of the argument is or_intro. *) (* Let's do maximal structural induction on OR. *) (* We start out in the same way as AND. *) (* forall (A B : Prop), .... *) (* What is the type of P? *) (* forall (A B : Prop) (P : forall (Z : A \/ B), Prop), .... *) (* How many principal premises are there? 2, one for each constructor. *) (* forall (A B : Prop) (P : forall (Z : A \/ B), Prop), (forall (a : A), P (or_introl B a)) -> (forall (b : B), P (or_intror A b)) -> forall (Z : A \/ B), P Z *) (* Now, we go ahead and prove it. *) Goal forall (A B : Prop) (P : A \/ B -> Prop), (forall (a : A), P (or_introl B a)) -> (forall (b : B), P (or_intror A b)) -> forall (Z : A \/ B), P Z. Proof. intros. (* let's do it explicitly. Note that we must help the type-checker with type annotations. *) refine ( match Z as Z0 return P Z0 with | or_introl l => _ : P (or_introl B l) | or_intror r => _ : P (or_intror A r) end). auto. auto. Qed. (* We can check it. *) Scheme or_ind' := Induction for or Sort Prop. Print or_ind'. (* Here we prove a simple propositional tautology. *) Goal forall (A B C : Prop), ((A -> B) \/ (A -> C)) /\ A -> (B \/ C). Proof. intros. auto. (* again, auto fails. *) induction H. (* We just did induction with and_ind, yielding a single subgoal. *) induction H. (* Induction or_ind yields two subgoals. *) (* In the first subgoal, we want to prove the left hand side. This corresponds to the or_introl constructor. *) apply or_introl; auto. (* In the second subgoal, we want to prove the right hand side. this corresponds to the or_intror constructor. *) apply or_intror; auto. Qed. (* We'll try this goal once again. Using a few specialized tactics. *) Goal forall (A B C : Prop), ((A -> B) \/ (A -> C)) /\ A -> (B \/ C). Proof. intros. induction H. induction H. (* left is a tactic that works on any inductive definition with just two constructors, selecting the first. *) (info left); auto. (* right does the same, but selects the second constructor. *) (info right); auto. Qed. (* split only works for inductive datatypes with one constructor. left, right only work for inductive datatypes with two constructors. *) (* There are is a tactic more general than left, right, or split: constructor. We solve the same proof again, using constructor. *) (* We'll try this goal once again. Using a few specialized tactics. *) Goal forall (A B C : Prop), ((A -> B) \/ (A -> C)) /\ A -> (B \/ C). Proof. intros. induction H. induction H. (* constructor 1 selects the first tactic, the same as left. *) constructor 1; auto. (* constructor 2 selects the second constructor. *) (constructor 2); auto. Qed. (* There is a degenerate version of constructor that applys the constructors in order until one fits. *) Goal forall (A B C : Prop), ((A -> B) \/ (A -> C)) /\ A -> (B \/ C). Proof. intros. induction H. induction H. (* constructor selects the first constructor, which is correct, so auto succeeds. *) info constructor; auto. (* for this goal, constructor will still select the first constructor, yielding an impossible goal. *) constructor; auto. Admitted. (* It turns out that there is a simple automation specialized to AND and OR, tauto. *) (* We can try to solve the above goal again using tauto. *) Goal forall (A B C : Prop), ((A -> B) \/ (A -> C)) /\ A -> (B \/ C). info tauto. (* Note that tauto followed a similar approach to ours. (elim is a primitive induction tactic.) *) Show Proof. Qed. (* Actually, tauto is not specialized to AND and OR. It solves goals that are isomorphic to goals constructed from AND and OR. *) (* Solving the following goal using auto and using tauto will illustrate their differences. *) Goal (2 <= 3 /\ 2 <= 4) -> 2 <= 3. info tauto. Qed. Goal (2 <= 3 /\ 2 <= 4) -> 2 <= 3. info auto. Qed. (* In the first solution, tauto used the hypothesis to prove the conclusion. In the second auto proved the conclusion directly. *) Require Import Arith. (* Here's a goal that can't be proved by either tactic. *) Goal forall n m, n <= m /\ m <= n -> m = n /\ True. auto with arith. (* Unlike auto, tauto fails if it doesn't solve the goal. Here we wrap tauto with the try tactical, to avoid failure. *) try tauto. (* If we destruct the conjunction in the hypothesis, auto will prove the conclusion. *) intros. induction H; info auto with arith. Qed. (* What we need is tauto's smarts with conjunctions and disjunctions, and auto to handle the rest. We can get this using the intuition tactic. *) Goal forall n m, n <= m /\ m <= n -> m = n /\ True. Proof. info intuition. (* intuition destruct the hypothesis and then applies auto with all loaded databases. *) Qed. (* not is not nearly so interesting as AND and OR. *) Print not. (* not A is just shorthand for A -> False. *) (* It's only defined for Props. You can't say not (nat), but you can say nat -> False. *) Check (nat -> False). (* There are some facts about not in the core database. *) Print Hint not. (* We prove something goofy. *) Goal not(False). Proof. info auto. Show Proof. Qed. (* We can easily come up with a goal which can't be solved by auto, tauto, or intuition. *) Goal forall (n m : nat), n <= m /\ n <> m -> (n < m /\ True). Proof. auto with *. try tauto. (* Note that intuition changes the goal even if it can't prove it. It also managed to solve one of our two subgoals. *) info intuition. Show Proof. (* Here we do some magic... *) destruct (le_lt_eq_dec n m H0). auto. (* contradiction is a simple tactic. If you have a proof of P and a proof of ~ P, it uses them to prove False. Then, it uses False to prove your goal. *) info contradiction. Qed. (* We can not prove forall (A : Prop), not A \/ A. Constructive logic excludes the law of the excluded middle. *) (* But we can prove specific instances by proving one or the other. *) Goal (True \/ not (True)) /\ (False \/ not (False)). Proof. info intuition. Show Proof. Qed. (* Classical logic can be encoded in constructive logic. *) Require Import Classical. Print Classical_Prop. (* The law of the excluded middle is an axiom in Classical_Prop. *) Print classic. (* Note that classic has no body, because it has no proof. *) (* Given classic we can go ahead and prove all sorts of facts impossible to prove in constructive logic. *) Goal forall (P : Prop), not (not P) -> P. Proof. intros. (* Here we specify an additional lemma to include with "using" *) (* Note that with the assert tactic, we can state and prove a mini-lemma. *) info assert (P \/ ~ P) by auto using classic. (* The proof now has a let binding corresponding to the proof of our mini-lemma. *) Show Proof. info intuition. Qed. (* We won't really talk a whole lot more about classical logic. *) (* We do notice that Coq does not prevent us from inserting unproven goals into our environment. *) Hint Resolve classic. (* Now we can use auto to prove LEM. *) Goal forall P, P \/ ~ P. info auto. Qed.