Commit da7a14bb authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

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.
parent 39e490e9
......@@ -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
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment