(* *********************************************************************)
(*                                                                     *)
(*              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.     *)
(*                                                                     *)
(* *********************************************************************)

(** Finite sets of integer intervals *)

Require Import Coqlib.

Module ISet.

(** "Raw", non-dependent implementation.  A set of intervals is a
  list of nonempty semi-open intervals [(lo, hi)],
  sorted in increasing order of the low bound,
  and with no overlap nor adjacency between elements.
  In particular, if the list contains [(lo1, hi1)] followed by [(lo2, hi2)],
  we have [lo1 < hi1 < lo2 < hi2]. *)

Module R.

Inductive t : Type := Nil | Cons (lo hi: Z) (tl: t).

Fixpoint In (x: Z) (s: t) :=
  match s with
  | Nil => False
  | Cons l h s' => l <= x < h \/ In x s'
  end.

Inductive ok: t -> Prop :=
  | ok_nil: ok Nil
  | ok_cons: forall l h s
      (BOUNDS: l < h)
      (BELOW: forall x, In x s -> h < x)
      (OK: ok s),
      ok (Cons l h s).

Fixpoint mem (x: Z) (s: t) : bool :=
  match s with
  | Nil => false
  | Cons l h s' => if zlt x h then zle l x else mem x s'
  end.

Lemma mem_In:
  forall x s, ok s -> (mem x s = true <-> In x s).
Proof.
(* Goal: forall (s2 : t) (_ : ok s2), ok (inter (Cons l h s) s2) *)
  induction 1; simpl.
- intuition congruence.
- destruct (zlt x h).
+ destruct (zle l x); simpl.
  * tauto.
  * split; intros. congruence.
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
    exfalso. destruct H0. omega. exploit BELOW; eauto. omega.
+ rewrite IHok. intuition.
Qed.

Fixpoint contains (L H: Z) (s: t) : bool :=
  match s with
  | Nil => false
  | Cons l h s' => (zle H h && zle l L) || contains L H s'
  end.

Lemma contains_In:
  forall l0 h0, l0 < h0 -> forall s, ok s ->
  (contains l0 h0 s = true <-> (forall x, l0 <= x < h0 -> In x s)).
Proof.
(* Goal: forall (l0 h0 : Z) (_ : Z.lt l0 h0) (s : t) (_ : ok s), ok (remove l0 h0 s) *)
  induction 2; simpl.
- intuition. elim (H0 l0); omega.
- destruct (zle h0 h); simpl.
(* Goal: iff (@eq bool (orb (@proj_sumbool (Z.le l l0) (Z.gt l l0) (zle l l0)) (contains l0 h0 s)) true) (forall (x : Z) (_ : and (Z.le l0 x) (Z.lt x h0)), or (and (Z.le l x) (Z.lt x h)) (In x s)) *)
(* Goal: iff (@eq bool (contains l0 h0 s) true) (forall (x : Z) (_ : and (Z.le l0 x) (Z.lt x h0)), or (and (Z.le l x) (Z.lt x h)) (In x s)) *)
  destruct (zle l l0); simpl.
(* Goal: iff False (and (Z.le l x) (Z.lt x h)) *)
  intuition.
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  rewrite IHok. intuition. destruct (H3 x); auto. exfalso.
(* Goal: forall _ : Z.lt h l0, False *)
  destruct (H3 l0). omega. omega. exploit BELOW; eauto. omega.
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  rewrite IHok. intuition. destruct (H3 x); auto. exfalso.
(* Goal: forall _ : Z.lt h l0, False *)
  destruct (H3 h). omega. omega. exploit BELOW; eauto. omega.
Qed.

