Require Export ZArith. Require Export List. Require Export Arith. Require Export Omega. Require Export Zwf. Require Export Relations. Require Export Inverse_Image. Inductive Z_btree : Set := Z_leaf : Z_btree | Z_bnode : Z->Z_btree->Z_btree->Z_btree. Print Z_btree_ind. Print Z_btree_rect. Inductive Z_fbtree : Set := Z_fleaf : Z_fbtree | Z_fnode : Z->(bool->Z_fbtree)->Z_fbtree. Inductive even : nat->Prop := | O_even : even 0%nat | plus_2_even : forall n:nat, even n -> even (S (S n)). Open Scope nat_scope. Inductive htree (A:Set) : nat->Set := hleaf : A -> htree A 0 | hnode : forall n:nat, A -> htree A n -> htree A n -> htree A (S n). Inductive list' : Type->Type := nil' : forall A:Type, list' A | cons' : forall A:Type, A -> list' A -> list' A. Inductive inf_branch_tree (A:Set) : Set := inf_leaf : inf_branch_tree A | inf_node : A ->(nat -> inf_branch_tree A)-> inf_branch_tree A. Record group : Type := {A : Type; op : A->A->A; sym : A->A; e : A; e_neutral_left : forall x:A, op e x = x; sym_op : forall x:A, op (sym x) x = e; op_assoc : forall x y z:A, op (op x y) z = op x (op y z); op_comm : forall x y:A, op x y = op y x}. Fixpoint nat_simple_rec (A:Set)(exp1:A)(exp2:nat->A->A)(x:nat) {struct x} : A := match x with | O => exp1 | S p => exp2 p (nat_simple_rec A exp1 exp2 p) end. Definition example_codomain (b:bool) : Set := match b with true => nat | false => bool end. Definition example_dep_function (b:bool) : example_codomain b := match b as x return example_codomain x with | true => 0 | false => true end. Inductive type_name (A B:Type) : nat -> nat -> Type := . Definition bool_case (F:bool->Set)(v1:F true)(v2:F false)(x:bool) := match x return F x with true => v1 | false => v2 end. Module redefine_nat_case. Definition nat_case (F:nat->Set)(exp1:F 0)(exp2:forall p:nat, F (S p))(n:nat) := match n as x return F x with | O => exp1 | S p => exp2 p end. End redefine_nat_case. Module Type nat_rec_type. Parameter nat_rec : forall f:nat->Set, f 0 ->(forall n:nat, f n -> f (S n))-> forall n:nat, f n. End nat_rec_type. Module nat_rec_module : nat_rec_type. Fixpoint nat_rec (f:nat->Set)(exp1:f 0) (exp2:forall p:nat, f p -> f (S p))(n:nat){struct n} : f n := match n as x return f x with | O => exp1 | S p => exp2 p (nat_rec f exp1 exp2 p) end. End nat_rec_module. Definition mult2' := nat_rec (fun n:nat => nat) 0 (fun p v:nat => S (S v)). Module redefine_nat_ind. Fixpoint nat_ind (P:nat->Prop)(exp1:P 0) (exp2:forall p:nat, P p -> P (S p))(n:nat){struct n} : P n := match n as x return P x with | O => exp1 | S p => exp2 p (nat_ind P exp1 exp2 p) end. End redefine_nat_ind. Module Type Z_btree_rec_type. Parameter Z_btree_rec : forall f:Z_btree->Set, f Z_leaf -> (forall (n:Z)(t1:Z_btree), f t1 -> forall t2:Z_btree, f t2 -> f (Z_bnode n t1 t2))-> forall t:Z_btree, f t. End Z_btree_rec_type. Module Z_btree_rec_module : Z_btree_rec_type. Fixpoint Z_btree_rec (f:Z_btree->Set)(exp1:f Z_leaf) (exp2:forall (n:Z)(t1:Z_btree), f t1 -> forall t2:Z_btree, f t2 -> f (Z_bnode n t1 t2)) (t:Z_btree){struct t} : f t := match t as x return f x with | Z_leaf => exp1 | Z_bnode n t1 t2 => exp2 n t1 (Z_btree_rec f exp1 exp2 t1) t2 (Z_btree_rec f exp1 exp2 t2) end. End Z_btree_rec_module. Scheme le_ind' := Induction for le Sort Prop. Eval compute in (forall (n:nat)(P:nat->Prop), (fun (n':nat)(P:forall m:nat, n' <= m -> Prop) => P n' (le_n n')-> (forall (m:nat)(h:n' <= m), P m h -> P (S m)(le_S n' m h))-> forall (m:nat)(h:n' <= m), P m h) n (fun (m:nat)(_:n <= m) => P m)). Fixpoint even_ind_max (P:forall n:nat, even n -> Prop) (exp1:P 0 O_even) (exp2:forall (n:nat)(t:even n), P n t -> P (S (S n))(plus_2_even n t))(n:nat)(t:even n) {struct t} : P n t := match t as x0 in (even x) return P x x0 with | O_even => exp1 | plus_2_even p t' => exp2 p t' (even_ind_max P exp1 exp2 p t') end. Fixpoint even_ind' (P:nat->Prop)(exp1:P 0) (exp2:forall n:nat, even n -> P n -> P (S (S n)))(n:nat)(t:even n) {struct t} : P n := match t in (even x) return P x with | O_even => exp1 | plus_2_even p t' => exp2 p t' (even_ind' P exp1 exp2 p t') end. Fixpoint clos_trans_ind' (A:Set)(R P:A->A->Prop) (exp1:forall x y:A, R x y -> P x y) (exp2:forall x y z:A, clos_trans A R x y -> P x y -> clos_trans A R y z -> P y z -> P x z)(x y:A) (p:clos_trans A R x y){struct p} : P x y := match p in (clos_trans _ _ _ x0) return P x x0 with | t_step y' h => exp1 x y' h | t_trans y' z' h1 h2 => exp2 x y' z' h1 (clos_trans_ind' A R P exp1 exp2 x y' h1) h2 (clos_trans_ind' A R P exp1 exp2 y' z' h2) end. Module even_ind_max_redefined. Scheme even_ind_max := Induction for even Sort Prop. End even_ind_max_redefined. Module nat_simple_rec_redefined. Scheme nat_simple_rec := Minimality for nat Sort Set. End nat_simple_rec_redefined. Definition rich_minus (n m:nat) := {x : nat | x+m = n}. Definition le_rich_minus : forall m n:nat, n <= m -> rich_minus m n. induction m. intros n Hle; exists 0. (** ...*) (** Hle : n <= 0*) (** ============================*) (** 0+n = 0*) inversion Hle; trivial. intros n; case n. intros Hle; exists (S m). (** ...*) (** IHm : forall n:nat, n <= m -> rich_minus m n*) (** n : nat*) (** Hle : 0 <= S m*) (** ============================*) (** S m + 0 = S m*) auto with arith. intros n' Hle. (** ...*) (** IHm : forall n:nat, n <= m -> rich_minus m n*) (** n : nat*) (** n' : nat*) (** Hle : S n' <= S m*) (** ============================*) (** rich_minus (S m)(S n')*) elim (IHm n'). intros r Heq. exists r. rewrite <- Heq; auto with arith. inversion Hle; auto with arith. Defined. Set Implicit Arguments. Inductive lfactor (A:Set) : list A -> list A -> Prop := lf1 : forall u:list A, lfactor nil u | lf2 : forall (a:A)(u v:list A), lfactor u v -> lfactor (cons a u)(cons a v). Set Strict Implicit. Unset Implicit Arguments. Check (forall (A:Set)(u v:list A), lfactor u v -> {w : list A | v = app u w}). Module redefine_eq_rec. Definition eq_rect (A:Type)(x:A)(P:A->Type)(f:P x)(y:A)(e:x = y) : P y := match e in (_ = x) return P x with | refl_equal => f end. Definition eq_rec (A:Type)(x:A)(P:A->Set) : P x -> forall y:A, x = y -> P y := eq_rect A x P. Implicit Arguments eq_rec [A]. End redefine_eq_rec. Section update_def. Variables (A : Set)(A_eq_dec : forall x y:A, {x = y}+{x <> y}). Variables (B : A->Set)(a : A)(v : B a)(f : forall x:A, B x). Definition update (x:A) : B x := match A_eq_dec a x with | left h => eq_rec a B v x h | right h' => f x end. End update_def. Check (fun eq_rec_eq :forall (U:Set)(p:U)(Q:U->Set)(x:Q p)(h:p = p), x = eq_rec p Q x p h => False). Check (fun update_eq :forall (A:Set)(eq_dec:forall x y:A, {x = y}+{x <> y}) (B:A->Set)(a:A)(v:B a)(f:forall x:A, B x), update A eq_dec B a v f a = v => False). Inductive ntree (A:Set) : Set := nnode : A -> nforest A -> ntree A with nforest (A:Set) : Set := nnil : nforest A | ncons : ntree A -> nforest A -> nforest A. Open Scope Z_scope. Fixpoint count (A:Set)(t:ntree A){struct t} : Z := match t with | nnode a l => 1 + count_list A l end with count_list (A:Set)(l:nforest A){struct l} : Z := match l with | nnil => 0 | ncons t tl => count A t + count_list A tl end. Module Type ntree_ind_type. Parameter ntree_ind : forall (A:Set)(P:ntree A -> Prop), (forall (a:A)(l:nforest A), P (nnode A a l))-> forall t:ntree A, P t. End ntree_ind_type. Module ntree_ind_module. Definition ntree_ind := ntree_ind. End ntree_ind_module. Print ntree_ind_module.ntree_ind. Scheme ntree_ind2 := Induction for ntree Sort Prop with nforest_ind2 := Induction for nforest Sort Prop. Inductive occurs (A:Set)(a:A) : ntree A -> Prop := occurs_root : forall l, occurs A a (nnode A a l) | occurs_branches : forall b l, occurs_forest A a l -> occurs A a (nnode A b l) with occurs_forest (A:Set)(a:A) : nforest A -> Prop := occurs_head : forall t tl, occurs A a t -> occurs_forest A a (ncons A t tl) | occurs_tail : forall t tl, occurs_forest A a tl -> occurs_forest A a (ncons A t tl). Fixpoint n_sum_values (t:ntree Z) : Z := match t with | nnode z l => z + n_sum_values_l l end with n_sum_values_l (l:nforest Z) : Z := match l with | nnil => 0 | ncons t tl => n_sum_values t + n_sum_values_l tl end. Hint Resolve occurs_branches occurs_root Zplus_le_compat. Theorem greater_values_sum : forall t:ntree Z, (forall x:Z, occurs Z x t -> 1 <= x)-> count Z t <= n_sum_values t. Proof. intros t; elim t using ntree_ind2 with (P0 := fun l:nforest Z => (forall x:Z, occurs_forest Z x l -> 1 <= x)-> count_list Z l <= n_sum_values_l l). intros z l Hl Hocc; lazy beta iota delta -[Zplus Zle]; fold count_list n_sum_values_l. auto with *. auto with zarith. intros t1 Hrec1 tl Hrec2 Hocc; lazy beta iota delta -[Zplus Zle]; fold count count_list n_sum_values n_sum_values_l. apply Zplus_le_compat. apply Hrec1; intros; apply Hocc; apply occurs_head; auto. apply Hrec2; intros; apply Hocc; apply occurs_tail; auto. Qed. Inductive ltree (A:Set) : Set := lnode : A -> list (ltree A)-> ltree A. Section correct_ltree_ind. Variables (A : Set)(P : ltree A -> Prop)(Q : list (ltree A)-> Prop). Hypotheses (H : forall (a:A)(l:list (ltree A)), Q l -> P (lnode A a l)) (H0 : Q nil) (H1 : forall t:ltree A, P t -> forall l:list (ltree A), Q l -> Q (cons t l)). Fixpoint ltree_ind2 (t:ltree A) : P t := match t as x return P x with | lnode a l => H a l (((fix l_ind (l':list (ltree A)) : Q l' := match l' as x return Q x with | nil => H0 | cons t1 tl => H1 t1 (ltree_ind2 t1) tl (l_ind tl) end)) l) end. End correct_ltree_ind.