Lvc.Infra.PartialOrder
Require Import Util LengthEq.
Require Import Containers.OrderedType Setoid Coq.Classes.Morphisms Computable Coq.Classes.RelationClasses.
Require Import Containers.OrderedTypeEx DecSolve MoreList.
Require Import OrderedTypeEx OrderedTypeComputable OrderedTypeLe.
Require Import AllInRel.
Create HintDb po discriminated.
Class PartialOrder (Dom:Type) := {
poLe : Dom → Dom → Prop;
poLe_dec :> ∀ d d', Computable (poLe d d');
poEq : Dom → Dom → Prop;
poEq_dec :> ∀ d d', Computable (poEq d d');
poEq_equivalence :> Equivalence poEq;
poLe_refl : ∀ d d', poEq d d' → poLe d d';
poLe_trans :> Transitive poLe;
poLe_antisymmetric :> Antisymmetric _ poEq poLe;
}.
Arguments poLe : simpl never.
Arguments poEq : simpl never.
Instance poLe_RR X `{PartialOrder X}
: RewriteRelation (@poLe X _).
Instance poEq_RR X `{PartialOrder X}
: RewriteRelation (@poEq X _).
Lemma poEq_sym A `{PartialOrder A} x y
: poEq x y → poEq y x.
Proof.
symmetry; eauto.
Qed.
Hint Immediate poEq_sym.
Instance PartialOrder_poLe_refl Dom `{PartialOrder Dom} : Reflexive poLe.
Proof.
hnf; intros. eapply poLe_refl. reflexivity.
Qed.
Hint Resolve poLe_refl poLe_antisymmetric | 100 : po.
Definition poLt {Dom} `{PartialOrder Dom} x y := poLe x y ∧ ¬ poLe y x.
Lemma poLt_intro Dom `{PartialOrder Dom} x y
: poLe x y → ¬ poEq x y → poLt x y.
Proof.
firstorder using poLe_antisymmetric.
Qed.
Lemma poLt_poLe Dom `{PartialOrder Dom} x y
: poLt x y → poLe x y.
Proof.
firstorder.
Qed.
Lemma poLt_not_poLe Dom `{PartialOrder Dom} x y
: poLt x y → ¬ poLe y x.
Proof.
firstorder.
Qed.
Hint Resolve poLt_intro poLt_poLe poLt_not_poLe | 100 : po.
Lemma poLt_not_poEq Dom `{PartialOrder Dom} x y
: poLt x y → ¬ poEq x y.
Proof.
firstorder with po.
Qed.
Lemma poLe_poLt Dom `{PartialOrder Dom} d d'
: poLe d d'
→ ¬ poLe d' d
→ poLt d d'.
Proof.
firstorder.
Qed.
Hint Resolve poLt_intro poLt_poLe poLe_refl poLe_antisymmetric | 100.
Lemma poLe_poEq_rel Dom `{PartialOrder Dom} d d'
: poEq d d' ↔ poLe d d' ∧ poLe d' d.
Proof.
split; intros.
- split; eapply poLe_refl; eauto.
- eapply poLe_antisymmetric; eauto.
Qed.
Notation "s '⊑' t" := (poLe s t) (at level 70, no associativity).
Notation "s '⊏' t" := (poLt s t) (at level 70, no associativity).
Notation "s '≣' t" := (poEq s t) (at level 70, no associativity).
Instance PartialOrder_prod_instance X `{PartialOrder X} Y `{PartialOrder Y}
: PartialOrder (X × Y) := {
poLe x y := poLe (fst x) (fst y) ∧ poLe (snd x) (snd y);
poLe_dec := _;
poEq x y := poEq (fst x) (fst y) ∧ poEq (snd x) (snd y);
poEq_dec := _
}.
Proof.
- econstructor.
+ hnf; intros; split; reflexivity.
+ hnf; intros; dcr; split; symmetry; eauto.
+ hnf; intros; dcr; split; etransitivity; eauto.
- intros; dcr; split; eapply poLe_refl; eauto.
- hnf; intros; dcr; split; etransitivity; eauto.
- hnf; intros; dcr; split; eapply poLe_antisymmetric; eauto.
Defined.
Lemma poEq_fst A `{PartialOrder A} B `{PartialOrder B} (a b:A × B)
: poEq a b → poEq (fst a) (fst b).
firstorder.
Qed.
Lemma poEq_snd A `{PartialOrder A} B `{PartialOrder B} (a b:A × B)
: poEq a b → poEq (snd a) (snd b).
firstorder.
Qed.
Lemma poEq_struct A `{PartialOrder A} B `{PartialOrder B} (a1 a2:A) (b1 b2:B)
: poEq a1 a2 → poEq b1 b2 → poEq (a1,b1) (a2,b2).
firstorder.
Qed.
Lemma poLe_fst A `{PartialOrder A} B `{PartialOrder B} (a b:A × B)
: poLe a b → poLe (fst a) (fst b).
firstorder.
Qed.
Lemma poLe_snd A `{PartialOrder A} B `{PartialOrder B} (a b:A × B)
: poLe a b → poLe (snd a) (snd b).
firstorder.
Qed.
Lemma poLe_struct A `{PartialOrder A} B `{PartialOrder B} (a1 a2:A) (b1 b2:B)
: poLe a1 a2 → poLe b1 b2 → poLe (a1,b1) (a2,b2).
firstorder.
Qed.
Hint Resolve poEq_fst poEq_snd poEq_struct poLe_fst poLe_snd poLe_struct.
Hint Resolve poEq_fst poEq_snd poEq_struct poLe_fst poLe_snd poLe_struct : po.
Instance poEq_pair_proper X `{PartialOrder X} Y `{PartialOrder Y}
: Proper (poEq ==> poEq ==> poEq) (@pair X Y).
Proof.
unfold Proper, respectful; intros.
eapply poEq_struct; eauto.
Qed.
Instance poLe_pair_proper X `{PartialOrder X} Y `{PartialOrder Y}
: Proper (poLe ==> poLe ==> poLe) (@pair X Y).
Proof.
unfold Proper, respectful; intros.
eapply poLe_struct; eauto.
Qed.
Instance PartialOrder_list_instance X `{PartialOrder X}
: PartialOrder (list X) := {
poLe := list_eq poLe;
poLe_dec := _;
poEq := list_eq poEq;
poEq_dec := _
}.
Proof.
- intros. general induction H0; eauto using @list_eq, poLe_refl.
- intros ? ? ? R1 R2.
general induction R1; inv R2; eauto using @list_eq, poLe_trans.
- intros ? ? EQ1 EQ2.
exploit list_eq_length as LEN; eauto. length_equify.
general induction LEN; inv EQ1; inv EQ2; eauto using @list_eq, poLe_antisymmetric.
Defined.
Instance poLe_poEq_impl Dom `{PartialOrder Dom}
: Proper (poEq ==> poEq ==> impl) poLe.
Proof.
unfold Proper, respectful, impl; intros.
symmetry in H0.
- eapply poLe_refl in H0. eapply poLe_refl in H1.
etransitivity; eauto. etransitivity; eauto.
Qed.
Instance poLe_poEq_flip_impl Dom `{PartialOrder Dom}
: Proper (poEq ==> poEq ==> flip impl) poLe.
Proof.
unfold Proper, respectful, flip, impl; intros.
- eapply poLe_refl in H0. symmetry in H1. eapply poLe_refl in H1.
etransitivity; eauto. etransitivity; eauto.
Qed.
Instance poLe_poEq_iff Dom `{PartialOrder Dom}
: Proper (poEq ==> poEq ==> iff) poLe.
Proof.
unfold Proper, respectful, impl; intros.
split; intros.
- rewrite <- H0. rewrite H2. eauto using poLe_refl.
- rewrite H0. rewrite H1. eauto using poLe_refl.
Qed.
Instance poLt_poLe_impl Dom `{PartialOrder Dom}
: Proper (flip poLe ==> poLe ==> impl) poLt.
Proof.
unfold Proper, respectful, flip, impl; intros.
destruct H2. split; intros.
- etransitivity; eauto. etransitivity; eauto.
- intro. eapply H3.
etransitivity; eauto. rewrite H4. eauto.
Qed.
Instance poLt_poLe_flip_impl Dom `{PartialOrder Dom}
: Proper (poLe ==> flip poLe ==> flip impl) poLt.
Proof.
unfold Proper, respectful, flip, impl; intros.
destruct H2. split; intros.
- etransitivity; eauto. etransitivity; eauto.
- intro. eapply H3.
etransitivity; eauto. rewrite H4. eauto.
Qed.
Instance poLt_poLe_iff Dom `{PartialOrder Dom}
: Proper (poEq ==> poEq ==> iff) poLt.
Proof.
unfold Proper, respectful, flip, impl; intros.
unfold poLt. rewrite H0, H1. reflexivity.
Qed.
Instance PartialOrder_list Dom `{PartialOrder Dom}
: PartialOrder (list Dom) := {
poLe := PIR2 poLe;
poLe_dec := @PIR2_computable _ _ poLe poLe_dec;
poEq := PIR2 poEq;
poEq_dec := @PIR2_computable _ _ poEq poEq_dec;
}.
Proof.
- intros. general induction H0; eauto using @PIR2, poLe_refl.
- intros ? ? A B. general induction A; inv B; eauto 20 using @PIR2, poLe_antisymmetric.
Defined.
Instance poEq_cons X `{PartialOrder X}
: Proper (poEq ==> poEq ==> poEq) cons.
Proof.
unfold Proper, respectful; intros.
econstructor; eauto.
Qed.
Instance poLt_poLe_PIR2_flip_impl Dom `{PartialOrder Dom}
: (Proper (PIR2 poLe ==> flip poLe ==> flip impl) poLt).
Proof.
unfold Proper, respectful, flip, impl; intros.
eapply poLt_poLe_flip_impl; eauto.
Qed.
Hint Extern 5 (poLe ?a ?a) ⇒ reflexivity.
Hint Extern 5 (poEq ?a ?a) ⇒ reflexivity.
Hint Extern 5 (poLe ?a ?a') ⇒ progress (first [has_evar a | has_evar a' | reflexivity]).
Hint Extern 5 (poEq ?a ?a') ⇒ progress (first [has_evar a | has_evar a' | reflexivity]).
Hint Extern 10 ⇒
match goal with
| [ H : poLe ?a ?b, H': poLe ?b ?c |- poLe ?a ?c ] ⇒
etransitivity; [ eapply H | eapply H' ]
| [ H : poLe ?a ?b, H': PIR2 _ ?b ?c |- poLe ?a ?c ] ⇒
etransitivity; [ eapply H | eapply H' ]
| [ H : poLe ?a ?b, H': poLe ?b ?c, H'' : poLe ?c ?d |- poLe ?a ?d ] ⇒
etransitivity; [ eapply H | etransitivity; [ eapply H' | eapply H''] ]
| [ H : PIR2 poLe ?a ?b, H': PIR2 poLe ?b ?c |- PIR2 poLe ?a ?c ] ⇒
etransitivity; [ eapply H | eapply H' ]
| [ H : PIR2 poLe ?a ?b, H': PIR2 poLe ?b ?c, H'' : PIR2 poLe ?c ?d |- PIR2 poLe ?a ?d ] ⇒
etransitivity; [ eapply H | etransitivity; [ eapply H' | eapply H''] ]
| [ H : poLe ?a ?b, H': PIR2 _ ?b ?c, H'' : poLe ?c ?d |- poLe ?a ?d ] ⇒
etransitivity; [ eapply H | etransitivity; [ eapply H' | eapply H''] ]
| [ H : poLe ?a ?b, H' : poLe ?b ?c, H'' : ¬ poEq ?b ?c |- poLt ?a ?c ] ⇒
rewrite H; eapply (@poLt_intro _ _ _ _ H' H'')
| [ H : poLe ?a ?b, H' : PIR2 _ ?b ?c, H'' : ¬ poEq ?b ?c |- poLt ?a ?c ] ⇒
rewrite H; eapply poLt_intro; [ eapply H' | eapply H'']
| [ H : poLt ?a ?b, H': poLe ?b ?c |- poLt ?a ?c ] ⇒
rewrite <- H'; eapply H
| [ H : poLe ?a ?b, H': poEq ?b ?c |- poLe ?a ?c ] ⇒
rewrite <- H'; eapply H
end.
Instance PartialOrder_sig Dom `{PartialOrder Dom} (P:Dom → Prop)
: PartialOrder { x :Dom | P x } := {
poLe x y := poLe (proj1_sig x) (proj1_sig y);
poLe_dec := _;
poEq x y := poEq (proj1_sig x) (proj1_sig y);
poEq_dec := _;
}.
Proof.
- econstructor; hnf; intros; destruct x; try destruct y; try destruct z; simpl in ×.
+ reflexivity.
+ symmetry; eauto.
+ etransitivity; eauto.
- intros [a b] [c d]; simpl. eapply poLe_refl.
- intros [a b] [c d] [e f]; simpl; intros.
etransitivity; eauto.
- intros [a b] [c d]; simpl; intros.
eapply poLe_antisymmetric; eauto.
Defined.
Instance PartialOrder_bool
: PartialOrder bool := {
poLe := impb;
poLe_dec := _;
poEq := eq;
poEq_dec := _;
}.
Proof.
- intros. unfold impb. hnf. destruct d, d'; try dec_solve; eauto.
- hnf; unfold impb. intros. destruct d,d'; simpl; eauto using bool.
congruence.
- hnf; unfold impb. intros. destruct x,y; eauto. exfalso; eauto.
Defined.
Instance fst_poLe Dom `{PartialOrder Dom} Dom' `{PartialOrder Dom'}
: Proper (poLe ==> poLe) (@fst Dom Dom').
Proof.
unfold Proper, respectful; intros.
inv H1; simpl; eauto.
Qed.
Instance snd_poLe Dom `{PartialOrder Dom} Dom' `{PartialOrder Dom'}
: Proper (poLe ==> poLe) (@snd Dom Dom').
Proof.
unfold Proper, respectful; intros.
inv H1; simpl; eauto.
Qed.
Instance fst_poEq Dom `{PartialOrder Dom} Dom' `{PartialOrder Dom'}
: Proper (poEq ==> poEq) (@fst Dom Dom').
Proof.
unfold Proper, respectful; intros.
inv H1; simpl; eauto.
Qed.
Instance snd_poEq Dom `{PartialOrder Dom} Dom' `{PartialOrder Dom'}
: Proper (poEq ==> poEq) (@snd Dom Dom').
Proof.
unfold Proper, respectful; intros.
inv H1; simpl; eauto.
Qed.
Lemma not_poLt_poLe_poEq X `{PartialOrder X} x y
: ¬ x ⊏ y → poLe x y → x === y.
Proof.
intros.
eapply poLe_antisymmetric; eauto.
decide_goal; eauto.
exfalso. eapply H0. split; eauto.
Qed.
Hint Resolve not_poLt_poLe_poEq : po.
Smpl Add 200
match goal with
| [ H : ?A === ?B |- _ ] ⇒ inv_if_ctor H A B; clear H
| [ H : @poEq _ _ ?A ?B |- _ ] ⇒ inv_if_one_ctor_and_var H A B; clear H
| [ H : @poLe _ _ ?A ?B |- _ ] ⇒ inv_if_one_ctor_and_var H A B; clear H
| [ H : ¬ ?a === ?a |- _ ] ⇒ exfalso; eapply H; reflexivity
end : inv_trivial.
Lemma poEq_pair_inv A `{PartialOrder A} B `{PartialOrder B} (x y:A × B)
: poEq x y ↔ poEq (fst x) (fst y) ∧ poEq (snd x) (snd y).
Proof.
firstorder.
Qed.
Lemma poLe_pair_inv A `{PartialOrder A} B `{PartialOrder B} (x y:A × B)
: poLe x y ↔ poLe (fst x) (fst y) ∧ poLe (snd x) (snd y).
Proof.
firstorder.
Qed.
Smpl Add 120
match goal with
| [ H : poEq (_,_) (_,_) |- _ ] ⇒
rewrite poEq_pair_inv in H; simpl fst in H; simpl snd in H;
let H' := fresh H in destruct H as [H H']
| [ H : poLe (_,_) (_,_) |- _ ] ⇒
rewrite poLe_pair_inv in H; simpl fst in H; simpl snd in H;
let H' := fresh H in destruct H as [H H']
| [H : poEq ?x ?x |- _ ] ⇒ clear H
| [H : poLe ?x ?x |- _ ] ⇒ clear H
end : inv_trivial.
Ltac is_in_context X :=
match goal with
| [ H : ?Y |- _ ] ⇒
unify X Y
end.
Lemma poLe_false x
: x ⊑ false → x = false.
Proof.
destruct x; inversion 1; eauto.
Qed.
Lemma poLe_true x
: true ⊑ x → x = true.
Proof.
destruct x; inversion 1; eauto.
Qed.
Smpl Add match goal with
| [ H : _ ⊑ false |- _ ] ⇒ eapply poLe_false in H; try subst
| [ H : false ⊑ _ |- _ ] ⇒ eapply poLe_false in H; try subst
end : inv_trivial.
Lemma poLe_sig_struct D `{PartialOrder D} (P: D → Prop) (x x':D) pf pf'
: x ⊑ x'
→ @poLe _ (@PartialOrder_sig D _ P) (exist P x pf) (exist P x' pf').
Proof.
intros. simpl. eapply H0.
Qed.
Lemma poLe_sig_struct' D `{PartialOrder D} (P: D → Prop) (x x':{x : D | P x})
: proj1_sig x ⊑ proj1_sig x'
→ x ⊑ x'.
Proof.
intros. simpl. eapply H0.
Qed.
Lemma poEq_sig_struct D `{PartialOrder D} (P: D → Prop) (x x':D) pf pf'
: x ≣ x'
→ @poEq _ (@PartialOrder_sig D _ P) (exist P x pf) (exist P x' pf').
Proof.
intros. simpl. eapply H0.
Qed.
Lemma poEq_sig_struct' D `{PartialOrder D} (P: D → Prop) (x x':D) pf pf'
: @poEq _ (@PartialOrder_sig D _ P) (exist P x pf) (exist P x' pf')
→ x ≣ x'.
Proof.
intros. eapply H0.
Qed.
Lemma poLe_sig_struct'' D `{PartialOrder D} (P: D → Prop) (x x':D) pf pf'
: @poLe _ (@PartialOrder_sig D _ P) (exist P x pf) (exist P x' pf')
→ x ⊑ x'.
Proof.
intros. eapply H0.
Qed.
Lemma poLe_sig_destruct D `{PartialOrder D} (P: D → Prop) (x x':{x : D | P x})
: x ⊑ x'
→ proj1_sig x ⊑ proj1_sig x'.
Proof.
intros. eapply H0.
Qed.
Lemma poEq_sig_destruct D `{PartialOrder D} (P: D → Prop) (x x':{x : D | P x})
: x ≣ x'
→ proj1_sig x ≣ proj1_sig x'.
Proof.
intros. eapply H0.
Qed.
Hint Resolve poLe_sig_destruct poEq_sig_destruct.
Lemma poLe_list_struct A `{PartialOrder A} (a1 a2:A) b1 b2
: poLe a1 a2 → poLe b1 b2 → poLe (a1::b1) (a2::b2).
intros; econstructor; eauto.
Qed.
Lemma poEq_list_struct A `{PartialOrder A} (a1 a2:A) b1 b2
: poEq a1 a2 → poEq b1 b2 → poEq (a1::b1) (a2::b2).
intros; econstructor; eauto.
Qed.
Hint Resolve poLe_list_struct poEq_list_struct.
Lemma poLe_map D `{PartialOrder D} D' `{PartialOrder D'} (f g:D → D') (L L':list D)
(LEf:∀ a b, poLe a b → poLe (f a) (g b))
(LE: poLe L L')
: poLe (f ⊝ L) (g ⊝ L').
Proof.
general induction LE; simpl; eauto.
Qed.
Lemma poLe_map_nd D D' `{PartialOrder D'} (f g:D → D') (L:list D)
(LEf:∀ a, poLe (f a) (g a))
: poLe (f ⊝ L) (g ⊝ L).
Proof.
general induction L; simpl; eauto.
Qed.
Lemma poEq_map D `{PartialOrder D} D' `{PartialOrder D'} (f g:D → D') (L L':list D)
(LEf:∀ a b, poEq a b → poEq (f a) (g b))
(LE: poEq L L')
: poEq (f ⊝ L) (g ⊝ L').
Proof.
general induction LE; simpl; eauto.
Qed.
Lemma poEq_map_nd D D' `{PartialOrder D'} (f g:D → D') (L:list D)
(LEf:∀ a, poEq (f a) (g a))
: poEq (f ⊝ L) (g ⊝ L).
Proof.
general induction L; simpl; eauto.
Qed.
Instance poLe_poLe_impl (Dom : Type) (H : PartialOrder Dom)
: Proper (poLe --> poLe ==> impl) poLe.
Proof.
unfold Proper, respectful , flip, impl; intros.
eauto.
Qed.
Instance poLe_poLe_flip_impl (Dom : Type) (H : PartialOrder Dom)
: Proper (poLe ==> flip poLe ==> flip impl) poLe.
Proof.
unfold Proper, respectful, flip, impl; intros ? ? A ? ? B C.
eauto.
Qed.
Lemma poLe_app X `{PartialOrder X} (L1 L2 : 〔X〕) (L1' L2' : 〔X〕)
: poLe L1 L1' → poLe L2 L2' → poLe (L1 ++ L2) (L1' ++ L2').
Proof.
intros. eapply PIR2_app; eauto.
Qed.
Lemma poEq_app X `{PartialOrder X} (L1 L2 : 〔X〕) (L1' L2' : 〔X〕)
: poEq L1 L1' → poEq L2 L2' → poEq (L1 ++ L2) (L1' ++ L2').
Proof.
intros. eapply PIR2_app; eauto.
Qed.
Hint Resolve poLe_app poEq_app.
Lemma poLe_app_proper X `{PartialOrder X}
: Proper (poLe ==> poLe ==> poLe) (@List.app X).
Proof.
unfold Proper, respectful; intros; eauto.
Qed.
Lemma poLe_app_proper_funny X `{PartialOrder X} L
: Proper (flip poLe ==> flip poLe) (@List.app X L).
Proof.
unfold Proper, respectful, flip; intros; eauto.
Qed.
Lemma poLe_app_proper' X `{PartialOrder X}
: Proper (flip poLe ==> flip poLe ==> flip poLe) (@List.app X).
Proof.
unfold Proper, respectful, flip; intros; eauto.
Qed.
Lemma poLe_app_proper_poEq X `{PartialOrder X}
: Proper (poEq ==> poEq ==> poEq) (@List.app X).
Proof.
unfold Proper, respectful; intros; eauto.
Qed.
Instance orb_poEq_proper : Proper (poEq ==> poEq ==> poEq) orb.
Proof.
intuition.
Qed.
Hint Resolve orb_poEq_proper.
Instance poLe_length_proper X `{PartialOrder X}
: Proper (poLe ==> eq) (@length X).
Proof.
unfold Proper, respectful; intros.
hnf in H0. eapply PIR2_length in H0. eauto.
Qed.
Instance poEq_length_proper X `{PartialOrder X}
: Proper (poEq ==> eq) (@length X).
Proof.
unfold Proper, respectful; intros.
hnf in H0. eapply PIR2_length in H0. eauto.
Qed.
Instance poLt_irr X `{PartialOrder X} : Irreflexive poLt.
Proof.
hnf. unfold complement. intros ? [? ?]. eauto.
Qed.
Instance poLt_trans X `{PartialOrder X} : Transitive poLt.
Proof.
hnf; intros.
unfold poLt in ×.
destruct H0, H1; eauto.
Qed.
(* Explicit Instance *)
Lemma ot_po X `{OrderedType X} : PartialOrder X.
eapply Build_PartialOrder with
(poLe := _le) (poEq := _eq); eauto using OT_le_refl with typeclass_instances.
Defined.
Lemma po_strict_order X `{PartialOrder X} : StrictOrder poLt.
econstructor; eauto with typeclass_instances.
Qed.
Require Import Containers.OrderedType Setoid Coq.Classes.Morphisms Computable Coq.Classes.RelationClasses.
Require Import Containers.OrderedTypeEx DecSolve MoreList.
Require Import OrderedTypeEx OrderedTypeComputable OrderedTypeLe.
Require Import AllInRel.
Create HintDb po discriminated.
Class PartialOrder (Dom:Type) := {
poLe : Dom → Dom → Prop;
poLe_dec :> ∀ d d', Computable (poLe d d');
poEq : Dom → Dom → Prop;
poEq_dec :> ∀ d d', Computable (poEq d d');
poEq_equivalence :> Equivalence poEq;
poLe_refl : ∀ d d', poEq d d' → poLe d d';
poLe_trans :> Transitive poLe;
poLe_antisymmetric :> Antisymmetric _ poEq poLe;
}.
Arguments poLe : simpl never.
Arguments poEq : simpl never.
Instance poLe_RR X `{PartialOrder X}
: RewriteRelation (@poLe X _).
Instance poEq_RR X `{PartialOrder X}
: RewriteRelation (@poEq X _).
Lemma poEq_sym A `{PartialOrder A} x y
: poEq x y → poEq y x.
Proof.
symmetry; eauto.
Qed.
Hint Immediate poEq_sym.
Instance PartialOrder_poLe_refl Dom `{PartialOrder Dom} : Reflexive poLe.
Proof.
hnf; intros. eapply poLe_refl. reflexivity.
Qed.
Hint Resolve poLe_refl poLe_antisymmetric | 100 : po.
Definition poLt {Dom} `{PartialOrder Dom} x y := poLe x y ∧ ¬ poLe y x.
Lemma poLt_intro Dom `{PartialOrder Dom} x y
: poLe x y → ¬ poEq x y → poLt x y.
Proof.
firstorder using poLe_antisymmetric.
Qed.
Lemma poLt_poLe Dom `{PartialOrder Dom} x y
: poLt x y → poLe x y.
Proof.
firstorder.
Qed.
Lemma poLt_not_poLe Dom `{PartialOrder Dom} x y
: poLt x y → ¬ poLe y x.
Proof.
firstorder.
Qed.
Hint Resolve poLt_intro poLt_poLe poLt_not_poLe | 100 : po.
Lemma poLt_not_poEq Dom `{PartialOrder Dom} x y
: poLt x y → ¬ poEq x y.
Proof.
firstorder with po.
Qed.
Lemma poLe_poLt Dom `{PartialOrder Dom} d d'
: poLe d d'
→ ¬ poLe d' d
→ poLt d d'.
Proof.
firstorder.
Qed.
Hint Resolve poLt_intro poLt_poLe poLe_refl poLe_antisymmetric | 100.
Lemma poLe_poEq_rel Dom `{PartialOrder Dom} d d'
: poEq d d' ↔ poLe d d' ∧ poLe d' d.
Proof.
split; intros.
- split; eapply poLe_refl; eauto.
- eapply poLe_antisymmetric; eauto.
Qed.
Notation "s '⊑' t" := (poLe s t) (at level 70, no associativity).
Notation "s '⊏' t" := (poLt s t) (at level 70, no associativity).
Notation "s '≣' t" := (poEq s t) (at level 70, no associativity).
Instance PartialOrder_prod_instance X `{PartialOrder X} Y `{PartialOrder Y}
: PartialOrder (X × Y) := {
poLe x y := poLe (fst x) (fst y) ∧ poLe (snd x) (snd y);
poLe_dec := _;
poEq x y := poEq (fst x) (fst y) ∧ poEq (snd x) (snd y);
poEq_dec := _
}.
Proof.
- econstructor.
+ hnf; intros; split; reflexivity.
+ hnf; intros; dcr; split; symmetry; eauto.
+ hnf; intros; dcr; split; etransitivity; eauto.
- intros; dcr; split; eapply poLe_refl; eauto.
- hnf; intros; dcr; split; etransitivity; eauto.
- hnf; intros; dcr; split; eapply poLe_antisymmetric; eauto.
Defined.
Lemma poEq_fst A `{PartialOrder A} B `{PartialOrder B} (a b:A × B)
: poEq a b → poEq (fst a) (fst b).
firstorder.
Qed.
Lemma poEq_snd A `{PartialOrder A} B `{PartialOrder B} (a b:A × B)
: poEq a b → poEq (snd a) (snd b).
firstorder.
Qed.
Lemma poEq_struct A `{PartialOrder A} B `{PartialOrder B} (a1 a2:A) (b1 b2:B)
: poEq a1 a2 → poEq b1 b2 → poEq (a1,b1) (a2,b2).
firstorder.
Qed.
Lemma poLe_fst A `{PartialOrder A} B `{PartialOrder B} (a b:A × B)
: poLe a b → poLe (fst a) (fst b).
firstorder.
Qed.
Lemma poLe_snd A `{PartialOrder A} B `{PartialOrder B} (a b:A × B)
: poLe a b → poLe (snd a) (snd b).
firstorder.
Qed.
Lemma poLe_struct A `{PartialOrder A} B `{PartialOrder B} (a1 a2:A) (b1 b2:B)
: poLe a1 a2 → poLe b1 b2 → poLe (a1,b1) (a2,b2).
firstorder.
Qed.
Hint Resolve poEq_fst poEq_snd poEq_struct poLe_fst poLe_snd poLe_struct.
Hint Resolve poEq_fst poEq_snd poEq_struct poLe_fst poLe_snd poLe_struct : po.
Instance poEq_pair_proper X `{PartialOrder X} Y `{PartialOrder Y}
: Proper (poEq ==> poEq ==> poEq) (@pair X Y).
Proof.
unfold Proper, respectful; intros.
eapply poEq_struct; eauto.
Qed.
Instance poLe_pair_proper X `{PartialOrder X} Y `{PartialOrder Y}
: Proper (poLe ==> poLe ==> poLe) (@pair X Y).
Proof.
unfold Proper, respectful; intros.
eapply poLe_struct; eauto.
Qed.
Instance PartialOrder_list_instance X `{PartialOrder X}
: PartialOrder (list X) := {
poLe := list_eq poLe;
poLe_dec := _;
poEq := list_eq poEq;
poEq_dec := _
}.
Proof.
- intros. general induction H0; eauto using @list_eq, poLe_refl.
- intros ? ? ? R1 R2.
general induction R1; inv R2; eauto using @list_eq, poLe_trans.
- intros ? ? EQ1 EQ2.
exploit list_eq_length as LEN; eauto. length_equify.
general induction LEN; inv EQ1; inv EQ2; eauto using @list_eq, poLe_antisymmetric.
Defined.
Instance poLe_poEq_impl Dom `{PartialOrder Dom}
: Proper (poEq ==> poEq ==> impl) poLe.
Proof.
unfold Proper, respectful, impl; intros.
symmetry in H0.
- eapply poLe_refl in H0. eapply poLe_refl in H1.
etransitivity; eauto. etransitivity; eauto.
Qed.
Instance poLe_poEq_flip_impl Dom `{PartialOrder Dom}
: Proper (poEq ==> poEq ==> flip impl) poLe.
Proof.
unfold Proper, respectful, flip, impl; intros.
- eapply poLe_refl in H0. symmetry in H1. eapply poLe_refl in H1.
etransitivity; eauto. etransitivity; eauto.
Qed.
Instance poLe_poEq_iff Dom `{PartialOrder Dom}
: Proper (poEq ==> poEq ==> iff) poLe.
Proof.
unfold Proper, respectful, impl; intros.
split; intros.
- rewrite <- H0. rewrite H2. eauto using poLe_refl.
- rewrite H0. rewrite H1. eauto using poLe_refl.
Qed.
Instance poLt_poLe_impl Dom `{PartialOrder Dom}
: Proper (flip poLe ==> poLe ==> impl) poLt.
Proof.
unfold Proper, respectful, flip, impl; intros.
destruct H2. split; intros.
- etransitivity; eauto. etransitivity; eauto.
- intro. eapply H3.
etransitivity; eauto. rewrite H4. eauto.
Qed.
Instance poLt_poLe_flip_impl Dom `{PartialOrder Dom}
: Proper (poLe ==> flip poLe ==> flip impl) poLt.
Proof.
unfold Proper, respectful, flip, impl; intros.
destruct H2. split; intros.
- etransitivity; eauto. etransitivity; eauto.
- intro. eapply H3.
etransitivity; eauto. rewrite H4. eauto.
Qed.
Instance poLt_poLe_iff Dom `{PartialOrder Dom}
: Proper (poEq ==> poEq ==> iff) poLt.
Proof.
unfold Proper, respectful, flip, impl; intros.
unfold poLt. rewrite H0, H1. reflexivity.
Qed.
Instance PartialOrder_list Dom `{PartialOrder Dom}
: PartialOrder (list Dom) := {
poLe := PIR2 poLe;
poLe_dec := @PIR2_computable _ _ poLe poLe_dec;
poEq := PIR2 poEq;
poEq_dec := @PIR2_computable _ _ poEq poEq_dec;
}.
Proof.
- intros. general induction H0; eauto using @PIR2, poLe_refl.
- intros ? ? A B. general induction A; inv B; eauto 20 using @PIR2, poLe_antisymmetric.
Defined.
Instance poEq_cons X `{PartialOrder X}
: Proper (poEq ==> poEq ==> poEq) cons.
Proof.
unfold Proper, respectful; intros.
econstructor; eauto.
Qed.
Instance poLt_poLe_PIR2_flip_impl Dom `{PartialOrder Dom}
: (Proper (PIR2 poLe ==> flip poLe ==> flip impl) poLt).
Proof.
unfold Proper, respectful, flip, impl; intros.
eapply poLt_poLe_flip_impl; eauto.
Qed.
Hint Extern 5 (poLe ?a ?a) ⇒ reflexivity.
Hint Extern 5 (poEq ?a ?a) ⇒ reflexivity.
Hint Extern 5 (poLe ?a ?a') ⇒ progress (first [has_evar a | has_evar a' | reflexivity]).
Hint Extern 5 (poEq ?a ?a') ⇒ progress (first [has_evar a | has_evar a' | reflexivity]).
Hint Extern 10 ⇒
match goal with
| [ H : poLe ?a ?b, H': poLe ?b ?c |- poLe ?a ?c ] ⇒
etransitivity; [ eapply H | eapply H' ]
| [ H : poLe ?a ?b, H': PIR2 _ ?b ?c |- poLe ?a ?c ] ⇒
etransitivity; [ eapply H | eapply H' ]
| [ H : poLe ?a ?b, H': poLe ?b ?c, H'' : poLe ?c ?d |- poLe ?a ?d ] ⇒
etransitivity; [ eapply H | etransitivity; [ eapply H' | eapply H''] ]
| [ H : PIR2 poLe ?a ?b, H': PIR2 poLe ?b ?c |- PIR2 poLe ?a ?c ] ⇒
etransitivity; [ eapply H | eapply H' ]
| [ H : PIR2 poLe ?a ?b, H': PIR2 poLe ?b ?c, H'' : PIR2 poLe ?c ?d |- PIR2 poLe ?a ?d ] ⇒
etransitivity; [ eapply H | etransitivity; [ eapply H' | eapply H''] ]
| [ H : poLe ?a ?b, H': PIR2 _ ?b ?c, H'' : poLe ?c ?d |- poLe ?a ?d ] ⇒
etransitivity; [ eapply H | etransitivity; [ eapply H' | eapply H''] ]
| [ H : poLe ?a ?b, H' : poLe ?b ?c, H'' : ¬ poEq ?b ?c |- poLt ?a ?c ] ⇒
rewrite H; eapply (@poLt_intro _ _ _ _ H' H'')
| [ H : poLe ?a ?b, H' : PIR2 _ ?b ?c, H'' : ¬ poEq ?b ?c |- poLt ?a ?c ] ⇒
rewrite H; eapply poLt_intro; [ eapply H' | eapply H'']
| [ H : poLt ?a ?b, H': poLe ?b ?c |- poLt ?a ?c ] ⇒
rewrite <- H'; eapply H
| [ H : poLe ?a ?b, H': poEq ?b ?c |- poLe ?a ?c ] ⇒
rewrite <- H'; eapply H
end.
Instance PartialOrder_sig Dom `{PartialOrder Dom} (P:Dom → Prop)
: PartialOrder { x :Dom | P x } := {
poLe x y := poLe (proj1_sig x) (proj1_sig y);
poLe_dec := _;
poEq x y := poEq (proj1_sig x) (proj1_sig y);
poEq_dec := _;
}.
Proof.
- econstructor; hnf; intros; destruct x; try destruct y; try destruct z; simpl in ×.
+ reflexivity.
+ symmetry; eauto.
+ etransitivity; eauto.
- intros [a b] [c d]; simpl. eapply poLe_refl.
- intros [a b] [c d] [e f]; simpl; intros.
etransitivity; eauto.
- intros [a b] [c d]; simpl; intros.
eapply poLe_antisymmetric; eauto.
Defined.
Instance PartialOrder_bool
: PartialOrder bool := {
poLe := impb;
poLe_dec := _;
poEq := eq;
poEq_dec := _;
}.
Proof.
- intros. unfold impb. hnf. destruct d, d'; try dec_solve; eauto.
- hnf; unfold impb. intros. destruct d,d'; simpl; eauto using bool.
congruence.
- hnf; unfold impb. intros. destruct x,y; eauto. exfalso; eauto.
Defined.
Instance fst_poLe Dom `{PartialOrder Dom} Dom' `{PartialOrder Dom'}
: Proper (poLe ==> poLe) (@fst Dom Dom').
Proof.
unfold Proper, respectful; intros.
inv H1; simpl; eauto.
Qed.
Instance snd_poLe Dom `{PartialOrder Dom} Dom' `{PartialOrder Dom'}
: Proper (poLe ==> poLe) (@snd Dom Dom').
Proof.
unfold Proper, respectful; intros.
inv H1; simpl; eauto.
Qed.
Instance fst_poEq Dom `{PartialOrder Dom} Dom' `{PartialOrder Dom'}
: Proper (poEq ==> poEq) (@fst Dom Dom').
Proof.
unfold Proper, respectful; intros.
inv H1; simpl; eauto.
Qed.
Instance snd_poEq Dom `{PartialOrder Dom} Dom' `{PartialOrder Dom'}
: Proper (poEq ==> poEq) (@snd Dom Dom').
Proof.
unfold Proper, respectful; intros.
inv H1; simpl; eauto.
Qed.
Lemma not_poLt_poLe_poEq X `{PartialOrder X} x y
: ¬ x ⊏ y → poLe x y → x === y.
Proof.
intros.
eapply poLe_antisymmetric; eauto.
decide_goal; eauto.
exfalso. eapply H0. split; eauto.
Qed.
Hint Resolve not_poLt_poLe_poEq : po.
Smpl Add 200
match goal with
| [ H : ?A === ?B |- _ ] ⇒ inv_if_ctor H A B; clear H
| [ H : @poEq _ _ ?A ?B |- _ ] ⇒ inv_if_one_ctor_and_var H A B; clear H
| [ H : @poLe _ _ ?A ?B |- _ ] ⇒ inv_if_one_ctor_and_var H A B; clear H
| [ H : ¬ ?a === ?a |- _ ] ⇒ exfalso; eapply H; reflexivity
end : inv_trivial.
Lemma poEq_pair_inv A `{PartialOrder A} B `{PartialOrder B} (x y:A × B)
: poEq x y ↔ poEq (fst x) (fst y) ∧ poEq (snd x) (snd y).
Proof.
firstorder.
Qed.
Lemma poLe_pair_inv A `{PartialOrder A} B `{PartialOrder B} (x y:A × B)
: poLe x y ↔ poLe (fst x) (fst y) ∧ poLe (snd x) (snd y).
Proof.
firstorder.
Qed.
Smpl Add 120
match goal with
| [ H : poEq (_,_) (_,_) |- _ ] ⇒
rewrite poEq_pair_inv in H; simpl fst in H; simpl snd in H;
let H' := fresh H in destruct H as [H H']
| [ H : poLe (_,_) (_,_) |- _ ] ⇒
rewrite poLe_pair_inv in H; simpl fst in H; simpl snd in H;
let H' := fresh H in destruct H as [H H']
| [H : poEq ?x ?x |- _ ] ⇒ clear H
| [H : poLe ?x ?x |- _ ] ⇒ clear H
end : inv_trivial.
Ltac is_in_context X :=
match goal with
| [ H : ?Y |- _ ] ⇒
unify X Y
end.
Lemma poLe_false x
: x ⊑ false → x = false.
Proof.
destruct x; inversion 1; eauto.
Qed.
Lemma poLe_true x
: true ⊑ x → x = true.
Proof.
destruct x; inversion 1; eauto.
Qed.
Smpl Add match goal with
| [ H : _ ⊑ false |- _ ] ⇒ eapply poLe_false in H; try subst
| [ H : false ⊑ _ |- _ ] ⇒ eapply poLe_false in H; try subst
end : inv_trivial.
Lemma poLe_sig_struct D `{PartialOrder D} (P: D → Prop) (x x':D) pf pf'
: x ⊑ x'
→ @poLe _ (@PartialOrder_sig D _ P) (exist P x pf) (exist P x' pf').
Proof.
intros. simpl. eapply H0.
Qed.
Lemma poLe_sig_struct' D `{PartialOrder D} (P: D → Prop) (x x':{x : D | P x})
: proj1_sig x ⊑ proj1_sig x'
→ x ⊑ x'.
Proof.
intros. simpl. eapply H0.
Qed.
Lemma poEq_sig_struct D `{PartialOrder D} (P: D → Prop) (x x':D) pf pf'
: x ≣ x'
→ @poEq _ (@PartialOrder_sig D _ P) (exist P x pf) (exist P x' pf').
Proof.
intros. simpl. eapply H0.
Qed.
Lemma poEq_sig_struct' D `{PartialOrder D} (P: D → Prop) (x x':D) pf pf'
: @poEq _ (@PartialOrder_sig D _ P) (exist P x pf) (exist P x' pf')
→ x ≣ x'.
Proof.
intros. eapply H0.
Qed.
Lemma poLe_sig_struct'' D `{PartialOrder D} (P: D → Prop) (x x':D) pf pf'
: @poLe _ (@PartialOrder_sig D _ P) (exist P x pf) (exist P x' pf')
→ x ⊑ x'.
Proof.
intros. eapply H0.
Qed.
Lemma poLe_sig_destruct D `{PartialOrder D} (P: D → Prop) (x x':{x : D | P x})
: x ⊑ x'
→ proj1_sig x ⊑ proj1_sig x'.
Proof.
intros. eapply H0.
Qed.
Lemma poEq_sig_destruct D `{PartialOrder D} (P: D → Prop) (x x':{x : D | P x})
: x ≣ x'
→ proj1_sig x ≣ proj1_sig x'.
Proof.
intros. eapply H0.
Qed.
Hint Resolve poLe_sig_destruct poEq_sig_destruct.
Lemma poLe_list_struct A `{PartialOrder A} (a1 a2:A) b1 b2
: poLe a1 a2 → poLe b1 b2 → poLe (a1::b1) (a2::b2).
intros; econstructor; eauto.
Qed.
Lemma poEq_list_struct A `{PartialOrder A} (a1 a2:A) b1 b2
: poEq a1 a2 → poEq b1 b2 → poEq (a1::b1) (a2::b2).
intros; econstructor; eauto.
Qed.
Hint Resolve poLe_list_struct poEq_list_struct.
Lemma poLe_map D `{PartialOrder D} D' `{PartialOrder D'} (f g:D → D') (L L':list D)
(LEf:∀ a b, poLe a b → poLe (f a) (g b))
(LE: poLe L L')
: poLe (f ⊝ L) (g ⊝ L').
Proof.
general induction LE; simpl; eauto.
Qed.
Lemma poLe_map_nd D D' `{PartialOrder D'} (f g:D → D') (L:list D)
(LEf:∀ a, poLe (f a) (g a))
: poLe (f ⊝ L) (g ⊝ L).
Proof.
general induction L; simpl; eauto.
Qed.
Lemma poEq_map D `{PartialOrder D} D' `{PartialOrder D'} (f g:D → D') (L L':list D)
(LEf:∀ a b, poEq a b → poEq (f a) (g b))
(LE: poEq L L')
: poEq (f ⊝ L) (g ⊝ L').
Proof.
general induction LE; simpl; eauto.
Qed.
Lemma poEq_map_nd D D' `{PartialOrder D'} (f g:D → D') (L:list D)
(LEf:∀ a, poEq (f a) (g a))
: poEq (f ⊝ L) (g ⊝ L).
Proof.
general induction L; simpl; eauto.
Qed.
Instance poLe_poLe_impl (Dom : Type) (H : PartialOrder Dom)
: Proper (poLe --> poLe ==> impl) poLe.
Proof.
unfold Proper, respectful , flip, impl; intros.
eauto.
Qed.
Instance poLe_poLe_flip_impl (Dom : Type) (H : PartialOrder Dom)
: Proper (poLe ==> flip poLe ==> flip impl) poLe.
Proof.
unfold Proper, respectful, flip, impl; intros ? ? A ? ? B C.
eauto.
Qed.
Lemma poLe_app X `{PartialOrder X} (L1 L2 : 〔X〕) (L1' L2' : 〔X〕)
: poLe L1 L1' → poLe L2 L2' → poLe (L1 ++ L2) (L1' ++ L2').
Proof.
intros. eapply PIR2_app; eauto.
Qed.
Lemma poEq_app X `{PartialOrder X} (L1 L2 : 〔X〕) (L1' L2' : 〔X〕)
: poEq L1 L1' → poEq L2 L2' → poEq (L1 ++ L2) (L1' ++ L2').
Proof.
intros. eapply PIR2_app; eauto.
Qed.
Hint Resolve poLe_app poEq_app.
Lemma poLe_app_proper X `{PartialOrder X}
: Proper (poLe ==> poLe ==> poLe) (@List.app X).
Proof.
unfold Proper, respectful; intros; eauto.
Qed.
Lemma poLe_app_proper_funny X `{PartialOrder X} L
: Proper (flip poLe ==> flip poLe) (@List.app X L).
Proof.
unfold Proper, respectful, flip; intros; eauto.
Qed.
Lemma poLe_app_proper' X `{PartialOrder X}
: Proper (flip poLe ==> flip poLe ==> flip poLe) (@List.app X).
Proof.
unfold Proper, respectful, flip; intros; eauto.
Qed.
Lemma poLe_app_proper_poEq X `{PartialOrder X}
: Proper (poEq ==> poEq ==> poEq) (@List.app X).
Proof.
unfold Proper, respectful; intros; eauto.
Qed.
Instance orb_poEq_proper : Proper (poEq ==> poEq ==> poEq) orb.
Proof.
intuition.
Qed.
Hint Resolve orb_poEq_proper.
Instance poLe_length_proper X `{PartialOrder X}
: Proper (poLe ==> eq) (@length X).
Proof.
unfold Proper, respectful; intros.
hnf in H0. eapply PIR2_length in H0. eauto.
Qed.
Instance poEq_length_proper X `{PartialOrder X}
: Proper (poEq ==> eq) (@length X).
Proof.
unfold Proper, respectful; intros.
hnf in H0. eapply PIR2_length in H0. eauto.
Qed.
Instance poLt_irr X `{PartialOrder X} : Irreflexive poLt.
Proof.
hnf. unfold complement. intros ? [? ?]. eauto.
Qed.
Instance poLt_trans X `{PartialOrder X} : Transitive poLt.
Proof.
hnf; intros.
unfold poLt in ×.
destruct H0, H1; eauto.
Qed.
(* Explicit Instance *)
Lemma ot_po X `{OrderedType X} : PartialOrder X.
eapply Build_PartialOrder with
(poLe := _le) (poEq := _eq); eauto using OT_le_refl with typeclass_instances.
Defined.
Lemma po_strict_order X `{PartialOrder X} : StrictOrder poLt.
econstructor; eauto with typeclass_instances.
Qed.