Fixpoint add (L H: Z) (s: t) {struct s} : t :=
  match s with
  | Nil => Cons L H Nil
  | Cons l h s' =>
      if zlt h L then Cons l h (add L H s')
      else if zlt H l then Cons L H s
      else add (Z.min l L) (Z.max h H) s'
  end.

Lemma In_add:
  forall x s, ok s -> forall l0 h0, (In x (add l0 h0 s) <-> l0 <= x < h0 \/ In x s).
Proof.
(* Goal: forall (s : t) (_ : ok s) (l0 h0 : Z) (_ : Z.lt l0 h0), ok (add l0 h0 s) *)
  induction 1; simpl; intros.
(* Goal: not False *)
  tauto.
(* Goal: ok (if zlt h l0 then Cons l h (remove l0 h0 s) else if zlt h0 l then Cons l h s else if zlt l l0 then if zlt h0 h then Cons l l0 (Cons h0 h s) else Cons l l0 (remove l0 h0 s) else if zlt h0 h then Cons h0 h s else remove l0 h0 s) *)
  destruct (zlt h l0).
(* Goal: not False *)
  simpl. rewrite IHok. tauto.
(* Goal: ok (if zlt h0 l then Cons l h s else if zlt l l0 then if zlt h0 h then Cons l l0 (Cons h0 h s) else Cons l l0 (remove l0 h0 s) else if zlt h0 h then Cons h0 h s else remove l0 h0 s) *)
  destruct (zlt h0 l).
(* Goal: not False *)
  simpl. tauto.
(* Goal: iff (In x (remove l0 h0 s)) (and (not (and (Z.le l0 x) (Z.lt x h0))) (or (and (Z.le l x) (Z.lt x h)) (In x s))) *)
  rewrite IHok. intuition.
(* Goal: not False *)
  assert (l0 <= x < h0 \/ l <= x < h) by xomega. tauto.
(* Goal: forall _ : Z.lt h l0, False *)
  left; xomega.
(* Goal: forall _ : Z.lt h l0, False *)
  left; xomega.
Qed.

Lemma add_ok:
  forall s, ok s -> forall l0 h0, l0 < h0 -> ok (add l0 h0 s).
Proof.
(* Goal: forall (s : t) (_ : ok s) (l0 h0 : Z) (_ : Z.lt l0 h0), ok (add l0 h0 s) *)
  induction 1; simpl; intros.
(* Goal: R.ok R.Nil *)
  constructor. auto. intros. inv H0. constructor.
(* Goal: ok (if zlt h l0 then Cons l h (remove l0 h0 s) else if zlt h0 l then Cons l h s else if zlt l l0 then if zlt h0 h then Cons l l0 (Cons h0 h s) else Cons l l0 (remove l0 h0 s) else if zlt h0 h then Cons h0 h s else remove l0 h0 s) *)
  destruct (zlt h l0).
(* Goal: @eq bool true true *)
  constructor; auto. intros. rewrite In_add in H1; auto.
(* Goal: forall _ : Z.lt h l0, False *)
  destruct H1. omega. auto.
(* Goal: ok (if zlt h0 l then Cons l h s else if zlt l l0 then if zlt h0 h then Cons l l0 (Cons h0 h s) else Cons l l0 (remove l0 h0 s) else if zlt h0 h then Cons h0 h s else remove l0 h0 s) *)
  destruct (zlt h0 l).
(* Goal: forall _ : Z.lt h l0, False *)
  constructor. auto. simpl; intros. destruct H1. omega. exploit BELOW; eauto. omega.
(* Goal: forall _ : Z.lt h l0, False *)
  constructor. omega. auto. auto.
(* Goal: forall _ : Z.lt h l0, False *)
  apply IHok. xomega.
Qed.

Fixpoint remove (L H: Z) (s: t) {struct s} : t :=
  match s with
  | Nil => Nil
  | Cons l h s' =>
      if zlt h L then Cons l h (remove L H s')
      else if zlt H l then s
      else if zlt l L then
        if zlt H h then Cons l L (Cons H h s') else Cons l L (remove L H s')
      else
        if zlt H h then Cons H h s' else remove L H s'
  end.

Lemma In_remove:
  forall x l0 h0 s, ok s ->
  (In x (remove l0 h0 s) <-> ~(l0 <= x < h0) /\ In x s).
Proof.
(* Goal: forall (s2 : t) (_ : ok s2), ok (inter (Cons l h s) s2) *)
  induction 1; simpl.
(* Goal: not False *)
  tauto.
(* Goal: ok (if zlt h l0 then Cons l h (remove l0 h0 s) else if zlt h0 l then Cons l h s else if zlt l l0 then if zlt h0 h then Cons l l0 (Cons h0 h s) else Cons l l0 (remove l0 h0 s) else if zlt h0 h then Cons h0 h s else remove l0 h0 s) *)
  destruct (zlt h l0).
(* Goal: forall _ : Z.lt h l0, False *)
  simpl. rewrite IHok. intuition omega.
(* Goal: ok (if zlt h0 l then Cons l h s else if zlt l l0 then if zlt h0 h then Cons l l0 (Cons h0 h s) else Cons l l0 (remove l0 h0 s) else if zlt h0 h then Cons h0 h s else remove l0 h0 s) *)
  destruct (zlt h0 l).
(* Goal: forall _ : Z.lt h l0, False *)
  simpl. intuition. exploit BELOW; eauto. omega.
(* Goal: False *)
  destruct (zlt l l0).
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@left (@eq Z h h0) (not (@eq Z h h0)) e0))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@right (@eq Z h h0) (not (@eq Z h h0)) n))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  destruct (zlt h0 h); simpl. clear IHok. split.
(* Goal: forall _ : or (and (Z.le l x) (Z.lt x l0)) (or (and (Z.le h0 x) (Z.lt x h)) (In x s)), and (not (and (Z.le l0 x) (Z.lt x h0))) (or (and (Z.le l x) (Z.lt x h)) (In x s)) *)
(* Goal: forall _ : and (not (and (Z.le l0 x) (Z.lt x h0))) (or (and (Z.le l x) (Z.lt x h)) (In x s)), or (and (Z.le l x) (Z.lt x l0)) (or (and (Z.le h0 x) (Z.lt x h)) (In x s)) *)
(* Goal: iff (or (and (Z.le l x) (Z.lt x l0)) (In x (remove l0 h0 s))) (and (not (and (Z.le l0 x) (Z.lt x h0))) (or (and (Z.le l x) (Z.lt x h)) (In x s))) *)
(* Goal: iff (In x (if zlt h0 h then Cons h0 h s else remove l0 h0 s)) (and (not (and (Z.le l0 x) (Z.lt x h0))) (or (and (Z.le l x) (Z.lt x h)) (In x s))) *)
  intros [A | [A | A]].
