(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Definitions and theorems about semi-open integer intervals *)

Require Import Coqlib.
Require Import Zwf.
Require Coq.Program.Wf.
Require Import Recdef.

Definition interv : Type := (Z * Z)%type.

(** * Membership *)

Definition In (x: Z) (i: interv) : Prop := fst i <= x < snd i.

Lemma In_dec:
  forall x i, {In x i} + {~In x i}.
Proof.
(* Goal: forall (x : Z) (i : interv), sumbool (In x i) (not (In x i)) *)
  unfold In; intros.
(* Goal: sumbool (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i))) (not (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i)))) *)
  case (zle (fst i) x); intros.
(* Goal: sumbool (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i))) (not (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i)))) *)
(* Goal: sumbool (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i))) (not (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i)))) *)
  case (zlt x (snd i)); intros.
(* Goal: sumbool (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i))) (not (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i)))) *)
(* Goal: sumbool (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i))) (not (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i)))) *)
(* Goal: sumbool (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i))) (not (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i)))) *)
  left; auto.
(* Goal: sumbool (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i))) (not (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i)))) *)
  right; intuition.
(* Goal: sumbool (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i))) (not (and (Z.le (@fst Z Z i) x) (Z.lt x (@snd Z Z i)))) *)
  right; intuition.
Qed.

Lemma notin_range:
  forall x i,
  x < fst i \/ x >= snd i -> ~In x i.
Proof.
(* Goal: forall (x : Z) (i : interv) (_ : not (In x i)) (_ : Z.lt (@fst Z Z i) (@snd Z Z i)), or (Z.lt x (@fst Z Z i)) (Z.ge x (@snd Z Z i)) *)
  unfold In; intros; omega.
Qed.

Lemma range_notin:
  forall x i,
  ~In x i -> fst i < snd i -> x < fst i \/ x >= snd i.
Proof.
(* Goal: forall (x : Z) (i : interv) (_ : not (In x i)) (_ : Z.lt (@fst Z Z i) (@snd Z Z i)), or (Z.lt x (@fst Z Z i)) (Z.ge x (@snd Z Z i)) *)
  unfold In; intros; omega.
Qed.

(** * Emptyness *)

Definition empty (i: interv) : Prop := fst i >= snd i.

Lemma empty_dec:
  forall i, {empty i} + {~empty i}.
Proof.
(* Goal: forall i : interv, sumbool (empty i) (not (empty i)) *)
  unfold empty; intros.
(* Goal: sumbool (Z.ge (@fst Z Z i) (@snd Z Z i)) (not (Z.ge (@fst Z Z i) (@snd Z Z i))) *)
  case (zle (snd i) (fst i)); intros.
(* Goal: sumbool (Z.ge (@fst Z Z i) (@snd Z Z i)) (not (Z.ge (@fst Z Z i) (@snd Z Z i))) *)
(* Goal: sumbool (Z.ge (@fst Z Z i) (@snd Z Z i)) (not (Z.ge (@fst Z Z i) (@snd Z Z i))) *)
  left; omega.
(* Goal: sumbool (Z.ge (@fst Z Z i) (@snd Z Z i)) (not (Z.ge (@fst Z Z i) (@snd Z Z i))) *)
  right; omega.
Qed.

Lemma is_notempty:
  forall i, fst i < snd i -> ~empty i.
Proof.
(* Goal: forall (i : prod Z Z) (_ : Z.lt (@fst Z Z i) (@snd Z Z i)), not (empty i) *)
  unfold empty; intros; omega.
Qed.

Lemma empty_notin:
  forall x i, empty i -> ~In x i.
Proof.
(* Goal: forall (x : Z) (i : interv) (_ : In x i), not (empty i) *)
  unfold empty, In; intros. omega.
Qed.

Lemma in_notempty:
  forall x i, In x i -> ~empty i.
Proof.
(* Goal: forall (x : Z) (i : interv) (_ : In x i), not (empty i) *)
  unfold empty, In; intros. omega.
Qed.

(** * Disjointness *)

Definition disjoint (i j: interv) : Prop :=
  forall x, In x i -> ~In x j.

Lemma disjoint_sym:
  forall i j, disjoint i j -> disjoint j i.
Proof.
(* Goal: forall (i j : interv) (_ : disjoint i j), disjoint j i *)
  unfold disjoint; intros; red; intros. elim (H x); auto.
