Require Import Arith Omega. Ltac puts t := generalize t; intro. Section Half. Fixpoint half (n : nat) : nat := match n with | 0 => 0 | 1 => 1 | S (S m) => S (half m) end. Lemma half_le : forall n, half n <= n. intros n. apply (@proj2 (half (S n) <= S n)). induction n. auto. intuition. simpl. auto with arith. Qed. Lemma half_double : forall n, half (n + n) = n. Proof. intros. induction n. auto. replace (S n + S n) with (S (S (n+n))) by omega. simpl. auto. Qed. Lemma half_grows : forall m n, m <= n -> half m <= half n. Proof. intros. rewrite (le_plus_minus _ _ H). rewrite plus_comm. clear H. apply (@proj2 (half m <= half (S (n-m) + m))). induction (n - m). intuition. simpl plus. apply (@proj2 (half (S m) <= half (S (S m)))). induction m. simpl. auto. simpl in *. intuition auto with arith. intuition. simpl; auto with arith. Qed. Lemma half_max : forall m n, half (m + n) <= Max.max m n. Proof. intros. destruct (le_lt_dec m n). rewrite (Max.max_r _ _ l). rewrite <- (half_double n) at 2. apply half_grows; omega. rewrite Max.max_l by auto with arith. rewrite <- (half_double m) at 2. apply half_grows; omega. Qed. Lemma half_min : forall m n, Min.min m n <= half (m + n). Proof. intros. destruct (le_lt_dec m n). rewrite Min.min_l by auto. rewrite <- (half_double m) at 1. apply half_grows; omega. rewrite Min.min_r by auto with arith. rewrite <- (half_double n) at 1. apply half_grows; omega. Qed. Lemma half_neq : forall m n, m < n -> m < half (m + n). Proof. intros m n. intros. rewrite (le_plus_minus m n) by omega. assert (n - m > 0) by omega. set (a := n-m) in *. clearbody a; clear H. induction m; simpl. destruct a. elimtype False; omega. destruct a; simpl; omega. rewrite plus_comm. simpl. rewrite plus_comm. auto with arith. Qed. Lemma half_loop : forall m n, m <= n -> half (m + n) <= m -> n = m. Proof. intros. destruct H. auto. assert (m < S m0) by auto with arith. puts (half_neq _ _ H1). elimtype False; omega. Qed. End Half. Hint Resolve half_le half_grows. Section State. Inductive state : Set := | Last : nat -> state | Cons : nat -> state -> state. Fixpoint hd (s : state) : nat := match s with Last a => a | Cons a _ => a end. Fixpoint length (s : state) : nat := match s with | Last _ => 1 | Cons _ s' => S (length s') end. Fixpoint next (fst : nat) (l : state) {struct l} : state := match l with | Last a => Last (half (a + fst)) | Cons a rem => Cons (half (a + hd rem)) (next fst rem) end. Definition next_state l := next (hd l) l. Fixpoint nth_state (n : nat) (s : state) {struct n} : state := match n with | 0 => s | S m => nth_state m (next_state s) end. Lemma nth_state_plus : forall m n s, nth_state (m + n) s = nth_state n (nth_state m s). Proof. induction m; simpl; intros; auto. Qed. Lemma length_stable : forall s, length (next_state s) = length s. Proof. intros. unfold next_state. set (a := hd s); clearbody a. induction s; simpl in *; auto. Qed. Lemma length_stable_nth : forall n s, length (nth_state n s) = length s. Proof. induction n; simpl; intros; auto. rewrite IHn. apply length_stable. Qed. Fixpoint max (l : state) : nat := match l with | Last a => a | Cons a rem => Max.max a (max rem) end. Fixpoint min (l : state) : nat := match l with | Last a => a | Cons a rem => Min.min a (min rem) end. Lemma le_min_max : forall s, min s <= max s. Proof. induction s; auto. simpl. eauto with arith. Qed. Lemma le_min_hd : forall s, min s <= hd s. Proof. destruct s; simpl; auto with arith. Qed. Lemma le_hd_max : forall s, hd s <= max s. Proof. destruct s; simpl; auto with arith. Qed. Definition diff s := max s - min s. Fixpoint num n (s : state) {struct s} : nat := match s with | Last a => if eq_nat_dec a n then 1 else 0 | Cons a rem => if eq_nat_dec a n then S (num n rem) else num n rem end. Lemma le_num_length : forall a s, num a s <= length s. Proof. induction s; simpl; destruct (eq_nat_dec n a); auto with arith. Qed. End State. Hint Resolve le_min_max le_min_hd le_hd_max. Lemma max_decr : forall s, max (next_state s) <= max s. Proof. intros. unfold next_state. assert (max (Cons (hd s) s) = max s) by (simpl; auto with arith). rewrite <- H; clear H. set (fst := hd s); clearbody fst. induction s; simpl. rewrite plus_comm. apply half_max. simpl in IHs. destruct (le_lt_dec (half (n + hd s)) (max (next fst s))). rewrite (Max.max_r _ _ l). destruct (Max.max_dec fst (max s)); rewrite e in IHs; eauto with arith. rewrite Max.max_l by auto with arith. clear; destruct s; simpl. eauto using half_max with arith. rewrite (Max.max_assoc n). eauto using half_max with arith. Qed. Lemma min_incr : forall s, min s <= min (next_state s). Proof. intros. unfold next_state. assert (min (Cons (hd s) s) = min s) by (simpl; auto with arith). rewrite <- H; clear H. set (fst := hd s); clearbody fst. induction s; simpl. rewrite plus_comm. apply half_min. simpl in IHs. destruct (le_lt_dec (half (n + hd s)) (min (next fst s))). rewrite (Min.min_l _ _ l). clear; destruct s; simpl; puts (half_min n n0). eauto with arith. rewrite (Min.min_assoc n). eauto with arith. rewrite (Min.min_r _ (min (next fst s))) by auto with arith. destruct (Min.min_dec fst (min s)); rewrite e in IHs; eauto with arith. Qed. Lemma min_num_stable : forall a b s, a <= min s -> a <= b -> num a (next b s) <= num a s. Proof. intros. induction s; simpl in *. destruct (eq_nat_dec (half (n + b)) a). destruct (eq_nat_dec n a). auto. elim n0; clear n0. assert (half (a + n) <= a). rewrite plus_comm. rewrite <- e at 2. auto with arith. apply half_loop; auto. auto with arith. assert (a <= min s) by (clear -H; eauto with arith). destruct (eq_nat_dec (half (n + hd s)) a); destruct (eq_nat_dec n a); try subst; auto with arith. elim n0; clear n0. set (a := half (n + hd s)). assert (a <= hd s) by eauto with arith. assert (a <= n) by (clear -H; eauto with arith). apply half_loop; auto. apply half_grows. omega. Qed. Lemma min_num_decr1 : forall b s, min s < b -> num (min s) (next b s) < num (min s) s. Proof. intros. induction s; simpl in *. destruct (eq_nat_dec (half (n + b))). puts (half_neq _ _ H). elimtype False; omega. destruct (eq_nat_dec n n); auto. elim n1; auto. destruct (le_lt_dec (min s) n). rewrite (Min.min_r _ _ l) in *. specialize (IHs H). destruct (eq_nat_dec (half (n + hd s)) (min s)); destruct (eq_nat_dec n (min s)); auto with arith. elim n0; clear n0. assert (half (min s + n) <= min s). rewrite <- e at 2. rewrite plus_comm. auto with arith. apply half_loop; auto. assert (n <= min s) by omega. rewrite (Min.min_l _ _ H0) in *. destruct (eq_nat_dec n n); try (elim n0; auto). clear e. destruct (eq_nat_dec (half (n + hd s)) n). puts (half_neq _ _ l). assert (half (n + min s) <= half (n + hd s)) by auto with arith. omega. apply le_lt_n_Sm. apply min_num_stable; auto with arith. Qed. Lemma min_num_decr2 : forall s, hd s = min s -> hd s < max s -> num (hd s) (next (hd s) s) < num (hd s) s. Proof. intros. induction s; simpl in *. elimtype False; omega. destruct (le_lt_dec (min s) n). rewrite (Min.min_r _ _ l) in *. subst n. destruct (eq_nat_dec (min s) (min s)); try (elim n; auto). clear e. destruct (eq_nat_dec (half (min s + hd s)) (min s)). assert (min s <= hd s) by auto. assert (half (min s + hd s) <= min s) by omega. puts (half_loop _ _ H H1). apply lt_n_S. rewrite Max.max_r in H0 by auto. rewrite H2 in *. apply IHs; auto. apply le_lt_n_Sm. apply min_num_stable; auto with arith. destruct (eq_nat_dec n n); try (elim n0; auto). clear e. destruct (eq_nat_dec (half (n + hd s)) n). puts (half_neq _ _ l). assert (half (n + min s) <= n). rewrite <- e at 2. auto with arith. elimtype False; omega. apply le_lt_n_Sm. apply min_num_stable; auto with arith. Qed. Lemma min_num_decr : forall s, min s < max s -> num (min s) (next_state s) < num (min s) s. Proof. intros. unfold next_state. destruct (le_lt_dec (hd s) (min s)). assert (hd s = min s) by (puts (le_min_hd s); omega). rewrite <- H0 in *. apply min_num_decr2; auto. apply min_num_decr1; auto. Qed. Lemma diff_decr : forall s, diff (next_state s) <= diff s. Proof. intros. unfold diff. specialize (min_incr s); intro. specialize (max_decr s); intro. omega. Qed. Lemma diff_decr_nth : forall n s, diff (nth_state n s) <= diff s. Proof. induction n; simpl; intros. auto. eauto using diff_decr with arith. Qed. Theorem raise_min : forall s, 0 < diff s -> diff (nth_state (length s) s) < diff s. Proof. intros. puts (le_num_length (min s) s). set (h := length s) in *; clearbody h. revert s H H0. induction h; simpl; intros. clear -H0. elimtype False. induction s; simpl in *. destruct (eq_nat_dec n n); omega. destruct (eq_nat_dec n (Min.min n (min s))). omega. destruct (Min.min_dec n (min s)); rewrite e in *. elim n0; auto. auto. destruct (le_lt_dec (diff s) (diff (next_state s))). apply (lt_le_trans _ (diff (next_state s)) _). apply IHh; try omega. destruct (eq_nat_dec (min s) (min (next_state s))). rewrite <- e in *. assert (min s < max s) by (unfold diff in H; omega). puts (min_num_decr _ H1); omega. unfold diff in l. generalize (le_min_max s) (le_min_max (next_state s)). generalize (min_incr s) (max_decr s); intros. elim n. omega. apply diff_decr. apply (le_lt_trans _ (diff (next_state s)) _). apply diff_decr_nth. auto. Qed. Theorem converges : forall s, exists n, diff (nth_state n s) = 0. Proof. intros. exists (diff s * length s). set (h := diff s). assert (diff s <= h) by auto. clearbody h. revert s H. induction h; intros. simpl; omega. case_eq (diff s); intros. puts (diff_decr_nth (S h * length s) s); omega. assert (0 < diff s) by omega. generalize (raise_min _ H1); intro Hred. simpl. rewrite nth_state_plus. rewrite <- (length_stable_nth (length s)) at 1. apply IHh. omega. Qed.