(* Goal: forall _ : Z.lt h l0, False *)
  split. omega. left; omega.
(* Goal: forall _ : Z.lt h l0, False *)
  split. omega. left; omega.
(* Goal: forall _ : Z.lt h l0, False *)
  split. exploit BELOW; eauto. omega. auto.
(* Goal: forall _ : and (not (and (Z.le l0 x) (Z.lt x h0))) (or (and (Z.le l x) (Z.lt x h)) (In x s)), or (and (Z.le l x) (Z.lt x l0)) (or (and (Z.le h0 x) (Z.lt x h)) (In x s)) *)
(* Goal: iff (or (and (Z.le l x) (Z.lt x l0)) (In x (remove l0 h0 s))) (and (not (and (Z.le l0 x) (Z.lt x h0))) (or (and (Z.le l x) (Z.lt x h)) (In x s))) *)
(* Goal: iff (In x (if zlt h0 h then Cons h0 h s else remove l0 h0 s)) (and (not (and (Z.le l0 x) (Z.lt x h0))) (or (and (Z.le l x) (Z.lt x h)) (In x s))) *)
  intros [A [B | B]].
(* Goal: forall _ : Z.lt h l0, False *)
  destruct (zlt x l0). left; omega. right; left; omega.
(* Goal: @eq bool true true *)
  auto.
(* Goal: forall _ : Z.lt h l0, False *)
  intuition omega.
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@left (@eq Z h h0) (not (@eq Z h h0)) e0))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@right (@eq Z h h0) (not (@eq Z h h0)) n))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  destruct (zlt h0 h); simpl.
(* Goal: forall _ : Z.lt h l0, False *)
  intuition. exploit BELOW; eauto. omega.
(* Goal: iff (In x (remove l0 h0 s)) (and (not (and (Z.le l0 x) (Z.lt x h0))) (or (and (Z.le l x) (Z.lt x h)) (In x s))) *)
  rewrite IHok. intuition. omegaContradiction.
Qed.

Lemma remove_ok:
  forall l0 h0, l0 < h0 -> forall s, ok s -> ok (remove l0 h0 s).
Proof.
(* Goal: forall (l0 h0 : Z) (_ : Z.lt l0 h0) (s : t) (_ : ok s), ok (remove l0 h0 s) *)
  induction 2; simpl.
(* Goal: R.ok R.Nil *)
  constructor.
