(* The propositions True and False are some very fundamental inductive definitions. *) Locate True. Locate False. (* They are both defined in the Logic Library, which is a good deal more fundamental than the datatypes library. *) (* Let's print there definitions. *) Print True. (* There's only one rule for True, which we write on the board. *) (* Easy exercise: Prove True. *) Goal True. exact (I). Qed. (* We also develop the structural induction principle for True and now we prove it. *) Definition True_ind' : forall (P : True -> Prop), P I -> forall t : True, P t. (* We build the function header. *) intros P H. (* We fill in the rest explicitly. *) exact (fun t => match t with | I => H end). Defined. Print True_ind'. (* Note again the explicit annotation for match. Note also that this is as close to a tautology as one can get. Essentially, we're proving P I in order to prove P I. *) (* Now, how about False. *) Print False. (* At this point, we write the structural inductive principle for False and prove it. *) Definition False_ind' : forall (P : False -> Prop), forall (f : False), P f. intros. destruct f. Defined. Print False_ind'. (* The great thing about False is that it has no constructors. Since we don't need to match any constructors the type of the match statement can be anything. *) (* Proofs of False are very powerful because we can prove anything from False. *) Goal False -> 0 = 1. Proof. intros. destruct H. Qed. Print Unnamed_thm0. Goal False -> 0 = 1. Proof. apply False_ind'. Qed. Print Unnamed_thm1. (* The proof above is not so dangerous. In order to prove 0 = 1 we need a proof of False. But proofs of False can't be built from scratch. We'll see later how we can arrive at them by sneaky means. *) (* It is pretty easy to come up with inductive datatypes that are a lot like False. *) (* Take the one below. Just like False, it can't be inhabited because it has no ground constructors. *) Inductive none : Set := | Snone : none -> none. Goal none -> 0 = 1. Proof. (* The goal is a little harder to prove, because we need to use recursion. This makes sense, as the one constructor was recursively defined. *) exact (fix F n : 0 = 1 := match n with | Snone a => F a end). Qed. Goal none -> 0 = 1. Proof. apply none_ind. intros. exact H. Qed. (* Note that if we were able to construct a value of none this function would never terminate. *)