diff options
Diffstat (limited to 'theories/IntMap')
| -rw-r--r-- | theories/IntMap/Adalloc.v | 339 | ||||
| -rw-r--r-- | theories/IntMap/Addec.v | 193 | ||||
| -rw-r--r-- | theories/IntMap/Addr.v | 491 | ||||
| -rw-r--r-- | theories/IntMap/Adist.v | 336 | ||||
| -rw-r--r-- | theories/IntMap/Allmaps.v | 7 | ||||
| -rw-r--r-- | theories/IntMap/Fset.v | 112 | ||||
| -rw-r--r-- | theories/IntMap/Lsort.v | 343 | ||||
| -rw-r--r-- | theories/IntMap/Map.v | 556 | ||||
| -rw-r--r-- | theories/IntMap/Mapaxioms.v | 30 | ||||
| -rw-r--r-- | theories/IntMap/Mapc.v | 7 | ||||
| -rw-r--r-- | theories/IntMap/Mapcanon.v | 88 | ||||
| -rw-r--r-- | theories/IntMap/Mapcard.v | 222 | ||||
| -rw-r--r-- | theories/IntMap/Mapfold.v | 137 | ||||
| -rw-r--r-- | theories/IntMap/Mapiter.v | 262 | ||||
| -rw-r--r-- | theories/IntMap/Maplists.v | 29 | ||||
| -rw-r--r-- | theories/IntMap/Mapsubset.v | 47 |
16 files changed, 844 insertions, 2355 deletions
diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v index 2136bfb5..ca8e7eeb 100644 --- a/theories/IntMap/Adalloc.v +++ b/theories/IntMap/Adalloc.v @@ -5,15 +5,15 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Adalloc.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Adalloc.v 8733 2006-04-25 22:52:18Z letouzey $ i*) Require Import Bool. Require Import Sumbool. -Require Import ZArith. Require Import Arith. -Require Import Addr. -Require Import Adist. -Require Import Addec. +Require Import NArith. +Require Import Ndigits. +Require Import Ndec. +Require Import Nnat. Require Import Map. Require Import Fset. @@ -21,215 +21,36 @@ Section AdAlloc. Variable A : Set. - Definition nat_of_ad (a:ad) := - match a with - | ad_z => 0 - | ad_x p => nat_of_P p - end. - - Fixpoint nat_le (m:nat) : nat -> bool := - match m with - | O => fun _:nat => true - | S m' => - fun n:nat => match n with - | O => false - | S n' => nat_le m' n' - end - end. - - Lemma nat_le_correct : forall m n:nat, m <= n -> nat_le m n = true. - Proof. - induction m as [| m IHm]. trivial. - destruct n. intro H. elim (le_Sn_O _ H). - intros. simpl in |- *. apply IHm. apply le_S_n. assumption. - Qed. - - Lemma nat_le_complete : forall m n:nat, nat_le m n = true -> m <= n. - Proof. - induction m. trivial with arith. - destruct n. intro H. discriminate H. - auto with arith. - Qed. - - Lemma nat_le_correct_conv : forall m n:nat, m < n -> nat_le n m = false. - Proof. - intros. elim (sumbool_of_bool (nat_le n m)). intro H0. - elim (lt_irrefl _ (lt_le_trans _ _ _ H (nat_le_complete _ _ H0))). - trivial. - Qed. - - Lemma nat_le_complete_conv : forall m n:nat, nat_le n m = false -> m < n. - Proof. - intros. elim (le_or_lt n m). intro. conditional trivial rewrite nat_le_correct in H. discriminate H. - trivial. - Qed. - - Definition ad_of_nat (n:nat) := - match n with - | O => ad_z - | S n' => ad_x (P_of_succ_nat n') - end. - - Lemma ad_of_nat_of_ad : forall a:ad, ad_of_nat (nat_of_ad a) = a. - Proof. - destruct a as [| p]. reflexivity. - simpl in |- *. elim (ZL4 p). intros n H. rewrite H. simpl in |- *. rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ in H. - rewrite nat_of_P_inj with (1 := H). reflexivity. - Qed. - - Lemma nat_of_ad_of_nat : forall n:nat, nat_of_ad (ad_of_nat n) = n. - Proof. - induction n. trivial. - intros. simpl in |- *. apply nat_of_P_o_P_of_succ_nat_eq_succ. - Qed. - - Definition ad_le (a b:ad) := nat_le (nat_of_ad a) (nat_of_ad b). - - Lemma ad_le_refl : forall a:ad, ad_le a a = true. - Proof. - intro. unfold ad_le in |- *. apply nat_le_correct. apply le_n. - Qed. - - Lemma ad_le_antisym : - forall a b:ad, ad_le a b = true -> ad_le b a = true -> a = b. - Proof. - unfold ad_le in |- *. intros. rewrite <- (ad_of_nat_of_ad a). rewrite <- (ad_of_nat_of_ad b). - rewrite (le_antisym _ _ (nat_le_complete _ _ H) (nat_le_complete _ _ H0)). reflexivity. - Qed. - - Lemma ad_le_trans : - forall a b c:ad, ad_le a b = true -> ad_le b c = true -> ad_le a c = true. - Proof. - unfold ad_le in |- *. intros. apply nat_le_correct. apply le_trans with (m := nat_of_ad b). - apply nat_le_complete. assumption. - apply nat_le_complete. assumption. - Qed. - - Lemma ad_le_lt_trans : - forall a b c:ad, - ad_le a b = true -> ad_le c b = false -> ad_le c a = false. - Proof. - unfold ad_le in |- *. intros. apply nat_le_correct_conv. apply le_lt_trans with (m := nat_of_ad b). - apply nat_le_complete. assumption. - apply nat_le_complete_conv. assumption. - Qed. - - Lemma ad_lt_le_trans : - forall a b c:ad, - ad_le b a = false -> ad_le b c = true -> ad_le c a = false. - Proof. - unfold ad_le in |- *. intros. apply nat_le_correct_conv. apply lt_le_trans with (m := nat_of_ad b). - apply nat_le_complete_conv. assumption. - apply nat_le_complete. assumption. - Qed. - - Lemma ad_lt_trans : - forall a b c:ad, - ad_le b a = false -> ad_le c b = false -> ad_le c a = false. - Proof. - unfold ad_le in |- *. intros. apply nat_le_correct_conv. apply lt_trans with (m := nat_of_ad b). - apply nat_le_complete_conv. assumption. - apply nat_le_complete_conv. assumption. - Qed. - - Lemma ad_lt_le_weak : forall a b:ad, ad_le b a = false -> ad_le a b = true. - Proof. - unfold ad_le in |- *. intros. apply nat_le_correct. apply lt_le_weak. - apply nat_le_complete_conv. assumption. - Qed. - - Definition ad_min (a b:ad) := if ad_le a b then a else b. - - Lemma ad_min_choice : forall a b:ad, {ad_min a b = a} + {ad_min a b = b}. - Proof. - unfold ad_min in |- *. intros. elim (sumbool_of_bool (ad_le a b)). intro H. left. rewrite H. - reflexivity. - intro H. right. rewrite H. reflexivity. - Qed. - - Lemma ad_min_le_1 : forall a b:ad, ad_le (ad_min a b) a = true. - Proof. - unfold ad_min in |- *. intros. elim (sumbool_of_bool (ad_le a b)). intro H. rewrite H. - apply ad_le_refl. - intro H. rewrite H. apply ad_lt_le_weak. assumption. - Qed. - - Lemma ad_min_le_2 : forall a b:ad, ad_le (ad_min a b) b = true. - Proof. - unfold ad_min in |- *. intros. elim (sumbool_of_bool (ad_le a b)). intro H. rewrite H. assumption. - intro H. rewrite H. apply ad_le_refl. - Qed. - - Lemma ad_min_le_3 : - forall a b c:ad, ad_le a (ad_min b c) = true -> ad_le a b = true. - Proof. - unfold ad_min in |- *. intros. elim (sumbool_of_bool (ad_le b c)). intro H0. rewrite H0 in H. - assumption. - intro H0. rewrite H0 in H. apply ad_lt_le_weak. apply ad_le_lt_trans with (b := c); assumption. - Qed. - - Lemma ad_min_le_4 : - forall a b c:ad, ad_le a (ad_min b c) = true -> ad_le a c = true. - Proof. - unfold ad_min in |- *. intros. elim (sumbool_of_bool (ad_le b c)). intro H0. rewrite H0 in H. - apply ad_le_trans with (b := b); assumption. - intro H0. rewrite H0 in H. assumption. - Qed. - - Lemma ad_min_le_5 : - forall a b c:ad, - ad_le a b = true -> ad_le a c = true -> ad_le a (ad_min b c) = true. - Proof. - intros. elim (ad_min_choice b c). intro H1. rewrite H1. assumption. - intro H1. rewrite H1. assumption. - Qed. - - Lemma ad_min_lt_3 : - forall a b c:ad, ad_le (ad_min b c) a = false -> ad_le b a = false. - Proof. - unfold ad_min in |- *. intros. elim (sumbool_of_bool (ad_le b c)). intro H0. rewrite H0 in H. - assumption. - intro H0. rewrite H0 in H. apply ad_lt_trans with (b := c); assumption. - Qed. - - Lemma ad_min_lt_4 : - forall a b c:ad, ad_le (ad_min b c) a = false -> ad_le c a = false. - Proof. - unfold ad_min in |- *. intros. elim (sumbool_of_bool (ad_le b c)). intro H0. rewrite H0 in H. - apply ad_lt_le_trans with (b := b); assumption. - intro H0. rewrite H0 in H. assumption. - Qed. - (** Allocator: returns an address not in the domain of [m]. This allocator is optimal in that it returns the lowest possible address, in the usual ordering on integers. It is not the most efficient, however. *) Fixpoint ad_alloc_opt (m:Map A) : ad := match m with - | M0 => ad_z - | M1 a _ => if ad_eq a ad_z then ad_x 1 else ad_z + | M0 => N0 + | M1 a _ => if Neqb a N0 then Npos 1 else N0 | M2 m1 m2 => - ad_min (ad_double (ad_alloc_opt m1)) - (ad_double_plus_un (ad_alloc_opt m2)) + Nmin (Ndouble (ad_alloc_opt m1)) + (Ndouble_plus_one (ad_alloc_opt m2)) end. Lemma ad_alloc_opt_allocates_1 : - forall m:Map A, MapGet A m (ad_alloc_opt m) = NONE A. + forall m:Map A, MapGet A m (ad_alloc_opt m) = None. Proof. induction m as [| a| m0 H m1 H0]. reflexivity. - simpl in |- *. elim (sumbool_of_bool (ad_eq a ad_z)). intro H. rewrite H. - rewrite (ad_eq_complete _ _ H). reflexivity. + simpl in |- *. elim (sumbool_of_bool (Neqb a N0)). intro H. rewrite H. + rewrite (Neqb_complete _ _ H). reflexivity. intro H. rewrite H. rewrite H. reflexivity. intros. change - (ad_alloc_opt (M2 A m0 m1)) with (ad_min (ad_double (ad_alloc_opt m0)) - (ad_double_plus_un (ad_alloc_opt m1))) + (ad_alloc_opt (M2 A m0 m1)) with (Nmin (Ndouble (ad_alloc_opt m0)) + (Ndouble_plus_one (ad_alloc_opt m1))) in |- *. elim - (ad_min_choice (ad_double (ad_alloc_opt m0)) - (ad_double_plus_un (ad_alloc_opt m1))). - intro H1. rewrite H1. rewrite MapGet_M2_bit_0_0. rewrite ad_double_div_2. assumption. - apply ad_double_bit_0. - intro H1. rewrite H1. rewrite MapGet_M2_bit_0_1. rewrite ad_double_plus_un_div_2. assumption. - apply ad_double_plus_un_bit_0. + (Nmin_choice (Ndouble (ad_alloc_opt m0)) + (Ndouble_plus_one (ad_alloc_opt m1))). + intro H1. rewrite H1. rewrite MapGet_M2_bit_0_0. rewrite Ndouble_div2. assumption. + apply Ndouble_bit0. + intro H1. rewrite H1. rewrite MapGet_M2_bit_0_1. rewrite Ndouble_plus_one_div2. assumption. + apply Ndouble_plus_one_bit0. Qed. Lemma ad_alloc_opt_allocates : @@ -241,122 +62,30 @@ Section AdAlloc. (** Moreover, this is optimal: all addresses below [(ad_alloc_opt m)] are in [dom m]: *) - Lemma nat_of_ad_double : - forall a:ad, nat_of_ad (ad_double a) = 2 * nat_of_ad a. - Proof. - destruct a as [| p]. trivial. - exact (nat_of_P_xO p). - Qed. - - Lemma nat_of_ad_double_plus_un : - forall a:ad, nat_of_ad (ad_double_plus_un a) = S (2 * nat_of_ad a). - Proof. - destruct a as [| p]. trivial. - exact (nat_of_P_xI p). - Qed. - - Lemma ad_le_double_mono : - forall a b:ad, - ad_le a b = true -> ad_le (ad_double a) (ad_double b) = true. - Proof. - unfold ad_le in |- *. intros. rewrite nat_of_ad_double. rewrite nat_of_ad_double. apply nat_le_correct. - simpl in |- *. apply plus_le_compat. apply nat_le_complete. assumption. - apply plus_le_compat. apply nat_le_complete. assumption. - apply le_n. - Qed. - - Lemma ad_le_double_plus_un_mono : - forall a b:ad, - ad_le a b = true -> - ad_le (ad_double_plus_un a) (ad_double_plus_un b) = true. - Proof. - unfold ad_le in |- *. intros. rewrite nat_of_ad_double_plus_un. rewrite nat_of_ad_double_plus_un. - apply nat_le_correct. apply le_n_S. simpl in |- *. apply plus_le_compat. apply nat_le_complete. - assumption. - apply plus_le_compat. apply nat_le_complete. assumption. - apply le_n. - Qed. - - Lemma ad_le_double_mono_conv : - forall a b:ad, - ad_le (ad_double a) (ad_double b) = true -> ad_le a b = true. - Proof. - unfold ad_le in |- *. intros a b. rewrite nat_of_ad_double. rewrite nat_of_ad_double. intro. - apply nat_le_correct. apply (mult_S_le_reg_l 1). apply nat_le_complete. assumption. - Qed. - - Lemma ad_le_double_plus_un_mono_conv : - forall a b:ad, - ad_le (ad_double_plus_un a) (ad_double_plus_un b) = true -> - ad_le a b = true. - Proof. - unfold ad_le in |- *. intros a b. rewrite nat_of_ad_double_plus_un. rewrite nat_of_ad_double_plus_un. - intro. apply nat_le_correct. apply (mult_S_le_reg_l 1). apply le_S_n. apply nat_le_complete. - assumption. - Qed. - - Lemma ad_lt_double_mono : - forall a b:ad, - ad_le a b = false -> ad_le (ad_double a) (ad_double b) = false. - Proof. - intros. elim (sumbool_of_bool (ad_le (ad_double a) (ad_double b))). intro H0. - rewrite (ad_le_double_mono_conv _ _ H0) in H. discriminate H. - trivial. - Qed. - - Lemma ad_lt_double_plus_un_mono : - forall a b:ad, - ad_le a b = false -> - ad_le (ad_double_plus_un a) (ad_double_plus_un b) = false. - Proof. - intros. elim (sumbool_of_bool (ad_le (ad_double_plus_un a) (ad_double_plus_un b))). intro H0. - rewrite (ad_le_double_plus_un_mono_conv _ _ H0) in H. discriminate H. - trivial. - Qed. - - Lemma ad_lt_double_mono_conv : - forall a b:ad, - ad_le (ad_double a) (ad_double b) = false -> ad_le a b = false. - Proof. - intros. elim (sumbool_of_bool (ad_le a b)). intro H0. rewrite (ad_le_double_mono _ _ H0) in H. - discriminate H. - trivial. - Qed. - - Lemma ad_lt_double_plus_un_mono_conv : - forall a b:ad, - ad_le (ad_double_plus_un a) (ad_double_plus_un b) = false -> - ad_le a b = false. - Proof. - intros. elim (sumbool_of_bool (ad_le a b)). intro H0. - rewrite (ad_le_double_plus_un_mono _ _ H0) in H. discriminate H. - trivial. - Qed. - Lemma ad_alloc_opt_optimal_1 : forall (m:Map A) (a:ad), - ad_le (ad_alloc_opt m) a = false -> {y : A | MapGet A m a = SOME A y}. + Nle (ad_alloc_opt m) a = false -> {y : A | MapGet A m a = Some y}. Proof. - induction m as [| a y| m0 H m1 H0]. simpl in |- *. unfold ad_le in |- *. simpl in |- *. intros. discriminate H. - simpl in |- *. intros b H. elim (sumbool_of_bool (ad_eq a ad_z)). intro H0. rewrite H0 in H. - unfold ad_le in H. cut (ad_z = b). intro. split with y. rewrite <- H1. rewrite H0. reflexivity. - rewrite <- (ad_of_nat_of_ad b). - rewrite <- (le_n_O_eq _ (le_S_n _ _ (nat_le_complete_conv _ _ H))). reflexivity. + induction m as [| a y| m0 H m1 H0]. simpl in |- *. unfold Nle in |- *. simpl in |- *. intros. discriminate H. + simpl in |- *. intros b H. elim (sumbool_of_bool (Neqb a N0)). intro H0. rewrite H0 in H. + unfold Nle in H. cut (N0 = b). intro. split with y. rewrite <- H1. rewrite H0. reflexivity. + rewrite <- (N_of_nat_of_N b). + rewrite <- (le_n_O_eq _ (le_S_n _ _ (leb_complete_conv _ _ H))). reflexivity. intro H0. rewrite H0 in H. discriminate H. - intros. simpl in H1. elim (ad_double_or_double_plus_un a). intro H2. elim H2. intros a0 H3. - rewrite H3 in H1. elim (H _ (ad_lt_double_mono_conv _ _ (ad_min_lt_3 _ _ _ H1))). intros y H4. - split with y. rewrite H3. rewrite MapGet_M2_bit_0_0. rewrite ad_double_div_2. assumption. - apply ad_double_bit_0. + intros. simpl in H1. elim (Ndouble_or_double_plus_un a). intro H2. elim H2. intros a0 H3. + rewrite H3 in H1. elim (H _ (Nlt_double_mono_conv _ _ (Nmin_lt_3 _ _ _ H1))). intros y H4. + split with y. rewrite H3. rewrite MapGet_M2_bit_0_0. rewrite Ndouble_div2. assumption. + apply Ndouble_bit0. intro H2. elim H2. intros a0 H3. rewrite H3 in H1. - elim (H0 _ (ad_lt_double_plus_un_mono_conv _ _ (ad_min_lt_4 _ _ _ H1))). intros y H4. - split with y. rewrite H3. rewrite MapGet_M2_bit_0_1. rewrite ad_double_plus_un_div_2. + elim (H0 _ (Nlt_double_plus_one_mono_conv _ _ (Nmin_lt_4 _ _ _ H1))). intros y H4. + split with y. rewrite H3. rewrite MapGet_M2_bit_0_1. rewrite Ndouble_plus_one_div2. assumption. - apply ad_double_plus_un_bit_0. + apply Ndouble_plus_one_bit0. Qed. Lemma ad_alloc_opt_optimal : forall (m:Map A) (a:ad), - ad_le (ad_alloc_opt m) a = false -> in_dom A a m = true. + Nle (ad_alloc_opt m) a = false -> in_dom A a m = true. Proof. intros. unfold in_dom in |- *. elim (ad_alloc_opt_optimal_1 m a H). intros y H0. rewrite H0. reflexivity. diff --git a/theories/IntMap/Addec.v b/theories/IntMap/Addec.v deleted file mode 100644 index f1a937a3..00000000 --- a/theories/IntMap/Addec.v +++ /dev/null @@ -1,193 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(*i $Id: Addec.v 5920 2004-07-16 20:01:26Z herbelin $ i*) - -(** Equality on adresses *) - -Require Import Bool. -Require Import Sumbool. -Require Import ZArith. -Require Import Addr. - -Fixpoint ad_eq_1 (p1 p2:positive) {struct p2} : bool := - match p1, p2 with - | xH, xH => true - | xO p'1, xO p'2 => ad_eq_1 p'1 p'2 - | xI p'1, xI p'2 => ad_eq_1 p'1 p'2 - | _, _ => false - end. - -Definition ad_eq (a a':ad) := - match a, a' with - | ad_z, ad_z => true - | ad_x p, ad_x p' => ad_eq_1 p p' - | _, _ => false - end. - -Lemma ad_eq_correct : forall a:ad, ad_eq a a = true. -Proof. - destruct a; trivial. - induction p; trivial. -Qed. - -Lemma ad_eq_complete : forall a a':ad, ad_eq a a' = true -> a = a'. -Proof. - destruct a. destruct a'; trivial. destruct p. - discriminate 1. - discriminate 1. - discriminate 1. - destruct a'. intros. discriminate H. - unfold ad_eq in |- *. intros. cut (p = p0). intros. rewrite H0. reflexivity. - generalize dependent p0. - induction p as [p IHp| p IHp| ]. destruct p0; intro H. - rewrite (IHp p0). reflexivity. - exact H. - discriminate H. - discriminate H. - destruct p0; intro H. discriminate H. - rewrite (IHp p0 H). reflexivity. - discriminate H. - destruct p0 as [p| p| ]; intro H. discriminate H. - discriminate H. - trivial. -Qed. - -Lemma ad_eq_comm : forall a a':ad, ad_eq a a' = ad_eq a' a. -Proof. - intros. cut (forall b b':bool, ad_eq a a' = b -> ad_eq a' a = b' -> b = b'). - intros. apply H. reflexivity. - reflexivity. - destruct b. intros. cut (a = a'). - intro. rewrite H1 in H0. rewrite (ad_eq_correct a') in H0. exact H0. - apply ad_eq_complete. exact H. - destruct b'. intros. cut (a' = a). - intro. rewrite H1 in H. rewrite H1 in H0. rewrite <- H. exact H0. - apply ad_eq_complete. exact H0. - trivial. -Qed. - -Lemma ad_xor_eq_true : - forall a a':ad, ad_xor a a' = ad_z -> ad_eq a a' = true. -Proof. - intros. rewrite (ad_xor_eq a a' H). apply ad_eq_correct. -Qed. - -Lemma ad_xor_eq_false : - forall (a a':ad) (p:positive), ad_xor a a' = ad_x p -> ad_eq a a' = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq a a')). intro H0. - rewrite (ad_eq_complete a a' H0) in H. rewrite (ad_xor_nilpotent a') in H. discriminate H. - trivial. -Qed. - -Lemma ad_bit_0_1_not_double : - forall a:ad, - ad_bit_0 a = true -> forall a0:ad, ad_eq (ad_double a0) a = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq (ad_double a0) a)). intro H0. - rewrite <- (ad_eq_complete _ _ H0) in H. rewrite (ad_double_bit_0 a0) in H. discriminate H. - trivial. -Qed. - -Lemma ad_not_div_2_not_double : - forall a a0:ad, - ad_eq (ad_div_2 a) a0 = false -> ad_eq a (ad_double a0) = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq (ad_double a0) a)). intro H0. - rewrite <- (ad_eq_complete _ _ H0) in H. rewrite (ad_double_div_2 a0) in H. - rewrite (ad_eq_correct a0) in H. discriminate H. - intro. rewrite ad_eq_comm. assumption. -Qed. - -Lemma ad_bit_0_0_not_double_plus_un : - forall a:ad, - ad_bit_0 a = false -> forall a0:ad, ad_eq (ad_double_plus_un a0) a = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq (ad_double_plus_un a0) a)). intro H0. - rewrite <- (ad_eq_complete _ _ H0) in H. rewrite (ad_double_plus_un_bit_0 a0) in H. - discriminate H. - trivial. -Qed. - -Lemma ad_not_div_2_not_double_plus_un : - forall a a0:ad, - ad_eq (ad_div_2 a) a0 = false -> ad_eq (ad_double_plus_un a0) a = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq a (ad_double_plus_un a0))). intro H0. - rewrite (ad_eq_complete _ _ H0) in H. rewrite (ad_double_plus_un_div_2 a0) in H. - rewrite (ad_eq_correct a0) in H. discriminate H. - intro H0. rewrite ad_eq_comm. assumption. -Qed. - -Lemma ad_bit_0_neq : - forall a a':ad, - ad_bit_0 a = false -> ad_bit_0 a' = true -> ad_eq a a' = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq a a')). intro H1. rewrite (ad_eq_complete _ _ H1) in H. - rewrite H in H0. discriminate H0. - trivial. -Qed. - -Lemma ad_div_eq : - forall a a':ad, ad_eq a a' = true -> ad_eq (ad_div_2 a) (ad_div_2 a') = true. -Proof. - intros. cut (a = a'). intros. rewrite H0. apply ad_eq_correct. - apply ad_eq_complete. exact H. -Qed. - -Lemma ad_div_neq : - forall a a':ad, - ad_eq (ad_div_2 a) (ad_div_2 a') = false -> ad_eq a a' = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq a a')). intro H0. - rewrite (ad_eq_complete _ _ H0) in H. rewrite (ad_eq_correct (ad_div_2 a')) in H. discriminate H. - trivial. -Qed. - -Lemma ad_div_bit_eq : - forall a a':ad, - ad_bit_0 a = ad_bit_0 a' -> ad_div_2 a = ad_div_2 a' -> a = a'. -Proof. - intros. apply ad_faithful. unfold eqf in |- *. destruct n. - rewrite ad_bit_0_correct. rewrite ad_bit_0_correct. assumption. - rewrite <- ad_div_2_correct. rewrite <- ad_div_2_correct. - rewrite H0. reflexivity. -Qed. - -Lemma ad_div_bit_neq : - forall a a':ad, - ad_eq a a' = false -> - ad_bit_0 a = ad_bit_0 a' -> ad_eq (ad_div_2 a) (ad_div_2 a') = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq (ad_div_2 a) (ad_div_2 a'))). intro H1. - rewrite (ad_div_bit_eq _ _ H0 (ad_eq_complete _ _ H1)) in H. - rewrite (ad_eq_correct a') in H. discriminate H. - trivial. -Qed. - -Lemma ad_neq : - forall a a':ad, - ad_eq a a' = false -> - ad_bit_0 a = negb (ad_bit_0 a') \/ - ad_eq (ad_div_2 a) (ad_div_2 a') = false. -Proof. - intros. cut (ad_bit_0 a = ad_bit_0 a' \/ ad_bit_0 a = negb (ad_bit_0 a')). - intros. elim H0. intro. right. apply ad_div_bit_neq. assumption. - assumption. - intro. left. assumption. - case (ad_bit_0 a); case (ad_bit_0 a'); auto. -Qed. - -Lemma ad_double_or_double_plus_un : - forall a:ad, - {a0 : ad | a = ad_double a0} + {a1 : ad | a = ad_double_plus_un a1}. -Proof. - intro. elim (sumbool_of_bool (ad_bit_0 a)). intro H. right. split with (ad_div_2 a). - rewrite (ad_div_2_double_plus_un a H). reflexivity. - intro H. left. split with (ad_div_2 a). rewrite (ad_div_2_double a H). reflexivity. -Qed.
\ No newline at end of file diff --git a/theories/IntMap/Addr.v b/theories/IntMap/Addr.v deleted file mode 100644 index 727117b3..00000000 --- a/theories/IntMap/Addr.v +++ /dev/null @@ -1,491 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(*i $Id: Addr.v 5920 2004-07-16 20:01:26Z herbelin $ i*) - -(** Representation of adresses by the [positive] type of binary numbers *) - -Require Import Bool. -Require Import ZArith. - -Inductive ad : Set := - | ad_z : ad - | ad_x : positive -> ad. - -Lemma ad_sum : forall a:ad, {p : positive | a = ad_x p} + {a = ad_z}. -Proof. - destruct a; auto. - left; exists p; trivial. -Qed. - -Fixpoint p_xor (p p2:positive) {struct p} : ad := - match p with - | xH => - match p2 with - | xH => ad_z - | xO p'2 => ad_x (xI p'2) - | xI p'2 => ad_x (xO p'2) - end - | xO p' => - match p2 with - | xH => ad_x (xI p') - | xO p'2 => - match p_xor p' p'2 with - | ad_z => ad_z - | ad_x p'' => ad_x (xO p'') - end - | xI p'2 => - match p_xor p' p'2 with - | ad_z => ad_x 1 - | ad_x p'' => ad_x (xI p'') - end - end - | xI p' => - match p2 with - | xH => ad_x (xO p') - | xO p'2 => - match p_xor p' p'2 with - | ad_z => ad_x 1 - | ad_x p'' => ad_x (xI p'') - end - | xI p'2 => - match p_xor p' p'2 with - | ad_z => ad_z - | ad_x p'' => ad_x (xO p'') - end - end - end. - -Definition ad_xor (a a':ad) := - match a with - | ad_z => a' - | ad_x p => match a' with - | ad_z => a - | ad_x p' => p_xor p p' - end - end. - -Lemma ad_xor_neutral_left : forall a:ad, ad_xor ad_z a = a. -Proof. - trivial. -Qed. - -Lemma ad_xor_neutral_right : forall a:ad, ad_xor a ad_z = a. -Proof. - destruct a; trivial. -Qed. - -Lemma ad_xor_comm : forall a a':ad, ad_xor a a' = ad_xor a' a. -Proof. - destruct a; destruct a'; simpl in |- *; auto. - generalize p0; clear p0; induction p as [p Hrecp| p Hrecp| ]; simpl in |- *; - auto. - destruct p0; simpl in |- *; trivial; intros. - rewrite Hrecp; trivial. - rewrite Hrecp; trivial. - destruct p0; simpl in |- *; trivial; intros. - rewrite Hrecp; trivial. - rewrite Hrecp; trivial. - destruct p0 as [p| p| ]; simpl in |- *; auto. -Qed. - -Lemma ad_xor_nilpotent : forall a:ad, ad_xor a a = ad_z. -Proof. - destruct a; trivial. - simpl in |- *. induction p as [p IHp| p IHp| ]; trivial. - simpl in |- *. rewrite IHp; reflexivity. - simpl in |- *. rewrite IHp; reflexivity. -Qed. - -Fixpoint ad_bit_1 (p:positive) : nat -> bool := - match p with - | xH => fun n:nat => match n with - | O => true - | S _ => false - end - | xO p => - fun n:nat => match n with - | O => false - | S n' => ad_bit_1 p n' - end - | xI p => fun n:nat => match n with - | O => true - | S n' => ad_bit_1 p n' - end - end. - -Definition ad_bit (a:ad) := - match a with - | ad_z => fun _:nat => false - | ad_x p => ad_bit_1 p - end. - -Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n. - -Lemma ad_faithful_1 : forall a:ad, eqf (ad_bit ad_z) (ad_bit a) -> ad_z = a. -Proof. - destruct a. trivial. - induction p as [p IHp| p IHp| ]; intro H. absurd (ad_z = ad_x p). discriminate. - exact (IHp (fun n:nat => H (S n))). - absurd (ad_z = ad_x p). discriminate. - exact (IHp (fun n:nat => H (S n))). - absurd (false = true). discriminate. - exact (H 0). -Qed. - -Lemma ad_faithful_2 : - forall a:ad, eqf (ad_bit (ad_x 1)) (ad_bit a) -> ad_x 1 = a. -Proof. - destruct a. intros. absurd (true = false). discriminate. - exact (H 0). - destruct p. intro H. absurd (ad_z = ad_x p). discriminate. - exact (ad_faithful_1 (ad_x p) (fun n:nat => H (S n))). - intros. absurd (true = false). discriminate. - exact (H 0). - trivial. -Qed. - -Lemma ad_faithful_3 : - forall (a:ad) (p:positive), - (forall p':positive, eqf (ad_bit (ad_x p)) (ad_bit (ad_x p')) -> p = p') -> - eqf (ad_bit (ad_x (xO p))) (ad_bit a) -> ad_x (xO p) = a. -Proof. - destruct a. intros. cut (eqf (ad_bit ad_z) (ad_bit (ad_x (xO p)))). - intro. rewrite (ad_faithful_1 (ad_x (xO p)) H1). reflexivity. - unfold eqf in |- *. intro. unfold eqf in H0. rewrite H0. reflexivity. - case p. intros. absurd (false = true). discriminate. - exact (H0 0). - intros. rewrite (H p0 (fun n:nat => H0 (S n))). reflexivity. - intros. absurd (false = true). discriminate. - exact (H0 0). -Qed. - -Lemma ad_faithful_4 : - forall (a:ad) (p:positive), - (forall p':positive, eqf (ad_bit (ad_x p)) (ad_bit (ad_x p')) -> p = p') -> - eqf (ad_bit (ad_x (xI p))) (ad_bit a) -> ad_x (xI p) = a. -Proof. - destruct a. intros. cut (eqf (ad_bit ad_z) (ad_bit (ad_x (xI p)))). - intro. rewrite (ad_faithful_1 (ad_x (xI p)) H1). reflexivity. - unfold eqf in |- *. intro. unfold eqf in H0. rewrite H0. reflexivity. - case p. intros. rewrite (H p0 (fun n:nat => H0 (S n))). reflexivity. - intros. absurd (true = false). discriminate. - exact (H0 0). - intros. absurd (ad_z = ad_x p0). discriminate. - cut (eqf (ad_bit (ad_x 1)) (ad_bit (ad_x (xI p0)))). - intro. exact (ad_faithful_1 (ad_x p0) (fun n:nat => H1 (S n))). - unfold eqf in |- *. unfold eqf in H0. intro. rewrite H0. reflexivity. -Qed. - -Lemma ad_faithful : forall a a':ad, eqf (ad_bit a) (ad_bit a') -> a = a'. -Proof. - destruct a. exact ad_faithful_1. - induction p. intros a' H. apply ad_faithful_4. intros. cut (ad_x p = ad_x p'). - intro. inversion H1. reflexivity. - exact (IHp (ad_x p') H0). - assumption. - intros. apply ad_faithful_3. intros. cut (ad_x p = ad_x p'). intro. inversion H1. reflexivity. - exact (IHp (ad_x p') H0). - assumption. - exact ad_faithful_2. -Qed. - -Definition adf_xor (f g:nat -> bool) (n:nat) := xorb (f n) (g n). - -Lemma ad_xor_sem_1 : forall a':ad, ad_bit (ad_xor ad_z a') 0 = ad_bit a' 0. -Proof. - trivial. -Qed. - -Lemma ad_xor_sem_2 : - forall a':ad, ad_bit (ad_xor (ad_x 1) a') 0 = negb (ad_bit a' 0). -Proof. - intro. case a'. trivial. - simpl in |- *. intro. - case p; trivial. -Qed. - -Lemma ad_xor_sem_3 : - forall (p:positive) (a':ad), - ad_bit (ad_xor (ad_x (xO p)) a') 0 = ad_bit a' 0. -Proof. - intros. case a'. trivial. - simpl in |- *. intro. - case p0; trivial. intro. - case (p_xor p p1); trivial. - intro. case (p_xor p p1); trivial. -Qed. - -Lemma ad_xor_sem_4 : - forall (p:positive) (a':ad), - ad_bit (ad_xor (ad_x (xI p)) a') 0 = negb (ad_bit a' 0). -Proof. - intros. case a'. trivial. - simpl in |- *. intro. case p0; trivial. intro. - case (p_xor p p1); trivial. - intro. - case (p_xor p p1); trivial. -Qed. - -Lemma ad_xor_sem_5 : - forall a a':ad, ad_bit (ad_xor a a') 0 = adf_xor (ad_bit a) (ad_bit a') 0. -Proof. - destruct a. intro. change (ad_bit a' 0 = xorb false (ad_bit a' 0)) in |- *. rewrite false_xorb. trivial. - case p. exact ad_xor_sem_4. - intros. change (ad_bit (ad_xor (ad_x (xO p0)) a') 0 = xorb false (ad_bit a' 0)) - in |- *. - rewrite false_xorb. apply ad_xor_sem_3. exact ad_xor_sem_2. -Qed. - -Lemma ad_xor_sem_6 : - forall n:nat, - (forall a a':ad, ad_bit (ad_xor a a') n = adf_xor (ad_bit a) (ad_bit a') n) -> - forall a a':ad, - ad_bit (ad_xor a a') (S n) = adf_xor (ad_bit a) (ad_bit a') (S n). -Proof. - intros. case a. unfold adf_xor in |- *. unfold ad_bit at 2 in |- *. rewrite false_xorb. reflexivity. - case a'. unfold adf_xor in |- *. unfold ad_bit at 3 in |- *. intro. rewrite xorb_false. reflexivity. - intros. case p0. case p. intros. - change - (ad_bit (ad_xor (ad_x (xI p2)) (ad_x (xI p1))) (S n) = - adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n) - in |- *. - rewrite <- H. simpl in |- *. - case (p_xor p2 p1); trivial. - intros. - change - (ad_bit (ad_xor (ad_x (xI p2)) (ad_x (xO p1))) (S n) = - adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n) - in |- *. - rewrite <- H. simpl in |- *. - case (p_xor p2 p1); trivial. - intro. unfold adf_xor in |- *. unfold ad_bit at 3 in |- *. unfold ad_bit_1 in |- *. rewrite xorb_false. reflexivity. - case p. intros. - change - (ad_bit (ad_xor (ad_x (xO p2)) (ad_x (xI p1))) (S n) = - adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n) - in |- *. - rewrite <- H. simpl in |- *. - case (p_xor p2 p1); trivial. - intros. - change - (ad_bit (ad_xor (ad_x (xO p2)) (ad_x (xO p1))) (S n) = - adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n) - in |- *. - rewrite <- H. simpl in |- *. - case (p_xor p2 p1); trivial. - intro. unfold adf_xor in |- *. unfold ad_bit at 3 in |- *. unfold ad_bit_1 in |- *. rewrite xorb_false. reflexivity. - unfold adf_xor in |- *. unfold ad_bit at 2 in |- *. unfold ad_bit_1 in |- *. rewrite false_xorb. simpl in |- *. case p; trivial. -Qed. - -Lemma ad_xor_semantics : - forall a a':ad, eqf (ad_bit (ad_xor a a')) (adf_xor (ad_bit a) (ad_bit a')). -Proof. - unfold eqf in |- *. intros. generalize a a'. elim n. exact ad_xor_sem_5. - exact ad_xor_sem_6. -Qed. - -Lemma eqf_sym : forall f f':nat -> bool, eqf f f' -> eqf f' f. -Proof. - unfold eqf in |- *. intros. rewrite H. reflexivity. -Qed. - -Lemma eqf_refl : forall f:nat -> bool, eqf f f. -Proof. - unfold eqf in |- *. trivial. -Qed. - -Lemma eqf_trans : - forall f f' f'':nat -> bool, eqf f f' -> eqf f' f'' -> eqf f f''. -Proof. - unfold eqf in |- *. intros. rewrite H. exact (H0 n). -Qed. - -Lemma adf_xor_eq : - forall f f':nat -> bool, eqf (adf_xor f f') (fun n:nat => false) -> eqf f f'. -Proof. - unfold eqf in |- *. unfold adf_xor in |- *. intros. apply xorb_eq. apply H. -Qed. - -Lemma ad_xor_eq : forall a a':ad, ad_xor a a' = ad_z -> a = a'. -Proof. - intros. apply ad_faithful. apply adf_xor_eq. apply eqf_trans with (f' := ad_bit (ad_xor a a')). - apply eqf_sym. apply ad_xor_semantics. - rewrite H. unfold eqf in |- *. trivial. -Qed. - -Lemma adf_xor_assoc : - forall f f' f'':nat -> bool, - eqf (adf_xor (adf_xor f f') f'') (adf_xor f (adf_xor f' f'')). -Proof. - unfold eqf in |- *. unfold adf_xor in |- *. intros. apply xorb_assoc. -Qed. - -Lemma eqf_xor_1 : - forall f f' f'' f''':nat -> bool, - eqf f f' -> eqf f'' f''' -> eqf (adf_xor f f'') (adf_xor f' f'''). -Proof. - unfold eqf in |- *. intros. unfold adf_xor in |- *. rewrite H. rewrite H0. reflexivity. -Qed. - -Lemma ad_xor_assoc : - forall a a' a'':ad, ad_xor (ad_xor a a') a'' = ad_xor a (ad_xor a' a''). -Proof. - intros. apply ad_faithful. - apply eqf_trans with - (f' := adf_xor (adf_xor (ad_bit a) (ad_bit a')) (ad_bit a'')). - apply eqf_trans with (f' := adf_xor (ad_bit (ad_xor a a')) (ad_bit a'')). - apply ad_xor_semantics. - apply eqf_xor_1. apply ad_xor_semantics. - apply eqf_refl. - apply eqf_trans with - (f' := adf_xor (ad_bit a) (adf_xor (ad_bit a') (ad_bit a''))). - apply adf_xor_assoc. - apply eqf_trans with (f' := adf_xor (ad_bit a) (ad_bit (ad_xor a' a''))). - apply eqf_xor_1. apply eqf_refl. - apply eqf_sym. apply ad_xor_semantics. - apply eqf_sym. apply ad_xor_semantics. -Qed. - -Definition ad_double (a:ad) := - match a with - | ad_z => ad_z - | ad_x p => ad_x (xO p) - end. - -Definition ad_double_plus_un (a:ad) := - match a with - | ad_z => ad_x 1 - | ad_x p => ad_x (xI p) - end. - -Definition ad_div_2 (a:ad) := - match a with - | ad_z => ad_z - | ad_x xH => ad_z - | ad_x (xO p) => ad_x p - | ad_x (xI p) => ad_x p - end. - -Lemma ad_double_div_2 : forall a:ad, ad_div_2 (ad_double a) = a. -Proof. - destruct a; trivial. -Qed. - -Lemma ad_double_plus_un_div_2 : - forall a:ad, ad_div_2 (ad_double_plus_un a) = a. -Proof. - destruct a; trivial. -Qed. - -Lemma ad_double_inj : forall a0 a1:ad, ad_double a0 = ad_double a1 -> a0 = a1. -Proof. - intros. rewrite <- (ad_double_div_2 a0). rewrite H. apply ad_double_div_2. -Qed. - -Lemma ad_double_plus_un_inj : - forall a0 a1:ad, ad_double_plus_un a0 = ad_double_plus_un a1 -> a0 = a1. -Proof. - intros. rewrite <- (ad_double_plus_un_div_2 a0). rewrite H. apply ad_double_plus_un_div_2. -Qed. - -Definition ad_bit_0 (a:ad) := - match a with - | ad_z => false - | ad_x (xO _) => false - | _ => true - end. - -Lemma ad_double_bit_0 : forall a:ad, ad_bit_0 (ad_double a) = false. -Proof. - destruct a; trivial. -Qed. - -Lemma ad_double_plus_un_bit_0 : - forall a:ad, ad_bit_0 (ad_double_plus_un a) = true. -Proof. - destruct a; trivial. -Qed. - -Lemma ad_div_2_double : - forall a:ad, ad_bit_0 a = false -> ad_double (ad_div_2 a) = a. -Proof. - destruct a. trivial. destruct p. intro H. discriminate H. - intros. reflexivity. - intro H. discriminate H. -Qed. - -Lemma ad_div_2_double_plus_un : - forall a:ad, ad_bit_0 a = true -> ad_double_plus_un (ad_div_2 a) = a. -Proof. - destruct a. intro. discriminate H. - destruct p. intros. reflexivity. - intro H. discriminate H. - intro. reflexivity. -Qed. - -Lemma ad_bit_0_correct : forall a:ad, ad_bit a 0 = ad_bit_0 a. -Proof. - destruct a; trivial. - destruct p; trivial. -Qed. - -Lemma ad_div_2_correct : - forall (a:ad) (n:nat), ad_bit (ad_div_2 a) n = ad_bit a (S n). -Proof. - destruct a; trivial. - destruct p; trivial. -Qed. - -Lemma ad_xor_bit_0 : - forall a a':ad, ad_bit_0 (ad_xor a a') = xorb (ad_bit_0 a) (ad_bit_0 a'). -Proof. - intros. rewrite <- ad_bit_0_correct. rewrite (ad_xor_semantics a a' 0). - unfold adf_xor in |- *. rewrite ad_bit_0_correct. rewrite ad_bit_0_correct. reflexivity. -Qed. - -Lemma ad_xor_div_2 : - forall a a':ad, ad_div_2 (ad_xor a a') = ad_xor (ad_div_2 a) (ad_div_2 a'). -Proof. - intros. apply ad_faithful. unfold eqf in |- *. intro. - rewrite (ad_xor_semantics (ad_div_2 a) (ad_div_2 a') n). - rewrite ad_div_2_correct. - rewrite (ad_xor_semantics a a' (S n)). - unfold adf_xor in |- *. rewrite ad_div_2_correct. rewrite ad_div_2_correct. - reflexivity. -Qed. - -Lemma ad_neg_bit_0 : - forall a a':ad, - ad_bit_0 (ad_xor a a') = true -> ad_bit_0 a = negb (ad_bit_0 a'). -Proof. - intros. rewrite <- true_xorb. rewrite <- H. rewrite ad_xor_bit_0. - rewrite xorb_assoc. rewrite xorb_nilpotent. rewrite xorb_false. reflexivity. -Qed. - -Lemma ad_neg_bit_0_1 : - forall a a':ad, ad_xor a a' = ad_x 1 -> ad_bit_0 a = negb (ad_bit_0 a'). -Proof. - intros. apply ad_neg_bit_0. rewrite H. reflexivity. -Qed. - -Lemma ad_neg_bit_0_2 : - forall (a a':ad) (p:positive), - ad_xor a a' = ad_x (xI p) -> ad_bit_0 a = negb (ad_bit_0 a'). -Proof. - intros. apply ad_neg_bit_0. rewrite H. reflexivity. -Qed. - -Lemma ad_same_bit_0 : - forall (a a':ad) (p:positive), - ad_xor a a' = ad_x (xO p) -> ad_bit_0 a = ad_bit_0 a'. -Proof. - intros. rewrite <- (xorb_false (ad_bit_0 a)). cut (ad_bit_0 (ad_x (xO p)) = false). - intro. rewrite <- H0. rewrite <- H. rewrite ad_xor_bit_0. rewrite <- xorb_assoc. - rewrite xorb_nilpotent. rewrite false_xorb. reflexivity. - reflexivity. -Qed.
\ No newline at end of file diff --git a/theories/IntMap/Adist.v b/theories/IntMap/Adist.v deleted file mode 100644 index 790218ce..00000000 --- a/theories/IntMap/Adist.v +++ /dev/null @@ -1,336 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(*i $Id: Adist.v 5920 2004-07-16 20:01:26Z herbelin $ i*) - -Require Import Bool. -Require Import ZArith. -Require Import Arith. -Require Import Min. -Require Import Addr. - -Fixpoint ad_plength_1 (p:positive) : nat := - match p with - | xH => 0 - | xI _ => 0 - | xO p' => S (ad_plength_1 p') - end. - -Inductive natinf : Set := - | infty : natinf - | ni : nat -> natinf. - -Definition ad_plength (a:ad) := - match a with - | ad_z => infty - | ad_x p => ni (ad_plength_1 p) - end. - -Lemma ad_plength_infty : forall a:ad, ad_plength a = infty -> a = ad_z. -Proof. - simple induction a; trivial. - unfold ad_plength in |- *; intros; discriminate H. -Qed. - -Lemma ad_plength_zeros : - forall (a:ad) (n:nat), - ad_plength a = ni n -> forall k:nat, k < n -> ad_bit a k = false. -Proof. - simple induction a; trivial. - simple induction p. simple induction n. intros. inversion H1. - simple induction k. simpl in H1. discriminate H1. - intros. simpl in H1. discriminate H1. - simple induction k. trivial. - generalize H0. case n. intros. inversion H3. - intros. simpl in |- *. unfold ad_bit in H. apply (H n0). simpl in H1. inversion H1. reflexivity. - exact (lt_S_n n1 n0 H3). - simpl in |- *. intros n H. inversion H. intros. inversion H0. -Qed. - -Lemma ad_plength_one : - forall (a:ad) (n:nat), ad_plength a = ni n -> ad_bit a n = true. -Proof. - simple induction a. intros. inversion H. - simple induction p. intros. simpl in H0. inversion H0. reflexivity. - intros. simpl in H0. inversion H0. simpl in |- *. unfold ad_bit in H. apply H. reflexivity. - intros. simpl in H. inversion H. reflexivity. -Qed. - -Lemma ad_plength_first_one : - forall (a:ad) (n:nat), - (forall k:nat, k < n -> ad_bit a k = false) -> - ad_bit a n = true -> ad_plength a = ni n. -Proof. - simple induction a. intros. simpl in H0. discriminate H0. - simple induction p. intros. generalize H0. case n. intros. reflexivity. - intros. absurd (ad_bit (ad_x (xI p0)) 0 = false). trivial with bool. - auto with bool arith. - intros. generalize H0 H1. case n. intros. simpl in H3. discriminate H3. - intros. simpl in |- *. unfold ad_plength in H. - cut (ni (ad_plength_1 p0) = ni n0). intro. inversion H4. reflexivity. - apply H. intros. change (ad_bit (ad_x (xO p0)) (S k) = false) in |- *. apply H2. apply lt_n_S. exact H4. - exact H3. - intro. case n. trivial. - intros. simpl in H0. discriminate H0. -Qed. - -Definition ni_min (d d':natinf) := - match d with - | infty => d' - | ni n => match d' with - | infty => d - | ni n' => ni (min n n') - end - end. - -Lemma ni_min_idemp : forall d:natinf, ni_min d d = d. -Proof. - simple induction d; trivial. - unfold ni_min in |- *. - simple induction n; trivial. - intros. - simpl in |- *. - inversion H. - rewrite H1. - rewrite H1. - reflexivity. -Qed. - -Lemma ni_min_comm : forall d d':natinf, ni_min d d' = ni_min d' d. -Proof. - simple induction d. simple induction d'; trivial. - simple induction d'; trivial. elim n. simple induction n0; trivial. - intros. elim n1; trivial. intros. unfold ni_min in H. cut (min n0 n2 = min n2 n0). - intro. unfold ni_min in |- *. simpl in |- *. rewrite H1. reflexivity. - cut (ni (min n0 n2) = ni (min n2 n0)). intros. - inversion H1; trivial. - exact (H n2). -Qed. - -Lemma ni_min_assoc : - forall d d' d'':natinf, ni_min (ni_min d d') d'' = ni_min d (ni_min d' d''). -Proof. - simple induction d; trivial. simple induction d'; trivial. - simple induction d''; trivial. - unfold ni_min in |- *. intro. cut (min (min n n0) n1 = min n (min n0 n1)). - intro. rewrite H. reflexivity. - generalize n0 n1. elim n; trivial. - simple induction n3; trivial. simple induction n5; trivial. - intros. simpl in |- *. auto. -Qed. - -Lemma ni_min_O_l : forall d:natinf, ni_min (ni 0) d = ni 0. -Proof. - simple induction d; trivial. -Qed. - -Lemma ni_min_O_r : forall d:natinf, ni_min d (ni 0) = ni 0. -Proof. - intros. rewrite ni_min_comm. apply ni_min_O_l. -Qed. - -Lemma ni_min_inf_l : forall d:natinf, ni_min infty d = d. -Proof. - trivial. -Qed. - -Lemma ni_min_inf_r : forall d:natinf, ni_min d infty = d. -Proof. - simple induction d; trivial. -Qed. - -Definition ni_le (d d':natinf) := ni_min d d' = d. - -Lemma ni_le_refl : forall d:natinf, ni_le d d. -Proof. - exact ni_min_idemp. -Qed. - -Lemma ni_le_antisym : forall d d':natinf, ni_le d d' -> ni_le d' d -> d = d'. -Proof. - unfold ni_le in |- *. intros d d'. rewrite ni_min_comm. intro H. rewrite H. trivial. -Qed. - -Lemma ni_le_trans : - forall d d' d'':natinf, ni_le d d' -> ni_le d' d'' -> ni_le d d''. -Proof. - unfold ni_le in |- *. intros. rewrite <- H. rewrite ni_min_assoc. rewrite H0. reflexivity. -Qed. - -Lemma ni_le_min_1 : forall d d':natinf, ni_le (ni_min d d') d. -Proof. - unfold ni_le in |- *. intros. rewrite (ni_min_comm d d'). rewrite ni_min_assoc. - rewrite ni_min_idemp. reflexivity. -Qed. - -Lemma ni_le_min_2 : forall d d':natinf, ni_le (ni_min d d') d'. -Proof. - unfold ni_le in |- *. intros. rewrite ni_min_assoc. rewrite ni_min_idemp. reflexivity. -Qed. - -Lemma ni_min_case : forall d d':natinf, ni_min d d' = d \/ ni_min d d' = d'. -Proof. - simple induction d. intro. right. exact (ni_min_inf_l d'). - simple induction d'. left. exact (ni_min_inf_r (ni n)). - unfold ni_min in |- *. cut (forall n0:nat, min n n0 = n \/ min n n0 = n0). - intros. case (H n0). intro. left. rewrite H0. reflexivity. - intro. right. rewrite H0. reflexivity. - elim n. intro. left. reflexivity. - simple induction n1. right. reflexivity. - intros. case (H n2). intro. left. simpl in |- *. rewrite H1. reflexivity. - intro. right. simpl in |- *. rewrite H1. reflexivity. -Qed. - -Lemma ni_le_total : forall d d':natinf, ni_le d d' \/ ni_le d' d. -Proof. - unfold ni_le in |- *. intros. rewrite (ni_min_comm d' d). apply ni_min_case. -Qed. - -Lemma ni_le_min_induc : - forall d d' dm:natinf, - ni_le dm d -> - ni_le dm d' -> - (forall d'':natinf, ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm) -> - ni_min d d' = dm. -Proof. - intros. case (ni_min_case d d'). intro. rewrite H2. - apply ni_le_antisym. apply H1. apply ni_le_refl. - exact H2. - exact H. - intro. rewrite H2. apply ni_le_antisym. apply H1. unfold ni_le in |- *. rewrite ni_min_comm. exact H2. - apply ni_le_refl. - exact H0. -Qed. - -Lemma le_ni_le : forall m n:nat, m <= n -> ni_le (ni m) (ni n). -Proof. - cut (forall m n:nat, m <= n -> min m n = m). - intros. unfold ni_le, ni_min in |- *. rewrite (H m n H0). reflexivity. - simple induction m. trivial. - simple induction n0. intro. inversion H0. - intros. simpl in |- *. rewrite (H n1 (le_S_n n n1 H1)). reflexivity. -Qed. - -Lemma ni_le_le : forall m n:nat, ni_le (ni m) (ni n) -> m <= n. -Proof. - unfold ni_le in |- *. unfold ni_min in |- *. intros. inversion H. apply le_min_r. -Qed. - -Lemma ad_plength_lb : - forall (a:ad) (n:nat), - (forall k:nat, k < n -> ad_bit a k = false) -> ni_le (ni n) (ad_plength a). -Proof. - simple induction a. intros. exact (ni_min_inf_r (ni n)). - intros. unfold ad_plength in |- *. apply le_ni_le. case (le_or_lt n (ad_plength_1 p)). trivial. - intro. absurd (ad_bit (ad_x p) (ad_plength_1 p) = false). - rewrite - (ad_plength_one (ad_x p) (ad_plength_1 p) - (refl_equal (ad_plength (ad_x p)))). - discriminate. - apply H. exact H0. -Qed. - -Lemma ad_plength_ub : - forall (a:ad) (n:nat), ad_bit a n = true -> ni_le (ad_plength a) (ni n). -Proof. - simple induction a. intros. discriminate H. - intros. unfold ad_plength in |- *. apply le_ni_le. case (le_or_lt (ad_plength_1 p) n). trivial. - intro. absurd (ad_bit (ad_x p) n = true). - rewrite - (ad_plength_zeros (ad_x p) (ad_plength_1 p) - (refl_equal (ad_plength (ad_x p))) n H0). - discriminate. - exact H. -Qed. - - -(** We define an ultrametric distance between addresses: - $d(a,a')=1/2^pd(a,a')$, - where $pd(a,a')$ is the number of identical bits at the beginning - of $a$ and $a'$ (infinity if $a=a'$). - Instead of working with $d$, we work with $pd$, namely - [ad_pdist]: *) - -Definition ad_pdist (a a':ad) := ad_plength (ad_xor a a'). - -(** d is a distance, so $d(a,a')=0$ iff $a=a'$; this means that - $pd(a,a')=infty$ iff $a=a'$: *) - -Lemma ad_pdist_eq_1 : forall a:ad, ad_pdist a a = infty. -Proof. - intros. unfold ad_pdist in |- *. rewrite ad_xor_nilpotent. reflexivity. -Qed. - -Lemma ad_pdist_eq_2 : forall a a':ad, ad_pdist a a' = infty -> a = a'. -Proof. - intros. apply ad_xor_eq. apply ad_plength_infty. exact H. -Qed. - -(** $d$ is a distance, so $d(a,a')=d(a',a)$: *) - -Lemma ad_pdist_comm : forall a a':ad, ad_pdist a a' = ad_pdist a' a. -Proof. - unfold ad_pdist in |- *. intros. rewrite ad_xor_comm. reflexivity. -Qed. - -(** $d$ is an ultrametric distance, that is, not only $d(a,a')\leq - d(a,a'')+d(a'',a')$, - but in fact $d(a,a')\leq max(d(a,a''),d(a'',a'))$. - This means that $min(pd(a,a''),pd(a'',a'))<=pd(a,a')$ (lemma [ad_pdist_ultra] below). - This follows from the fact that $a ~Ra~|a| = 1/2^{\texttt{ad\_plength}}(a))$ - is an ultrametric norm, i.e. that $|a-a'| \leq max (|a-a''|, |a''-a'|)$, - or equivalently that $|a+b|<=max(|a|,|b|)$, i.e. that - min $(\texttt{ad\_plength}(a), \texttt{ad\_plength}(b)) \leq - \texttt{ad\_plength} (a~\texttt{xor}~ b)$ - (lemma [ad_plength_ultra]). -*) - -Lemma ad_plength_ultra_1 : - forall a a':ad, - ni_le (ad_plength a) (ad_plength a') -> - ni_le (ad_plength a) (ad_plength (ad_xor a a')). -Proof. - simple induction a. intros. unfold ni_le in H. unfold ad_plength at 1 3 in H. - rewrite (ni_min_inf_l (ad_plength a')) in H. - rewrite (ad_plength_infty a' H). simpl in |- *. apply ni_le_refl. - intros. unfold ad_plength at 1 in |- *. apply ad_plength_lb. intros. - cut (forall a'':ad, ad_xor (ad_x p) a' = a'' -> ad_bit a'' k = false). - intros. apply H1. reflexivity. - intro a''. case a''. intro. reflexivity. - intros. rewrite <- H1. rewrite (ad_xor_semantics (ad_x p) a' k). unfold adf_xor in |- *. - rewrite - (ad_plength_zeros (ad_x p) (ad_plength_1 p) - (refl_equal (ad_plength (ad_x p))) k H0). - generalize H. case a'. trivial. - intros. cut (ad_bit (ad_x p1) k = false). intros. rewrite H3. reflexivity. - apply ad_plength_zeros with (n := ad_plength_1 p1). reflexivity. - apply (lt_le_trans k (ad_plength_1 p) (ad_plength_1 p1)). exact H0. - apply ni_le_le. exact H2. -Qed. - -Lemma ad_plength_ultra : - forall a a':ad, - ni_le (ni_min (ad_plength a) (ad_plength a')) (ad_plength (ad_xor a a')). -Proof. - intros. case (ni_le_total (ad_plength a) (ad_plength a')). intro. - cut (ni_min (ad_plength a) (ad_plength a') = ad_plength a). - intro. rewrite H0. apply ad_plength_ultra_1. exact H. - exact H. - intro. cut (ni_min (ad_plength a) (ad_plength a') = ad_plength a'). - intro. rewrite H0. rewrite ad_xor_comm. apply ad_plength_ultra_1. exact H. - rewrite ni_min_comm. exact H. -Qed. - -Lemma ad_pdist_ultra : - forall a a' a'':ad, - ni_le (ni_min (ad_pdist a a'') (ad_pdist a'' a')) (ad_pdist a a'). -Proof. - intros. unfold ad_pdist in |- *. cut (ad_xor (ad_xor a a'') (ad_xor a'' a') = ad_xor a a'). - intro. rewrite <- H. apply ad_plength_ultra. - rewrite ad_xor_assoc. rewrite <- (ad_xor_assoc a'' a'' a'). rewrite ad_xor_nilpotent. - rewrite ad_xor_neutral_left. reflexivity. -Qed.
\ No newline at end of file diff --git a/theories/IntMap/Allmaps.v b/theories/IntMap/Allmaps.v index f9a0feac..d5af8f80 100644 --- a/theories/IntMap/Allmaps.v +++ b/theories/IntMap/Allmaps.v @@ -5,17 +5,12 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Allmaps.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Allmaps.v 8733 2006-04-25 22:52:18Z letouzey $ i*) -Require Export Addr. -Require Export Adist. -Require Export Addec. Require Export Map. - Require Export Fset. Require Export Mapaxioms. Require Export Mapiter. - Require Export Mapsubset. Require Export Lsort. Require Export Mapfold. diff --git a/theories/IntMap/Fset.v b/theories/IntMap/Fset.v index 27f739c1..5b46c969 100644 --- a/theories/IntMap/Fset.v +++ b/theories/IntMap/Fset.v @@ -5,16 +5,15 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Fset.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Fset.v 8733 2006-04-25 22:52:18Z letouzey $ i*) (*s Sets operations on maps *) Require Import Bool. Require Import Sumbool. -Require Import ZArith. -Require Import Addr. -Require Import Adist. -Require Import Addec. +Require Import NArith. +Require Import Ndigits. +Require Import Ndec. Require Import Map. Section Dom. @@ -26,7 +25,7 @@ Section Dom. | M0 => fun _:Map B => M0 A | M1 a y => fun m':Map B => match MapGet B m' a with - | NONE => M0 A + | None => M0 A | _ => m end | M2 m1 m2 => @@ -35,8 +34,8 @@ Section Dom. | M0 => M0 A | M1 a' y' => match MapGet A m a' with - | NONE => M0 A - | SOME y => M1 A a' y + | None => M0 A + | Some y => M1 A a' y end | M2 m'1 m'2 => makeM2 A (MapDomRestrTo m1 m'1) (MapDomRestrTo m2 m'2) @@ -48,35 +47,35 @@ Section Dom. eqm A (MapGet A (MapDomRestrTo m m')) (fun a0:ad => match MapGet B m' a0 with - | NONE => NONE A + | None => None | _ => MapGet A m a0 end). Proof. unfold eqm in |- *. simple induction m. simpl in |- *. intros. case (MapGet B m' a); trivial. - intros. simpl in |- *. elim (sumbool_of_bool (ad_eq a a1)). intro H. rewrite H. - rewrite <- (ad_eq_complete _ _ H). case (MapGet B m' a). reflexivity. + intros. simpl in |- *. elim (sumbool_of_bool (Neqb a a1)). intro H. rewrite H. + rewrite <- (Neqb_complete _ _ H). case (MapGet B m' a); try reflexivity. intro. apply M1_semantics_1. intro H. rewrite H. case (MapGet B m' a). - case (MapGet B m' a1); reflexivity. case (MapGet B m' a1); intros; exact (M1_semantics_2 A a a1 a0 H). + case (MapGet B m' a1); reflexivity. simple induction m'. trivial. - unfold MapDomRestrTo in |- *. intros. elim (sumbool_of_bool (ad_eq a a1)). + unfold MapDomRestrTo in |- *. intros. elim (sumbool_of_bool (Neqb a a1)). intro H1. - rewrite (ad_eq_complete _ _ H1). rewrite (M1_semantics_1 B a1 a0). - case (MapGet A (M2 A m0 m1) a1). reflexivity. + rewrite (Neqb_complete _ _ H1). rewrite (M1_semantics_1 B a1 a0). + case (MapGet A (M2 A m0 m1) a1); try reflexivity. intro. apply M1_semantics_1. - intro H1. rewrite (M1_semantics_2 B a a1 a0 H1). case (MapGet A (M2 A m0 m1) a). reflexivity. + intro H1. rewrite (M1_semantics_2 B a a1 a0 H1). case (MapGet A (M2 A m0 m1) a); try reflexivity. intro. exact (M1_semantics_2 A a a1 a2 H1). intros. change (MapGet A (makeM2 A (MapDomRestrTo m0 m2) (MapDomRestrTo m1 m3)) a = match MapGet B (M2 B m2 m3) a with - | NONE => NONE A - | SOME _ => MapGet A (M2 A m0 m1) a + | None => None + | Some _ => MapGet A (M2 A m0 m1) a end) in |- *. rewrite (makeM2_M2 A (MapDomRestrTo m0 m2) (MapDomRestrTo m1 m3) a). - rewrite MapGet_M2_bit_0_if. rewrite (H0 m3 (ad_div_2 a)). rewrite (H m2 (ad_div_2 a)). + rewrite MapGet_M2_bit_0_if. rewrite (H0 m3 (Ndiv2 a)). rewrite (H m2 (Ndiv2 a)). rewrite (MapGet_M2_bit_0_if B m2 m3 a). rewrite (MapGet_M2_bit_0_if A m0 m1 a). - case (ad_bit_0 a); reflexivity. + case (Nbit0 a); reflexivity. Qed. Fixpoint MapDomRestrBy (m:Map A) : Map B -> Map A := @@ -84,7 +83,7 @@ Section Dom. | M0 => fun _:Map B => M0 A | M1 a y => fun m':Map B => match MapGet B m' a with - | NONE => m + | None => m | _ => M0 A end | M2 m1 m2 => @@ -102,37 +101,38 @@ Section Dom. eqm A (MapGet A (MapDomRestrBy m m')) (fun a0:ad => match MapGet B m' a0 with - | NONE => MapGet A m a0 - | _ => NONE A + | None => MapGet A m a0 + | _ => None end). Proof. unfold eqm in |- *. simple induction m. simpl in |- *. intros. case (MapGet B m' a); trivial. - intros. simpl in |- *. elim (sumbool_of_bool (ad_eq a a1)). intro H. rewrite H. - rewrite (ad_eq_complete _ _ H). case (MapGet B m' a1). apply M1_semantics_1. - trivial. - intro H. rewrite H. case (MapGet B m' a). rewrite (M1_semantics_2 A a a1 a0 H). + intros. simpl in |- *. elim (sumbool_of_bool (Neqb a a1)). intro H. rewrite H. + rewrite (Neqb_complete _ _ H). case (MapGet B m' a1). trivial. + apply M1_semantics_1. + intro H. rewrite H. case (MapGet B m' a). case (MapGet B m' a1); trivial. + rewrite (M1_semantics_2 A a a1 a0 H). case (MapGet B m' a1); trivial. simple induction m'. trivial. unfold MapDomRestrBy in |- *. intros. rewrite (MapRemove_semantics A (M2 A m0 m1) a a1). - elim (sumbool_of_bool (ad_eq a a1)). intro H1. rewrite H1. rewrite (ad_eq_complete _ _ H1). + elim (sumbool_of_bool (Neqb a a1)). intro H1. rewrite H1. rewrite (Neqb_complete _ _ H1). rewrite (M1_semantics_1 B a1 a0). reflexivity. intro H1. rewrite H1. rewrite (M1_semantics_2 B a a1 a0 H1). reflexivity. intros. change (MapGet A (makeM2 A (MapDomRestrBy m0 m2) (MapDomRestrBy m1 m3)) a = match MapGet B (M2 B m2 m3) a with - | NONE => MapGet A (M2 A m0 m1) a - | SOME _ => NONE A + | None => MapGet A (M2 A m0 m1) a + | Some _ => None end) in |- *. rewrite (makeM2_M2 A (MapDomRestrBy m0 m2) (MapDomRestrBy m1 m3) a). - rewrite MapGet_M2_bit_0_if. rewrite (H0 m3 (ad_div_2 a)). rewrite (H m2 (ad_div_2 a)). + rewrite MapGet_M2_bit_0_if. rewrite (H0 m3 (Ndiv2 a)). rewrite (H m2 (Ndiv2 a)). rewrite (MapGet_M2_bit_0_if B m2 m3 a). rewrite (MapGet_M2_bit_0_if A m0 m1 a). - case (ad_bit_0 a); reflexivity. + case (Nbit0 a); reflexivity. Qed. Definition in_dom (a:ad) (m:Map A) := match MapGet A m a with - | NONE => false + | None => false | _ => true end. @@ -141,32 +141,32 @@ Section Dom. trivial. Qed. - Lemma in_dom_M1 : forall (a a0:ad) (y:A), in_dom a0 (M1 A a y) = ad_eq a a0. + Lemma in_dom_M1 : forall (a a0:ad) (y:A), in_dom a0 (M1 A a y) = Neqb a a0. Proof. - unfold in_dom in |- *. intros. simpl in |- *. case (ad_eq a a0); reflexivity. + unfold in_dom in |- *. intros. simpl in |- *. case (Neqb a a0); reflexivity. Qed. Lemma in_dom_M1_1 : forall (a:ad) (y:A), in_dom a (M1 A a y) = true. Proof. - intros. rewrite in_dom_M1. apply ad_eq_correct. + intros. rewrite in_dom_M1. apply Neqb_correct. Qed. Lemma in_dom_M1_2 : forall (a a0:ad) (y:A), in_dom a0 (M1 A a y) = true -> a = a0. Proof. - intros. apply (ad_eq_complete a a0). rewrite (in_dom_M1 a a0 y) in H. assumption. + intros. apply (Neqb_complete a a0). rewrite (in_dom_M1 a a0 y) in H. assumption. Qed. Lemma in_dom_some : forall (m:Map A) (a:ad), - in_dom a m = true -> {y : A | MapGet A m a = SOME A y}. + in_dom a m = true -> {y : A | MapGet A m a = Some y}. Proof. unfold in_dom in |- *. intros. elim (option_sum _ (MapGet A m a)). trivial. intro H0. rewrite H0 in H. discriminate H. Qed. Lemma in_dom_none : - forall (m:Map A) (a:ad), in_dom a m = false -> MapGet A m a = NONE A. + forall (m:Map A) (a:ad), in_dom a m = false -> MapGet A m a = None. Proof. unfold in_dom in |- *. intros. elim (option_sum _ (MapGet A m a)). intro H0. elim H0. intros y H1. rewrite H1 in H. discriminate H. @@ -175,33 +175,33 @@ Section Dom. Lemma in_dom_put : forall (m:Map A) (a0:ad) (y0:A) (a:ad), - in_dom a (MapPut A m a0 y0) = orb (ad_eq a a0) (in_dom a m). + in_dom a (MapPut A m a0 y0) = orb (Neqb a a0) (in_dom a m). Proof. unfold in_dom in |- *. intros. rewrite (MapPut_semantics A m a0 y0 a). - elim (sumbool_of_bool (ad_eq a a0)). intro H. rewrite H. rewrite (ad_eq_comm a a0) in H. + elim (sumbool_of_bool (Neqb a a0)). intro H. rewrite H. rewrite (Neqb_comm a a0) in H. rewrite H. rewrite orb_true_b. reflexivity. - intro H. rewrite H. rewrite (ad_eq_comm a a0) in H. rewrite H. rewrite orb_false_b. + intro H. rewrite H. rewrite (Neqb_comm a a0) in H. rewrite H. rewrite orb_false_b. reflexivity. Qed. Lemma in_dom_put_behind : forall (m:Map A) (a0:ad) (y0:A) (a:ad), - in_dom a (MapPut_behind A m a0 y0) = orb (ad_eq a a0) (in_dom a m). + in_dom a (MapPut_behind A m a0 y0) = orb (Neqb a a0) (in_dom a m). Proof. unfold in_dom in |- *. intros. rewrite (MapPut_behind_semantics A m a0 y0 a). - elim (sumbool_of_bool (ad_eq a a0)). intro H. rewrite H. rewrite (ad_eq_comm a a0) in H. + elim (sumbool_of_bool (Neqb a a0)). intro H. rewrite H. rewrite (Neqb_comm a a0) in H. rewrite H. case (MapGet A m a); reflexivity. - intro H. rewrite H. rewrite (ad_eq_comm a a0) in H. rewrite H. case (MapGet A m a); trivial. + intro H. rewrite H. rewrite (Neqb_comm a a0) in H. rewrite H. case (MapGet A m a); trivial. Qed. Lemma in_dom_remove : forall (m:Map A) (a0 a:ad), - in_dom a (MapRemove A m a0) = andb (negb (ad_eq a a0)) (in_dom a m). + in_dom a (MapRemove A m a0) = andb (negb (Neqb a a0)) (in_dom a m). Proof. unfold in_dom in |- *. intros. rewrite (MapRemove_semantics A m a0 a). - elim (sumbool_of_bool (ad_eq a a0)). intro H. rewrite H. rewrite (ad_eq_comm a a0) in H. + elim (sumbool_of_bool (Neqb a a0)). intro H. rewrite H. rewrite (Neqb_comm a a0) in H. rewrite H. reflexivity. - intro H. rewrite H. rewrite (ad_eq_comm a a0) in H. rewrite H. + intro H. rewrite H. rewrite (Neqb_comm a a0) in H. rewrite H. case (MapGet A m a); reflexivity. Qed. @@ -272,35 +272,35 @@ Section FSetDefs. Lemma MapDom_semantics_1 : forall (m:Map A) (a:ad) (y:A), - MapGet A m a = SOME A y -> in_FSet a (MapDom m) = true. + MapGet A m a = Some y -> in_FSet a (MapDom m) = true. Proof. simple induction m. intros. discriminate H. unfold MapDom in |- *. unfold in_FSet in |- *. unfold in_dom in |- *. unfold MapGet in |- *. intros a y a0 y0. - case (ad_eq a a0). trivial. + case (Neqb a a0). trivial. intro. discriminate H. intros m0 H m1 H0 a y. rewrite (MapGet_M2_bit_0_if A m0 m1 a). simpl in |- *. unfold in_FSet in |- *. unfold in_dom in |- *. rewrite (MapGet_M2_bit_0_if unit (MapDom m0) (MapDom m1) a). - case (ad_bit_0 a). unfold in_FSet, in_dom in H0. intro. apply H0 with (y := y). assumption. + case (Nbit0 a). unfold in_FSet, in_dom in H0. intro. apply H0 with (y := y). assumption. unfold in_FSet, in_dom in H. intro. apply H with (y := y). assumption. Qed. Lemma MapDom_semantics_2 : forall (m:Map A) (a:ad), - in_FSet a (MapDom m) = true -> {y : A | MapGet A m a = SOME A y}. + in_FSet a (MapDom m) = true -> {y : A | MapGet A m a = Some y}. Proof. simple induction m. intros. discriminate H. - unfold MapDom in |- *. unfold in_FSet in |- *. unfold in_dom in |- *. unfold MapGet in |- *. intros a y a0. case (ad_eq a a0). + unfold MapDom in |- *. unfold in_FSet in |- *. unfold in_dom in |- *. unfold MapGet in |- *. intros a y a0. case (Neqb a a0). intro. split with y. reflexivity. intro. discriminate H. intros m0 H m1 H0 a. rewrite (MapGet_M2_bit_0_if A m0 m1 a). simpl in |- *. unfold in_FSet in |- *. unfold in_dom in |- *. rewrite (MapGet_M2_bit_0_if unit (MapDom m0) (MapDom m1) a). - case (ad_bit_0 a). unfold in_FSet, in_dom in H0. intro. apply H0. assumption. + case (Nbit0 a). unfold in_FSet, in_dom in H0. intro. apply H0. assumption. unfold in_FSet, in_dom in H. intro. apply H. assumption. Qed. Lemma MapDom_semantics_3 : forall (m:Map A) (a:ad), - MapGet A m a = NONE A -> in_FSet a (MapDom m) = false. + MapGet A m a = None -> in_FSet a (MapDom m) = false. Proof. intros. elim (sumbool_of_bool (in_FSet a (MapDom m))). intro H0. elim (MapDom_semantics_2 m a H0). intros y H1. rewrite H in H1. discriminate H1. @@ -309,7 +309,7 @@ Section FSetDefs. Lemma MapDom_semantics_4 : forall (m:Map A) (a:ad), - in_FSet a (MapDom m) = false -> MapGet A m a = NONE A. + in_FSet a (MapDom m) = false -> MapGet A m a = None. Proof. intros. elim (option_sum A (MapGet A m a)). intro H0. elim H0. intros y H1. rewrite (MapDom_semantics_1 m a y H1) in H. discriminate H. diff --git a/theories/IntMap/Lsort.v b/theories/IntMap/Lsort.v index d31d8133..c8d793a1 100644 --- a/theories/IntMap/Lsort.v +++ b/theories/IntMap/Lsort.v @@ -5,15 +5,14 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Lsort.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Lsort.v 8733 2006-04-25 22:52:18Z letouzey $ i*) Require Import Bool. Require Import Sumbool. Require Import Arith. -Require Import ZArith. -Require Import Addr. -Require Import Adist. -Require Import Addec. +Require Import NArith. +Require Import Ndigits. +Require Import Ndec. Require Import Map. Require Import List. Require Import Mapiter. @@ -22,199 +21,19 @@ Section LSort. Variable A : Set. - Fixpoint ad_less_1 (a a':ad) (p:positive) {struct p} : bool := - match p with - | xO p' => ad_less_1 (ad_div_2 a) (ad_div_2 a') p' - | _ => andb (negb (ad_bit_0 a)) (ad_bit_0 a') - end. - - Definition ad_less (a a':ad) := - match ad_xor a a' with - | ad_z => false - | ad_x p => ad_less_1 a a' p - end. - - Lemma ad_bit_0_less : - forall a a':ad, - ad_bit_0 a = false -> ad_bit_0 a' = true -> ad_less a a' = true. - Proof. - intros. elim (ad_sum (ad_xor a a')). intro H1. elim H1. intros p H2. unfold ad_less in |- *. - rewrite H2. generalize H2. elim p. intros. simpl in |- *. rewrite H. rewrite H0. reflexivity. - intros. cut (ad_bit_0 (ad_xor a a') = false). intro. rewrite (ad_xor_bit_0 a a') in H5. - rewrite H in H5. rewrite H0 in H5. discriminate H5. - rewrite H4. reflexivity. - intro. simpl in |- *. rewrite H. rewrite H0. reflexivity. - intro H1. cut (ad_bit_0 (ad_xor a a') = false). intro. rewrite (ad_xor_bit_0 a a') in H2. - rewrite H in H2. rewrite H0 in H2. discriminate H2. - rewrite H1. reflexivity. - Qed. - - Lemma ad_bit_0_gt : - forall a a':ad, - ad_bit_0 a = true -> ad_bit_0 a' = false -> ad_less a a' = false. - Proof. - intros. elim (ad_sum (ad_xor a a')). intro H1. elim H1. intros p H2. unfold ad_less in |- *. - rewrite H2. generalize H2. elim p. intros. simpl in |- *. rewrite H. rewrite H0. reflexivity. - intros. cut (ad_bit_0 (ad_xor a a') = false). intro. rewrite (ad_xor_bit_0 a a') in H5. - rewrite H in H5. rewrite H0 in H5. discriminate H5. - rewrite H4. reflexivity. - intro. simpl in |- *. rewrite H. rewrite H0. reflexivity. - intro H1. unfold ad_less in |- *. rewrite H1. reflexivity. - Qed. - - Lemma ad_less_not_refl : forall a:ad, ad_less a a = false. - Proof. - intro. unfold ad_less in |- *. rewrite (ad_xor_nilpotent a). reflexivity. - Qed. - - Lemma ad_ind_double : - forall (a:ad) (P:ad -> Prop), - P ad_z -> - (forall a:ad, P a -> P (ad_double a)) -> - (forall a:ad, P a -> P (ad_double_plus_un a)) -> P a. - Proof. - intros; elim a. trivial. - simple induction p. intros. - apply (H1 (ad_x p0)); trivial. - intros; apply (H0 (ad_x p0)); trivial. - intros; apply (H1 ad_z); assumption. - Qed. - - Lemma ad_rec_double : - forall (a:ad) (P:ad -> Set), - P ad_z -> - (forall a:ad, P a -> P (ad_double a)) -> - (forall a:ad, P a -> P (ad_double_plus_un a)) -> P a. - Proof. - intros; elim a. trivial. - simple induction p. intros. - apply (H1 (ad_x p0)); trivial. - intros; apply (H0 (ad_x p0)); trivial. - intros; apply (H1 ad_z); assumption. - Qed. - - Lemma ad_less_def_1 : - forall a a':ad, ad_less (ad_double a) (ad_double a') = ad_less a a'. - Proof. - simple induction a. simple induction a'. reflexivity. - trivial. - simple induction a'. unfold ad_less in |- *. simpl in |- *. elim p; trivial. - unfold ad_less in |- *. simpl in |- *. intro. case (p_xor p p0). reflexivity. - trivial. - Qed. - - Lemma ad_less_def_2 : - forall a a':ad, - ad_less (ad_double_plus_un a) (ad_double_plus_un a') = ad_less a a'. - Proof. - simple induction a. simple induction a'. reflexivity. - trivial. - simple induction a'. unfold ad_less in |- *. simpl in |- *. elim p; trivial. - unfold ad_less in |- *. simpl in |- *. intro. case (p_xor p p0). reflexivity. - trivial. - Qed. - - Lemma ad_less_def_3 : - forall a a':ad, ad_less (ad_double a) (ad_double_plus_un a') = true. - Proof. - intros. apply ad_bit_0_less. apply ad_double_bit_0. - apply ad_double_plus_un_bit_0. - Qed. - - Lemma ad_less_def_4 : - forall a a':ad, ad_less (ad_double_plus_un a) (ad_double a') = false. - Proof. - intros. apply ad_bit_0_gt. apply ad_double_plus_un_bit_0. - apply ad_double_bit_0. - Qed. - - Lemma ad_less_z : forall a:ad, ad_less a ad_z = false. - Proof. - simple induction a. reflexivity. - unfold ad_less in |- *. intro. rewrite (ad_xor_neutral_right (ad_x p)). elim p; trivial. - Qed. - - Lemma ad_z_less_1 : - forall a:ad, ad_less ad_z a = true -> {p : positive | a = ad_x p}. - Proof. - simple induction a. intro. discriminate H. - intros. split with p. reflexivity. - Qed. - - Lemma ad_z_less_2 : forall a:ad, ad_less ad_z a = false -> a = ad_z. - Proof. - simple induction a. trivial. - unfold ad_less in |- *. simpl in |- *. cut (forall p:positive, ad_less_1 ad_z (ad_x p) p = false -> False). - intros. elim (H p H0). - simple induction p. intros. discriminate H0. - intros. exact (H H0). - intro. discriminate H. - Qed. - - Lemma ad_less_trans : - forall a a' a'':ad, - ad_less a a' = true -> ad_less a' a'' = true -> ad_less a a'' = true. - Proof. - intro a. apply ad_ind_double with - (P := fun a:ad => - forall a' a'':ad, - ad_less a a' = true -> - ad_less a' a'' = true -> ad_less a a'' = true). - intros. elim (sumbool_of_bool (ad_less ad_z a'')). trivial. - intro H1. rewrite (ad_z_less_2 a'' H1) in H0. rewrite (ad_less_z a') in H0. discriminate H0. - intros a0 H a'. apply ad_ind_double with - (P := fun a':ad => - forall a'':ad, - ad_less (ad_double a0) a' = true -> - ad_less a' a'' = true -> ad_less (ad_double a0) a'' = true). - intros. rewrite (ad_less_z (ad_double a0)) in H0. discriminate H0. - intros a1 H0 a'' H1. rewrite (ad_less_def_1 a0 a1) in H1. - apply ad_ind_double with - (P := fun a'':ad => - ad_less (ad_double a1) a'' = true -> - ad_less (ad_double a0) a'' = true). - intro. rewrite (ad_less_z (ad_double a1)) in H2. discriminate H2. - intros. rewrite (ad_less_def_1 a1 a2) in H3. rewrite (ad_less_def_1 a0 a2). - exact (H a1 a2 H1 H3). - intros. apply ad_less_def_3. - intros a1 H0 a'' H1. apply ad_ind_double with - (P := fun a'':ad => - ad_less (ad_double_plus_un a1) a'' = true -> - ad_less (ad_double a0) a'' = true). - intro. rewrite (ad_less_z (ad_double_plus_un a1)) in H2. discriminate H2. - intros. rewrite (ad_less_def_4 a1 a2) in H3. discriminate H3. - intros. apply ad_less_def_3. - intros a0 H a'. apply ad_ind_double with - (P := fun a':ad => - forall a'':ad, - ad_less (ad_double_plus_un a0) a' = true -> - ad_less a' a'' = true -> - ad_less (ad_double_plus_un a0) a'' = true). - intros. rewrite (ad_less_z (ad_double_plus_un a0)) in H0. discriminate H0. - intros. rewrite (ad_less_def_4 a0 a1) in H1. discriminate H1. - intros a1 H0 a'' H1. apply ad_ind_double with - (P := fun a'':ad => - ad_less (ad_double_plus_un a1) a'' = true -> - ad_less (ad_double_plus_un a0) a'' = true). - intro. rewrite (ad_less_z (ad_double_plus_un a1)) in H2. discriminate H2. - intros. rewrite (ad_less_def_4 a1 a2) in H3. discriminate H3. - rewrite (ad_less_def_2 a0 a1) in H1. intros. rewrite (ad_less_def_2 a1 a2) in H3. - rewrite (ad_less_def_2 a0 a2). exact (H a1 a2 H1 H3). - Qed. - Fixpoint alist_sorted (l:alist A) : bool := match l with | nil => true | (a, _) :: l' => match l' with | nil => true - | (a', y') :: l'' => andb (ad_less a a') (alist_sorted l') + | (a', y') :: l'' => andb (Nless a a') (alist_sorted l') end end. Fixpoint alist_nth_ad (n:nat) (l:alist A) {struct l} : ad := match l with - | nil => ad_z (* dummy *) + | nil => N0 (* dummy *) | (a, y) :: l' => match n with | O => a | S n' => alist_nth_ad n' l' @@ -224,7 +43,7 @@ Section LSort. Definition alist_sorted_1 (l:alist A) := forall n:nat, S (S n) <= length l -> - ad_less (alist_nth_ad n l) (alist_nth_ad (S n) l) = true. + Nless (alist_nth_ad n l) (alist_nth_ad (S n) l) = true. Lemma alist_sorted_imp_1 : forall l:alist A, alist_sorted l = true -> alist_sorted_1 l. @@ -235,7 +54,7 @@ Section LSort. intro r0. elim r0. intros a0 y0. simple induction n. intros. simpl in |- *. simpl in H1. exact (proj1 (andb_prop _ _ H1)). intros. change - (ad_less (alist_nth_ad n0 ((a0, y0) :: l1)) + (Nless (alist_nth_ad n0 ((a0, y0) :: l1)) (alist_nth_ad (S n0) ((a0, y0) :: l1)) = true) in |- *. apply H0. exact (proj2 (andb_prop _ _ H1)). @@ -245,13 +64,13 @@ Section LSort. Definition alist_sorted_2 (l:alist A) := forall m n:nat, m < n -> - S n <= length l -> ad_less (alist_nth_ad m l) (alist_nth_ad n l) = true. + S n <= length l -> Nless (alist_nth_ad m l) (alist_nth_ad n l) = true. Lemma alist_sorted_1_imp_2 : forall l:alist A, alist_sorted_1 l -> alist_sorted_2 l. Proof. unfold alist_sorted_1, alist_sorted_2, lt in |- *. intros l H m n H0. elim H0. exact (H m). - intros. apply ad_less_trans with (a' := alist_nth_ad m0 l). apply H2. apply le_Sn_le. + intros. apply Nless_trans with (a' := alist_nth_ad m0 l). apply H2. apply le_Sn_le. assumption. apply H. assumption. Qed. @@ -262,7 +81,7 @@ Section LSort. unfold alist_sorted_2, lt in |- *. simple induction l. trivial. intro r. elim r. intros a y. simple induction l0. trivial. intro r0. elim r0. intros a0 y0. intros. - change (andb (ad_less a a0) (alist_sorted ((a0, y0) :: l1)) = true) + change (andb (Nless a a0) (alist_sorted ((a0, y0) :: l1)) = true) in |- *. apply andb_true_intro. split. apply (H1 0 1). apply le_n. simpl in |- *. apply le_n_S. apply le_n_S. apply le_O_n. @@ -319,7 +138,7 @@ Section LSort. (forall n n':nat, S n <= length l -> S n' <= length l' -> - ad_less (alist_nth_ad n l) (alist_nth_ad n' l') = true) -> + Nless (alist_nth_ad n l) (alist_nth_ad n' l') = true) -> alist_sorted_2 (aapp A l l'). Proof. unfold alist_sorted_2, lt in |- *. intros. rewrite (aapp_length l l') in H3. @@ -348,14 +167,14 @@ Section LSort. Lemma alist_nth_ad_semantics : forall (l:alist A) (n:nat), S n <= length l -> - {y : A | alist_semantics A l (alist_nth_ad n l) = SOME A y}. + {y : A | alist_semantics A l (alist_nth_ad n l) = Some y}. Proof. simple induction l. intros. elim (le_Sn_O _ H). intro r. elim r. intros a y l0 H. simple induction n. simpl in |- *. intro. split with y. - rewrite (ad_eq_correct a). reflexivity. + rewrite (Neqb_correct a). reflexivity. intros. elim (H _ (le_S_n _ _ H1)). intros y0 H2. - elim (sumbool_of_bool (ad_eq a (alist_nth_ad n0 l0))). intro H3. split with y. - rewrite (ad_eq_complete _ _ H3). simpl in |- *. rewrite (ad_eq_correct (alist_nth_ad n0 l0)). + elim (sumbool_of_bool (Neqb a (alist_nth_ad n0 l0))). intro H3. split with y. + rewrite (Neqb_complete _ _ H3). simpl in |- *. rewrite (Neqb_correct (alist_nth_ad n0 l0)). reflexivity. intro H3. split with y0. simpl in |- *. rewrite H3. assumption. Qed. @@ -373,16 +192,16 @@ Section LSort. Qed. Definition ad_monotonic (pf:ad -> ad) := - forall a a':ad, ad_less a a' = true -> ad_less (pf a) (pf a') = true. + forall a a':ad, Nless a a' = true -> Nless (pf a) (pf a') = true. - Lemma ad_double_monotonic : ad_monotonic ad_double. + Lemma Ndouble_monotonic : ad_monotonic Ndouble. Proof. - unfold ad_monotonic in |- *. intros. rewrite ad_less_def_1. assumption. + unfold ad_monotonic in |- *. intros. rewrite Nless_def_1. assumption. Qed. - Lemma ad_double_plus_un_monotonic : ad_monotonic ad_double_plus_un. + Lemma Ndouble_plus_one_monotonic : ad_monotonic Ndouble_plus_one. Proof. - unfold ad_monotonic in |- *. intros. rewrite ad_less_def_2. assumption. + unfold ad_monotonic in |- *. intros. rewrite Nless_def_2. assumption. Qed. Lemma ad_comp_monotonic : @@ -395,18 +214,18 @@ Section LSort. Lemma ad_comp_double_monotonic : forall pf:ad -> ad, - ad_monotonic pf -> ad_monotonic (fun a0:ad => pf (ad_double a0)). + ad_monotonic pf -> ad_monotonic (fun a0:ad => pf (Ndouble a0)). Proof. intros. apply ad_comp_monotonic. assumption. - exact ad_double_monotonic. + exact Ndouble_monotonic. Qed. Lemma ad_comp_double_plus_un_monotonic : forall pf:ad -> ad, - ad_monotonic pf -> ad_monotonic (fun a0:ad => pf (ad_double_plus_un a0)). + ad_monotonic pf -> ad_monotonic (fun a0:ad => pf (Ndouble_plus_one a0)). Proof. intros. apply ad_comp_monotonic. assumption. - exact ad_double_plus_un_monotonic. + exact Ndouble_plus_one_monotonic. Qed. Lemma alist_of_Map_sorts_1 : @@ -420,22 +239,22 @@ Section LSort. intros. simpl in |- *. apply alist_sorted_1_imp_2. apply alist_sorted_imp_1. reflexivity. intros. simpl in |- *. apply alist_conc_sorted. exact - (H (fun a0:ad => pf (ad_double a0)) (ad_comp_double_monotonic pf H1)). + (H (fun a0:ad => pf (Ndouble a0)) (ad_comp_double_monotonic pf H1)). exact - (H0 (fun a0:ad => pf (ad_double_plus_un a0)) + (H0 (fun a0:ad => pf (Ndouble_plus_one a0)) (ad_comp_double_plus_un_monotonic pf H1)). intros. elim - (alist_of_Map_nth_ad m0 (fun a0:ad => pf (ad_double a0)) + (alist_of_Map_nth_ad m0 (fun a0:ad => pf (Ndouble a0)) (MapFold1 A (alist A) (anil A) (aapp A) (fun (a0:ad) (y:A) => acons A (a0, y) (anil A)) - (fun a0:ad => pf (ad_double a0)) m0) (refl_equal _) n H2). + (fun a0:ad => pf (Ndouble a0)) m0) (refl_equal _) n H2). intros a H4. rewrite H4. elim - (alist_of_Map_nth_ad m1 (fun a0:ad => pf (ad_double_plus_un a0)) + (alist_of_Map_nth_ad m1 (fun a0:ad => pf (Ndouble_plus_one a0)) (MapFold1 A (alist A) (anil A) (aapp A) (fun (a0:ad) (y:A) => acons A (a0, y) (anil A)) - (fun a0:ad => pf (ad_double_plus_un a0)) m1) ( + (fun a0:ad => pf (Ndouble_plus_one a0)) m1) ( refl_equal _) n' H3). - intros a' H5. rewrite H5. unfold ad_monotonic in H1. apply H1. apply ad_less_def_3. + intros a' H5. rewrite H5. unfold ad_monotonic in H1. apply H1. apply Nless_def_3. Qed. Lemma alist_of_Map_sorts : @@ -444,7 +263,7 @@ Section LSort. intro. apply alist_sorted_2_imp. exact (alist_of_Map_sorts_1 m (fun a0:ad => a0) - (fun (a a':ad) (p:ad_less a a' = true) => p)). + (fun (a a':ad) (p:Nless a a' = true) => p)). Qed. Lemma alist_of_Map_sorts1 : @@ -458,59 +277,25 @@ Section LSort. Proof. intro. apply alist_sorted_1_imp_2. apply alist_of_Map_sorts1. Qed. - - Lemma ad_less_total : - forall a a':ad, {ad_less a a' = true} + {ad_less a' a = true} + {a = a'}. - Proof. - intro a. refine - (ad_rec_double a - (fun a:ad => - forall a':ad, - {ad_less a a' = true} + {ad_less a' a = true} + {a = a'}) _ _ _). - intro. elim (sumbool_of_bool (ad_less ad_z a')). intro H. left. left. assumption. - intro H. right. rewrite (ad_z_less_2 a' H). reflexivity. - intros a0 H a'. refine - (ad_rec_double a' - (fun a':ad => - {ad_less (ad_double a0) a' = true} + - {ad_less a' (ad_double a0) = true} + {ad_double a0 = a'}) _ _ _). - elim (sumbool_of_bool (ad_less ad_z (ad_double a0))). intro H0. left. right. assumption. - intro H0. right. exact (ad_z_less_2 _ H0). - intros a1 H0. rewrite ad_less_def_1. rewrite ad_less_def_1. elim (H a1). intro H1. - left. assumption. - intro H1. right. rewrite H1. reflexivity. - intros a1 H0. left. left. apply ad_less_def_3. - intros a0 H a'. refine - (ad_rec_double a' - (fun a':ad => - {ad_less (ad_double_plus_un a0) a' = true} + - {ad_less a' (ad_double_plus_un a0) = true} + - {ad_double_plus_un a0 = a'}) _ _ _). - left. right. case a0; reflexivity. - intros a1 H0. left. right. apply ad_less_def_3. - intros a1 H0. rewrite ad_less_def_2. rewrite ad_less_def_2. elim (H a1). intro H1. - left. assumption. - intro H1. right. rewrite H1. reflexivity. - Qed. Lemma alist_too_low : forall (l:alist A) (a a':ad) (y:A), - ad_less a a' = true -> + Nless a a' = true -> alist_sorted_2 ((a', y) :: l) -> - alist_semantics A ((a', y) :: l) a = NONE A. + alist_semantics A ((a', y) :: l) a = None. Proof. - simple induction l. intros. simpl in |- *. elim (sumbool_of_bool (ad_eq a' a)). intro H1. - rewrite (ad_eq_complete _ _ H1) in H. rewrite (ad_less_not_refl a) in H. discriminate H. + simple induction l. intros. simpl in |- *. elim (sumbool_of_bool (Neqb a' a)). intro H1. + rewrite (Neqb_complete _ _ H1) in H. rewrite (Nless_not_refl a) in H. discriminate H. intro H1. rewrite H1. reflexivity. intro r. elim r. intros a y l0 H a0 a1 y0 H0 H1. change - (match ad_eq a1 a0 with - | true => SOME A y0 + (match Neqb a1 a0 with + | true => Some y0 | false => alist_semantics A ((a, y) :: l0) a0 - end = NONE A) in |- *. - elim (sumbool_of_bool (ad_eq a1 a0)). intro H2. rewrite (ad_eq_complete _ _ H2) in H0. - rewrite (ad_less_not_refl a0) in H0. discriminate H0. - intro H2. rewrite H2. apply H. apply ad_less_trans with (a' := a1). assumption. + end = None) in |- *. + elim (sumbool_of_bool (Neqb a1 a0)). intro H2. rewrite (Neqb_complete _ _ H2) in H0. + rewrite (Nless_not_refl a0) in H0. discriminate H0. + intro H2. rewrite H2. apply H. apply Nless_trans with (a' := a1). assumption. unfold alist_sorted_2 in H1. apply (H1 0 1). apply lt_n_Sn. simpl in |- *. apply le_n_S. apply le_n_S. apply le_O_n. apply alist_sorted_1_imp_2. apply alist_sorted_imp_1. @@ -521,13 +306,13 @@ Section LSort. Lemma alist_semantics_nth_ad : forall (l:alist A) (a:ad) (y:A), - alist_semantics A l a = SOME A y -> + alist_semantics A l a = Some y -> {n : nat | S n <= length l /\ alist_nth_ad n l = a}. Proof. simple induction l. intros. discriminate H. - intro r. elim r. intros a y l0 H a0 y0 H0. simpl in H0. elim (sumbool_of_bool (ad_eq a a0)). + intro r. elim r. intros a y l0 H a0 y0 H0. simpl in H0. elim (sumbool_of_bool (Neqb a a0)). intro H1. rewrite H1 in H0. split with 0. split. simpl in |- *. apply le_n_S. apply le_O_n. - simpl in |- *. exact (ad_eq_complete _ _ H1). + simpl in |- *. exact (Neqb_complete _ _ H1). intro H1. rewrite H1 in H0. elim (H a0 y0 H0). intros n' H2. split with (S n'). split. simpl in |- *. apply le_n_S. exact (proj1 H2). exact (proj2 H2). @@ -538,16 +323,16 @@ Section LSort. alist_sorted_2 ((a, y) :: l) -> eqm A (alist_semantics A l) (fun a0:ad => - if ad_eq a a0 then NONE A else alist_semantics A ((a, y) :: l) a0). + if Neqb a a0 then None else alist_semantics A ((a, y) :: l) a0). Proof. - unfold eqm in |- *. intros. elim (sumbool_of_bool (ad_eq a a0)). intro H0. rewrite H0. - rewrite <- (ad_eq_complete _ _ H0). unfold alist_sorted_2 in H. + unfold eqm in |- *. intros. elim (sumbool_of_bool (Neqb a a0)). intro H0. rewrite H0. + rewrite <- (Neqb_complete _ _ H0). unfold alist_sorted_2 in H. elim (option_sum A (alist_semantics A l a)). intro H1. elim H1. intros y0 H2. elim (alist_semantics_nth_ad l a y0 H2). intros n H3. elim H3. intros. cut - (ad_less (alist_nth_ad 0 ((a, y) :: l)) + (Nless (alist_nth_ad 0 ((a, y) :: l)) (alist_nth_ad (S n) ((a, y) :: l)) = true). - intro. simpl in H6. rewrite H5 in H6. rewrite (ad_less_not_refl a) in H6. discriminate H6. + intro. simpl in H6. rewrite H5 in H6. rewrite (Nless_not_refl a) in H6. discriminate H6. apply H. apply lt_O_Sn. simpl in |- *. apply le_n_S. assumption. trivial. @@ -563,7 +348,7 @@ Section LSort. eqm A (alist_semantics A l) (alist_semantics A l'). Proof. unfold eqm in |- *. intros. rewrite (alist_semantics_tail _ _ _ H a0). - rewrite (alist_semantics_tail _ _ _ H0 a0). case (ad_eq a a0). reflexivity. + rewrite (alist_semantics_tail _ _ _ H0 a0). case (Neqb a a0). reflexivity. exact (H1 a0). Qed. @@ -583,40 +368,40 @@ Section LSort. unfold eqm in |- *. simple induction l. simple induction l'. trivial. intro r. elim r. intros a y l0 H H0 H1 H2. simpl in H0. cut - (NONE A = - match ad_eq a a with - | true => SOME A y + (None = + match Neqb a a with + | true => Some y | false => alist_semantics A l0 a end). - rewrite (ad_eq_correct a). intro. discriminate H3. + rewrite (Neqb_correct a). intro. discriminate H3. exact (H0 a). intro r. elim r. intros a y l0 H. simple induction l'. intros. simpl in H0. cut - (match ad_eq a a with - | true => SOME A y + (match Neqb a a with + | true => Some y | false => alist_semantics A l0 a - end = NONE A). - rewrite (ad_eq_correct a). intro. discriminate H3. + end = None). + rewrite (Neqb_correct a). intro. discriminate H3. exact (H0 a). - intro r'. elim r'. intros a' y' l'0 H0 H1 H2 H3. elim (ad_less_total a a'). intro H4. + intro r'. elim r'. intros a' y' l'0 H0 H1 H2 H3. elim (Nless_total a a'). intro H4. elim H4. intro H5. cut (alist_semantics A ((a, y) :: l0) a = alist_semantics A ((a', y') :: l'0) a). intro. rewrite (alist_too_low l'0 a a' y' H5 H3) in H6. simpl in H6. - rewrite (ad_eq_correct a) in H6. discriminate H6. + rewrite (Neqb_correct a) in H6. discriminate H6. exact (H1 a). intro H5. cut (alist_semantics A ((a, y) :: l0) a' = alist_semantics A ((a', y') :: l'0) a'). intro. rewrite (alist_too_low l0 a' a y H5 H2) in H6. simpl in H6. - rewrite (ad_eq_correct a') in H6. discriminate H6. + rewrite (Neqb_correct a') in H6. discriminate H6. exact (H1 a'). intro H4. rewrite H4. cut (alist_semantics A ((a, y) :: l0) a = alist_semantics A ((a', y') :: l'0) a). - intro. simpl in H5. rewrite H4 in H5. rewrite (ad_eq_correct a') in H5. inversion H5. + intro. simpl in H5. rewrite H4 in H5. rewrite (Neqb_correct a') in H5. inversion H5. rewrite H4 in H1. rewrite H7 in H1. cut (l0 = l'0). intro. rewrite H6. reflexivity. apply H. rewrite H4 in H2. rewrite H7 in H2. exact (alist_semantics_same_tail l0 l'0 a' y' H2 H3 H1). diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v index 5345f81b..2be6de04 100644 --- a/theories/IntMap/Map.v +++ b/theories/IntMap/Map.v @@ -5,21 +5,26 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Map.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Map.v 8733 2006-04-25 22:52:18Z letouzey $ i*) (** Definition of finite sets as trees indexed by adresses *) Require Import Bool. Require Import Sumbool. -Require Import ZArith. -Require Import Addr. -Require Import Adist. -Require Import Addec. +Require Import NArith. +Require Import Ndigits. +Require Import Ndec. +(* The type [ad] of addresses is now [N] in [BinNat]. *) + +Definition ad := N. + +(* a Notation or complete replacement would be nice, + but that would changes hyps names *) Section MapDefs. -(** We define maps from ad to A. *) +(** We now define maps from ad to A. *) Variable A : Set. Inductive Map : Set := @@ -27,31 +32,28 @@ Section MapDefs. | M1 : ad -> A -> Map | M2 : Map -> Map -> Map. - Inductive option : Set := - | NONE : option - | SOME : A -> option. - - Lemma option_sum : forall o:option, {y : A | o = SOME y} + {o = NONE}. + Lemma option_sum : forall o:option A, {y : A | o = Some y} + {o = None}. Proof. - simple induction o. right. reflexivity. + simple induction o. left. split with a. reflexivity. + right. reflexivity. Qed. (** The semantics of maps is given by the function [MapGet]. The semantics of a map [m] is a partial, finite function from [ad] to [A]: *) - Fixpoint MapGet (m:Map) : ad -> option := + Fixpoint MapGet (m:Map) : ad -> option A := match m with - | M0 => fun a:ad => NONE - | M1 x y => fun a:ad => if ad_eq x a then SOME y else NONE + | M0 => fun a:ad => None + | M1 x y => fun a:ad => if Neqb x a then Some y else None | M2 m1 m2 => fun a:ad => match a with - | ad_z => MapGet m1 ad_z - | ad_x xH => MapGet m2 ad_z - | ad_x (xO p) => MapGet m1 (ad_x p) - | ad_x (xI p) => MapGet m2 (ad_x p) + | N0 => MapGet m1 N0 + | Npos xH => MapGet m2 N0 + | Npos (xO p) => MapGet m1 (Npos p) + | Npos (xI p) => MapGet m2 (Npos p) end end. @@ -59,9 +61,9 @@ Section MapDefs. Definition MapSingleton := M1. - Definition eqm (g g':ad -> option) := forall a:ad, g a = g' a. + Definition eqm (g g':ad -> option A) := forall a:ad, g a = g' a. - Lemma newMap_semantics : eqm (MapGet newMap) (fun a:ad => NONE). + Lemma newMap_semantics : eqm (MapGet newMap) (fun a:ad => None). Proof. simpl in |- *. unfold eqm in |- *. trivial. Qed. @@ -69,61 +71,61 @@ Section MapDefs. Lemma MapSingleton_semantics : forall (a:ad) (y:A), eqm (MapGet (MapSingleton a y)) - (fun a':ad => if ad_eq a a' then SOME y else NONE). + (fun a':ad => if Neqb a a' then Some y else None). Proof. simpl in |- *. unfold eqm in |- *. trivial. Qed. - Lemma M1_semantics_1 : forall (a:ad) (y:A), MapGet (M1 a y) a = SOME y. + Lemma M1_semantics_1 : forall (a:ad) (y:A), MapGet (M1 a y) a = Some y. Proof. - unfold MapGet in |- *. intros. rewrite (ad_eq_correct a). reflexivity. + unfold MapGet in |- *. intros. rewrite (Neqb_correct a). reflexivity. Qed. Lemma M1_semantics_2 : - forall (a a':ad) (y:A), ad_eq a a' = false -> MapGet (M1 a y) a' = NONE. + forall (a a':ad) (y:A), Neqb a a' = false -> MapGet (M1 a y) a' = None. Proof. intros. simpl in |- *. rewrite H. reflexivity. Qed. Lemma Map2_semantics_1 : forall m m':Map, - eqm (MapGet m) (fun a:ad => MapGet (M2 m m') (ad_double a)). + eqm (MapGet m) (fun a:ad => MapGet (M2 m m') (Ndouble a)). Proof. unfold eqm in |- *. simple induction a; trivial. Qed. Lemma Map2_semantics_1_eq : - forall (m m':Map) (f:ad -> option), - eqm (MapGet (M2 m m')) f -> eqm (MapGet m) (fun a:ad => f (ad_double a)). + forall (m m':Map) (f:ad -> option A), + eqm (MapGet (M2 m m')) f -> eqm (MapGet m) (fun a:ad => f (Ndouble a)). Proof. unfold eqm in |- *. intros. - rewrite <- (H (ad_double a)). + rewrite <- (H (Ndouble a)). exact (Map2_semantics_1 m m' a). Qed. Lemma Map2_semantics_2 : forall m m':Map, - eqm (MapGet m') (fun a:ad => MapGet (M2 m m') (ad_double_plus_un a)). + eqm (MapGet m') (fun a:ad => MapGet (M2 m m') (Ndouble_plus_one a)). Proof. unfold eqm in |- *. simple induction a; trivial. Qed. Lemma Map2_semantics_2_eq : - forall (m m':Map) (f:ad -> option), + forall (m m':Map) (f:ad -> option A), eqm (MapGet (M2 m m')) f -> - eqm (MapGet m') (fun a:ad => f (ad_double_plus_un a)). + eqm (MapGet m') (fun a:ad => f (Ndouble_plus_one a)). Proof. unfold eqm in |- *. intros. - rewrite <- (H (ad_double_plus_un a)). + rewrite <- (H (Ndouble_plus_one a)). exact (Map2_semantics_2 m m' a). Qed. Lemma MapGet_M2_bit_0_0 : forall a:ad, - ad_bit_0 a = false -> - forall m m':Map, MapGet (M2 m m') a = MapGet m (ad_div_2 a). + Nbit0 a = false -> + forall m m':Map, MapGet (M2 m m') a = MapGet m (Ndiv2 a). Proof. simple induction a; trivial. simple induction p. intros. discriminate H0. trivial. @@ -132,8 +134,8 @@ Section MapDefs. Lemma MapGet_M2_bit_0_1 : forall a:ad, - ad_bit_0 a = true -> - forall m m':Map, MapGet (M2 m m') a = MapGet m' (ad_div_2 a). + Nbit0 a = true -> + forall m m':Map, MapGet (M2 m m') a = MapGet m' (Ndiv2 a). Proof. simple induction a. intros. discriminate H. simple induction p. trivial. @@ -144,19 +146,19 @@ Section MapDefs. Lemma MapGet_M2_bit_0_if : forall (m m':Map) (a:ad), MapGet (M2 m m') a = - (if ad_bit_0 a then MapGet m' (ad_div_2 a) else MapGet m (ad_div_2 a)). + (if Nbit0 a then MapGet m' (Ndiv2 a) else MapGet m (Ndiv2 a)). Proof. - intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H. rewrite H. + intros. elim (sumbool_of_bool (Nbit0 a)). intro H. rewrite H. apply MapGet_M2_bit_0_1; assumption. intro H. rewrite H. apply MapGet_M2_bit_0_0; assumption. Qed. Lemma MapGet_M2_bit_0 : forall (m m' m'':Map) (a:ad), - (if ad_bit_0 a then MapGet (M2 m' m) a else MapGet (M2 m m'') a) = - MapGet m (ad_div_2 a). + (if Nbit0 a then MapGet (M2 m' m) a else MapGet (M2 m m'') a) = + MapGet m (Ndiv2 a). Proof. - intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H. rewrite H. + intros. elim (sumbool_of_bool (Nbit0 a)). intro H. rewrite H. apply MapGet_M2_bit_0_1; assumption. intro H. rewrite H. apply MapGet_M2_bit_0_0; assumption. Qed. @@ -165,9 +167,9 @@ Section MapDefs. forall m m':Map, eqm (MapGet (M2 m m')) (fun a:ad => - match ad_bit_0 a with - | false => MapGet m (ad_div_2 a) - | true => MapGet m' (ad_div_2 a) + match Nbit0 a with + | false => MapGet m (Ndiv2 a) + | true => MapGet m' (Ndiv2 a) end). Proof. unfold eqm in |- *. @@ -176,20 +178,20 @@ Section MapDefs. Qed. Lemma Map2_semantics_3_eq : - forall (m m':Map) (f f':ad -> option), + forall (m m':Map) (f f':ad -> option A), eqm (MapGet m) f -> eqm (MapGet m') f' -> eqm (MapGet (M2 m m')) (fun a:ad => - match ad_bit_0 a with - | false => f (ad_div_2 a) - | true => f' (ad_div_2 a) + match Nbit0 a with + | false => f (Ndiv2 a) + | true => f' (Ndiv2 a) end). Proof. unfold eqm in |- *. intros. - rewrite <- (H (ad_div_2 a)). - rewrite <- (H0 (ad_div_2 a)). + rewrite <- (H (Ndiv2 a)). + rewrite <- (H0 (Ndiv2 a)). exact (Map2_semantics_3 m m' a). Qed. @@ -197,15 +199,15 @@ Section MapDefs. Map := match p with | xO p' => - let m := MapPut1 (ad_div_2 a) y (ad_div_2 a') y' p' in - match ad_bit_0 a with + let m := MapPut1 (Ndiv2 a) y (Ndiv2 a') y' p' in + match Nbit0 a with | false => M2 m M0 | true => M2 M0 m end | _ => - match ad_bit_0 a with - | false => M2 (M1 (ad_div_2 a) y) (M1 (ad_div_2 a') y') - | true => M2 (M1 (ad_div_2 a') y') (M1 (ad_div_2 a) y) + match Nbit0 a with + | false => M2 (M1 (Ndiv2 a) y) (M1 (Ndiv2 a') y') + | true => M2 (M1 (Ndiv2 a') y') (M1 (Ndiv2 a) y) end end. @@ -218,14 +220,14 @@ Section MapDefs. (*i Lemma MapGet_M2_bit_0_1' : (m,m',m'',m''':Map) - (a:ad) (MapGet (if (ad_bit_0 a) then (M2 m m') else (M2 m'' m''')) a)= - (MapGet (if (ad_bit_0 a) then m' else m'') (ad_div_2 a)). + (a:ad) (MapGet (if (Nbit0 a) then (M2 m m') else (M2 m'' m''')) a)= + (MapGet (if (Nbit0 a) then m' else m'') (Ndiv2 a)). Proof. - Intros. Rewrite (MapGet_if_commute (ad_bit_0 a)). Rewrite (MapGet_if_commute (ad_bit_0 a)). - Cut (ad_bit_0 a)=false\/(ad_bit_0 a)=true. Intros. Elim H. Intros. Rewrite H0. + Intros. Rewrite (MapGet_if_commute (Nbit0 a)). Rewrite (MapGet_if_commute (Nbit0 a)). + Cut (Nbit0 a)=false\/(Nbit0 a)=true. Intros. Elim H. Intros. Rewrite H0. Apply MapGet_M2_bit_0_0. Assumption. Intros. Rewrite H0. Apply MapGet_M2_bit_0_1. Assumption. - Case (ad_bit_0 a); Auto. + Case (Nbit0 a); Auto. Qed. i*) @@ -237,107 +239,107 @@ Section MapDefs. Lemma MapGet_M2_bit_0_2 : forall (m m' m'':Map) (a:ad), - MapGet (if ad_bit_0 a then M2 m m' else M2 m' m'') a = - MapGet m' (ad_div_2 a). + MapGet (if Nbit0 a then M2 m m' else M2 m' m'') a = + MapGet m' (Ndiv2 a). Proof. intros. rewrite MapGet_if_commute. apply MapGet_M2_bit_0. Qed. Lemma MapPut1_semantics_1 : forall (p:positive) (a a':ad) (y y':A), - ad_xor a a' = ad_x p -> MapGet (MapPut1 a y a' y' p) a = SOME y. + Nxor a a' = Npos p -> MapGet (MapPut1 a y a' y' p) a = Some y. Proof. simple induction p. intros. unfold MapPut1 in |- *. rewrite MapGet_M2_bit_0_2. apply M1_semantics_1. - intros. simpl in |- *. rewrite MapGet_M2_bit_0_2. apply H. rewrite <- ad_xor_div_2. rewrite H0. + intros. simpl in |- *. rewrite MapGet_M2_bit_0_2. apply H. rewrite <- Nxor_div2. rewrite H0. reflexivity. intros. unfold MapPut1 in |- *. rewrite MapGet_M2_bit_0_2. apply M1_semantics_1. Qed. Lemma MapPut1_semantics_2 : forall (p:positive) (a a':ad) (y y':A), - ad_xor a a' = ad_x p -> MapGet (MapPut1 a y a' y' p) a' = SOME y'. + Nxor a a' = Npos p -> MapGet (MapPut1 a y a' y' p) a' = Some y'. Proof. - simple induction p. intros. unfold MapPut1 in |- *. rewrite (ad_neg_bit_0_2 a a' p0 H0). + simple induction p. intros. unfold MapPut1 in |- *. rewrite (Nneg_bit0_2 a a' p0 H0). rewrite if_negb. rewrite MapGet_M2_bit_0_2. apply M1_semantics_1. - intros. simpl in |- *. rewrite (ad_same_bit_0 a a' p0 H0). rewrite MapGet_M2_bit_0_2. - apply H. rewrite <- ad_xor_div_2. rewrite H0. reflexivity. - intros. unfold MapPut1 in |- *. rewrite (ad_neg_bit_0_1 a a' H). rewrite if_negb. + intros. simpl in |- *. rewrite (Nsame_bit0 a a' p0 H0). rewrite MapGet_M2_bit_0_2. + apply H. rewrite <- Nxor_div2. rewrite H0. reflexivity. + intros. unfold MapPut1 in |- *. rewrite (Nneg_bit0_1 a a' H). rewrite if_negb. rewrite MapGet_M2_bit_0_2. apply M1_semantics_1. Qed. - Lemma MapGet_M2_both_NONE : + Lemma MapGet_M2_both_None : forall (m m':Map) (a:ad), - MapGet m (ad_div_2 a) = NONE -> - MapGet m' (ad_div_2 a) = NONE -> MapGet (M2 m m') a = NONE. + MapGet m (Ndiv2 a) = None -> + MapGet m' (Ndiv2 a) = None -> MapGet (M2 m m') a = None. Proof. intros. rewrite (Map2_semantics_3 m m' a). - case (ad_bit_0 a); assumption. + case (Nbit0 a); assumption. Qed. Lemma MapPut1_semantics_3 : forall (p:positive) (a a' a0:ad) (y y':A), - ad_xor a a' = ad_x p -> - ad_eq a a0 = false -> - ad_eq a' a0 = false -> MapGet (MapPut1 a y a' y' p) a0 = NONE. - Proof. - simple induction p. intros. unfold MapPut1 in |- *. elim (ad_neq a a0 H1). intro. rewrite H3. rewrite if_negb. - rewrite MapGet_M2_bit_0_2. apply M1_semantics_2. apply ad_div_bit_neq. assumption. - rewrite (ad_neg_bit_0_2 a a' p0 H0) in H3. rewrite (negb_intro (ad_bit_0 a')). - rewrite (negb_intro (ad_bit_0 a0)). rewrite H3. reflexivity. - intro. elim (ad_neq a' a0 H2). intro. rewrite (ad_neg_bit_0_2 a a' p0 H0). rewrite H4. - rewrite (negb_elim (ad_bit_0 a0)). rewrite MapGet_M2_bit_0_2. + Nxor a a' = Npos p -> + Neqb a a0 = false -> + Neqb a' a0 = false -> MapGet (MapPut1 a y a' y' p) a0 = None. + Proof. + simple induction p. intros. unfold MapPut1 in |- *. elim (Nneq_elim a a0 H1). intro. rewrite H3. rewrite if_negb. + rewrite MapGet_M2_bit_0_2. apply M1_semantics_2. apply Ndiv2_bit_neq. assumption. + rewrite (Nneg_bit0_2 a a' p0 H0) in H3. rewrite (negb_intro (Nbit0 a')). + rewrite (negb_intro (Nbit0 a0)). rewrite H3. reflexivity. + intro. elim (Nneq_elim a' a0 H2). intro. rewrite (Nneg_bit0_2 a a' p0 H0). rewrite H4. + rewrite (negb_elim (Nbit0 a0)). rewrite MapGet_M2_bit_0_2. apply M1_semantics_2; assumption. - intro; case (ad_bit_0 a); apply MapGet_M2_both_NONE; apply M1_semantics_2; + intro; case (Nbit0 a); apply MapGet_M2_both_None; apply M1_semantics_2; assumption. - intros. simpl in |- *. elim (ad_neq a a0 H1). intro. rewrite H3. rewrite if_negb. + intros. simpl in |- *. elim (Nneq_elim a a0 H1). intro. rewrite H3. rewrite if_negb. rewrite MapGet_M2_bit_0_2. reflexivity. - intro. elim (ad_neq a' a0 H2). intro. rewrite (ad_same_bit_0 a a' p0 H0). rewrite H4. + intro. elim (Nneq_elim a' a0 H2). intro. rewrite (Nsame_bit0 a a' p0 H0). rewrite H4. rewrite if_negb. rewrite MapGet_M2_bit_0_2. reflexivity. - intro. cut (ad_xor (ad_div_2 a) (ad_div_2 a') = ad_x p0). intro. - case (ad_bit_0 a); apply MapGet_M2_both_NONE; trivial; apply H; + intro. cut (Nxor (Ndiv2 a) (Ndiv2 a') = Npos p0). intro. + case (Nbit0 a); apply MapGet_M2_both_None; trivial; apply H; assumption. - rewrite <- ad_xor_div_2. rewrite H0. reflexivity. - intros. simpl in |- *. elim (ad_neq a a0 H0). intro. rewrite H2. rewrite if_negb. - rewrite MapGet_M2_bit_0_2. apply M1_semantics_2. apply ad_div_bit_neq. assumption. - rewrite (ad_neg_bit_0_1 a a' H) in H2. rewrite (negb_intro (ad_bit_0 a')). - rewrite (negb_intro (ad_bit_0 a0)). rewrite H2. reflexivity. - intro. elim (ad_neq a' a0 H1). intro. rewrite (ad_neg_bit_0_1 a a' H). rewrite H3. - rewrite (negb_elim (ad_bit_0 a0)). rewrite MapGet_M2_bit_0_2. + rewrite <- Nxor_div2. rewrite H0. reflexivity. + intros. simpl in |- *. elim (Nneq_elim a a0 H0). intro. rewrite H2. rewrite if_negb. + rewrite MapGet_M2_bit_0_2. apply M1_semantics_2. apply Ndiv2_bit_neq. assumption. + rewrite (Nneg_bit0_1 a a' H) in H2. rewrite (negb_intro (Nbit0 a')). + rewrite (negb_intro (Nbit0 a0)). rewrite H2. reflexivity. + intro. elim (Nneq_elim a' a0 H1). intro. rewrite (Nneg_bit0_1 a a' H). rewrite H3. + rewrite (negb_elim (Nbit0 a0)). rewrite MapGet_M2_bit_0_2. apply M1_semantics_2; assumption. - intro. case (ad_bit_0 a); apply MapGet_M2_both_NONE; apply M1_semantics_2; + intro. case (Nbit0 a); apply MapGet_M2_both_None; apply M1_semantics_2; assumption. Qed. Lemma MapPut1_semantics : forall (p:positive) (a a':ad) (y y':A), - ad_xor a a' = ad_x p -> + Nxor a a' = Npos p -> eqm (MapGet (MapPut1 a y a' y' p)) (fun a0:ad => - if ad_eq a a0 - then SOME y - else if ad_eq a' a0 then SOME y' else NONE). - Proof. - unfold eqm in |- *. intros. elim (sumbool_of_bool (ad_eq a a0)). intro H0. rewrite H0. - rewrite <- (ad_eq_complete _ _ H0). exact (MapPut1_semantics_1 p a a' y y' H). - intro H0. rewrite H0. elim (sumbool_of_bool (ad_eq a' a0)). intro H1. - rewrite <- (ad_eq_complete _ _ H1). rewrite (ad_eq_correct a'). + if Neqb a a0 + then Some y + else if Neqb a' a0 then Some y' else None). + Proof. + unfold eqm in |- *. intros. elim (sumbool_of_bool (Neqb a a0)). intro H0. rewrite H0. + rewrite <- (Neqb_complete _ _ H0). exact (MapPut1_semantics_1 p a a' y y' H). + intro H0. rewrite H0. elim (sumbool_of_bool (Neqb a' a0)). intro H1. + rewrite <- (Neqb_complete _ _ H1). rewrite (Neqb_correct a'). exact (MapPut1_semantics_2 p a a' y y' H). intro H1. rewrite H1. exact (MapPut1_semantics_3 p a a' a0 y y' H H0 H1). Qed. Lemma MapPut1_semantics' : forall (p:positive) (a a':ad) (y y':A), - ad_xor a a' = ad_x p -> + Nxor a a' = Npos p -> eqm (MapGet (MapPut1 a y a' y' p)) (fun a0:ad => - if ad_eq a' a0 - then SOME y' - else if ad_eq a a0 then SOME y else NONE). + if Neqb a' a0 + then Some y' + else if Neqb a a0 then Some y else None). Proof. unfold eqm in |- *. intros. rewrite (MapPut1_semantics p a a' y y' H a0). - elim (sumbool_of_bool (ad_eq a a0)). intro H0. rewrite H0. - rewrite <- (ad_eq_complete a a0 H0). rewrite (ad_eq_comm a' a). - rewrite (ad_xor_eq_false a a' p H). reflexivity. + elim (sumbool_of_bool (Neqb a a0)). intro H0. rewrite H0. + rewrite <- (Neqb_complete a a0 H0). rewrite (Neqb_comm a' a). + rewrite (Nxor_eq_false a a' p H). reflexivity. intro H0. rewrite H0. reflexivity. Qed. @@ -346,17 +348,17 @@ Section MapDefs. | M0 => M1 | M1 a y => fun (a':ad) (y':A) => - match ad_xor a a' with - | ad_z => M1 a' y' - | ad_x p => MapPut1 a y a' y' p + match Nxor a a' with + | N0 => M1 a' y' + | Npos p => MapPut1 a y a' y' p end | M2 m1 m2 => fun (a:ad) (y:A) => match a with - | ad_z => M2 (MapPut m1 ad_z y) m2 - | ad_x xH => M2 m1 (MapPut m2 ad_z y) - | ad_x (xO p) => M2 (MapPut m1 (ad_x p) y) m2 - | ad_x (xI p) => M2 m1 (MapPut m2 (ad_x p) y) + | N0 => M2 (MapPut m1 N0 y) m2 + | Npos xH => M2 m1 (MapPut m2 N0 y) + | Npos (xO p) => M2 (MapPut m1 (Npos p) y) m2 + | Npos (xI p) => M2 m1 (MapPut m2 (Npos p) y) end end. @@ -370,39 +372,39 @@ Section MapDefs. Lemma MapPut_semantics_2_1 : forall (a:ad) (y y':A) (a0:ad), MapGet (MapPut (M1 a y) a y') a0 = - (if ad_eq a a0 then SOME y' else NONE). + (if Neqb a a0 then Some y' else None). Proof. - simpl in |- *. intros. rewrite (ad_xor_nilpotent a). trivial. + simpl in |- *. intros. rewrite (Nxor_nilpotent a). trivial. Qed. Lemma MapPut_semantics_2_2 : forall (a a':ad) (y y':A) (a0 a'':ad), - ad_xor a a' = a'' -> + Nxor a a' = a'' -> MapGet (MapPut (M1 a y) a' y') a0 = - (if ad_eq a' a0 then SOME y' else if ad_eq a a0 then SOME y else NONE). + (if Neqb a' a0 then Some y' else if Neqb a a0 then Some y else None). Proof. - simple induction a''. intro. rewrite (ad_xor_eq _ _ H). rewrite MapPut_semantics_2_1. - case (ad_eq a' a0); trivial. + simple induction a''. intro. rewrite (Nxor_eq _ _ H). rewrite MapPut_semantics_2_1. + case (Neqb a' a0); trivial. intros. simpl in |- *. rewrite H. rewrite (MapPut1_semantics p a a' y y' H a0). - elim (sumbool_of_bool (ad_eq a a0)). intro H0. rewrite H0. rewrite <- (ad_eq_complete _ _ H0). - rewrite (ad_eq_comm a' a). rewrite (ad_xor_eq_false _ _ _ H). reflexivity. + elim (sumbool_of_bool (Neqb a a0)). intro H0. rewrite H0. rewrite <- (Neqb_complete _ _ H0). + rewrite (Neqb_comm a' a). rewrite (Nxor_eq_false _ _ _ H). reflexivity. intro H0. rewrite H0. reflexivity. Qed. Lemma MapPut_semantics_2 : forall (a a':ad) (y y':A) (a0:ad), MapGet (MapPut (M1 a y) a' y') a0 = - (if ad_eq a' a0 then SOME y' else if ad_eq a a0 then SOME y else NONE). + (if Neqb a' a0 then Some y' else if Neqb a a0 then Some y else None). Proof. - intros. apply MapPut_semantics_2_2 with (a'' := ad_xor a a'); trivial. + intros. apply MapPut_semantics_2_2 with (a'' := Nxor a a'); trivial. Qed. Lemma MapPut_semantics_3_1 : forall (m m':Map) (a:ad) (y:A), MapPut (M2 m m') a y = - (if ad_bit_0 a - then M2 m (MapPut m' (ad_div_2 a) y) - else M2 (MapPut m (ad_div_2 a) y) m'). + (if Nbit0 a + then M2 m (MapPut m' (Ndiv2 a) y) + else M2 (MapPut m (Ndiv2 a) y) m'). Proof. simple induction a. trivial. simple induction p; trivial. @@ -411,24 +413,24 @@ Section MapDefs. Lemma MapPut_semantics : forall (m:Map) (a:ad) (y:A), eqm (MapGet (MapPut m a y)) - (fun a':ad => if ad_eq a a' then SOME y else MapGet m a'). + (fun a':ad => if Neqb a a' then Some y else MapGet m a'). Proof. unfold eqm in |- *. simple induction m. exact MapPut_semantics_1. intros. unfold MapGet at 2 in |- *. apply MapPut_semantics_2; assumption. intros. rewrite MapPut_semantics_3_1. rewrite (MapGet_M2_bit_0_if m0 m1 a0). - elim (sumbool_of_bool (ad_bit_0 a)). intro H1. rewrite H1. rewrite MapGet_M2_bit_0_if. - elim (sumbool_of_bool (ad_bit_0 a0)). intro H2. rewrite H2. - rewrite (H0 (ad_div_2 a) y (ad_div_2 a0)). elim (sumbool_of_bool (ad_eq a a0)). - intro H3. rewrite H3. rewrite (ad_div_eq _ _ H3). reflexivity. - intro H3. rewrite H3. rewrite <- H2 in H1. rewrite (ad_div_bit_neq _ _ H3 H1). reflexivity. - intro H2. rewrite H2. rewrite (ad_eq_comm a a0). rewrite (ad_bit_0_neq a0 a H2 H1). + elim (sumbool_of_bool (Nbit0 a)). intro H1. rewrite H1. rewrite MapGet_M2_bit_0_if. + elim (sumbool_of_bool (Nbit0 a0)). intro H2. rewrite H2. + rewrite (H0 (Ndiv2 a) y (Ndiv2 a0)). elim (sumbool_of_bool (Neqb a a0)). + intro H3. rewrite H3. rewrite (Ndiv2_eq _ _ H3). reflexivity. + intro H3. rewrite H3. rewrite <- H2 in H1. rewrite (Ndiv2_bit_neq _ _ H3 H1). reflexivity. + intro H2. rewrite H2. rewrite (Neqb_comm a a0). rewrite (Nbit0_neq a0 a H2 H1). reflexivity. - intro H1. rewrite H1. rewrite MapGet_M2_bit_0_if. elim (sumbool_of_bool (ad_bit_0 a0)). - intro H2. rewrite H2. rewrite (ad_bit_0_neq a a0 H1 H2). reflexivity. - intro H2. rewrite H2. rewrite (H (ad_div_2 a) y (ad_div_2 a0)). - elim (sumbool_of_bool (ad_eq a a0)). intro H3. rewrite H3. - rewrite (ad_div_eq a a0 H3). reflexivity. - intro H3. rewrite H3. rewrite <- H2 in H1. rewrite (ad_div_bit_neq a a0 H3 H1). reflexivity. + intro H1. rewrite H1. rewrite MapGet_M2_bit_0_if. elim (sumbool_of_bool (Nbit0 a0)). + intro H2. rewrite H2. rewrite (Nbit0_neq a a0 H1 H2). reflexivity. + intro H2. rewrite H2. rewrite (H (Ndiv2 a) y (Ndiv2 a0)). + elim (sumbool_of_bool (Neqb a a0)). intro H3. rewrite H3. + rewrite (Ndiv2_eq a a0 H3). reflexivity. + intro H3. rewrite H3. rewrite <- H2 in H1. rewrite (Ndiv2_bit_neq a a0 H3 H1). reflexivity. Qed. Fixpoint MapPut_behind (m:Map) : ad -> A -> Map := @@ -436,26 +438,26 @@ Section MapDefs. | M0 => M1 | M1 a y => fun (a':ad) (y':A) => - match ad_xor a a' with - | ad_z => m - | ad_x p => MapPut1 a y a' y' p + match Nxor a a' with + | N0 => m + | Npos p => MapPut1 a y a' y' p end | M2 m1 m2 => fun (a:ad) (y:A) => match a with - | ad_z => M2 (MapPut_behind m1 ad_z y) m2 - | ad_x xH => M2 m1 (MapPut_behind m2 ad_z y) - | ad_x (xO p) => M2 (MapPut_behind m1 (ad_x p) y) m2 - | ad_x (xI p) => M2 m1 (MapPut_behind m2 (ad_x p) y) + | N0 => M2 (MapPut_behind m1 N0 y) m2 + | Npos xH => M2 m1 (MapPut_behind m2 N0 y) + | Npos (xO p) => M2 (MapPut_behind m1 (Npos p) y) m2 + | Npos (xI p) => M2 m1 (MapPut_behind m2 (Npos p) y) end end. Lemma MapPut_behind_semantics_3_1 : forall (m m':Map) (a:ad) (y:A), MapPut_behind (M2 m m') a y = - (if ad_bit_0 a - then M2 m (MapPut_behind m' (ad_div_2 a) y) - else M2 (MapPut_behind m (ad_div_2 a) y) m'). + (if Nbit0 a + then M2 m (MapPut_behind m' (Ndiv2 a) y) + else M2 (MapPut_behind m (Ndiv2 a) y) m'). Proof. simple induction a. trivial. simple induction p; trivial. @@ -463,52 +465,52 @@ Section MapDefs. Lemma MapPut_behind_as_before_1 : forall a a' a0:ad, - ad_eq a' a0 = false -> + Neqb a' a0 = false -> forall y y':A, MapGet (MapPut (M1 a y) a' y') a0 = MapGet (MapPut_behind (M1 a y) a' y') a0. Proof. - intros a a' a0. simpl in |- *. intros H y y'. elim (ad_sum (ad_xor a a')). intro H0. elim H0. + intros a a' a0. simpl in |- *. intros H y y'. elim (Ndiscr (Nxor a a')). intro H0. elim H0. intros p H1. rewrite H1. reflexivity. - intro H0. rewrite H0. rewrite (ad_xor_eq _ _ H0). rewrite (M1_semantics_2 a' a0 y H). + intro H0. rewrite H0. rewrite (Nxor_eq _ _ H0). rewrite (M1_semantics_2 a' a0 y H). exact (M1_semantics_2 a' a0 y' H). Qed. Lemma MapPut_behind_as_before : forall (m:Map) (a:ad) (y:A) (a0:ad), - ad_eq a a0 = false -> + Neqb a a0 = false -> MapGet (MapPut m a y) a0 = MapGet (MapPut_behind m a y) a0. Proof. simple induction m. trivial. intros a y a' y' a0 H. exact (MapPut_behind_as_before_1 a a' a0 H y y'). intros. rewrite MapPut_semantics_3_1. rewrite MapPut_behind_semantics_3_1. - elim (sumbool_of_bool (ad_bit_0 a)). intro H2. rewrite H2. rewrite MapGet_M2_bit_0_if. - rewrite MapGet_M2_bit_0_if. elim (sumbool_of_bool (ad_bit_0 a0)). intro H3. - rewrite H3. apply H0. rewrite <- H3 in H2. exact (ad_div_bit_neq a a0 H1 H2). + elim (sumbool_of_bool (Nbit0 a)). intro H2. rewrite H2. rewrite MapGet_M2_bit_0_if. + rewrite MapGet_M2_bit_0_if. elim (sumbool_of_bool (Nbit0 a0)). intro H3. + rewrite H3. apply H0. rewrite <- H3 in H2. exact (Ndiv2_bit_neq a a0 H1 H2). intro H3. rewrite H3. reflexivity. intro H2. rewrite H2. rewrite MapGet_M2_bit_0_if. rewrite MapGet_M2_bit_0_if. - elim (sumbool_of_bool (ad_bit_0 a0)). intro H3. rewrite H3. reflexivity. - intro H3. rewrite H3. apply H. rewrite <- H3 in H2. exact (ad_div_bit_neq a a0 H1 H2). + elim (sumbool_of_bool (Nbit0 a0)). intro H3. rewrite H3. reflexivity. + intro H3. rewrite H3. apply H. rewrite <- H3 in H2. exact (Ndiv2_bit_neq a a0 H1 H2). Qed. Lemma MapPut_behind_new : forall (m:Map) (a:ad) (y:A), MapGet (MapPut_behind m a y) a = match MapGet m a with - | SOME y' => SOME y' - | _ => SOME y + | Some y' => Some y' + | _ => Some y end. Proof. - simple induction m. simpl in |- *. intros. rewrite (ad_eq_correct a). reflexivity. - intros. elim (ad_sum (ad_xor a a1)). intro H. elim H. intros p H0. simpl in |- *. - rewrite H0. rewrite (ad_xor_eq_false a a1 p). exact (MapPut1_semantics_2 p a a1 a0 y H0). + simple induction m. simpl in |- *. intros. rewrite (Neqb_correct a). reflexivity. + intros. elim (Ndiscr (Nxor a a1)). intro H. elim H. intros p H0. simpl in |- *. + rewrite H0. rewrite (Nxor_eq_false a a1 p). exact (MapPut1_semantics_2 p a a1 a0 y H0). assumption. - intro H. simpl in |- *. rewrite H. rewrite <- (ad_xor_eq _ _ H). rewrite (ad_eq_correct a). + intro H. simpl in |- *. rewrite H. rewrite <- (Nxor_eq _ _ H). rewrite (Neqb_correct a). exact (M1_semantics_1 a a0). intros. rewrite MapPut_behind_semantics_3_1. rewrite (MapGet_M2_bit_0_if m0 m1 a). - elim (sumbool_of_bool (ad_bit_0 a)). intro H1. rewrite H1. rewrite (MapGet_M2_bit_0_1 a H1). - exact (H0 (ad_div_2 a) y). - intro H1. rewrite H1. rewrite (MapGet_M2_bit_0_0 a H1). exact (H (ad_div_2 a) y). + elim (sumbool_of_bool (Nbit0 a)). intro H1. rewrite H1. rewrite (MapGet_M2_bit_0_1 a H1). + exact (H0 (Ndiv2 a) y). + intro H1. rewrite H1. rewrite (MapGet_M2_bit_0_0 a H1). exact (H (Ndiv2 a) y). Qed. Lemma MapPut_behind_semantics : @@ -516,12 +518,12 @@ Section MapDefs. eqm (MapGet (MapPut_behind m a y)) (fun a':ad => match MapGet m a' with - | SOME y' => SOME y' - | _ => if ad_eq a a' then SOME y else NONE + | Some y' => Some y' + | _ => if Neqb a a' then Some y else None end). Proof. - unfold eqm in |- *. intros. elim (sumbool_of_bool (ad_eq a a0)). intro H. rewrite H. - rewrite (ad_eq_complete _ _ H). apply MapPut_behind_new. + unfold eqm in |- *. intros. elim (sumbool_of_bool (Neqb a a0)). intro H. rewrite H. + rewrite (Neqb_complete _ _ H). apply MapPut_behind_new. intro H. rewrite H. rewrite <- (MapPut_behind_as_before m a y a0 H). rewrite (MapPut_semantics m a y a0). rewrite H. case (MapGet m a0); trivial. Qed. @@ -529,41 +531,41 @@ Section MapDefs. Definition makeM2 (m m':Map) := match m, m' with | M0, M0 => M0 - | M0, M1 a y => M1 (ad_double_plus_un a) y - | M1 a y, M0 => M1 (ad_double a) y + | M0, M1 a y => M1 (Ndouble_plus_one a) y + | M1 a y, M0 => M1 (Ndouble a) y | _, _ => M2 m m' end. Lemma makeM2_M2 : forall m m':Map, eqm (MapGet (makeM2 m m')) (MapGet (M2 m m')). Proof. - unfold eqm in |- *. intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H. + unfold eqm in |- *. intros. elim (sumbool_of_bool (Nbit0 a)). intro H. rewrite (MapGet_M2_bit_0_1 a H m m'). case m'. case m. reflexivity. - intros a0 y. simpl in |- *. rewrite (ad_bit_0_1_not_double a H a0). reflexivity. + intros a0 y. simpl in |- *. rewrite (Nodd_not_double a H a0). reflexivity. intros m1 m2. unfold makeM2 in |- *. rewrite MapGet_M2_bit_0_1. reflexivity. assumption. - case m. intros a0 y. simpl in |- *. elim (sumbool_of_bool (ad_eq a0 (ad_div_2 a))). - intro H0. rewrite H0. rewrite (ad_eq_complete _ _ H0). rewrite (ad_div_2_double_plus_un a H). - rewrite (ad_eq_correct a). reflexivity. - intro H0. rewrite H0. rewrite (ad_eq_comm a0 (ad_div_2 a)) in H0. - rewrite (ad_not_div_2_not_double_plus_un a a0 H0). reflexivity. + case m. intros a0 y. simpl in |- *. elim (sumbool_of_bool (Neqb a0 (Ndiv2 a))). + intro H0. rewrite H0. rewrite (Neqb_complete _ _ H0). rewrite (Ndiv2_double_plus_one a H). + rewrite (Neqb_correct a). reflexivity. + intro H0. rewrite H0. rewrite (Neqb_comm a0 (Ndiv2 a)) in H0. + rewrite (Nnot_div2_not_double_plus_one a a0 H0). reflexivity. intros a0 y0 a1 y1. unfold makeM2 in |- *. rewrite MapGet_M2_bit_0_1. reflexivity. assumption. intros m1 m2 a0 y. unfold makeM2 in |- *. rewrite MapGet_M2_bit_0_1. reflexivity. assumption. intros m1 m2. unfold makeM2 in |- *. - cut (MapGet (M2 m (M2 m1 m2)) a = MapGet (M2 m1 m2) (ad_div_2 a)). + cut (MapGet (M2 m (M2 m1 m2)) a = MapGet (M2 m1 m2) (Ndiv2 a)). case m; trivial. exact (MapGet_M2_bit_0_1 a H m (M2 m1 m2)). intro H. rewrite (MapGet_M2_bit_0_0 a H m m'). case m. case m'. reflexivity. - intros a0 y. simpl in |- *. rewrite (ad_bit_0_0_not_double_plus_un a H a0). reflexivity. + intros a0 y. simpl in |- *. rewrite (Neven_not_double_plus_one a H a0). reflexivity. intros m1 m2. unfold makeM2 in |- *. rewrite MapGet_M2_bit_0_0. reflexivity. assumption. - case m'. intros a0 y. simpl in |- *. elim (sumbool_of_bool (ad_eq a0 (ad_div_2 a))). intro H0. - rewrite H0. rewrite (ad_eq_complete _ _ H0). rewrite (ad_div_2_double a H). - rewrite (ad_eq_correct a). reflexivity. - intro H0. rewrite H0. rewrite (ad_eq_comm (ad_double a0) a). - rewrite (ad_eq_comm a0 (ad_div_2 a)) in H0. rewrite (ad_not_div_2_not_double a a0 H0). + case m'. intros a0 y. simpl in |- *. elim (sumbool_of_bool (Neqb a0 (Ndiv2 a))). intro H0. + rewrite H0. rewrite (Neqb_complete _ _ H0). rewrite (Ndiv2_double a H). + rewrite (Neqb_correct a). reflexivity. + intro H0. rewrite H0. rewrite (Neqb_comm (Ndouble a0) a). + rewrite (Neqb_comm a0 (Ndiv2 a)) in H0. rewrite (Nnot_div2_not_double a a0 H0). reflexivity. intros a0 y0 a1 y1. unfold makeM2 in |- *. rewrite MapGet_M2_bit_0_0. reflexivity. assumption. @@ -576,55 +578,55 @@ Section MapDefs. match m with | M0 => fun _:ad => M0 | M1 a y => - fun a':ad => match ad_eq a a' with + fun a':ad => match Neqb a a' with | true => M0 | false => m end | M2 m1 m2 => fun a:ad => - if ad_bit_0 a - then makeM2 m1 (MapRemove m2 (ad_div_2 a)) - else makeM2 (MapRemove m1 (ad_div_2 a)) m2 + if Nbit0 a + then makeM2 m1 (MapRemove m2 (Ndiv2 a)) + else makeM2 (MapRemove m1 (Ndiv2 a)) m2 end. Lemma MapRemove_semantics : forall (m:Map) (a:ad), eqm (MapGet (MapRemove m a)) - (fun a':ad => if ad_eq a a' then NONE else MapGet m a'). - Proof. - unfold eqm in |- *. simple induction m. simpl in |- *. intros. case (ad_eq a a0); trivial. - intros. simpl in |- *. elim (sumbool_of_bool (ad_eq a1 a2)). intro H. rewrite H. - elim (sumbool_of_bool (ad_eq a a1)). intro H0. rewrite H0. reflexivity. - intro H0. rewrite H0. rewrite (ad_eq_complete _ _ H) in H0. exact (M1_semantics_2 a a2 a0 H0). - intro H. elim (sumbool_of_bool (ad_eq a a1)). intro H0. rewrite H0. rewrite H. - rewrite <- (ad_eq_complete _ _ H0) in H. rewrite H. reflexivity. + (fun a':ad => if Neqb a a' then None else MapGet m a'). + Proof. + unfold eqm in |- *. simple induction m. simpl in |- *. intros. case (Neqb a a0); trivial. + intros. simpl in |- *. elim (sumbool_of_bool (Neqb a1 a2)). intro H. rewrite H. + elim (sumbool_of_bool (Neqb a a1)). intro H0. rewrite H0. reflexivity. + intro H0. rewrite H0. rewrite (Neqb_complete _ _ H) in H0. exact (M1_semantics_2 a a2 a0 H0). + intro H. elim (sumbool_of_bool (Neqb a a1)). intro H0. rewrite H0. rewrite H. + rewrite <- (Neqb_complete _ _ H0) in H. rewrite H. reflexivity. intro H0. rewrite H0. rewrite H. reflexivity. intros. change (MapGet - (if ad_bit_0 a - then makeM2 m0 (MapRemove m1 (ad_div_2 a)) - else makeM2 (MapRemove m0 (ad_div_2 a)) m1) a0 = - (if ad_eq a a0 then NONE else MapGet (M2 m0 m1) a0)) + (if Nbit0 a + then makeM2 m0 (MapRemove m1 (Ndiv2 a)) + else makeM2 (MapRemove m0 (Ndiv2 a)) m1) a0 = + (if Neqb a a0 then None else MapGet (M2 m0 m1) a0)) in |- *. - elim (sumbool_of_bool (ad_bit_0 a)). intro H1. rewrite H1. - rewrite (makeM2_M2 m0 (MapRemove m1 (ad_div_2 a)) a0). elim (sumbool_of_bool (ad_bit_0 a0)). - intro H2. rewrite MapGet_M2_bit_0_1. rewrite (H0 (ad_div_2 a) (ad_div_2 a0)). - elim (sumbool_of_bool (ad_eq a a0)). intro H3. rewrite H3. rewrite (ad_div_eq _ _ H3). + elim (sumbool_of_bool (Nbit0 a)). intro H1. rewrite H1. + rewrite (makeM2_M2 m0 (MapRemove m1 (Ndiv2 a)) a0). elim (sumbool_of_bool (Nbit0 a0)). + intro H2. rewrite MapGet_M2_bit_0_1. rewrite (H0 (Ndiv2 a) (Ndiv2 a0)). + elim (sumbool_of_bool (Neqb a a0)). intro H3. rewrite H3. rewrite (Ndiv2_eq _ _ H3). reflexivity. - intro H3. rewrite H3. rewrite <- H2 in H1. rewrite (ad_div_bit_neq _ _ H3 H1). + intro H3. rewrite H3. rewrite <- H2 in H1. rewrite (Ndiv2_bit_neq _ _ H3 H1). rewrite (MapGet_M2_bit_0_1 a0 H2 m0 m1). reflexivity. assumption. - intro H2. rewrite (MapGet_M2_bit_0_0 a0 H2 m0 (MapRemove m1 (ad_div_2 a))). - rewrite (ad_eq_comm a a0). rewrite (ad_bit_0_neq _ _ H2 H1). + intro H2. rewrite (MapGet_M2_bit_0_0 a0 H2 m0 (MapRemove m1 (Ndiv2 a))). + rewrite (Neqb_comm a a0). rewrite (Nbit0_neq _ _ H2 H1). rewrite (MapGet_M2_bit_0_0 a0 H2 m0 m1). reflexivity. - intro H1. rewrite H1. rewrite (makeM2_M2 (MapRemove m0 (ad_div_2 a)) m1 a0). - elim (sumbool_of_bool (ad_bit_0 a0)). intro H2. rewrite MapGet_M2_bit_0_1. - rewrite (MapGet_M2_bit_0_1 a0 H2 m0 m1). rewrite (ad_bit_0_neq a a0 H1 H2). reflexivity. + intro H1. rewrite H1. rewrite (makeM2_M2 (MapRemove m0 (Ndiv2 a)) m1 a0). + elim (sumbool_of_bool (Nbit0 a0)). intro H2. rewrite MapGet_M2_bit_0_1. + rewrite (MapGet_M2_bit_0_1 a0 H2 m0 m1). rewrite (Nbit0_neq a a0 H1 H2). reflexivity. assumption. - intro H2. rewrite MapGet_M2_bit_0_0. rewrite (H (ad_div_2 a) (ad_div_2 a0)). - rewrite (MapGet_M2_bit_0_0 a0 H2 m0 m1). elim (sumbool_of_bool (ad_eq a a0)). intro H3. - rewrite H3. rewrite (ad_div_eq _ _ H3). reflexivity. - intro H3. rewrite H3. rewrite <- H2 in H1. rewrite (ad_div_bit_neq _ _ H3 H1). reflexivity. + intro H2. rewrite MapGet_M2_bit_0_0. rewrite (H (Ndiv2 a) (Ndiv2 a0)). + rewrite (MapGet_M2_bit_0_0 a0 H2 m0 m1). elim (sumbool_of_bool (Neqb a a0)). intro H3. + rewrite H3. rewrite (Ndiv2_eq _ _ H3). reflexivity. + intro H3. rewrite H3. rewrite <- H2 in H1. rewrite (Ndiv2_bit_neq _ _ H3 H1). reflexivity. assumption. Qed. @@ -653,21 +655,21 @@ Section MapDefs. eqm (MapGet (MapMerge m m')) (fun a0:ad => match MapGet m' a0 with - | SOME y' => SOME y' - | NONE => MapGet m a0 + | Some y' => Some y' + | None => MapGet m a0 end). Proof. unfold eqm in |- *. simple induction m. intros. simpl in |- *. case (MapGet m' a); trivial. intros. simpl in |- *. rewrite (MapPut_behind_semantics m' a a0 a1). reflexivity. simple induction m'. trivial. intros. unfold MapMerge in |- *. rewrite (MapPut_semantics (M2 m0 m1) a a0 a1). - elim (sumbool_of_bool (ad_eq a a1)). intro H1. rewrite H1. rewrite (ad_eq_complete _ _ H1). + elim (sumbool_of_bool (Neqb a a1)). intro H1. rewrite H1. rewrite (Neqb_complete _ _ H1). rewrite (M1_semantics_1 a1 a0). reflexivity. intro H1. rewrite H1. rewrite (M1_semantics_2 a a1 a0 H1). reflexivity. intros. cut (MapMerge (M2 m0 m1) (M2 m2 m3) = M2 (MapMerge m0 m2) (MapMerge m1 m3)). - intro. rewrite H3. rewrite MapGet_M2_bit_0_if. rewrite (H0 m3 (ad_div_2 a)). - rewrite (H m2 (ad_div_2 a)). rewrite (MapGet_M2_bit_0_if m2 m3 a). - rewrite (MapGet_M2_bit_0_if m0 m1 a). case (ad_bit_0 a); trivial. + intro. rewrite H3. rewrite MapGet_M2_bit_0_if. rewrite (H0 m3 (Ndiv2 a)). + rewrite (H m2 (Ndiv2 a)). rewrite (MapGet_M2_bit_0_if m2 m3 a). + rewrite (MapGet_M2_bit_0_if m0 m1 a). case (Nbit0 a); trivial. reflexivity. Qed. @@ -680,7 +682,7 @@ Section MapDefs. | M1 a y => fun m':Map => match MapGet m' a with - | NONE => MapPut m' a y + | None => MapPut m' a y | _ => MapRemove m' a end | M2 m1 m2 => @@ -689,7 +691,7 @@ Section MapDefs. | M0 => m | M1 a' y' => match MapGet m a' with - | NONE => MapPut m a' y' + | None => MapPut m a' y' | _ => MapRemove m a' end | M2 m'1 m'2 => makeM2 (MapDelta m1 m'1) (MapDelta m2 m'2) @@ -701,17 +703,17 @@ Section MapDefs. Proof. unfold eqm in |- *. simple induction m. simple induction m'; reflexivity. simple induction m'. reflexivity. - unfold MapDelta in |- *. intros. elim (sumbool_of_bool (ad_eq a a1)). intro H. - rewrite <- (ad_eq_complete _ _ H). rewrite (M1_semantics_1 a a2). - rewrite (M1_semantics_1 a a0). simpl in |- *. rewrite (ad_eq_correct a). reflexivity. - intro H. rewrite (M1_semantics_2 a a1 a0 H). rewrite (ad_eq_comm a a1) in H. + unfold MapDelta in |- *. intros. elim (sumbool_of_bool (Neqb a a1)). intro H. + rewrite <- (Neqb_complete _ _ H). rewrite (M1_semantics_1 a a2). + rewrite (M1_semantics_1 a a0). simpl in |- *. rewrite (Neqb_correct a). reflexivity. + intro H. rewrite (M1_semantics_2 a a1 a0 H). rewrite (Neqb_comm a a1) in H. rewrite (M1_semantics_2 a1 a a2 H). rewrite (MapPut_semantics (M1 a a0) a1 a2 a3). - rewrite (MapPut_semantics (M1 a1 a2) a a0 a3). elim (sumbool_of_bool (ad_eq a a3)). - intro H0. rewrite H0. rewrite (ad_eq_complete _ _ H0) in H. rewrite H. - rewrite (ad_eq_complete _ _ H0). rewrite (M1_semantics_1 a3 a0). reflexivity. + rewrite (MapPut_semantics (M1 a1 a2) a a0 a3). elim (sumbool_of_bool (Neqb a a3)). + intro H0. rewrite H0. rewrite (Neqb_complete _ _ H0) in H. rewrite H. + rewrite (Neqb_complete _ _ H0). rewrite (M1_semantics_1 a3 a0). reflexivity. intro H0. rewrite H0. rewrite (M1_semantics_2 a a3 a0 H0). - elim (sumbool_of_bool (ad_eq a1 a3)). intro H1. rewrite H1. - rewrite (ad_eq_complete _ _ H1). exact (M1_semantics_1 a3 a2). + elim (sumbool_of_bool (Neqb a1 a3)). intro H1. rewrite H1. + rewrite (Neqb_complete _ _ H1). exact (M1_semantics_1 a3 a2). intro H1. rewrite H1. exact (M1_semantics_2 a1 a3 a2 H1). intros. reflexivity. simple induction m'. reflexivity. @@ -720,24 +722,25 @@ Section MapDefs. rewrite (makeM2_M2 (MapDelta m2 m0) (MapDelta m3 m1) a). rewrite (MapGet_M2_bit_0_if (MapDelta m0 m2) (MapDelta m1 m3) a). rewrite (MapGet_M2_bit_0_if (MapDelta m2 m0) (MapDelta m3 m1) a). - rewrite (H0 m3 (ad_div_2 a)). rewrite (H m2 (ad_div_2 a)). reflexivity. + rewrite (H0 m3 (Ndiv2 a)). rewrite (H m2 (Ndiv2 a)). reflexivity. Qed. Lemma MapDelta_semantics_1_1 : forall (a:ad) (y:A) (m':Map) (a0:ad), - MapGet (M1 a y) a0 = NONE -> - MapGet m' a0 = NONE -> MapGet (MapDelta (M1 a y) m') a0 = NONE. + MapGet (M1 a y) a0 = None -> + MapGet m' a0 = None -> MapGet (MapDelta (M1 a y) m') a0 = None. Proof. - intros. unfold MapDelta in |- *. elim (sumbool_of_bool (ad_eq a a0)). intro H1. - rewrite (ad_eq_complete _ _ H1) in H. rewrite (M1_semantics_1 a0 y) in H. discriminate H. - intro H1. case (MapGet m' a). rewrite (MapPut_semantics m' a y a0). rewrite H1. assumption. + intros. unfold MapDelta in |- *. elim (sumbool_of_bool (Neqb a a0)). intro H1. + rewrite (Neqb_complete _ _ H1) in H. rewrite (M1_semantics_1 a0 y) in H. discriminate H. + intro H1. case (MapGet m' a). rewrite (MapRemove_semantics m' a a0). rewrite H1. trivial. + rewrite (MapPut_semantics m' a y a0). rewrite H1. assumption. Qed. Lemma MapDelta_semantics_1 : forall (m m':Map) (a:ad), - MapGet m a = NONE -> - MapGet m' a = NONE -> MapGet (MapDelta m m') a = NONE. + MapGet m a = None -> + MapGet m' a = None -> MapGet (MapDelta m m') a = None. Proof. simple induction m. trivial. exact MapDelta_semantics_1_1. @@ -745,7 +748,7 @@ Section MapDefs. intros. rewrite (MapDelta_semantics_comm (M2 m0 m1) (M1 a a0) a1). apply MapDelta_semantics_1_1; trivial. intros. simpl in |- *. rewrite (makeM2_M2 (MapDelta m0 m2) (MapDelta m1 m3) a). - rewrite MapGet_M2_bit_0_if. elim (sumbool_of_bool (ad_bit_0 a)). intro H5. rewrite H5. + rewrite MapGet_M2_bit_0_if. elim (sumbool_of_bool (Nbit0 a)). intro H5. rewrite H5. apply H0. rewrite (MapGet_M2_bit_0_1 a H5 m0 m1) in H3. exact H3. rewrite (MapGet_M2_bit_0_1 a H5 m2 m3) in H4. exact H4. intro H5. rewrite H5. apply H. rewrite (MapGet_M2_bit_0_0 a H5 m0 m1) in H3. exact H3. @@ -754,31 +757,32 @@ Section MapDefs. Lemma MapDelta_semantics_2_1 : forall (a:ad) (y:A) (m':Map) (a0:ad) (y0:A), - MapGet (M1 a y) a0 = NONE -> - MapGet m' a0 = SOME y0 -> MapGet (MapDelta (M1 a y) m') a0 = SOME y0. + MapGet (M1 a y) a0 = None -> + MapGet m' a0 = Some y0 -> MapGet (MapDelta (M1 a y) m') a0 = Some y0. Proof. - intros. unfold MapDelta in |- *. elim (sumbool_of_bool (ad_eq a a0)). intro H1. - rewrite (ad_eq_complete _ _ H1) in H. rewrite (M1_semantics_1 a0 y) in H. discriminate H. - intro H1. case (MapGet m' a). rewrite (MapPut_semantics m' a y a0). rewrite H1. assumption. + intros. unfold MapDelta in |- *. elim (sumbool_of_bool (Neqb a a0)). intro H1. + rewrite (Neqb_complete _ _ H1) in H. rewrite (M1_semantics_1 a0 y) in H. discriminate H. + intro H1. case (MapGet m' a). rewrite (MapRemove_semantics m' a a0). rewrite H1. trivial. + rewrite (MapPut_semantics m' a y a0). rewrite H1. assumption. Qed. Lemma MapDelta_semantics_2_2 : forall (a:ad) (y:A) (m':Map) (a0:ad) (y0:A), - MapGet (M1 a y) a0 = SOME y0 -> - MapGet m' a0 = NONE -> MapGet (MapDelta (M1 a y) m') a0 = SOME y0. + MapGet (M1 a y) a0 = Some y0 -> + MapGet m' a0 = None -> MapGet (MapDelta (M1 a y) m') a0 = Some y0. Proof. - intros. unfold MapDelta in |- *. elim (sumbool_of_bool (ad_eq a a0)). intro H1. - rewrite (ad_eq_complete _ _ H1) in H. rewrite (ad_eq_complete _ _ H1). - rewrite H0. rewrite (MapPut_semantics m' a0 y a0). rewrite (ad_eq_correct a0). + intros. unfold MapDelta in |- *. elim (sumbool_of_bool (Neqb a a0)). intro H1. + rewrite (Neqb_complete _ _ H1) in H. rewrite (Neqb_complete _ _ H1). + rewrite H0. rewrite (MapPut_semantics m' a0 y a0). rewrite (Neqb_correct a0). rewrite (M1_semantics_1 a0 y) in H. simple inversion H. assumption. intro H1. rewrite (M1_semantics_2 a a0 y H1) in H. discriminate H. Qed. Lemma MapDelta_semantics_2 : forall (m m':Map) (a:ad) (y:A), - MapGet m a = NONE -> - MapGet m' a = SOME y -> MapGet (MapDelta m m') a = SOME y. + MapGet m a = None -> + MapGet m' a = Some y -> MapGet (MapDelta m m') a = Some y. Proof. simple induction m. trivial. exact MapDelta_semantics_2_1. @@ -786,7 +790,7 @@ Section MapDefs. intros. rewrite (MapDelta_semantics_comm (M2 m0 m1) (M1 a a0) a1). apply MapDelta_semantics_2_2; assumption. intros. simpl in |- *. rewrite (makeM2_M2 (MapDelta m0 m2) (MapDelta m1 m3) a). - rewrite MapGet_M2_bit_0_if. elim (sumbool_of_bool (ad_bit_0 a)). intro H5. rewrite H5. + rewrite MapGet_M2_bit_0_if. elim (sumbool_of_bool (Nbit0 a)). intro H5. rewrite H5. apply H0. rewrite <- (MapGet_M2_bit_0_1 a H5 m0 m1). assumption. rewrite <- (MapGet_M2_bit_0_1 a H5 m2 m3). assumption. intro H5. rewrite H5. apply H. rewrite <- (MapGet_M2_bit_0_0 a H5 m0 m1). assumption. @@ -795,19 +799,19 @@ Section MapDefs. Lemma MapDelta_semantics_3_1 : forall (a0:ad) (y0:A) (m':Map) (a:ad) (y y':A), - MapGet (M1 a0 y0) a = SOME y -> - MapGet m' a = SOME y' -> MapGet (MapDelta (M1 a0 y0) m') a = NONE. + MapGet (M1 a0 y0) a = Some y -> + MapGet m' a = Some y' -> MapGet (MapDelta (M1 a0 y0) m') a = None. Proof. - intros. unfold MapDelta in |- *. elim (sumbool_of_bool (ad_eq a0 a)). intro H1. - rewrite (ad_eq_complete a0 a H1). rewrite H0. rewrite (MapRemove_semantics m' a a). - rewrite (ad_eq_correct a). reflexivity. + intros. unfold MapDelta in |- *. elim (sumbool_of_bool (Neqb a0 a)). intro H1. + rewrite (Neqb_complete a0 a H1). rewrite H0. rewrite (MapRemove_semantics m' a a). + rewrite (Neqb_correct a). reflexivity. intro H1. rewrite (M1_semantics_2 a0 a y0 H1) in H. discriminate H. Qed. Lemma MapDelta_semantics_3 : forall (m m':Map) (a:ad) (y y':A), - MapGet m a = SOME y -> - MapGet m' a = SOME y' -> MapGet (MapDelta m m') a = NONE. + MapGet m a = Some y -> + MapGet m' a = Some y' -> MapGet (MapDelta m m') a = None. Proof. simple induction m. intros. discriminate H. exact MapDelta_semantics_3_1. @@ -815,10 +819,10 @@ Section MapDefs. intros. rewrite (MapDelta_semantics_comm (M2 m0 m1) (M1 a a0) a1). exact (MapDelta_semantics_3_1 a a0 (M2 m0 m1) a1 y' y H2 H1). intros. simpl in |- *. rewrite (makeM2_M2 (MapDelta m0 m2) (MapDelta m1 m3) a). - rewrite MapGet_M2_bit_0_if. elim (sumbool_of_bool (ad_bit_0 a)). intro H5. rewrite H5. - apply (H0 m3 (ad_div_2 a) y y'). rewrite <- (MapGet_M2_bit_0_1 a H5 m0 m1). assumption. + rewrite MapGet_M2_bit_0_if. elim (sumbool_of_bool (Nbit0 a)). intro H5. rewrite H5. + apply (H0 m3 (Ndiv2 a) y y'). rewrite <- (MapGet_M2_bit_0_1 a H5 m0 m1). assumption. rewrite <- (MapGet_M2_bit_0_1 a H5 m2 m3). assumption. - intro H5. rewrite H5. apply (H m2 (ad_div_2 a) y y'). + intro H5. rewrite H5. apply (H m2 (Ndiv2 a) y y'). rewrite <- (MapGet_M2_bit_0_0 a H5 m0 m1). assumption. rewrite <- (MapGet_M2_bit_0_0 a H5 m2 m3). assumption. Qed. @@ -828,9 +832,9 @@ Section MapDefs. eqm (MapGet (MapDelta m m')) (fun a0:ad => match MapGet m a0, MapGet m' a0 with - | NONE, SOME y' => SOME y' - | SOME y, NONE => SOME y - | _, _ => NONE + | None, Some y' => Some y' + | Some y, None => Some y + | _, _ => None end). Proof. unfold eqm in |- *. intros. elim (option_sum (MapGet m' a)). intro H. elim H. intros a0 H0. diff --git a/theories/IntMap/Mapaxioms.v b/theories/IntMap/Mapaxioms.v index b6a2b134..0722bcfa 100644 --- a/theories/IntMap/Mapaxioms.v +++ b/theories/IntMap/Mapaxioms.v @@ -5,14 +5,13 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Mapaxioms.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Mapaxioms.v 8733 2006-04-25 22:52:18Z letouzey $ i*) Require Import Bool. Require Import Sumbool. -Require Import ZArith. -Require Import Addr. -Require Import Adist. -Require Import Addec. +Require Import NArith. +Require Import Ndigits. +Require Import Ndec. Require Import Map. Require Import Fset. @@ -59,8 +58,8 @@ Section MapAxioms. eqmap (MapPut A m a y) (MapMerge A m (M1 A a y)). Proof. unfold eqmap, eqm in |- *. intros. rewrite (MapPut_semantics A m a y a0). - rewrite (MapMerge_semantics A m (M1 A a y) a0). unfold MapGet at 2 in |- *. - elim (sumbool_of_bool (ad_eq a a0)); intro H; rewrite H; reflexivity. + rewrite (MapMerge_semantics A m (M1 A a y) a0). unfold MapGet at 2. + elim (sumbool_of_bool (Neqb a a0)); intro H; rewrite H; reflexivity. Qed. Lemma MapPut_ext : @@ -70,7 +69,7 @@ Section MapAxioms. Proof. unfold eqmap, eqm in |- *. intros. rewrite (MapPut_semantics A m' a y a0). rewrite (MapPut_semantics A m a y a0). - case (ad_eq a a0); [ reflexivity | apply H ]. + case (Neqb a a0); [ reflexivity | apply H ]. Qed. Lemma MapPut_behind_as_Merge : @@ -115,7 +114,7 @@ Section MapAxioms. forall m m':Map A, eqmap (MapMerge A m m') (M0 A) -> eqmap m (M0 A). Proof. unfold eqmap, eqm in |- *. intros. cut (MapGet A (MapMerge A m m') a = MapGet A (M0 A) a). - rewrite (MapMerge_semantics A m m' a). case (MapGet A m' a). trivial. + rewrite (MapMerge_semantics A m m' a). case (MapGet A m' a); trivial. intros. discriminate H0. exact (H a). Qed. @@ -124,8 +123,7 @@ Section MapAxioms. forall m m':Map A, eqmap (MapMerge A m m') (M0 A) -> eqmap m' (M0 A). Proof. unfold eqmap, eqm in |- *. intros. cut (MapGet A (MapMerge A m m') a = MapGet A (M0 A) a). - rewrite (MapMerge_semantics A m m' a). case (MapGet A m' a). trivial. - intros. discriminate H0. + rewrite (MapMerge_semantics A m m' a). case (MapGet A m' a); trivial. exact (H a). Qed. @@ -190,8 +188,8 @@ Section MapAxioms. eqmap (MapRemove A m a) (MapDomRestrBy A B m (M1 B a y)). Proof. unfold eqmap, eqm in |- *. intros. rewrite (MapRemove_semantics A m a a0). - rewrite (MapDomRestrBy_semantics A B m (M1 B a y) a0). elim (sumbool_of_bool (ad_eq a a0)). - intro H. rewrite H. rewrite (ad_eq_complete a a0 H). rewrite (M1_semantics_1 B a0 y). + rewrite (MapDomRestrBy_semantics A B m (M1 B a y) a0). elim (sumbool_of_bool (Neqb a a0)). + intro H. rewrite H. rewrite (Neqb_complete a a0 H). rewrite (M1_semantics_1 B a0 y). reflexivity. intro H. rewrite H. rewrite (M1_semantics_2 B a a0 y H). reflexivity. Qed. @@ -202,7 +200,7 @@ Section MapAxioms. Proof. unfold eqmap, eqm in |- *. intros. rewrite (MapRemove_semantics A m' a a0). rewrite (MapRemove_semantics A m a a0). - case (ad_eq a a0); [ reflexivity | apply H ]. + case (Neqb a a0); [ reflexivity | apply H ]. Qed. Lemma MapDomRestrTo_empty_m_1 : @@ -259,7 +257,7 @@ Section MapAxioms. elim (MapDom_semantics_2 B m' a H). intros y H0. rewrite H0. unfold in_FSet, in_dom in H. generalize H. case (MapGet unit (MapDom B m') a); trivial. intro H1. discriminate H1. intro H. rewrite (MapDom_semantics_4 B m' a H). unfold in_FSet, in_dom in H. - generalize H. case (MapGet unit (MapDom B m') a). trivial. + generalize H. case (MapGet unit (MapDom B m') a); trivial. intros H0 H1. discriminate H1. Qed. @@ -298,7 +296,7 @@ Section MapAxioms. unfold in_FSet, in_dom in H. generalize H. case (MapGet unit (MapDom B m') a); trivial. intro H1. discriminate H1. intro H. rewrite (MapDom_semantics_4 B m' a H). unfold in_FSet, in_dom in H. - generalize H. case (MapGet unit (MapDom B m') a). trivial. + generalize H. case (MapGet unit (MapDom B m') a); trivial. intros H0 H1. discriminate H1. Qed. diff --git a/theories/IntMap/Mapc.v b/theories/IntMap/Mapc.v index d7a779ff..163373bf 100644 --- a/theories/IntMap/Mapc.v +++ b/theories/IntMap/Mapc.v @@ -5,15 +5,12 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Mapc.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Mapc.v 8733 2006-04-25 22:52:18Z letouzey $ i*) Require Import Bool. Require Import Sumbool. Require Import Arith. -Require Import ZArith. -Require Import Addr. -Require Import Adist. -Require Import Addec. +Require Import NArith. Require Import Map. Require Import Mapaxioms. Require Import Fset. diff --git a/theories/IntMap/Mapcanon.v b/theories/IntMap/Mapcanon.v index 23e0669e..33741b98 100644 --- a/theories/IntMap/Mapcanon.v +++ b/theories/IntMap/Mapcanon.v @@ -5,15 +5,14 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Mapcanon.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Mapcanon.v 8733 2006-04-25 22:52:18Z letouzey $ i*) Require Import Bool. Require Import Sumbool. Require Import Arith. -Require Import ZArith. -Require Import Addr. -Require Import Adist. -Require Import Addec. +Require Import NArith. +Require Import Ndigits. +Require Import Ndec. Require Import Map. Require Import Mapaxioms. Require Import Mapiter. @@ -57,37 +56,37 @@ Section MapCanon. forall m0 m1 m2 m3:Map A, eqmap A (M2 A m0 m1) (M2 A m2 m3) -> eqmap A m0 m2. Proof. - unfold eqmap, eqm in |- *. intros. rewrite <- (ad_double_div_2 a). - rewrite <- (MapGet_M2_bit_0_0 A _ (ad_double_bit_0 a) m0 m1). - rewrite <- (MapGet_M2_bit_0_0 A _ (ad_double_bit_0 a) m2 m3). - exact (H (ad_double a)). + unfold eqmap, eqm in |- *. intros. rewrite <- (Ndouble_div2 a). + rewrite <- (MapGet_M2_bit_0_0 A _ (Ndouble_bit0 a) m0 m1). + rewrite <- (MapGet_M2_bit_0_0 A _ (Ndouble_bit0 a) m2 m3). + exact (H (Ndouble a)). Qed. Lemma M2_eqmap_2 : forall m0 m1 m2 m3:Map A, eqmap A (M2 A m0 m1) (M2 A m2 m3) -> eqmap A m1 m3. Proof. - unfold eqmap, eqm in |- *. intros. rewrite <- (ad_double_plus_un_div_2 a). - rewrite <- (MapGet_M2_bit_0_1 A _ (ad_double_plus_un_bit_0 a) m0 m1). - rewrite <- (MapGet_M2_bit_0_1 A _ (ad_double_plus_un_bit_0 a) m2 m3). - exact (H (ad_double_plus_un a)). + unfold eqmap, eqm in |- *. intros. rewrite <- (Ndouble_plus_one_div2 a). + rewrite <- (MapGet_M2_bit_0_1 A _ (Ndouble_plus_one_bit0 a) m0 m1). + rewrite <- (MapGet_M2_bit_0_1 A _ (Ndouble_plus_one_bit0 a) m2 m3). + exact (H (Ndouble_plus_one a)). Qed. Lemma mapcanon_unique : forall m m':Map A, mapcanon m -> mapcanon m' -> eqmap A m m' -> m = m'. Proof. simple induction m. simple induction m'. trivial. - intros a y H H0 H1. cut (NONE A = MapGet A (M1 A a y) a). simpl in |- *. rewrite (ad_eq_correct a). + intros a y H H0 H1. cut (None = MapGet A (M1 A a y) a). simpl in |- *. rewrite (Neqb_correct a). intro. discriminate H2. exact (H1 a). intros. cut (2 <= MapCard A (M0 A)). intro. elim (le_Sn_O _ H4). rewrite (MapCard_ext A _ _ H3). exact (mapcanon_M2 _ _ H2). - intros a y. simple induction m'. intros. cut (MapGet A (M1 A a y) a = NONE A). simpl in |- *. - rewrite (ad_eq_correct a). intro. discriminate H2. + intros a y. simple induction m'. intros. cut (MapGet A (M1 A a y) a = None). simpl in |- *. + rewrite (Neqb_correct a). intro. discriminate H2. exact (H1 a). intros a0 y0 H H0 H1. cut (MapGet A (M1 A a y) a = MapGet A (M1 A a0 y0) a). simpl in |- *. - rewrite (ad_eq_correct a). intro. elim (sumbool_of_bool (ad_eq a0 a)). intro H3. - rewrite H3 in H2. inversion H2. rewrite (ad_eq_complete _ _ H3). reflexivity. + rewrite (Neqb_correct a). intro. elim (sumbool_of_bool (Neqb a0 a)). intro H3. + rewrite H3 in H2. inversion H2. rewrite (Neqb_complete _ _ H3). reflexivity. intro H3. rewrite H3 in H2. discriminate H2. exact (H1 a). intros. cut (2 <= MapCard A (M1 A a y)). intro. elim (le_Sn_O _ (le_S_n _ _ H4)). @@ -109,19 +108,19 @@ Section MapCanon. Lemma MapPut1_canon : forall (p:positive) (a a':ad) (y y':A), mapcanon (MapPut1 A a y a' y' p). Proof. - simple induction p. simpl in |- *. intros. case (ad_bit_0 a). apply M2_canon. apply M1_canon. + simple induction p. simpl in |- *. intros. case (Nbit0 a). apply M2_canon. apply M1_canon. apply M1_canon. apply le_n. apply M2_canon. apply M1_canon. apply M1_canon. apply le_n. - simpl in |- *. intros. case (ad_bit_0 a). apply M2_canon. apply M0_canon. + simpl in |- *. intros. case (Nbit0 a). apply M2_canon. apply M0_canon. apply H. simpl in |- *. rewrite MapCard_Put1_equals_2. apply le_n. apply M2_canon. apply H. apply M0_canon. simpl in |- *. rewrite MapCard_Put1_equals_2. apply le_n. - simpl in |- *. simpl in |- *. intros. case (ad_bit_0 a). apply M2_canon. apply M1_canon. + simpl in |- *. simpl in |- *. intros. case (Nbit0 a). apply M2_canon. apply M1_canon. apply M1_canon. simpl in |- *. apply le_n. apply M2_canon. apply M1_canon. @@ -134,28 +133,28 @@ Section MapCanon. mapcanon m -> forall (a:ad) (y:A), mapcanon (MapPut A m a y). Proof. simple induction m. intros. simpl in |- *. apply M1_canon. - intros a0 y0 H a y. simpl in |- *. case (ad_xor a0 a). apply M1_canon. + intros a0 y0 H a y. simpl in |- *. case (Nxor a0 a). apply M1_canon. intro. apply MapPut1_canon. intros. simpl in |- *. elim a. apply M2_canon. apply H. exact (mapcanon_M2_1 m0 m1 H1). exact (mapcanon_M2_2 m0 m1 H1). simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). exact (mapcanon_M2 _ _ H1). - apply plus_le_compat. exact (MapCard_Put_lb A m0 ad_z y). + apply plus_le_compat. exact (MapCard_Put_lb A m0 N0 y). apply le_n. intro. case p. intro. apply M2_canon. exact (mapcanon_M2_1 m0 m1 H1). apply H0. exact (mapcanon_M2_2 m0 m1 H1). simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). exact (mapcanon_M2 m0 m1 H1). - apply plus_le_compat_l. exact (MapCard_Put_lb A m1 (ad_x p0) y). + apply plus_le_compat_l. exact (MapCard_Put_lb A m1 (Npos p0) y). intro. apply M2_canon. apply H. exact (mapcanon_M2_1 m0 m1 H1). exact (mapcanon_M2_2 m0 m1 H1). simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). exact (mapcanon_M2 m0 m1 H1). - apply plus_le_compat_r. exact (MapCard_Put_lb A m0 (ad_x p0) y). + apply plus_le_compat_r. exact (MapCard_Put_lb A m0 (Npos p0) y). apply M2_canon. apply (mapcanon_M2_1 m0 m1 H1). apply H0. apply (mapcanon_M2_2 m0 m1 H1). simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). exact (mapcanon_M2 m0 m1 H1). - apply plus_le_compat_l. exact (MapCard_Put_lb A m1 ad_z y). + apply plus_le_compat_l. exact (MapCard_Put_lb A m1 N0 y). Qed. Lemma MapPut_behind_canon : @@ -163,37 +162,37 @@ Section MapCanon. mapcanon m -> forall (a:ad) (y:A), mapcanon (MapPut_behind A m a y). Proof. simple induction m. intros. simpl in |- *. apply M1_canon. - intros a0 y0 H a y. simpl in |- *. case (ad_xor a0 a). apply M1_canon. + intros a0 y0 H a y. simpl in |- *. case (Nxor a0 a). apply M1_canon. intro. apply MapPut1_canon. intros. simpl in |- *. elim a. apply M2_canon. apply H. exact (mapcanon_M2_1 m0 m1 H1). exact (mapcanon_M2_2 m0 m1 H1). simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). exact (mapcanon_M2 _ _ H1). - apply plus_le_compat. rewrite MapCard_Put_behind_Put. exact (MapCard_Put_lb A m0 ad_z y). + apply plus_le_compat. rewrite MapCard_Put_behind_Put. exact (MapCard_Put_lb A m0 N0 y). apply le_n. intro. case p. intro. apply M2_canon. exact (mapcanon_M2_1 m0 m1 H1). apply H0. exact (mapcanon_M2_2 m0 m1 H1). simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). exact (mapcanon_M2 m0 m1 H1). - apply plus_le_compat_l. rewrite MapCard_Put_behind_Put. exact (MapCard_Put_lb A m1 (ad_x p0) y). + apply plus_le_compat_l. rewrite MapCard_Put_behind_Put. exact (MapCard_Put_lb A m1 (Npos p0) y). intro. apply M2_canon. apply H. exact (mapcanon_M2_1 m0 m1 H1). exact (mapcanon_M2_2 m0 m1 H1). simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). exact (mapcanon_M2 m0 m1 H1). - apply plus_le_compat_r. rewrite MapCard_Put_behind_Put. exact (MapCard_Put_lb A m0 (ad_x p0) y). + apply plus_le_compat_r. rewrite MapCard_Put_behind_Put. exact (MapCard_Put_lb A m0 (Npos p0) y). apply M2_canon. apply (mapcanon_M2_1 m0 m1 H1). apply H0. apply (mapcanon_M2_2 m0 m1 H1). simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). exact (mapcanon_M2 m0 m1 H1). - apply plus_le_compat_l. rewrite MapCard_Put_behind_Put. exact (MapCard_Put_lb A m1 ad_z y). + apply plus_le_compat_l. rewrite MapCard_Put_behind_Put. exact (MapCard_Put_lb A m1 N0 y). Qed. Lemma makeM2_canon : forall m m':Map A, mapcanon m -> mapcanon m' -> mapcanon (makeM2 A m m'). Proof. intro. case m. intro. case m'. intros. exact M0_canon. - intros a y H H0. exact (M1_canon (ad_double_plus_un a) y). + intros a y H H0. exact (M1_canon (Ndouble_plus_one a) y). intros. simpl in |- *. apply M2_canon; try assumption. exact (mapcanon_M2 m0 m1 H0). - intros a y m'. case m'. intros. exact (M1_canon (ad_double a) y). + intros a y m'. case m'. intros. exact (M1_canon (Ndouble a) y). intros a0 y0 H H0. simpl in |- *. apply M2_canon; try assumption. apply le_n. intros. simpl in |- *. apply M2_canon; try assumption. apply le_trans with (m := MapCard A (M2 A m0 m1)). exact (mapcanon_M2 _ _ H0). @@ -216,7 +215,7 @@ Section MapCanon. intros. simpl in |- *. unfold eqmap, eqm in |- *. intro. rewrite (makeM2_M2 A (MapCanonicalize m0) (MapCanonicalize m1) a). rewrite MapGet_M2_bit_0_if. rewrite MapGet_M2_bit_0_if. - rewrite <- (H (ad_div_2 a)). rewrite <- (H0 (ad_div_2 a)). reflexivity. + rewrite <- (H (Ndiv2 a)). rewrite <- (H0 (Ndiv2 a)). reflexivity. Qed. Lemma mapcanon_exists_2 : forall m:Map A, mapcanon (MapCanonicalize m). @@ -237,9 +236,9 @@ Section MapCanon. forall m:Map A, mapcanon m -> forall a:ad, mapcanon (MapRemove A m a). Proof. simple induction m. intros. exact M0_canon. - intros a y H a0. simpl in |- *. case (ad_eq a a0). exact M0_canon. + intros a y H a0. simpl in |- *. case (Neqb a a0). exact M0_canon. assumption. - intros. simpl in |- *. case (ad_bit_0 a). apply makeM2_canon. exact (mapcanon_M2_1 _ _ H1). + intros. simpl in |- *. case (Nbit0 a). apply makeM2_canon. exact (mapcanon_M2_1 _ _ H1). apply H0. exact (mapcanon_M2_2 _ _ H1). apply makeM2_canon. apply H. exact (mapcanon_M2_1 _ _ H1). exact (mapcanon_M2_2 _ _ H1). @@ -265,12 +264,13 @@ Section MapCanon. forall m m':Map A, mapcanon m -> mapcanon m' -> mapcanon (MapDelta A m m'). Proof. simple induction m. intros. exact H0. - simpl in |- *. intros a y m' H H0. case (MapGet A m' a). exact (MapPut_canon m' H0 a y). + simpl in |- *. intros a y m' H H0. case (MapGet A m' a). intro. exact (MapRemove_canon m' H0 a). + exact (MapPut_canon m' H0 a y). simple induction m'. intros. exact H1. - unfold MapDelta in |- *. intros a y H1 H2. case (MapGet A (M2 A m0 m1) a). - exact (MapPut_canon _ H1 a y). + unfold MapDelta in |- *. intros a y H1 H2. case (MapGet A (M2 A m0 m1) a). intro. exact (MapRemove_canon _ H1 a). + exact (MapPut_canon _ H1 a y). intros. simpl in |- *. apply makeM2_canon. apply H. exact (mapcanon_M2_1 _ _ H3). exact (mapcanon_M2_1 _ _ H4). apply H0. exact (mapcanon_M2_2 _ _ H3). @@ -284,11 +284,13 @@ Section MapCanon. mapcanon m -> forall m':Map B, mapcanon (MapDomRestrTo A B m m'). Proof. simple induction m. intros. exact M0_canon. - simpl in |- *. intros a y H m'. case (MapGet B m' a). exact M0_canon. + simpl in |- *. intros a y H m'. case (MapGet B m' a). intro. apply M1_canon. + exact M0_canon. simple induction m'. exact M0_canon. - unfold MapDomRestrTo in |- *. intros a y. case (MapGet A (M2 A m0 m1) a). exact M0_canon. + unfold MapDomRestrTo in |- *. intros a y. case (MapGet A (M2 A m0 m1) a). intro. apply M1_canon. + exact M0_canon. intros. simpl in |- *. apply makeM2_canon. apply H. exact (mapcanon_M2_1 m0 m1 H1). apply H0. exact (mapcanon_M2_2 m0 m1 H1). Qed. @@ -298,10 +300,10 @@ Section MapCanon. mapcanon m -> forall m':Map B, mapcanon (MapDomRestrBy A B m m'). Proof. simple induction m. intros. exact M0_canon. - simpl in |- *. intros a y H m'. case (MapGet B m' a). assumption. + simpl in |- *. intros a y H m'. case (MapGet B m' a); try assumption. intro. exact M0_canon. simple induction m'. exact H1. - intros a y. simpl in |- *. case (ad_bit_0 a). apply makeM2_canon. exact (mapcanon_M2_1 _ _ H1). + intros a y. simpl in |- *. case (Nbit0 a). apply makeM2_canon. exact (mapcanon_M2_1 _ _ H1). apply MapRemove_canon. exact (mapcanon_M2_2 _ _ H1). apply makeM2_canon. apply MapRemove_canon. exact (mapcanon_M2_1 _ _ H1). exact (mapcanon_M2_2 _ _ H1). diff --git a/theories/IntMap/Mapcard.v b/theories/IntMap/Mapcard.v index 35efac47..36be9bf9 100644 --- a/theories/IntMap/Mapcard.v +++ b/theories/IntMap/Mapcard.v @@ -5,15 +5,14 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Mapcard.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Mapcard.v 8733 2006-04-25 22:52:18Z letouzey $ i*) Require Import Bool. Require Import Sumbool. Require Import Arith. -Require Import ZArith. -Require Import Addr. -Require Import Adist. -Require Import Addec. +Require Import NArith. +Require Import Ndigits. +Require Import Ndec. Require Import Map. Require Import Mapaxioms. Require Import Mapiter. @@ -38,80 +37,80 @@ Section MapCard. Qed. Lemma MapCard_is_O : - forall m:Map A, MapCard A m = 0 -> forall a:ad, MapGet A m a = NONE A. + forall m:Map A, MapCard A m = 0 -> forall a:ad, MapGet A m a = None. Proof. simple induction m. trivial. intros a y H. discriminate H. intros. simpl in H1. elim (plus_is_O _ _ H1). intros. rewrite (MapGet_M2_bit_0_if A m0 m1 a). - case (ad_bit_0 a). apply H0. assumption. + case (Nbit0 a). apply H0. assumption. apply H. assumption. Qed. Lemma MapCard_is_not_O : forall (m:Map A) (a:ad) (y:A), - MapGet A m a = SOME A y -> {n : nat | MapCard A m = S n}. + MapGet A m a = Some y -> {n : nat | MapCard A m = S n}. Proof. simple induction m. intros. discriminate H. - intros a y a0 y0 H. simpl in H. elim (sumbool_of_bool (ad_eq a a0)). intro H0. split with 0. + intros a y a0 y0 H. simpl in H. elim (sumbool_of_bool (Neqb a a0)). intro H0. split with 0. reflexivity. intro H0. rewrite H0 in H. discriminate H. - intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H2. - rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1) in H1. elim (H0 (ad_div_2 a) y H1). intros n H3. + intros. elim (sumbool_of_bool (Nbit0 a)). intro H2. + rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1) in H1. elim (H0 (Ndiv2 a) y H1). intros n H3. simpl in |- *. rewrite H3. split with (MapCard A m0 + n). rewrite <- (plus_Snm_nSm (MapCard A m0) n). reflexivity. - intro H2. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1) in H1. elim (H (ad_div_2 a) y H1). + intro H2. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1) in H1. elim (H (Ndiv2 a) y H1). intros n H3. simpl in |- *. rewrite H3. split with (n + MapCard A m1). reflexivity. Qed. Lemma MapCard_is_one : forall m:Map A, - MapCard A m = 1 -> {a : ad & {y : A | MapGet A m a = SOME A y}}. + MapCard A m = 1 -> {a : ad & {y : A | MapGet A m a = Some y}}. Proof. simple induction m. intro. discriminate H. intros a y H. split with a. split with y. apply M1_semantics_1. intros. simpl in H1. elim (plus_is_one (MapCard A m0) (MapCard A m1) H1). - intro H2. elim H2. intros. elim (H0 H4). intros a H5. split with (ad_double_plus_un a). - rewrite (MapGet_M2_bit_0_1 A _ (ad_double_plus_un_bit_0 a) m0 m1). - rewrite ad_double_plus_un_div_2. exact H5. - intro H2. elim H2. intros. elim (H H3). intros a H5. split with (ad_double a). - rewrite (MapGet_M2_bit_0_0 A _ (ad_double_bit_0 a) m0 m1). - rewrite ad_double_div_2. exact H5. + intro H2. elim H2. intros. elim (H0 H4). intros a H5. split with (Ndouble_plus_one a). + rewrite (MapGet_M2_bit_0_1 A _ (Ndouble_plus_one_bit0 a) m0 m1). + rewrite Ndouble_plus_one_div2. exact H5. + intro H2. elim H2. intros. elim (H H3). intros a H5. split with (Ndouble a). + rewrite (MapGet_M2_bit_0_0 A _ (Ndouble_bit0 a) m0 m1). + rewrite Ndouble_div2. exact H5. Qed. Lemma MapCard_is_one_unique : forall m:Map A, MapCard A m = 1 -> forall (a a':ad) (y y':A), - MapGet A m a = SOME A y -> - MapGet A m a' = SOME A y' -> a = a' /\ y = y'. + MapGet A m a = Some y -> + MapGet A m a' = Some y' -> a = a' /\ y = y'. Proof. simple induction m. intro. discriminate H. - intros. elim (sumbool_of_bool (ad_eq a a1)). intro H2. rewrite (ad_eq_complete _ _ H2) in H0. - rewrite (M1_semantics_1 A a1 a0) in H0. inversion H0. elim (sumbool_of_bool (ad_eq a a')). - intro H5. rewrite (ad_eq_complete _ _ H5) in H1. rewrite (M1_semantics_1 A a' a0) in H1. - inversion H1. rewrite <- (ad_eq_complete _ _ H2). rewrite <- (ad_eq_complete _ _ H5). + intros. elim (sumbool_of_bool (Neqb a a1)). intro H2. rewrite (Neqb_complete _ _ H2) in H0. + rewrite (M1_semantics_1 A a1 a0) in H0. inversion H0. elim (sumbool_of_bool (Neqb a a')). + intro H5. rewrite (Neqb_complete _ _ H5) in H1. rewrite (M1_semantics_1 A a' a0) in H1. + inversion H1. rewrite <- (Neqb_complete _ _ H2). rewrite <- (Neqb_complete _ _ H5). rewrite <- H4. rewrite <- H6. split; reflexivity. intro H5. rewrite (M1_semantics_2 A a a' a0 H5) in H1. discriminate H1. intro H2. rewrite (M1_semantics_2 A a a1 a0 H2) in H0. discriminate H0. intros. simpl in H1. elim (plus_is_one _ _ H1). intro H4. elim H4. intros. - rewrite (MapGet_M2_bit_0_if A m0 m1 a) in H2. elim (sumbool_of_bool (ad_bit_0 a)). + rewrite (MapGet_M2_bit_0_if A m0 m1 a) in H2. elim (sumbool_of_bool (Nbit0 a)). intro H7. rewrite H7 in H2. rewrite (MapGet_M2_bit_0_if A m0 m1 a') in H3. - elim (sumbool_of_bool (ad_bit_0 a')). intro H8. rewrite H8 in H3. elim (H0 H6 _ _ _ _ H2 H3). - intros. split. rewrite <- (ad_div_2_double_plus_un a H7). - rewrite <- (ad_div_2_double_plus_un a' H8). rewrite H9. reflexivity. + elim (sumbool_of_bool (Nbit0 a')). intro H8. rewrite H8 in H3. elim (H0 H6 _ _ _ _ H2 H3). + intros. split. rewrite <- (Ndiv2_double_plus_one a H7). + rewrite <- (Ndiv2_double_plus_one a' H8). rewrite H9. reflexivity. assumption. - intro H8. rewrite H8 in H3. rewrite (MapCard_is_O m0 H5 (ad_div_2 a')) in H3. + intro H8. rewrite H8 in H3. rewrite (MapCard_is_O m0 H5 (Ndiv2 a')) in H3. discriminate H3. - intro H7. rewrite H7 in H2. rewrite (MapCard_is_O m0 H5 (ad_div_2 a)) in H2. + intro H7. rewrite H7 in H2. rewrite (MapCard_is_O m0 H5 (Ndiv2 a)) in H2. discriminate H2. intro H4. elim H4. intros. rewrite (MapGet_M2_bit_0_if A m0 m1 a) in H2. - elim (sumbool_of_bool (ad_bit_0 a)). intro H7. rewrite H7 in H2. - rewrite (MapCard_is_O m1 H6 (ad_div_2 a)) in H2. discriminate H2. + elim (sumbool_of_bool (Nbit0 a)). intro H7. rewrite H7 in H2. + rewrite (MapCard_is_O m1 H6 (Ndiv2 a)) in H2. discriminate H2. intro H7. rewrite H7 in H2. rewrite (MapGet_M2_bit_0_if A m0 m1 a') in H3. - elim (sumbool_of_bool (ad_bit_0 a')). intro H8. rewrite H8 in H3. - rewrite (MapCard_is_O m1 H6 (ad_div_2 a')) in H3. discriminate H3. + elim (sumbool_of_bool (Nbit0 a')). intro H8. rewrite H8 in H3. + rewrite (MapCard_is_O m1 H6 (Ndiv2 a')) in H3. discriminate H3. intro H8. rewrite H8 in H3. elim (H H5 _ _ _ _ H2 H3). intros. split. - rewrite <- (ad_div_2_double a H7). rewrite <- (ad_div_2_double a' H8). + rewrite <- (Ndiv2_double a H7). rewrite <- (Ndiv2_double a' H8). rewrite H9. reflexivity. assumption. Qed. @@ -139,8 +138,8 @@ Section MapCard. Proof. simple induction m. trivial. trivial. - intros. simpl in |- *. rewrite <- (H (fun a0:ad => pf (ad_double a0))). - rewrite <- (H0 (fun a0:ad => pf (ad_double_plus_un a0))). reflexivity. + intros. simpl in |- *. rewrite <- (H (fun a0:ad => pf (Ndouble a0))). + rewrite <- (H0 (fun a0:ad => pf (Ndouble_plus_one a0))). reflexivity. Qed. Lemma MapCard_as_Fold : @@ -164,10 +163,10 @@ Section MapCard. forall (p:positive) (a a':ad) (y y':A), MapCard A (MapPut1 A a y a' y' p) = 2. Proof. - simple induction p. intros. simpl in |- *. case (ad_bit_0 a); reflexivity. - intros. simpl in |- *. case (ad_bit_0 a). exact (H (ad_div_2 a) (ad_div_2 a') y y'). - simpl in |- *. rewrite <- plus_n_O. exact (H (ad_div_2 a) (ad_div_2 a') y y'). - intros. simpl in |- *. case (ad_bit_0 a); reflexivity. + simple induction p. intros. simpl in |- *. case (Nbit0 a); reflexivity. + intros. simpl in |- *. case (Nbit0 a). exact (H (Ndiv2 a) (Ndiv2 a') y y'). + simpl in |- *. rewrite <- plus_n_O. exact (H (Ndiv2 a) (Ndiv2 a') y y'). + intros. simpl in |- *. case (Nbit0 a); reflexivity. Qed. Lemma MapCard_Put_sum : @@ -177,17 +176,17 @@ Section MapCard. Proof. simple induction m. simpl in |- *. intros. rewrite H in H1. simpl in H1. right. rewrite H0. rewrite H1. reflexivity. - intros a y m' a0 y0 n n' H H0 H1. simpl in H. elim (ad_sum (ad_xor a a0)). intro H2. + intros a y m' a0 y0 n n' H H0 H1. simpl in H. elim (Ndiscr (Nxor a a0)). intro H2. elim H2. intros p H3. rewrite H3 in H. rewrite H in H1. rewrite (MapCard_Put1_equals_2 p a a0 y y0) in H1. simpl in H0. right. rewrite H0. rewrite H1. reflexivity. intro H2. rewrite H2 in H. rewrite H in H1. simpl in H1. simpl in H0. left. rewrite H0. rewrite H1. reflexivity. intros. simpl in H2. rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H1. - elim (sumbool_of_bool (ad_bit_0 a)). intro H4. rewrite H4 in H1. + elim (sumbool_of_bool (Nbit0 a)). intro H4. rewrite H4 in H1. elim - (H0 (MapPut A m1 (ad_div_2 a) y) (ad_div_2 a) y ( - MapCard A m1) (MapCard A (MapPut A m1 (ad_div_2 a) y)) ( + (H0 (MapPut A m1 (Ndiv2 a) y) (Ndiv2 a) y ( + MapCard A m1) (MapCard A (MapPut A m1 (Ndiv2 a) y)) ( refl_equal _) (refl_equal _) (refl_equal _)). intro H5. rewrite H1 in H3. simpl in H3. rewrite H5 in H3. rewrite <- H2 in H3. left. assumption. @@ -196,8 +195,8 @@ Section MapCard. simpl in H3. rewrite <- H2 in H3. right. assumption. intro H4. rewrite H4 in H1. elim - (H (MapPut A m0 (ad_div_2 a) y) (ad_div_2 a) y ( - MapCard A m0) (MapCard A (MapPut A m0 (ad_div_2 a) y)) ( + (H (MapPut A m0 (Ndiv2 a) y) (Ndiv2 a) y ( + MapCard A m0) (MapCard A (MapPut A m0 (Ndiv2 a) y)) ( refl_equal _) (refl_equal _) (refl_equal _)). intro H5. rewrite H1 in H3. simpl in H3. rewrite H5 in H3. rewrite <- H2 in H3. left. assumption. @@ -233,35 +232,35 @@ Section MapCard. Lemma MapCard_Put_1 : forall (m:Map A) (a:ad) (y:A), MapCard A (MapPut A m a y) = MapCard A m -> - {y : A | MapGet A m a = SOME A y}. + {y : A | MapGet A m a = Some y}. Proof. simple induction m. intros. discriminate H. - intros a y a0 y0 H. simpl in H. elim (ad_sum (ad_xor a a0)). intro H0. elim H0. + intros a y a0 y0 H. simpl in H. elim (Ndiscr (Nxor a a0)). intro H0. elim H0. intros p H1. rewrite H1 in H. rewrite (MapCard_Put1_equals_2 p a a0 y y0) in H. discriminate H. - intro H0. rewrite H0 in H. rewrite (ad_xor_eq _ _ H0). split with y. apply M1_semantics_1. - intros. rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H1. elim (sumbool_of_bool (ad_bit_0 a)). - intro H2. rewrite H2 in H1. simpl in H1. elim (H0 (ad_div_2 a) y ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1)). + intro H0. rewrite H0 in H. rewrite (Nxor_eq _ _ H0). split with y. apply M1_semantics_1. + intros. rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H1. elim (sumbool_of_bool (Nbit0 a)). + intro H2. rewrite H2 in H1. simpl in H1. elim (H0 (Ndiv2 a) y ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1)). intros y0 H3. split with y0. rewrite <- H3. exact (MapGet_M2_bit_0_1 A a H2 m0 m1). intro H2. rewrite H2 in H1. simpl in H1. rewrite - (plus_comm (MapCard A (MapPut A m0 (ad_div_2 a) y)) (MapCard A m1)) + (plus_comm (MapCard A (MapPut A m0 (Ndiv2 a) y)) (MapCard A m1)) in H1. rewrite (plus_comm (MapCard A m0) (MapCard A m1)) in H1. - elim (H (ad_div_2 a) y ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1)). intros y0 H3. split with y0. + elim (H (Ndiv2 a) y ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1)). intros y0 H3. split with y0. rewrite <- H3. exact (MapGet_M2_bit_0_0 A a H2 m0 m1). Qed. Lemma MapCard_Put_2 : forall (m:Map A) (a:ad) (y:A), - MapCard A (MapPut A m a y) = S (MapCard A m) -> MapGet A m a = NONE A. + MapCard A (MapPut A m a y) = S (MapCard A m) -> MapGet A m a = None. Proof. simple induction m. trivial. - intros. simpl in H. elim (sumbool_of_bool (ad_eq a a1)). intro H0. - rewrite (ad_eq_complete _ _ H0) in H. rewrite (ad_xor_nilpotent a1) in H. discriminate H. + intros. simpl in H. elim (sumbool_of_bool (Neqb a a1)). intro H0. + rewrite (Neqb_complete _ _ H0) in H. rewrite (Nxor_nilpotent a1) in H. discriminate H. intro H0. exact (M1_semantics_2 A a a1 a0 H0). - intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H2. - rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). apply (H0 (ad_div_2 a) y). + intros. elim (sumbool_of_bool (Nbit0 a)). intro H2. + rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). apply (H0 (Ndiv2 a) y). apply (fun n m p:nat => plus_reg_l m p n) with (n := MapCard A m0). rewrite <- (plus_Snm_nSm (MapCard A m0) (MapCard A m1)). simpl in H1. simpl in |- *. rewrite <- H1. clear H1. @@ -269,11 +268,11 @@ Section MapCard. induction p. reflexivity. discriminate H2. reflexivity. - intro H2. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). apply (H (ad_div_2 a) y). + intro H2. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). apply (H (Ndiv2 a) y). cut - (MapCard A (MapPut A m0 (ad_div_2 a) y) + MapCard A m1 = + (MapCard A (MapPut A m0 (Ndiv2 a) y) + MapCard A m1 = S (MapCard A m0) + MapCard A m1). - intro. rewrite (plus_comm (MapCard A (MapPut A m0 (ad_div_2 a) y)) (MapCard A m1)) + intro. rewrite (plus_comm (MapCard A (MapPut A m0 (Ndiv2 a) y)) (MapCard A m1)) in H3. rewrite (plus_comm (S (MapCard A m0)) (MapCard A m1)) in H3. exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H3). simpl in |- *. simpl in H1. rewrite <- H1. induction a. trivial. @@ -284,7 +283,7 @@ Section MapCard. Lemma MapCard_Put_1_conv : forall (m:Map A) (a:ad) (y y':A), - MapGet A m a = SOME A y -> MapCard A (MapPut A m a y') = MapCard A m. + MapGet A m a = Some y -> MapCard A (MapPut A m a y') = MapCard A m. Proof. intros. elim @@ -297,7 +296,7 @@ Section MapCard. Lemma MapCard_Put_2_conv : forall (m:Map A) (a:ad) (y:A), - MapGet A m a = NONE A -> MapCard A (MapPut A m a y) = S (MapCard A m). + MapGet A m a = None -> MapCard A (MapPut A m a y) = S (MapCard A m). Proof. intros. elim @@ -331,10 +330,10 @@ Section MapCard. MapDom A (MapPut_behind A m a y) = MapDom A (MapPut A m a y). Proof. simple induction m. trivial. - intros a y a0 y0. simpl in |- *. elim (ad_sum (ad_xor a a0)). intro H. elim H. + intros a y a0 y0. simpl in |- *. elim (Ndiscr (Nxor a a0)). intro H. elim H. intros p H0. rewrite H0. reflexivity. - intro H. rewrite H. rewrite (ad_xor_eq _ _ H). reflexivity. - intros. simpl in |- *. elim (ad_sum a). intro H1. elim H1. intros p H2. rewrite H2. case p. + intro H. rewrite H. rewrite (Nxor_eq _ _ H). reflexivity. + intros. simpl in |- *. elim (Ndiscr a). intro H1. elim H1. intros p H2. rewrite H2. case p. intro p0. simpl in |- *. rewrite H0. reflexivity. intro p0. simpl in |- *. rewrite H. reflexivity. simpl in |- *. rewrite H0. reflexivity. @@ -370,27 +369,27 @@ Section MapCard. n = MapCard A m -> n' = MapCard A m' -> {n = n'} + {n = S n'}. Proof. simple induction m. simpl in |- *. intros. rewrite H in H1. simpl in H1. left. rewrite H1. assumption. - simpl in |- *. intros. elim (sumbool_of_bool (ad_eq a a1)). intro H2. rewrite H2 in H. + simpl in |- *. intros. elim (sumbool_of_bool (Neqb a a1)). intro H2. rewrite H2 in H. rewrite H in H1. simpl in H1. right. rewrite H1. assumption. intro H2. rewrite H2 in H. rewrite H in H1. simpl in H1. left. rewrite H1. assumption. - intros. simpl in H1. simpl in H2. elim (sumbool_of_bool (ad_bit_0 a)). intro H4. + intros. simpl in H1. simpl in H2. elim (sumbool_of_bool (Nbit0 a)). intro H4. rewrite H4 in H1. rewrite H1 in H3. - rewrite (MapCard_makeM2 m0 (MapRemove A m1 (ad_div_2 a))) in H3. + rewrite (MapCard_makeM2 m0 (MapRemove A m1 (Ndiv2 a))) in H3. elim - (H0 (MapRemove A m1 (ad_div_2 a)) (ad_div_2 a) ( - MapCard A m1) (MapCard A (MapRemove A m1 (ad_div_2 a))) + (H0 (MapRemove A m1 (Ndiv2 a)) (Ndiv2 a) ( + MapCard A m1) (MapCard A (MapRemove A m1 (Ndiv2 a))) (refl_equal _) (refl_equal _) (refl_equal _)). intro H5. rewrite H5 in H2. left. rewrite H3. exact H2. intro H5. rewrite H5 in H2. rewrite <- - (plus_Snm_nSm (MapCard A m0) (MapCard A (MapRemove A m1 (ad_div_2 a)))) + (plus_Snm_nSm (MapCard A m0) (MapCard A (MapRemove A m1 (Ndiv2 a)))) in H2. right. rewrite H3. exact H2. intro H4. rewrite H4 in H1. rewrite H1 in H3. - rewrite (MapCard_makeM2 (MapRemove A m0 (ad_div_2 a)) m1) in H3. + rewrite (MapCard_makeM2 (MapRemove A m0 (Ndiv2 a)) m1) in H3. elim - (H (MapRemove A m0 (ad_div_2 a)) (ad_div_2 a) ( - MapCard A m0) (MapCard A (MapRemove A m0 (ad_div_2 a))) + (H (MapRemove A m0 (Ndiv2 a)) (Ndiv2 a) ( + MapCard A m0) (MapCard A (MapRemove A m0 (Ndiv2 a))) (refl_equal _) (refl_equal _) (refl_equal _)). intro H5. rewrite H5 in H2. left. rewrite H3. exact H2. intro H5. rewrite H5 in H2. right. rewrite H3. exact H2. @@ -422,20 +421,20 @@ Section MapCard. Lemma MapCard_Remove_1 : forall (m:Map A) (a:ad), - MapCard A (MapRemove A m a) = MapCard A m -> MapGet A m a = NONE A. + MapCard A (MapRemove A m a) = MapCard A m -> MapGet A m a = None. Proof. simple induction m. trivial. - simpl in |- *. intros a y a0 H. elim (sumbool_of_bool (ad_eq a a0)). intro H0. + simpl in |- *. intros a y a0 H. elim (sumbool_of_bool (Neqb a a0)). intro H0. rewrite H0 in H. discriminate H. intro H0. rewrite H0. reflexivity. - intros. simpl in H1. elim (sumbool_of_bool (ad_bit_0 a)). intro H2. rewrite H2 in H1. - rewrite (MapCard_makeM2 m0 (MapRemove A m1 (ad_div_2 a))) in H1. + intros. simpl in H1. elim (sumbool_of_bool (Nbit0 a)). intro H2. rewrite H2 in H1. + rewrite (MapCard_makeM2 m0 (MapRemove A m1 (Ndiv2 a))) in H1. rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). apply H0. exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1). intro H2. rewrite H2 in H1. - rewrite (MapCard_makeM2 (MapRemove A m0 (ad_div_2 a)) m1) in H1. + rewrite (MapCard_makeM2 (MapRemove A m0 (Ndiv2 a)) m1) in H1. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). apply H. rewrite - (plus_comm (MapCard A (MapRemove A m0 (ad_div_2 a))) (MapCard A m1)) + (plus_comm (MapCard A (MapRemove A m0 (Ndiv2 a))) (MapCard A m1)) in H1. rewrite (plus_comm (MapCard A m0) (MapCard A m1)) in H1. exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1). Qed. @@ -443,36 +442,36 @@ Section MapCard. Lemma MapCard_Remove_2 : forall (m:Map A) (a:ad), S (MapCard A (MapRemove A m a)) = MapCard A m -> - {y : A | MapGet A m a = SOME A y}. + {y : A | MapGet A m a = Some y}. Proof. simple induction m. intros. discriminate H. - intros a y a0 H. simpl in H. elim (sumbool_of_bool (ad_eq a a0)). intro H0. - rewrite (ad_eq_complete _ _ H0). split with y. exact (M1_semantics_1 A a0 y). + intros a y a0 H. simpl in H. elim (sumbool_of_bool (Neqb a a0)). intro H0. + rewrite (Neqb_complete _ _ H0). split with y. exact (M1_semantics_1 A a0 y). intro H0. rewrite H0 in H. discriminate H. - intros. simpl in H1. elim (sumbool_of_bool (ad_bit_0 a)). intro H2. rewrite H2 in H1. - rewrite (MapCard_makeM2 m0 (MapRemove A m1 (ad_div_2 a))) in H1. + intros. simpl in H1. elim (sumbool_of_bool (Nbit0 a)). intro H2. rewrite H2 in H1. + rewrite (MapCard_makeM2 m0 (MapRemove A m1 (Ndiv2 a))) in H1. rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). apply H0. change - (S (MapCard A m0) + MapCard A (MapRemove A m1 (ad_div_2 a)) = + (S (MapCard A m0) + MapCard A (MapRemove A m1 (Ndiv2 a)) = MapCard A m0 + MapCard A m1) in H1. rewrite - (plus_Snm_nSm (MapCard A m0) (MapCard A (MapRemove A m1 (ad_div_2 a)))) + (plus_Snm_nSm (MapCard A m0) (MapCard A (MapRemove A m1 (Ndiv2 a)))) in H1. exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1). intro H2. rewrite H2 in H1. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). apply H. - rewrite (MapCard_makeM2 (MapRemove A m0 (ad_div_2 a)) m1) in H1. + rewrite (MapCard_makeM2 (MapRemove A m0 (Ndiv2 a)) m1) in H1. change - (S (MapCard A (MapRemove A m0 (ad_div_2 a))) + MapCard A m1 = + (S (MapCard A (MapRemove A m0 (Ndiv2 a))) + MapCard A m1 = MapCard A m0 + MapCard A m1) in H1. rewrite - (plus_comm (S (MapCard A (MapRemove A m0 (ad_div_2 a)))) (MapCard A m1)) + (plus_comm (S (MapCard A (MapRemove A m0 (Ndiv2 a)))) (MapCard A m1)) in H1. rewrite (plus_comm (MapCard A m0) (MapCard A m1)) in H1. exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1). Qed. Lemma MapCard_Remove_1_conv : forall (m:Map A) (a:ad), - MapGet A m a = NONE A -> MapCard A (MapRemove A m a) = MapCard A m. + MapGet A m a = None -> MapCard A (MapRemove A m a) = MapCard A m. Proof. intros. elim @@ -486,7 +485,7 @@ Section MapCard. Lemma MapCard_Remove_2_conv : forall (m:Map A) (a:ad) (y:A), - MapGet A m a = SOME A y -> S (MapCard A (MapRemove A m a)) = MapCard A m. + MapGet A m a = Some y -> S (MapCard A (MapRemove A m a)) = MapCard A m. Proof. intros. elim @@ -577,20 +576,20 @@ Section MapCard. Proof. simple induction m. intros. apply Map_M0_disjoint. simpl in |- *. intros. rewrite (MapCard_Put_behind_Put m' a a0) in H. unfold MapDisjoint, in_dom in |- *. - simpl in |- *. intros. elim (sumbool_of_bool (ad_eq a a1)). intro H2. - rewrite (ad_eq_complete _ _ H2) in H. rewrite (MapCard_Put_2 m' a1 a0 H) in H1. + simpl in |- *. intros. elim (sumbool_of_bool (Neqb a a1)). intro H2. + rewrite (Neqb_complete _ _ H2) in H. rewrite (MapCard_Put_2 m' a1 a0 H) in H1. discriminate H1. intro H2. rewrite H2 in H0. discriminate H0. simple induction m'. intros. apply Map_disjoint_M0. intros a y H1. rewrite <- (MapCard_ext _ _ (MapPut_as_Merge A (M2 A m0 m1) a y)) in H1. unfold MapCard at 3 in H1. rewrite <- (plus_Snm_nSm (MapCard A (M2 A m0 m1)) 0) in H1. rewrite <- (plus_n_O (S (MapCard A (M2 A m0 m1)))) in H1. unfold MapDisjoint, in_dom in |- *. - unfold MapGet at 2 in |- *. intros. elim (sumbool_of_bool (ad_eq a a0)). intro H4. - rewrite <- (ad_eq_complete _ _ H4) in H2. rewrite (MapCard_Put_2 _ _ _ H1) in H2. + unfold MapGet at 2 in |- *. intros. elim (sumbool_of_bool (Neqb a a0)). intro H4. + rewrite <- (Neqb_complete _ _ H4) in H2. rewrite (MapCard_Put_2 _ _ _ H1) in H2. discriminate H2. intro H4. rewrite H4 in H3. discriminate H3. - intros. unfold MapDisjoint in |- *. intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H6. - unfold MapDisjoint in H0. apply H0 with (m' := m3) (a := ad_div_2 a). apply le_antisym. + intros. unfold MapDisjoint in |- *. intros. elim (sumbool_of_bool (Nbit0 a)). intro H6. + unfold MapDisjoint in H0. apply H0 with (m' := m3) (a := Ndiv2 a). apply le_antisym. apply MapMerge_Card_ub. apply (fun p n m:nat => plus_le_reg_l n m p) with (p := MapCard A m0 + MapCard A m2). @@ -606,7 +605,7 @@ Section MapCard. unfold in_dom in |- *. rewrite H7. reflexivity. elim (in_dom_some _ _ _ H5). intros y H7. rewrite (MapGet_M2_bit_0_1 _ a H6 m2 m3) in H7. unfold in_dom in |- *. rewrite H7. reflexivity. - intro H6. unfold MapDisjoint in H. apply H with (m' := m2) (a := ad_div_2 a). apply le_antisym. + intro H6. unfold MapDisjoint in H. apply H with (m' := m2) (a := Ndiv2 a). apply le_antisym. apply MapMerge_Card_ub. apply (fun p n m:nat => plus_le_reg_l n m p) with (p := MapCard A m1 + MapCard A m3). @@ -637,15 +636,15 @@ Section MapCard. simple induction m. intros. discriminate H. intros a y n H. split with a. unfold in_dom in |- *. rewrite (M1_semantics_1 _ a y). reflexivity. intros. simpl in H1. elim (O_or_S (MapCard _ m0)). intro H2. elim H2. intros m2 H3. - elim (H _ (sym_eq H3)). intros a H4. split with (ad_double a). unfold in_dom in |- *. - rewrite (MapGet_M2_bit_0_0 A (ad_double a) (ad_double_bit_0 a) m0 m1). - rewrite (ad_double_div_2 a). elim (in_dom_some _ _ _ H4). intros y H5. rewrite H5. reflexivity. + elim (H _ (sym_eq H3)). intros a H4. split with (Ndouble a). unfold in_dom in |- *. + rewrite (MapGet_M2_bit_0_0 A (Ndouble a) (Ndouble_bit0 a) m0 m1). + rewrite (Ndouble_div2 a). elim (in_dom_some _ _ _ H4). intros y H5. rewrite H5. reflexivity. intro H2. rewrite <- H2 in H1. simpl in H1. elim (H0 _ H1). intros a H3. - split with (ad_double_plus_un a). unfold in_dom in |- *. + split with (Ndouble_plus_one a). unfold in_dom in |- *. rewrite - (MapGet_M2_bit_0_1 A (ad_double_plus_un a) (ad_double_plus_un_bit_0 a) + (MapGet_M2_bit_0_1 A (Ndouble_plus_one a) (Ndouble_plus_one_bit0 a) m0 m1). - rewrite (ad_double_plus_un_div_2 a). elim (in_dom_some _ _ _ H3). intros y H4. rewrite H4. + rewrite (Ndouble_plus_one_div2 a). elim (in_dom_some _ _ _ H3). intros y H4. rewrite H4. reflexivity. Qed. @@ -675,11 +674,11 @@ Section MapCard2. rewrite <- (MapCard_Remove_2_conv _ m a y H4) in H1. inversion_clear H1. reflexivity. rewrite <- (MapCard_Remove_2_conv _ m' a y' H6) in H2. inversion_clear H2. reflexivity. unfold eqmap, eqm in |- *. intro. rewrite (MapPut_semantics _ (MapRemove B m' a) a y' a0). - elim (sumbool_of_bool (ad_eq a a0)). intro H7. rewrite H7. rewrite <- (ad_eq_complete _ _ H7). + elim (sumbool_of_bool (Neqb a a0)). intro H7. rewrite H7. rewrite <- (Neqb_complete _ _ H7). apply sym_eq. assumption. intro H7. rewrite H7. rewrite (MapRemove_semantics _ m' a a0). rewrite H7. reflexivity. unfold eqmap, eqm in |- *. intro. rewrite (MapPut_semantics _ (MapRemove A m a) a y a0). - elim (sumbool_of_bool (ad_eq a a0)). intro H7. rewrite H7. rewrite <- (ad_eq_complete _ _ H7). + elim (sumbool_of_bool (Neqb a a0)). intro H7. rewrite H7. rewrite <- (Neqb_complete _ _ H7). apply sym_eq. assumption. intro H7. rewrite H7. rewrite (MapRemove_semantics A m a a0). rewrite H7. reflexivity. Qed. @@ -695,8 +694,9 @@ Section MapCard2. intro H. rewrite H. simpl in |- *. apply le_O_n. simple induction m'. simpl in |- *. apply le_O_n. - intros a y. unfold MapDomRestrTo in |- *. case (MapGet A (M2 A m0 m1) a). simpl in |- *. apply le_O_n. + intros a y. unfold MapDomRestrTo in |- *. case (MapGet A (M2 A m0 m1) a). simpl in |- *. intro. simpl in |- *. apply le_n. + apply le_O_n. intros. simpl in |- *. rewrite (MapCard_makeM2 A (MapDomRestrTo A B m0 m2) (MapDomRestrTo A B m1 m3)) . diff --git a/theories/IntMap/Mapfold.v b/theories/IntMap/Mapfold.v index 335a1384..eb58cb64 100644 --- a/theories/IntMap/Mapfold.v +++ b/theories/IntMap/Mapfold.v @@ -5,14 +5,13 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Mapfold.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Mapfold.v 8733 2006-04-25 22:52:18Z letouzey $ i*) Require Import Bool. Require Import Sumbool. -Require Import ZArith. -Require Import Addr. -Require Import Adist. -Require Import Addec. +Require Import NArith. +Require Import Ndigits. +Require Import Ndec. Require Import Map. Require Import Fset. Require Import Mapaxioms. @@ -50,22 +49,22 @@ Section MapFoldResults. Lemma MapFold_ext_f_1 : forall (m:Map A) (f g:ad -> A -> M) (pf:ad -> ad), - (forall (a:ad) (y:A), MapGet _ m a = SOME _ y -> f (pf a) y = g (pf a) y) -> + (forall (a:ad) (y:A), MapGet _ m a = Some y -> f (pf a) y = g (pf a) y) -> MapFold1 _ _ neutral op f pf m = MapFold1 _ _ neutral op g pf m. Proof. simple induction m. trivial. - simpl in |- *. intros. apply H. rewrite (ad_eq_correct a). reflexivity. - intros. simpl in |- *. rewrite (H f g (fun a0:ad => pf (ad_double a0))). - rewrite (H0 f g (fun a0:ad => pf (ad_double_plus_un a0))). reflexivity. - intros. apply H1. rewrite MapGet_M2_bit_0_1. rewrite ad_double_plus_un_div_2. assumption. - apply ad_double_plus_un_bit_0. - intros. apply H1. rewrite MapGet_M2_bit_0_0. rewrite ad_double_div_2. assumption. - apply ad_double_bit_0. + simpl in |- *. intros. apply H. rewrite (Neqb_correct a). reflexivity. + intros. simpl in |- *. rewrite (H f g (fun a0:ad => pf (Ndouble a0))). + rewrite (H0 f g (fun a0:ad => pf (Ndouble_plus_one a0))). reflexivity. + intros. apply H1. rewrite MapGet_M2_bit_0_1. rewrite Ndouble_plus_one_div2. assumption. + apply Ndouble_plus_one_bit0. + intros. apply H1. rewrite MapGet_M2_bit_0_0. rewrite Ndouble_div2. assumption. + apply Ndouble_bit0. Qed. Lemma MapFold_ext_f : forall (f g:ad -> A -> M) (m:Map A), - (forall (a:ad) (y:A), MapGet _ m a = SOME _ y -> f a y = g a y) -> + (forall (a:ad) (y:A), MapGet _ m a = Some y -> f a y = g a y) -> MapFold _ _ neutral op f m = MapFold _ _ neutral op g m. Proof. intros. exact (MapFold_ext_f_1 m f g (fun a0:ad => a0) H). @@ -80,11 +79,11 @@ Section MapFoldResults. intros. simpl in |- *. apply H. intros. simpl in |- *. rewrite - (H f f' (fun a0:ad => pf (ad_double a0)) - (fun a0:ad => pf' (ad_double a0))). + (H f f' (fun a0:ad => pf (Ndouble a0)) + (fun a0:ad => pf' (Ndouble a0))). rewrite - (H0 f f' (fun a0:ad => pf (ad_double_plus_un a0)) - (fun a0:ad => pf' (ad_double_plus_un a0))). + (H0 f f' (fun a0:ad => pf (Ndouble_plus_one a0)) + (fun a0:ad => pf' (Ndouble_plus_one a0))). reflexivity. intros. apply H1. intros. apply H1. @@ -112,81 +111,83 @@ Section MapFoldResults. Lemma MapFold_Put_disjoint_1 : forall (p:positive) (f:ad -> A -> M) (pf:ad -> ad) (a1 a2:ad) (y1 y2:A), - ad_xor a1 a2 = ad_x p -> + Nxor a1 a2 = Npos p -> MapFold1 A M neutral op f pf (MapPut1 A a1 y1 a2 y2 p) = op (f (pf a1) y1) (f (pf a2) y2). Proof. - simple induction p. intros. simpl in |- *. elim (sumbool_of_bool (ad_bit_0 a1)). intro H1. rewrite H1. - simpl in |- *. rewrite ad_div_2_double_plus_un. rewrite ad_div_2_double. apply comm. - change (ad_bit_0 a2 = negb true) in |- *. rewrite <- H1. rewrite (ad_neg_bit_0_2 _ _ _ H0). + simple induction p. intros. simpl in |- *. elim (sumbool_of_bool (Nbit0 a1)). intro H1. rewrite H1. + simpl in |- *. rewrite Ndiv2_double_plus_one. rewrite Ndiv2_double. apply comm. + change (Nbit0 a2 = negb true) in |- *. rewrite <- H1. rewrite (Nneg_bit0_2 _ _ _ H0). rewrite negb_elim. reflexivity. assumption. - intro H1. rewrite H1. simpl in |- *. rewrite ad_div_2_double. rewrite ad_div_2_double_plus_un. + intro H1. rewrite H1. simpl in |- *. rewrite Ndiv2_double. rewrite Ndiv2_double_plus_one. reflexivity. - change (ad_bit_0 a2 = negb false) in |- *. rewrite <- H1. rewrite (ad_neg_bit_0_2 _ _ _ H0). + change (Nbit0 a2 = negb false) in |- *. rewrite <- H1. rewrite (Nneg_bit0_2 _ _ _ H0). rewrite negb_elim. reflexivity. assumption. - simpl in |- *. intros. elim (sumbool_of_bool (ad_bit_0 a1)). intro H1. rewrite H1. simpl in |- *. + simpl in |- *. intros. elim (sumbool_of_bool (Nbit0 a1)). intro H1. rewrite H1. simpl in |- *. rewrite nleft. rewrite - (H f (fun a0:ad => pf (ad_double_plus_un a0)) ( - ad_div_2 a1) (ad_div_2 a2) y1 y2). - rewrite ad_div_2_double_plus_un. rewrite ad_div_2_double_plus_un. reflexivity. - rewrite <- (ad_same_bit_0 _ _ _ H0). assumption. + (H f (fun a0:ad => pf (Ndouble_plus_one a0)) ( + Ndiv2 a1) (Ndiv2 a2) y1 y2). + rewrite Ndiv2_double_plus_one. rewrite Ndiv2_double_plus_one. reflexivity. + unfold Nodd. + rewrite <- (Nsame_bit0 _ _ _ H0). assumption. assumption. - rewrite <- ad_xor_div_2. rewrite H0. reflexivity. + rewrite <- Nxor_div2. rewrite H0. reflexivity. intro H1. rewrite H1. simpl in |- *. rewrite nright. rewrite - (H f (fun a0:ad => pf (ad_double a0)) (ad_div_2 a1) (ad_div_2 a2) y1 y2) + (H f (fun a0:ad => pf (Ndouble a0)) (Ndiv2 a1) (Ndiv2 a2) y1 y2) . - rewrite ad_div_2_double. rewrite ad_div_2_double. reflexivity. - rewrite <- (ad_same_bit_0 _ _ _ H0). assumption. + rewrite Ndiv2_double. rewrite Ndiv2_double. reflexivity. + unfold Neven. + rewrite <- (Nsame_bit0 _ _ _ H0). assumption. assumption. - rewrite <- ad_xor_div_2. rewrite H0. reflexivity. - intros. simpl in |- *. elim (sumbool_of_bool (ad_bit_0 a1)). intro H0. rewrite H0. simpl in |- *. - rewrite ad_div_2_double. rewrite ad_div_2_double_plus_un. apply comm. + rewrite <- Nxor_div2. rewrite H0. reflexivity. + intros. simpl in |- *. elim (sumbool_of_bool (Nbit0 a1)). intro H0. rewrite H0. simpl in |- *. + rewrite Ndiv2_double. rewrite Ndiv2_double_plus_one. apply comm. assumption. - change (ad_bit_0 a2 = negb true) in |- *. rewrite <- H0. rewrite (ad_neg_bit_0_1 _ _ H). + change (Nbit0 a2 = negb true) in |- *. rewrite <- H0. rewrite (Nneg_bit0_1 _ _ H). rewrite negb_elim. reflexivity. - intro H0. rewrite H0. simpl in |- *. rewrite ad_div_2_double. rewrite ad_div_2_double_plus_un. + intro H0. rewrite H0. simpl in |- *. rewrite Ndiv2_double. rewrite Ndiv2_double_plus_one. reflexivity. - change (ad_bit_0 a2 = negb false) in |- *. rewrite <- H0. rewrite (ad_neg_bit_0_1 _ _ H). + change (Nbit0 a2 = negb false) in |- *. rewrite <- H0. rewrite (Nneg_bit0_1 _ _ H). rewrite negb_elim. reflexivity. assumption. Qed. Lemma MapFold_Put_disjoint_2 : forall (f:ad -> A -> M) (m:Map A) (a:ad) (y:A) (pf:ad -> ad), - MapGet A m a = NONE A -> + MapGet A m a = None -> MapFold1 A M neutral op f pf (MapPut A m a y) = op (f (pf a) y) (MapFold1 A M neutral op f pf m). Proof. simple induction m. intros. simpl in |- *. rewrite (nright (f (pf a) y)). reflexivity. - intros a1 y1 a2 y2 pf H. simpl in |- *. elim (ad_sum (ad_xor a1 a2)). intro H0. elim H0. + intros a1 y1 a2 y2 pf H. simpl in |- *. elim (Ndiscr (Nxor a1 a2)). intro H0. elim H0. intros p H1. rewrite H1. rewrite comm. exact (MapFold_Put_disjoint_1 p f pf a1 a2 y1 y2 H1). - intro H0. rewrite (ad_eq_complete _ _ (ad_xor_eq_true _ _ H0)) in H. + intro H0. rewrite (Neqb_complete _ _ (Nxor_eq_true _ _ H0)) in H. rewrite (M1_semantics_1 A a2 y1) in H. discriminate H. - intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H2. - cut (MapPut A (M2 A m0 m1) a y = M2 A m0 (MapPut A m1 (ad_div_2 a) y)). intro. - rewrite H3. simpl in |- *. rewrite (H0 (ad_div_2 a) y (fun a0:ad => pf (ad_double_plus_un a0))). - rewrite ad_div_2_double_plus_un. rewrite <- assoc. + intros. elim (sumbool_of_bool (Nbit0 a)). intro H2. + cut (MapPut A (M2 A m0 m1) a y = M2 A m0 (MapPut A m1 (Ndiv2 a) y)). intro. + rewrite H3. simpl in |- *. rewrite (H0 (Ndiv2 a) y (fun a0:ad => pf (Ndouble_plus_one a0))). + rewrite Ndiv2_double_plus_one. rewrite <- assoc. rewrite - (comm (MapFold1 A M neutral op f (fun a0:ad => pf (ad_double a0)) m0) + (comm (MapFold1 A M neutral op f (fun a0:ad => pf (Ndouble a0)) m0) (f (pf a) y)). rewrite assoc. reflexivity. assumption. rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1) in H1. assumption. - simpl in |- *. elim (ad_sum a). intro H3. elim H3. intro p. elim p. intros p0 H4 H5. rewrite H5. + simpl in |- *. elim (Ndiscr a). intro H3. elim H3. intro p. elim p. intros p0 H4 H5. rewrite H5. reflexivity. intros p0 H4 H5. rewrite H5 in H2. discriminate H2. intro H4. rewrite H4. reflexivity. intro H3. rewrite H3 in H2. discriminate H2. - intro H2. cut (MapPut A (M2 A m0 m1) a y = M2 A (MapPut A m0 (ad_div_2 a) y) m1). - intro. rewrite H3. simpl in |- *. rewrite (H (ad_div_2 a) y (fun a0:ad => pf (ad_double a0))). - rewrite ad_div_2_double. rewrite <- assoc. reflexivity. + intro H2. cut (MapPut A (M2 A m0 m1) a y = M2 A (MapPut A m0 (Ndiv2 a) y) m1). + intro. rewrite H3. simpl in |- *. rewrite (H (Ndiv2 a) y (fun a0:ad => pf (Ndouble a0))). + rewrite Ndiv2_double. rewrite <- assoc. reflexivity. assumption. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1) in H1. assumption. - simpl in |- *. elim (ad_sum a). intro H3. elim H3. intro p. elim p. intros p0 H4 H5. rewrite H5 in H2. + simpl in |- *. elim (Ndiscr a). intro H3. elim H3. intro p. elim p. intros p0 H4 H5. rewrite H5 in H2. discriminate H2. intros p0 H4 H5. rewrite H5. reflexivity. intro H4. rewrite H4 in H2. discriminate H2. @@ -195,7 +196,7 @@ Section MapFoldResults. Lemma MapFold_Put_disjoint : forall (f:ad -> A -> M) (m:Map A) (a:ad) (y:A), - MapGet A m a = NONE A -> + MapGet A m a = None -> MapFold A M neutral op f (MapPut A m a y) = op (f a y) (MapFold A M neutral op f m). Proof. @@ -204,7 +205,7 @@ Section MapFoldResults. Lemma MapFold_Put_behind_disjoint_2 : forall (f:ad -> A -> M) (m:Map A) (a:ad) (y:A) (pf:ad -> ad), - MapGet A m a = NONE A -> + MapGet A m a = None -> MapFold1 A M neutral op f pf (MapPut_behind A m a y) = op (f (pf a) y) (MapFold1 A M neutral op f pf m). Proof. @@ -213,12 +214,12 @@ Section MapFoldResults. apply eqmap_trans with (m' := MapMerge A (M1 A a y) m). apply MapPut_behind_as_Merge. apply eqmap_trans with (m' := MapMerge A m (M1 A a y)). apply eqmap_trans with (m' := MapDelta A (M1 A a y) m). apply eqmap_sym. apply MapDelta_disjoint. - unfold MapDisjoint in |- *. unfold in_dom in |- *. simpl in |- *. intros. elim (sumbool_of_bool (ad_eq a a0)). - intro H2. rewrite (ad_eq_complete _ _ H2) in H. rewrite H in H1. discriminate H1. + unfold MapDisjoint in |- *. unfold in_dom in |- *. simpl in |- *. intros. elim (sumbool_of_bool (Neqb a a0)). + intro H2. rewrite (Neqb_complete _ _ H2) in H. rewrite H in H1. discriminate H1. intro H2. rewrite H2 in H0. discriminate H0. apply eqmap_trans with (m' := MapDelta A m (M1 A a y)). apply MapDelta_sym. apply MapDelta_disjoint. unfold MapDisjoint in |- *. unfold in_dom in |- *. simpl in |- *. intros. - elim (sumbool_of_bool (ad_eq a a0)). intro H2. rewrite (ad_eq_complete _ _ H2) in H. + elim (sumbool_of_bool (Neqb a a0)). intro H2. rewrite (Neqb_complete _ _ H2) in H. rewrite H in H0. discriminate H0. intro H2. rewrite H2 in H1. discriminate H1. apply eqmap_sym. apply MapPut_as_Merge. @@ -226,7 +227,7 @@ Section MapFoldResults. Lemma MapFold_Put_behind_disjoint : forall (f:ad -> A -> M) (m:Map A) (a:ad) (y:A), - MapGet A m a = NONE A -> + MapGet A m a = None -> MapFold A M neutral op f (MapPut_behind A m a y) = op (f a y) (MapFold A M neutral op f m). Proof. @@ -245,8 +246,8 @@ Section MapFoldResults. simple induction m2. intros. simpl in |- *. rewrite nright. reflexivity. intros. unfold MapMerge in |- *. rewrite (MapFold_Put_disjoint_2 f (M2 A m m0) a a0 pf). apply comm. apply in_dom_none. exact (MapDisjoint_M1_r _ _ (M2 A m m0) a a0 H1). - intros. simpl in |- *. rewrite (H m3 (fun a0:ad => pf (ad_double a0))). - rewrite (H0 m4 (fun a0:ad => pf (ad_double_plus_un a0))). + intros. simpl in |- *. rewrite (H m3 (fun a0:ad => pf (Ndouble a0))). + rewrite (H0 m4 (fun a0:ad => pf (Ndouble_plus_one a0))). cut (forall a b c d:M, op (op a b) (op c d) = op (op a c) (op b d)). intro. apply H4. intros. rewrite assoc. rewrite <- (assoc b c d). rewrite (comm b c). rewrite (assoc c b d). rewrite assoc. reflexivity. @@ -346,22 +347,22 @@ Section MapFoldExists. forall (f:ad -> A -> bool) (m:Map A) (pf:ad -> ad), MapFold1 A bool false orb f pf m = match MapSweep1 A f pf m with - | SOME _ => true + | Some _ => true | _ => false end. Proof. simple induction m. trivial. intros a y pf. simpl in |- *. unfold MapSweep2 in |- *. case (f (pf a) y); reflexivity. - intros. simpl in |- *. rewrite (H (fun a0:ad => pf (ad_double a0))). - rewrite (H0 (fun a0:ad => pf (ad_double_plus_un a0))). - case (MapSweep1 A f (fun a0:ad => pf (ad_double a0)) m0); reflexivity. + intros. simpl in |- *. rewrite (H (fun a0:ad => pf (Ndouble a0))). + rewrite (H0 (fun a0:ad => pf (Ndouble_plus_one a0))). + case (MapSweep1 A f (fun a0:ad => pf (Ndouble a0)) m0); reflexivity. Qed. Lemma MapFold_orb : forall (f:ad -> A -> bool) (m:Map A), MapFold A bool false orb f m = match MapSweep A f m with - | SOME _ => true + | Some _ => true | _ => false end. Proof. @@ -381,7 +382,7 @@ Section DMergeDef. forall (m:Map (Map A)) (a:ad), in_dom A a (DMerge m) = match MapSweep _ (fun (_:ad) (m0:Map A) => in_dom A a m0) m with - | SOME _ => true + | Some _ => true | _ => false end. Proof. @@ -397,7 +398,7 @@ Section DMergeDef. forall (m:Map (Map A)) (a:ad), in_dom A a (DMerge m) = true -> {b : ad & - {m0 : Map A | MapGet _ m b = SOME _ m0 /\ in_dom A a m0 = true}}. + {m0 : Map A | MapGet _ m b = Some m0 /\ in_dom A a m0 = true}}. Proof. intros m a. rewrite in_dom_DMerge_1. elim @@ -411,7 +412,7 @@ Section DMergeDef. Lemma in_dom_DMerge_3 : forall (m:Map (Map A)) (a b:ad) (m0:Map A), - MapGet _ m a = SOME _ m0 -> + MapGet _ m a = Some m0 -> in_dom A b m0 = true -> in_dom A b (DMerge m) = true. Proof. intros m a b m0 H H0. rewrite in_dom_DMerge_1. diff --git a/theories/IntMap/Mapiter.v b/theories/IntMap/Mapiter.v index 31e98c49..a8ba7e39 100644 --- a/theories/IntMap/Mapiter.v +++ b/theories/IntMap/Mapiter.v @@ -5,14 +5,13 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Mapiter.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Mapiter.v 8733 2006-04-25 22:52:18Z letouzey $ i*) Require Import Bool. Require Import Sumbool. -Require Import ZArith. -Require Import Addr. -Require Import Adist. -Require Import Addec. +Require Import NArith. +Require Import Ndigits. +Require Import Ndec. Require Import Map. Require Import Mapaxioms. Require Import Fset. @@ -27,17 +26,17 @@ Section MapIter. Variable f : ad -> A -> bool. Definition MapSweep2 (a0:ad) (y:A) := - if f a0 y then SOME _ (a0, y) else NONE _. + if f a0 y then Some (a0, y) else None. Fixpoint MapSweep1 (pf:ad -> ad) (m:Map A) {struct m} : option (ad * A) := match m with - | M0 => NONE _ + | M0 => None | M1 a y => MapSweep2 (pf a) y | M2 m m' => - match MapSweep1 (fun a:ad => pf (ad_double a)) m with - | SOME r => SOME _ r - | NONE => MapSweep1 (fun a:ad => pf (ad_double_plus_un a)) m' + match MapSweep1 (fun a:ad => pf (Ndouble a)) m with + | Some r => Some r + | None => MapSweep1 (fun a:ad => pf (Ndouble_plus_one a)) m' end end. @@ -45,27 +44,27 @@ Section MapIter. Lemma MapSweep_semantics_1_1 : forall (m:Map A) (pf:ad -> ad) (a:ad) (y:A), - MapSweep1 pf m = SOME _ (a, y) -> f a y = true. + MapSweep1 pf m = Some (a, y) -> f a y = true. Proof. simple induction m. intros. discriminate H. simpl in |- *. intros a y pf a0 y0. elim (sumbool_of_bool (f (pf a) y)). intro H. unfold MapSweep2 in |- *. rewrite H. intro H0. inversion H0. rewrite <- H3. assumption. intro H. unfold MapSweep2 in |- *. rewrite H. intro H0. discriminate H0. - simpl in |- *. intros. elim (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (ad_double a0)) m0)). + simpl in |- *. intros. elim (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (Ndouble a0)) m0)). intro H2. elim H2. intros r H3. rewrite H3 in H1. inversion H1. rewrite H5 in H3. - exact (H (fun a0:ad => pf (ad_double a0)) a y H3). - intro H2. rewrite H2 in H1. exact (H0 (fun a0:ad => pf (ad_double_plus_un a0)) a y H1). + exact (H (fun a0:ad => pf (Ndouble a0)) a y H3). + intro H2. rewrite H2 in H1. exact (H0 (fun a0:ad => pf (Ndouble_plus_one a0)) a y H1). Qed. Lemma MapSweep_semantics_1 : - forall (m:Map A) (a:ad) (y:A), MapSweep m = SOME _ (a, y) -> f a y = true. + forall (m:Map A) (a:ad) (y:A), MapSweep m = Some (a, y) -> f a y = true. Proof. intros. exact (MapSweep_semantics_1_1 m (fun a:ad => a) a y H). Qed. Lemma MapSweep_semantics_2_1 : forall (m:Map A) (pf:ad -> ad) (a:ad) (y:A), - MapSweep1 pf m = SOME _ (a, y) -> {a' : ad | a = pf a'}. + MapSweep1 pf m = Some (a, y) -> {a' : ad | a = pf a'}. Proof. simple induction m. intros. discriminate H. simpl in |- *. unfold MapSweep2 in |- *. intros a y pf a0 y0. case (f (pf a) y). intros. split with a. @@ -73,63 +72,63 @@ Section MapIter. intro. discriminate H. intros m0 H m1 H0 pf a y. simpl in |- *. elim - (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (ad_double a0)) m0)). intro H1. elim H1. + (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (Ndouble a0)) m0)). intro H1. elim H1. intros r H2. rewrite H2. intro H3. inversion H3. rewrite H5 in H2. - elim (H (fun a0:ad => pf (ad_double a0)) a y H2). intros a0 H6. split with (ad_double a0). + elim (H (fun a0:ad => pf (Ndouble a0)) a y H2). intros a0 H6. split with (Ndouble a0). assumption. - intro H1. rewrite H1. intro H2. elim (H0 (fun a0:ad => pf (ad_double_plus_un a0)) a y H2). - intros a0 H3. split with (ad_double_plus_un a0). assumption. + intro H1. rewrite H1. intro H2. elim (H0 (fun a0:ad => pf (Ndouble_plus_one a0)) a y H2). + intros a0 H3. split with (Ndouble_plus_one a0). assumption. Qed. Lemma MapSweep_semantics_2_2 : forall (m:Map A) (pf fp:ad -> ad), (forall a0:ad, fp (pf a0) = a0) -> forall (a:ad) (y:A), - MapSweep1 pf m = SOME _ (a, y) -> MapGet A m (fp a) = SOME _ y. + MapSweep1 pf m = Some (a, y) -> MapGet A m (fp a) = Some y. Proof. simple induction m. intros. discriminate H0. simpl in |- *. intros a y pf fp H a0 y0. unfold MapSweep2 in |- *. elim (sumbool_of_bool (f (pf a) y)). - intro H0. rewrite H0. intro H1. inversion H1. rewrite (H a). rewrite (ad_eq_correct a). + intro H0. rewrite H0. intro H1. inversion H1. rewrite (H a). rewrite (Neqb_correct a). reflexivity. intro H0. rewrite H0. intro H1. discriminate H1. - intros. rewrite (MapGet_M2_bit_0_if A m0 m1 (fp a)). elim (sumbool_of_bool (ad_bit_0 (fp a))). - intro H3. rewrite H3. elim (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (ad_double a0)) m0)). + intros. rewrite (MapGet_M2_bit_0_if A m0 m1 (fp a)). elim (sumbool_of_bool (Nbit0 (fp a))). + intro H3. rewrite H3. elim (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (Ndouble a0)) m0)). intro H4. simpl in H2. apply - (H0 (fun a0:ad => pf (ad_double_plus_un a0)) - (fun a0:ad => ad_div_2 (fp a0))). - intro. rewrite H1. apply ad_double_plus_un_div_2. + (H0 (fun a0:ad => pf (Ndouble_plus_one a0)) + (fun a0:ad => Ndiv2 (fp a0))). + intro. rewrite H1. apply Ndouble_plus_one_div2. elim - (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (ad_double a0)) m0)). intro H5. elim H5. + (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (Ndouble a0)) m0)). intro H5. elim H5. intros r H6. rewrite H6 in H2. inversion H2. rewrite H8 in H6. - elim (MapSweep_semantics_2_1 m0 (fun a0:ad => pf (ad_double a0)) a y H6). intros a0 H9. - rewrite H9 in H3. rewrite (H1 (ad_double a0)) in H3. rewrite (ad_double_bit_0 a0) in H3. + elim (MapSweep_semantics_2_1 m0 (fun a0:ad => pf (Ndouble a0)) a y H6). intros a0 H9. + rewrite H9 in H3. rewrite (H1 (Ndouble a0)) in H3. rewrite (Ndouble_bit0 a0) in H3. discriminate H3. intro H5. rewrite H5 in H2. assumption. intro H4. simpl in H2. rewrite H4 in H2. apply - (H0 (fun a0:ad => pf (ad_double_plus_un a0)) - (fun a0:ad => ad_div_2 (fp a0))). intro. - rewrite H1. apply ad_double_plus_un_div_2. + (H0 (fun a0:ad => pf (Ndouble_plus_one a0)) + (fun a0:ad => Ndiv2 (fp a0))). intro. + rewrite H1. apply Ndouble_plus_one_div2. assumption. intro H3. rewrite H3. simpl in H2. elim - (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (ad_double a0)) m0)). intro H4. elim H4. + (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (Ndouble a0)) m0)). intro H4. elim H4. intros r H5. rewrite H5 in H2. inversion H2. rewrite H7 in H5. apply - (H (fun a0:ad => pf (ad_double a0)) (fun a0:ad => ad_div_2 (fp a0))). intro. rewrite H1. - apply ad_double_div_2. + (H (fun a0:ad => pf (Ndouble a0)) (fun a0:ad => Ndiv2 (fp a0))). intro. rewrite H1. + apply Ndouble_div2. assumption. intro H4. rewrite H4 in H2. elim - (MapSweep_semantics_2_1 m1 (fun a0:ad => pf (ad_double_plus_un a0)) a y + (MapSweep_semantics_2_1 m1 (fun a0:ad => pf (Ndouble_plus_one a0)) a y H2). - intros a0 H5. rewrite H5 in H3. rewrite (H1 (ad_double_plus_un a0)) in H3. - rewrite (ad_double_plus_un_bit_0 a0) in H3. discriminate H3. + intros a0 H5. rewrite H5 in H3. rewrite (H1 (Ndouble_plus_one a0)) in H3. + rewrite (Ndouble_plus_one_bit0 a0) in H3. discriminate H3. Qed. Lemma MapSweep_semantics_2 : forall (m:Map A) (a:ad) (y:A), - MapSweep m = SOME _ (a, y) -> MapGet A m a = SOME _ y. + MapSweep m = Some (a, y) -> MapGet A m a = Some y. Proof. intros. exact @@ -139,28 +138,28 @@ Section MapIter. Lemma MapSweep_semantics_3_1 : forall (m:Map A) (pf:ad -> ad), - MapSweep1 pf m = NONE _ -> - forall (a:ad) (y:A), MapGet A m a = SOME _ y -> f (pf a) y = false. + MapSweep1 pf m = None -> + forall (a:ad) (y:A), MapGet A m a = Some y -> f (pf a) y = false. Proof. simple induction m. intros. discriminate H0. simpl in |- *. unfold MapSweep2 in |- *. intros a y pf. elim (sumbool_of_bool (f (pf a) y)). intro H. rewrite H. intro. discriminate H0. - intro H. rewrite H. intros H0 a0 y0. elim (sumbool_of_bool (ad_eq a a0)). intro H1. rewrite H1. - intro H2. inversion H2. rewrite <- H4. rewrite <- (ad_eq_complete _ _ H1). assumption. + intro H. rewrite H. intros H0 a0 y0. elim (sumbool_of_bool (Neqb a a0)). intro H1. rewrite H1. + intro H2. inversion H2. rewrite <- H4. rewrite <- (Neqb_complete _ _ H1). assumption. intro H1. rewrite H1. intro. discriminate H2. - intros. simpl in H1. elim (option_sum (ad * A) (MapSweep1 (fun a:ad => pf (ad_double a)) m0)). + intros. simpl in H1. elim (option_sum (ad * A) (MapSweep1 (fun a:ad => pf (Ndouble a)) m0)). intro H3. elim H3. intros r H4. rewrite H4 in H1. discriminate H1. - intro H3. rewrite H3 in H1. elim (sumbool_of_bool (ad_bit_0 a)). intro H4. - rewrite (MapGet_M2_bit_0_1 A a H4 m0 m1) in H2. rewrite <- (ad_div_2_double_plus_un a H4). - exact (H0 (fun a:ad => pf (ad_double_plus_un a)) H1 (ad_div_2 a) y H2). - intro H4. rewrite (MapGet_M2_bit_0_0 A a H4 m0 m1) in H2. rewrite <- (ad_div_2_double a H4). - exact (H (fun a:ad => pf (ad_double a)) H3 (ad_div_2 a) y H2). + intro H3. rewrite H3 in H1. elim (sumbool_of_bool (Nbit0 a)). intro H4. + rewrite (MapGet_M2_bit_0_1 A a H4 m0 m1) in H2. rewrite <- (Ndiv2_double_plus_one a H4). + exact (H0 (fun a:ad => pf (Ndouble_plus_one a)) H1 (Ndiv2 a) y H2). + intro H4. rewrite (MapGet_M2_bit_0_0 A a H4 m0 m1) in H2. rewrite <- (Ndiv2_double a H4). + exact (H (fun a:ad => pf (Ndouble a)) H3 (Ndiv2 a) y H2). Qed. Lemma MapSweep_semantics_3 : forall m:Map A, - MapSweep m = NONE _ -> - forall (a:ad) (y:A), MapGet A m a = SOME _ y -> f a y = false. + MapSweep m = None -> + forall (a:ad) (y:A), MapGet A m a = Some y -> f a y = false. Proof. intros. exact (MapSweep_semantics_3_1 m (fun a0:ad => a0) H a y H0). @@ -168,36 +167,36 @@ Section MapIter. Lemma MapSweep_semantics_4_1 : forall (m:Map A) (pf:ad -> ad) (a:ad) (y:A), - MapGet A m a = SOME A y -> + MapGet A m a = Some y -> f (pf a) y = true -> - {a' : ad & {y' : A | MapSweep1 pf m = SOME _ (a', y')}}. + {a' : ad & {y' : A | MapSweep1 pf m = Some (a', y')}}. Proof. simple induction m. intros. discriminate H. - intros. elim (sumbool_of_bool (ad_eq a a1)). intro H1. split with (pf a1). split with y. - rewrite (ad_eq_complete _ _ H1). unfold MapSweep1, MapSweep2 in |- *. - rewrite (ad_eq_complete _ _ H1) in H. rewrite (M1_semantics_1 _ a1 a0) in H. + intros. elim (sumbool_of_bool (Neqb a a1)). intro H1. split with (pf a1). split with y. + rewrite (Neqb_complete _ _ H1). unfold MapSweep1, MapSweep2 in |- *. + rewrite (Neqb_complete _ _ H1) in H. rewrite (M1_semantics_1 _ a1 a0) in H. inversion H. rewrite H0. reflexivity. intro H1. rewrite (M1_semantics_2 _ a a1 a0 H1) in H. discriminate H. - intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H3. + intros. elim (sumbool_of_bool (Nbit0 a)). intro H3. rewrite (MapGet_M2_bit_0_1 _ _ H3 m0 m1) in H1. - rewrite <- (ad_div_2_double_plus_un a H3) in H2. - elim (H0 (fun a0:ad => pf (ad_double_plus_un a0)) (ad_div_2 a) y H1 H2). intros a'' H4. elim H4. - intros y'' H5. simpl in |- *. elim (option_sum _ (MapSweep1 (fun a:ad => pf (ad_double a)) m0)). + rewrite <- (Ndiv2_double_plus_one a H3) in H2. + elim (H0 (fun a0:ad => pf (Ndouble_plus_one a0)) (Ndiv2 a) y H1 H2). intros a'' H4. elim H4. + intros y'' H5. simpl in |- *. elim (option_sum _ (MapSweep1 (fun a:ad => pf (Ndouble a)) m0)). intro H6. elim H6. intro r. elim r. intros a''' y''' H7. rewrite H7. split with a'''. split with y'''. reflexivity. intro H6. rewrite H6. split with a''. split with y''. assumption. intro H3. rewrite (MapGet_M2_bit_0_0 _ _ H3 m0 m1) in H1. - rewrite <- (ad_div_2_double a H3) in H2. - elim (H (fun a0:ad => pf (ad_double a0)) (ad_div_2 a) y H1 H2). intros a'' H4. elim H4. + rewrite <- (Ndiv2_double a H3) in H2. + elim (H (fun a0:ad => pf (Ndouble a0)) (Ndiv2 a) y H1 H2). intros a'' H4. elim H4. intros y'' H5. split with a''. split with y''. simpl in |- *. rewrite H5. reflexivity. Qed. Lemma MapSweep_semantics_4 : forall (m:Map A) (a:ad) (y:A), - MapGet A m a = SOME A y -> - f a y = true -> {a' : ad & {y' : A | MapSweep m = SOME _ (a', y')}}. + MapGet A m a = Some y -> + f a y = true -> {a' : ad & {y' : A | MapSweep m = Some (a', y')}}. Proof. intros. exact (MapSweep_semantics_4_1 m (fun a0:ad => a0) a y H H0). Qed. @@ -212,8 +211,8 @@ Section MapIter. | M0 => M0 B | M1 a y => f (pf a) y | M2 m1 m2 => - MapMerge B (MapCollect1 f (fun a0:ad => pf (ad_double a0)) m1) - (MapCollect1 f (fun a0:ad => pf (ad_double_plus_un a0)) m2) + MapMerge B (MapCollect1 f (fun a0:ad => pf (Ndouble a0)) m1) + (MapCollect1 f (fun a0:ad => pf (Ndouble_plus_one a0)) m2) end. Definition MapCollect (f:ad -> A -> Map B) (m:Map A) := @@ -231,8 +230,8 @@ Section MapIter. | M0 => neutral | M1 a y => f (pf a) y | M2 m1 m2 => - op (MapFold1 f (fun a0:ad => pf (ad_double a0)) m1) - (MapFold1 f (fun a0:ad => pf (ad_double_plus_un a0)) m2) + op (MapFold1 f (fun a0:ad => pf (Ndouble a0)) m1) + (MapFold1 f (fun a0:ad => pf (Ndouble_plus_one a0)) m2) end. Definition MapFold (f:ad -> A -> M) (m:Map A) := @@ -258,11 +257,11 @@ Section MapIter. | M0 => (state, neutral) | M1 a y => f state (pf a) y | M2 m1 m2 => - match MapFold1_state state (fun a0:ad => pf (ad_double a0)) m1 with + match MapFold1_state state (fun a0:ad => pf (Ndouble a0)) m1 with | (state1, x1) => match MapFold1_state state1 - (fun a0:ad => pf (ad_double_plus_un a0)) m2 + (fun a0:ad => pf (Ndouble_plus_one a0)) m2 with | (state2, x2) => (state2, op x1 x2) end @@ -285,19 +284,19 @@ Section MapIter. simple induction m. trivial. intros. simpl in |- *. apply H. intros. simpl in |- *. rewrite - (pair_sp _ _ (MapFold1_state state (fun a0:ad => pf (ad_double a0)) m0)) + (pair_sp _ _ (MapFold1_state state (fun a0:ad => pf (Ndouble a0)) m0)) . - rewrite (H g (fun a0:ad => pf (ad_double a0)) H1 state). + rewrite (H g (fun a0:ad => pf (Ndouble a0)) H1 state). rewrite (pair_sp _ _ (MapFold1_state - (fst (MapFold1_state state (fun a0:ad => pf (ad_double a0)) m0)) - (fun a0:ad => pf (ad_double_plus_un a0)) m1)) + (fst (MapFold1_state state (fun a0:ad => pf (Ndouble a0)) m0)) + (fun a0:ad => pf (Ndouble_plus_one a0)) m1)) . simpl in |- *. rewrite - (H0 g (fun a0:ad => pf (ad_double_plus_un a0)) H1 - (fst (MapFold1_state state (fun a0:ad => pf (ad_double a0)) m0))) + (H0 g (fun a0:ad => pf (Ndouble_plus_one a0)) H1 + (fst (MapFold1_state state (fun a0:ad => pf (Ndouble a0)) m0))) . reflexivity. Qed. @@ -330,21 +329,21 @@ Section MapIter. Fixpoint alist_semantics (l:alist) : ad -> option A := match l with - | nil => fun _:ad => NONE A + | nil => fun _:ad => None | (a, y) :: l' => - fun a0:ad => if ad_eq a a0 then SOME A y else alist_semantics l' a0 + fun a0:ad => if Neqb a a0 then Some y else alist_semantics l' a0 end. Lemma alist_semantics_app : forall (l l':alist) (a:ad), alist_semantics (aapp l l') a = match alist_semantics l a with - | NONE => alist_semantics l' a - | SOME y => SOME A y + | None => alist_semantics l' a + | Some y => Some y end. Proof. unfold aapp in |- *. simple induction l. trivial. - intros. elim a. intros a1 y1. simpl in |- *. case (ad_eq a1 a0). reflexivity. + intros. elim a. intros a1 y1. simpl in |- *. case (Neqb a1 a0). reflexivity. apply H. Qed. @@ -352,53 +351,53 @@ Section MapIter. forall (m:Map A) (pf:ad -> ad) (a:ad) (y:A), alist_semantics (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil) pf - m) a = SOME A y -> {a' : ad | a = pf a'}. + m) a = Some y -> {a' : ad | a = pf a'}. Proof. simple induction m. simpl in |- *. intros. discriminate H. - simpl in |- *. intros a y pf a0 y0. elim (sumbool_of_bool (ad_eq (pf a) a0)). intro H. rewrite H. - intro H0. split with a. rewrite (ad_eq_complete _ _ H). reflexivity. + simpl in |- *. intros a y pf a0 y0. elim (sumbool_of_bool (Neqb (pf a) a0)). intro H. rewrite H. + intro H0. split with a. rewrite (Neqb_complete _ _ H). reflexivity. intro H. rewrite H. intro H0. discriminate H0. intros. change (alist_semantics (aapp (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil) - (fun a0:ad => pf (ad_double a0)) m0) + (fun a0:ad => pf (Ndouble a0)) m0) (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil) - (fun a0:ad => pf (ad_double_plus_un a0)) m1)) a = - SOME A y) in H1. + (fun a0:ad => pf (Ndouble_plus_one a0)) m1)) a = + Some y) in H1. rewrite (alist_semantics_app (MapFold1 alist anil aapp (fun (a0:ad) (y0:A) => acons (a0, y0) anil) - (fun a0:ad => pf (ad_double a0)) m0) + (fun a0:ad => pf (Ndouble a0)) m0) (MapFold1 alist anil aapp (fun (a0:ad) (y0:A) => acons (a0, y0) anil) - (fun a0:ad => pf (ad_double_plus_un a0)) m1) a) + (fun a0:ad => pf (Ndouble_plus_one a0)) m1) a) in H1. elim (option_sum A (alist_semantics (MapFold1 alist anil aapp (fun (a0:ad) (y0:A) => acons (a0, y0) anil) - (fun a0:ad => pf (ad_double a0)) m0) a)). - intro H2. elim H2. intros y0 H3. elim (H (fun a0:ad => pf (ad_double a0)) a y0 H3). intros a0 H4. - split with (ad_double a0). assumption. - intro H2. rewrite H2 in H1. elim (H0 (fun a0:ad => pf (ad_double_plus_un a0)) a y H1). - intros a0 H3. split with (ad_double_plus_un a0). assumption. + (fun a0:ad => pf (Ndouble a0)) m0) a)). + intro H2. elim H2. intros y0 H3. elim (H (fun a0:ad => pf (Ndouble a0)) a y0 H3). intros a0 H4. + split with (Ndouble a0). assumption. + intro H2. rewrite H2 in H1. elim (H0 (fun a0:ad => pf (Ndouble_plus_one a0)) a y H1). + intros a0 H3. split with (Ndouble_plus_one a0). assumption. Qed. Definition ad_inj (pf:ad -> ad) := forall a0 a1:ad, pf a0 = pf a1 -> a0 = a1. Lemma ad_comp_double_inj : - forall pf:ad -> ad, ad_inj pf -> ad_inj (fun a0:ad => pf (ad_double a0)). + forall pf:ad -> ad, ad_inj pf -> ad_inj (fun a0:ad => pf (Ndouble a0)). Proof. - unfold ad_inj in |- *. intros. apply ad_double_inj. exact (H _ _ H0). + unfold ad_inj in |- *. intros. apply Ndouble_inj. exact (H _ _ H0). Qed. Lemma ad_comp_double_plus_un_inj : forall pf:ad -> ad, - ad_inj pf -> ad_inj (fun a0:ad => pf (ad_double_plus_un a0)). + ad_inj pf -> ad_inj (fun a0:ad => pf (Ndouble_plus_one a0)). Proof. - unfold ad_inj in |- *. intros. apply ad_double_plus_un_inj. exact (H _ _ H0). + unfold ad_inj in |- *. intros. apply Ndouble_plus_one_inj. exact (H _ _ H0). Qed. Lemma alist_of_Map_semantics_1 : @@ -411,10 +410,10 @@ Section MapIter. pf m) (pf a). Proof. simple induction m. trivial. - simpl in |- *. intros. elim (sumbool_of_bool (ad_eq a a1)). intro H0. rewrite H0. - rewrite (ad_eq_complete _ _ H0). rewrite (ad_eq_correct (pf a1)). reflexivity. - intro H0. rewrite H0. elim (sumbool_of_bool (ad_eq (pf a) (pf a1))). intro H1. - rewrite (H a a1 (ad_eq_complete _ _ H1)) in H0. rewrite (ad_eq_correct a1) in H0. + simpl in |- *. intros. elim (sumbool_of_bool (Neqb a a1)). intro H0. rewrite H0. + rewrite (Neqb_complete _ _ H0). rewrite (Neqb_correct (pf a1)). reflexivity. + intro H0. rewrite H0. elim (sumbool_of_bool (Neqb (pf a) (pf a1))). intro H1. + rewrite (H a a1 (Neqb_complete _ _ H1)) in H0. rewrite (Neqb_correct a1) in H0. discriminate H0. intro H1. rewrite H1. reflexivity. intros. change @@ -422,54 +421,53 @@ Section MapIter. alist_semantics (aapp (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil) - (fun a0:ad => pf (ad_double a0)) m0) + (fun a0:ad => pf (Ndouble a0)) m0) (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil) - (fun a0:ad => pf (ad_double_plus_un a0)) m1)) ( + (fun a0:ad => pf (Ndouble_plus_one a0)) m1)) ( pf a)) in |- *. rewrite alist_semantics_app. rewrite (MapGet_M2_bit_0_if A m0 m1 a). - elim (ad_double_or_double_plus_un a). intro H2. elim H2. intros a0 H3. rewrite H3. - rewrite (ad_double_bit_0 a0). + elim (Ndouble_or_double_plus_un a). intro H2. elim H2. intros a0 H3. rewrite H3. + rewrite (Ndouble_bit0 a0). rewrite <- - (H (fun a1:ad => pf (ad_double a1)) (ad_comp_double_inj pf H1) a0) + (H (fun a1:ad => pf (Ndouble a1)) (ad_comp_double_inj pf H1) a0) . - rewrite ad_double_div_2. case (MapGet A m0 a0). + rewrite Ndouble_div2. case (MapGet A m0 a0); trivial. elim (option_sum A (alist_semantics (MapFold1 alist anil aapp (fun (a1:ad) (y:A) => acons (a1, y) anil) - (fun a1:ad => pf (ad_double_plus_un a1)) m1) - (pf (ad_double a0)))). + (fun a1:ad => pf (Ndouble_plus_one a1)) m1) + (pf (Ndouble a0)))). intro H4. elim H4. intros y H5. elim - (alist_of_Map_semantics_1_1 m1 (fun a1:ad => pf (ad_double_plus_un a1)) - (pf (ad_double a0)) y H5). - intros a1 H6. cut (ad_bit_0 (ad_double a0) = ad_bit_0 (ad_double_plus_un a1)). - intro. rewrite (ad_double_bit_0 a0) in H7. rewrite (ad_double_plus_un_bit_0 a1) in H7. + (alist_of_Map_semantics_1_1 m1 (fun a1:ad => pf (Ndouble_plus_one a1)) + (pf (Ndouble a0)) y H5). + intros a1 H6. cut (Nbit0 (Ndouble a0) = Nbit0 (Ndouble_plus_one a1)). + intro. rewrite (Ndouble_bit0 a0) in H7. rewrite (Ndouble_plus_one_bit0 a1) in H7. discriminate H7. - rewrite (H1 (ad_double a0) (ad_double_plus_un a1) H6). reflexivity. + rewrite (H1 (Ndouble a0) (Ndouble_plus_one a1) H6). reflexivity. intro H4. rewrite H4. reflexivity. - trivial. - intro H2. elim H2. intros a0 H3. rewrite H3. rewrite (ad_double_plus_un_bit_0 a0). + intro H2. elim H2. intros a0 H3. rewrite H3. rewrite (Ndouble_plus_one_bit0 a0). rewrite <- - (H0 (fun a1:ad => pf (ad_double_plus_un a1)) + (H0 (fun a1:ad => pf (Ndouble_plus_one a1)) (ad_comp_double_plus_un_inj pf H1) a0). - rewrite ad_double_plus_un_div_2. + rewrite Ndouble_plus_one_div2. elim (option_sum A (alist_semantics (MapFold1 alist anil aapp (fun (a1:ad) (y:A) => acons (a1, y) anil) - (fun a1:ad => pf (ad_double a1)) m0) - (pf (ad_double_plus_un a0)))). + (fun a1:ad => pf (Ndouble a1)) m0) + (pf (Ndouble_plus_one a0)))). intro H4. elim H4. intros y H5. elim - (alist_of_Map_semantics_1_1 m0 (fun a1:ad => pf (ad_double a1)) - (pf (ad_double_plus_un a0)) y H5). - intros a1 H6. cut (ad_bit_0 (ad_double_plus_un a0) = ad_bit_0 (ad_double a1)). - intro H7. rewrite (ad_double_plus_un_bit_0 a0) in H7. rewrite (ad_double_bit_0 a1) in H7. + (alist_of_Map_semantics_1_1 m0 (fun a1:ad => pf (Ndouble a1)) + (pf (Ndouble_plus_one a0)) y H5). + intros a1 H6. cut (Nbit0 (Ndouble_plus_one a0) = Nbit0 (Ndouble a1)). + intro H7. rewrite (Ndouble_plus_one_bit0 a0) in H7. rewrite (Ndouble_bit0 a1) in H7. discriminate H7. - rewrite (H1 (ad_double_plus_un a0) (ad_double a1) H6). reflexivity. + rewrite (H1 (Ndouble_plus_one a0) (Ndouble a1) H6). reflexivity. intro H4. rewrite H4. reflexivity. Qed. @@ -491,9 +489,9 @@ Section MapIter. forall l:alist, eqm A (alist_semantics l) (MapGet A (Map_of_alist l)). Proof. unfold eqm in |- *. simple induction l. trivial. - intros r l0 H a. elim r. intros a0 y0. simpl in |- *. elim (sumbool_of_bool (ad_eq a0 a)). - intro H0. rewrite H0. rewrite (ad_eq_complete _ _ H0). - rewrite (MapPut_semantics A (Map_of_alist l0) a y0 a). rewrite (ad_eq_correct a). + intros r l0 H a. elim r. intros a0 y0. simpl in |- *. elim (sumbool_of_bool (Neqb a0 a)). + intro H0. rewrite H0. rewrite (Neqb_complete _ _ H0). + rewrite (MapPut_semantics A (Map_of_alist l0) a y0 a). rewrite (Neqb_correct a). reflexivity. intro H0. rewrite H0. rewrite (MapPut_semantics A (Map_of_alist l0) a0 y0 a). rewrite H0. apply H. @@ -551,7 +549,7 @@ Section MapIter. simple induction m. trivial. intros. simpl in |- *. rewrite H1. reflexivity. intros. simpl in |- *. rewrite (fold_right_aapp M neutral op H H0 f). - rewrite (H2 (fun a0:ad => pf (ad_double a0))). rewrite (H3 (fun a0:ad => pf (ad_double_plus_un a0))). + rewrite (H2 (fun a0:ad => pf (Ndouble a0))). rewrite (H3 (fun a0:ad => pf (Ndouble_plus_one a0))). reflexivity. Qed. @@ -590,7 +588,7 @@ Section MapIter. rewrite <- (alist_of_Map_semantics (MapMerge A m m') a). rewrite (MapMerge_semantics A m m' a). elim (option_sum _ (MapGet A m a)). intro H0. elim H0. intros y H1. rewrite H1. elim (option_sum _ (MapGet A m' a)). intro H2. elim H2. intros y' H3. - cut (MapGet A (MapDomRestrTo A A m m') a = NONE A). + cut (MapGet A (MapDomRestrTo A A m m') a = None). rewrite (MapDomRestrTo_semantics A A m m' a). rewrite H3. rewrite H1. intro. discriminate H4. exact (H a). intro H2. rewrite H2. reflexivity. diff --git a/theories/IntMap/Maplists.v b/theories/IntMap/Maplists.v index 1d53e6e5..56a3c160 100644 --- a/theories/IntMap/Maplists.v +++ b/theories/IntMap/Maplists.v @@ -5,10 +5,11 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Maplists.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Maplists.v 8733 2006-04-25 22:52:18Z letouzey $ i*) -Require Import Addr. -Require Import Addec. +Require Import BinNat. +Require Import Ndigits. +Require Import Ndec. Require Import Map. Require Import Fset. Require Import Mapaxioms. @@ -28,7 +29,7 @@ Section MapLists. Fixpoint ad_in_list (a:ad) (l:list ad) {struct l} : bool := match l with | nil => false - | a' :: l' => orb (ad_eq a a') (ad_in_list a l') + | a' :: l' => orb (Neqb a a') (ad_in_list a l') end. Fixpoint ad_list_stutters (l:list ad) : bool := @@ -43,8 +44,8 @@ Section MapLists. {l1 : list ad & {l2 : list ad | l = l1 ++ x :: l2}}. Proof. simple induction l. intro. discriminate H. - intros. elim (sumbool_of_bool (ad_eq x a)). intro H1. simpl in H0. split with (nil (A:=ad)). - split with l0. rewrite (ad_eq_complete _ _ H1). reflexivity. + intros. elim (sumbool_of_bool (Neqb x a)). intro H1. simpl in H0. split with (nil (A:=ad)). + split with l0. rewrite (Neqb_complete _ _ H1). reflexivity. intro H2. simpl in H0. rewrite H2 in H0. simpl in H0. elim (H H0). intros l'1 H3. split with (a :: l'1). elim H3. intros l2 H4. split with l2. rewrite H4. reflexivity. Qed. @@ -223,7 +224,7 @@ Section MapLists. Lemma ad_in_list_app_1 : forall (l l':list ad) (x:ad), ad_in_list x (l ++ x :: l') = true. Proof. - simple induction l. simpl in |- *. intros. rewrite (ad_eq_correct x). reflexivity. + simple induction l. simpl in |- *. intros. rewrite (Neqb_correct x). reflexivity. intros. simpl in |- *. rewrite (H l' x). apply orb_b_true. Qed. @@ -353,18 +354,18 @@ Section MapLists. (fun (a:ad) (l:list ad) => ad_in_list a l) ( fun c:ad => refl_equal _) ad_in_list_app (fun (a0:ad) (_:A) => a0 :: nil) m a). - simpl in |- *. rewrite (MapFold_orb A (fun (a0:ad) (_:A) => orb (ad_eq a a0) false) m). + simpl in |- *. rewrite (MapFold_orb A (fun (a0:ad) (_:A) => orb (Neqb a a0) false) m). elim (option_sum _ - (MapSweep A (fun (a0:ad) (_:A) => orb (ad_eq a a0) false) m)). intro H. elim H. + (MapSweep A (fun (a0:ad) (_:A) => orb (Neqb a a0) false) m)). intro H. elim H. intro r. elim r. intros a0 y H0. rewrite H0. unfold in_dom in |- *. elim (orb_prop _ _ (MapSweep_semantics_1 _ _ _ _ _ H0)). intro H1. - rewrite (ad_eq_complete _ _ H1). rewrite (MapSweep_semantics_2 A _ _ _ _ H0). reflexivity. + rewrite (Neqb_complete _ _ H1). rewrite (MapSweep_semantics_2 A _ _ _ _ H0). reflexivity. intro H1. discriminate H1. intro H. rewrite H. elim (sumbool_of_bool (in_dom A a m)). intro H0. elim (in_dom_some A m a H0). intros y H1. elim (orb_false_elim _ _ (MapSweep_semantics_3 _ _ _ H _ _ H1)). intro H2. - rewrite (ad_eq_correct a) in H2. discriminate H2. + rewrite (Neqb_correct a) in H2. discriminate H2. exact (sym_eq (y:=_)). Qed. @@ -397,7 +398,7 @@ Section MapLists. pf m) = MapCard A m. Proof. simple induction m; try trivial. simpl in |- *. intros. rewrite ad_list_app_length. - rewrite (H (fun a0:ad => pf (ad_double a0))). rewrite (H0 (fun a0:ad => pf (ad_double_plus_un a0))). + rewrite (H (fun a0:ad => pf (Ndouble a0))). rewrite (H0 (fun a0:ad => pf (Ndouble_plus_one a0))). reflexivity. Qed. @@ -423,8 +424,8 @@ Section MapLists. MapFold1 unit (list ad) nil (app (A:=ad)) (fun (a:ad) (_:unit) => a :: nil) pf (MapDom A m). Proof. - simple induction m; try trivial. simpl in |- *. intros. rewrite (H (fun a0:ad => pf (ad_double a0))). - rewrite (H0 (fun a0:ad => pf (ad_double_plus_un a0))). reflexivity. + simple induction m; try trivial. simpl in |- *. intros. rewrite (H (fun a0:ad => pf (Ndouble a0))). + rewrite (H0 (fun a0:ad => pf (Ndouble_plus_one a0))). reflexivity. Qed. Lemma ad_list_of_dom_Dom : diff --git a/theories/IntMap/Mapsubset.v b/theories/IntMap/Mapsubset.v index e27943fb..6771c03e 100644 --- a/theories/IntMap/Mapsubset.v +++ b/theories/IntMap/Mapsubset.v @@ -5,15 +5,14 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Mapsubset.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Mapsubset.v 8733 2006-04-25 22:52:18Z letouzey $ i*) Require Import Bool. Require Import Sumbool. Require Import Arith. -Require Import ZArith. -Require Import Addr. -Require Import Adist. -Require Import Addec. +Require Import NArith. +Require Import Ndigits. +Require Import Ndec. Require Import Map. Require Import Fset. Require Import Mapaxioms. @@ -28,7 +27,7 @@ Section MapSubsetDef. Definition MapSubset_1 (m:Map A) (m':Map B) := match MapSweep A (fun (a:ad) (_:A) => negb (in_dom B a m')) m with - | NONE => true + | None => true | _ => false end. @@ -76,10 +75,10 @@ Section MapSubsetDef. unfold eqmap, eqm, in_dom in |- *. intros. cut (match MapGet A m a with - | NONE => false - | SOME _ => true + | None => false + | Some _ => true end = false). - case (MapGet A m a). trivial. + case (MapGet A m a); trivial. intros. discriminate H0. exact (H a). Qed. @@ -346,7 +345,7 @@ Section MapDisjointDef. Definition MapDisjoint_1 (m:Map A) (m':Map B) := match MapSweep A (fun (a:ad) (_:A) => in_dom B a m') m with - | NONE => true + | None => true | _ => false end. @@ -395,7 +394,7 @@ Section MapDisjointDef. Proof. unfold MapDisjoint, MapDisjoint_2 in |- *. unfold eqmap, eqm in |- *. intros. elim (in_dom_some _ _ _ H0). intros y H2. elim (in_dom_some _ _ _ H1). intros y' H3. - cut (MapGet A (MapDomRestrTo A B m m') a = NONE A). intro. + cut (MapGet A (MapDomRestrTo A B m m') a = None). intro. rewrite (MapDomRestrTo_semantics _ _ m m' a) in H4. rewrite H3 in H4. rewrite H2 in H4. discriminate H4. exact (H a). @@ -449,11 +448,11 @@ Section MapDisjointExtra. Proof. unfold MapDisjoint, in_dom in |- *. intros. elim (option_sum _ (MapGet A m0 a)). intro H2. elim H2. intros y H3. elim (option_sum _ (MapGet B m2 a)). intro H4. elim H4. - intros y' H5. apply (H (ad_double a)). - rewrite (MapGet_M2_bit_0_0 _ (ad_double a) (ad_double_bit_0 a) m0 m1). - rewrite (ad_double_div_2 a). rewrite H3. reflexivity. - rewrite (MapGet_M2_bit_0_0 _ (ad_double a) (ad_double_bit_0 a) m2 m3). - rewrite (ad_double_div_2 a). rewrite H5. reflexivity. + intros y' H5. apply (H (Ndouble a)). + rewrite (MapGet_M2_bit_0_0 _ (Ndouble a) (Ndouble_bit0 a) m0 m1). + rewrite (Ndouble_div2 a). rewrite H3. reflexivity. + rewrite (MapGet_M2_bit_0_0 _ (Ndouble a) (Ndouble_bit0 a) m2 m3). + rewrite (Ndouble_div2 a). rewrite H5. reflexivity. intro H4. rewrite H4 in H1. discriminate H1. intro H2. rewrite H2 in H0. discriminate H0. Qed. @@ -464,15 +463,15 @@ Section MapDisjointExtra. Proof. unfold MapDisjoint, in_dom in |- *. intros. elim (option_sum _ (MapGet A m1 a)). intro H2. elim H2. intros y H3. elim (option_sum _ (MapGet B m3 a)). intro H4. elim H4. - intros y' H5. apply (H (ad_double_plus_un a)). + intros y' H5. apply (H (Ndouble_plus_one a)). rewrite - (MapGet_M2_bit_0_1 _ (ad_double_plus_un a) (ad_double_plus_un_bit_0 a) + (MapGet_M2_bit_0_1 _ (Ndouble_plus_one a) (Ndouble_plus_one_bit0 a) m0 m1). - rewrite (ad_double_plus_un_div_2 a). rewrite H3. reflexivity. + rewrite (Ndouble_plus_one_div2 a). rewrite H3. reflexivity. rewrite - (MapGet_M2_bit_0_1 _ (ad_double_plus_un a) (ad_double_plus_un_bit_0 a) + (MapGet_M2_bit_0_1 _ (Ndouble_plus_one a) (Ndouble_plus_one_bit0 a) m2 m3). - rewrite (ad_double_plus_un_div_2 a). rewrite H5. reflexivity. + rewrite (Ndouble_plus_one_div2 a). rewrite H5. reflexivity. intro H4. rewrite H4 in H1. discriminate H1. intro H2. rewrite H2 in H0. discriminate H0. Qed. @@ -482,11 +481,11 @@ Section MapDisjointExtra. MapDisjoint A B m0 m2 -> MapDisjoint A B m1 m3 -> MapDisjoint A B (M2 A m0 m1) (M2 B m2 m3). Proof. - unfold MapDisjoint, in_dom in |- *. intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H3. + unfold MapDisjoint, in_dom in |- *. intros. elim (sumbool_of_bool (Nbit0 a)). intro H3. rewrite (MapGet_M2_bit_0_1 A a H3 m0 m1) in H1. - rewrite (MapGet_M2_bit_0_1 B a H3 m2 m3) in H2. exact (H0 (ad_div_2 a) H1 H2). + rewrite (MapGet_M2_bit_0_1 B a H3 m2 m3) in H2. exact (H0 (Ndiv2 a) H1 H2). intro H3. rewrite (MapGet_M2_bit_0_0 A a H3 m0 m1) in H1. - rewrite (MapGet_M2_bit_0_0 B a H3 m2 m3) in H2. exact (H (ad_div_2 a) H1 H2). + rewrite (MapGet_M2_bit_0_0 B a H3 m2 m3) in H2. exact (H (Ndiv2 a) H1 H2). Qed. Lemma MapDisjoint_M1_l : |