(* Goal: ok (if zlt h l0 then Cons l h (remove l0 h0 s) else if zlt h0 l then Cons l h s else if zlt l l0 then if zlt h0 h then Cons l l0 (Cons h0 h s) else Cons l l0 (remove l0 h0 s) else if zlt h0 h then Cons h0 h s else remove l0 h0 s) *)
  destruct (zlt h l0).
(* Goal: not False *)
  constructor; auto. intros; apply BELOW. rewrite In_remove in H1; tauto.
(* Goal: ok (if zlt h0 l then Cons l h s else if zlt l l0 then if zlt h0 h then Cons l l0 (Cons h0 h s) else Cons l l0 (remove l0 h0 s) else if zlt h0 h then Cons h0 h s else remove l0 h0 s) *)
  destruct (zlt h0 l).
(* Goal: @eq bool true true *)
  constructor; auto.
(* Goal: False *)
  destruct (zlt l l0).
(* Goal: ok (if zlt h0 h then Cons h0 h s else remove l0 h0 s) *)
  destruct (zlt h0 h).
(* Goal: forall _ : Z.lt h l0, False *)
  constructor. omega. intros. inv H1. omega. exploit BELOW; eauto. omega.
(* Goal: forall _ : Z.lt h l0, False *)
  constructor. omega. auto. auto.
(* Goal: forall _ : Z.lt h l0, False *)
  constructor; auto. intros. rewrite In_remove in H1 by auto. destruct H1. exploit BELOW; eauto. omega.
(* Goal: ok (if zlt h0 h then Cons h0 h s else remove l0 h0 s) *)
  destruct (zlt h0 h).
(* Goal: @eq bool true true *)
  constructor; auto.
(* Goal: @eq bool true true *)
  auto.
Qed.

Fixpoint inter (s1 s2: t) {struct s1} : t :=
  let fix intr (s2: t) : t :=
    match s1, s2 with
    | Nil, _ => Nil
    | _, Nil => Nil
    | Cons l1 h1 s1', Cons l2 h2 s2' =>
        if zle h1 l2 then inter s1' s2
        else if zle h2 l1 then intr s2'
        else if zle l1 l2 then
          if zle h2 h1 then Cons l2 h2 (intr s2') else Cons l2 h1 (inter s1' s2)
        else
          if zle h1 h2 then Cons l1 h1 (inter s1' s2) else Cons l1 h2 (intr s2')
    end
  in intr s2.

Lemma In_inter:
  forall x s1, ok s1 -> forall s2, ok s2 ->
  (In x (inter s1 s2) <-> In x s1 /\ In x s2).
Proof.
(* Goal: forall (s1 : t) (_ : ok s1) (s2 : t) (_ : ok s2), ok (inter s1 s2) *)
  induction 1.
(* Goal: forall (s2 : t) (_ : ok s2), ok (inter (Cons l h s) s2) *)
  simpl. induction 1; simpl. tauto. tauto.
(* Goal: forall (s2 : t) (_ : ok s2), iff (In x (inter (Cons l h s) s2)) (and (In x (Cons l h s)) (In x s2)) *)
  assert (ok (Cons l h s)) by (constructor; auto).
(* Goal: forall (s2 : t) (_ : ok s2), ok (inter (Cons l h s) s2) *)
  induction 1; simpl.
(* Goal: not False *)
  tauto.
(* Goal: iff (In x (if zle h l0 then inter s (Cons l0 h0 s0) else if zle h0 l then (fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0 else if zle l l0 then if zle h0 h then Cons l0 h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0) else Cons l0 h (inter s (Cons l0 h0 s0)) else if zle h h0 then Cons l h (inter s (Cons l0 h0 s0)) else Cons l h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0))) (and (or (and (Z.le l x) (Z.lt x h)) (In x s)) (or (and (Z.le l0 x) (Z.lt x h0)) (In x s0))) *)
  assert (ok (Cons l0 h0 s0)) by (constructor; auto).
(* Goal: ok (if zle h l0 then inter s (Cons l0 h0 s0) else if zle h0 l then (fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0 else if zle l l0 then if zle h0 h then Cons l0 h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0) else Cons l0 h (inter s (Cons l0 h0 s0)) else if zle h h0 then Cons l h (inter s (Cons l0 h0 s0)) else Cons l h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0)) *)
  destruct (zle h l0).
