Module Shadow_Bool. Inductive bool : Type := | true : bool | false : bool. (* bool, bool_rect, bool_ind, bool_rec *) Check bool_ind. Definition andb (b1 b2 : bool) : bool := match b1 with | true => b2 | false => false end. Compute (andb true false). Example andb_true_false : andb true false = false. Proof. reflexivity. Qed. Check andb_true_false. Print andb_true_false. Definition andb_true_false' : andb true false = false := eq_refl. Definition and_same (b : bool) : (andb b b = b) := match b with | true => eq_refl | false => eq_refl end. Print and_same. Theorem and_same' : forall b, andb b b = b. Proof. intro b. case b. reflexivity. reflexivity. Qed. Theorem and_same'' : forall b, andb b b = b. Proof. intros b. case b. - reflexivity. - reflexivity. Qed. Theorem and_commutative : forall b1 b2, andb b1 b2 = andb b2 b1. Proof. intros b1 b2. case b1. - case b2. + reflexivity. + reflexivity. - case b2. + reflexivity. + reflexivity. Qed. Theorem and_commutative' : forall b1 b2, andb b1 b2 = andb b2 b1. Proof. intros b1 b2; case b1; case b2; reflexivity. Qed. Definition and_same_true := (and_same true). Check and_same_true. Theorem and_same_true': andb true true = true. Proof. apply (and_same true). Qed. Print and_same_true'. Theorem and_same_true'': andb true true = true. Proof. apply and_same. Qed. End Shadow_Bool. Module Shadow_Nat. Inductive nat : Set := | Z : nat (* Coq uses the letter O, alas *) | S : nat -> nat. (* Coq has special shorthand for predefined nats: 0, 1, 2... *) (* definition of recursive function *) Fixpoint plus (n : nat) (m : nat) : nat := match n with | Z => m | S n' => S (plus n' m) end. (* telling Coq about infix notation *) Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope. Fixpoint mult (n m : nat) : nat := match n with | Z => Z | S n' => plus m (mult n' m) end. Notation "x * y" := (mult x y) (at level 40, left associativity) : nat_scope. Fixpoint evenb (n:nat) : bool := match n with | Z => true | S Z => false | S (S n') => evenb n' end. (* We'll return to Nat after looking at logic. *) End Shadow_Nat.