From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Camlcoq.ml | 5 + lib/Coqlib.v | 21 +++ lib/FSetAVLplus.v | 513 ++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/Floats.v | 72 +++----- lib/Integers.v | 464 +++++++++++++++++++++++++++++++++++++++++++---- lib/Lattice.v | 100 +++++++++++ lib/Maps.v | 524 ++++++++++++++++++++---------------------------------- lib/Ordered.v | 30 ++++ 8 files changed, 1321 insertions(+), 408 deletions(-) create mode 100644 lib/FSetAVLplus.v (limited to 'lib') diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index d99e20f..e057771 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -252,6 +252,11 @@ let camlstring_of_coqstring (s: char list) = | c :: s -> r.[pos] <- c; fill (pos + 1) s in fill 0 s +let coqstring_of_camlstring s = + let rec cstring accu pos = + if pos < 0 then accu else cstring (s.[pos] :: accu) (pos - 1) + in cstring [] (String.length s - 1) + (* Floats *) let coqfloat_of_camlfloat f = diff --git a/lib/Coqlib.v b/lib/Coqlib.v index b936b9b..ce5d94e 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -559,6 +559,16 @@ Proof. Defined. Global Opaque Zdivide_dec. +Lemma Zdivide_interval: + forall a b c, + 0 < c -> 0 <= a < b -> (c | a) -> (c | b) -> 0 <= a <= b - c. +Proof. + intros. destruct H1 as [x EQ1]. destruct H2 as [y EQ2]. subst. destruct H0. + split. omega. exploit Zmult_lt_reg_r; eauto. intros. + replace (y * c - c) with ((y - 1) * c) by ring. + apply Zmult_le_compat_r; omega. +Qed. + (** Conversion from [Z] to [nat]. *) Definition nat_of_Z: Z -> nat := Z.to_nat. @@ -1250,6 +1260,17 @@ Proof. intros. unfold proj_sumbool. destruct a. auto. contradiction. Qed. +Ltac InvBooleans := + match goal with + | [ H: _ && _ = true |- _ ] => + destruct (andb_prop _ _ H); clear H; InvBooleans + | [ H: _ || _ = false |- _ ] => + destruct (orb_false_elim _ _ H); clear H; InvBooleans + | [ H: proj_sumbool ?x = true |- _ ] => + generalize (proj_sumbool_true _ H); clear H; intro; InvBooleans + | _ => idtac + end. + Section DECIDABLE_EQUALITY. Variable A: Type. diff --git a/lib/FSetAVLplus.v b/lib/FSetAVLplus.v new file mode 100644 index 0000000..5f5cc51 --- /dev/null +++ b/lib/FSetAVLplus.v @@ -0,0 +1,513 @@ +(* *********************************************************************) +(* *) +(* 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** An extension of [FSetAVL] (finite sets as balanced binary search trees) + with extra interval-based operations, more efficient than standard + operations. *) + +Require Import FSetInterface. +Require FSetAVL. +Require Import Coqlib. + +Module Make(X: OrderedType). + +Include FSetAVL.Make(X). + +Module Raw := MSet.Raw. + +Section MEM_BETWEEN. + +(** [mem_between above below s] is [true] iff there exists an element of [s] + that belongs to the interval described by the predicates [above] and [below]. + Using the monotonicity of [above] and [below], the implementation of + [mem_between] avoids traversing the subtrees of [s] that + lie entirely outside the interval of interest. *) + +Variable above_low_bound: elt -> bool. +Variable below_high_bound: elt -> bool. + +Fixpoint raw_mem_between (m: Raw.tree) : bool := + match m with + | Raw.Leaf => false + | Raw.Node _ l x r => + if above_low_bound x + then if below_high_bound x + then true + else raw_mem_between l + else raw_mem_between r + end. + +Definition mem_between (m: t) : bool := raw_mem_between m.(MSet.this). + +Hypothesis above_monotone: + forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true. +Hypothesis below_monotone: + forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true. + +Lemma raw_mem_between_1: + forall m, + raw_mem_between m = true -> + exists x, Raw.In x m /\ above_low_bound x = true /\ below_high_bound x = true. +Proof. + induction m; simpl; intros. +- discriminate. +- destruct (above_low_bound t1) eqn: LB; [destruct (below_high_bound t1) eqn: HB | idtac]. + + (* in interval *) + exists t1; split; auto. apply Raw.IsRoot. auto. + + (* above interval *) + exploit IHm1; auto. intros [x' [A B]]. exists x'; split; auto. apply Raw.InLeft; auto. + + (* below interval *) + exploit IHm2; auto. intros [x' [A B]]. exists x'; split; auto. apply Raw.InRight; auto. +Qed. + +Lemma raw_mem_between_2: + forall x m, + Raw.bst m -> + Raw.In x m -> above_low_bound x = true -> below_high_bound x = true -> + raw_mem_between m = true. +Proof. + induction 1; simpl; intros. +- inv H. +- rewrite Raw.In_node_iff in H1. + destruct (above_low_bound x0) eqn: LB; [destruct (below_high_bound x0) eqn: HB | idtac]. + + (* in interval *) + auto. + + (* above interval *) + assert (X.eq x x0 \/ X.lt x0 x -> False). + { intros. exploit below_monotone; eauto. congruence. } + intuition. + + assert (X.eq x x0 \/ X.lt x x0 -> False). + { intros. exploit above_monotone; eauto. congruence. } + intuition. +Qed. + +Theorem mem_between_1: + forall s, + mem_between s = true -> + exists x, In x s /\ above_low_bound x = true /\ below_high_bound x = true. +Proof. + intros. apply raw_mem_between_1. auto. +Qed. + +Theorem mem_between_2: + forall x s, + In x s -> above_low_bound x = true -> below_high_bound x = true -> + mem_between s = true. +Proof. + unfold mem_between; intros. apply raw_mem_between_2 with x; auto. apply MSet.is_ok. +Qed. + +End MEM_BETWEEN. + +Section ELEMENTS_BETWEEN. + +(** [elements_between above below s] returns the set of elements of [s] + that belong to the interval [above,below]. *) + +Variable above_low_bound: elt -> bool. +Variable below_high_bound: elt -> bool. + +Fixpoint raw_elements_between (m: Raw.tree) : Raw.tree := + match m with + | Raw.Leaf => Raw.Leaf + | Raw.Node _ l x r => + if above_low_bound x then + if below_high_bound x then + Raw.join (raw_elements_between l) x (raw_elements_between r) + else + raw_elements_between l + else + raw_elements_between r + end. + +Remark In_raw_elements_between_1: + forall x m, + Raw.In x (raw_elements_between m) -> Raw.In x m. +Proof. + induction m; simpl; intros. +- inv H. +- rewrite Raw.In_node_iff. + destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H. + + rewrite Raw.join_spec in H. intuition. + + left; apply IHm1; auto. + + right; right; apply IHm2; auto. +Qed. + +Lemma raw_elements_between_ok: + forall m, Raw.bst m -> Raw.bst (raw_elements_between m). +Proof. + induction 1; simpl. +- constructor. +- destruct (above_low_bound x) eqn:LB; [destruct (below_high_bound x) eqn: RB | idtac]; simpl. + + apply Raw.join_ok; auto. + red; intros. apply l0. apply In_raw_elements_between_1; auto. + red; intros. apply g. apply In_raw_elements_between_1; auto. + + auto. + + auto. +Qed. + +Definition elements_between (s: t) : t := + @MSet.Mkt (raw_elements_between s.(MSet.this)) (raw_elements_between_ok s.(MSet.this) s.(MSet.is_ok)). + +Hypothesis above_monotone: + forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true. +Hypothesis below_monotone: + forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true. + +Remark In_raw_elements_between_2: + forall x m, + Raw.In x (raw_elements_between m) -> above_low_bound x = true /\ below_high_bound x = true. +Proof. + induction m; simpl; intros. +- inv H. +- destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H. + + rewrite Raw.join_spec in H. intuition. + apply above_monotone with t1; auto. + apply below_monotone with t1; auto. + + auto. + + auto. +Qed. + +Remark In_raw_elements_between_3: + forall x m, + Raw.bst m -> + Raw.In x m -> above_low_bound x = true -> below_high_bound x = true -> + Raw.In x (raw_elements_between m). +Proof. + induction 1; simpl; intros. +- auto. +- rewrite Raw.In_node_iff in H1. + destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]. + + rewrite Raw.join_spec. intuition. + + assert (X.eq x x0 \/ X.lt x0 x -> False). + { intros. exploit below_monotone; eauto. congruence. } + intuition. elim H7. apply g. auto. + + assert (X.eq x x0 \/ X.lt x x0 -> False). + { intros. exploit above_monotone; eauto. congruence. } + intuition. elim H7. apply l0. auto. +Qed. + +Theorem elements_between_iff: + forall x s, + In x (elements_between s) <-> In x s /\ above_low_bound x = true /\ below_high_bound x = true. +Proof. + intros. unfold elements_between, In; simpl. split. + intros. split. apply In_raw_elements_between_1; auto. eapply In_raw_elements_between_2; eauto. + intros [A [B C]]. apply In_raw_elements_between_3; auto. apply MSet.is_ok. +Qed. + +End ELEMENTS_BETWEEN. + +Section FOR_ALL_BETWEEN. + +(** [for_all_between pred above below s] is [true] iff all elements of [s] + in a given variation interval satisfy predicate [pred]. + The variation interval is given by two predicates [above] and [below] + which must both hold if the element is part of the interval. + Using the monotonicity of [above] and [below], the implementation of + [for_all_between] avoids traversing the subtrees of [s] that + lie entirely outside the interval of interest. *) + +Variable pred: elt -> bool. +Variable above_low_bound: elt -> bool. +Variable below_high_bound: elt -> bool. + +Fixpoint raw_for_all_between (m: Raw.tree) : bool := + match m with + | Raw.Leaf => true + | Raw.Node _ l x r => + if above_low_bound x + then if below_high_bound x + then raw_for_all_between l && pred x && raw_for_all_between r + else raw_for_all_between l + else raw_for_all_between r + end. + +Definition for_all_between (m: t) : bool := raw_for_all_between m.(MSet.this). + +Hypothesis pred_compat: + forall x1 x2, X.eq x1 x2 -> pred x1 = pred x2. +Hypothesis above_monotone: + forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true. +Hypothesis below_monotone: + forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true. + +Lemma raw_for_all_between_1: + forall x m, + Raw.bst m -> + raw_for_all_between m = true -> + Raw.In x m -> + above_low_bound x = true -> + below_high_bound x = true -> + pred x = true. +Proof. + induction 1; simpl; intros. +- inv H0. +- destruct (above_low_bound x0) eqn: LB; [destruct (below_high_bound x0) eqn: HB | idtac]. + + (* in interval *) + destruct (andb_prop _ _ H1) as [P C]. destruct (andb_prop _ _ P) as [A B]. clear H1 P. + inv H2. + * erewrite pred_compat; eauto. + * apply IHbst1; auto. + * apply IHbst2; auto. + + (* above interval *) + inv H2. + * assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). + congruence. + * apply IHbst1; auto. + * assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). + congruence. + + (* below interval *) + inv H2. + * assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). + congruence. + * assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). + congruence. + * apply IHbst2; auto. +Qed. + +Lemma raw_for_all_between_2: + forall m, + Raw.bst m -> + (forall x, Raw.In x m -> above_low_bound x = true -> below_high_bound x = true -> pred x = true) -> + raw_for_all_between m = true. +Proof. + induction 1; intros; simpl. +- auto. +- destruct (above_low_bound x) eqn: LB; [destruct (below_high_bound x) eqn: HB | idtac]. + + (* in interval *) + rewrite IHbst1. rewrite (H1 x). rewrite IHbst2. auto. + intros. apply H1; auto. apply Raw.InRight; auto. + apply Raw.IsRoot. reflexivity. auto. auto. + intros. apply H1; auto. apply Raw.InLeft; auto. + + (* above interval *) + apply IHbst1. intros. apply H1; auto. apply Raw.InLeft; auto. + + (* below interval *) + apply IHbst2. intros. apply H1; auto. apply Raw.InRight; auto. +Qed. + +Theorem for_all_between_iff: + forall s, + for_all_between s = true <-> (forall x, In x s -> above_low_bound x = true -> below_high_bound x = true -> pred x = true). +Proof. + unfold for_all_between; intros; split; intros. +- eapply raw_for_all_between_1; eauto. apply MSet.is_ok. +- apply raw_for_all_between_2; auto. apply MSet.is_ok. +Qed. + +End FOR_ALL_BETWEEN. + +Section PARTITION_BETWEEN. + +Variable above_low_bound: elt -> bool. +Variable below_high_bound: elt -> bool. + +Fixpoint raw_partition_between (m: Raw.tree) : Raw.tree * Raw.tree := + match m with + | Raw.Leaf => (Raw.Leaf, Raw.Leaf) + | Raw.Node _ l x r => + if above_low_bound x then + if below_high_bound x then + (let (l1, l2) := raw_partition_between l in + let (r1, r2) := raw_partition_between r in + (Raw.join l1 x r1, Raw.concat l2 r2)) + else + (let (l1, l2) := raw_partition_between l in + (l1, Raw.join l2 x r)) + else + (let (r1, r2) := raw_partition_between r in + (r1, Raw.join l x r2)) + end. + +Remark In_raw_partition_between_1: + forall x m, + Raw.In x (fst (raw_partition_between m)) -> Raw.In x m. +Proof. + induction m; simpl; intros. +- inv H. +- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. + destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *. + destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H. + + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition. + + rewrite Raw.In_node_iff. intuition. + + rewrite Raw.In_node_iff. intuition. +Qed. + +Remark In_raw_partition_between_2: + forall x m, + Raw.In x (snd (raw_partition_between m)) -> Raw.In x m. +Proof. + induction m; simpl; intros. +- inv H. +- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. + destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *. + destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H. + + rewrite Raw.concat_spec in H. rewrite Raw.In_node_iff. intuition. + + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition. + + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition. +Qed. + +Lemma raw_partition_between_ok: + forall m, Raw.bst m -> Raw.bst (fst (raw_partition_between m)) /\ Raw.bst (snd (raw_partition_between m)). +Proof. + induction 1; simpl. +- split; constructor. +- destruct IHbst1 as [L1 L2]. destruct IHbst2 as [R1 R2]. + destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. + destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *. + destruct (above_low_bound x) eqn:LB; [destruct (below_high_bound x) eqn: RB | idtac]; simpl. + + split. + apply Raw.join_ok; auto. + red; intros. apply l0. apply In_raw_partition_between_1. rewrite LEQ; auto. + red; intros. apply g. apply In_raw_partition_between_1. rewrite REQ; auto. + apply Raw.concat_ok; auto. + intros. transitivity x. + apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto. + apply g. apply In_raw_partition_between_2. rewrite REQ; auto. + + split. + auto. + apply Raw.join_ok; auto. + red; intros. apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto. + + split. + auto. + apply Raw.join_ok; auto. + red; intros. apply g. apply In_raw_partition_between_2. rewrite REQ; auto. +Qed. + +Hypothesis above_monotone: + forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true. +Hypothesis below_monotone: + forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true. + +Remark In_raw_partition_between_3: + forall x m, + Raw.In x (fst (raw_partition_between m)) -> above_low_bound x = true /\ below_high_bound x = true. +Proof. + induction m; simpl; intros. +- inv H. +- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. + destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *. + destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H. + + rewrite Raw.join_spec in H. intuition. + apply above_monotone with t1; auto. + apply below_monotone with t1; auto. + + auto. + + auto. +Qed. + +Remark In_raw_partition_between_4: + forall x m, + Raw.bst m -> + Raw.In x (snd (raw_partition_between m)) -> above_low_bound x = false \/ below_high_bound x = false. +Proof. + induction 1; simpl; intros. +- inv H. +- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. + destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *. + destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H. + + simpl in H1. rewrite Raw.concat_spec in H1. intuition. + + assert (forall y, X.eq y x0 \/ X.lt x0 y -> below_high_bound y = false). + { intros. destruct (below_high_bound y) eqn:E; auto. + assert (below_high_bound x0 = true) by (apply below_monotone with y; auto). + congruence. } + simpl in H1. rewrite Raw.join_spec in H1. intuition. + + assert (forall y, X.eq y x0 \/ X.lt y x0 -> above_low_bound y = false). + { intros. destruct (above_low_bound y) eqn:E; auto. + assert (above_low_bound x0 = true) by (apply above_monotone with y; auto). + congruence. } + simpl in H1. rewrite Raw.join_spec in H1. intuition. +Qed. + +Remark In_raw_partition_between_5: + forall x m, + Raw.bst m -> + Raw.In x m -> above_low_bound x = true -> below_high_bound x = true -> + Raw.In x (fst (raw_partition_between m)). +Proof. + induction 1; simpl; intros. +- inv H. +- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. + destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *. + destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H. + + simpl. rewrite Raw.join_spec. inv H1. + auto. + right; left; apply IHbst1; auto. + right; right; apply IHbst2; auto. + + simpl. inv H1. + assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). + congruence. + auto. + assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). + congruence. + + simpl. inv H1. + assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). + congruence. + assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). + congruence. + eauto. +Qed. + +Remark In_raw_partition_between_6: + forall x m, + Raw.bst m -> + Raw.In x m -> above_low_bound x = false \/ below_high_bound x = false -> + Raw.In x (snd (raw_partition_between m)). +Proof. + induction 1; simpl; intros. +- inv H. +- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. + destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *. + destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H. + + simpl. rewrite Raw.concat_spec. inv H1. + assert (below_high_bound x = true) by (apply below_monotone with x0; auto; left; symmetry; auto). + assert (above_low_bound x = true) by (apply above_monotone with x0; auto; left; symmetry; auto). + destruct H2; congruence. + left; apply IHbst1; auto. + right; apply IHbst2; auto. + + simpl. rewrite Raw.join_spec. inv H1. + auto. + right; left; apply IHbst1; auto. + auto. + + simpl. rewrite Raw.join_spec. inv H1. + auto. + auto. + right; right; apply IHbst2; auto. +Qed. + +Definition partition_between (s: t) : t * t := + let p := raw_partition_between s.(MSet.this) in + (@MSet.Mkt (fst p) (proj1 (raw_partition_between_ok s.(MSet.this) s.(MSet.is_ok))), + @MSet.Mkt (snd p) (proj2 (raw_partition_between_ok s.(MSet.this) s.(MSet.is_ok)))). + +Theorem partition_between_iff_1: + forall x s, + In x (fst (partition_between s)) <-> + In x s /\ above_low_bound x = true /\ below_high_bound x = true. +Proof. + intros. unfold partition_between, In; simpl. split. + intros. split. apply In_raw_partition_between_1; auto. eapply In_raw_partition_between_3; eauto. + intros [A [B C]]. apply In_raw_partition_between_5; auto. apply MSet.is_ok. +Qed. + +Theorem partition_between_iff_2: + forall x s, + In x (snd (partition_between s)) <-> + In x s /\ (above_low_bound x = false \/ below_high_bound x = false). +Proof. + intros. unfold partition_between, In; simpl. split. + intros. split. apply In_raw_partition_between_2; auto. eapply In_raw_partition_between_4; eauto. apply MSet.is_ok. + intros [A B]. apply In_raw_partition_between_6; auto. apply MSet.is_ok. +Qed. + +End PARTITION_BETWEEN. + +End Make. diff --git a/lib/Floats.v b/lib/Floats.v index eb86027..02ff25c 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -121,6 +121,26 @@ Definition intuoffloat (f:float): option int := (**r conversion to unsigned 32-b | None => None end. +Definition longoffloat (f:float): option int64 := (**r conversion to signed 64-bit int *) + match Zoffloat f with + | Some n => + if Zle_bool Int64.min_signed n && Zle_bool n Int64.max_signed then + Some (Int64.repr n) + else + None + | None => None + end. + +Definition longuoffloat (f:float): option int64 := (**r conversion to unsigned 64-bit int *) + match Zoffloat f with + | Some n => + if Zle_bool 0 n && Zle_bool n Int64.max_unsigned then + Some (Int64.repr n) + else + None + | None => None + end. + (* Functions used to parse floats *) Program Definition build_from_parsed (prec:Z) (emax:Z) (prec_gt_0 :Prec_gt_0 prec) (Hmax:prec < emax) @@ -154,6 +174,11 @@ Definition floatofint (n:int): float := (**r conversion from signed 32-bit int * binary_normalize64 (Int.signed n) 0 false. Definition floatofintu (n:int): float:= (**r conversion from unsigned 32-bit int *) binary_normalize64 (Int.unsigned n) 0 false. +Definition floatoflong (n:int64): float := (**r conversion from signed 64-bit int *) + binary_normalize64 (Int64.signed n) 0 false. +Definition floatoflongu (n:int64): float:= (**r conversion from unsigned 64-bit int *) + binary_normalize64 (Int64.unsigned n) 0 false. + Definition add: float -> float -> float := b64_plus mode_NE. (**r addition *) Definition sub: float -> float -> float := b64_minus mode_NE. (**r subtraction *) Definition mul: float -> float -> float := b64_mult mode_NE. (**r multiplication *) @@ -217,24 +242,7 @@ Definition double_of_bits (b: int64): float := b64_of_bits (Int64.unsigned b). Definition bits_of_single (f: float) : int := Int.repr (bits_of_b32 (binary32offloat f)). Definition single_of_bits (b: int): float := floatofbinary32 (b32_of_bits (Int.unsigned b)). -Definition from_words (hi lo: int) : float := - double_of_bits - (Int64.or (Int64.shl (Int64.repr (Int.unsigned hi)) (Int64.repr 32)) - (Int64.repr (Int.unsigned lo))). - -Lemma from_words_eq: - forall lo hi, - from_words hi lo = - double_of_bits (Int64.repr (Int.unsigned hi * two_p 32 + Int.unsigned lo)). -Proof. - intros. unfold from_words. decEq. - rewrite Int64.shifted_or_is_add. - apply Int64.eqm_samerepr. auto with ints. - change Int64.zwordsize with 64. omega. - generalize (Int.unsigned_range lo). intros [A B]. - rewrite Int64.unsigned_repr. assumption. - assert (Int.modulus < Int64.max_unsigned). compute; auto. omega. -Qed. +Definition from_words (hi lo: int) : float := double_of_bits (Int64.ofwords hi lo). (** Below are the only properties of floating-point arithmetic that we rely on in the compiler proof. *) @@ -747,35 +755,11 @@ Definition ox4330_0000 := Int.repr 1127219200. (**r [0x4330_0000] *) Lemma split_bits_or: forall x, - split_bits 52 11 - (Int64.unsigned - (Int64.or - (Int64.shl (Int64.repr (Int.unsigned ox4330_0000)) (Int64.repr 32)) - (Int64.repr (Int.unsigned x)))) = (false, Int.unsigned x, 1075). + split_bits 52 11 (Int64.unsigned (Int64.ofwords ox4330_0000 x)) = (false, Int.unsigned x, 1075). Proof. intros. transitivity (split_bits 52 11 (join_bits 52 11 false (Int.unsigned x) 1075)). - - f_equal. - assert (Int64.unsigned (Int64.repr (Int.unsigned x)) = Int.unsigned x). - apply Int64.unsigned_repr. - generalize (Int.unsigned_range x). - compute_this (Int.modulus). - compute_this (Int64.max_unsigned). - omega. - rewrite Int64.shifted_or_is_add. - unfold join_bits. - rewrite H. - apply Int64.unsigned_repr. - generalize (Int.unsigned_range x). - compute_this ((0 + 1075) * 2 ^ 52). - compute_this (Int.modulus). - compute_this (Int64.max_unsigned). - omega. - compute_this Int64.zwordsize. omega. - rewrite H. - generalize (Int.unsigned_range x). - change (two_p 32) with Int.modulus. - omega. + - f_equal. rewrite Int64.ofwords_add'. reflexivity. - apply split_join_bits. compute; auto. generalize (Int.unsigned_range x). diff --git a/lib/Integers.v b/lib/Integers.v index af9decd..84b82bf 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -16,8 +16,8 @@ (** Formalizations of machine integers modulo $2^N$ #2N#. *) Require Import Eqdep_dec. +Require Import Zquot. Require Import Zwf. -Require Recdef. Require Import Coqlib. (** * Comparisons *) @@ -1061,36 +1061,7 @@ Proof. apply eqm_mult; apply eqm_sym; apply eqm_signed_unsigned. Qed. -(** ** Properties of division and Lemma Ztestbit_same_equal: - forall x y, - (forall i, 0 <= i -> Z.testbit x i = Z.testbit y i) -> - x = y. -Proof. - assert (forall x, 0 <= x -> - forall y, - (forall i, 0 <= i -> Z.testbit x i = Z.testbit y i) -> - x = y). - { - intros x0 POS0; pattern x0; apply Zdiv2_pos_ind; auto. - - intros. symmetry. apply Ztestbit_is_zero. - intros. rewrite <- H; auto. apply Z.testbit_0_l. - - intros. rewrite (Zdecomp x); rewrite (Zdecomp y). f_equal. - + exploit (H0 0). omega. rewrite !(Ztestbit_eq 0). - rewrite !zeq_true. auto. omega. omega. - + intros. apply H; intros. - exploit (H0 (Zsucc i)). omega. rewrite !(Ztestbit_eq (Z.succ i)). - rewrite !zeq_false. rewrite !Z.pred_succ. auto. - omega. omega. omega. omega. - } - intros. destruct (zle 0 x). - - apply H; auto. - - assert (-x-1 = -y-1). - { apply H. omega. intros. rewrite !Z_one_complement; auto. - rewrite H0; auto. - } - omega. -Qed. -modulus *) +(** ** Properties of division and modulus *) Lemma modu_divu_Euclid: forall x y, y <> zero -> x = add (mul (divu x y) y) (modu x y). @@ -1155,8 +1126,6 @@ Proof. apply one_not_zero. Qed. -Require Import Zquot. - Theorem divs_mone: forall x, divs x mone = neg x. Proof. @@ -3707,7 +3676,434 @@ Module Wordsize_64. Proof. unfold wordsize; congruence. Qed. End Wordsize_64. -Module Int64 := Make(Wordsize_64). +Module Int64. + +Include Make(Wordsize_64). + +(** Shifts with amount given as a 32-bit integer *) + +Definition iwordsize': Int.int := Int.repr zwordsize. + +Definition shl' (x: int) (y: Int.int): int := + repr (Z.shiftl (unsigned x) (Int.unsigned y)). +Definition shru' (x: int) (y: Int.int): int := + repr (Z.shiftr (unsigned x) (Int.unsigned y)). +Definition shr' (x: int) (y: Int.int): int := + repr (Z.shiftr (signed x) (Int.unsigned y)). + +Lemma bits_shl': + forall x y i, + 0 <= i < zwordsize -> + testbit (shl' x y) i = + if zlt i (Int.unsigned y) then false else testbit x (i - Int.unsigned y). +Proof. + intros. unfold shl'. rewrite testbit_repr; auto. + destruct (zlt i (Int.unsigned y)). + apply Z.shiftl_spec_low. auto. + apply Z.shiftl_spec_high. omega. omega. +Qed. + +Lemma bits_shru': + forall x y i, + 0 <= i < zwordsize -> + testbit (shru' x y) i = + if zlt (i + Int.unsigned y) zwordsize then testbit x (i + Int.unsigned y) else false. +Proof. + intros. unfold shru'. rewrite testbit_repr; auto. + rewrite Z.shiftr_spec. fold (testbit x (i + Int.unsigned y)). + destruct (zlt (i + Int.unsigned y) zwordsize). + auto. + apply bits_above; auto. + omega. +Qed. + +Lemma bits_shr': + forall x y i, + 0 <= i < zwordsize -> + testbit (shr' x y) i = + testbit x (if zlt (i + Int.unsigned y) zwordsize then i + Int.unsigned y else zwordsize - 1). +Proof. + intros. unfold shr'. rewrite testbit_repr; auto. + rewrite Z.shiftr_spec. apply bits_signed. + generalize (Int.unsigned_range y); omega. + omega. +Qed. + +(** Decomposing 64-bit ints as pairs of 32-bit ints *) + +Definition loword (n: int) : Int.int := Int.repr (unsigned n). + +Definition hiword (n: int) : Int.int := Int.repr (unsigned (shru n (repr Int.zwordsize))). + +Definition ofwords (hi lo: Int.int) : int := + or (shl (repr (Int.unsigned hi)) (repr Int.zwordsize)) (repr (Int.unsigned lo)). + +Lemma bits_loword: + forall n i, 0 <= i < Int.zwordsize -> Int.testbit (loword n) i = testbit n i. +Proof. + intros. unfold loword. rewrite Int.testbit_repr; auto. +Qed. + +Lemma bits_hiword: + forall n i, 0 <= i < Int.zwordsize -> Int.testbit (hiword n) i = testbit n (i + Int.zwordsize). +Proof. + intros. unfold hiword. rewrite Int.testbit_repr; auto. + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. + fold (testbit (shru n (repr Int.zwordsize)) i). rewrite bits_shru. + change (unsigned (repr Int.zwordsize)) with Int.zwordsize. + apply zlt_true. omega. omega. +Qed. + +Lemma bits_ofwords: + forall hi lo i, 0 <= i < zwordsize -> + testbit (ofwords hi lo) i = + if zlt i Int.zwordsize then Int.testbit lo i else Int.testbit hi (i - Int.zwordsize). +Proof. + intros. unfold ofwords. rewrite bits_or; auto. rewrite bits_shl; auto. + change (unsigned (repr Int.zwordsize)) with Int.zwordsize. + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. + destruct (zlt i Int.zwordsize). + rewrite testbit_repr; auto. + rewrite !testbit_repr; auto. + fold (Int.testbit lo i). rewrite Int.bits_above. apply orb_false_r. auto. + omega. +Qed. + +Lemma lo_ofwords: + forall hi lo, loword (ofwords hi lo) = lo. +Proof. + intros. apply Int.same_bits_eq; intros. + rewrite bits_loword; auto. rewrite bits_ofwords. apply zlt_true. omega. + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. omega. +Qed. + +Lemma hi_ofwords: + forall hi lo, hiword (ofwords hi lo) = hi. +Proof. + intros. apply Int.same_bits_eq; intros. + rewrite bits_hiword; auto. rewrite bits_ofwords. + rewrite zlt_false. f_equal. omega. omega. + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. omega. +Qed. + +Lemma ofwords_recompose: + forall n, ofwords (hiword n) (loword n) = n. +Proof. + intros. apply same_bits_eq; intros. rewrite bits_ofwords; auto. + destruct (zlt i Int.zwordsize). + apply bits_loword. omega. + rewrite bits_hiword. f_equal. omega. + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. omega. +Qed. + +Lemma ofwords_add: + forall lo hi, ofwords hi lo = repr (Int.unsigned hi * two_p 32 + Int.unsigned lo). +Proof. + intros. unfold ofwords. rewrite shifted_or_is_add. + apply eqm_samerepr. apply eqm_add. apply eqm_mult. + apply eqm_sym; apply eqm_unsigned_repr. + apply eqm_refl. + apply eqm_sym; apply eqm_unsigned_repr. + change Int.zwordsize with 32; change zwordsize with 64; omega. + rewrite unsigned_repr. generalize (Int.unsigned_range lo). intros [A B]. exact B. + assert (Int.max_unsigned < max_unsigned) by (compute; auto). + generalize (Int.unsigned_range_2 lo); omega. +Qed. + +Lemma ofwords_add': + forall lo hi, unsigned (ofwords hi lo) = Int.unsigned hi * two_p 32 + Int.unsigned lo. +Proof. + intros. rewrite ofwords_add. apply unsigned_repr. + generalize (Int.unsigned_range hi) (Int.unsigned_range lo). + change (two_p 32) with Int.modulus. + change Int.modulus with 4294967296. + change max_unsigned with 18446744073709551615. + omega. +Qed. + +(** Expressing 64-bit operations in terms of 32-bit operations *) + +Lemma decompose_bitwise_binop: + forall f f64 f32 xh xl yh yl, + (forall x y i, 0 <= i < zwordsize -> testbit (f64 x y) i = f (testbit x i) (testbit y i)) -> + (forall x y i, 0 <= i < Int.zwordsize -> Int.testbit (f32 x y) i = f (Int.testbit x i) (Int.testbit y i)) -> + f64 (ofwords xh xl) (ofwords yh yl) = ofwords (f32 xh yh) (f32 xl yl). +Proof. + intros. apply Int64.same_bits_eq; intros. + rewrite H by auto. rewrite ! bits_ofwords by auto. + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. + destruct (zlt i Int.zwordsize); rewrite H0 by omega; auto. +Qed. + +Lemma decompose_and: + forall xh xl yh yl, + and (ofwords xh xl) (ofwords yh yl) = ofwords (Int.and xh yh) (Int.and xl yl). +Proof. + intros. apply decompose_bitwise_binop with andb. + apply bits_and. apply Int.bits_and. +Qed. + +Lemma decompose_or: + forall xh xl yh yl, + or (ofwords xh xl) (ofwords yh yl) = ofwords (Int.or xh yh) (Int.or xl yl). +Proof. + intros. apply decompose_bitwise_binop with orb. + apply bits_or. apply Int.bits_or. +Qed. + +Lemma decompose_xor: + forall xh xl yh yl, + xor (ofwords xh xl) (ofwords yh yl) = ofwords (Int.xor xh yh) (Int.xor xl yl). +Proof. + intros. apply decompose_bitwise_binop with xorb. + apply bits_xor. apply Int.bits_xor. +Qed. + +Lemma decompose_not: + forall xh xl, + not (ofwords xh xl) = ofwords (Int.not xh) (Int.not xl). +Proof. + intros. unfold not, Int.not. rewrite <- decompose_xor. f_equal. + apply (Int64.eq_spec mone (ofwords Int.mone Int.mone)). +Qed. + +Lemma decompose_shl_1: + forall xh xl y, + 0 <= Int.unsigned y < Int.zwordsize -> + shl' (ofwords xh xl) y = + ofwords (Int.or (Int.shl xh y) (Int.shru xl (Int.sub Int.iwordsize y))) + (Int.shl xl y). +Proof. + intros. + assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y). + { unfold Int.sub. rewrite Int.unsigned_repr. auto. + rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. } + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. + apply Int64.same_bits_eq; intros. + rewrite bits_shl' by auto. symmetry. rewrite bits_ofwords by auto. + destruct (zlt i Int.zwordsize). rewrite Int.bits_shl by omega. + destruct (zlt i (Int.unsigned y)). auto. + rewrite bits_ofwords by omega. rewrite zlt_true by omega. auto. + rewrite zlt_false by omega. rewrite bits_ofwords by omega. + rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. + rewrite Int.bits_shru by omega. rewrite H0. + destruct (zlt (i - Int.unsigned y) (Int.zwordsize)). + rewrite zlt_true by omega. rewrite zlt_true by omega. + rewrite orb_false_l. f_equal. omega. + rewrite zlt_false by omega. rewrite zlt_false by omega. + rewrite orb_false_r. f_equal. omega. +Qed. + +Lemma decompose_shl_2: + forall xh xl y, + Int.zwordsize <= Int.unsigned y < zwordsize -> + shl' (ofwords xh xl) y = + ofwords (Int.shl xl (Int.sub y Int.iwordsize)) Int.zero. +Proof. + intros. + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. + assert (Int.unsigned (Int.sub y Int.iwordsize) = Int.unsigned y - Int.zwordsize). + { unfold Int.sub. rewrite Int.unsigned_repr. auto. + rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. } + apply Int64.same_bits_eq; intros. + rewrite bits_shl' by auto. symmetry. rewrite bits_ofwords by auto. + destruct (zlt i Int.zwordsize). rewrite zlt_true by omega. apply Int.bits_zero. + rewrite Int.bits_shl by omega. + destruct (zlt i (Int.unsigned y)). + rewrite zlt_true by omega. auto. + rewrite zlt_false by omega. + rewrite bits_ofwords by omega. rewrite zlt_true by omega. f_equal. omega. +Qed. + +Lemma decompose_shru_1: + forall xh xl y, + 0 <= Int.unsigned y < Int.zwordsize -> + shru' (ofwords xh xl) y = + ofwords (Int.shru xh y) + (Int.or (Int.shru xl y) (Int.shl xh (Int.sub Int.iwordsize y))). +Proof. + intros. + assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y). + { unfold Int.sub. rewrite Int.unsigned_repr. auto. + rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. } + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. + apply Int64.same_bits_eq; intros. + rewrite bits_shru' by auto. symmetry. rewrite bits_ofwords by auto. + destruct (zlt i Int.zwordsize). + rewrite zlt_true by omega. + rewrite bits_ofwords by omega. + rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. + rewrite Int.bits_shru by omega. rewrite H0. + destruct (zlt (i + Int.unsigned y) (Int.zwordsize)). + rewrite zlt_true by omega. + rewrite orb_false_r. auto. + rewrite zlt_false by omega. + rewrite orb_false_l. f_equal. omega. + rewrite Int.bits_shru by omega. + destruct (zlt (i + Int.unsigned y) zwordsize). + rewrite bits_ofwords by omega. + rewrite zlt_true by omega. rewrite zlt_false by omega. f_equal. omega. + rewrite zlt_false by omega. auto. +Qed. + +Lemma decompose_shru_2: + forall xh xl y, + Int.zwordsize <= Int.unsigned y < zwordsize -> + shru' (ofwords xh xl) y = + ofwords Int.zero (Int.shru xh (Int.sub y Int.iwordsize)). +Proof. + intros. + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. + assert (Int.unsigned (Int.sub y Int.iwordsize) = Int.unsigned y - Int.zwordsize). + { unfold Int.sub. rewrite Int.unsigned_repr. auto. + rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. } + apply Int64.same_bits_eq; intros. + rewrite bits_shru' by auto. symmetry. rewrite bits_ofwords by auto. + destruct (zlt i Int.zwordsize). + rewrite Int.bits_shru by omega. rewrite H1. + destruct (zlt (i + Int.unsigned y) zwordsize). + rewrite zlt_true by omega. rewrite bits_ofwords by omega. + rewrite zlt_false by omega. f_equal; omega. + rewrite zlt_false by omega. auto. + rewrite zlt_false by omega. apply Int.bits_zero. +Qed. + +Lemma decompose_shr_1: + forall xh xl y, + 0 <= Int.unsigned y < Int.zwordsize -> + shr' (ofwords xh xl) y = + ofwords (Int.shr xh y) + (Int.or (Int.shru xl y) (Int.shl xh (Int.sub Int.iwordsize y))). +Proof. + intros. + assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y). + { unfold Int.sub. rewrite Int.unsigned_repr. auto. + rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. } + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. + apply Int64.same_bits_eq; intros. + rewrite bits_shr' by auto. symmetry. rewrite bits_ofwords by auto. + destruct (zlt i Int.zwordsize). + rewrite zlt_true by omega. + rewrite bits_ofwords by omega. + rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. + rewrite Int.bits_shru by omega. rewrite H0. + destruct (zlt (i + Int.unsigned y) (Int.zwordsize)). + rewrite zlt_true by omega. + rewrite orb_false_r. auto. + rewrite zlt_false by omega. + rewrite orb_false_l. f_equal. omega. + rewrite Int.bits_shr by omega. + destruct (zlt (i + Int.unsigned y) zwordsize). + rewrite bits_ofwords by omega. + rewrite zlt_true by omega. rewrite zlt_false by omega. f_equal. omega. + rewrite zlt_false by omega. rewrite bits_ofwords by omega. + rewrite zlt_false by omega. f_equal. +Qed. + +Lemma decompose_shr_2: + forall xh xl y, + Int.zwordsize <= Int.unsigned y < zwordsize -> + shr' (ofwords xh xl) y = + ofwords (Int.shr xh (Int.sub Int.iwordsize Int.one)) + (Int.shr xh (Int.sub y Int.iwordsize)). +Proof. + intros. + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. + assert (Int.unsigned (Int.sub y Int.iwordsize) = Int.unsigned y - Int.zwordsize). + { unfold Int.sub. rewrite Int.unsigned_repr. auto. + rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. } + apply Int64.same_bits_eq; intros. + rewrite bits_shr' by auto. symmetry. rewrite bits_ofwords by auto. + destruct (zlt i Int.zwordsize). + rewrite Int.bits_shr by omega. rewrite H1. + destruct (zlt (i + Int.unsigned y) zwordsize). + rewrite zlt_true by omega. rewrite bits_ofwords by omega. + rewrite zlt_false by omega. f_equal; omega. + rewrite zlt_false by omega. rewrite bits_ofwords by omega. + rewrite zlt_false by omega. auto. + rewrite Int.bits_shr by omega. + change (Int.unsigned (Int.sub Int.iwordsize Int.one)) with (Int.zwordsize - 1). + destruct (zlt (i + Int.unsigned y) zwordsize); + rewrite bits_ofwords by omega. + symmetry. rewrite zlt_false by omega. f_equal. + destruct (zlt (i - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega. + symmetry. rewrite zlt_false by omega. f_equal. + destruct (zlt (i - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega. +Qed. + +Remark eqm_mul_2p32: + forall x y, Int.eqm x y -> eqm (x * two_p 32) (y * two_p 32). +Proof. + intros. destruct H as [k EQ]. exists k. rewrite EQ. + change Int.modulus with (two_p 32). + change modulus with (two_p 32 * two_p 32). + ring. +Qed. + +Lemma decompose_add: + forall xh xl yh yl, + add (ofwords xh xl) (ofwords yh yl) = + ofwords (Int.add (Int.add xh yh) (Int.add_carry xl yl Int.zero)) + (Int.add xl yl). +Proof. + intros. symmetry. rewrite ofwords_add. rewrite add_unsigned. + apply eqm_samerepr. + rewrite ! ofwords_add'. rewrite (Int.unsigned_add_carry xl yl). + set (cc := Int.add_carry xl yl Int.zero). + set (Xl := Int.unsigned xl); set (Xh := Int.unsigned xh); + set (Yl := Int.unsigned yl); set (Yh := Int.unsigned yh). + change Int.modulus with (two_p 32). + replace (Xh * two_p 32 + Xl + (Yh * two_p 32 + Yl)) + with ((Xh + Yh) * two_p 32 + (Xl + Yl)) by ring. + replace (Int.unsigned (Int.add (Int.add xh yh) cc) * two_p 32 + + (Xl + Yl - Int.unsigned cc * two_p 32)) + with ((Int.unsigned (Int.add (Int.add xh yh) cc) - Int.unsigned cc) * two_p 32 + + (Xl + Yl)) by ring. + apply eqm_add. 2: apply eqm_refl. apply eqm_mul_2p32. + replace (Xh + Yh) with ((Xh + Yh + Int.unsigned cc) - Int.unsigned cc) by ring. + apply Int.eqm_sub. 2: apply Int.eqm_refl. + apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. 2: apply Int.eqm_refl. + apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. +Qed. + +Definition mul' (x y: Int.int) : int := repr (Int.unsigned x * Int.unsigned y). + +Lemma decompose_mul: + forall xh xl yh yl, + mul (ofwords xh xl) (ofwords yh yl) = + ofwords (Int.add (Int.add (hiword (mul' xl yl)) (Int.mul xl yh)) (Int.mul xh yl)) + (loword (mul' xl yl)). +Proof. + intros. + set (pl := loword (mul' xl yl)); set (ph := hiword (mul' xl yl)). + assert (EQ0: unsigned (mul' xl yl) = Int.unsigned ph * two_p 32 + Int.unsigned pl). + { rewrite <- (ofwords_recompose (mul' xl yl)). apply ofwords_add'. } + symmetry. rewrite ofwords_add. unfold mul. rewrite !ofwords_add'. + set (XL := Int.unsigned xl); set (XH := Int.unsigned xh); + set (YL := Int.unsigned yl); set (YH := Int.unsigned yh). + set (PH := Int.unsigned ph) in *. set (PL := Int.unsigned pl) in *. + transitivity (repr (((PH + XL * YH) + XH * YL) * two_p 32 + PL)). + apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. + apply eqm_mul_2p32. + rewrite Int.add_unsigned. apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. + rewrite Int.add_unsigned. apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. + apply Int.eqm_refl. + unfold Int.mul. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. + unfold Int.mul. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. + transitivity (repr (unsigned (mul' xl yl) + (XL * YH + XH * YL) * two_p 32)). + rewrite EQ0. f_equal. ring. + transitivity (repr ((XL * YL + (XL * YH + XH * YL) * two_p 32))). + apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. + unfold mul'. apply eqm_unsigned_repr_l. apply eqm_refl. + transitivity (repr (0 + (XL * YL + (XL * YH + XH * YL) * two_p 32))). + rewrite Zplus_0_l; auto. + transitivity (repr (XH * YH * (two_p 32 * two_p 32) + (XL * YL + (XL * YH + XH * YL) * two_p 32))). + apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. + change (two_p 32 * two_p 32) with modulus. exists (- XH * YH). ring. + f_equal. ring. +Qed. + +End Int64. Notation int64 := Int64.int. diff --git a/lib/Lattice.v b/lib/Lattice.v index c4b55e9..3fc0d4c 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -747,3 +747,103 @@ Lemma ge_lub_right: forall x y, ge (lub x y) y. Proof. destruct x; destruct y; compute; tauto. Qed. End LBoolean. + +(** * Option semi-lattice *) + +(** This lattice adds a top element (represented by [None]) to a given + semi-lattice (whose elements are injected via [Some]). *) + +Module LOption(L: SEMILATTICE) <: SEMILATTICE_WITH_TOP. + +Definition t: Type := option L.t. + +Definition eq (x y: t) : Prop := + match x, y with + | None, None => True + | Some x1, Some y1 => L.eq x1 y1 + | _, _ => False + end. + +Lemma eq_refl: forall x, eq x x. +Proof. + unfold eq; intros; destruct x. apply L.eq_refl. auto. +Qed. + +Lemma eq_sym: forall x y, eq x y -> eq y x. +Proof. + unfold eq; intros; destruct x; destruct y; auto. apply L.eq_sym; auto. +Qed. + +Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. +Proof. + unfold eq; intros; destruct x; destruct y; destruct z; auto. + eapply L.eq_trans; eauto. + contradiction. +Qed. + +Definition beq (x y: t) : bool := + match x, y with + | None, None => true + | Some x1, Some y1 => L.beq x1 y1 + | _, _ => false + end. + +Lemma beq_correct: forall x y, beq x y = true -> eq x y. +Proof. + unfold beq, eq; intros; destruct x; destruct y. + apply L.beq_correct; auto. + discriminate. discriminate. auto. +Qed. + +Definition ge (x y: t) : Prop := + match x, y with + | None, _ => True + | _, None => False + | Some x1, Some y1 => L.ge x1 y1 + end. + +Lemma ge_refl: forall x y, eq x y -> ge x y. +Proof. + unfold eq, ge; intros; destruct x; destruct y. + apply L.ge_refl; auto. + auto. elim H. auto. +Qed. + +Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. +Proof. + unfold ge; intros; destruct x; destruct y; destruct z; auto. + eapply L.ge_trans; eauto. contradiction. +Qed. + +Definition bot : t := Some L.bot. + +Lemma ge_bot: forall x, ge x bot. +Proof. + unfold ge, bot; intros. destruct x; auto. apply L.ge_bot. +Qed. + +Definition lub (x y: t) : t := + match x, y with + | None, _ => None + | _, None => None + | Some x1, Some y1 => Some (L.lub x1 y1) + end. + +Lemma ge_lub_left: forall x y, ge (lub x y) x. +Proof. + unfold ge, lub; intros; destruct x; destruct y; auto. apply L.ge_lub_left. +Qed. + +Lemma ge_lub_right: forall x y, ge (lub x y) y. +Proof. + unfold ge, lub; intros; destruct x; destruct y; auto. apply L.ge_lub_right. +Qed. + +Definition top : t := None. + +Lemma ge_top: forall x, ge top x. +Proof. + unfold ge, top; intros. auto. +Qed. + +End LOption. diff --git a/lib/Maps.v b/lib/Maps.v index f667ea4..ddb0c33 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -377,23 +377,18 @@ Module PTree <: TREE. end. Lemma bempty_correct: - forall m, bempty m = true -> forall x, get x m = None. + forall m, bempty m = true <-> (forall x, get x m = None). Proof. - induction m; simpl; intros. - change (@Leaf A) with (empty A). apply gempty. - destruct o. congruence. destruct (andb_prop _ _ H). + induction m; simpl. + split; intros. apply gleaf. auto. + destruct o; split; intros. + congruence. + generalize (H xH); simpl; congruence. + destruct (andb_prop _ _ H). rewrite IHm1 in H0. rewrite IHm2 in H1. destruct x; simpl; auto. - Qed. - - Lemma bempty_complete: - forall m, (forall x, get x m = None) -> bempty m = true. - Proof. - induction m; simpl; intros. - auto. - destruct o. generalize (H xH); simpl; congruence. - rewrite IHm1. rewrite IHm2. auto. - intros; apply (H (xI x)). - intros; apply (H (xO x)). + apply andb_true_intro; split. + apply IHm1. intros; apply (H (xO x)). + apply IHm2. intros; apply (H (xI x)). Qed. Lemma beq_correct: @@ -406,38 +401,23 @@ Module PTree <: TREE. | _, _ => False end). Proof. - intros; split. - - (* beq = true -> exteq *) - revert m1 m2. induction m1; destruct m2; simpl. - intros; red; intros. change (@Leaf A) with (empty A). - repeat rewrite gempty. auto. - destruct o; intro. congruence. - red; intros. change (@Leaf A) with (empty A). rewrite gempty. - rewrite bempty_correct. auto. assumption. - destruct o; intro. congruence. - red; intros. change (@Leaf A) with (empty A). rewrite gempty. - rewrite bempty_correct. auto. assumption. - destruct o; destruct o0; simpl; intro; try congruence. - destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). - destruct x; simpl. - apply IHm1_2; auto. apply IHm1_1; auto. auto. - destruct (andb_prop _ _ H). - red; intros. destruct x; simpl. - apply IHm1_2; auto. apply IHm1_1; auto. - auto. - - (* exteq -> beq = true *) - revert m1 m2. induction m1; destruct m2; simpl; intros. - auto. - change (bempty (Node m2_1 o m2_2) = true). - apply bempty_complete. intros. generalize (H x). rewrite gleaf. - destruct (get x (Node m2_1 o m2_2)); tauto. - change (bempty (Node m1_1 o m1_2) = true). - apply bempty_complete. intros. generalize (H x). rewrite gleaf. - destruct (get x (Node m1_1 o m1_2)); tauto. - apply andb_true_intro. split. apply andb_true_intro. split. - generalize (H xH); simpl. destruct o; destruct o0; auto. - apply IHm1_1. intros. apply (H (xO x)). - apply IHm1_2. intros. apply (H (xI x)). + induction m1; intros. + - simpl. rewrite bempty_correct. split; intros. + rewrite gleaf. rewrite H. auto. + generalize (H x). rewrite gleaf. destruct (get x m2); tauto. + - destruct m2. + + unfold beq. rewrite bempty_correct. split; intros. + rewrite H. rewrite gleaf. auto. + generalize (H x). rewrite gleaf. destruct (get x (Node m1_1 o m1_2)); tauto. + + simpl. split; intros. + * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). + rewrite IHm1_1 in H3. rewrite IHm1_2 in H1. + destruct x; simpl. apply H1. apply H3. + destruct o; destruct o0; auto || congruence. + * apply andb_true_intro. split. apply andb_true_intro. split. + generalize (H xH); simpl. destruct o; destruct o0; tauto. + apply IHm1_1. intros; apply (H (xO x)). + apply IHm1_2. intros; apply (H (xI x)). Qed. End BOOLEAN_EQUALITY. @@ -559,7 +539,7 @@ Module PTree <: TREE. Section COMBINE. - Variable A B C: Type. + Variables A B C: Type. Variable f: option A -> option B -> option C. Hypothesis f_none_none: f None None = None. @@ -646,45 +626,53 @@ Module PTree <: TREE. auto. Qed. - Fixpoint xelements (A : Type) (m : t A) (i : positive) {struct m} - : list (positive * A) := + Fixpoint xelements (A : Type) (m : t A) (i : positive) + (k: list (positive * A)) {struct m} + : list (positive * A) := match m with - | Leaf => nil + | Leaf => k | Node l None r => - (xelements l (append i (xO xH))) ++ (xelements r (append i (xI xH))) + xelements l (append i (xO xH)) (xelements r (append i (xI xH)) k) | Node l (Some x) r => - (xelements l (append i (xO xH))) - ++ ((i, x) :: xelements r (append i (xI xH))) + xelements l (append i (xO xH)) + ((i, x) :: xelements r (append i (xI xH)) k) end. - (* Note: function [xelements] above is inefficient. We should apply - deforestation to it, but that makes the proofs even harder. *) - Definition elements A (m : t A) := xelements m xH. + Definition elements (A: Type) (m : t A) := xelements m xH nil. + + Lemma xelements_incl: + forall (A: Type) (m: t A) (i : positive) k x, + In x k -> In x (xelements m i k). + Proof. + induction m; intros; simpl. + auto. + destruct o. + apply IHm1. simpl; right; auto. + auto. + Qed. Lemma xelements_correct: - forall (A: Type) (m: t A) (i j : positive) (v: A), - get i m = Some v -> In (append j i, v) (xelements m j). + forall (A: Type) (m: t A) (i j : positive) (v: A) k, + get i m = Some v -> In (append j i, v) (xelements m j k). Proof. induction m; intros. rewrite (gleaf A i) in H; congruence. destruct o; destruct i; simpl; simpl in H. - rewrite append_assoc_1; apply in_or_app; right; apply in_cons; - apply IHm2; auto. - rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. - rewrite append_neutral_r; apply in_or_app; injection H; - intro EQ; rewrite EQ; right; apply in_eq. - rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto. - rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. - congruence. + rewrite append_assoc_1. apply xelements_incl. right. auto. + rewrite append_assoc_0. auto. + inv H. apply xelements_incl. left. rewrite append_neutral_r; auto. + rewrite append_assoc_1. apply xelements_incl. auto. + rewrite append_assoc_0. auto. + inv H. Qed. Theorem elements_correct: forall (A: Type) (m: t A) (i: positive) (v: A), get i m = Some v -> In (i, v) (elements m). Proof. - intros A m i v H. - exact (xelements_correct m i xH H). + intros A m i v H. + exact (xelements_correct m i xH nil H). Qed. Fixpoint xget (A : Type) (i j : positive) (m : t A) {struct j} : option A := @@ -695,6 +683,13 @@ Module PTree <: TREE. | _, _ => None end. + Lemma xget_diag : + forall (A : Type) (i : positive) (m1 m2 : t A) (o : option A), + xget i i (Node m1 o m2) = o. + Proof. + induction i; intros; simpl; auto. + Qed. + Lemma xget_left : forall (A : Type) (j i : positive) (m1 m2 : t A) (o : option A) (v : A), xget i (append j (xO xH)) m1 = Some v -> xget i j (Node m1 o m2) = Some v. @@ -703,122 +698,26 @@ Module PTree <: TREE. destruct i; congruence. Qed. - Lemma xelements_ii : - forall (A: Type) (m: t A) (i j : positive) (v: A), - In (xI i, v) (xelements m (xI j)) -> In (i, v) (xelements m j). - Proof. - induction m. - simpl; auto. - intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H); - apply in_or_app. - left; apply IHm1; auto. - right; destruct (in_inv H0). - injection H1; intros EQ1 EQ2; rewrite EQ1; rewrite EQ2; apply in_eq. - apply in_cons; apply IHm2; auto. - left; apply IHm1; auto. - right; apply IHm2; auto. - Qed. - - Lemma xelements_io : - forall (A: Type) (m: t A) (i j : positive) (v: A), - ~In (xI i, v) (xelements m (xO j)). - Proof. - induction m. - simpl; auto. - intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). - apply (IHm1 _ _ _ H0). - destruct (in_inv H0). - congruence. - apply (IHm2 _ _ _ H1). - apply (IHm1 _ _ _ H0). - apply (IHm2 _ _ _ H0). - Qed. - - Lemma xelements_oo : - forall (A: Type) (m: t A) (i j : positive) (v: A), - In (xO i, v) (xelements m (xO j)) -> In (i, v) (xelements m j). - Proof. - induction m. - simpl; auto. - intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H); - apply in_or_app. - left; apply IHm1; auto. - right; destruct (in_inv H0). - injection H1; intros EQ1 EQ2; rewrite EQ1; rewrite EQ2; apply in_eq. - apply in_cons; apply IHm2; auto. - left; apply IHm1; auto. - right; apply IHm2; auto. - Qed. - - Lemma xelements_oi : - forall (A: Type) (m: t A) (i j : positive) (v: A), - ~In (xO i, v) (xelements m (xI j)). - Proof. - induction m. - simpl; auto. - intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). - apply (IHm1 _ _ _ H0). - destruct (in_inv H0). - congruence. - apply (IHm2 _ _ _ H1). - apply (IHm1 _ _ _ H0). - apply (IHm2 _ _ _ H0). - Qed. - - Lemma xelements_ih : - forall (A: Type) (m1 m2: t A) (o: option A) (i : positive) (v: A), - In (xI i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m2 xH). - Proof. - destruct o; simpl; intros; destruct (in_app_or _ _ _ H). - absurd (In (xI i, v) (xelements m1 2)); auto; apply xelements_io; auto. - destruct (in_inv H0). - congruence. - apply xelements_ii; auto. - absurd (In (xI i, v) (xelements m1 2)); auto; apply xelements_io; auto. - apply xelements_ii; auto. - Qed. - - Lemma xelements_oh : - forall (A: Type) (m1 m2: t A) (o: option A) (i : positive) (v: A), - In (xO i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m1 xH). - Proof. - destruct o; simpl; intros; destruct (in_app_or _ _ _ H). - apply xelements_oo; auto. - destruct (in_inv H0). - congruence. - absurd (In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto. - apply xelements_oo; auto. - absurd (In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto. - Qed. - - Lemma xelements_hi : - forall (A: Type) (m: t A) (i : positive) (v: A), - ~In (xH, v) (xelements m (xI i)). + Lemma xget_right : + forall (A : Type) (j i : positive) (m1 m2 : t A) (o : option A) (v : A), + xget i (append j (xI xH)) m2 = Some v -> xget i j (Node m1 o m2) = Some v. Proof. - induction m; intros. - simpl; auto. - destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). - generalize H0; apply IHm1; auto. - destruct (in_inv H0). - congruence. - generalize H1; apply IHm2; auto. - generalize H0; apply IHm1; auto. - generalize H0; apply IHm2; auto. + induction j; intros; destruct i; simpl; simpl in H; auto; try congruence. + destruct i; congruence. Qed. - Lemma xelements_ho : - forall (A: Type) (m: t A) (i : positive) (v: A), - ~In (xH, v) (xelements m (xO i)). + Lemma xelements_complete: + forall (A: Type) (m: t A) (i j : positive) (v: A) k, + In (i, v) (xelements m j k) -> xget i j m = Some v \/ In (i, v) k. Proof. - induction m; intros. - simpl; auto. - destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). - generalize H0; apply IHm1; auto. - destruct (in_inv H0). - congruence. - generalize H1; apply IHm2; auto. - generalize H0; apply IHm1; auto. - generalize H0; apply IHm2; auto. + induction m; simpl; intros. + auto. + destruct o. + edestruct IHm1; eauto. left; apply xget_left; auto. + destruct H0. inv H0. left; apply xget_diag. + edestruct IHm2; eauto. left; apply xget_right; auto. + edestruct IHm1; eauto. left; apply xget_left; auto. + edestruct IHm2; eauto. left; apply xget_right; auto. Qed. Lemma get_xget_h : @@ -827,89 +726,50 @@ Module PTree <: TREE. destruct i; simpl; auto. Qed. - Lemma xelements_complete: - forall (A: Type) (i j : positive) (m: t A) (v: A), - In (i, v) (xelements m j) -> xget i j m = Some v. - Proof. - induction i; simpl; intros; destruct j; simpl. - apply IHi; apply xelements_ii; auto. - absurd (In (xI i, v) (xelements m (xO j))); auto; apply xelements_io. - destruct m. - simpl in H; tauto. - rewrite get_xget_h. apply IHi. apply (xelements_ih _ _ _ _ _ H). - absurd (In (xO i, v) (xelements m (xI j))); auto; apply xelements_oi. - apply IHi; apply xelements_oo; auto. - destruct m. - simpl in H; tauto. - rewrite get_xget_h. apply IHi. apply (xelements_oh _ _ _ _ _ H). - absurd (In (xH, v) (xelements m (xI j))); auto; apply xelements_hi. - absurd (In (xH, v) (xelements m (xO j))); auto; apply xelements_ho. - destruct m. - simpl in H; tauto. - destruct o; simpl in H; destruct (in_app_or _ _ _ H). - absurd (In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho. - destruct (in_inv H0). - congruence. - absurd (In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi. - absurd (In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho. - absurd (In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi. - Qed. - Theorem elements_complete: forall (A: Type) (m: t A) (i: positive) (v: A), In (i, v) (elements m) -> get i m = Some v. Proof. - intros A m i v H. - unfold elements in H. - rewrite get_xget_h. - exact (xelements_complete i xH m v H). + intros A m i v H. unfold elements in H. + edestruct xelements_complete; eauto. + rewrite get_xget_h. auto. + contradiction. Qed. Lemma in_xelements: - forall (A: Type) (m: t A) (i k: positive) (v: A), - In (k, v) (xelements m i) -> - exists j, k = append i j. + forall (A: Type) (m: t A) (i k: positive) (v: A) l, + In (k, v) (xelements m i l) -> + (exists j, k = append i j) \/ In (k, v) l. Proof. induction m; simpl; intros. - tauto. - assert (k = i \/ In (k, v) (xelements m1 (append i 2)) - \/ In (k, v) (xelements m2 (append i 3))). - destruct o. - elim (in_app_or _ _ _ H); simpl; intuition. - replace k with i. tauto. congruence. - elim (in_app_or _ _ _ H); simpl; intuition. - elim H0; intro. - exists xH. rewrite append_neutral_r. auto. - elim H1; intro. - elim (IHm1 _ _ _ H2). intros k1 EQ. rewrite EQ. - rewrite <- append_assoc_0. exists (xO k1); auto. - elim (IHm2 _ _ _ H2). intros k1 EQ. rewrite EQ. - rewrite <- append_assoc_1. exists (xI k1); auto. + auto. + destruct o. + edestruct IHm1 as [[j EQ] | IN]; eauto. + rewrite <- append_assoc_0 in EQ. left; econstructor; eauto. + destruct IN. + inv H0. left; exists xH; symmetry; apply append_neutral_r. + edestruct IHm2 as [[j EQ] | IN]; eauto. + rewrite <- append_assoc_1 in EQ. left; econstructor; eauto. + edestruct IHm1 as [[j EQ] | IN]; eauto. + rewrite <- append_assoc_0 in EQ. left; econstructor; eauto. + edestruct IHm2 as [[j EQ] | IN']; eauto. + rewrite <- append_assoc_1 in EQ. left; econstructor; eauto. Qed. - Definition xkeys (A: Type) (m: t A) (i: positive) := - List.map (@fst positive A) (xelements m i). + Definition xkeys (A: Type) (m: t A) (i: positive) (l: list (positive * A)) := + List.map (@fst positive A) (xelements m i l). Lemma in_xkeys: - forall (A: Type) (m: t A) (i k: positive), - In k (xkeys m i) -> - exists j, k = append i j. + forall (A: Type) (m: t A) (i k: positive) l, + In k (xkeys m i l) -> + (exists j, k = append i j) \/ In k (List.map fst l). Proof. - unfold xkeys; intros. - elim (list_in_map_inv _ _ _ H). intros [k1 v1] [EQ IN]. - simpl in EQ; subst k1. apply in_xelements with A m v1. auto. - Qed. - - Remark list_append_cons_norepet: - forall (A: Type) (l1 l2: list A) (x: A), - list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 -> - ~In x l1 -> ~In x l2 -> - list_norepet (l1 ++ x :: l2). - Proof. - intros. apply list_norepet_append_commut. simpl; constructor. - red; intros. elim (in_app_or _ _ _ H4); intro; tauto. - apply list_norepet_append; auto. - apply list_disjoint_sym; auto. + unfold xkeys; intros. + exploit list_in_map_inv; eauto. intros [[k1 v1] [EQ IN]]. + simpl in EQ; subst k1. + exploit in_xelements; eauto. intros [EX | IN']. + auto. + right. change k with (fst (k, v1)). apply List.in_map; auto. Qed. Lemma append_injective: @@ -922,44 +782,52 @@ Module PTree <: TREE. Qed. Lemma xelements_keys_norepet: - forall (A: Type) (m: t A) (i: positive), - list_norepet (xkeys m i). + forall (A: Type) (m: t A) (i: positive) l, + (forall k v, get k m = Some v -> ~In (append i k) (List.map fst l)) -> + list_norepet (List.map fst l) -> + list_norepet (xkeys m i l). Proof. - induction m; unfold xkeys; simpl; fold xkeys; intros. - constructor. - assert (list_disjoint (xkeys m1 (append i 2)) (xkeys m2 (append i 3))). - red; intros; red; intro. subst y. - elim (in_xkeys _ _ _ H); intros j1 EQ1. - elim (in_xkeys _ _ _ H0); intros j2 EQ2. - rewrite EQ1 in EQ2. - rewrite <- append_assoc_0 in EQ2. - rewrite <- append_assoc_1 in EQ2. - generalize (append_injective _ _ _ EQ2). congruence. - assert (forall (m: t A) j, - j = 2%positive \/ j = 3%positive -> - ~In i (xkeys m (append i j))). - intros; red; intros. - elim (in_xkeys _ _ _ H1); intros k EQ. - assert (EQ1: append i xH = append (append i j) k). - rewrite append_neutral_r. auto. - elim H0; intro; subst j; - try (rewrite <- append_assoc_0 in EQ1); - try (rewrite <- append_assoc_1 in EQ1); - generalize (append_injective _ _ _ EQ1); congruence. - destruct o; rewrite list_append_map; simpl; - change (List.map (@fst positive A) (xelements m1 (append i 2))) - with (xkeys m1 (append i 2)); - change (List.map (@fst positive A) (xelements m2 (append i 3))) - with (xkeys m2 (append i 3)). - apply list_append_cons_norepet; auto. - apply list_norepet_append; auto. + unfold xkeys; induction m; simpl; intros. + auto. + destruct o. + apply IHm1. + intros; red; intros IN. rewrite <- append_assoc_0 in IN. simpl in IN; destruct IN. + exploit (append_injective i k~0 xH). rewrite append_neutral_r. auto. + congruence. + exploit in_xkeys; eauto. intros [[j EQ] | IN]. + rewrite <- append_assoc_1 in EQ. exploit append_injective; eauto. congruence. + elim (H (xO k) v); auto. + simpl. constructor. + red; intros IN. exploit in_xkeys; eauto. intros [[j EQ] | IN']. + rewrite <- append_assoc_1 in EQ. + exploit (append_injective i j~1 xH). rewrite append_neutral_r. auto. congruence. + elim (H xH a). auto. rewrite append_neutral_r. auto. + apply IHm2; auto. intros. rewrite <- append_assoc_1. eapply H; eauto. + apply IHm1. + intros; red; intros IN. rewrite <- append_assoc_0 in IN. + exploit in_xkeys; eauto. intros [[j EQ] | IN']. + rewrite <- append_assoc_1 in EQ. exploit append_injective; eauto. congruence. + elim (H (xO k) v); auto. + apply IHm2; auto. intros. rewrite <- append_assoc_1. eapply H; eauto. Qed. Theorem elements_keys_norepet: forall (A: Type) (m: t A), list_norepet (List.map (@fst elt A) (elements m)). Proof. - intros. change (list_norepet (xkeys m 1)). apply xelements_keys_norepet. + intros. change (list_norepet (xkeys m 1 nil)). apply xelements_keys_norepet. + intros; red; intros. elim H0. constructor. + Qed. + + Remark xelements_empty: + forall (A: Type) (m: t A) i l, (forall i, get i m = None) -> xelements m i l = l. + Proof. + induction m; simpl; intros. + auto. + destruct o. generalize (H xH); simpl; congruence. + rewrite IHm1. apply IHm2. + intros. apply (H (xI i0)). + intros. apply (H (xO i0)). Qed. Theorem elements_canonical_order: @@ -971,48 +839,48 @@ Module PTree <: TREE. (elements m) (elements n). Proof. intros until R. - assert (forall m n j, + assert (forall m n j l1 l2, (forall i x, get i m = Some x -> exists y, get i n = Some y /\ R x y) -> (forall i y, get i n = Some y -> exists x, get i m = Some x /\ R x y) -> list_forall2 (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y)) - (xelements m j) (xelements n j)). - induction m; induction n; intros; simpl. - constructor. - destruct o. exploit (H0 xH). simpl. reflexivity. simpl. intros [x [P Q]]. congruence. - change (@nil (positive*A)) with ((@nil (positive * A))++nil). - apply list_forall2_app. - apply IHn1. - intros. rewrite gleaf in H1. congruence. - intros. exploit (H0 (xO i)). simpl; eauto. rewrite gleaf. intros [x [P Q]]. congruence. - apply IHn2. - intros. rewrite gleaf in H1. congruence. - intros. exploit (H0 (xI i)). simpl; eauto. rewrite gleaf. intros [x [P Q]]. congruence. - destruct o. exploit (H xH). simpl. reflexivity. simpl. intros [x [P Q]]. congruence. - change (@nil (positive*B)) with (xelements (@Leaf B) (append j 2) ++ (xelements (@Leaf B) (append j 3))). - apply list_forall2_app. - apply IHm1. - intros. exploit (H (xO i)). simpl; eauto. rewrite gleaf. intros [y [P Q]]. congruence. - intros. rewrite gleaf in H1. congruence. - apply IHm2. - intros. exploit (H (xI i)). simpl; eauto. rewrite gleaf. intros [y [P Q]]. congruence. - intros. rewrite gleaf in H1. congruence. - exploit (IHm1 n1 (append j 2)). - intros. exploit (H (xO i)). simpl; eauto. simpl. auto. - intros. exploit (H0 (xO i)). simpl; eauto. simpl; auto. - intro REC1. - exploit (IHm2 n2 (append j 3)). - intros. exploit (H (xI i)). simpl; eauto. simpl. auto. - intros. exploit (H0 (xI i)). simpl; eauto. simpl; auto. - intro REC2. - destruct o; destruct o0. - apply list_forall2_app; auto. constructor; auto. - simpl; split; auto. exploit (H xH). simpl; eauto. simpl. intros [y [P Q]]. congruence. - exploit (H xH). simpl; eauto. simpl. intros [y [P Q]]; congruence. - exploit (H0 xH). simpl; eauto. simpl. intros [x [P Q]]; congruence. - apply list_forall2_app; auto. - - unfold elements; auto. + l1 l2 -> + list_forall2 + (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y)) + (xelements m j l1) (xelements n j l2)). + { + induction m; simpl; intros. + rewrite xelements_empty. auto. + intros. destruct (get i n) eqn:E; auto. exploit H0; eauto. + intros [x [P Q]]. rewrite gleaf in P; congruence. + destruct o. + destruct n. exploit (H xH a); auto. simpl. intros [y [P Q]]; congruence. + exploit (H xH a); auto. intros [y [P Q]]. simpl in P. subst o. + simpl. apply IHm1. + intros i x. exact (H (xO i) x). + intros i x. exact (H0 (xO i) x). + constructor. simpl; auto. + apply IHm2. + intros i x. exact (H (xI i) x). + intros i x. exact (H0 (xI i) x). + auto. + destruct n. simpl. + rewrite ! xelements_empty. auto. + intros. destruct (get i m2) eqn:E; auto. exploit (H (xI i)); eauto. + rewrite gleaf. intros [y [P Q]]; congruence. + intros. destruct (get i m1) eqn:E; auto. exploit (H (xO i)); eauto. + rewrite gleaf. intros [y [P Q]]; congruence. + destruct o. + exploit (H0 xH); simpl; eauto. intros [y [P Q]]; congruence. + simpl. apply IHm1. + intros i x. exact (H (xO i) x). + intros i x. exact (H0 (xO i) x). + apply IHm2. + intros i x. exact (H (xI i) x). + intros i x. exact (H0 (xI i) x). + auto. + } + intros. apply H. auto. auto. constructor. Qed. Theorem elements_extensional: @@ -1045,19 +913,15 @@ Module PTree <: TREE. xfold f xH m v. Lemma xfold_xelements: - forall (A B: Type) (f: B -> positive -> A -> B) m i v, - xfold f i m v = - List.fold_left (fun a p => f a (fst p) (snd p)) - (xelements m i) - v. + forall (A B: Type) (f: B -> positive -> A -> B) m i v l, + List.fold_left (fun a p => f a (fst p) (snd p)) l (xfold f i m v) = + List.fold_left (fun a p => f a (fst p) (snd p)) (xelements m i l) v. Proof. induction m; intros. simpl. auto. - simpl. destruct o. - rewrite fold_left_app. simpl. - rewrite IHm1. apply IHm2. - rewrite fold_left_app. simpl. - rewrite IHm1. apply IHm2. + destruct o; simpl. + rewrite <- IHm1. simpl. rewrite <- IHm2. auto. + rewrite <- IHm1. rewrite <- IHm2. auto. Qed. Theorem fold_spec: @@ -1065,7 +929,7 @@ Module PTree <: TREE. fold f m v = List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v. Proof. - intros. unfold fold, elements. apply xfold_xelements. + intros. unfold fold, elements. rewrite <- xfold_xelements. auto. Qed. End PTree. diff --git a/lib/Ordered.v b/lib/Ordered.v index f52a7ef..026671a 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -48,6 +48,36 @@ Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq. End OrderedPositive. +(** The ordered type of integers *) + +Module OrderedZ <: OrderedType. + +Definition t := Z. +Definition eq (x y: t) := x = y. +Definition lt := Zlt. + +Lemma eq_refl : forall x : t, eq x x. +Proof (@refl_equal t). +Lemma eq_sym : forall x y : t, eq x y -> eq y x. +Proof (@sym_equal t). +Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. +Proof (@trans_equal t). +Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. +Proof Zlt_trans. +Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. +Proof. unfold lt, eq, t; intros. omega. Qed. +Lemma compare : forall x y : t, Compare lt eq x y. +Proof. + intros. destruct (Z.compare x y) as [] eqn:E. + apply EQ. red. apply Z.compare_eq_iff. assumption. + apply LT. assumption. + apply GT. apply Z.compare_gt_iff. assumption. +Defined. + +Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := zeq. + +End OrderedZ. + (** The ordered type of machine integers *) Module OrderedInt <: OrderedType. -- cgit v1.2.3