(* Goal: iff False (and (Z.le l x) (Z.lt x h)) *)
  rewrite IHok; auto. simpl. intuition. omegaContradiction.
(* Goal: @eq bool true true *)
  exploit BELOW0; eauto. intros. omegaContradiction.
(* Goal: ok (if zle h0 l then (fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0 else if zle l l0 then if zle h0 h then Cons l0 h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0) else Cons l0 h (inter s (Cons l0 h0 s0)) else if zle h h0 then Cons l h (inter s (Cons l0 h0 s0)) else Cons l h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0)) *)
  destruct (zle h0 l).
(* Goal: iff False (and (Z.le l x) (Z.lt x h)) *)
  simpl in IHok0; rewrite IHok0. intuition. omegaContradiction.
(* Goal: False *)
  exploit BELOW; eauto. intros; omegaContradiction.
(* Goal: ok (if zle l l0 then if zle h0 h then Cons l0 h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0) else Cons l0 h (inter s (Cons l0 h0 s0)) else if zle h h0 then Cons l h (inter s (Cons l0 h0 s0)) else Cons l h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0)) *)
  destruct (zle l l0).
(* Goal: ok (if zle h0 h then Cons l0 h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0) else Cons l0 h (inter s (Cons l0 h0 s0))) *)
(* Goal: ok (if zle h h0 then Cons l h (inter s (Cons l0 h0 s0)) else Cons l h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0)) *)
  destruct (zle h0 h).
(* Goal: iff False (and (Z.le l x) (Z.lt x h)) *)
  simpl. simpl in IHok0; rewrite IHok0. intuition.
(* Goal: iff False (and (Z.le l x) (Z.lt x h)) *)
  simpl. rewrite IHok; auto. simpl. intuition.  exploit BELOW0; eauto. intros; omegaContradiction.
(* Goal: ok (if zle h h0 then Cons l h (inter s (Cons l0 h0 s0)) else Cons l h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0)) *)
  destruct (zle h h0).
(* Goal: iff False (and (Z.le l x) (Z.lt x h)) *)
  simpl. rewrite IHok; auto. simpl. intuition.
(* Goal: iff False (and (Z.le l x) (Z.lt x h)) *)
  simpl. simpl in IHok0; rewrite IHok0. intuition.
(* Goal: False *)
  exploit BELOW; eauto. intros; omegaContradiction.
Qed.

Lemma inter_ok:
  forall s1, ok s1 -> forall s2, ok s2 -> ok (inter s1 s2).
Proof.
(* Goal: forall (s1 : t) (_ : ok s1) (s2 : t) (_ : ok s2), ok (inter s1 s2) *)
  induction 1.
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@left (@eq Z h h0) (not (@eq Z h h0)) e0))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@right (@eq Z h h0) (not (@eq Z h h0)) n))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  intros; simpl. destruct s2; constructor.
(* Goal: @eq bool true true *)
  assert (ok (Cons l h s)). constructor; auto.
(* Goal: forall (s2 : t) (_ : ok s2), ok (inter (Cons l h s) s2) *)
  induction 1; simpl.
(* Goal: R.ok R.Nil *)
  constructor.
(* Goal: @eq bool true true *)
  assert (ok (Cons l0 h0 s0)). constructor; auto.
(* Goal: ok (if zle h l0 then inter s (Cons l0 h0 s0) else if zle h0 l then (fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0 else if zle l l0 then if zle h0 h then Cons l0 h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0) else Cons l0 h (inter s (Cons l0 h0 s0)) else if zle h h0 then Cons l h (inter s (Cons l0 h0 s0)) else Cons l h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0)) *)
  destruct (zle h l0).
(* Goal: @eq bool true true *)
  auto.
(* Goal: ok (if zle h0 l then (fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0 else if zle l l0 then if zle h0 h then Cons l0 h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0) else Cons l0 h (inter s (Cons l0 h0 s0)) else if zle h h0 then Cons l h (inter s (Cons l0 h0 s0)) else Cons l h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0)) *)
  destruct (zle h0 l).
(* Goal: @eq bool true true *)
  auto.
(* Goal: ok (if zle l l0 then if zle h0 h then Cons l0 h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0) else Cons l0 h (inter s (Cons l0 h0 s0)) else if zle h h0 then Cons l h (inter s (Cons l0 h0 s0)) else Cons l h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0)) *)
  destruct (zle l l0).
