Library Scat.BoundedIteration

Require Export ZArith.

Open Scope Z_scope.

Definition biter_nat {A} (n:nat) (f: Z → A → A) (init: Z×A) :=
  iter_nat n (Z×A)%type (fun c ⇒ let (n,x):=c in (n+1,f n x)) init.

Lemma biter_nat_spec_1 A n (f: Z → A → A) (init: Z×A):
  fst (biter_nat n f init) = (fst init)+(Z_of_nat n).
Proof.
 unfold biter_nat; induction n; simpl; auto.
 omega.
 generalize IHn; clear IHn.
 case (iter_nat n (Z × A)%type (fun c ⇒ let (n, x) := c in (n + 1, f n x)) init); simpl.
 intros; rewrite Zpos_P_of_succ_nat.
 subst.
 omega.
Qed.

Lemma biter_nat_aux A n (f: Z → A → A) (init: Z×A):
  fst init ≤ fst (biter_nat n f init).
Proof.
  rewrite biter_nat_spec_1.
  generalize (Zle_0_nat n).
  intros; omega.
Qed.

Lemma bounder_iter_nat_spec A n (f: Z → A → A) (init: Z×A) (Inv: Z → A → Prop):
  Inv ((fst init)-1) (snd init) → (∀ m x, fst init ≤ m < (fst init)+(Z_of_nat n) → Inv (m-1) x → Inv m (f m x))
    → Inv ((fst init)+(Z_of_nat n)-1) (snd (biter_nat n f init)).
Proof.
  intros H1.
  rewrite <- biter_nat_spec_1 with (f:=f).
  unfold biter_nat; induction n; simpl; auto.
  generalize (biter_nat_aux _ n f init); unfold biter_nat.
  generalize IHn; clear IHn.
  case (iter_nat n (Z × A)%type (fun c ⇒ let (n, x) := c in (n + 1, f n x)) init); simpl.
  intros z; cutrewrite (z+1-1=z).
  firstorder.
  omega.
Qed.

Definition biter {A} (min max: Z) (f: Z → A → A) (init: A) :=
  snd (iter (max+1-min) (Z×A)%type (fun c ⇒ let (n,x):=c in (n+1,f n x)) (min, init)).

Theorem biter_spec A (min max: Z) (f: Z → A → A) (init: A) (Inv: Z → A → Prop):
  (∀ n, n < min → Inv n init) → (∀ n x, min ≤ n ≤ max → Inv (n-1) x → Inv n (f n x))
    → Inv max (biter min max f init).
Proof.
  intros H1 H2; unfold biter.
  elimtype (∃ n, n=(max + 1 - min)); eauto.
  intros n H3; rewrite <- H3.
  case (Z_le_dec 0 n).
  intros H4; rewrite iter_nat_of_Z; auto.
  lapply (bounder_iter_nat_spec _ (Zabs_nat n) f (min,init) Inv); simpl.
  rewrite inj_Zabs_nat. rewrite Zabs_eq; auto.
  clear H1; cutrewrite (min+n-1=max); firstorder.
  clear H2; firstorder.
  generalize H3; clear H3; case n; simpl.
  intros H3 H; case H; omega.
  intros p H3 H; case H; auto with zarith.
  intros p H3; rewrite H3.
  intros H; clear H2 H3; firstorder.
Qed.

Lemma split_le {a b c}: a ≤ b ≤ c → a ≤ b ≤ c-1 ∨ b=c.
Proof.
  intros H; case (Z_eq_dec b c).
  intros; subst; auto.
  firstorder.
Qed.

Ltac biter_split_le H := case (split_le H); [ idtac | intros; subst; auto].

Ltac biter_ind :=
   match goal with
   | |- appcontext [biter ?min ?max ?f ?init] ⇒
         pattern max, (biter min max f init);
         apply (biter_spec _ min max f init);
         trivial;
         try (intros; elimtype False; omega) ;
         try (intros; match goal with
                     | H: ?a ≤ ?b ≤ ?c |- _ ⇒ biter_split_le H; intuition; fail
                     end)
   | |- _ ⇒ fail 1 "not found any biter application in the current goal"
   end.

Lemma biter_zero A (min max: Z) (f: Z → A → A) (init: A):
  max < min → biter min max f init=init.
Proof.
  intros; biter_ind.
Qed.

Lemma biter_one A (min: Z) (f: Z → A → A) (init: A) :
  biter min min f init = f min init.
Proof.
  unfold biter.
  cutrewrite (min+1 - min = 1); simpl.
  auto.
  omega.
Qed.

Lemma biter_succ A (min max: Z) (f: Z → A → A) (init: A) :
  min ≤ max → biter min max f init = f max (biter min (max-1) f init).
