orders.v 3.74 KB
 Robbert Krebbers committed Mar 15, 2017 1 ``````(* Copyright (c) 2012-2017, Coq-std++ developers. *) `````` Robbert Krebbers committed Aug 29, 2012 2 ``````(* This file is distributed under the terms of the BSD license. *) `````` Robbert Krebbers committed Aug 12, 2013 3 4 ``````(** Properties about arbitrary pre-, partial, and total orders. We do not use the relation [⊆] because we often have multiple orders on the same structure *) `````` Robbert Krebbers committed Jul 22, 2016 5 ``````From stdpp Require Export tactics. `````` Ralf Jung committed Jan 31, 2017 6 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Jul 22, 2016 7 `````` `````` Robbert Krebbers committed Aug 12, 2013 8 9 10 11 12 13 14 15 16 ``````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. `````` Robbert Krebbers committed Feb 11, 2016 17 18 `````` 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 committed Aug 12, 2013 19 20 21 22 23 24 25 26 27 28 `````` 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. `````` Ralf Jung committed Feb 20, 2016 29 30 `````` intros [? HXY] ?. split; [by trans Y|]. contradict HXY. by trans Z. `````` Robbert Krebbers committed Aug 12, 2013 31 32 33 `````` Qed. Lemma strict_transitive_r `{!Transitive R} X Y Z : X ⊆ Y → Y ⊂ Z → X ⊂ Z. Proof. `````` Ralf Jung committed Feb 20, 2016 34 35 `````` intros ? [? HYZ]. split; [by trans Y|]. contradict HYZ. by trans X. `````` Robbert Krebbers committed Aug 12, 2013 36 37 38 39 40 41 42 43 44 45 `````` 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 := _. `````` Robbert Krebbers committed Feb 11, 2016 46 `````` Lemma strict_spec_alt `{!AntiSymm (=) R} X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y. `````` Robbert Krebbers committed Aug 12, 2013 47 48 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 49 50 `````` - intros [? HYX]. split. done. by intros <-. - intros [? HXY]. split. done. by contradict HXY; apply (anti_symm R). `````` Robbert Krebbers committed Aug 12, 2013 51 `````` Qed. `````` Robbert Krebbers committed Sep 20, 2016 52 `````` Lemma po_eq_dec `{!PartialOrder R, ∀ X Y, Decision (X ⊆ Y)} : EqDecision A. `````` Robbert Krebbers committed Aug 12, 2013 53 `````` Proof. `````` Robbert Krebbers committed Sep 20, 2016 54 `````` refine (λ X Y, cast_if_and (decide (X ⊆ Y)) (decide (Y ⊆ X))); `````` Robbert Krebbers committed Feb 11, 2016 55 `````` abstract (rewrite anti_symm_iff; tauto). `````` Robbert Krebbers committed Aug 12, 2013 56 57 58 59 60 `````` 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. `````` Robbert Krebbers committed Sep 09, 2013 61 `````` Global Instance trichotomy_total `````` Robbert Krebbers committed Nov 15, 2014 62 `````` `{!Trichotomy (strict R), !Reflexive R} : Total R. `````` Robbert Krebbers committed Sep 09, 2013 63 64 65 66 67 68 69 70 71 72 73 74 75 `````` 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. `````` Robbert Krebbers committed Feb 11, 2016 76 `````` Lemma strict_anti_symm `{!StrictOrder R} X Y : `````` Robbert Krebbers committed Sep 09, 2013 77 `````` X ⊂ Y → Y ⊂ X → False. `````` Ralf Jung committed Feb 20, 2016 78 `````` Proof. intros. apply (irreflexivity R X). by trans Y. Qed. `````` Robbert Krebbers committed Nov 15, 2014 79 80 `````` Global Instance trichotomyT_dec `{!TrichotomyT R, !StrictOrder R} X Y : Decision (X ⊂ Y) := `````` Robbert Krebbers committed Aug 12, 2013 81 `````` match trichotomyT R X Y with `````` Robbert Krebbers committed Sep 09, 2013 82 83 `````` | inleft (left H) => left H | inleft (right H) => right (irreflexive_eq _ _ H) `````` Robbert Krebbers committed Feb 11, 2016 84 `````` | inright H => right (strict_anti_symm _ _ H) `````` Robbert Krebbers committed Aug 12, 2013 85 86 87 `````` end. Global Instance trichotomyT_trichotomy `{!TrichotomyT R} : Trichotomy R. Proof. intros X Y. destruct (trichotomyT R X Y) as [[|]|]; tauto. Qed. `````` Robbert Krebbers committed Sep 09, 2013 88 ``````End strict_orders. `````` Robbert Krebbers committed Aug 12, 2013 89 90 91 `````` Ltac simplify_order := repeat match goal with `````` Robbert Krebbers committed Feb 17, 2016 92 `````` | _ => progress simplify_eq/= `````` Robbert Krebbers committed Sep 09, 2013 93 `````` | H : ?R ?x ?x |- _ => by destruct (irreflexivity _ _ H) `````` Robbert Krebbers committed Aug 12, 2013 94 95 96 `````` | H1 : ?R ?x ?y |- _ => match goal with | H2 : R y x |- _ => `````` Robbert Krebbers committed Feb 11, 2016 97 `````` assert (x = y) by (by apply (anti_symm R)); clear H1 H2 `````` Robbert Krebbers committed Aug 12, 2013 98 99 `````` | H2 : R y ?z |- _ => unless (R x z) by done; `````` Ralf Jung committed Feb 20, 2016 100 `````` assert (R x z) by (by trans y) `````` Robbert Krebbers committed Aug 12, 2013 101 102 `````` end end.``````