Qed.

Lemma empty_disjoint_r:
  forall i j, empty j -> disjoint i j.
Proof.
(* Goal: forall (i j : interv) (_ : empty j), disjoint i j *)
  unfold disjoint; intros. apply empty_notin; auto.
Qed.

Lemma empty_disjoint_l:
  forall i j, empty i -> disjoint i j.
Proof.
(* Goal: forall (A : Type) (f : forall (_ : Z) (_ : A), A) (a : A) (i : interv), @eq A (@fold A f a i) (@fold_right A Z f a (elements i)) *)
  intros. apply disjoint_sym. apply empty_disjoint_r; auto.
Qed.

Lemma disjoint_range:
  forall i j,
  snd i <= fst j \/ snd j <= fst i -> disjoint i j.
Proof.
(* Goal: and (Z.le lo (Z.sub hi (Zpos xH))) (Z.lt (Z.sub hi (Zpos xH)) hi) *)
  unfold disjoint, In; intros. omega.
Qed.

Lemma range_disjoint:
  forall i j,
  disjoint i j ->
  empty i \/ empty j \/ snd i <= fst j \/ snd j <= fst i.
Proof.
(* Goal: forall (A : Type) (f : forall (_ : Z) (_ : A), A) (a : A) (i : interv), @eq A (@fold A f a i) (@fold_right A Z f a (elements i)) *)
  unfold disjoint, empty; intros.
(* Goal: or (Z.ge (@fst Z Z i) (@snd Z Z i)) (or (Z.ge (@fst Z Z j) (@snd Z Z j)) (or (Z.le (@snd Z Z i) (@fst Z Z j)) (Z.le (@snd Z Z j) (@fst Z Z i)))) *)
  destruct (zlt (fst i) (snd i)); auto.
(* Goal: or (Z.ge (@fst Z Z i) (@snd Z Z i)) (or (Z.ge (@fst Z Z j) (@snd Z Z j)) (or (Z.le (@snd Z Z i) (@fst Z Z j)) (Z.le (@snd Z Z j) (@fst Z Z i)))) *)
  destruct (zlt (fst j) (snd j)); auto.
(* Goal: or (Z.ge (@fst Z Z i) (@snd Z Z i)) (or (Z.ge (@fst Z Z j) (@snd Z Z j)) (or (Z.le (@snd Z Z i) (@fst Z Z j)) (Z.le (@snd Z Z j) (@fst Z Z i)))) *)
  right; right.
(* Goal: or (Z.le (@snd Z Z i) (@fst Z Z j)) (Z.le (@snd Z Z j) (@fst Z Z i)) *)
  destruct (zlt (fst i) (fst j)).
(* Case 1: i starts to the left of j. *)
(* Goal: sumbool (disjoint i j) (not (disjoint i j)) *)
  destruct (zle (snd i) (fst j)).
(* Case 1.1: i ends to the left of j, OK *)
(* Goal: P x *)
  auto.
