Require Import ZArith. Open Scope Z_scope. Require Import Recdef. Require Import Zwf. Require Import Omega. Require Import Wf. Require Import Inverse_Image. Require Import Inclusion. Require Import Tools. Require Import Zmeasure. Open Scope Z_scope. Section Definitions. Definition array_t := Z -> Z. Definition search_t := Z * Z -> option Z. Variable a : array_t. Variable x : Z. Definition correct (s : search_t) from to:= forall i, s (from ,to) = Some i ->from <= i /\ i <= to /\ a(i)=x. Definition complete (s : search_t) from to := s (from,to) = None -> forall k, from <= k <= to -> a k <> x. Definition middle (n p : Z) := (n + p)/ 2. Lemma middle_ge : forall n p, n <= p -> n <= middle n p. intros n p H;pattern n at 1;replace n with ((n*2)/2). unfold middle;apply Z_div_le;auto with zarith. rewrite Z_div_mult_full;auto with zarith. Qed. Lemma middle_le : forall n p, n <= p -> middle n p <= p. intros n p H;pattern p at 2;replace p with ((p*2)/2). unfold middle;apply Z_div_le;auto with zarith. rewrite Z_div_mult_full;auto with zarith. Qed. Ltac abstract_middle n p name := generalize (middle_le n p);generalize (middle_ge n p); pose (name := middle n p); fold name. Let R : relation (Z * Z ) := Zmeasure (fun p => snd p - fst p) 0. Function search (bounds : Z*Z ){wf (Zmeasure (fun p => snd p - fst p) 0) bounds} : option Z := let (from,to) := bounds in if Zle_bool from to then let m := middle from to in if Zeq_bool x (a m) then Some m else if andb (Zle_bool from (m-1)) (Zlt_bool x (a m)) then search (from, m - 1) else if Zle_bool (m +1) to then search (m+1, to) else None else None. Proof. intros; Zbool2Prop. abstract_middle from to m; unfold R;simpl; intros;fold m in H,H0; unfold Zmeasure;simpl; omega. intros;Zbool2Prop;abstract_middle from to m;intros. fold m in teq3;unfold Zmeasure;simpl;omega. intros;simpl; Zbool2Prop. fold m in teq3;unfold Zmeasure;simpl;omega. apply Zmeasure_wf. Qed. Lemma search_1 : forall from to : Z, from <= to -> correct search from to. Proof. intros from to H';pose (p := (from,to)). red;intros;fold p in H. replace from with (fst p) in *;replace to with (snd p) in *;auto. functional induction (search p); try discriminate; clear from to;rename from0 into from;rename to0 into to; abstract_middle from to m;Zbool2Prop;simpl in *. injection H;intro H0;subst i;clear H;fold m in e1;simpl. fold m;omega. split;fold m in H, H0, H1, e1, IHo. destruct IHo;auto. simpl in *;split;Zbool2Prop. destruct (IHo H0);auto. omega. destruct IHo;tauto. fold m in e1, e, e3, IHo, H;split. destruct (IHo e3);auto;omega. destruct (IHo e3);tauto. intros;destruct (IHo e3);auto;split. destruct H3;fold m in H2;auto;try omega. omega. Qed. Definition sorted (from to : Z) := forall i j, from <= i -> i <= j -> j <= to -> a i <= a j. Lemma sorted_restriction : forall from to from' to', sorted from to ->from <= from' -> to' <= to -> sorted from' to'. unfold sorted;intros; apply H;omega. Qed. Lemma search_2 : forall from to , from <= to -> sorted from to -> complete search from to. Proof. intros from to H';pose (p := (from,to));red;fold p;intros. replace from with (fst p) in *;replace to with (snd p) in *;auto. functional induction (search p) ; try discriminate; simpl in *; clear from to;rename from0 into from;rename to0 into to;Zbool2Prop; abstract_middle from to m;intros m_1 m_2. fold m in e1,H0, IHo, H2, H3. destruct (Z_dec k m). destruct s. apply IHo;auto. eapply sorted_restriction with from to;eauto with zarith. omega. assert (a m <= a k). apply H;try omega. omega. subst k;omega. fold m in H,e, e1, e3, IHo ;destruct (Z_dec m k ). destruct s. assert (m=from) by omega. assert (a m <= a k)%Z by (apply H ;auto;try omega). apply IHo;auto;try omega. apply sorted_restriction with from to;auto;omega. omega. subst k;omega. fold m in H,e, e1, e3, IHo ;destruct (Z_dec m k ). destruct s. apply IHo;auto;try omega. apply sorted_restriction with from to;auto;try omega. fold m in H0;assert (a m < x) by omega. intro eg;subst x;clear H2;assert (a k <= a m)%Z. apply H;auto;try omega. omega. subst k;omega. intros;assert (from = m) by omega. rewrite H2 in *;assert (from=to) by omega. assert (k=from) by omega. rewrite H4 in *;fold m in e,e1,e3. rewrite <- H2 in e1;auto. rewrite <- H2 in e,e3. fold m in e1,e,e3;assert (m = to) by omega. rewrite H2;auto. fold m in e1,e,e3;assert (a m < x) by omega. intro eg;subst x;assert (a k <= a m). apply H;try omega. omega. omega. Qed. End Definitions. Definition a : array_t := fun i => (i / 4) . Definition r := search a 5 (-10000,2000). Definition r1 := search a 5 (100,1000). Extraction "search.ml" r r1. Unset Printing Notations. Check 21. Check 22.