------------------------------------------------------------------------
-- The Agda standard library
--
-- A definition for the permutation relation using setoid equality
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (Setoid)
module Data.List.Relation.Binary.Permutation.Setoid
{a ℓ} (S : Setoid a ℓ) where
open import Data.List.Base using (List; _∷_)
import Data.List.Relation.Binary.Permutation.Homogeneous as Homogeneous
import Data.List.Relation.Binary.Equality.Setoid as ≋
open import Function.Base using (_∘′_)
open import Level using (_⊔_)
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Definitions
using (Reflexive; Symmetric; Transitive; LeftTrans; RightTrans)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
open import Relation.Binary.Reasoning.Syntax
open import Relation.Binary.Structures using (IsEquivalence)
open module ≈ = Setoid S using (_≈_) renaming (Carrier to A)
open ≋ S using (_≋_; _∷_; ≋-refl; ≋-sym; ≋-trans)
------------------------------------------------------------------------
-- Definition, based on `Homogeneous`
open Homogeneous public
using (refl; prep; swap; trans; onIndices)
infix 3 _↭_
_↭_ : Rel (List A) (a ⊔ ℓ)
_↭_ = Homogeneous.Permutation _≈_
steps = Homogeneous.steps {R = _≈_}
------------------------------------------------------------------------
-- Constructor aliases
-- Constructor alias
↭-reflexive-≋ : _≋_ ⇒ _↭_
↭-reflexive-≋ = refl
↭-trans : Transitive _↭_
↭-trans = trans
-- These provide aliases for `swap` and `prep` when the elements being
-- swapped or prepended are propositionally equal
↭-prep : ∀ x {xs ys} → xs ↭ ys → x ∷ xs ↭ x ∷ ys
↭-prep x xs↭ys = prep ≈.refl xs↭ys
↭-swap : ∀ x y {xs ys} → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
↭-swap x y xs↭ys = swap ≈.refl ≈.refl xs↭ys
------------------------------------------------------------------------
-- _↭_ is an equivalence
↭-reflexive : _≡_ ⇒ _↭_
↭-reflexive refl = ↭-reflexive-≋ ≋-refl
↭-refl : Reflexive _↭_
↭-refl = ↭-reflexive refl
↭-sym : Symmetric _↭_
↭-sym = Homogeneous.sym ≈.sym
-- As with the existing proofs `↭-respʳ-≋` and `↭-respˡ-≋` in `Setoid.Properties`
-- (which appeal to symmetry of the underlying equality, and its effect on the
-- proofs of symmetry for both pointwise equality and permutation) to the effect
-- that _↭_ respects _≋_ on the left and right, such arguments can be both
-- streamlined, and used to define a 'smart' constructor `↭-trans′` for transitivity.
--
-- The arguments below show how proofs of permutation can have all transitive
-- compositions with instances of `refl` pushed to the leaves of derivations,
-- thereby addressing the inefficiencies analysed in issue #1113
--
-- Conjecture: these transformations are `steps` invariant, but that is moot,
-- given their use here, and in `Setoid.Properties.↭-split` (without requiring
-- WF-induction on `steps`) to enable a new, sharper, analysis of lists `xs`
-- such that `xs ↭ ys ++ [ x ] ++ zs` in terms of `x`, `ys`, and `zs`.
↭-transˡ-≋ : LeftTrans _≋_ _↭_
↭-transˡ-≋ xs≋ys (refl ys≋zs)
= refl (≋-trans xs≋ys ys≋zs)
↭-transˡ-≋ (x≈y ∷ xs≋ys) (prep y≈z ys↭zs)
= prep (≈.trans x≈y y≈z) (↭-transˡ-≋ xs≋ys ys↭zs)
↭-transˡ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ ys↭zs)
= swap (≈.trans x≈y eq₁) (≈.trans w≈z eq₂) (↭-transˡ-≋ xs≋ys ys↭zs)
↭-transˡ-≋ xs≋ys (trans ys↭ws ws↭zs)
= trans (↭-transˡ-≋ xs≋ys ys↭ws) ws↭zs
↭-transʳ-≋ : RightTrans _↭_ _≋_
↭-transʳ-≋ (refl xs≋ys) ys≋zs
= refl (≋-trans xs≋ys ys≋zs)
↭-transʳ-≋ (prep x≈y xs↭ys) (y≈z ∷ ys≋zs)
= prep (≈.trans x≈y y≈z) (↭-transʳ-≋ xs↭ys ys≋zs)
↭-transʳ-≋ (swap eq₁ eq₂ xs↭ys) (x≈w ∷ y≈z ∷ ys≋zs)
= swap (≈.trans eq₁ y≈z) (≈.trans eq₂ x≈w) (↭-transʳ-≋ xs↭ys ys≋zs)
↭-transʳ-≋ (trans xs↭ws ws↭ys) ys≋zs
= trans xs↭ws (↭-transʳ-≋ ws↭ys ys≋zs)
↭-trans′ : Transitive _↭_
↭-trans′ (refl xs≋ys) ys↭zs = ↭-transˡ-≋ xs≋ys ys↭zs
↭-trans′ xs↭ys (refl ys≋zs) = ↭-transʳ-≋ xs↭ys ys≋zs
↭-trans′ xs↭ys ys↭zs = trans xs↭ys ys↭zs
↭-isEquivalence : IsEquivalence _↭_
↭-isEquivalence = record
{ refl = ↭-refl
; sym = ↭-sym
; trans = ↭-trans
}
↭-setoid : Setoid _ _
↭-setoid = record { isEquivalence = ↭-isEquivalence }
------------------------------------------------------------------------
-- A reasoning API to chain permutation proofs
module PermutationReasoning where
private module Base = ≈-Reasoning ↭-setoid
open Base public
hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨)
renaming (≈-go to ↭-go)
open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public
open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ ↭-reflexive-≋) ≋-sym public
-- Some extra combinators that allow us to skip certain elements
infixr 2 step-swap step-prep
-- Skip reasoning on the first element
step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs →
xs ↭ ys → (x ∷ xs) IsRelatedTo zs
step-prep x xs rel xs↭ys = ↭-go (↭-prep x xs↭ys) rel
-- Skip reasoning about the first two elements
step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs →
xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs
step-swap x y xs rel xs↭ys = ↭-go (↭-swap x y xs↭ys) rel
syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z
syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4