(* 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. *)