Section zmyla. Inductive bool : Set := true : bool | false : bool. Check bool_ind. Eval compute in bool_ind. Inductive nat : Set := O : nat | S : nat -> nat. Check nat_ind. Eval compute in nat_ind. End zmyla. Inductive blist : Set := bnil : blist | bcons : bool -> blist -> blist. Check blist_ind. Eval compute in blist_ind. Inductive plist (A:Set) : Set := pnil : plist A | pcons : A -> plist A -> plist A. Check plist_ind. Eval compute in plist_ind. Inductive blistn : nat -> Set := bniln : blistn O | bconsn : bool -> forall n, blistn n -> blistn (S n). Check blistn_ind. Eval compute in blistn_ind. Inductive plistn (A:Set) : nat -> Set := pniln : plistn A O | pconsn : A -> forall n, plistn A n -> plistn A (S n). Check plistn_ind. Eval compute in plistn_ind. Inductive hlist : Type := hnil : hlist | hcons : forall A:Set, A -> hlist -> hlist. Check hlist_ind. Eval compute in hlist_ind. Inductive tree : Set := node : forest -> tree with forest : Set := | emptyf : forest | consf : tree -> forest -> forest. Check tree_ind. Eval compute in tree_ind. Scheme tree_i := Induction for tree Sort Prop with forest_i := Induction for forest Sort Prop. Check conj tree_i forest_i. Print tree_i. Inductive and (A : Prop) (B : Prop) : Prop := conj : A -> B -> and A B. Check and_ind. Eval compute in and_ind. Inductive or (A : Prop) (B : Prop) : Prop := or_introl : A -> or A B | or_intror : B -> or A B. Check or_ind. Eval compute in or_ind. Inductive ex (A : Set) (P : A -> Prop) : Prop := ex_intro : forall x : A, P x -> ex A P. Check ex_ind. Eval compute in ex_ind. Inductive Even : nat -> Prop := evO : Even O | evSS : forall n, Even n -> Even (S(S n)). Check Even_ind. Eval compute in Even_ind. Scheme Ev_dind := Induction for Even Sort Prop. Check Ev_dind. Inductive Length (A:Set) : plist A -> nat -> Prop := | Lnil : Length A (pnil A) O | Lcons : forall (a:A) (l:plist A) (n:nat), Length A l n -> Length A (pcons A a l) (S n). Check Length_ind. Eval compute in Length_ind. Import Datatypes. Implicit Arguments pcons. Inductive Sorted : plist nat -> Prop := | Snil : Sorted (pnil nat) | Sone : forall n, Sorted (pcons n (pnil nat)) | Scons : forall l n1 n2, Sorted (pcons n2 l) -> n1 < n2 -> Sorted (pcons n1 (pcons n2 l)). Check Sorted_ind. Eval compute in Sorted_ind. Inductive btree : Set := bleaf : btree | bnode : btree -> btree -> btree. Check btree_ind. Eval compute in btree_ind. Inductive ftree : Set := fleaf : ftree | fnode : (bool -> ftree) -> ftree. Check ftree_ind. Eval compute in ftree_ind. Fixpoint ftree_of_btree (b : btree) {struct b} : ftree := match b with | bleaf => fleaf | bnode b1 b2 => fnode (fun b => if b then ftree_of_btree b1 else ftree_of_btree b2) end. Fixpoint btree_of_ftree (f : ftree) {struct f} : btree := match f with | fleaf => bleaf | fnode fb => bnode (btree_of_ftree (fb true)) (btree_of_ftree (fb false)) end. Definition b := bnode bleaf (bnode (bnode bleaf bleaf) bleaf). Eval compute in (ftree_of_btree b). Definition f := fnode (fun b : bool => if b then fleaf else fnode (fun b0 : bool => if b0 then fnode (fun b1 : bool => if b1 then fleaf else fleaf) else fleaf)). Eval compute in (btree_of_ftree f). Inductive ntree : Set := nleaf : ntree | nnode : (nat -> ntree) -> ntree. Check ntree_ind. Eval compute in ntree_ind. Fixpoint patyk (n:nat) {struct n} : ntree := match n with | O => nleaf | (S m) => nnode (fun n=> match n with O => patyk m | _ => nleaf end) end. Eval compute in nnode patyk.