From da7a14bb509e8c561eff60fe71d17772233327fb Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Sat, 15 Nov 2014 14:51:12 +0100 Subject: [PATCH] More accurate formalization of integer ranks. Integers with the same size, are no longer supposed to have the same rank. As a result, the C integer types (char, short, int, long, long long) are different (and thus cannot alias) even if they have the same size. We now have to use a more involved definition of integer promotions and usual arithmetic conversions. However, this new definition follows the C standard literally. --- theories/base.v | 53 +++++++++-------------- theories/collections.v | 9 ++-- theories/fin_maps.v | 17 ++++---- theories/finite.v | 10 ++--- theories/numbers.v | 4 ++ theories/orders.v | 96 ++++++++++++++++++------------------------ 6 files changed, 85 insertions(+), 104 deletions(-) diff --git a/theories/base.v b/theories/base.v index 3a72ad1..e9d3476 100644 --- a/theories/base.v +++ b/theories/base.v @@ -612,46 +612,37 @@ Lemma right_distr_L {A} (f g : A → A → A) `{!RightDistr (=) f g} y z x : Proof. auto. Qed. (** ** Axiomatization of ordered structures *) -(** The classes [PreOrder], [PartialOrder], and [TotalOrder] do not use the -relation [⊆] because we often have multiple orders on the same structure. *) +(** The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary +relation [R] instead of [⊆] to support multiple orders on the same type. *) Class PartialOrder {A} (R : relation A) : Prop := { - po_preorder :> PreOrder R; - po_anti_symmetric :> AntiSymmetric (=) R + partial_order_pre :> PreOrder R; + partial_order_anti_symmetric :> AntiSymmetric (=) R }. Class TotalOrder {A} (R : relation A) : Prop := { - to_po :> PartialOrder R; - to_trichotomy :> Trichotomy R + total_order_partial :> PartialOrder R; + total_order_trichotomy :> Trichotomy (strict R) }. -(** We do not include equality in the following interfaces so as to avoid the -need for proofs that the relations and operations respect setoid equality. -Instead, we will define setoid equality in a generic way as -[λ X Y, X ⊆ Y ∧ Y ⊆ X]. *) -Class BoundedPreOrder A `{Empty A, SubsetEq A} : Prop := { - bounded_preorder :>> PreOrder (⊆); - subseteq_empty X : ∅ ⊆ X -}. -Class BoundedJoinSemiLattice A `{Empty A, SubsetEq A, Union A} : Prop := { - bjsl_preorder :>> BoundedPreOrder A; +(** We do not use a setoid equality in the following interfaces to avoid the +need for proofs that the relations and operations are proper. Instead, we +define setoid equality generically [λ X Y, X ⊆ Y ∧ Y ⊆ X]. *) +Class EmptySpec A `{Empty A, SubsetEq A} : Prop := subseteq_empty X : ∅ ⊆ X. +Class JoinSemiLattice A `{SubsetEq A, Union A} : Prop := { + join_semi_lattice_pre :>> PreOrder (⊆); union_subseteq_l X Y : X ⊆ X ∪ Y; union_subseteq_r X Y : Y ⊆ X ∪ Y; union_least X Y Z : X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z }. -Class MeetSemiLattice A `{Empty A, SubsetEq A, Intersection A} : Prop := { - msl_preorder :>> BoundedPreOrder A; +Class MeetSemiLattice A `{SubsetEq A, Intersection A} : Prop := { + meet_semi_lattice_pre :>> PreOrder (⊆); intersection_subseteq_l X Y : X ∩ Y ⊆ X; intersection_subseteq_r X Y : X ∩ Y ⊆ Y; intersection_greatest X Y Z : Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y }. - -(** A join distributive lattice with distributivity stated in the order -theoretic way. We will prove that distributivity of join, and distributivity -as an equality can be derived. *) -Class LowerBoundedLattice A - `{Empty A, SubsetEq A, Union A, Intersection A} : Prop := { - lbl_bjsl :>> BoundedJoinSemiLattice A; - lbl_msl :>> MeetSemiLattice A; - lbl_distr X Y Z : (X ∪ Y) ∩ (X ∪ Z) ⊆ X ∪ (Y ∩ Z) +Class Lattice A `{SubsetEq A, Union A, Intersection A} : Prop := { + lattice_join :>> JoinSemiLattice A; + lattice_meet :>> MeetSemiLattice A; + lattice_distr X Y Z : (X ∪ Y) ∩ (X ∪ Z) ⊆ X ∪ (Y ∩ Z) }. (** ** Axiomatization of collections *) @@ -670,14 +661,12 @@ Class Collection A C `{ElemOf A C, Empty C, Singleton A C, elem_of_intersection X Y (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y; elem_of_difference X Y (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y }. -Class CollectionOps A C `{ElemOf A C, Empty C, Singleton A C, - Union C, Intersection C, Difference C, - IntersectionWith A C, Filter A C} : Prop := { +Class CollectionOps A C `{ElemOf A C, Empty C, Singleton A C, Union C, + Intersection C, Difference C, IntersectionWith A C, Filter A C} : Prop := { collection_ops :>> Collection A C; elem_of_intersection_with (f : A → A → option A) X Y (x : A) : x ∈ intersection_with f X Y ↔ ∃ x1 x2, x1 ∈ X ∧ x2 ∈ Y ∧ f x1 x2 = Some x; - elem_of_filter X P `{∀ x, Decision (P x)} x : - x ∈ filter P X ↔ P x ∧ x ∈ X + elem_of_filter X P `{∀ x, Decision (P x)} x : x ∈ filter P X ↔ P x ∧ x ∈ X }. (** We axiomative a finite collection as a collection whose elements can be diff --git a/theories/collections.v b/theories/collections.v index 1129405..c71f3a9 100644 --- a/theories/collections.v +++ b/theories/collections.v @@ -18,7 +18,9 @@ Section simple_collection. Proof. intros. apply elem_of_union. auto. Qed. Lemma elem_of_union_r x X Y : x ∈ Y → x ∈ X ∪ Y. Proof. intros. apply elem_of_union. auto. Qed. - Global Instance: BoundedJoinSemiLattice C. + Global Instance: EmptySpec C. + Proof. firstorder auto. Qed. + Global Instance: JoinSemiLattice C. Proof. firstorder auto. Qed. Lemma elem_of_subseteq X Y : X ⊆ Y ↔ ∀ x, x ∈ X → x ∈ Y. Proof. done. Qed. @@ -229,9 +231,8 @@ Tactic Notation "esolve_elem_of" := esolve_elem_of eauto. Section collection. Context `{Collection A C}. - Global Instance: LowerBoundedLattice C. + Global Instance: Lattice C. Proof. split. apply _. firstorder auto. solve_elem_of. Qed. - Lemma intersection_singletons x : {[x]} ∩ {[x]} ≡ {[x]}. Proof. esolve_elem_of. Qed. Lemma difference_twice X Y : (X ∖ Y) ∖ Y ≡ X ∖ Y. @@ -484,14 +485,12 @@ Section collection_monad. Lemma collection_mapM_length {A B} (f : A → M B) l k : l ∈ mapM f k → length l = length k. Proof. revert l; induction k; esolve_elem_of. Qed. - Lemma elem_of_mapM_fmap {A B} (f : A → B) (g : B → M A) l k : Forall (λ x, ∀ y, y ∈ g x → f y = x) l → k ∈ mapM g l → fmap f k = l. Proof. intros Hl. revert k. induction Hl; simpl; intros; decompose_elem_of; f_equal'; auto. Qed. - Lemma elem_of_mapM_Forall {A B} (f : A → M B) (P : B → Prop) l k : l ∈ mapM f k → Forall (λ x, ∀ y, y ∈ f x → P y) k → Forall P l. Proof. rewrite elem_of_mapM. apply Forall2_Forall_l. Qed. diff --git a/theories/fin_maps.v b/theories/fin_maps.v index f4b7567..a599f2b 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -122,17 +122,18 @@ Proof. unfold subseteq, map_subseteq, map_Forall2. split; intros Hm i; specialize (Hm i); destruct (m1 !! i), (m2 !! i); naive_solver. Qed. -Global Instance: BoundedPreOrder (M A). +Global Instance: EmptySpec (M A). Proof. - repeat split. - * intros m. by rewrite map_subseteq_spec. - * intros m1 m2 m3. rewrite !map_subseteq_spec. naive_solver. - * intros m. rewrite !map_subseteq_spec. intros i x. by rewrite lookup_empty. + intros A m. rewrite !map_subseteq_spec. + intros i x. by rewrite lookup_empty. Qed. -Global Instance : PartialOrder (@subseteq (M A) _). +Global Instance: PartialOrder ((⊆) : relation (M A)). Proof. - split; [apply _ |]. intros ??. rewrite !map_subseteq_spec. - intros ??. apply map_eq; intros i. apply option_eq. naive_solver. + repeat split. + * intros m; rewrite !map_subseteq_spec; naive_solver. + * intros m1 m2 m3; rewrite !map_subseteq_spec; naive_solver. + * intros m1 m2; rewrite !map_subseteq_spec. + intros; apply map_eq; intros i; apply option_eq; naive_solver. Qed. Lemma lookup_weaken {A} (m1 m2 : M A) i x : m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some x. diff --git a/theories/finite.v b/theories/finite.v index 2315bdc..6c78c6a 100644 --- a/theories/finite.v +++ b/theories/finite.v @@ -177,8 +177,8 @@ Section enc_finite. End enc_finite. Section bijective_finite. - Context `{Finite A} `{∀ x y : B, Decision (x = y)} (f : A → B) (g : B → A). - Context `{!Injective (=) (=) f} `{!Cancel (=) f g}. + Context `{Finite A, ∀ x y : B, Decision (x = y)} (f : A → B) (g : B → A). + Context `{!Injective (=) (=) f, !Cancel (=) f g}. Program Instance bijective_finite: Finite B := {| enum := f <\$> enum A |}. Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed. @@ -215,7 +215,7 @@ Next Obligation. intros [|]. left. right; left. Qed. Lemma bool_card : card bool = 2. Proof. done. Qed. -Program Instance sum_finite `{Finite A} `{Finite B} : Finite (A + B)%type := +Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type := {| enum := (inl <\$> enum A) ++ (inr <\$> enum B) |}. Next Obligation. intros. apply NoDup_app; split_ands. @@ -227,10 +227,10 @@ Next Obligation. intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap; eauto using @elem_of_enum. Qed. -Lemma sum_card `{Finite A} `{Finite B} : card (A + B) = card A + card B. +Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B. Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed. -Program Instance prod_finite `{Finite A} `{Finite B} : Finite (A * B)%type := +Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type := {| enum := foldr (λ x, (pair x <\$> enum B ++)) [] (enum A) |}. Next Obligation. intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl. diff --git a/theories/numbers.v b/theories/numbers.v index 0681b7f..dab1c2c 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -77,6 +77,10 @@ Proof. intros. destruct (Nat_mul_split_l n x2 x1 y2 y1); auto with lia. Qed. Notation lcm := Nat.lcm. Notation divide := Nat.divide. Notation "( x | y )" := (divide x y) : nat_scope. +Instance divide_dec x y : Decision (x | y). +Proof. + refine (cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff. +Defined. Instance: PartialOrder divide. Proof. repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia. diff --git a/theories/orders.v b/theories/orders.v index 0a98b2e..5b6da04 100644 --- a/theories/orders.v +++ b/theories/orders.v @@ -29,15 +29,13 @@ Section orders. Proof. by intros [??] <-. Qed. Lemma strict_transitive_l `{!Transitive R} X Y Z : X ⊂ Y → Y ⊆ Z → X ⊂ Z. Proof. - intros [? HXY] ?. split. - * by transitivity Y. - * contradict HXY. by transitivity Z. + intros [? HXY] ?. split; [by transitivity Y|]. + contradict HXY. by transitivity Z. Qed. Lemma strict_transitive_r `{!Transitive R} X Y Z : X ⊆ Y → Y ⊂ Z → X ⊂ Z. Proof. - intros ? [? HYZ]. split. - * by transitivity Y. - * contradict HYZ. by transitivity X. + intros ? [? HYZ]. split; [by transitivity Y|]. + contradict HYZ. by transitivity X. Qed. Global Instance: Irreflexive (strict R). Proof. firstorder. Qed. @@ -54,7 +52,7 @@ Section orders. * intros [? HYX]. split. done. by intros <-. * intros [? HXY]. split. done. by contradict HXY; apply (anti_symmetric R). Qed. - Lemma po_eq_dec `{!PartialOrder R} `{∀ X Y, Decision (X ⊆ Y)} (X Y : A) : + Lemma po_eq_dec `{!PartialOrder R, ∀ X Y, Decision (X ⊆ Y)} (X Y : A) : Decision (X = Y). Proof. refine (cast_if_and (decide (X ⊆ Y)) (decide (Y ⊆ X))); @@ -65,7 +63,7 @@ Section orders. Lemma total_not_strict `{!Total R} X Y : X ⊈ Y → Y ⊂ X. Proof. red; auto using total_not. Qed. Global Instance trichotomy_total - `{!Trichotomy (strict R)} `{!Reflexive R} : Total R. + `{!Trichotomy (strict R), !Reflexive R} : Total R. Proof. intros X Y. destruct (trichotomy (strict R) X Y) as [[??]|[<-|[??]]]; intuition. @@ -82,15 +80,13 @@ Section strict_orders. Lemma strict_anti_symmetric `{!StrictOrder R} X Y : X ⊂ Y → Y ⊂ X → False. Proof. intros. apply (irreflexivity R X). by transitivity Y. Qed. - - Global Instance trichotomyT_dec `{!TrichotomyT R} - `{!StrictOrder R} X Y : Decision (X ⊂ Y) := + Global Instance trichotomyT_dec `{!TrichotomyT R, !StrictOrder R} X Y : + Decision (X ⊂ Y) := match trichotomyT R X Y with | inleft (left H) => left H | inleft (right H) => right (irreflexive_eq _ _ H) | inright H => right (strict_anti_symmetric _ _ H) end. - Global Instance trichotomyT_trichotomy `{!TrichotomyT R} : Trichotomy R. Proof. intros X Y. destruct (trichotomyT R X Y) as [[|]|]; tauto. Qed. End strict_orders. @@ -168,7 +164,7 @@ Section sorted. inversion Hx1'; inversion Hx2'; simplify_equality; auto. } f_equal. by apply IH, (injective (x2 ::)). Qed. - Lemma Sorted_unique `{!Transitive R} `{!AntiSymmetric (=) R} l1 l2 : + Lemma Sorted_unique `{!Transitive R, !AntiSymmetric (=) R} l1 l2 : Sorted R l1 → Sorted R l2 → l1 ≡ₚ l2 → l1 = l2. Proof. auto using StronglySorted_unique, Sorted_StronglySorted. Qed. @@ -181,7 +177,6 @@ Section sorted. | y :: l => cast_if (decide (R x y)) end; abstract first [by constructor | by inversion 1]. Defined. - Global Instance Sorted_dec `{∀ x y, Decision (R x y)} : ∀ l, Decision (Sorted R l). Proof. @@ -228,7 +223,6 @@ Section merge_sort_correct. if decide (R x1 x2) then x1 :: list_merge R l1 (x2 :: l2) else x2 :: list_merge R (x1 :: l1) l2. Proof. done. Qed. - Lemma HdRel_list_merge x l1 l2 : HdRel R x l1 → HdRel R x l2 → HdRel R x (list_merge R l1 l2). Proof. @@ -318,7 +312,7 @@ setoid. *) Instance preorder_equiv `{SubsetEq A} : Equiv A := λ X Y, X ⊆ Y ∧ Y ⊆ X. Section preorder. - Context `{SubsetEq A} `{!PreOrder (@subseteq A _)}. + Context `{SubsetEq A, !PreOrder (@subseteq A _)}. Instance preorder_equivalence: @Equivalence A (≡). Proof. @@ -349,35 +343,34 @@ Section preorder. Lemma not_subset_inv X Y : X ⊄ Y → X ⊈ Y ∨ X ≡ Y. Proof. rewrite subset_spec. destruct (decide (X ≡ Y)); tauto. Qed. End dec. -End preorder. - -Section preorder_leibniz. - Context `{SubsetEq A} `{!PreOrder (@subseteq A _)} `{!LeibnizEquiv A}. - Lemma subset_spec_L X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y. - Proof. unfold_leibniz. apply subset_spec. Qed. - Context `{∀ X Y : A, Decision (X ⊆ Y)}. - Lemma subseteq_inv_L X Y : X ⊆ Y → X ⊂ Y ∨ X = Y. - Proof. unfold_leibniz. apply subseteq_inv. Qed. - Lemma not_subset_inv_L X Y : X ⊄ Y → X ⊈ Y ∨ X = Y. - Proof. unfold_leibniz. apply not_subset_inv. Qed. -End preorder_leibniz. + Section leibniz. + Context `{!LeibnizEquiv A}. + Lemma subset_spec_L X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y. + Proof. unfold_leibniz. apply subset_spec. Qed. + Context `{∀ X Y : A, Decision (X ⊆ Y)}. + Lemma subseteq_inv_L X Y : X ⊆ Y → X ⊂ Y ∨ X = Y. + Proof. unfold_leibniz. apply subseteq_inv. Qed. + Lemma not_subset_inv_L X Y : X ⊄ Y → X ⊈ Y ∨ X = Y. + Proof. unfold_leibniz. apply not_subset_inv. Qed. + End leibniz. +End preorder. Typeclasses Opaque preorder_equiv. Hint Extern 0 (@Equivalence _ (≡)) => class_apply preorder_equivalence : typeclass_instances. (** * Partial orders *) -Section partialorder. - Context `{SubsetEq A} `{!PartialOrder (@subseteq A _)}. +Section partial_order. + Context `{SubsetEq A, !PartialOrder (@subseteq A _)}. Global Instance: LeibnizEquiv A. Proof. split. intros [??]. by apply (anti_symmetric (⊆)). by intros ->. Qed. -End partialorder. +End partial_order. (** * Join semi lattices *) (** General purpose theorems on join semi lattices. *) -Section bounded_join_sl. - Context `{BoundedJoinSemiLattice A}. +Section join_semi_lattice. + Context `{Empty A, JoinSemiLattice A, !EmptySpec A}. Implicit Types X Y : A. Implicit Types Xs Ys : list A. @@ -418,8 +411,7 @@ Section bounded_join_sl. Proof. apply subseteq_union. Qed. Lemma equiv_empty X : X ⊆ ∅ → X ≡ ∅. Proof. split; eauto. Qed. - Global Instance union_list_proper: - Proper (Forall2 (≡) ==> (≡)) union_list. + Global Instance union_list_proper: Proper (Forall2 (≡) ==> (≡)) union_list. Proof. induction 1; simpl. done. by apply union_proper. Qed. Lemma union_list_nil : ⋃ @nil A = ∅. Proof. done. Qed. @@ -498,11 +490,11 @@ Section bounded_join_sl. Lemma non_empty_union_list_L Xs : ⋃ Xs ≠ ∅ → Exists (≠ ∅) Xs. Proof. unfold_leibniz. apply non_empty_union_list. Qed. End dec. -End bounded_join_sl. +End join_semi_lattice. (** * Meet semi lattices *) (** The dual of the above section, but now for meet semi lattices. *) -Section meet_sl. +Section meet_semi_lattice. Context `{MeetSemiLattice A}. Implicit Types X Y : A. Implicit Types Xs Ys : list A. @@ -555,27 +547,24 @@ Section meet_sl. Lemma subseteq_intersection_2_L X Y : X ∩ Y = X → X ⊆ Y. Proof. unfold_leibniz. apply subseteq_intersection_2. Qed. End leibniz. -End meet_sl. +End meet_semi_lattice. (** * Lower bounded lattices *) -Section lower_bounded_lattice. - Context `{LowerBoundedLattice A}. +Section lattice. + Context `{Empty A, Lattice A, !EmptySpec A}. Global Instance: LeftAbsorb (≡) ∅ (∩). - Proof. - split. by apply intersection_subseteq_l. by apply subseteq_empty. - Qed. + Proof. split. by apply intersection_subseteq_l. by apply subseteq_empty. Qed. Global Instance: RightAbsorb (≡) ∅ (∩). Proof. intros ?. by rewrite (commutative _), (left_absorb _ _). Qed. Global Instance: LeftDistr (≡) (∪) (∩). Proof. - intros X Y Z. split. - * apply union_least. - { apply intersection_greatest; auto using union_subseteq_l. } - apply intersection_greatest. - + apply union_subseteq_r_transitive, intersection_subseteq_l. - + apply union_subseteq_r_transitive, intersection_subseteq_r. - * apply lbl_distr. + intros X Y Z. split; [|apply lattice_distr]. + apply union_least. + { apply intersection_greatest; auto using union_subseteq_l. } + apply intersection_greatest. + * apply union_subseteq_r_transitive, intersection_subseteq_l. + * apply union_subseteq_r_transitive, intersection_subseteq_r. Qed. Global Instance: RightDistr (≡) (∪) (∩). Proof. intros X Y Z. by rewrite !(commutative _ _ Z), (left_distr _ _). Qed. @@ -585,9 +574,8 @@ Section lower_bounded_lattice. * rewrite (left_distr (∪) (∩)). apply intersection_greatest. { apply union_subseteq_r_transitive, intersection_subseteq_l. } - rewrite (right_distr (∪) (∩)). apply intersection_preserving. - + apply union_subseteq_l. - + done. + rewrite (right_distr (∪) (∩)). + apply intersection_preserving; auto using union_subseteq_l. * apply intersection_greatest. { apply union_least; auto using intersection_subseteq_l. } apply union_least. @@ -612,4 +600,4 @@ Section lower_bounded_lattice. Global Instance: RightDistr (=) (∩) (∪). Proof. intros ???. unfold_leibniz. apply (right_distr _ _). Qed. End leibniz. -End lower_bounded_lattice. +End lattice. -- GitLab