Require Import CpdtTactics. (* what is the difference between Require and Require Import *) (****************** ENUMERATIONS ********************) Inductive T := E1 | E2 | E3. Check T_ind. Inductive Empty : Set := . Check Empty_ind. Theorem empty1 : Empty -> (2 + 2 = 5). Proof. induction 1. Qed. Definition empty2 (e : Empty) : 2 + 2 = 5 := match e with end. Inductive bool : Set := | true : bool | false : bool. Check bool_ind. Definition negb : bool -> bool := fun b => match b with | true => false | false => true end. Definition negb' : bool -> bool := fun b => if b then false else true. Theorem negb_ineq : forall b : bool, negb b <> b. Proof. destruct b; simpl. discriminate. discriminate. Qed. (****************** RECURSIVE TYPES ********************) Inductive nat : Set := | O : nat | S : nat -> nat. Check nat_ind. Check S. Inductive nattree : Set := | L : nat -> nattree | N : nattree -> nattree -> nattree. Check nattree_ind. Fixpoint plus (n m : nat) : nat := match n with | O => m | S n' => S (plus n' m) end. Theorem O_plus_n : forall n : nat, plus O n = n. Proof. intro; reflexivity. Qed. Theorem n_plus_O : forall n : nat, plus n O = n. Proof. induction n. - reflexivity. - simpl. rewrite IHn. reflexivity. Qed. Theorem S_inj : forall n m : nat, S n = S m -> n = m. Proof. (* intros n m H. injection H. intros. assumption. *) injection 1; auto. Qed. Theorem S_inj' : forall n m, S n = S m -> n = m. Proof. congruence. Qed. (****************** REFLEXIVE TYPES ********************) Inductive formula : Set := | Eq : nat -> nat -> formula | And : formula -> formula -> formula | Neg : formula -> formula | Or : formula -> formula -> formula | Forall : (nat -> formula) -> formula. Example forall_refl : formula := Forall (fun x => Eq x x). Example nat_deceq : formula := Forall (fun x => Forall (fun y => Or (Eq x y) (Neg (Eq x y)))). Fixpoint formulaDenote (f : formula) : Prop := match f with | Eq n1 n2 => n1 = n2 | And f1 f2 => formulaDenote f1 /\ formulaDenote f2 | Or f1 f2 => formulaDenote f1 \/ formulaDenote f2 | Neg f' => not (formulaDenote f') | Forall f' => forall n : nat, formulaDenote (f' n) end. Example forall_refl_proof : formulaDenote forall_refl. Proof. simpl. crush. Qed. (* Exercise: prove formulaDenote nat_deceq *) (* Inductive term : Set := | App : term -> term -> term | Abs : (term -> term) -> term. *)(* Inductive test : Set := t : ((nat -> test) -> nat) -> test. Inductive test : Set := t : ((test -> nat) -> nat) -> test. *) (****************** POLYMORPHIC TYPES ********************) Inductive list (T : Set) : Set := | Nil : list T | Cons : T -> list T -> list T. Implicit Arguments Cons. Check Cons. Check Nil. Check @list. Check Nil. Check Cons. Arguments Nil [T]. Arguments Cons [T] hd tail. Check Nil. Check Cons. About Cons. Fixpoint length {T} (ls : list T) : nat := match ls with | Nil => O | Cons _ ls' => S (length ls') end. Check @length. Check list_ind. Reset list. Section list. Variable T : Set. Inductive list : Set := | Nil : list | Cons : T -> list -> list. Fixpoint length (ls : list) : nat := match ls with | Nil => O | Cons _ ls' => S (length ls') end. Fixpoint app (ls1 ls2 : list) : list := match ls1 with | Nil => ls2 | Cons x ls1' => Cons x (app ls1' ls2) end. Theorem length_app : forall ls1 ls2 : list, length (app ls1 ls2) = plus (length ls1) (length ls2). induction ls1; crush. Qed. End list. Check app. (****************** INDUCTION PRINCIPLES ******************) Print nat_ind. Check nat_rect. Print nat_rect. Section nat_rect. Variable P : nat -> Type. Variable B : P O. Variable IH : forall (n :nat), P n -> P (S n). Fixpoint nat_rect' (n : nat) : P n := match n with | O => B | S n' => IH n' (nat_rect' n') end. End nat_rect. Reset nattree. Reset nat. Inductive utree : Set := | L : nat -> utree | N : list utree -> utree. Check utree_ind. (* this is quite useless *) Section utree_ind. Require Import Coq.Lists.List. Print Forall. (* Inductive Forall (A : Type) (P : A -> Prop) : list A -> Prop := Forall_nil : Forall P nil | Forall_cons : forall (x : A) (l : list A), P x -> Forall P l -> Forall P (x :: l) *) Variable P : utree -> Prop. Variable HL : forall n, P (L n). Variable HN : forall l, Forall P l -> P (N l). Fixpoint utree_ind' (t : utree) : P t := match t with | L n => HL n | N l => HN l ((fix fold (ls : list utree) : Forall P ls := match ls with | nil => Forall_nil P | x::xs => Forall_cons x (utree_ind' x) (fold xs) end) l) end. End utree_ind. Check utree_ind'. (* Example usage *) About fold_right. Fixpoint tsum (t : utree) : Datatypes.nat := match t with | L n => n | N l => fold_right (fun t' s => tsum t' + s) 0 l end. Fixpoint splice1 (t1 t2 : utree) : utree := match t1 with | L n => N (L n::t2::nil) | N nil => N (t2::nil) | N (x::xs) => N ((splice1 x t2)::xs) end. Lemma splice_tsum_id : forall t1 t2, tsum t1 + tsum t2 = tsum (splice1 t1 t2). Proof. intros t1 t2. induction t1 using utree_ind'; simpl. - omega. - destruct l; crush. Check Forall_inv. pose (Forall_inv H) as Hu. simpl in Hu. crush. Qed. (*************** EXERCISES ***************) Inductive binary : Set := | leaf : nat -> binary | node : (binary * binary) -> binary. Check binary_ind. (* What is the induction principle binary_ind and what is the problem with it? Can you come up with a better induction principle and prove it? *) Inductive W : Set := WW : W -> W. (* *************************************************************** *) Module RB. (* Here is a simple datatype declaration describing one of the key structural properties of red-black trees -- the fact that both children of a red node must be black. *) Inductive node : Set := | R : red -> node | B : black -> node with red : Set := | RN : nat -> black -> black -> red with black : Set := | BL : black | BN : nat -> node -> node -> black. (* TODO: - write down the type of the _most natural / useful_ induction principle for [node] - use [Scheme] to construct a term that has this type - construct another term of this type without using [Scheme] *) End RB.