(* Goal: ok (if zle h0 h then Cons l0 h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0) else Cons l0 h (inter s (Cons l0 h0 s0))) *)
(* Goal: ok (if zle h h0 then Cons l h (inter s (Cons l0 h0 s0)) else Cons l h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0)) *)
  destruct (zle h0 h).
(* Goal: @eq bool true true *)
  constructor; auto. intros.
(* Goal: Z.lt h0 x *)
(* Goal: ok ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0) *)
  assert (In x (inter (Cons l h s) s0)) by exact H3.
(* Goal: not False *)
  rewrite In_inter in H4; auto. apply BELOW0. tauto.
(* Goal: not False *)
  constructor. omega. intros. rewrite In_inter in H3; auto. apply BELOW. tauto.
(* Goal: @eq bool true true *)
  auto.
(* Goal: ok (if zle h h0 then Cons l h (inter s (Cons l0 h0 s0)) else Cons l h0 ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0)) *)
  destruct (zle h h0).
(* Goal: not False *)
  constructor. omega. intros. rewrite In_inter in H3; auto. apply BELOW. tauto.
(* Goal: @eq bool true true *)
  auto.
(* Goal: forall _ : Z.lt h l0, False *)
  constructor. omega. intros.
(* Goal: Z.lt h0 x *)
(* Goal: ok ((fix intr (s2 : t) : t := match s2 with | Nil => Nil | Cons l2 h2 s2' => if zle h l2 then inter s s2 else if zle h2 l then intr s2' else if zle l l2 then if zle h2 h then Cons l2 h2 (intr s2') else Cons l2 h (inter s s2) else if zle h h2 then Cons l h (inter s s2) else Cons l h2 (intr s2') end) s0) *)
  assert (In x (inter (Cons l h s) s0)) by exact H3.
(* Goal: not False *)
  rewrite In_inter in H4; auto. apply BELOW0. tauto.
(* Goal: @eq bool true true *)
  auto.
Qed.

Fixpoint union (s1 s2: t) : t :=
  match s1, s2 with
  | Nil, _ => s2
  | _, Nil => s1
  | Cons l1 h1 s1', Cons l2 h2 s2' => add l1 h1 (add l2 h2 (union s1' s2'))
  end.

Lemma In_ok_union:
  forall s1, ok s1 -> forall s2, ok s2 ->
  ok (union s1 s2) /\ (forall x, In x s1 \/ In x s2 <-> In x (union s1 s2)).
Proof.
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@left (@eq Z h h0) (not (@eq Z h h0)) e0))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@right (@eq Z h h0) (not (@eq Z h h0)) n))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  induction 1; destruct 1; simpl.
(* Goal: not False *)
  split. constructor. tauto.
(* Goal: not False *)
  split. constructor; auto. tauto.
(* Goal: not False *)
  split. constructor; auto. tauto.
(* Goal: @eq bool true true *)
  destruct (IHok s0) as [A B]; auto.
(* Goal: @eq bool true true *)
  split. apply add_ok; auto. apply add_ok; auto.
  intros. rewrite In_add. rewrite In_add. rewrite <- B. tauto. auto. apply add_ok; auto.
Qed.

Fixpoint beq (s1 s2: t) : bool :=
  match s1, s2 with
  | Nil, Nil => true
  | Cons l1 h1 t1, Cons l2 h2 t2 => zeq l1 l2 && zeq h1 h2 && beq t1 t2
  | _, _ => false
  end.

Lemma beq_spec:
  forall s1, ok s1 -> forall s2, ok s2 ->
  (beq s1 s2 = true <-> (forall x, In x s1 <-> In x s2)).
