------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the membership predicate for fresh lists
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)

module Data.List.Fresh.Membership.Setoid.Properties {c ℓ} (S : Setoid c ℓ) where

open import Level using (Level; _⊔_)
open import Data.Empty
open import Data.Nat.Base
open import Data.Nat.Properties
open import Data.Product.Base using (∃; _×_; _,_)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; fromInj₂)

open import Function.Base using (id; _∘′_; _$_)
open import Relation.Nullary
open import Relation.Unary as Unary using (Pred)
import Relation.Binary.Definitions as Binary
import Relation.Binary.PropositionalEquality.Core as ≡
open import Relation.Nary

open import Data.List.Fresh
open import Data.List.Fresh.Properties
open import Data.List.Fresh.Membership.Setoid S
open import Data.List.Fresh.Relation.Unary.Any using (Any; here; there; _─_)
import Data.List.Fresh.Relation.Unary.Any.Properties as List#

open Setoid S renaming (Carrier to A)

private
  variable
    p r : Level

------------------------------------------------------------------------
-- transport

module _ {R : Rel A r} where

  ≈-subst-∈ : ∀ {x y} {xs : List# A R} → x ≈ y → x ∈ xs → y ∈ xs
  ≈-subst-∈ x≈y (here x≈x′)  = here (trans (sym x≈y) x≈x′)
  ≈-subst-∈ x≈y (there x∈xs) = there (≈-subst-∈ x≈y x∈xs)

------------------------------------------------------------------------
-- relationship to fresh

module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) where

  fresh⇒∉ : ∀ {x} {xs : List# A R} → x # xs → x ∉ xs
  fresh⇒∉ (r , _)    (here x≈y)   = R⇒≉ r x≈y
  fresh⇒∉ (_ , x#xs) (there x∈xs) = fresh⇒∉ x#xs x∈xs

------------------------------------------------------------------------
-- disjointness

module _ {R : Rel A r} where

  distinct : ∀ {x y} {xs : List# A R} → x ∈ xs → y ∉ xs → x ≉ y
  distinct x∈xs y∉xs x≈y = y∉xs (≈-subst-∈ x≈y x∈xs)

------------------------------------------------------------------------
-- remove

module _ {R : Rel A r} where

  remove-inv : ∀ {x y} {xs : List# A R} (x∈xs : x ∈ xs) →
               y ∈ xs → x ≈ y ⊎ y ∈ (xs ─ x∈xs)
  remove-inv (here x≈z)   (here y≈z)   = inj₁ (trans x≈z (sym y≈z))
  remove-inv (here _)     (there y∈xs) = inj₂ y∈xs
  remove-inv (there _)    (here y≈z)   = inj₂ (here y≈z)
  remove-inv (there x∈xs) (there y∈xs) = Sum.map₂ there (remove-inv x∈xs y∈xs)

  ∈-remove : ∀ {x y} {xs : List# A R} (x∈xs : x ∈ xs) → y ∈ xs → x ≉ y → y ∈ (xs ─ x∈xs)
  ∈-remove x∈xs y∈xs x≉y = fromInj₂ (⊥-elim ∘′ x≉y) (remove-inv x∈xs y∈xs)

module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) (≉⇒R : ∀[ _≉_ ⇒ R ]) where

  private
    R≈ : R Binary.Respectsˡ _≈_
    R≈ x≈y Rxz = ≉⇒R (R⇒≉ Rxz ∘′ trans x≈y)

  fresh-remove : ∀ {x} {xs : List# A R} (x∈xs : x ∈ xs) → x # (xs ─ x∈xs)
  fresh-remove {xs = cons x xs pr} (here x≈y)   = fresh-respectsˡ R≈ (sym x≈y) pr
  fresh-remove {xs = cons x xs pr} (there x∈xs) =
    ≉⇒R (distinct x∈xs (fresh⇒∉ R⇒≉ pr)) , fresh-remove x∈xs

  ∉-remove : ∀ {x} {xs : List# A R} (x∈xs : x ∈ xs) → x ∉ (xs ─ x∈xs)
  ∉-remove x∈xs = fresh⇒∉ R⇒≉ (fresh-remove x∈xs)

------------------------------------------------------------------------
-- injection

module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) where

  injection : ∀ {xs ys : List# A R} (inj : ∀ {x} → x ∈ xs → x ∈ ys) →
              length xs ≤ length ys
  injection {[]}                 {ys} inj = z≤n
  injection {xxs@(cons x xs pr)} {ys} inj = begin
    length xxs               ≤⟨ s≤s (injection step) ⟩
    suc (length (ys ─ x∈ys)) ≡⟨ ≡.sym (List#.length-remove x∈ys) ⟩
    length ys                ∎

    where

    open ≤-Reasoning

    x∉xs : x ∉ xs
    x∉xs = fresh⇒∉ R⇒≉ pr

    x∈ys : x ∈ ys
    x∈ys = inj (here refl)

    step : ∀ {y} → y ∈ xs → y ∈ (ys ─ x∈ys)
    step {y} y∈xs = ∈-remove x∈ys (inj (there y∈xs)) (distinct y∈xs x∉xs ∘′ sym)

  strict-injection : ∀ {xs ys : List# A R} (inj : ∀ {x} → x ∈ xs → x ∈ ys) →
   (∃ λ x → x ∈ ys × x ∉ xs) → length xs < length ys
  strict-injection {xs} {ys} inj (x , x∈ys , x∉xs) = begin
    suc (length xs)          ≤⟨ s≤s (injection step) ⟩
    suc (length (ys ─ x∈ys)) ≡⟨ ≡.sym (List#.length-remove x∈ys) ⟩
    length ys                ∎

    where

    open ≤-Reasoning

    step : ∀ {y} → y ∈ xs → y ∈ (ys ─ x∈ys)
    step {y} y∈xs = fromInj₂ (λ x≈y → ⊥-elim (x∉xs (≈-subst-∈ (sym x≈y) y∈xs)))
                  $ remove-inv x∈ys (inj y∈xs)


------------------------------------------------------------------------
-- proof irrelevance

module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) (≈-irrelevant : Binary.Irrelevant _≈_) where

  ∈-irrelevant : ∀ {x} {xs : List# A R} → Irrelevant (x ∈ xs)
  -- positive cases
  ∈-irrelevant (here x≈y₁)   (here x≈y₂)   = ≡.cong here (≈-irrelevant x≈y₁ x≈y₂)
  ∈-irrelevant (there x∈xs₁) (there x∈xs₂) = ≡.cong there (∈-irrelevant x∈xs₁ x∈xs₂)
  -- absurd cases
  ∈-irrelevant {xs = cons x xs pr} (here x≈y)    (there x∈xs₂) =
    ⊥-elim (distinct x∈xs₂ (fresh⇒∉ R⇒≉ pr) x≈y)
  ∈-irrelevant {xs = cons x xs pr} (there x∈xs₁) (here x≈y)    =
    ⊥-elim (distinct x∈xs₁ (fresh⇒∉ R⇒≉ pr) x≈y)