diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Camlcoq.ml | 12 | ||||
-rw-r--r-- | lib/Coqlib.v | 5 | ||||
-rw-r--r-- | lib/Fappli_IEEE_extra.v | 40 | ||||
-rw-r--r-- | lib/Floats.v | 21 | ||||
-rw-r--r-- | lib/Integers.v | 8 | ||||
-rw-r--r-- | lib/Intv.v | 6 | ||||
-rw-r--r-- | lib/Lattice.v | 34 | ||||
-rw-r--r-- | lib/Maps.v | 102 | ||||
-rw-r--r-- | lib/UnionFind.v | 98 | ||||
-rw-r--r-- | lib/Wfsimpl.v | 3 |
10 files changed, 156 insertions, 173 deletions
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 7e8a1018..5b5d37ee 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -56,8 +56,6 @@ module P = struct let one = Coq_xH let succ = Pos.succ let pred = Pos.pred - let add = Pos.add - let sub = Pos.sub let eq x y = (Pos.compare x y = Eq) let lt x y = (Pos.compare x y = Lt) let gt x y = (Pos.compare x y = Gt) @@ -106,8 +104,6 @@ module P = struct then Coq_xH else Coq_xI (of_int64 (Int64.shift_right_logical n 1)) - let (+) = add - let (-) = sub let (=) = eq let (<) = lt let (<=) = le @@ -124,11 +120,6 @@ module N = struct let zero = N0 let one = Npos Coq_xH - let succ = N.succ - let pred = N.pred - let add = N.add - let sub = N.sub - let mul = N.mul let eq x y = (N.compare x y = Eq) let lt x y = (N.compare x y = Lt) let gt x y = (N.compare x y = Gt) @@ -157,9 +148,6 @@ module N = struct let of_int64 n = if n = 0L then N0 else Npos (P.of_int64 n) - let (+) = add - let (-) = sub - let ( * ) = mul let (=) = eq let (<) = lt let (<=) = le diff --git a/lib/Coqlib.v b/lib/Coqlib.v index fc4a59f6..6fa82492 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -22,6 +22,8 @@ Require Export Znumtheory. Require Export List. Require Export Bool. +Global Set Asymmetric Patterns. + (** * Useful tactics *) Ltac inv H := inversion H; clear H; subst. @@ -768,7 +770,7 @@ Proof. discriminate. rewrite list_length_z_cons. destruct (zeq n 0). generalize (list_length_z_pos l); omega. - exploit IHl; eauto. unfold Zpred. omega. + exploit IHl; eauto. omega. Qed. (** Properties of [List.incl] (list inclusion). *) @@ -1431,4 +1433,3 @@ Lemma nlist_forall2_imply: Proof. induction 1; simpl; intros; constructor; auto. Qed. - diff --git a/lib/Fappli_IEEE_extra.v b/lib/Fappli_IEEE_extra.v index fe7f7c6d..f5ccec2a 100644 --- a/lib/Fappli_IEEE_extra.v +++ b/lib/Fappli_IEEE_extra.v @@ -63,10 +63,10 @@ Qed. Definition is_finite_pos0 (f: binary_float) : bool := match f with - | B754_zero s => negb s - | B754_infinity _ => false - | B754_nan _ _ => false - | B754_finite _ _ _ _ => true + | B754_zero _ _ s => negb s + | B754_infinity _ _ _ => false + | B754_nan _ _ _ _ => false + | B754_finite _ _ _ _ _ _ => true end. Lemma Bsign_pos0: @@ -693,10 +693,10 @@ Qed. Definition ZofB (f: binary_float): option Z := match f with - | B754_finite s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Zpower_pos radix2 e)%Z - | B754_finite s m 0 _ => Some (cond_Zopp s (Zpos m)) - | B754_finite s m (Zneg e) _ => Some (cond_Zopp s (Zpos m / Zpower_pos radix2 e))%Z - | B754_zero _ => Some 0%Z + | B754_finite _ _ s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Zpower_pos radix2 e)%Z + | B754_finite _ _ s m 0 _ => Some (cond_Zopp s (Zpos m)) + | B754_finite _ _ s m (Zneg e) _ => Some (cond_Zopp s (Zpos m / Zpower_pos radix2 e))%Z + | B754_zero _ _ _ => Some 0%Z | _ => None end. @@ -949,7 +949,9 @@ Proof. - revert H H0. fold emin. fold fexp. set (x := B754_finite prec emax b0 m0 e1 e2). set (rx := B2R _ _ x). set (y := B754_finite prec emax b m e e0). set (ry := B2R _ _ y). - rewrite (Rmult_comm ry rx). destruct Rlt_bool. + rewrite (Rmult_comm ry rx). + destruct (Rlt_bool (Rabs (round radix2 fexp (round_mode mode) (rx * ry))) + (bpow radix2 emax)). + intros (A1 & A2 & A3) (B1 & B2 & B3). apply B2R_Bsign_inj; auto. rewrite <- B1 in A1. auto. rewrite ! Bsign_FF2B. f_equal. f_equal. apply xorb_comm. apply Pos.mul_comm. apply Z.add_comm. @@ -1002,9 +1004,9 @@ Definition Bexact_inverse_mantissa := Z.iter (prec - 1) xO xH. Remark Bexact_inverse_mantissa_value: Zpos Bexact_inverse_mantissa = 2 ^ (prec - 1). Proof. - assert (REC: forall n, Z.pos (nat_iter n xO xH) = 2 ^ (Z.of_nat n)). + assert (REC: forall n, Z.pos (nat_rect _ xH (fun _ => xO) n) = 2 ^ (Z.of_nat n)). { induction n. reflexivity. - simpl nat_iter. transitivity (2 * Z.pos (nat_iter n xO xH)). reflexivity. + simpl nat_rect. transitivity (2 * Z.pos (nat_rect _ xH (fun _ => xO) n)). reflexivity. rewrite inj_S. rewrite IHn. unfold Z.succ. rewrite Zpower_plus by omega. change (2 ^ 1) with 2. ring. } red in prec_gt_0_. @@ -1015,12 +1017,12 @@ Qed. Remark Bexact_inverse_mantissa_digits2_pos: Z.pos (digits2_pos Bexact_inverse_mantissa) = prec. Proof. - assert (DIGITS: forall n, digits2_pos (nat_iter n xO xH) = Pos.of_nat (n+1)). + assert (DIGITS: forall n, digits2_pos (nat_rect _ xH (fun _ => xO) n) = Pos.of_nat (n+1)). { induction n; simpl. auto. rewrite IHn. destruct n; auto. } red in prec_gt_0_. unfold Bexact_inverse_mantissa. rewrite iter_nat_of_Z by omega. rewrite DIGITS. rewrite Zabs2Nat.abs_nat_nonneg, Z2Nat.inj_sub by omega. - destruct prec; try discriminate. rewrite NPeano.Nat.sub_add. + destruct prec; try discriminate. rewrite Nat.sub_add. simpl. rewrite Pos2Nat.id. auto. simpl. zify; omega. Qed. @@ -1039,7 +1041,7 @@ Qed. Program Definition Bexact_inverse (f: binary_float) : option binary_float := match f with - | B754_finite s m e B => + | B754_finite _ _ s m e B => if positive_eq_dec m Bexact_inverse_mantissa then let e' := -e - (prec - 1) * 2 in if Z_le_dec emin e' then @@ -1125,7 +1127,7 @@ Lemma pos_pow_spec: forall x y, Z.pos (pos_pow x y) = Z.pos x ^ Z.pos y. Proof. intros x. - assert (REC: forall y a, Pos.iter y (Pos.mul x) a = Pos.mul (pos_pow x y) a). + assert (REC: forall y a, Pos.iter (Pos.mul x) a y = Pos.mul (pos_pow x y) a). { induction y; simpl; intros. - rewrite ! IHy, Pos.square_spec, ! Pos.mul_assoc. auto. - rewrite ! IHy, Pos.square_spec, ! Pos.mul_assoc. auto. @@ -1347,10 +1349,10 @@ Let binary_float2 := binary_float prec2 emax2. Definition Bconv (conv_nan: bool -> nan_pl prec1 -> bool * nan_pl prec2) (md: mode) (f: binary_float1) : binary_float2 := match f with - | B754_nan s pl => let '(s, pl) := conv_nan s pl in B754_nan _ _ s pl - | B754_infinity s => B754_infinity _ _ s - | B754_zero s => B754_zero _ _ s - | B754_finite s m e _ => binary_normalize _ _ _ Hmax2 md (cond_Zopp s (Zpos m)) e s + | B754_nan _ _ s pl => let '(s, pl) := conv_nan s pl in B754_nan _ _ s pl + | B754_infinity _ _ s => B754_infinity _ _ s + | B754_zero _ _ s => B754_zero _ _ s + | B754_finite _ _ s m e _ => binary_normalize _ _ _ Hmax2 md (cond_Zopp s (Zpos m)) e s end. Theorem Bconv_correct: diff --git a/lib/Floats.v b/lib/Floats.v index cf25852e..51b0c415 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -109,7 +109,7 @@ Module Float. (** Transform a Nan payload to a quiet Nan payload. *) Program Definition transform_quiet_pl (pl:nan_pl 53) : nan_pl 53 := - Pos.lor pl (nat_iter 51 xO xH). + Pos.lor pl (iter_nat xO 51 xH). Next Obligation. destruct pl. simpl. rewrite Z.ltb_lt in *. @@ -147,7 +147,7 @@ Definition expand_pl (pl: nan_pl 24) : nan_pl 53. Proof. refine (exist _ (Pos.shiftl_nat (proj1_sig pl) 29) _). abstract ( - destruct pl; unfold proj1_sig, Pos.shiftl_nat, nat_iter, Fcore_digits.digits2_pos; + destruct pl; unfold proj1_sig, Pos.shiftl_nat, nat_rect, Fcore_digits.digits2_pos; fold (Fcore_digits.digits2_pos x); rewrite Z.ltb_lt in *; zify; omega). @@ -163,7 +163,7 @@ Definition reduce_pl (pl: nan_pl 53) : nan_pl 24. Proof. refine (exist _ (Pos.shiftr_nat (proj1_sig pl) 29) _). abstract ( - destruct pl; unfold proj1_sig, Pos.shiftr_nat, nat_iter; + destruct pl; unfold proj1_sig, Pos.shiftr_nat, nat_rect; rewrite Z.ltb_lt in *; assert (forall x, Fcore_digits.digits2_pos (Pos.div2 x) = (Fcore_digits.digits2_pos x - 1)%positive) @@ -473,13 +473,11 @@ Proof. apply Rgt_ge; apply Rcompare_Gt_inv; auto. } assert (EQ: ZofB_range _ _ (sub x y) Int.min_signed Int.max_signed = Some (p - Int.unsigned ox8000_0000)). - { - apply ZofB_range_minus. exact E. + { apply ZofB_range_minus. exact E. compute_this (Int.unsigned ox8000_0000). smart_omega. apply Rge_le; auto. } - unfold to_int; rewrite EQ. simpl. f_equal. unfold Int.sub. f_equal. f_equal. - symmetry; apply Int.unsigned_repr. omega. + unfold to_int; rewrite EQ. simpl. unfold Int.sub. rewrite Int.unsigned_repr by omega. auto. Qed. (** Conversions from ints to floats can be defined as bitwise manipulations @@ -538,7 +536,7 @@ Theorem of_intu_from_words: Proof. intros. pose proof (Int.unsigned_range x). rewrite ! from_words_eq. unfold sub. rewrite BofZ_minus. - unfold of_intu. f_equal. rewrite Int.unsigned_zero. omega. + unfold of_intu. apply (f_equal (BofZ 53 1024 __ __)). rewrite Int.unsigned_zero. omega. apply integer_representable_n; auto; smart_omega. apply integer_representable_n; auto; rewrite Int.unsigned_zero; smart_omega. Qed. @@ -565,7 +563,7 @@ Proof. rewrite ! from_words_eq. rewrite ox8000_0000_signed_unsigned. change (Int.unsigned ox8000_0000) with Int.half_modulus. unfold sub. rewrite BofZ_minus. - unfold of_int. f_equal. omega. + unfold of_int. apply f_equal. omega. apply integer_representable_n; auto; smart_omega. apply integer_representable_n; auto; smart_omega. Qed. @@ -674,7 +672,7 @@ Proof. with ((xh - 2^20) * 2^32) by (compute_this p; compute_this Int.half_modulus; ring). unfold add. rewrite BofZ_plus. - unfold of_long. f_equal. + unfold of_long. apply f_equal. rewrite <- (Int64.ofwords_recompose l) at 1. rewrite Int64.ofwords_add''. fold xh; fold xl. compute_this (two_p 32); ring. apply integer_representable_n2p; auto. @@ -831,7 +829,7 @@ Module Float32. (** ** NaN payload manipulations *) Program Definition transform_quiet_pl (pl:nan_pl 24) : nan_pl 24 := - Pos.lor pl (nat_iter 22 xO xH). + Pos.lor pl (iter_nat xO 22 xH). Next Obligation. destruct pl. simpl. rewrite Z.ltb_lt in *. @@ -1280,4 +1278,3 @@ Global Opaque Float32.to_int Float32.to_intu Float32.to_long Float32.to_longu Float32.add Float32.sub Float32.mul Float32.div Float32.cmp Float32.to_bits Float32.of_bits. - diff --git a/lib/Integers.v b/lib/Integers.v index a0140e57..316dfb52 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -53,7 +53,7 @@ Definition swap_comparison (c: comparison): comparison := (** * Parameterization by the word size, in bits. *) Module Type WORDSIZE. - Variable wordsize: nat. + Parameter wordsize: nat. Axiom wordsize_not_zero: wordsize <> 0%nat. End WORDSIZE. @@ -3378,7 +3378,7 @@ Proof. repeat rewrite unsigned_repr. tauto. generalize wordsize_max_unsigned; omega. generalize wordsize_max_unsigned; omega. - intros. unfold one_bits in H. + unfold one_bits. intros. destruct (list_in_map_inv _ _ _ H) as [i0 [EQ IN]]. subst i. apply A. apply Z_one_bits_range with (unsigned x); auto. Qed. @@ -3576,8 +3576,8 @@ Proof. intros. destruct (andb_prop _ _ H1). clear H1. destruct (andb_prop _ _ H2). clear H2. - exploit proj_sumbool_true. eexact H1. intro A; clear H1. - exploit proj_sumbool_true. eexact H4. intro B; clear H4. + apply proj_sumbool_true in H1. + apply proj_sumbool_true in H4. assert (unsigned ofs1 + sz1 <= unsigned ofs2 \/ unsigned ofs2 + sz2 <= unsigned ofs1). destruct (orb_prop _ _ H3). left. eapply proj_sumbool_true; eauto. right. eapply proj_sumbool_true; eauto. clear H3. @@ -248,7 +248,7 @@ Next Obligation. destruct H2. congruence. auto. Qed. Next Obligation. - exists wildcard'0; split; auto. omega. + exists wildcard'; split; auto. omega. Qed. Next Obligation. exists (hi - 1); split; auto. omega. @@ -310,7 +310,3 @@ Hint Resolve disjoint_range in_shift in_shift_inv in_elements elements_in : intv. - - - - diff --git a/lib/Lattice.v b/lib/Lattice.v index 352b4479..4455e22f 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -33,21 +33,21 @@ Local Unset Case Analysis Schemes. Module Type SEMILATTICE. - Variable t: Type. - Variable eq: t -> t -> Prop. - Hypothesis eq_refl: forall x, eq x x. - Hypothesis eq_sym: forall x y, eq x y -> eq y x. - Hypothesis eq_trans: forall x y z, eq x y -> eq y z -> eq x z. - Variable beq: t -> t -> bool. - Hypothesis beq_correct: forall x y, beq x y = true -> eq x y. - Variable ge: t -> t -> Prop. - Hypothesis ge_refl: forall x y, eq x y -> ge x y. - Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Variable bot: t. - Hypothesis ge_bot: forall x, ge x bot. - Variable lub: t -> t -> t. - Hypothesis ge_lub_left: forall x y, ge (lub x y) x. - Hypothesis ge_lub_right: forall x y, ge (lub x y) y. + Parameter t: Type. + Parameter eq: t -> t -> Prop. + Axiom eq_refl: forall x, eq x x. + Axiom eq_sym: forall x y, eq x y -> eq y x. + Axiom eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Parameter beq: t -> t -> bool. + Axiom beq_correct: forall x y, beq x y = true -> eq x y. + Parameter ge: t -> t -> Prop. + Axiom ge_refl: forall x y, eq x y -> ge x y. + Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Parameter bot: t. + Axiom ge_bot: forall x, ge x bot. + Parameter lub: t -> t -> t. + Axiom ge_lub_left: forall x y, ge (lub x y) x. + Axiom ge_lub_right: forall x y, ge (lub x y) y. End SEMILATTICE. @@ -57,8 +57,8 @@ End SEMILATTICE. Module Type SEMILATTICE_WITH_TOP. Include Type SEMILATTICE. - Variable top: t. - Hypothesis ge_top: forall x, ge top x. + Parameter top: t. + Axiom ge_top: forall x, ge top x. End SEMILATTICE_WITH_TOP. @@ -44,24 +44,24 @@ Set Implicit Arguments. (** * The abstract signatures of trees *) Module Type TREE. - Variable elt: Type. - Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}. - Variable t: Type -> Type. - Variable empty: forall (A: Type), t A. - Variable get: forall (A: Type), elt -> t A -> option A. - Variable set: forall (A: Type), elt -> A -> t A -> t A. - Variable remove: forall (A: Type), elt -> t A -> t A. + Parameter elt: Type. + Parameter elt_eq: forall (a b: elt), {a = b} + {a <> b}. + Parameter t: Type -> Type. + Parameter empty: forall (A: Type), t A. + Parameter get: forall (A: Type), elt -> t A -> option A. + Parameter set: forall (A: Type), elt -> A -> t A -> t A. + Parameter remove: forall (A: Type), elt -> t A -> t A. (** The ``good variables'' properties for trees, expressing commutations between [get], [set] and [remove]. *) - Hypothesis gempty: + Axiom gempty: forall (A: Type) (i: elt), get i (empty A) = None. - Hypothesis gss: + Axiom gss: forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x. - Hypothesis gso: + Axiom gso: forall (A: Type) (i j: elt) (x: A) (m: t A), i <> j -> get i (set j x m) = get i m. - Hypothesis gsspec: + Axiom gsspec: forall (A: Type) (i j: elt) (x: A) (m: t A), get i (set j x m) = if elt_eq i j then Some x else get i m. (* We could implement the following, but it's not needed for the moment. @@ -72,18 +72,18 @@ Module Type TREE. forall (A: Type) (i: elt) (m: t A) (v: A), get i m = None -> remove i m = m. *) - Hypothesis grs: + Axiom grs: forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None. - Hypothesis gro: + Axiom gro: forall (A: Type) (i j: elt) (m: t A), i <> j -> get i (remove j m) = get i m. - Hypothesis grspec: + Axiom grspec: forall (A: Type) (i j: elt) (m: t A), get i (remove j m) = if elt_eq i j then None else get i m. (** Extensional equality between trees. *) - Variable beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool. - Hypothesis beq_correct: + Parameter beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool. + Axiom beq_correct: forall (A: Type) (eqA: A -> A -> bool) (t1 t2: t A), beq eqA t1 t2 = true <-> (forall (x: elt), @@ -94,60 +94,60 @@ Module Type TREE. end). (** Applying a function to all data of a tree. *) - Variable map: + Parameter map: forall (A B: Type), (elt -> A -> B) -> t A -> t B. - Hypothesis gmap: + Axiom gmap: forall (A B: Type) (f: elt -> A -> B) (i: elt) (m: t A), get i (map f m) = option_map (f i) (get i m). (** Same as [map], but the function does not receive the [elt] argument. *) - Variable map1: + Parameter map1: forall (A B: Type), (A -> B) -> t A -> t B. - Hypothesis gmap1: + Axiom gmap1: forall (A B: Type) (f: A -> B) (i: elt) (m: t A), get i (map1 f m) = option_map f (get i m). (** Applying a function pairwise to all data of two trees. *) - Variable combine: + Parameter combine: forall (A B C: Type), (option A -> option B -> option C) -> t A -> t B -> t C. - Hypothesis gcombine: + Axiom gcombine: forall (A B C: Type) (f: option A -> option B -> option C), f None None = None -> forall (m1: t A) (m2: t B) (i: elt), get i (combine f m1 m2) = f (get i m1) (get i m2). (** Enumerating the bindings of a tree. *) - Variable elements: + Parameter elements: forall (A: Type), t A -> list (elt * A). - Hypothesis elements_correct: + Axiom elements_correct: forall (A: Type) (m: t A) (i: elt) (v: A), get i m = Some v -> In (i, v) (elements m). - Hypothesis elements_complete: + Axiom elements_complete: forall (A: Type) (m: t A) (i: elt) (v: A), In (i, v) (elements m) -> get i m = Some v. - Hypothesis elements_keys_norepet: + Axiom elements_keys_norepet: forall (A: Type) (m: t A), list_norepet (List.map (@fst elt A) (elements m)). - Hypothesis elements_extensional: + Axiom elements_extensional: forall (A: Type) (m n: t A), (forall i, get i m = get i n) -> elements m = elements n. - Hypothesis elements_remove: + Axiom elements_remove: forall (A: Type) i v (m: t A), get i m = Some v -> exists l1 l2, elements m = l1 ++ (i,v) :: l2 /\ elements (remove i m) = l1 ++ l2. (** Folding a function over all bindings of a tree. *) - Variable fold: + Parameter fold: forall (A B: Type), (B -> elt -> A -> B) -> t A -> B -> B. - Hypothesis fold_spec: + Axiom fold_spec: forall (A B: Type) (f: B -> elt -> A -> B) (v: B) (m: t A), fold f m v = List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v. (** Same as [fold], but the function does not receive the [elt] argument. *) - Variable fold1: + Parameter fold1: forall (A B: Type), (B -> A -> B) -> t A -> B -> B. - Hypothesis fold1_spec: + Axiom fold1_spec: forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A), fold1 f m v = List.fold_left (fun a p => f a (snd p)) (elements m) v. @@ -156,26 +156,26 @@ End TREE. (** * The abstract signatures of maps *) Module Type MAP. - Variable elt: Type. - Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}. - Variable t: Type -> Type. - Variable init: forall (A: Type), A -> t A. - Variable get: forall (A: Type), elt -> t A -> A. - Variable set: forall (A: Type), elt -> A -> t A -> t A. - Hypothesis gi: + Parameter elt: Type. + Parameter elt_eq: forall (a b: elt), {a = b} + {a <> b}. + Parameter t: Type -> Type. + Parameter init: forall (A: Type), A -> t A. + Parameter get: forall (A: Type), elt -> t A -> A. + Parameter set: forall (A: Type), elt -> A -> t A -> t A. + Axiom gi: forall (A: Type) (i: elt) (x: A), get i (init x) = x. - Hypothesis gss: + Axiom gss: forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = x. - Hypothesis gso: + Axiom gso: forall (A: Type) (i j: elt) (x: A) (m: t A), i <> j -> get i (set j x m) = get i m. - Hypothesis gsspec: + Axiom gsspec: forall (A: Type) (i j: elt) (x: A) (m: t A), get i (set j x m) = if elt_eq i j then x else get i m. - Hypothesis gsident: + Axiom gsident: forall (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m. - Variable map: forall (A B: Type), (A -> B) -> t A -> t B. - Hypothesis gmap: + Parameter map: forall (A B: Type), (A -> B) -> t A -> t B. + Axiom gmap: forall (A B: Type) (f: A -> B) (i: elt) (m: t A), get i (map f m) = f(get i m). End MAP. @@ -1040,10 +1040,10 @@ End PMap. (** * An implementation of maps over any type that injects into type [positive] *) Module Type INDEXED_TYPE. - Variable t: Type. - Variable index: t -> positive. - Hypothesis index_inj: forall (x y: t), index x = index y -> x = y. - Variable eq: forall (x y: t), {x = y} + {x <> y}. + Parameter t: Type. + Parameter index: t -> positive. + Axiom index_inj: forall (x y: t), index x = index y -> x = y. + Parameter eq: forall (x y: t), {x = y} + {x <> y}. End INDEXED_TYPE. Module IMap(X: INDEXED_TYPE). @@ -1148,8 +1148,8 @@ Module NMap := IMap(NIndexed). (** * An implementation of maps over any type with decidable equality *) Module Type EQUALITY_TYPE. - Variable t: Type. - Variable eq: forall (x y: t), {x = y} + {x <> y}. + Parameter t: Type. + Parameter eq: forall (x y: t), {x = y} + {x <> y}. End EQUALITY_TYPE. Module EMap(X: EQUALITY_TYPE) <: MAP. diff --git a/lib/UnionFind.v b/lib/UnionFind.v index 76dd6b31..27278b01 100644 --- a/lib/UnionFind.v +++ b/lib/UnionFind.v @@ -26,96 +26,96 @@ Local Unset Elimination Schemes. Local Unset Case Analysis Schemes. Module Type MAP. - Variable elt: Type. - Variable elt_eq: forall (x y: elt), {x=y} + {x<>y}. - Variable t: Type -> Type. - Variable empty: forall (A: Type), t A. - Variable get: forall (A: Type), elt -> t A -> option A. - Variable set: forall (A: Type), elt -> A -> t A -> t A. - Hypothesis gempty: forall (A: Type) (x: elt), get x (empty A) = None. - Hypothesis gsspec: forall (A: Type) (x y: elt) (v: A) (m: t A), + Parameter elt: Type. + Parameter elt_eq: forall (x y: elt), {x=y} + {x<>y}. + Parameter t: Type -> Type. + Parameter empty: forall (A: Type), t A. + Parameter get: forall (A: Type), elt -> t A -> option A. + Parameter set: forall (A: Type), elt -> A -> t A -> t A. + Axiom gempty: forall (A: Type) (x: elt), get x (empty A) = None. + Axiom gsspec: forall (A: Type) (x y: elt) (v: A) (m: t A), get x (set y v m) = if elt_eq x y then Some v else get x m. End MAP. Unset Implicit Arguments. Module Type UNIONFIND. - Variable elt: Type. - Variable elt_eq: forall (x y: elt), {x=y} + {x<>y}. - Variable t: Type. + Parameter elt: Type. + Parameter elt_eq: forall (x y: elt), {x=y} + {x<>y}. + Parameter t: Type. - Variable repr: t -> elt -> elt. - Hypothesis repr_canonical: forall uf a, repr uf (repr uf a) = repr uf a. + Parameter repr: t -> elt -> elt. + Axiom repr_canonical: forall uf a, repr uf (repr uf a) = repr uf a. Definition sameclass (uf: t) (a b: elt) : Prop := repr uf a = repr uf b. - Hypothesis sameclass_refl: + Axiom sameclass_refl: forall uf a, sameclass uf a a. - Hypothesis sameclass_sym: + Axiom sameclass_sym: forall uf a b, sameclass uf a b -> sameclass uf b a. - Hypothesis sameclass_trans: + Axiom sameclass_trans: forall uf a b c, sameclass uf a b -> sameclass uf b c -> sameclass uf a c. - Hypothesis sameclass_repr: + Axiom sameclass_repr: forall uf a, sameclass uf a (repr uf a). - Variable empty: t. - Hypothesis repr_empty: + Parameter empty: t. + Axiom repr_empty: forall a, repr empty a = a. - Hypothesis sameclass_empty: + Axiom sameclass_empty: forall a b, sameclass empty a b -> a = b. - Variable find: t -> elt -> elt * t. - Hypothesis find_repr: + Parameter find: t -> elt -> elt * t. + Axiom find_repr: forall uf a, fst (find uf a) = repr uf a. - Hypothesis find_unchanged: + Axiom find_unchanged: forall uf a x, repr (snd (find uf a)) x = repr uf x. - Hypothesis sameclass_find_1: + Axiom sameclass_find_1: forall uf a x y, sameclass (snd (find uf a)) x y <-> sameclass uf x y. - Hypothesis sameclass_find_2: + Axiom sameclass_find_2: forall uf a, sameclass uf a (fst (find uf a)). - Hypothesis sameclass_find_3: + Axiom sameclass_find_3: forall uf a, sameclass (snd (find uf a)) a (fst (find uf a)). - Variable union: t -> elt -> elt -> t. - Hypothesis repr_union_1: + Parameter union: t -> elt -> elt -> t. + Axiom repr_union_1: forall uf a b x, repr uf x <> repr uf a -> repr (union uf a b) x = repr uf x. - Hypothesis repr_union_2: + Axiom repr_union_2: forall uf a b x, repr uf x = repr uf a -> repr (union uf a b) x = repr uf b. - Hypothesis repr_union_3: + Axiom repr_union_3: forall uf a b, repr (union uf a b) b = repr uf b. - Hypothesis sameclass_union_1: + Axiom sameclass_union_1: forall uf a b, sameclass (union uf a b) a b. - Hypothesis sameclass_union_2: + Axiom sameclass_union_2: forall uf a b x y, sameclass uf x y -> sameclass (union uf a b) x y. - Hypothesis sameclass_union_3: + Axiom sameclass_union_3: forall uf a b x y, sameclass (union uf a b) x y -> sameclass uf x y \/ sameclass uf x a /\ sameclass uf y b \/ sameclass uf x b /\ sameclass uf y a. - Variable merge: t -> elt -> elt -> t. - Hypothesis repr_merge: + Parameter merge: t -> elt -> elt -> t. + Axiom repr_merge: forall uf a b x, repr (merge uf a b) x = repr (union uf a b) x. - Hypothesis sameclass_merge: + Axiom sameclass_merge: forall uf a b x y, sameclass (merge uf a b) x y <-> sameclass (union uf a b) x y. - Variable path_ord: t -> elt -> elt -> Prop. - Hypothesis path_ord_wellfounded: + Parameter path_ord: t -> elt -> elt -> Prop. + Axiom path_ord_wellfounded: forall uf, well_founded (path_ord uf). - Hypothesis path_ord_canonical: + Axiom path_ord_canonical: forall uf x y, repr uf x = x -> ~path_ord uf y x. - Hypothesis path_ord_merge_1: + Axiom path_ord_merge_1: forall uf a b x y, path_ord uf x y -> path_ord (merge uf a b) x y. - Hypothesis path_ord_merge_2: + Axiom path_ord_merge_2: forall uf a b, repr uf a <> repr uf b -> path_ord (merge uf a b) b (repr uf a). - Variable pathlen: t -> elt -> nat. - Hypothesis pathlen_zero: + Parameter pathlen: t -> elt -> nat. + Axiom pathlen_zero: forall uf a, repr uf a = a <-> pathlen uf a = O. - Hypothesis pathlen_merge: + Axiom pathlen_merge: forall uf a b x, pathlen (merge uf a b) x = if elt_eq (repr uf a) (repr uf b) then @@ -124,7 +124,7 @@ Module Type UNIONFIND. pathlen uf x + pathlen uf b + 1 else pathlen uf x. - Hypothesis pathlen_gt_merge: + Axiom pathlen_gt_merge: forall uf a b x y, repr uf x = repr uf y -> pathlen uf x > pathlen uf y -> @@ -652,21 +652,21 @@ Qed. Next Obligation. (* a <> b*) destruct (find_x a') - as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. + as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous. apply repr_some_diff. auto. Qed. Next Obligation. - destruct (find_x a') as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. + destruct (find_x a') as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous. rewrite B. apply repr_some. auto. Qed. Next Obligation. split. destruct (find_x a') - as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. + as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous. symmetry. apply repr_some. auto. intros. rewrite repr_compress. destruct (find_x a') - as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. auto. + as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous. auto. Qed. Next Obligation. split; auto. symmetry. apply repr_none. auto. diff --git a/lib/Wfsimpl.v b/lib/Wfsimpl.v index 4f80822e..a1e4b4ff 100644 --- a/lib/Wfsimpl.v +++ b/lib/Wfsimpl.v @@ -18,7 +18,7 @@ to be defined have non-dependent types, and function extensionality is assumed. *) Require Import Axioms. -Require Import Wf. +Require Import Init.Wf. Require Import Wf_nat. Set Implicit Arguments. @@ -65,4 +65,3 @@ Qed. End FIXM. - |