orders.v 3.73 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** Properties about arbitrary pre-, partial, and total orders. We do not use
the relation [⊆] because we often have multiple orders on the same structure *)
5 6
From iris.prelude Require Export tactics.

Robbert Krebbers's avatar
Robbert Krebbers committed
7 8 9 10 11 12 13 14 15
Section orders.
  Context {A} {R : relation A}.
  Implicit Types X Y : A.
  Infix "⊆" := R.
  Notation "X ⊈ Y" := (¬X  Y).
  Infix "⊂" := (strict R).

  Lemma reflexive_eq `{!Reflexive R} X Y : X = Y  X  Y.
  Proof. by intros <-. Qed.
16 17
  Lemma anti_symm_iff `{!PartialOrder R} X Y : X = Y  R X Y  R Y X.
  Proof. split. by intros ->. by intros [??]; apply (anti_symm _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
18 19 20 21 22 23 24 25 26 27
  Lemma strict_spec X Y : X  Y  X  Y  Y  X.
  Proof. done. Qed.
  Lemma strict_include X Y : X  Y  X  Y.
  Proof. by intros [? _]. Qed.
  Lemma strict_ne X Y : X  Y  X  Y.
  Proof. by intros [??] <-. Qed.
  Lemma strict_ne_sym X Y : X  Y  Y  X.
  Proof. by intros [??] <-. Qed.
  Lemma strict_transitive_l `{!Transitive R} X Y Z : X  Y  Y  Z  X  Z.
  Proof.
28 29
    intros [? HXY] ?. split; [by trans Y|].
    contradict HXY. by trans Z.
Robbert Krebbers's avatar
Robbert Krebbers committed
30 31 32
  Qed.
  Lemma strict_transitive_r `{!Transitive R} X Y Z : X  Y  Y  Z  X  Z.
  Proof.
33 34
    intros ? [? HYZ]. split; [by trans Y|].
    contradict HYZ. by trans X.
Robbert Krebbers's avatar
Robbert Krebbers committed
35 36 37 38 39 40 41 42 43 44
  Qed.
  Global Instance: Irreflexive (strict R).
  Proof. firstorder. Qed.
  Global Instance: Transitive R  StrictOrder (strict R).
  Proof.
    split; try apply _.
    eauto using strict_transitive_r, strict_include.
  Qed.
  Global Instance preorder_subset_dec_slow `{ X Y, Decision (X  Y)}
    (X Y : A) : Decision (X  Y) | 100 := _.
45
  Lemma strict_spec_alt `{!AntiSymm (=) R} X Y : X  Y  X  Y  X  Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
46 47
  Proof.
    split.
48 49
    - intros [? HYX]. split. done. by intros <-.
    - intros [? HXY]. split. done. by contradict HXY; apply (anti_symm R).
Robbert Krebbers's avatar
Robbert Krebbers committed
50 51 52 53 54
  Qed.
  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)));
55
     abstract (rewrite anti_symm_iff; tauto).
Robbert Krebbers's avatar
Robbert Krebbers committed
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75
  Defined.
  Lemma total_not `{!Total R} X Y : X  Y  Y  X.
  Proof. intros. destruct (total R X Y); tauto. Qed.
  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.
  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.
76
  Lemma strict_anti_symm `{!StrictOrder R} X Y :
Robbert Krebbers's avatar
Robbert Krebbers committed
77
    X  Y  Y  X  False.
78
  Proof. intros. apply (irreflexivity R X). by trans Y. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
79 80 81 82 83
  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)
84
    | inright H => right (strict_anti_symm _ _ H)
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86 87 88 89 90 91
    end.
  Global Instance trichotomyT_trichotomy `{!TrichotomyT R} : Trichotomy R.
  Proof. intros X Y. destruct (trichotomyT R X Y) as [[|]|]; tauto. Qed.
End strict_orders.

Ltac simplify_order := repeat
  match goal with
92
  | _ => progress simplify_eq/=
Robbert Krebbers's avatar
Robbert Krebbers committed
93 94 95 96
  | H : ?R ?x ?x |- _ => by destruct (irreflexivity _ _ H)
  | H1 : ?R ?x ?y |- _ =>
    match goal with
    | H2 : R y x |- _ =>
97
      assert (x = y) by (by apply (anti_symm R)); clear H1 H2
Robbert Krebbers's avatar
Robbert Krebbers committed
98 99
    | H2 : R y ?z |- _ =>
      unless (R x z) by done;
100
      assert (R x z) by (by trans y)
Robbert Krebbers's avatar
Robbert Krebbers committed
101 102
    end
  end.