Proof.
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@left (@eq Z h h0) (not (@eq Z h h0)) e0))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@right (@eq Z h h0) (not (@eq Z h h0)) n))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  induction 1; destruct 1; simpl.
- tauto.
- split; intros. discriminate. exfalso. apply (H0 l). left; omega.
- split; intros. discriminate. exfalso. apply (H0 l). left; omega.
- split; intros.
+ InvBooleans. subst. rewrite IHok in H3 by auto. rewrite H3. tauto.
+ destruct (zeq l l0). destruct (zeq h h0). simpl. subst.
(* Goal: iff (@eq bool true true) (forall (x : Z) (_ : and (Z.le l x) (Z.lt x h)), R.In x (@proj1_sig R.t (fun r : R.t => R.ok r) s)) *)
  apply IHok. auto. intros; split; intros.
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  destruct (proj1 (H1 x)); auto. exfalso. exploit BELOW; eauto. omega.
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  destruct (proj2 (H1 x)); auto. exfalso. exploit BELOW0; eauto. omega.
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  exfalso. subst l0. destruct (zlt h h0).
(* Goal: forall _ : Z.lt h l0, False *)
  destruct (proj2 (H1 h)). left; omega. omega. exploit BELOW; eauto. omega.
(* Goal: forall _ : Z.lt h l0, False *)
  destruct (proj1 (H1 h0)). left; omega. omega. exploit BELOW0; eauto. omega.
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  exfalso. destruct (zlt l l0).
(* Goal: forall _ : Z.lt h l0, False *)
  destruct (proj1 (H1 l)). left; omega. omega. exploit BELOW0; eauto. omega.
(* Goal: forall _ : Z.lt h l0, False *)
  destruct (proj2 (H1 l0)). left; omega. omega. exploit BELOW; eauto. omega.
Qed.

End R.

(** Exported interface, wrapping the [ok] invariant in a dependent type. *)

Definition t := { r: R.t | R.ok r }.

Program Definition In (x: Z) (s: t) := R.In x s.

Program Definition empty : t := R.Nil.
Next Obligation. constructor. Qed.

Theorem In_empty: forall x, ~(In x empty).
Proof.
(* Goal: not False *)
  unfold In; intros; simpl. tauto.
Qed.

Program Definition interval (l h: Z) : t :=
  if zlt l h then R.Cons l h R.Nil else R.Nil.
Next Obligation.
(* Goal: not False *)
  constructor; auto. simpl; tauto. constructor.
Qed.
Next Obligation.
(* Goal: R.ok R.Nil *)
  constructor.
Qed.

Theorem In_interval: forall x l h, In x (interval l h) <-> l <= x < h.
Proof.
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@left (@eq Z h h0) (not (@eq Z h h0)) e0))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@right (@eq Z h h0) (not (@eq Z h h0)) n))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  intros. unfold In, interval; destruct (zlt l h); simpl.
(* Goal: iff False (and (Z.le l x) (Z.lt x h)) *)
  intuition.
(* Goal: iff False (and (Z.le l x) (Z.lt x h)) *)
  intuition.
Qed.

Program Definition add (l h: Z) (s: t) : t :=
  if zlt l h then R.add l h s else s.
Next Obligation.
(* Goal: @eq bool true true *)
  apply R.add_ok. apply proj2_sig. auto.
Qed.

Theorem In_add: forall x l h s, In x (add l h s) <-> l <= x < h \/ In x s.
Proof.
(* Goal: forall x l h : Z, iff (In x (interval l h)) (and (Z.le l x) (Z.lt x h)) *)
  unfold add, In; intros.
(* Goal: iff (@eq bool (if zlt l h then R.contains l h (@proj1_sig R.t (fun r : R.t => R.ok r) s) else true) true) (forall (x : Z) (_ : and (Z.le l x) (Z.lt x h)), R.In x (@proj1_sig R.t (fun r : R.t => R.ok r) s)) *)
  destruct (zlt l h).
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@left (@eq Z h h0) (not (@eq Z h h0)) e0))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@right (@eq Z h h0) (not (@eq Z h h0)) n))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  simpl. apply R.In_add. apply proj2_sig.
(* Goal: iff False (and (Z.le l x) (Z.lt x h)) *)
  intuition. omegaContradiction.
Qed.

Program Definition remove (l h: Z) (s: t) : t :=
  if zlt l h then R.remove l h s else s.
Next Obligation.
(* Goal: @eq bool true true *)
  apply R.remove_ok. auto. apply proj2_sig.
Qed.

Theorem In_remove: forall x l h s, In x (remove l h s) <-> ~(l <= x < h) /\ In x s.
Proof.
(* Goal: forall x l h : Z, iff (In x (interval l h)) (and (Z.le l x) (Z.lt x h)) *)
  unfold remove, In; intros.
