Commit 02b74a1f authored by Robbert Krebbers's avatar Robbert Krebbers

Define lexicographical orders directly as a strict order.

parent 6aac4455
......@@ -12,18 +12,18 @@ Require Export fin_maps.
(** Because the association list is sorted using [strict lexico] instead of
[lexico], it automatically guarantees that no duplicates exist. *)
Definition assoc (K : Type) `{Lexico K} `{!TrichotomyT lexico}
`{!PartialOrder lexico} (A : Type) : Type :=
dsig (λ l : list (K * A), StronglySorted (strict lexico) (fst <$> l)).
`{!StrictOrder lexico} (A : Type) : Type :=
dsig (λ l : list (K * A), StronglySorted lexico (fst <$> l)).
Section assoc.
Context `{Lexico K} `{!PartialOrder lexico}.
Context `{Lexico K} `{!StrictOrder lexico}.
Context `{ x y : K, Decision (x = y)} `{!TrichotomyT lexico}.
Infix "⊂" := (strict lexico).
Infix "⊂" := lexico.
Notation assoc_before j l :=
(Forall (strict lexico j) (fst <$> l)) (only parsing).
(Forall (lexico j) (fst <$> l)) (only parsing).
Notation assoc_wf l :=
(StronglySorted (strict lexico) (fst <$> l)) (only parsing).
(StronglySorted (lexico) (fst <$> l)) (only parsing).
Lemma assoc_before_transitive {A} (l : list (K * A)) i j :
i j assoc_before j l assoc_before i l.
......@@ -245,7 +245,7 @@ Lemma assoc_to_list_nodup {A} (l : list (K * A)) : assoc_wf l → NoDup l.
Proof.
revert l. assert ( i x (l : list (K * A)), assoc_before i l (i,x) l).
{ intros i x l. rewrite Forall_fmap, Forall_forall. intros Hl Hi.
destruct (irreflexivity (strict lexico) i). by apply (Hl (i,x) Hi). }
destruct (irreflexivity (lexico) i). by apply (Hl (i,x) Hi). }
induction l as [|[??]]; simplify_assoc; constructor; auto.
Qed.
Lemma assoc_to_list_elem_of {A} (l : list (K * A)) i x :
......@@ -276,7 +276,7 @@ End assoc.
(** We construct finite sets using the above implementation of maps. *)
Notation assoc_set K := (mapset (assoc K)).
Instance assoc_map_dom `{Lexico K} `{!TrichotomyT (@lexico K _)}
`{!PartialOrder lexico} {A} : Dom (assoc K A) (assoc_set K) := mapset_dom.
`{!StrictOrder lexico} {A} : Dom (assoc K A) (assoc_set K) := mapset_dom.
Instance assoc_map_dom_spec `{Lexico K} `{!TrichotomyT (@lexico K _)}
`{!PartialOrder lexico} `{ x y : K, Decision (x = y)} :
`{!StrictOrder lexico} `{ x y : K, Decision (x = y)} :
FinMapDom K (assoc K) (assoc_set K) := mapset_dom_spec.
......@@ -480,9 +480,9 @@ Class AntiSymmetric {A} (R S : relation A) : Prop :=
anti_symmetric: x y, S x y S y x R x y.
Class Total {A} (R : relation A) := total x y : R x y R y x.
Class Trichotomy {A} (R : relation A) :=
trichotomy : x y, strict R x y x = y strict R y x.
trichotomy : x y, R x y x = y R y x.
Class TrichotomyT {A} (R : relation A) :=
trichotomyT : x y, {strict R x y} + {x = y} + {strict R y x}.
trichotomyT : x y, {R x y} + {x = y} + {R y x}.
Arguments irreflexivity {_} _ {_} _ _.
Arguments injective {_ _ _ _} _ {_} _ _ _.
......
......@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This files defines a lexicographic order on various common data structures
and proves that it is a partial order having a strong variant of trichotomy. *)
Require Import orders.
Require Import numbers.
Notation cast_trichotomy T :=
match T with
......@@ -12,59 +12,48 @@ Notation cast_trichotomy T :=
end.
Instance prod_lexico `{Lexico A} `{Lexico B} : Lexico (A * B) := λ p1 p2,
(**i 1.) *) strict lexico (fst p1) (fst p2)
(**i 1.) *) lexico (fst p1) (fst p2)
(**i 2.) *) fst p1 = fst p2 lexico (snd p1) (snd p2).
Lemma prod_lexico_strict `{Lexico A} `{Lexico B} (p1 p2 : A * B) :
strict lexico p1 p2
strict lexico (fst p1) (fst p2)
fst p1 = fst p2 strict lexico (snd p1) (snd p2).
Proof.
destruct p1, p2. repeat (unfold lexico, prod_lexico, strict). naive_solver.
Qed.
Instance bool_lexico : Lexico bool := ().
Instance nat_lexico : Lexico nat := ().
Instance N_lexico : Lexico N := ()%N.
Instance Z_lexico : Lexico Z := ()%Z.
Instance bool_lexico : Lexico bool := λ b1 b2,
match b1, b2 with false, true => True | _, _ => False end.
Instance nat_lexico : Lexico nat := (<).
Instance N_lexico : Lexico N := (<)%N.
Instance Z_lexico : Lexico Z := (<)%Z.
Typeclasses Opaque bool_lexico nat_lexico N_lexico Z_lexico.
Instance list_lexico `{Lexico A} : Lexico (list A) :=
fix go l1 l2 :=
let _ : Lexico (list A) := @go in
match l1, l2 with
| [], _ => True
| _ :: _, [] => False
| [], _ :: _ => True
| x1 :: l1, x2 :: l2 => lexico (x1,l1) (x2,l2)
| _, _ => False
end.
Instance sig_lexico `{Lexico A} (P : A Prop) `{ x, ProofIrrel (P x)} :
Lexico (sig P) := λ x1 x2, lexico (`x1) (`x2).
Lemma prod_lexico_reflexive `{Lexico A} `{!PartialOrder (@lexico A _)}
`{Lexico B} (x : A) (y : B) : lexico y y lexico (x,y) (x,y).
Proof. by right. Qed.
Lemma prod_lexico_transitive `{Lexico A} `{!PartialOrder (@lexico A _)}
`{Lexico B} (x1 x2 x3 : A) (y1 y2 y3 : B) :
Lemma prod_lexico_irreflexive `{Lexico A} `{Lexico B}
`{!Irreflexive (@lexico A _)} (x : A) (y : B) :
complement lexico y y complement lexico (x,y) (x,y).
Proof. intros ? [?|[??]]. by apply (irreflexivity lexico x). done. Qed.
Lemma prod_lexico_transitive `{Lexico A} `{Lexico B}
`{!Transitive (@lexico A _)} (x1 x2 x3 : A) (y1 y2 y3 : B) :
lexico (x1,y1) (x2,y2) lexico (x2,y2) (x3,y3)
(lexico y1 y2 lexico y2 y3 lexico y1 y3) lexico (x1,y1) (x3,y3).
Proof.
intros Hx12 Hx23 ?; revert Hx12 Hx23. unfold lexico, prod_lexico.
intros [|[??]] [?|[??]]; simplify_equality'; auto. left. by transitivity x2.
intros [|[??]] [?|[??]]; simplify_equality'; auto.
by left; transitivity x2.
Qed.
Lemma prod_lexico_anti_symmetric `{Lexico A} `{!PartialOrder (@lexico A _)}
`{Lexico B} (x1 x2 : A) (y1 y2 : B) :
lexico (x1,y1) (x2,y2) lexico (x2,y2) (x1,y1)
(lexico y1 y2 lexico y2 y1 y1 = y2) x1 = x2 y1 = y2.
Proof. by intros [[??]|[??]] [[??]|[??]] ?; simplify_equality'; auto. Qed.
Instance prod_lexico_po `{Lexico A} `{Lexico B} `{!PartialOrder (@lexico A _)}
`{!PartialOrder (@lexico B _)} : PartialOrder (@lexico (A * B) _).
Instance prod_lexico_po `{Lexico A} `{Lexico B} `{!StrictOrder (@lexico A _)}
`{!StrictOrder (@lexico B _)} : StrictOrder (@lexico (A * B) _).
Proof.
repeat split.
* by intros [??]; apply prod_lexico_reflexive.
split.
* intros [x y]. apply prod_lexico_irreflexive.
by apply (irreflexivity lexico y).
* intros [??] [??] [??] ??.
eapply prod_lexico_transitive; eauto. apply @transitivity, _.
* intros [x1 y1] [x2 y2] ??.
destruct (prod_lexico_anti_symmetric x1 x2 y1 y2); try intuition congruence.
apply (anti_symmetric _).
eapply prod_lexico_transitive; eauto. apply transitivity.
Qed.
Instance prod_lexico_trichotomyT `{Lexico A} `{tA: !TrichotomyT (@lexico A _)}
`{Lexico B} `{tB:!TrichotomyT (@lexico B _)}: TrichotomyT (@lexico (A * B) _).
......@@ -75,17 +64,12 @@ Proof.
| inleft (right _) =>
cast_trichotomy (trichotomyT lexico (snd p1) (snd p2))
| inright _ => inright _
end); clear tA tB; abstract (rewrite ?prod_lexico_strict;
intuition (auto using injective_projections with congruence)).
end); clear tA tB;
abstract (unfold lexico, prod_lexico; auto using injective_projections).
Defined.
Instance bool_lexico_po : PartialOrder (@lexico bool _).
Proof.
unfold lexico, bool_lexico. repeat split.
* intros []; simpl; tauto.
* intros [] [] []; simpl; tauto.
* intros [] []; simpl; tauto.
Qed.
Instance bool_lexico_po : StrictOrder (@lexico bool _).
Proof. split. by intros [] ?. by intros [] [] [] ??. Qed.
Instance bool_lexico_trichotomy: TrichotomyT (@lexico bool _).
Proof.
red; refine (λ b1 b2,
......@@ -97,65 +81,51 @@ Proof.
end); abstract (unfold strict, lexico, bool_lexico; naive_solver).
Defined.
Lemma nat_lexico_strict (x1 x2 : nat) : strict lexico x1 x2 x1 < x2.
Proof. unfold strict, lexico, nat_lexico. lia. Qed.
Instance nat_lexico_po : PartialOrder (@lexico nat _).
Instance nat_lexico_po : StrictOrder (@lexico nat _).
Proof. unfold lexico, nat_lexico. apply _. Qed.
Instance nat_lexico_trichotomy: TrichotomyT (@lexico nat _).
Proof.
red; refine (λ n1 n2,
match Nat.compare n1 n2 as c return Nat.compare n1 n2 = c _ with
| Lt => λ H,
inleft (left (proj2 (nat_lexico_strict _ _) (nat_compare_Lt_lt _ _ H)))
| Lt => λ H, inleft (left (nat_compare_Lt_lt _ _ H))
| Eq => λ H, inleft (right (nat_compare_eq _ _ H))
| Gt => λ H,
inright (proj2 (nat_lexico_strict _ _) (nat_compare_Gt_gt _ _ H))
| Gt => λ H, inright (nat_compare_Gt_gt _ _ H)
end eq_refl).
Defined.
Lemma N_lexico_strict (x1 x2 : N) : strict lexico x1 x2 (x1 < x2)%N.
Proof. unfold strict, lexico, N_lexico. lia. Qed.
Instance N_lexico_po : PartialOrder (@lexico N _).
Instance N_lexico_po : StrictOrder (@lexico N _).
Proof. unfold lexico, N_lexico. apply _. Qed.
Instance N_lexico_trichotomy: TrichotomyT (@lexico N _).
Proof.
red; refine (λ n1 n2,
match N.compare n1 n2 as c return N.compare n1 n2 = c _ with
| Lt => λ H,
inleft (left (proj2 (N_lexico_strict _ _) (proj2 (N.compare_lt_iff _ _) H)))
| Lt => λ H, inleft (left (proj2 (N.compare_lt_iff _ _) H))
| Eq => λ H, inleft (right (N.compare_eq _ _ H))
| Gt => λ H,
inright (proj2 (N_lexico_strict _ _) (proj1 (N.compare_gt_iff _ _) H))
| Gt => λ H, inright (proj1 (N.compare_gt_iff _ _) H)
end eq_refl).
Defined.
Lemma Z_lexico_strict (x1 x2 : Z) : strict lexico x1 x2 (x1 < x2)%Z.
Proof. unfold strict, lexico, Z_lexico. lia. Qed.
Instance Z_lexico_po : PartialOrder (@lexico Z _).
Instance Z_lexico_po : StrictOrder (@lexico Z _).
Proof. unfold lexico, Z_lexico. apply _. Qed.
Instance Z_lexico_trichotomy: TrichotomyT (@lexico Z _).
Proof.
red; refine (λ n1 n2,
match Z.compare n1 n2 as c return Z.compare n1 n2 = c _ with
| Lt => λ H,
inleft (left (proj2 (Z_lexico_strict _ _) (proj2 (Z.compare_lt_iff _ _) H)))
| Lt => λ H, inleft (left (proj2 (Z.compare_lt_iff _ _) H))
| Eq => λ H, inleft (right (Z.compare_eq _ _ H))
| Gt => λ H,
inright (proj2 (Z_lexico_strict _ _) (proj1 (Z.compare_gt_iff _ _) H))
| Gt => λ H, inright (proj1 (Z.compare_gt_iff _ _) H)
end eq_refl).
Defined.
Instance list_lexico_po `{Lexico A} `{!PartialOrder (@lexico A _)} :
PartialOrder (@lexico (list A) _).
Instance list_lexico_po `{Lexico A} `{!StrictOrder (@lexico A _)} :
StrictOrder (@lexico (list A) _).
Proof.
repeat split.
* intros l. induction l. done. by apply prod_lexico_reflexive.
split.
* intros l. induction l. by intros ?. by apply prod_lexico_irreflexive.
* intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] [|x3 l3] ??; try done.
eapply prod_lexico_transitive; eauto.
* intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] ??; try done.
destruct (prod_lexico_anti_symmetric x1 x2 l1 l2); naive_solver.
Qed.
Instance list_lexico_trichotomy `{Lexico A} `{!TrichotomyT (@lexico A _)} :
Instance list_lexico_trichotomy `{Lexico A} `{tA:!TrichotomyT (@lexico A _)} :
TrichotomyT (@lexico (list A) _).
Proof.
refine (
......@@ -166,17 +136,16 @@ Proof.
| [], _ :: _ => inleft (left _)
| _ :: _, [] => inright _
| x1 :: l1, x2 :: l2 => cast_trichotomy (trichotomyT lexico (x1,l1) (x2,l2))
end); clear go go';
abstract (repeat (done || constructor || congruence || by inversion 1)).
end); clear tA go go';
abstract (repeat (done || constructor || congruence || by inversion 1)).
Defined.
Instance sig_lexico_po `{Lexico A} `{!PartialOrder (@lexico A _)}
(P : A Prop) `{ x, ProofIrrel (P x)} : PartialOrder (@lexico (sig P) _).
Instance sig_lexico_po `{Lexico A} `{!StrictOrder (@lexico A _)}
(P : A Prop) `{ x, ProofIrrel (P x)} : StrictOrder (@lexico (sig P) _).
Proof.
unfold lexico, sig_lexico. repeat split.
* by intros [??].
* intros [x1 ?] [x2 ?] [x3 ?] ??. by simplify_order.
* intros [x1 ?] [x2 ?] ??. apply (sig_eq_pi _). by simplify_order.
unfold lexico, sig_lexico. split.
* intros [x ?] ?. by apply (irreflexivity lexico x).
* intros [x1 ?] [x2 ?] [x3 ?] ??. by transitivity x2.
Qed.
Instance sig_lexico_trichotomy `{Lexico A} `{tA: !TrichotomyT (@lexico A _)}
(P : A Prop) `{ x, ProofIrrel (P x)} : TrichotomyT (@lexico (sig P) _).
......
......@@ -11,7 +11,6 @@ the relation [⊆] because we often have multiple orders on the same structure *
Section orders.
Context {A} {R : relation A}.
Implicit Types X Y : A.
Infix "⊆" := R.
Notation "X ⊈ Y" := (¬X Y).
Infix "⊂" := (strict R).
......@@ -71,25 +70,41 @@ Section orders.
Lemma total_not_strict `{!Total R} X Y : X Y Y X.
Proof. red; auto using total_not. Qed.
Global Instance trichotomyT_dec `{!TrichotomyT R} `{!Reflexive R} X Y :
Decision (X Y) :=
Global Instance trichotomy_total
`{!Trichotomy (strict R)} `{!Reflexive R} : Total R.
Proof.
intros X Y.
destruct (trichotomy (strict R) X Y) as [[??]|[<-|[??]]]; intuition.
Qed.
End orders.
Section strict_orders.
Context {A} {R : relation A}.
Implicit Types X Y : A.
Infix "⊂" := R.
Lemma irreflexive_eq `{!Irreflexive R} X Y : X = Y ¬X Y.
Proof. intros ->. apply (irreflexivity R). Qed.
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) :=
match trichotomyT R X Y with
| inleft (left H) => left (proj1 H)
| inleft (right H) => left (reflexive_eq _ _ H)
| inright H => right (proj2 H)
| 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.
Global Instance trichotomy_total `{!Trichotomy R} `{!Reflexive R} : Total R.
Proof.
intros X Y. destruct (trichotomy R X Y) as [[??]|[<-|[??]]]; intuition.
Qed.
End orders.
End strict_orders.
Ltac simplify_order := repeat
match goal with
| _ => progress simplify_equality
| H : strict _ ?x ?x |- _ => by destruct (irreflexivity _ _ H)
| H : ?R ?x ?x |- _ => by destruct (irreflexivity _ _ H)
| H1 : ?R ?x ?y |- _ =>
match goal with
| H2 : R y x |- _ =>
......
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