------------------------------------------------------------------------ -- The Agda standard library -- -- Some properties imply others ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Relation.Binary.Consequences where open import Data.Product.Base using (_,_) open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′) open import Function.Base using (_∘_; _∘₂_; _$_; flip) open import Level using (Level) open import Relation.Binary.Core open import Relation.Binary.Definitions open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Nullary.Decidable.Core using (yes; no; recompute; map′; dec⇒maybe) open import Relation.Unary using (∁; Pred) private variable a ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ p : Level A B C : Set a ------------------------------------------------------------------------ -- Substitutive properties module _ {_∼_ : Rel A ℓ} (R : Rel A p) where subst⇒respˡ : Substitutive _∼_ p → R Respectsˡ _∼_ subst⇒respˡ subst {y} x′∼x Px′y = subst (flip R y) x′∼x Px′y subst⇒respʳ : Substitutive _∼_ p → R Respectsʳ _∼_ subst⇒respʳ subst {x} y′∼y Pxy′ = subst (R x) y′∼y Pxy′ subst⇒resp₂ : Substitutive _∼_ p → R Respects₂ _∼_ subst⇒resp₂ subst = subst⇒respʳ subst , subst⇒respˡ subst module _ {_∼_ : Rel A ℓ} {P : Pred A p} where resp⇒¬-resp : Symmetric _∼_ → P Respects _∼_ → (∁ P) Respects _∼_ resp⇒¬-resp sym resp x∼y ¬Px Py = ¬Px (resp (sym x∼y) Py) ------------------------------------------------------------------------ -- Proofs for negation module _ {_∼_ : Rel A ℓ} where sym⇒¬-sym : Symmetric _∼_ → Symmetric (¬_ ∘₂ _∼_) sym⇒¬-sym sym≁ x≁y y∼x = x≁y (sym≁ y∼x) -- N.B. the implicit arguments to Cotransitive are permuted w.r.t. -- those of Transitive cotrans⇒¬-trans : Cotransitive _∼_ → Transitive (¬_ ∘₂ _∼_) cotrans⇒¬-trans cotrans {j = z} x≁z z≁y x∼y = [ x≁z , z≁y ]′ (cotrans x∼y z) ------------------------------------------------------------------------ -- Proofs for Irreflexive relations module _ {_≈_ : Rel A ℓ₁} {_∼_ : Rel A ℓ₂} where irrefl⇒¬-refl : Reflexive _≈_ → Irreflexive _≈_ _∼_ → Reflexive (¬_ ∘₂ _∼_) irrefl⇒¬-refl re irr = irr re ------------------------------------------------------------------------ -- Proofs for non-strict orders module _ {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} where total⇒refl : _≤_ Respects₂ _≈_ → Symmetric _≈_ → Total _≤_ → _≈_ ⇒ _≤_ total⇒refl (respʳ , respˡ) sym total {x} {y} x≈y with total x y ... | inj₁ x∼y = x∼y ... | inj₂ y∼x = respʳ x≈y (respˡ (sym x≈y) y∼x) total∧dec⇒dec : _≈_ ⇒ _≤_ → Antisymmetric _≈_ _≤_ → Total _≤_ → Decidable _≈_ → Decidable _≤_ total∧dec⇒dec refl antisym total _≟_ x y with total x y ... | inj₁ x≤y = yes x≤y ... | inj₂ y≤x = map′ refl (flip antisym y≤x) (x ≟ y) module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {≤₁ : Rel A ℓ₃} {≤₂ : Rel B ℓ₄} where mono⇒cong : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ → ∀ {f} → Monotonic₁ ≤₁ ≤₂ f → Monotonic₁ ≈₁ ≈₂ f mono⇒cong sym reflexive antisym mono x≈y = antisym (mono (reflexive x≈y)) (mono (reflexive (sym x≈y))) antimono⇒cong : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ → ∀ {f} → f Preserves ≤₁ ⟶ (flip ≤₂) → Monotonic₁ ≈₁ ≈₂ f antimono⇒cong sym reflexive antisym antimono p≈q = antisym (antimono (reflexive (sym p≈q))) (antimono (reflexive p≈q)) mono₂⇒cong₂ : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ → ∀ {f} → Monotonic₂ ≤₁ ≤₁ ≤₂ f → Monotonic₂ ≈₁ ≈₁ ≈₂ f mono₂⇒cong₂ sym reflexive antisym mono x≈y u≈v = antisym (mono (reflexive x≈y) (reflexive u≈v)) (mono (reflexive (sym x≈y)) (reflexive (sym u≈v))) module _ (≤₁ : Rel A ℓ₁) (≤₂ : Rel B ℓ₂) (≤₃ : Rel C ℓ₂) where mono₂⇒monoˡ : ∀ {f} → Reflexive ≤₁ → Monotonic₂ ≤₁ ≤₂ ≤₃ f → LeftMonotonic ≤₂ ≤₃ f mono₂⇒monoˡ refl mono x = mono (refl {x = x}) mono₂⇒monoʳ : ∀ {f} → Reflexive ≤₂ → Monotonic₂ ≤₁ ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f mono₂⇒monoʳ refl mono y = flip mono (refl {x = y}) monoˡ∧monoʳ⇒mono₂ : ∀ {f} → Transitive ≤₃ → LeftMonotonic ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f → Monotonic₂ ≤₁ ≤₂ ≤₃ f monoˡ∧monoʳ⇒mono₂ trans monoˡ monoʳ x≤₁y u≤₂v = trans (monoˡ _ u≤₂v) (monoʳ _ x≤₁y) ------------------------------------------------------------------------ -- Proofs for strict orders module _ {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where trans∧irr⇒asym : Reflexive _≈_ → Transitive _<_ → Irreflexive _≈_ _<_ → Asymmetric _<_ trans∧irr⇒asym refl trans irrefl x<y y<x = irrefl refl (trans x<y y<x) irr∧antisym⇒asym : Irreflexive _≈_ _<_ → Antisymmetric _≈_ _<_ → Asymmetric _<_ irr∧antisym⇒asym irrefl antisym x<y y<x = irrefl (antisym x<y y<x) x<y asym⇒antisym : Asymmetric _<_ → Antisymmetric _≈_ _<_ asym⇒antisym asym x<y y<x = contradiction y<x (asym x<y) asym⇒irr : _<_ Respects₂ _≈_ → Symmetric _≈_ → Asymmetric _<_ → Irreflexive _≈_ _<_ asym⇒irr (respʳ , respˡ) sym asym {x} {y} x≈y x<y = asym x<y (respʳ (sym x≈y) (respˡ x≈y x<y)) tri⇒asym : Trichotomous _≈_ _<_ → Asymmetric _<_ tri⇒asym tri {x} {y} x<y x>y with tri x y ... | tri< _ _ x≯y = x≯y x>y ... | tri≈ _ _ x≯y = x≯y x>y ... | tri> x≮y _ _ = x≮y x<y tri⇒irr : Trichotomous _≈_ _<_ → Irreflexive _≈_ _<_ tri⇒irr compare {x} {y} x≈y x<y with compare x y ... | tri< _ x≉y y≮x = x≉y x≈y ... | tri> x≮y x≉y y<x = x≉y x≈y ... | tri≈ x≮y _ y≮x = x≮y x<y tri⇒dec≈ : Trichotomous _≈_ _<_ → Decidable _≈_ tri⇒dec≈ compare x y with compare x y ... | tri< _ x≉y _ = no x≉y ... | tri≈ _ x≈y _ = yes x≈y ... | tri> _ x≉y _ = no x≉y tri⇒dec< : Trichotomous _≈_ _<_ → Decidable _<_ tri⇒dec< compare x y with compare x y ... | tri< x<y _ _ = yes x<y ... | tri≈ x≮y _ _ = no x≮y ... | tri> x≮y _ _ = no x≮y trans∧tri⇒respʳ : Symmetric _≈_ → Transitive _≈_ → Transitive _<_ → Trichotomous _≈_ _<_ → _<_ Respectsʳ _≈_ trans∧tri⇒respʳ sym ≈-tr <-tr tri {x} {y} {z} y≈z x<y with tri x z ... | tri< x<z _ _ = x<z ... | tri≈ _ x≈z _ = contradiction x<y (tri⇒irr tri (≈-tr x≈z (sym y≈z))) ... | tri> _ _ z<x = contradiction (<-tr z<x x<y) (tri⇒irr tri (sym y≈z)) trans∧tri⇒respˡ : Transitive _≈_ → Transitive _<_ → Trichotomous _≈_ _<_ → _<_ Respectsˡ _≈_ trans∧tri⇒respˡ ≈-tr <-tr tri {z} {_} {y} x≈y x<z with tri y z ... | tri< y<z _ _ = y<z ... | tri≈ _ y≈z _ = contradiction x<z (tri⇒irr tri (≈-tr x≈y y≈z)) ... | tri> _ _ z<y = contradiction (<-tr x<z z<y) (tri⇒irr tri x≈y) trans∧tri⇒resp : Symmetric _≈_ → Transitive _≈_ → Transitive _<_ → Trichotomous _≈_ _<_ → _<_ Respects₂ _≈_ trans∧tri⇒resp sym ≈-tr <-tr tri = trans∧tri⇒respʳ sym ≈-tr <-tr tri , trans∧tri⇒respˡ ≈-tr <-tr tri ------------------------------------------------------------------------ -- Without Loss of Generality module _ {_R_ : Rel A ℓ₁} {Q : Rel A ℓ₂} where wlog : Total _R_ → Symmetric Q → (∀ a b → a R b → Q a b) → ∀ a b → Q a b wlog r-total q-sym prf a b with r-total a b ... | inj₁ aRb = prf a b aRb ... | inj₂ bRa = q-sym (prf b a bRa) ------------------------------------------------------------------------ -- Other proofs module _ {R : REL A B p} where dec⇒weaklyDec : Decidable R → WeaklyDecidable R dec⇒weaklyDec dec x y = dec⇒maybe (dec x y) dec⇒recomputable : Decidable R → Recomputable R dec⇒recomputable dec {a} {b} = recompute $ dec a b module _ {R : REL A B ℓ₁} {S : REL A B ℓ₂} where map-NonEmpty : R ⇒ S → NonEmpty R → NonEmpty S map-NonEmpty f x = nonEmpty (f (NonEmpty.proof x)) module _ {R : REL A B ℓ₁} {S : REL B A ℓ₂} where flip-Connex : Connex R S → Connex S R flip-Connex f x y = Sum.swap (f y x) ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ -- Please use the new names as continuing support for the old names is -- not guaranteed. -- Version 1.6 subst⟶respˡ = subst⇒respˡ {-# WARNING_ON_USAGE subst⟶respˡ "Warning: subst⟶respˡ was deprecated in v1.6. Please use subst⇒respˡ instead." #-} subst⟶respʳ = subst⇒respʳ {-# WARNING_ON_USAGE subst⟶respʳ "Warning: subst⟶respʳ was deprecated in v1.6. Please use subst⇒respʳ instead." #-} subst⟶resp₂ = subst⇒resp₂ {-# WARNING_ON_USAGE subst⟶resp₂ "Warning: subst⟶resp₂ was deprecated in v1.6. Please use subst⇒resp₂ instead." #-} P-resp⟶¬P-resp = resp⇒¬-resp {-# WARNING_ON_USAGE P-resp⟶¬P-resp "Warning: P-resp⟶¬P-resp was deprecated in v1.6. Please use resp⇒¬-resp instead." #-} total⟶refl = total⇒refl {-# WARNING_ON_USAGE total⟶refl "Warning: total⟶refl was deprecated in v1.6. Please use total⇒refl instead." #-} total+dec⟶dec = total∧dec⇒dec {-# WARNING_ON_USAGE total+dec⟶dec "Warning: total+dec⟶dec was deprecated in v1.6. Please use total∧dec⇒dec instead." #-} trans∧irr⟶asym = trans∧irr⇒asym {-# WARNING_ON_USAGE trans∧irr⟶asym "Warning: trans∧irr⟶asym was deprecated in v1.6. Please use trans∧irr⇒asym instead." #-} irr∧antisym⟶asym = irr∧antisym⇒asym {-# WARNING_ON_USAGE irr∧antisym⟶asym "Warning: irr∧antisym⟶asym was deprecated in v1.6. Please use irr∧antisym⇒asym instead." #-} asym⟶antisym = asym⇒antisym {-# WARNING_ON_USAGE asym⟶antisym "Warning: asym⟶antisym was deprecated in v1.6. Please use asym⇒antisym instead." #-} asym⟶irr = asym⇒irr {-# WARNING_ON_USAGE asym⟶irr "Warning: asym⟶irr was deprecated in v1.6. Please use asym⇒irr instead." #-} tri⟶asym = tri⇒asym {-# WARNING_ON_USAGE tri⟶asym "Warning: tri⟶asym was deprecated in v1.6. Please use tri⇒asym instead." #-} tri⟶irr = tri⇒irr {-# WARNING_ON_USAGE tri⟶irr "Warning: tri⟶irr was deprecated in v1.6. Please use tri⇒irr instead." #-} tri⟶dec≈ = tri⇒dec≈ {-# WARNING_ON_USAGE tri⟶dec≈ "Warning: tri⟶dec≈ was deprecated in v1.6. Please use tri⇒dec≈ instead." #-} tri⟶dec< = tri⇒dec< {-# WARNING_ON_USAGE tri⟶dec< "Warning: tri⟶dec< was deprecated in v1.6. Please use tri⇒dec< instead." #-} trans∧tri⟶respʳ≈ = trans∧tri⇒respʳ {-# WARNING_ON_USAGE trans∧tri⟶respʳ≈ "Warning: trans∧tri⟶respʳ≈ was deprecated in v1.6. Please use trans∧tri⇒respʳ instead." #-} trans∧tri⟶respˡ≈ = trans∧tri⇒respˡ {-# WARNING_ON_USAGE trans∧tri⟶respˡ≈ "Warning: trans∧tri⟶respˡ≈ was deprecated in v1.6. Please use trans∧tri⇒respˡ instead." #-} trans∧tri⟶resp≈ = trans∧tri⇒resp {-# WARNING_ON_USAGE trans∧tri⟶resp≈ "Warning: trans∧tri⟶resp≈ was deprecated in v1.6. Please use trans∧tri⇒resp instead." #-} dec⟶weaklyDec = dec⇒weaklyDec {-# WARNING_ON_USAGE dec⟶weaklyDec "Warning: dec⟶weaklyDec was deprecated in v1.6. Please use dec⇒weaklyDec instead." #-} dec⟶recomputable = dec⇒recomputable {-# WARNING_ON_USAGE dec⟶recomputable "Warning: dec⟶recomputable was deprecated in v1.6. Please use dec⇒recomputable instead." #-}