diff options
Diffstat (limited to 'src/Relation')
| -rw-r--r-- | src/Relation/Binary/List/Pointwise.agda | 52 | ||||
| -rw-r--r-- | src/Relation/Binary/Product/StrictLex.agda | 9 | ||||
| -rw-r--r-- | src/Relation/Binary/Reflection.agda | 28 | ||||
| -rw-r--r-- | src/Relation/Binary/Sigma/Pointwise.agda | 168 | ||||
| -rw-r--r-- | src/Relation/Binary/Vec/Pointwise.agda | 204 | ||||
| -rw-r--r-- | src/Relation/Nullary/Negation.agda | 2 |
6 files changed, 395 insertions, 68 deletions
diff --git a/src/Relation/Binary/List/Pointwise.agda b/src/Relation/Binary/List/Pointwise.agda index d0314f0..04a4fe0 100644 --- a/src/Relation/Binary/List/Pointwise.agda +++ b/src/Relation/Binary/List/Pointwise.agda @@ -2,6 +2,8 @@ -- Pointwise lifting of relations to lists ------------------------------------------------------------------------ +{-# OPTIONS --universe-polymorphism #-} + module Relation.Binary.List.Pointwise where open import Function @@ -13,47 +15,54 @@ open import Relation.Binary renaming (Rel to Rel₂) open import Relation.Binary.PropositionalEquality as PropEq using (_≡_) private - module Dummy {A : Set} where + module Dummy {a} {A : Set a} where infixr 5 _∷_ - data Rel (_∼_ : Rel₂ A zero) : List A → List A → Set where + data Rel {ℓ} (_∼_ : Rel₂ A ℓ) : List A → List A → Set (ℓ ⊔ a) where [] : Rel _∼_ [] [] _∷_ : ∀ {x xs y ys} (x∼y : x ∼ y) (xs∼ys : Rel _∼_ xs ys) → Rel _∼_ (x ∷ xs) (y ∷ ys) - head : ∀ {_∼_ x y xs ys} → Rel _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y + head : ∀ {ℓ} {_∼_ : Rel₂ A ℓ} {x y xs ys} → + Rel _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y head (x∼y ∷ xs∼ys) = x∼y - tail : ∀ {_∼_ x y xs ys} → Rel _∼_ (x ∷ xs) (y ∷ ys) → Rel _∼_ xs ys + tail : ∀ {ℓ} {_∼_ : Rel₂ A ℓ} {x y xs ys} → + Rel _∼_ (x ∷ xs) (y ∷ ys) → Rel _∼_ xs ys tail (x∼y ∷ xs∼ys) = xs∼ys - reflexive : ∀ {_≈_ _∼_} → _≈_ ⇒ _∼_ → Rel _≈_ ⇒ Rel _∼_ + reflexive : ∀ {ℓ₁ ℓ₂} {_≈_ : Rel₂ A ℓ₁} {_∼_ : Rel₂ A ℓ₂} → + _≈_ ⇒ _∼_ → Rel _≈_ ⇒ Rel _∼_ reflexive ≈⇒∼ [] = [] reflexive ≈⇒∼ (x≈y ∷ xs≈ys) = ≈⇒∼ x≈y ∷ reflexive ≈⇒∼ xs≈ys - refl : ∀ {_∼_} → Reflexive _∼_ → Reflexive (Rel _∼_) + refl : ∀ {ℓ} {_∼_ : Rel₂ A ℓ} → + Reflexive _∼_ → Reflexive (Rel _∼_) refl rfl {[]} = [] refl rfl {x ∷ xs} = rfl ∷ refl rfl - symmetric : ∀ {_∼_} → Symmetric _∼_ → Symmetric (Rel _∼_) + symmetric : ∀ {ℓ} {_∼_ : Rel₂ A ℓ} → + Symmetric _∼_ → Symmetric (Rel _∼_) symmetric sym [] = [] symmetric sym (x∼y ∷ xs∼ys) = sym x∼y ∷ symmetric sym xs∼ys - transitive : ∀ {_∼_} → Transitive _∼_ → Transitive (Rel _∼_) + transitive : ∀ {ℓ} {_∼_ : Rel₂ A ℓ} → + Transitive _∼_ → Transitive (Rel _∼_) transitive trans [] [] = [] transitive trans (x∼y ∷ xs∼ys) (y∼z ∷ ys∼zs) = trans x∼y y∼z ∷ transitive trans xs∼ys ys∼zs - antisymmetric : ∀ {_≈_ _≤_} → Antisymmetric _≈_ _≤_ → + antisymmetric : ∀ {ℓ₁ ℓ₂} {_≈_ : Rel₂ A ℓ₁} {_≤_ : Rel₂ A ℓ₂} → + Antisymmetric _≈_ _≤_ → Antisymmetric (Rel _≈_) (Rel _≤_) antisymmetric antisym [] [] = [] antisymmetric antisym (x∼y ∷ xs∼ys) (y∼x ∷ ys∼xs) = antisym x∼y y∼x ∷ antisymmetric antisym xs∼ys ys∼xs - respects₂ : ∀ {_≈_ _∼_} → + respects₂ : ∀ {ℓ₁ ℓ₂} {_≈_ : Rel₂ A ℓ₁} {_∼_ : Rel₂ A ℓ₂} → _∼_ Respects₂ _≈_ → (Rel _∼_) Respects₂ (Rel _≈_) - respects₂ {_≈_} {_∼_} resp = + respects₂ {_} {_} {_≈_} {_∼_} resp = (λ {xs} {ys} {zs} → resp¹ {xs} {ys} {zs}) , (λ {xs} {ys} {zs} → resp² {xs} {ys} {zs}) where @@ -67,7 +76,8 @@ private resp² (x≈y ∷ xs≈ys) (x∼z ∷ xs∼zs) = proj₂ resp x≈y x∼z ∷ resp² xs≈ys xs∼zs - decidable : ∀ {_∼_} → Decidable _∼_ → Decidable (Rel _∼_) + decidable : ∀ {ℓ} {_∼_ : Rel₂ A ℓ} → + Decidable _∼_ → Decidable (Rel _∼_) decidable dec [] [] = yes [] decidable dec [] (y ∷ ys) = no (λ ()) decidable dec (x ∷ xs) [] = no (λ ()) @@ -77,14 +87,15 @@ private ... | no ¬xs∼ys = no (¬xs∼ys ∘ tail) ... | yes xs∼ys = yes (x∼y ∷ xs∼ys) - isEquivalence : ∀ {_≈_} → IsEquivalence _≈_ → IsEquivalence (Rel _≈_) + isEquivalence : ∀ {ℓ} {_≈_ : Rel₂ A ℓ} → + IsEquivalence _≈_ → IsEquivalence (Rel _≈_) isEquivalence eq = record { refl = refl Eq.refl ; sym = symmetric Eq.sym ; trans = transitive Eq.trans } where module Eq = IsEquivalence eq - isPreorder : ∀ {_≈_ _∼_} → + isPreorder : ∀ {ℓ₁ ℓ₂} {_≈_ : Rel₂ A ℓ₁} {_∼_ : Rel₂ A ℓ₂} → IsPreorder _≈_ _∼_ → IsPreorder (Rel _≈_) (Rel _∼_) isPreorder pre = record { isEquivalence = isEquivalence Pre.isEquivalence @@ -92,14 +103,15 @@ private ; trans = transitive Pre.trans } where module Pre = IsPreorder pre - isDecEquivalence : ∀ {_≈_} → IsDecEquivalence _≈_ → + isDecEquivalence : ∀ {ℓ} {_≈_ : Rel₂ A ℓ} → IsDecEquivalence _≈_ → IsDecEquivalence (Rel _≈_) isDecEquivalence eq = record { isEquivalence = isEquivalence Dec.isEquivalence ; _≟_ = decidable Dec._≟_ } where module Dec = IsDecEquivalence eq - isPartialOrder : ∀ {_≈_ _≤_} → IsPartialOrder _≈_ _≤_ → + isPartialOrder : ∀ {ℓ₁ ℓ₂} {_≈_ : Rel₂ A ℓ₁} {_≤_ : Rel₂ A ℓ₂} → + IsPartialOrder _≈_ _≤_ → IsPartialOrder (Rel _≈_) (Rel _≤_) isPartialOrder po = record { isPreorder = isPreorder PO.isPreorder @@ -118,22 +130,22 @@ private open Dummy public -preorder : Preorder _ _ _ → Preorder _ _ _ +preorder : ∀ {p₁ p₂ p₃} → Preorder p₁ p₂ p₃ → Preorder _ _ _ preorder p = record { isPreorder = isPreorder (Preorder.isPreorder p) } -setoid : Setoid _ _ → Setoid _ _ +setoid : ∀ {c ℓ} → Setoid c ℓ → Setoid _ _ setoid s = record { isEquivalence = isEquivalence (Setoid.isEquivalence s) } -decSetoid : DecSetoid _ _ → DecSetoid _ _ +decSetoid : ∀ {c ℓ} → DecSetoid c ℓ → DecSetoid _ _ decSetoid d = record { isDecEquivalence = isDecEquivalence (DecSetoid.isDecEquivalence d) } -poset : Poset _ _ _ → Poset _ _ _ +poset : ∀ {c ℓ₁ ℓ₂} → Poset c ℓ₁ ℓ₂ → Poset _ _ _ poset p = record { isPartialOrder = isPartialOrder (Poset.isPartialOrder p) } diff --git a/src/Relation/Binary/Product/StrictLex.agda b/src/Relation/Binary/Product/StrictLex.agda index 3a3542b..42755b6 100644 --- a/src/Relation/Binary/Product/StrictLex.agda +++ b/src/Relation/Binary/Product/StrictLex.agda @@ -106,7 +106,7 @@ private ×-≈-respects₂ : ∀ {_≈₁_ _<₁_} → IsEquivalence _≈₁_ → _<₁_ Respects₂ _≈₁_ → - ∀ {_≈₂_ _<₂_} → _<₂_ Respects₂ _≈₂_ → + {_≈₂_ _<₂_ : Rel A₂ ℓ₂} → _<₂_ Respects₂ _≈₂_ → (×-Lex _≈₁_ _<₁_ _<₂_) Respects₂ (_≈₁_ ×-Rel _≈₂_) ×-≈-respects₂ {_≈₁_ = _≈₁_} {_<₁_ = _<₁_} eq₁ resp₁ {_≈₂_ = _≈₂_} {_<₂_ = _<₂_} resp₂ = @@ -149,9 +149,10 @@ private ... | inj₁ x₁<y₁ = inj₁ (inj₁ x₁<y₁) ... | inj₂ x₁>y₁ = inj₂ (inj₁ x₁>y₁) - ×-compare : ∀ {_≈₁_ _<₁_} → Symmetric _≈₁_ → Trichotomous _≈₁_ _<₁_ → - ∀ {_≈₂_ _<₂_} → Trichotomous _≈₂_ _<₂_ → - Trichotomous (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_) + ×-compare : + {_≈₁_ _<₁_ : Rel A₁ ℓ₁} → Symmetric _≈₁_ → Trichotomous _≈₁_ _<₁_ → + {_≈₂_ _<₂_ : Rel A₂ ℓ₂} → Trichotomous _≈₂_ _<₂_ → + Trichotomous (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_) ×-compare {_≈₁_} {_<₁_} sym₁ compare₁ {_≈₂_} {_<₂_} compare₂ = cmp where cmp″ : ∀ {x₁ y₁ x₂ y₂} → diff --git a/src/Relation/Binary/Reflection.agda b/src/Relation/Binary/Reflection.agda index 149f897..5f54c6a 100644 --- a/src/Relation/Binary/Reflection.agda +++ b/src/Relation/Binary/Reflection.agda @@ -6,11 +6,14 @@ {-# OPTIONS --universe-polymorphism #-} open import Data.Fin -open import Function open import Data.Nat open import Data.Vec as Vec +open import Function +open import Function.Equality using (_⟨$⟩_) +open import Function.Equivalence using (module Equivalent) open import Level open import Relation.Binary +import Relation.Binary.PropositionalEquality as P -- Think of the parameters as follows: -- @@ -72,13 +75,26 @@ solve : ∀ n (f : N-ary n (Expr n) (Expr n × Expr n)) → Eqʰ n _≈_ (curryⁿ ⟦ proj₁ (close n f) ⇓⟧) (curryⁿ ⟦ proj₂ (close n f) ⇓⟧) → Eq n _≈_ (curryⁿ ⟦ proj₁ (close n f) ⟧) (curryⁿ ⟦ proj₂ (close n f) ⟧) solve n f hyp = - curryⁿ-cong ⟦ proj₁ (close n f) ⟧ ⟦ proj₂ (close n f) ⟧ + curryⁿ-cong _≈_ ⟦ proj₁ (close n f) ⟧ ⟦ proj₂ (close n f) ⟧ (λ ρ → prove ρ (proj₁ (close n f)) (proj₂ (close n f)) - (curryⁿ-cong⁻¹ ⟦ proj₁ (close n f) ⇓⟧ ⟦ proj₂ (close n f) ⇓⟧ - (Eqʰ-to-Eq n hyp) ρ)) + (curryⁿ-cong⁻¹ _≈_ + ⟦ proj₁ (close n f) ⇓⟧ ⟦ proj₂ (close n f) ⇓⟧ + (Eqʰ-to-Eq n _≈_ hyp) ρ)) + +-- A variant of solve which does not require that the normal form +-- equality is proved for an arbitrary environment. + +solve₁ : ∀ n (f : N-ary n (Expr n) (Expr n × Expr n)) → + ∀ⁿ n (curryⁿ λ ρ → + ⟦ proj₁ (close n f) ⇓⟧ ρ ≈ ⟦ proj₂ (close n f) ⇓⟧ ρ → + ⟦ proj₁ (close n f) ⟧ ρ ≈ ⟦ proj₂ (close n f) ⟧ ρ) +solve₁ n f = + Equivalent.from (uncurry-∀ⁿ n) ⟨$⟩ λ ρ → + P.subst id (P.sym (left-inverse (λ _ → _ ≈ _ → _ ≈ _) ρ)) + (prove ρ (proj₁ (close n f)) (proj₂ (close n f))) --- A variant of _,_ which is intended to make uses of solve look a --- bit nicer. +-- A variant of _,_ which is intended to make uses of solve and solve₁ +-- look a bit nicer. infix 4 _⊜_ diff --git a/src/Relation/Binary/Sigma/Pointwise.agda b/src/Relation/Binary/Sigma/Pointwise.agda index dfac94e..dadec84 100644 --- a/src/Relation/Binary/Sigma/Pointwise.agda +++ b/src/Relation/Binary/Sigma/Pointwise.agda @@ -9,7 +9,8 @@ module Relation.Binary.Sigma.Pointwise where open import Data.Product as Prod open import Level open import Function -import Function.Equality as F +open import Function.Equality as F using (_⟶_; _⟨$⟩_) + renaming (_∘_ to _⊚_) open import Function.Equivalence as Eq using (Equivalent; _⇔_; module Equivalent) renaming (_∘_ to _⟨∘⟩_) @@ -18,6 +19,7 @@ open import Function.Inverse as Inv renaming (_∘_ to _⟪∘⟫_) open import Function.LeftInverse using (_LeftInverseOf_; _RightInverseOf_) +open import Function.Surjection using (_↠_; module Surjection) import Relation.Binary as B open import Relation.Binary.Indexed as I using (_at_) import Relation.Binary.HeterogeneousEquality as H @@ -110,45 +112,101 @@ Rel⇿≡ {a} {b} {A} {B} = record -- Equivalences and inverses are also preserved equivalent : - ∀ {i} {I : Set i} - {f₁ f₂ t₁ t₂} {From : I.Setoid I f₁ f₂} {To : I.Setoid I t₁ t₂} → - (∀ {i} → Equivalent (From at i) (To at i)) → - Equivalent (setoid (P.setoid I) From) (setoid (P.setoid I) To) -equivalent {I = I} {From = F} {T} F⇔T = record + ∀ {a₁ a₂ b₁ b₁′ b₂ b₂′} + {A₁ : Set a₁} {A₂ : Set a₂} + {B₁ : I.Setoid A₁ b₁ b₁′} {B₂ : I.Setoid A₂ b₂ b₂′} + (A₁⇔A₂ : A₁ ⇔ A₂) → + (∀ {x} → B₁ at x ⟶ B₂ at (Equivalent.to A₁⇔A₂ ⟨$⟩ x)) → + (∀ {y} → B₂ at y ⟶ B₁ at (Equivalent.from A₁⇔A₂ ⟨$⟩ y)) → + Equivalent (setoid (P.setoid A₁) B₁) (setoid (P.setoid A₂) B₂) +equivalent {A₁ = A₁} {A₂} {B₁} {B₂} A₁⇔A₂ B-to B-from = record { to = record { _⟨$⟩_ = to; cong = to-cong } ; from = record { _⟨$⟩_ = from; cong = from-cong } } where - open B.Setoid (setoid (P.setoid I) F) using () renaming (_≈_ to _≈F_) - open B.Setoid (setoid (P.setoid I) T) using () renaming (_≈_ to _≈T_) + open B.Setoid (setoid (P.setoid A₁) B₁) + using () renaming (_≈_ to _≈₁_) + open B.Setoid (setoid (P.setoid A₂) B₂) + using () renaming (_≈_ to _≈₂_) open B using (_=[_]⇒_) - to = Prod.map id (F._⟨$⟩_ (Equivalent.to F⇔T)) + to = Prod.map (_⟨$⟩_ (Equivalent.to A₁⇔A₂)) (_⟨$⟩_ B-to) - to-cong : _≈F_ =[ to ]⇒ _≈T_ - to-cong (P.refl , ∼) = (P.refl , F.cong (Equivalent.to F⇔T) ∼) + to-cong : _≈₁_ =[ to ]⇒ _≈₂_ + to-cong (P.refl , ∼) = (P.refl , F.cong B-to ∼) - from = Prod.map id (F._⟨$⟩_ (Equivalent.from F⇔T)) + from = Prod.map (_⟨$⟩_ (Equivalent.from A₁⇔A₂)) (_⟨$⟩_ B-from) - from-cong : _≈T_ =[ from ]⇒ _≈F_ - from-cong (P.refl , ∼) = (P.refl , F.cong (Equivalent.from F⇔T) ∼) + from-cong : _≈₂_ =[ from ]⇒ _≈₁_ + from-cong (P.refl , ∼) = (P.refl , F.cong B-from ∼) -⇔ : ∀ {a b₁ b₂} {A : Set a} {B₁ : A → Set b₁} {B₂ : A → Set b₂} → - (∀ {x} → B₁ x ⇔ B₂ x) → Σ A B₁ ⇔ Σ A B₂ -⇔ {B₁ = B₁} {B₂} B₁⇔B₂ = +equivalent′ : + ∀ {a₁ a₂ b₁ b₁′ b₂ b₂′} + {A₁ : Set a₁} {A₂ : Set a₂} + {B₁ : I.Setoid A₁ b₁ b₁′} (B₂ : I.Setoid A₂ b₂ b₂′) + (A₁↠A₂ : A₁ ↠ A₂) → + (∀ {x} → Equivalent (B₁ at x) (B₂ at (Surjection.to A₁↠A₂ ⟨$⟩ x))) → + Equivalent (setoid (P.setoid A₁) B₁) (setoid (P.setoid A₂) B₂) +equivalent′ {B₁ = B₁} B₂ A₁↠A₂ B₁⇔B₂ = + equivalent (Surjection.equivalent A₁↠A₂) B-to B-from + where + B-to : ∀ {x} → B₁ at x ⟶ B₂ at (Surjection.to A₁↠A₂ ⟨$⟩ x) + B-to = Equivalent.to B₁⇔B₂ + + subst-cong : ∀ {i a p} {I : Set i} {A : I → Set a} + (P : ∀ {i} → A i → A i → Set p) {i i′} {x y : A i} + (i≡i′ : P._≡_ i i′) → + P x y → P (P.subst A i≡i′ x) (P.subst A i≡i′ y) + subst-cong P P.refl p = p + + B-from : ∀ {y} → B₂ at y ⟶ B₁ at (Surjection.from A₁↠A₂ ⟨$⟩ y) + B-from = record + { _⟨$⟩_ = λ x → Equivalent.from B₁⇔B₂ ⟨$⟩ + P.subst (I.Setoid.Carrier B₂) + (P.sym $ Surjection.right-inverse-of A₁↠A₂ _) + x + ; cong = F.cong (Equivalent.from B₁⇔B₂) ∘ + subst-cong (λ {x} → I.Setoid._≈_ B₂ {x} {x}) + (P.sym (Surjection.right-inverse-of A₁↠A₂ _)) + } + +⇔ : ∀ {a₁ a₂ b₁ b₂} + {A₁ : Set a₁} {A₂ : Set a₂} + {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂} + (A₁⇔A₂ : A₁ ⇔ A₂) → + (∀ {x} → B₁ x → B₂ (Equivalent.to A₁⇔A₂ ⟨$⟩ x)) → + (∀ {y} → B₂ y → B₁ (Equivalent.from A₁⇔A₂ ⟨$⟩ y)) → + Σ A₁ B₁ ⇔ Σ A₂ B₂ +⇔ {B₁ = B₁} {B₂} A₁⇔A₂ B-to B-from = Inverse.equivalent (Rel⇿≡ {B = B₂}) ⟨∘⟩ - equivalent (λ {x} → - Inverse.equivalent (H.≡⇿≅ B₂) ⟨∘⟩ - B₁⇔B₂ {x} ⟨∘⟩ - Inverse.equivalent (Inv.sym (H.≡⇿≅ B₁))) ⟨∘⟩ + equivalent A₁⇔A₂ + (Inverse.to (H.≡⇿≅ B₂) ⊚ P.→-to-⟶ B-to ⊚ Inverse.from (H.≡⇿≅ B₁)) + (Inverse.to (H.≡⇿≅ B₁) ⊚ P.→-to-⟶ B-from ⊚ Inverse.from (H.≡⇿≅ B₂)) + ⟨∘⟩ + Eq.sym (Inverse.equivalent (Rel⇿≡ {B = B₁})) + +⇔′ : ∀ {a₁ a₂ b₁ b₂} + {A₁ : Set a₁} {A₂ : Set a₂} + {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂} + (A₁↠A₂ : A₁ ↠ A₂) → + (∀ {x} → _⇔_ (B₁ x) (B₂ (Surjection.to A₁↠A₂ ⟨$⟩ x))) → + _⇔_ (Σ A₁ B₁) (Σ A₂ B₂) +⇔′ {B₁ = B₁} {B₂} A₁↠A₂ B₁⇔B₂ = + Inverse.equivalent (Rel⇿≡ {B = B₂}) ⟨∘⟩ + equivalent′ (H.indexedSetoid B₂) A₁↠A₂ + (λ {x} → Inverse.equivalent (H.≡⇿≅ B₂) ⟨∘⟩ + B₁⇔B₂ {x} ⟨∘⟩ + Inverse.equivalent (Inv.sym (H.≡⇿≅ B₁))) ⟨∘⟩ Eq.sym (Inverse.equivalent (Rel⇿≡ {B = B₁})) inverse : - ∀ {i} {I : Set i} - {f₁ f₂ t₁ t₂} {From : I.Setoid I f₁ f₂} {To : I.Setoid I t₁ t₂} → - (∀ {i} → Inverse (From at i) (To at i)) → - Inverse (setoid (P.setoid I) From) (setoid (P.setoid I) To) -inverse {I = I} {From = F} {T} F⇿T = record + ∀ {a₁ a₂ b₁ b₁′ b₂ b₂′} + {A₁ : Set a₁} {A₂ : Set a₂} + {B₁ : I.Setoid A₁ b₁ b₁′} (B₂ : I.Setoid A₂ b₂ b₂′) → + (A₁⇿A₂ : A₁ ⇿ A₂) → + (∀ {x} → Inverse (B₁ at x) (B₂ at (Inverse.to A₁⇿A₂ ⟨$⟩ x))) → + Inverse (setoid (P.setoid A₁) B₁) (setoid (P.setoid A₂) B₂) +inverse {A₁ = A₁} {A₂} {B₁} B₂ A₁⇿A₂ B₁⇿B₂ = record { to = Equivalent.to eq ; from = Equivalent.from eq ; inverse-of = record @@ -157,23 +215,59 @@ inverse {I = I} {From = F} {T} F⇿T = record } } where - eq = equivalent (Inverse.equivalent F⇿T) + eq = equivalent′ B₂ (Inverse.surjection A₁⇿A₂) + (Inverse.equivalent B₁⇿B₂) left : Equivalent.from eq LeftInverseOf Equivalent.to eq - left (x , y) = (P.refl , Inverse.left-inverse-of F⇿T y) + left (x , y) = + Inverse.left-inverse-of A₁⇿A₂ x , + I.Setoid.trans B₁ + (lemma (P.sym (Inverse.left-inverse-of A₁⇿A₂ x)) + (P.sym (Inverse.right-inverse-of A₁⇿A₂ + (Inverse.to A₁⇿A₂ ⟨$⟩ x)))) + (Inverse.left-inverse-of B₁⇿B₂ y) + where + lemma : + ∀ {x x′ y} → P._≡_ x x′ → + (eq : P._≡_ (Inverse.to A₁⇿A₂ ⟨$⟩ x) (Inverse.to A₁⇿A₂ ⟨$⟩ x′)) → + I.Setoid._≈_ B₁ + (Inverse.from B₁⇿B₂ ⟨$⟩ P.subst (I.Setoid.Carrier B₂) eq y) + (Inverse.from B₁⇿B₂ ⟨$⟩ y) + lemma P.refl P.refl = I.Setoid.refl B₁ right : Equivalent.from eq RightInverseOf Equivalent.to eq - right (x , y) = (P.refl , Inverse.right-inverse-of F⇿T y) + right (x , y) = + Inverse.right-inverse-of A₁⇿A₂ x , + I.Setoid.trans B₂ + (Inverse.right-inverse-of B₁⇿B₂ + (P.subst (I.Setoid.Carrier B₂) p y)) + (lemma p) + where + p = P.sym $ Inverse.right-inverse-of A₁⇿A₂ x + + lemma : ∀ {x x′ y} (eq : P._≡_ x x′) → + I.Setoid._≈_ B₂ + (P.subst (I.Setoid.Carrier B₂) eq y) + y + lemma P.refl = I.Setoid.refl B₂ -⇿ : ∀ {a b₁ b₂} {A : Set a} {B₁ : A → Set b₁} {B₂ : A → Set b₂} → - (∀ {x} → B₁ x ⇿ B₂ x) → Σ A B₁ ⇿ Σ A B₂ -⇿ {B₁ = B₁} {B₂} B₁⇿B₂ = +⇿ : ∀ {a₁ a₂ b₁ b₂} + {A₁ : Set a₁} {A₂ : Set a₂} + {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂} + (A₁⇿A₂ : A₁ ⇿ A₂) → + (∀ {x} → B₁ x ⇿ B₂ (Inverse.to A₁⇿A₂ ⟨$⟩ x)) → + Σ A₁ B₁ ⇿ Σ A₂ B₂ +⇿ {B₁ = B₁} {B₂} A₁⇿A₂ B₁⇿B₂ = Rel⇿≡ {B = B₂} ⟪∘⟫ - inverse (λ {x} → H.≡⇿≅ B₂ ⟪∘⟫ B₁⇿B₂ {x} ⟪∘⟫ Inv.sym (H.≡⇿≅ B₁)) ⟪∘⟫ + inverse (H.indexedSetoid B₂) A₁⇿A₂ + (λ {x} → H.≡⇿≅ B₂ ⟪∘⟫ B₁⇿B₂ {x} ⟪∘⟫ Inv.sym (H.≡⇿≅ B₁)) ⟪∘⟫ Inv.sym (Rel⇿≡ {B = B₁}) -cong : ∀ {k a b₁ b₂} {A : Set a} {B₁ : A → Set b₁} {B₂ : A → Set b₂} → - (∀ {x} → Isomorphism k (B₁ x) (B₂ x)) → - Isomorphism k (Σ A B₁) (Σ A B₂) -cong {k = Inv.equivalent} = ⇔ +cong : ∀ {k a₁ a₂ b₁ b₂} + {A₁ : Set a₁} {A₂ : Set a₂} + {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂} + (A₁⇿A₂ : _⇿_ A₁ A₂) → + (∀ {x} → Isomorphism k (B₁ x) (B₂ (Inverse.to A₁⇿A₂ ⟨$⟩ x))) → + Isomorphism k (Σ A₁ B₁) (Σ A₂ B₂) +cong {k = Inv.equivalent} = ⇔′ ∘ Inverse.surjection cong {k = Inv.inverse} = ⇿ diff --git a/src/Relation/Binary/Vec/Pointwise.agda b/src/Relation/Binary/Vec/Pointwise.agda new file mode 100644 index 0000000..9613aa4 --- /dev/null +++ b/src/Relation/Binary/Vec/Pointwise.agda @@ -0,0 +1,204 @@ +------------------------------------------------------------------------ +-- Pointwise lifting of relations to vectors +------------------------------------------------------------------------ + +{-# OPTIONS --universe-polymorphism #-} + +module Relation.Binary.Vec.Pointwise where + +open import Category.Applicative.Indexed +open import Data.Fin +open import Data.Plus as Plus hiding (equivalent; map) +open import Data.Vec as Vec hiding ([_]; map) +import Data.Vec.Properties as VecProp +open import Function +open import Function.Equality using (_⟨$⟩_) +open import Function.Equivalence as Equiv + using (_⇔_; module Equivalent) +open import Level +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as P using (_≡_) +open import Relation.Nullary + +private + module Dummy {a} {A : Set a} where + + -- Functional definition. + + record Pointwise (_∼_ : Rel A a) {n} (xs ys : Vec A n) : Set a where + constructor ext + field app : ∀ i → lookup i xs ∼ lookup i ys + + -- Inductive definition. + + infixr 5 _∷_ + + data Pointwise′ (_∼_ : Rel A a) : + ∀ {n} (xs ys : Vec A n) → Set a where + [] : Pointwise′ _∼_ [] [] + _∷_ : ∀ {n x y} {xs ys : Vec A n} + (x∼y : x ∼ y) (xs∼ys : Pointwise′ _∼_ xs ys) → + Pointwise′ _∼_ (x ∷ xs) (y ∷ ys) + + -- The two definitions are equivalent. + + equivalent : ∀ {_∼_ : Rel A a} {n} {xs ys : Vec A n} → + Pointwise _∼_ xs ys ⇔ Pointwise′ _∼_ xs ys + equivalent {_∼_} = Equiv.equivalent (to _ _) from + where + to : ∀ {n} (xs ys : Vec A n) → + Pointwise _∼_ xs ys → Pointwise′ _∼_ xs ys + to [] [] xs∼ys = [] + to (x ∷ xs) (y ∷ ys) xs∼ys = + Pointwise.app xs∼ys zero ∷ + to xs ys (ext (Pointwise.app xs∼ys ∘ suc)) + + nil : Pointwise _∼_ [] [] + nil = ext λ() + + cons : ∀ {n x y} {xs ys : Vec A n} → + x ∼ y → Pointwise _∼_ xs ys → Pointwise _∼_ (x ∷ xs) (y ∷ ys) + cons {x = x} {y} {xs} {ys} x∼y xs∼ys = ext helper + where + helper : ∀ i → lookup i (x ∷ xs) ∼ lookup i (y ∷ ys) + helper zero = x∼y + helper (suc i) = Pointwise.app xs∼ys i + + from : ∀ {n} {xs ys : Vec A n} → + Pointwise′ _∼_ xs ys → Pointwise _∼_ xs ys + from [] = nil + from (x∼y ∷ xs∼ys) = cons x∼y (from xs∼ys) + + -- Pointwise preserves reflexivity. + + refl : ∀ {_∼_ : Rel A a} {n} → + Reflexive _∼_ → Reflexive (Pointwise _∼_ {n = n}) + refl rfl = ext (λ _ → rfl) + + -- Pointwise preserves symmetry. + + sym : ∀ {_∼_ : Rel A a} {n} → + Symmetric _∼_ → Symmetric (Pointwise _∼_ {n = n}) + sym sm xs∼ys = ext λ i → sm (Pointwise.app xs∼ys i) + + -- Pointwise preserves transitivity. + + trans : ∀ {_∼_ : Rel A a} {n} → + Transitive _∼_ → Transitive (Pointwise _∼_ {n = n}) + trans trns xs∼ys ys∼zs = ext λ i → + trns (Pointwise.app xs∼ys i) (Pointwise.app ys∼zs i) + + -- Pointwise preserves equivalences. + + isEquivalence : + ∀ {_∼_ : Rel A a} {n} → + IsEquivalence _∼_ → IsEquivalence (Pointwise _∼_ {n = n}) + isEquivalence equiv = record + { refl = refl (IsEquivalence.refl equiv) + ; sym = sym (IsEquivalence.sym equiv) + ; trans = trans (IsEquivalence.trans equiv) + } + + -- Pointwise _≡_ is equivalent to _≡_. + + Pointwise-≡ : ∀ {n} {xs ys : Vec A n} → + Pointwise _≡_ xs ys ⇔ xs ≡ ys + Pointwise-≡ = + Equiv.equivalent + (to ∘ _⟨$⟩_ (Equivalent.to equivalent)) + (λ xs≡ys → P.subst (Pointwise _≡_ _) xs≡ys (refl P.refl)) + where + to : ∀ {n} {xs ys : Vec A n} → Pointwise′ _≡_ xs ys → xs ≡ ys + to [] = P.refl + to (P.refl ∷ xs∼ys) = P.cong (_∷_ _) $ to xs∼ys + + -- Pointwise and Plus commute when the underlying relation is + -- reflexive. + + ⁺∙⇒∙⁺ : ∀ {_∼_ : Rel A a} {n} {xs ys : Vec A n} → + Plus (Pointwise _∼_) xs ys → Pointwise (Plus _∼_) xs ys + ⁺∙⇒∙⁺ [ ρ≈ρ′ ] = ext (λ x → [ Pointwise.app ρ≈ρ′ x ]) + ⁺∙⇒∙⁺ (ρ ∼⁺⟨ ρ≈ρ′ ⟩ ρ′≈ρ″) = + ext (λ x → _ ∼⁺⟨ Pointwise.app (⁺∙⇒∙⁺ ρ≈ρ′ ) x ⟩ + Pointwise.app (⁺∙⇒∙⁺ ρ′≈ρ″) x) + + ∙⁺⇒⁺∙ : ∀ {_∼_ : Rel A a} {n} {xs ys : Vec A n} → + Reflexive _∼_ → + Pointwise (Plus _∼_) xs ys → Plus (Pointwise _∼_) xs ys + ∙⁺⇒⁺∙ {_∼_} x∼x = + Plus.map (_⟨$⟩_ (Equivalent.from equivalent)) ∘ + helper ∘ + _⟨$⟩_ (Equivalent.to equivalent) + where + helper : ∀ {n} {xs ys : Vec A n} → + Pointwise′ (Plus _∼_) xs ys → Plus (Pointwise′ _∼_) xs ys + helper [] = [ [] ] + helper (_∷_ {x = x} {y = y} {xs = xs} {ys = ys} x∼y xs∼ys) = + x ∷ xs ∼⁺⟨ Plus.map (λ x∼y → x∼y ∷ xs∼xs) x∼y ⟩ + y ∷ xs ∼⁺⟨ Plus.map (λ xs∼ys → x∼x ∷ xs∼ys) (helper xs∼ys) ⟩∎ + y ∷ ys ∎ + where + xs∼xs : Pointwise′ _∼_ xs xs + xs∼xs = Equivalent.to equivalent ⟨$⟩ refl x∼x + +open Dummy public + +-- Note that ∙⁺⇒⁺∙ cannot be defined if the requirement of reflexivity +-- is dropped. + +private + + module Counterexample where + + data D : Set where + i j x y z : D + + data _R_ : Rel D zero where + iRj : i R j + xRy : x R y + yRz : y R z + + xR⁺z : x [ _R_ ]⁺ z + xR⁺z = + x ∼⁺⟨ [ xRy ] ⟩ + y ∼⁺⟨ [ yRz ] ⟩∎ + z ∎ + + ix = i ∷ x ∷ [] + jz = j ∷ z ∷ [] + + ix∙⁺jz : Pointwise′ (Plus _R_) ix jz + ix∙⁺jz = [ iRj ] ∷ xR⁺z ∷ [] + + ¬ix⁺∙jz : ¬ Plus′ (Pointwise′ _R_) ix jz + ¬ix⁺∙jz [ iRj ∷ () ∷ [] ] + ¬ix⁺∙jz ((iRj ∷ xRy ∷ []) ∷ [ () ∷ yRz ∷ [] ]) + ¬ix⁺∙jz ((iRj ∷ xRy ∷ []) ∷ (() ∷ yRz ∷ []) ∷ _) + + counterexample : + ¬ (∀ {n} {xs ys : Vec D n} → + Pointwise (Plus _R_) xs ys → + Plus (Pointwise _R_) xs ys) + counterexample ∙⁺⇒⁺∙ = + ¬ix⁺∙jz (Equivalent.to Plus.equivalent ⟨$⟩ + Plus.map (_⟨$⟩_ (Equivalent.to equivalent)) + (∙⁺⇒⁺∙ (Equivalent.from equivalent ⟨$⟩ ix∙⁺jz))) + +-- Map. + +map : ∀ {a} {A : Set a} {_R_ _R′_ : Rel A a} {n} → + _R_ ⇒ _R′_ → Pointwise _R_ ⇒ Pointwise _R′_ {n} +map R⇒R′ xsRys = ext λ i → + R⇒R′ (Pointwise.app xsRys i) + +-- A variant. + +gmap : ∀ {a} {A A′ : Set a} + {_R_ : Rel A a} {_R′_ : Rel A′ a} {f : A → A′} {n} → + _R_ =[ f ]⇒ _R′_ → + Pointwise _R_ =[ Vec.map {n = n} f ]⇒ Pointwise _R′_ +gmap {_R′_ = _R′_} {f} R⇒R′ {i = xs} {j = ys} xsRys = ext λ i → + let module M = Morphism (VecProp.lookup-morphism i) in + P.subst₂ _R′_ (P.sym $ M.op-<$> f xs) + (P.sym $ M.op-<$> f ys) + (R⇒R′ (Pointwise.app xsRys i)) diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda index 173ec65..a9ec05c 100644 --- a/src/Relation/Nullary/Negation.agda +++ b/src/Relation/Nullary/Negation.agda @@ -98,7 +98,7 @@ decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p) -- Double-negation is a monad (if we assume that all elements of ¬ ¬ P -- are equal). -¬¬-Monad : RawMonad (λ P → ¬ ¬ P) +¬¬-Monad : ∀ {p} → RawMonad (λ (P : Set p) → ¬ ¬ P) ¬¬-Monad = record { return = contradiction ; _>>=_ = λ x f → negated-stable (¬¬-map f x) |