From 7698300cfe2d3f944ce2e1d4a60a263620487718 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 20 Dec 2013 13:05:53 +0000 Subject: Merge of branch value-analysis. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/IntvSets.v | 410 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 410 insertions(+) create mode 100644 lib/IntvSets.v (limited to 'lib/IntvSets.v') diff --git a/lib/IntvSets.v b/lib/IntvSets.v new file mode 100644 index 00000000..9f1a895f --- /dev/null +++ b/lib/IntvSets.v @@ -0,0 +1,410 @@ +(* *********************************************************************) +(* *) +(* 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. + induction 1; simpl. +- intuition congruence. +- destruct (zlt x h). ++ destruct (zle l x); simpl. + * tauto. + * split; intros. congruence. + 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. + induction 2; simpl. +- intuition. elim (H0 l0); omega. +- destruct (zle h0 h); simpl. + destruct (zle l l0); simpl. + intuition. + rewrite IHok. intuition. destruct (H3 x); auto. exfalso. + destruct (H3 l0). omega. omega. exploit BELOW; eauto. omega. + rewrite IHok. intuition. destruct (H3 x); auto. exfalso. + 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. + induction 1; simpl; intros. + tauto. + destruct (zlt h l0). + simpl. rewrite IHok. tauto. + destruct (zlt h0 l). + simpl. tauto. + rewrite IHok. intuition. + assert (l0 <= x < h0 \/ l <= x < h) by xomega. tauto. + left; xomega. + left; xomega. +Qed. + +Lemma add_ok: + forall s, ok s -> forall l0 h0, l0 < h0 -> ok (add l0 h0 s). +Proof. + induction 1; simpl; intros. + constructor. auto. intros. inv H0. constructor. + destruct (zlt h l0). + constructor; auto. intros. rewrite In_add in H1; auto. + destruct H1. omega. auto. + destruct (zlt h0 l). + constructor. auto. simpl; intros. destruct H1. omega. exploit BELOW; eauto. omega. + constructor. omega. auto. auto. + 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. + induction 1; simpl. + tauto. + destruct (zlt h l0). + simpl. rewrite IHok. intuition omega. + destruct (zlt h0 l). + simpl. intuition. exploit BELOW; eauto. omega. + destruct (zlt l l0). + destruct (zlt h0 h); simpl. clear IHok. split. + intros [A | [A | A]]. + split. omega. left; omega. + split. omega. left; omega. + split. exploit BELOW; eauto. omega. auto. + intros [A [B | B]]. + destruct (zlt x l0). left; omega. right; left; omega. + auto. + intuition omega. + destruct (zlt h0 h); simpl. + intuition. exploit BELOW; eauto. omega. + rewrite IHok. intuition. omegaContradiction. +Qed. + +Lemma remove_ok: + forall l0 h0, l0 < h0 -> forall s, ok s -> ok (remove l0 h0 s). +Proof. + induction 2; simpl. + constructor. + destruct (zlt h l0). + constructor; auto. intros; apply BELOW. rewrite In_remove in H1; tauto. + destruct (zlt h0 l). + constructor; auto. + destruct (zlt l l0). + destruct (zlt h0 h). + constructor. omega. intros. inv H1. omega. exploit BELOW; eauto. omega. + constructor. omega. auto. auto. + constructor; auto. intros. rewrite In_remove in H1 by auto. destruct H1. exploit BELOW; eauto. omega. + destruct (zlt h0 h). + constructor; auto. + 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. + induction 1. + simpl. induction 1; simpl. tauto. tauto. + assert (ok (Cons l h s)) by (constructor; auto). + induction 1; simpl. + tauto. + assert (ok (Cons l0 h0 s0)) by (constructor; auto). + destruct (zle h l0). + rewrite IHok; auto. simpl. intuition. omegaContradiction. + exploit BELOW0; eauto. intros. omegaContradiction. + destruct (zle h0 l). + simpl in IHok0; rewrite IHok0. intuition. omegaContradiction. + exploit BELOW; eauto. intros; omegaContradiction. + destruct (zle l l0). + destruct (zle h0 h). + simpl. simpl in IHok0; rewrite IHok0. intuition. + simpl. rewrite IHok; auto. simpl. intuition. exploit BELOW0; eauto. intros; omegaContradiction. + destruct (zle h h0). + simpl. rewrite IHok; auto. simpl. intuition. + simpl. simpl in IHok0; rewrite IHok0. intuition. + exploit BELOW; eauto. intros; omegaContradiction. +Qed. + +Lemma inter_ok: + forall s1, ok s1 -> forall s2, ok s2 -> ok (inter s1 s2). +Proof. + induction 1. + intros; simpl. destruct s2; constructor. + assert (ok (Cons l h s)). constructor; auto. + induction 1; simpl. + constructor. + assert (ok (Cons l0 h0 s0)). constructor; auto. + destruct (zle h l0). + auto. + destruct (zle h0 l). + auto. + destruct (zle l l0). + destruct (zle h0 h). + constructor; auto. intros. + assert (In x (inter (Cons l h s) s0)) by exact H3. + rewrite In_inter in H4; auto. apply BELOW0. tauto. + constructor. omega. intros. rewrite In_inter in H3; auto. apply BELOW. tauto. + auto. + destruct (zle h h0). + constructor. omega. intros. rewrite In_inter in H3; auto. apply BELOW. tauto. + auto. + constructor. omega. intros. + assert (In x (inter (Cons l h s) s0)) by exact H3. + rewrite In_inter in H4; auto. apply BELOW0. tauto. + 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. + induction 1; destruct 1; simpl. + split. constructor. tauto. + split. constructor; auto. tauto. + split. constructor; auto. tauto. + destruct (IHok s0) as [A B]; auto. + 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. + 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. + apply IHok. auto. intros; split; intros. + destruct (proj1 (H1 x)); auto. exfalso. exploit BELOW; eauto. omega. + destruct (proj2 (H1 x)); auto. exfalso. exploit BELOW0; eauto. omega. + exfalso. subst l0. destruct (zlt h h0). + destruct (proj2 (H1 h)). left; omega. omega. exploit BELOW; eauto. omega. + destruct (proj1 (H1 h0)). left; omega. omega. exploit BELOW0; eauto. omega. + exfalso. destruct (zlt l l0). + destruct (proj1 (H1 l)). left; omega. omega. exploit BELOW0; eauto. omega. + 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. + 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. + constructor; auto. simpl; tauto. constructor. +Qed. +Next Obligation. + constructor. +Qed. + +Theorem In_interval: forall x l h, In x (interval l h) <-> l <= x < h. +Proof. + intros. unfold In, interval; destruct (zlt l h); simpl. + intuition. + 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. + 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. + unfold add, In; intros. + destruct (zlt l h). + simpl. apply R.In_add. apply proj2_sig. + 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. + 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. + unfold remove, In; intros. + destruct (zlt l h). + simpl. apply R.In_remove. apply proj2_sig. + 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. + 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. + 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. + unfold union, In; intros; simpl. + destruct (R.In_ok_union _ (proj2_sig s1) _ (proj2_sig s2)). + 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. + 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. + unfold contains, In; intros. destruct (zlt l h). + apply R.contains_In. auto. apply proj2_sig. + 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. + unfold mem, In; intros. apply R.beq_spec; apply proj2_sig. +Qed. + +End ISet. + + + + -- cgit