(* Case 1.2: i ends to the right of j's start, not disjoint. *)
(* Goal: and (Z.le lo (Z.sub hi (Zpos xH))) (Z.lt (Z.sub hi (Zpos xH)) hi) *)
  elim (H (fst j)). red; omega. red; omega.
(* Case 2: j starts to the left of i *)
(* Goal: sumbool (disjoint i j) (not (disjoint i j)) *)
  destruct (zle (snd j) (fst i)).
(* Case 2.1: j ends to the left of i, OK *)
(* Goal: P x *)
  auto.
(* Case 2.2: j ends to the right of i's start, not disjoint. *)
(* Goal: and (Z.le lo (Z.sub hi (Zpos xH))) (Z.lt (Z.sub hi (Zpos xH)) hi) *)
  elim (H (fst i)). red; omega. red; omega.
Qed.

Lemma range_disjoint':
  forall i j,
  disjoint i j -> fst i < snd i -> fst j < snd j ->
  snd i <= fst j \/ snd j <= fst i.
Proof.
(* Goal: and (Z.le lo (Z.sub hi (Zpos xH))) (Z.lt (Z.sub hi (Zpos xH)) hi) *)
  intros. exploit range_disjoint; eauto. unfold empty; intuition omega.
Qed.

Lemma disjoint_dec:
  forall i j, {disjoint i j} + {~disjoint i j}.
Proof.
(* Goal: forall (A : Type) (f : forall (_ : Z) (_ : A), A) (a : A) (i : interv), @eq A (@fold A f a i) (@fold_right A Z f a (elements i)) *)
  intros.
(* Goal: P x *)
  destruct (empty_dec i). left; apply empty_disjoint_l; auto.
(* Goal: disjoint j i *)
  destruct (empty_dec j). left; apply empty_disjoint_r; auto.
(* Goal: sumbool (disjoint i j) (not (disjoint i j)) *)
  destruct (zle (snd i) (fst j)). left; apply disjoint_range; auto.
(* Goal: P x *)
  destruct (zle (snd j) (fst i)). left; apply disjoint_range; auto.
(* Goal: P x *)
  right; red; intro. exploit range_disjoint; eauto. intuition.
Qed.

(** * Shifting an interval by some amount *)

Definition shift (i: interv) (delta: Z) : interv := (fst i + delta, snd i + delta).

Lemma in_shift:
  forall x i delta,
  In x i -> In (x + delta) (shift i delta).
Proof.
(* Goal: and (Z.le lo (Z.sub hi (Zpos xH))) (Z.lt (Z.sub hi (Zpos xH)) hi) *)
  unfold shift, In; intros. simpl. omega.
Qed.

Lemma in_shift_inv:
  forall x i delta,
  In x (shift i delta) -> In (x - delta) i.
Proof.
(* Goal: and (Z.le lo (Z.sub hi (Zpos xH))) (Z.lt (Z.sub hi (Zpos xH)) hi) *)
  unfold shift, In; simpl; intros. omega.
Qed.

(** * Enumerating the elements of an interval *)

Section ELEMENTS.

Variable lo: Z.

Function elements_rec (hi: Z) {wf (Zwf lo) hi} : list Z :=
  if zlt lo hi then (hi-1) :: elements_rec (hi-1) else nil.
Proof.
(* Goal: and (Z.le lo (Z.sub hi (Zpos xH))) (Z.lt (Z.sub hi (Zpos xH)) hi) *)
  intros. red. omega.
  apply Zwf_well_founded.
Qed.

Lemma In_elements_rec:
  forall hi x,
  List.In x (elements_rec hi) <-> lo <= x < hi.
Proof.
(* Goal: forall (A : Type) (f : forall (_ : Z) (_ : A), A) (a : A) (i : interv), @eq A (@fold A f a i) (@fold_right A Z f a (elements i)) *)
  intros. functional induction (elements_rec hi).
(* Goal: forall (A : Type) (f : forall (_ : Z) (_ : A), A) (a : A) (i : interv), @eq A (@fold A f a i) (@fold_right A Z f a (elements i)) *)
  simpl; split; intros.
(* Goal: and (Z.le lo (Z.sub hi (Zpos xH))) (Z.lt (Z.sub hi (Zpos xH)) hi) *)
  destruct H. clear IHl. omega. rewrite IHl in H. clear IHl. omega.
(* Goal: and (Z.le lo (Z.sub hi (Zpos xH))) (Z.lt (Z.sub hi (Zpos xH)) hi) *)
  destruct (zeq (hi - 1) x); auto. right. rewrite IHl. clear IHl. omega.
(* Goal: forall _ : or (empty i) (or (empty j) (or (Z.le (@snd Z Z i) (@fst Z Z j)) (Z.le (@snd Z Z j) (@fst Z Z i)))), False *)
  simpl; intuition.
Qed.

End ELEMENTS.

Definition elements (i: interv) : list Z :=
  elements_rec (fst i) (snd i).

Lemma in_elements:
  forall x i,
  In x i -> List.In x (elements i).
Proof.
(* Goal: forall (A : Type) (f : forall (_ : Z) (_ : A), A) (a : A) (i : interv), @eq A (@fold A f a i) (@fold_right A Z f a (elements i)) *)
  intros. unfold elements. rewrite In_elements_rec. auto.
Qed.

Lemma elements_in:
  forall x i,
  List.In x (elements i) -> In x i.
Proof.
(* Goal: forall (A : Type) (f : forall (_ : Z) (_ : A), A) (a : A) (i : interv), @eq A (@fold A f a i) (@fold_right A Z f a (elements i)) *)
  unfold elements; intros.
(* Goal: P x *)
  rewrite In_elements_rec in H. auto.
Qed.

(** * Checking properties on all elements of an interval *)

Section FORALL.

Variables P Q: Z -> Prop.
Variable f: forall (x: Z), {P x} + {Q x}.
Variable lo: Z.

Program Fixpoint forall_rec (hi: Z) {wf (Zwf lo) hi}:
                 {forall x, lo <= x < hi -> P x}
                 + {exists x, lo <= x < hi /\ Q x} :=
  if zlt lo hi then
    match f (hi - 1) with
    | left _ =>
        match forall_rec (hi - 1) with
        | left _ => left _ _
        | right _ => right _ _
        end
    | right _ => right _ _
    end
  else
    left _ _
.
Next Obligation.
(* Goal: and (Z.le lo (Z.sub hi (Zpos xH))) (Z.lt (Z.sub hi (Zpos xH)) hi) *)
  red. omega.
Qed.
Next Obligation.
(* Goal: and (Z.le lo (Z.sub hi (Zpos xH))) (Z.lt (Z.sub hi (Zpos xH)) hi) *)
  assert (x = hi - 1 \/ x < hi - 1) by omega.
(* Goal: P x *)
  destruct H2. congruence. auto.
Qed.
Next Obligation.
(* Goal: and (Z.le lo (Z.sub hi (Zpos xH))) (Z.lt (Z.sub hi (Zpos xH)) hi) *)
  exists wildcard'; split; auto. omega.
Qed.
Next Obligation.
(* Goal: and (Z.le lo (Z.sub hi (Zpos xH))) (Z.lt (Z.sub hi (Zpos xH)) hi) *)
  exists (hi - 1); split; auto. omega.
Qed.
Next Obligation.
(* Goal: P x *)
  omegaContradiction.
Defined.

End FORALL.

Definition forall_dec
       (P Q: Z -> Prop) (f: forall (x: Z), {P x} + {Q x}) (i: interv) :
       {forall x, In x i -> P x} + {exists x, In x i /\ Q x} :=
 forall_rec P Q f (fst i) (snd i).

(** * Folding a function over all elements of an interval *)

Section FOLD.

Variable A: Type.
Variable f: Z -> A -> A.
Variable lo: Z.
Variable a: A.

Function fold_rec (hi: Z) {wf (Zwf lo) hi} : A :=
  if zlt lo hi then f (hi - 1) (fold_rec (hi - 1)) else a.
Proof.
(* Goal: and (Z.le lo (Z.sub hi (Zpos xH))) (Z.lt (Z.sub hi (Zpos xH)) hi) *)
  intros. red. omega.
  apply Zwf_well_founded.
Qed.

Lemma fold_rec_elements:
  forall hi, fold_rec hi = List.fold_right f a (elements_rec lo hi).
Proof.
(* Goal: forall (A : Type) (f : forall (_ : Z) (_ : A), A) (a : A) (i : interv), @eq A (@fold A f a i) (@fold_right A Z f a (elements i)) *)
  intros. functional induction (fold_rec hi).
(* Goal: P x *)
  rewrite elements_rec_equation. rewrite zlt_true; auto.
(* Goal: @eq A (f (Z.sub hi (Zpos xH)) (fold_rec (Z.sub hi (Zpos xH)))) (@fold_right A Z f a (@cons Z (Z.sub hi (Zpos xH)) (elements_rec lo (Z.sub hi (Zpos xH))))) *)
(* Goal: @eq A a (@fold_right A Z f a (elements_rec lo hi)) *)
  simpl. congruence.
(* Goal: P x *)
  rewrite elements_rec_equation. rewrite zlt_false; auto.
Qed.

End FOLD.

Definition fold {A: Type} (f: Z -> A -> A) (a: A) (i: interv) : A :=
  fold_rec A f (fst i) a (snd i).

Lemma fold_elements:
  forall (A: Type) (f: Z -> A -> A) a i,
  fold f a i = List.fold_right f a (elements i).
Proof.
(* Goal: forall (A : Type) (f : forall (_ : Z) (_ : A), A) (a : A) (i : interv), @eq A (@fold A f a i) (@fold_right A Z f a (elements i)) *)
  intros. unfold fold, elements. apply fold_rec_elements.
Qed.

(** Hints *)

Hint Resolve
  notin_range range_notin
  is_notempty empty_notin in_notempty
  disjoint_sym empty_disjoint_r empty_disjoint_l
  disjoint_range
  in_shift in_shift_inv
  in_elements elements_in : intv.
