Require Import List. Require Import ZArith. Require Import Tools. Definition plus_length (u_v : list Z * list Z):nat := (length (fst u_v) + length (snd u_v))%nat. Require Import Recdef. Function merge (u_v : list Z * list Z){measure plus_length u_v} : list Z := match u_v with (nil,v) => v | (u,nil) => u | ((a::u') as u,(b::v') as v) => if Zle_bool a b then a::(merge (u',v)) else b::(merge (u,v')) end. unfold plus_length; simpl; auto with arith. intros;unfold plus_length; simpl;auto with arith. Qed. Check merge_equation. Fixpoint nb_occ (n:Z) (l: list Z) : nat := match l with nil => 0%nat | p::l' => if Zeq_bool n p then S(nb_occ n l') else nb_occ n l' end. Lemma nb_occ_merge : forall u_v n, nb_occ n (merge u_v) = nb_occ n (fst u_v) + nb_occ n (snd u_v). intros. functional induction (merge u_v);simpl;auto. case_eq (Zeq_bool n a); case_eq (Zeq_bool n b);simpl in *;intros; rewrite H in *; rewrite IHl;auto. case_eq (Zeq_bool n a); case_eq (Zeq_bool n b);simpl in *;intros; rewrite H0 in *; rewrite IHl;auto. omega. Qed. Open Scope Z_scope. Inductive sorted : list Z -> Prop := sorted_nil : sorted nil | sorted_single : forall a, sorted (a::nil) | sorted_2 : forall a b l, a <= b -> sorted (b::l) -> sorted (a::b::l). Hint Constructors sorted. Lemma sorted_merge_0: forall u_v, sorted (fst u_v) -> sorted (snd u_v) -> sorted (merge u_v). Proof. intro u_v; functional induction (merge u_v) ;simpl in *;auto. (* third case *) inversion 1;inversion 1;simpl. repeat rewrite merge_equation;Zbool2Prop;constructor;auto. repeat rewrite merge_equation;Zbool2Prop;constructor;auto. subst v' u'. rewrite merge_equation. case_eq (Zle_bool b0 b); intro eg. rewrite merge_equation in IHl. rewrite eg in IHl. auto. rewrite merge_equation in IHl. rewrite eg in IHl. constructor 3;auto. Zbool2Prop;auto. subst v';subst u';rewrite merge_equation in IHl. rewrite merge_equation. case_eq (Zle_bool b0 b);intro eg;rewrite eg in *. constructor 3;auto. constructor 3;auto. Zbool2Prop;auto. (* last case *) inversion 1;inversion 1;simpl. repeat rewrite merge_equation;Zbool2Prop;constructor;auto. omega. rewrite merge_equation. case_eq (Zle_bool a b0). intro eg. constructor;auto. Zbool2Prop;omega. subst u'; subst v';auto. rewrite merge_equation in IHl. rewrite eg in IHl; apply IHl; auto. subst v';subst u';rewrite merge_equation in IHl. intro eg; rewrite eg in IHl. constructor 3;auto. subst v';subst u';rewrite merge_equation in IHl. rewrite merge_equation. constructor 3;auto. Zbool2Prop;omega. subst v';subst u';rewrite merge_equation in IHl. case_eq (Zle_bool a b1);intro eg;rewrite eg in IHl. rewrite merge_equation;rewrite eg. constructor 3;auto. Zbool2Prop;omega. rewrite merge_equation. rewrite eg. constructor 3;auto. Qed. Lemma sorted_merge : forall u v, sorted u -> sorted v -> sorted (merge (u,v)). intros;apply sorted_merge_0;simpl;auto. Qed. Extraction "merge.ml" merge.