(* Quiz time! I'll give you the name of an inductive type in Set, you tell me an identically structured type in Prop. *) Print Empty_set. Print unit. Print sumbool. Print sum. Print prod. Print sumor. Extraction sumbool. Extraction sum. Extraction sumor. (* sumbool, sumor, and sum all have the same structure as or, the only difference is how the types of the arguments to the constructors are restricted. *) (* We use even again today. *) Inductive even : nat -> Prop := | EvenO : even 0 | EvenS : forall n, even n -> even (S (S n)) . (* Recall that previously we used the partial type for our checkEven function. At that time, we wanted the checkEven function to represent all decision procedures, even those that check undecidable properties. Now we write a new checkEven that represents decision procedures for properties that are decideable. *) (* sumbool is a great return type for that. *) Print sumbool. (* We want to use the annotations for the specif scope. *) Require Import MoreSpecif. Open Scope specif_scope. Locate "Yes". (* Note that Yes now represents the first constructor of sumbool *) Locate "No". (* No represents the second constructor. *) Locate "Reduce". (* Reduce is also all about sumbool now. *) (* We want to stick with the left constructor meaning something positive. So A is the property even n. B is the property not even n. *) Definition isEven (n : nat) : { even n } + {not (even n) }. Hint Constructors even. refine (fix F (n : nat) : {even n } + { not (even n) } := match n as n0 return {even n0 } + { not (even n0) } with | O => Yes | 1 => No | S (S n) => Reduce (F n) end); info auto. (* After auto has handled the easy goals, we're left with goals that need inversion. *) red. intros H. inversion H. contradict _H. inversion _H. auto. Defined. (* This extracts to something reasonable if Left is true and Right is false. *) Extraction isEven. (* So now, we have a decision procedure that takes a natural number and returns either a proof that the number is even or that it is odd. How do we use it? *) (* We write a function to get it out. *) Definition sumboolOut (A B : Prop) (b : sumbool A B) : match b with | left _ => A | right _ => B end := match b with | left a => a | right b => b end. Goal even 1024. exact (sumboolOut _ _ (isEven 1024)). Qed. Goal not (even 1023). exact (sumboolOut _ _ (isEven 1023)). Qed. (* Exercise 1 : Define oddness for natural numbers. Write a decision procedure for evenness vs. oddness in the style of the isEven procedure above. Use any hints necessary so that the entire proof can be completed with auto. *) (* Exercise 2 : Do the same for the representation of positive binary integers. *) Require Import BinPos. Print positive.