(* Goal: iff (@eq bool (if zlt l h then R.contains l h (@proj1_sig R.t (fun r : R.t => R.ok r) s) else true) true) (forall (x : Z) (_ : and (Z.le l x) (Z.lt x h)), R.In x (@proj1_sig R.t (fun r : R.t => R.ok r) s)) *)
  destruct (zlt l h).
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@left (@eq Z h h0) (not (@eq Z h h0)) e0))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@right (@eq Z h h0) (not (@eq Z h h0)) n))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  simpl. apply R.In_remove. apply proj2_sig.
(* Goal: iff False (and (Z.le l x) (Z.lt x h)) *)
  intuition.
Qed.

Program Definition inter (s1 s2: t) : t := R.inter s1 s2.
Next Obligation. apply R.inter_ok; apply proj2_sig. Qed.

Theorem In_inter: forall x s1 s2, In x (inter s1 s2) <-> In x s1 /\ In x s2.
Proof.
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@left (@eq Z h h0) (not (@eq Z h h0)) e0))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@right (@eq Z h h0) (not (@eq Z h h0)) n))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  unfold inter, In; intros; simpl. apply R.In_inter; apply proj2_sig.
Qed.

Program Definition union (s1 s2: t) : t := R.union s1 s2.
Next Obligation.
(* Goal: @eq bool true true *)
  destruct (R.In_ok_union _ (proj2_sig s1) _ (proj2_sig s2)). auto.
Qed.

Theorem In_union: forall x s1 s2, In x (union s1 s2) <-> In x s1 \/ In x s2.
Proof.
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@left (@eq Z h h0) (not (@eq Z h h0)) e0))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@left (@eq Z l l0) (not (@eq Z l l0)) e)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (@right (@eq Z h h0) (not (@eq Z h h0)) n))) (beq s s0)) true *)
(* Goal: @eq bool (andb (andb (@proj_sumbool (@eq Z l l0) (not (@eq Z l l0)) (@right (@eq Z l l0) (not (@eq Z l l0)) n)) (@proj_sumbool (@eq Z h h0) (not (@eq Z h h0)) (zeq h h0))) (beq s s0)) true *)
  unfold union, In; intros; simpl.
(* Goal: iff (R.In x (R.union (@proj1_sig R.t (fun r : R.t => R.ok r) s1) (@proj1_sig R.t (fun r : R.t => R.ok r) s2))) (or (R.In x (@proj1_sig R.t (fun r : R.t => R.ok r) s1)) (R.In x (@proj1_sig R.t (fun r : R.t => R.ok r) s2))) *)
  destruct (R.In_ok_union _ (proj2_sig s1) _ (proj2_sig s2)).
(* Goal: not False *)
  generalize (H0 x); tauto.
Qed.

Program Definition mem (x: Z) (s: t) := R.mem x s.

Theorem mem_spec: forall x s, mem x s = true <-> In x s.
Proof.
(* Goal: forall x l h : Z, iff (In x (interval l h)) (and (Z.le l x) (Z.lt x h)) *)
  unfold mem, In; intros. apply R.mem_In. apply proj2_sig.
Qed.

Program Definition contains (l h: Z) (s: t) :=
  if zlt l h then R.contains l h s else true.

Theorem contains_spec:
  forall l h s, contains l h s = true <-> (forall x, l <= x < h -> In x s).
Proof.
(* Goal: forall x l h : Z, iff (In x (interval l h)) (and (Z.le l x) (Z.lt x h)) *)
  unfold contains, In; intros. destruct (zlt l h).
(* Goal: @eq bool true true *)
  apply R.contains_In. auto. apply proj2_sig.
(* Goal: iff (@eq bool true true) (forall (x : Z) (_ : and (Z.le l x) (Z.lt x h)), R.In x (@proj1_sig R.t (fun r : R.t => R.ok r) s)) *)
  split; intros. omegaContradiction. auto.
Qed.

Program Definition beq (s1 s2: t) : bool := R.beq s1 s2.

Theorem beq_spec:
  forall s1 s2, beq s1 s2 = true <-> (forall x, In x s1 <-> In x s2).
Proof.
(* Goal: forall x l h : Z, iff (In x (interval l h)) (and (Z.le l x) (Z.lt x h)) *)
  unfold mem, In; intros. apply R.beq_spec; apply proj2_sig.
Qed.

End ISet.