Proof.
  unfold biter; intros H.
  cutrewrite (max - 1 + 1 - min = max - min); try omega.
  rewrite iter_nat_of_Z; try omega.
  cutrewrite (max + 1 - min = 1 + (max - min)); try omega.
  rewrite Zabs_nat_Zplus; try omega.
  rewrite iter_nat_plus. simpl.
  rewrite iter_nat_of_Z; try omega.
  generalize (biter_nat_spec_1 _ (Zabs_nat (max - min)) f (min, init)).
  elimtype (∃ x, x=biter_nat (Zabs_nat (max - min)) f (min, init)); eauto.
  unfold biter_nat.
  intros x H0; rewrite <- H0; clear H0.
  destruct x; simpl.
  rewrite inj_Zabs_nat. rewrite Zabs_eq; try omega.
  cutrewrite (min + (max - min) = max); try omega.
  intros; subst; auto.
Qed.


Require Export MiscUtils.

Definition Zforall (min max: Z) (P: Z → bool) :=
  biter min max (fun x Q ⇒ P x &&& Q) true.

Lemma Zforall_spec_1 min max P: Zforall min max P = true → ∀ x, min ≤ x ≤ max → P x = true.
Proof.
  unfold Zforall.
  biter_ind.
  intros n z H H0 H1 y H2.
  biter_split_le H2; generalize H1; eqtrue.
Qed.

Lemma Zforall_spec_2 min max P: (∀ x, min ≤ x ≤ max → P x = true) → Zforall min max P = true.
Proof.
  unfold Zforall;
  biter_ind.
  intros n z H H0 H1.
  lapply (H1 n); try omega.
  generalize H0; clear H0.
  eqtrue.
  intuition.
Qed.

Definition Zexists (min max: Z) (P: Z → Prop) :=
  biter min max (fun x Q ⇒ P x ∨ Q) False.

Lemma Zexists_spec_1 min max P: Zexists min max P → ∃ x, min ≤ x ≤ max ∧ P x.
Proof.
  unfold Zexists.
  biter_ind; firstorder.
Qed.

Lemma Zexists_spec_2 min max (P: Z → Prop) x: min ≤ x ≤ max → P x → Zexists min max P.
Proof.
  unfold Zexists.
  biter_ind.
Qed.

Lemma zexists_monotonic (min max: Z) (P Q: Z → Prop): Zexists min max P → (∀ x, min ≤ x ≤ max → P x → Q x) → Zexists min max Q.
Proof.
  intros H1 H2; case (Zexists_spec_1 min max P H1).
  intuition; eapply Zexists_spec_2; eauto.
Qed.

Program Fixpoint dbiter_natx {A} (n:nat) (z: Z) (f:{z0:Z | z ≤ z0 < z+(Z_of_nat n)} → A → A) (x:A) (m: nat){struct m}:
      {z0:Z | le m n ∧ z0 = z+(Z_of_nat n)-(Z_of_nat m)} → A :=
  match m return {z0:Z | le m n ∧ z0 = z+(Z_of_nat n)-(Z_of_nat m)} → A with
  | O ⇒ fun _ ⇒ x
  | S m ⇒ fun z0 ⇒ dbiter_natx n z f (f z0 x) m (z0+1)
  end.
Obligation 1.
  rewrite Zpos_P_of_succ_nat.
  intuition.
Qed.
Obligation 2.
  rewrite Zpos_P_of_succ_nat.
  intuition.
Qed.

Program Definition dbiter_nat {A} (n:nat) (z: Z) (f:{z0:Z | z ≤ z0 < z+(Z_of_nat n)} → A → A) (x:A)
  := dbiter_natx n z f x n z.
Obligation 1.
  intuition.
Qed.

Lemma dbiter_natx_spec A n z (f: {z0:Z | z ≤ z0 < z+(Z_of_nat n)} → A → A) (Inv: Z → A → Prop):
 (∀ z0 y (h:z ≤ z0 < z+(Z_of_nat n)), Inv (z0-1) y → Inv z0 (f (exist (fun z0 ⇒ z ≤ z0 < z+(Z_of_nat n)) _ h) y))
 → ∀ (m:nat) (x:A) (z0:{z0:Z | (le m n) ∧ z0 = z+(Z_of_nat n)-(Z_of_nat m)}),
        (Inv (proj1_sig z0-1) x) → Inv (z+(Z_of_nat n)-1) (dbiter_natx n z f x m z0).
Proof.
  induction m;
  intros x z0; case z0; simpl; clear z0; intros z0;
  intros H0; case H0; clear H0; intros H0 H1.
  subst.
  cutrewrite (z + Z_of_nat n - 0 = z + Z_of_nat n).
  auto.
  omega.
  intros.
  refine (IHm _ (exist _ (z0+1) _) _).
  simpl.
  cutrewrite (z0+1-1=z0).
  auto.
  omega.
Qed.

Lemma dbiter_nat_spec A n z (f: {z0:Z | z ≤ z0 < z+(Z_of_nat n)} → A → A) (x:A) (Inv: Z → A → Prop):
  Inv (z-1) x →
  (∀ z0 y (h:z ≤ z0 < z+(Z_of_nat n)), Inv (z0-1) y → Inv z0 (f (exist (fun z0 ⇒ z ≤ z0 < z+(Z_of_nat n)) _ h) y))
    → Inv (z+(Z_of_nat n)-1) (dbiter_nat n z f x).
Proof.
  intros; unfold dbiter_nat.
  apply dbiter_natx_spec; simpl; auto.
Qed.