text:
module BasicIS4.Metatheory.DyadicHilbert-TarskiOvergluedDyadicImplicit where

open import BasicIS4.Syntax.DyadicHilbert public
open import BasicIS4.Semantics.TarskiOvergluedDyadicImplicit public

open ImplicitSyntax (_⊢_) (mono²⊢) public

-- Completeness with respect to a particular model.

module _ {{_ : Model}} where
  reify : ∀ {A Γ Δ} → Γ ⁏ Δ ⊩ A → Γ ⁏ Δ ⊢ A
  reify {α P}   s = syn s
  reify {A ▻ B} s = syn (s refl⊆²)
  reify {□ A}   s = syn (s refl⊆²)
  reify {A ∧ B} s = pair (reify (π₁ s)) (reify (π₂ s))
  reify {⊤}    s = unit

  reify⋆ : ∀ {Ξ Γ Δ} → Γ ⁏ Δ ⊩⋆ Ξ → Γ ⁏ Δ ⊢⋆ Ξ
  reify⋆ {∅}     ∙        = ∙
  reify⋆ {Ξ , A} (ts , t) = reify⋆ ts , reify t

-- Additional useful equipment.

module _ {{_ : Model}} where
  ⟪K⟫ : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊩ A → Γ ⁏ Δ ⊩ B ▻ A
  ⟪K⟫ {A} a ψ = let a′ = mono²⊩ {A} ψ a
                in  app ck (reify a′) ⅋ K a′

  ⟪S⟫′ : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊩ A ▻ B ▻ C → Γ ⁏ Δ ⊩ (A ▻ B) ▻ A ▻ C
  ⟪S⟫′ {A} {B} {C} s₁ ψ = let s₁′ = mono²⊩ {A ▻ B ▻ C} ψ s₁
                              t   = syn (s₁′ refl⊆²)
                          in  app cs t ⅋ λ s₂ ψ′ →
                                let s₁″ = mono²⊩ {A ▻ B ▻ C} (trans⊆² ψ ψ′) s₁
                                    s₂′ = mono²⊩ {A ▻ B} ψ′ s₂
                                    t′  = syn (s₁″ refl⊆²)
                                    u   = syn (s₂′ refl⊆²)
                                in  app (app cs t′) u ⅋ ⟪S⟫ s₁″ s₂′

  _⟪D⟫_ : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊩ □ (A ▻ B) → Γ ⁏ Δ ⊩ □ A → Γ ⁏ Δ ⊩ □ B
  (s₁ ⟪D⟫ s₂) ψ = let t ⅋ s₁′ = s₁ ψ
                      u ⅋ a   = s₂ ψ
                  in  app (app cdist t) u ⅋ s₁′ ⟪$⟫ a

  _⟪D⟫′_ : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊩ □ (A ▻ B) → Γ ⁏ Δ ⊩ □ A ▻ □ B
  _⟪D⟫′_ {A} {B} s₁ ψ = let s₁′ = mono²⊩ {□ (A ▻ B)} ψ s₁
                        in  app cdist (reify (λ {_} ψ′ → s₁′ ψ′)) ⅋ _⟪D⟫_ s₁′

  ⟪↑⟫ : ∀ {A Γ Δ} → Γ ⁏ Δ ⊩ □ A → Γ ⁏ Δ ⊩ □ □ A
  ⟪↑⟫ {A} s ψ = app cup (syn (s ψ)) ⅋ λ ψ′ → s (trans⊆² ψ ψ′)

  _⟪,⟫′_ : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊩ A → Γ ⁏ Δ ⊩ B ▻ A ∧ B
  _⟪,⟫′_ {A} a ψ = let a′ = mono²⊩ {A} ψ a
                   in  app cpair (reify a′) ⅋ _,_ a′

-- Soundness with respect to all models, or evaluation.

eval : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊨ A
eval (var i)   γ δ = lookup i γ
eval (app t u) γ δ = eval t γ δ ⟪$⟫ eval u γ δ
eval ci        γ δ = K (ci ⅋ I)
eval ck        γ δ = K (ck ⅋ ⟪K⟫)
eval cs        γ δ = K (cs ⅋ ⟪S⟫′)
eval (mvar i)  γ δ = mlookup i δ
eval (box t)   γ δ = λ ψ → let δ′ = mono²⊩⋆ ψ δ
                            in  mmulticut (reify⋆ δ′) (box t) ⅋
                                  eval t ∙ δ′
eval cdist     γ δ = K (cdist ⅋ _⟪D⟫′_)
eval cup       γ δ = K (cup ⅋ ⟪↑⟫)
eval cdown     γ δ = K (cdown ⅋ ⟪↓⟫)
eval cpair     γ δ = K (cpair ⅋ _⟪,⟫′_)
eval cfst      γ δ = K (cfst ⅋ π₁)
eval csnd      γ δ = K (csnd ⅋ π₂)
eval unit      γ δ = ∙

-- TODO: Correctness of evaluation with respect to conversion.

-- The canonical model.

private
  instance
    canon : Model
    canon = record
      { _⊩ᵅ_    = λ Π P → Π ⊢ α P
      ; mono²⊩ᵅ = mono²⊢
      }

-- Soundness with respect to the canonical model.

reflectᶜ : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊩ A
reflectᶜ {α P}   t = t ⅋ t
reflectᶜ {A ▻ B} t = λ ψ → let t′ = mono²⊢ ψ t
                            in  t′ ⅋ λ a → reflectᶜ (app t′ (reify a))
reflectᶜ {□ A}   t = λ ψ → let t′ = mono²⊢ ψ t
                            in  t′ ⅋ reflectᶜ (down t′)
reflectᶜ {A ∧ B} t = reflectᶜ (fst t) , reflectᶜ (snd t)
reflectᶜ {⊤}    t = ∙

reflectᶜ⋆ : ∀ {Ξ Γ Δ} → Γ ⁏ Δ ⊢⋆ Ξ → Γ ⁏ Δ ⊩⋆ Ξ
reflectᶜ⋆ {∅}     ∙        = ∙
reflectᶜ⋆ {Ξ , A} (ts , t) = reflectᶜ⋆ ts , reflectᶜ t

-- Reflexivity and transitivity.

refl⊩⋆ : ∀ {Γ Δ} → Γ ⁏ Δ ⊩⋆ Γ
refl⊩⋆ = reflectᶜ⋆ refl⊢⋆

mrefl⊩⋆ : ∀ {Γ Δ} → Γ ⁏ Δ ⊩⋆ □⋆ Δ
mrefl⊩⋆ = reflectᶜ⋆ mrefl⊢⋆

trans⊩⋆ : ∀ {Γ Γ′ Δ Δ′ Ξ} → Γ ⁏ Δ ⊩⋆ Γ′ ⧺ (□⋆ Δ′) → Γ′ ⁏ Δ′ ⊩⋆ Ξ → Γ ⁏ Δ ⊩⋆ Ξ
trans⊩⋆ ts us = reflectᶜ⋆ (trans⊢⋆ (reify⋆ ts) (reify⋆ us))

-- Completeness with respect to all models, or quotation.

quot : ∀ {A Γ Δ} → Γ ⁏ Δ ⊨ A → Γ ⁏ Δ ⊢ A
quot s = reify (s refl⊩⋆ mrefl⊩⋆)

-- Normalisation by evaluation.

norm : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ A
norm = quot ∘ eval

-- TODO: Correctness of normalisation with respect to conversion.

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to bag and set equality
------------------------------------------------------------------------

-- Bag and set equality are defined in Data.List.Any.

module Data.List.Any.BagAndSetEquality where

open import Algebra
open import Algebra.FunctionProperties
open import Category.Monad
open import Data.List as List
import Data.List.Properties as LP
open import Data.List.Any as Any using (Any); open Any.Any
open import Data.List.Any.Properties
open import Data.Product
open import Data.Sum
open import Function
open import Function.Equality using (_⟨$⟩_)
import Function.Equivalence as FE
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Function.Related as Related using (↔⇒; ⌊_⌋; ⌊_⌋→; ⇒→)
open import Function.Related.TypeIsomorphisms
open import Relation.Binary
import Relation.Binary.EqReasoning as EqR
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≗_)
open import Relation.Binary.Sum
open import Relation.Nullary

open Any.Membership-≡
private
  module Eq  {k a} {A : Set a} = Setoid ([ k ]-Equality A)
  module Ord {k a} {A : Set a} = Preorder ([ k ]-Order A)
  module ×⊎ {k ℓ} = CommutativeSemiring (×⊎-CommutativeSemiring k ℓ)
  open module ListMonad {ℓ} = RawMonad (List.monad {ℓ = ℓ})
  module ListMonoid {a} {A : Set a} = Monoid (List.monoid A)

------------------------------------------------------------------------
-- Congruence lemmas

-- _∷_ is a congruence.

∷-cong : ∀ {a k} {A : Set a} {x₁ x₂ : A} {xs₁ xs₂} →
         x₁ ≡ x₂ → xs₁ ∼[ k ] xs₂ → x₁ ∷ xs₁ ∼[ k ] x₂ ∷ xs₂
∷-cong {x₂ = x} {xs₁} {xs₂} P.refl xs₁≈xs₂ {y} =
  y ∈ x ∷ xs₁        ↔⟨ sym $ ∷↔ (_≡_ y) ⟩
  (y ≡ x ⊎ y ∈ xs₁)  ∼⟨ (y ≡ x ∎) ⊎-cong xs₁≈xs₂ ⟩
  (y ≡ x ⊎ y ∈ xs₂)  ↔⟨ ∷↔ (_≡_ y) ⟩
  y ∈ x ∷ xs₂        ∎
  where open Related.EquationalReasoning

-- List.map is a congruence.

map-cong : ∀ {ℓ k} {A B : Set ℓ} {f₁ f₂ : A → B} {xs₁ xs₂} →
           f₁ ≗ f₂ → xs₁ ∼[ k ] xs₂ →
           List.map f₁ xs₁ ∼[ k ] List.map f₂ xs₂
map-cong {ℓ} {f₁ = f₁} {f₂} {xs₁} {xs₂} f₁≗f₂ xs₁≈xs₂ {x} =
  x ∈ List.map f₁ xs₁       ↔⟨ sym $ map↔ {a = ℓ} {b = ℓ} {p = ℓ} ⟩
  Any (λ y → x ≡ f₁ y) xs₁  ∼⟨ Any-cong (↔⇒ ∘ helper) xs₁≈xs₂ ⟩
  Any (λ y → x ≡ f₂ y) xs₂  ↔⟨ map↔ {a = ℓ} {b = ℓ} {p = ℓ} ⟩
  x ∈ List.map f₂ xs₂       ∎
  where
  open Related.EquationalReasoning

  helper : ∀ y → x ≡ f₁ y ↔ x ≡ f₂ y
  helper y = record
    { to         = P.→-to-⟶ (λ x≡f₁y → P.trans x≡f₁y (        f₁≗f₂ y))
    ; from       = P.→-to-⟶ (λ x≡f₂y → P.trans x≡f₂y (P.sym $ f₁≗f₂ y))
    ; inverse-of = record
      { left-inverse-of  = λ _ → P.proof-irrelevance _ _
      ; right-inverse-of = λ _ → P.proof-irrelevance _ _
      }
    }

-- _++_ is a congruence.

++-cong : ∀ {a k} {A : Set a} {xs₁ xs₂ ys₁ ys₂ : List A} →
          xs₁ ∼[ k ] xs₂ → ys₁ ∼[ k ] ys₂ →
          xs₁ ++ ys₁ ∼[ k ] xs₂ ++ ys₂
++-cong {a} {xs₁ = xs₁} {xs₂} {ys₁} {ys₂} xs₁≈xs₂ ys₁≈ys₂ {x} =
  x ∈ xs₁ ++ ys₁       ↔⟨ sym $ ++↔ {a = a} {p = a} ⟩
  (x ∈ xs₁ ⊎ x ∈ ys₁)  ∼⟨ xs₁≈xs₂ ⊎-cong ys₁≈ys₂ ⟩
  (x ∈ xs₂ ⊎ x ∈ ys₂)  ↔⟨ ++↔ {a = a} {p = a} ⟩
  x ∈ xs₂ ++ ys₂       ∎
  where open Related.EquationalReasoning

-- concat is a congruence.

concat-cong : ∀ {a k} {A : Set a} {xss₁ xss₂ : List (List A)} →
              xss₁ ∼[ k ] xss₂ → concat xss₁ ∼[ k ] concat xss₂
concat-cong {a} {xss₁ = xss₁} {xss₂} xss₁≈xss₂ {x} =
  x ∈ concat xss₁         ↔⟨ sym $ concat↔ {a = a} {p = a} ⟩
  Any (Any (_≡_ x)) xss₁  ∼⟨ Any-cong (λ _ → _ ∎) xss₁≈xss₂ ⟩
  Any (Any (_≡_ x)) xss₂  ↔⟨ concat↔ {a = a} {p = a} ⟩
  x ∈ concat xss₂         ∎
  where open Related.EquationalReasoning

-- The list monad's bind is a congruence.

>>=-cong : ∀ {ℓ k} {A B : Set ℓ} {xs₁ xs₂} {f₁ f₂ : A → List B} →
           xs₁ ∼[ k ] xs₂ → (∀ x → f₁ x ∼[ k ] f₂ x) →
           (xs₁ >>= f₁) ∼[ k ] (xs₂ >>= f₂)
>>=-cong {ℓ} {xs₁ = xs₁} {xs₂} {f₁} {f₂} xs₁≈xs₂ f₁≈f₂ {x} =
  x ∈ (xs₁ >>= f₁)          ↔⟨ sym $ >>=↔ {ℓ = ℓ} {p = ℓ} ⟩
  Any (λ y → x ∈ f₁ y) xs₁  ∼⟨ Any-cong (λ x → f₁≈f₂ x) xs₁≈xs₂ ⟩
  Any (λ y → x ∈ f₂ y) xs₂  ↔⟨ >>=↔ {ℓ = ℓ} {p = ℓ} ⟩
  x ∈ (xs₂ >>= f₂)          ∎
  where open Related.EquationalReasoning

-- _⊛_ is a congruence.

⊛-cong : ∀ {ℓ k} {A B : Set ℓ} {fs₁ fs₂ : List (A → B)} {xs₁ xs₂} →
         fs₁ ∼[ k ] fs₂ → xs₁ ∼[ k ] xs₂ → fs₁ ⊛ xs₁ ∼[ k ] fs₂ ⊛ xs₂
⊛-cong fs₁≈fs₂ xs₁≈xs₂ =
  >>=-cong fs₁≈fs₂ λ f →
  >>=-cong xs₁≈xs₂ λ x →
  _ ∎
  where open Related.EquationalReasoning

-- _⊗_ is a congruence.

⊗-cong : ∀ {ℓ k} {A B : Set ℓ} {xs₁ xs₂ : List A} {ys₁ ys₂ : List B} →
         xs₁ ∼[ k ] xs₂ → ys₁ ∼[ k ] ys₂ →
         (xs₁ ⊗ ys₁) ∼[ k ] (xs₂ ⊗ ys₂)
⊗-cong {ℓ} xs₁≈xs₂ ys₁≈ys₂ =
  ⊛-cong (⊛-cong (Ord.refl {x = [ _,_ {a = ℓ} {b = ℓ} ]})
                 xs₁≈xs₂)
         ys₁≈ys₂

------------------------------------------------------------------------
-- Other properties

-- _++_ and [] form a commutative monoid, with either bag or set
-- equality as the underlying equality.

commutativeMonoid : ∀ {a} → Symmetric-kind → Set a →
                    CommutativeMonoid _ _
commutativeMonoid {a} k A = record
  { Carrier             = List A
  ; _≈_                 = λ xs ys → xs ∼[ ⌊ k ⌋ ] ys
  ; _∙_                 = _++_
  ; ε                   = []
  ; isCommutativeMonoid = record
    { isSemigroup = record
      { isEquivalence = Eq.isEquivalence
      ; assoc         = λ xs ys zs →
                          Eq.reflexive (ListMonoid.assoc xs ys zs)
      ; ∙-cong        = ++-cong
      }
    ; identityˡ = λ xs {x} → x ∈ xs ∎
    ; comm      = λ xs ys {x} →
                    x ∈ xs ++ ys  ↔⟨ ++↔++ {a = a} {p = a} xs ys ⟩
                    x ∈ ys ++ xs  ∎
    }
  }
  where open Related.EquationalReasoning

-- The only list which is bag or set equal to the empty list (or a
-- subset or subbag of the list) is the empty list itself.

empty-unique : ∀ {k a} {A : Set a} {xs : List A} →
               xs ∼[ ⌊ k ⌋→ ] [] → xs ≡ []
empty-unique {xs = []}    _    = P.refl
empty-unique {xs = _ ∷ _} ∷∼[] with ⇒→ ∷∼[] (here P.refl)
... | ()

-- _++_ is idempotent (under set equality).

++-idempotent : ∀ {a} {A : Set a} →
                Idempotent (λ (xs ys : List A) → xs ∼[ set ] ys) _++_
++-idempotent {a} xs {x} =
  x ∈ xs ++ xs  ∼⟨ FE.equivalence ([ id , id ]′ ∘ _⟨$⟩_ (Inverse.from $ ++↔ {a = a} {p = a}))
                                  (_⟨$⟩_ (Inverse.to $ ++↔ {a = a} {p = a}) ∘ inj₁) ⟩
  x ∈ xs        ∎
  where open Related.EquationalReasoning

-- The list monad's bind distributes from the left over _++_.

>>=-left-distributive :
  ∀ {ℓ} {A B : Set ℓ} (xs : List A) {f g : A → List B} →
  (xs >>= λ x → f x ++ g x) ∼[ bag ] (xs >>= f) ++ (xs >>= g)
>>=-left-distributive {ℓ} xs {f} {g} {y} =
  y ∈ (xs >>= λ x → f x ++ g x)                      ↔⟨ sym $ >>=↔ {ℓ = ℓ} {p = ℓ} ⟩
  Any (λ x → y ∈ f x ++ g x) xs                      ↔⟨ sym (Any-cong (λ _ → ++↔ {a = ℓ} {p = ℓ}) (_ ∎)) ⟩
  Any (λ x → y ∈ f x ⊎ y ∈ g x) xs                   ↔⟨ sym $ ⊎↔ {a = ℓ} {p = ℓ} {q = ℓ} ⟩
  (Any (λ x → y ∈ f x) xs ⊎ Any (λ x → y ∈ g x) xs)  ↔⟨ >>=↔ {ℓ = ℓ} {p = ℓ} ⟨ ×⊎.+-cong {ℓ = ℓ} ⟩ >>=↔ {ℓ = ℓ} {p = ℓ} ⟩
  (y ∈ (xs >>= f) ⊎ y ∈ (xs >>= g))                  ↔⟨ ++↔ {a = ℓ} {p = ℓ} ⟩
  y ∈ (xs >>= f) ++ (xs >>= g)                       ∎
  where open Related.EquationalReasoning

-- The same applies to _⊛_.

⊛-left-distributive :
  ∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) xs₁ xs₂ →
  fs ⊛ (xs₁ ++ xs₂) ∼[ bag ] (fs ⊛ xs₁) ++ (fs ⊛ xs₂)
⊛-left-distributive {B = B} fs xs₁ xs₂ = begin
  fs ⊛ (xs₁ ++ xs₂)                         ≡⟨ P.refl ⟩
  (fs >>= λ f → xs₁ ++ xs₂ >>= return ∘ f)  ≡⟨ (LP.Monad.cong (P.refl {x = fs}) λ f →
                                                LP.Monad.right-distributive xs₁ xs₂ (return ∘ f)) ⟩
  (fs >>= λ f → (xs₁ >>= return ∘ f) ++
                (xs₂ >>= return ∘ f))       ≈⟨ >>=-left-distributive fs ⟩

  (fs >>= λ f → xs₁ >>= return ∘ f) ++
  (fs >>= λ f → xs₂ >>= return ∘ f)         ≡⟨ P.refl ⟩

  (fs ⊛ xs₁) ++ (fs ⊛ xs₂)                  ∎
  where open EqR ([ bag ]-Equality B)

private

  -- If x ∷ xs is set equal to x ∷ ys, then xs and ys are not
  -- necessarily set equal.

  ¬-drop-cons :
    ∀ {a} {A : Set a} {x : A} →
    ¬ (∀ {xs ys} → x ∷ xs ∼[ set ] x ∷ ys → xs ∼[ set ] ys)
  ¬-drop-cons {x = x} drop-cons
    with FE.Equivalence.to x∼[] ⟨$⟩ here P.refl
    where
    x,x≈x :  (x ∷ x ∷ []) ∼[ set ] [ x ]
    x,x≈x = ++-idempotent [ x ]

    x∼[] : [ x ] ∼[ set ] []
    x∼[] = drop-cons x,x≈x
  ... | ()

-- However, the corresponding property does hold for bag equality.

drop-cons : ∀ {a} {A : Set a} {x : A} {xs ys} →
            x ∷ xs ∼[ bag ] x ∷ ys → xs ∼[ bag ] ys
drop-cons {A = A} {x} {xs} {ys} x∷xs≈x∷ys {z} = record
  { to         = P.→-to-⟶ $ f           x∷xs≈x∷ys
  ; from       = P.→-to-⟶ $ f $ Inv.sym x∷xs≈x∷ys
  ; inverse-of = record
    { left-inverse-of  = f∘f           x∷xs≈x∷ys
    ; right-inverse-of = f∘f $ Inv.sym x∷xs≈x∷ys
    }
  }
  where
  open Inverse
  open P.≡-Reasoning

  f : ∀ {xs ys z} → (z ∈ x ∷ xs) ↔ (z ∈ x ∷ ys) → z ∈ xs → z ∈ ys
  f inv z∈xs with to inv ⟨$⟩ there z∈xs | left-inverse-of inv (there z∈xs)
  f inv z∈xs | there z∈ys   | left⁺ = z∈ys
  f inv z∈xs | here  z≡x    | left⁺ with to inv ⟨$⟩ here z≡x | left-inverse-of inv (here z≡x)
  f inv z∈xs | here  z≡x    | left⁺ | there z∈ys   | left⁰ = z∈ys
  f inv z∈xs | here  P.refl | left⁺ | here  P.refl | left⁰ with begin
    here P.refl               ≡⟨ P.sym left⁰ ⟩
    from inv ⟨$⟩ here P.refl  ≡⟨ left⁺ ⟩
    there z∈xs                ∎
  ... | ()

  f∘f : ∀ {xs ys z}
        (inv : (z ∈ x ∷ xs) ↔ (z ∈ x ∷ ys)) (p : z ∈ xs) →
        f (Inv.sym inv) (f inv p) ≡ p
  f∘f inv z∈xs with to inv ⟨$⟩ there z∈xs | left-inverse-of inv (there z∈xs)
  f∘f inv z∈xs | there z∈ys  | left⁺ with from inv ⟨$⟩ there z∈ys | right-inverse-of inv (there z∈ys)
  f∘f inv z∈xs | there z∈ys  | P.refl | .(there z∈xs) | _ = P.refl
  f∘f inv z∈xs | here z≡x    | left⁺ with to inv ⟨$⟩ here z≡x | left-inverse-of inv (here z≡x)
  f∘f inv z∈xs | here z≡x    | left⁺  | there z∈ys   | left⁰ with from inv ⟨$⟩ there z∈ys | right-inverse-of inv (there z∈ys)
  f∘f inv z∈xs | here z≡x    | left⁺  | there z∈ys   | P.refl | .(here z≡x) | _ with from inv ⟨$⟩ here z≡x
                                                                                | right-inverse-of inv (here z≡x)
  f∘f inv z∈xs | here z≡x    | P.refl | there z∈ys   | P.refl | .(here z≡x) | _ | .(there z∈xs) | _ = P.refl
  f∘f inv z∈xs | here P.refl | left⁺  | here  P.refl | left⁰ with begin
    here P.refl               ≡⟨ P.sym left⁰ ⟩
    from inv ⟨$⟩ here P.refl  ≡⟨ left⁺ ⟩
    there z∈xs                ∎
  ... | ()

ext: agda


text:
-- Issue 3536 reported by Malin Altenmüller

-- The problem was that the Treeless compiler reruns the clause
-- compiler, but without the split tree from the coverage
-- checker. However, the split tree is necessary to direct the clause
-- compiler.

data Unit : Set where
 true : Unit

record R : Set where
 coinductive
 field
   f1 : R
   f2 : R
open R public

foo : Unit -> R
f1 (foo true) = foo true
f2 (foo b) = foo b

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --termination-depth=2 #-}

module TerminationWithMerge where

data List (a : Set) : Set where
  []  : List a
  _∷_ : a -> List a -> List a

-- infix

postulate
  a : Set
  Bool : Set
  _≤?_ : a -> a -> Bool

merge : List a -> List a -> List a
merge xs           []           = xs
merge []           ys           = ys
merge (x ∷ xs) (y ∷ ys) with x ≤? y
... | true  = x ∷ merge xs  (y ∷ ys)
... | false = y ∷ merge (x ∷ xs) ys

{- still cannot pass the termination checker, since

   size(x :: xs) <= 1 + max(size(x),size(xs))

but the termination checker does not have maximum, and no
type information that tells it to ignore x in this caculation.

Solution: sized types!
-}


text:
postulate
  F : Set → Set

{-# POLARITY F ⚄ #-}


text:
data ⊥ : Set where

record ⊤ : Set where
  constructor unit

data T : ⊥ → Set where
  con : (i : ⊥) → T i

module M (x : ⊤) where
  bar : (i : ⊥) → T i → ⊥
  bar .i (con i) = i
    module N where
      foo : ⊥
      foo = i

  -- Should not be accepted.
  -- Type signature should be `test : ⊥ → ⊥`
  test : ⊥ → ⊥
  test = N.foo

false : ⊥
false = M.test unit unit


text:
module sn-calculus-confluence.potrec where

open import utility
open import sn-calculus
open import context-properties
  using (->pot-view ; ->E-view)
open import sn-calculus-confluence.helper

open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.Properties
open import Esterel.Lang.CanFunction
open import Esterel.Lang.CanFunction.Properties
  using (canθₛ-subset ; canθₛₕ-subset ; canθₛ-membership ; canθₛₕ-membership
       ; canθₛ-mergeˡ ; canθₛₕ-mergeˡ
       ; canθ-is-present ; canθ-is-absent
       ; canθₛₕ-emit ; canθₛ-emit
       ; term-raise ; canₛ-raise ; canₛₕ-raise
       ; term-nothin ; canₛ-term-nothin ; canₛₕ-term-nothin
       ; canₛ-if-true ; canₛ-if-false ; canₛₕ-if-true ; canₛₕ-if-false
       ; canₛ-capture-emit-signal ; canₛₕ-capture-set-shared)

open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.Context
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import Esterel.Variable.Signal as Signal
  using (Signal)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)

open import Data.Bool
  using (Bool ; true ; false ; if_then_else_)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; [] ; _∷_ ; [_])
open import Data.List.Any
  using (Any ; here ; there ; any)
open import Data.Maybe
  using (Maybe ; just ; nothing)
open import Data.Nat
  using (ℕ ; _≟_ ; zero ; suc ; _+_)
open import Data.Product
  using (Σ ; Σ-syntax ; _,_ ; proj₁ ; proj₂ ; _,′_ ; _×_)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Function
  using (_∘_ ; id ; _∋_)
open import Relation.Nullary
  using (¬_ ; Dec ; yes ; no)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; sym ; trans ; cong ; subst ; module ≡-Reasoning)

open ->pot-view
open ->E-view

open term-nothin
open term-raise
open ≡-Reasoning
  using (begin_ ; _∎ ; _≡⟨_⟩_ ; _≡⟨⟩_)

open import Data.OrderedListMap Signal Signal.unwrap Signal.Status as SigM
open import Data.OrderedListMap SharedVar SharedVar.unwrap (Σ SharedVar.Status (λ _ → ℕ)) as ShrM
open import Data.OrderedListMap SeqVar SeqVar.unwrap ℕ as SeqM

ρ-pot-conf-rec : ∀{p θ ql θl qr θr p≡ql E pin qin FV₀ BV₀ A Al Ar A≡Al}
                 → {ρθ·psn⟶₁ρθl·ql : (ρ⟨ θ , A ⟩· p) sn⟶₁ (ρ⟨ θl , Al ⟩· ql)}
                 → {ρθ·psn⟶₁ρθr·qr : (ρ⟨ θ , A ⟩· p) sn⟶₁ (ρ⟨ θr , Ar ⟩· qr)}
                 → {p≐E⟦pin⟧      : p ≐ E ⟦ pin ⟧e}
                 → {qr≐E⟦qin⟧     : qr ≐ E ⟦ qin ⟧e}
                 → CorrectBinding (ρ⟨ θ , A ⟩· p) FV₀ BV₀
                 → ->pot-view ρθ·psn⟶₁ρθl·ql p≡ql A≡Al
                 → ->E-view   ρθ·psn⟶₁ρθr·qr p≐E⟦pin⟧ qr≐E⟦qin⟧
                 →
                  (ρ⟨ θl , Al ⟩· ql sn⟶₁ ρ⟨ θr , Ar ⟩· qr) ⊎
                  (Σ[ s ∈ Term ]
                   Σ[ θo ∈ Env.Env ]
                   Σ[ Ao ∈ Ctrl ]
                      (ρ⟨ θl , Al ⟩· ql) sn⟶₁ (ρ⟨ θo , Ao ⟩· s)
                    × (ρ⟨ θr , Ar ⟩· qr) sn⟶₁ (ρ⟨ θo , Ao ⟩· s))

ρ-pot-conf-rec {p} {θ} {ql} {θl} {.(E ⟦ qin ⟧e)} {θr} {_} {E} {(ρ⟨ .θin , Ain ⟩· .qin)} {qin} {_} {_} {A} {.A} {_} {_}
               {.(rabsence {θ} {p} {S} S∈ θS≡unknown S∉can-p-θ)} {.(rmerge {θ} {θin} p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧}
               (CBρ cbp)
               (vabsence S S∈ θS≡unknown S∉can-p-θ)
               (vmerge {.θ} {θin} {.p} {.qin} {.E})
  with Env.Sig∈ S θin
... | yes S∈Domθin
  rewrite SigMap.update-union-union S Signal.absent (Env.sig θ) (Env.sig θin) S∈ S∈Domθin
  = inj₁ (ρ⟨ θl , A ⟩· ql sn⟶₁ ρ⟨ (θl ← θin) , A-max A Ain ⟩· E ⟦ qin  ⟧e ∋ rmerge {θl} {θin} p≐E⟦pin⟧)
... | no S∉Domθin
  with Env.sig-←-irr-get {θ} {θin} {S} S∈ S∉Domθin -- θr ≡ (θ ← θin)
... | S∈Domθ←θin , θS≡⟨θ←θin⟩S
  = inj₂
    (_ , _ , A-max A Ain ,
     subst (λ { θ* → ρ⟨ θl , A ⟩· ql sn⟶₁ ρ⟨ θ* , A-max A Ain ⟩· E ⟦ qin ⟧e})
       ((Env.set-sig {S} θ S∈ Signal.absent) ← θin ≡
        Env.set-sig {S} (θ ← θin) S∈Domθ←θin Signal.absent ∋
        cong (λ sig* → Θ sig* (Env.shr (θ ← θin)) (Env.var (θ ← θin)))
          (SigMap.put-union-comm S Signal.absent (Env.sig θ) (Env.sig θin) S∉Domθin))
       (ρ⟨ θl , A ⟩· ql sn⟶₁ ρ⟨ (θl ← θin) , A-max A Ain ⟩· E ⟦ qin ⟧e ∋
        rmerge {θl} {θin} p≐E⟦pin⟧) ,′
     (ρ⟨ (θ ← θin) , A-max A Ain ⟩· E ⟦ qin ⟧e sn⟶₁ ρ⟨ (Env.set-sig {S} (θ ← θin) S∈Domθ←θin Signal.absent) , A-max A Ain ⟩· E ⟦ qin ⟧e ∋
      (rabsence {θr} {_} {S} S∈Domθ←θin (trans (sym θS≡⟨θ←θin⟩S) θS≡unknown)
        (λ S∈can-E⟦qin⟧-θ←θin →
          S∉can-p-θ
            (canθₛ-mergeˡ (Env.sig θ) Env.[]env cbp p≐E⟦pin⟧
              S S∉Domθin S∈can-E⟦qin⟧-θ←θin)))))

ρ-pot-conf-rec {p} {θ} {ql} {θl} {.(E ⟦ qin ⟧e)} {θr} {_} {E} {(ρ⟨ .θin , Ain ⟩· qin)} {qin} {_} {_} {A} {Al} {Ar} {_}
               {.(rreadyness {θ} {p} {s} s∈ θs≡old⊎θs≡new s∉can-p-θ)} {.(rmerge p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧}
               (CBρ cbp)
               (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
               (vmerge {.θ} {θin} {.p} {.qin} {.E})
  with Env.Shr∈ s θin
... | yes s∈Domθin
  rewrite ShrMap.update-union-union s (SharedVar.ready , Env.shr-vals {s} θ s∈) (Env.shr θ) (Env.shr θin) s∈ s∈Domθin
  = inj₁ (rmerge {θl} {θin} p≐E⟦pin⟧)
... | no s∉Domθin
  with Env.shr-←-irr-get {θ} {θin} {s} s∈ s∉Domθin
... | s∈Domθ←θin , θs≡⟨θ←θin⟩s
  = inj₂
    (_ , _ , _ ,
     subst (λ { θ* → ρ⟨ θl , A ⟩· ql sn⟶₁ ρ⟨ θ* , A-max A Ain ⟩· E ⟦ qin ⟧e })
       (cong (λ shr* → Θ (Env.sig (θ ← θin)) shr* (Env.var (θ ← θin)))
         (trans
           (cong (λ shrval* →
                   ShrMap.union
                     (ShrMap.update (Env.shr θ) s (SharedVar.ready , proj₂ shrval*))
                     (Env.shr θin))
             (ShrMap.U-∉-irr-get-help-m {_} {Env.shr θ} {Env.shr θin} {s}
                                        s∈ s∉Domθin s∈Domθ←θin ))
           (ShrMap.put-union-comm s (SharedVar.ready , Env.shr-vals {s} (θ ← θin) s∈Domθ←θin)
                                  (Env.shr θ) (Env.shr θin) s∉Domθin)))
       (rmerge {θl} {θin} p≐E⟦pin⟧) ,′
     rreadyness {θr} {_} {s} s∈Domθ←θin
       (Data.Sum.map (trans (sym θs≡⟨θ←θin⟩s)) (trans (sym θs≡⟨θ←θin⟩s))
                     θs≡old⊎θs≡new)
       (λ s∈can-E⟦qin⟧-θ←θin →
         s∉can-p-θ
           (canθₛₕ-mergeˡ (Env.sig θ) Env.[]env cbp p≐E⟦pin⟧
             s s∉Domθin s∈can-E⟦qin⟧-θ←θin)))

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ qin ⟧e)} {.θ} {_} {E}
               {.(present _ ∣⇒ qin ∣⇒ _)} {qin} {_} {_} {_} {_} {_} {_}
               {.(rabsence {θ} {p} {S} S∈ θS≡unknown S∉can-p-θ)}
               {.(ris-present {θ} {S'} S'∈ θS'≡present p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧}
               (CBρ cbp)
               (vabsence S S∈ θS≡unknown S∉can-p-θ)
               (vis-present {.θ} {S'} {S∈ = S'∈} {θS'≡present} {.p≐E⟦pin⟧})
  with S' Signal.≟ S
... | yes refl =
  ((Signal.unknown ≡ Signal.present → _) ∋ λ ())
  (trans (trans (sym θS≡unknown) (Env.sig-stats-∈-irr {S} {θ} S∈ S'∈)) θS'≡present)
... | no S'≠S =
  inj₂
  (_ , _ , _ ,
   ris-present {θl} {S'}
     (Env.sig-set-mono' {S'} {S} {θ} {_} {S∈} S'∈)
     (Env.sig-putputget {S'} {S} {θ} S'≠S S'∈ S∈ _ θS'≡present)
     p≐E⟦pin⟧ ,′
   rabsence {θ} {_} {S} S∈ θS≡unknown
     (λ S∈can-E⟦qin⟧-θ →
      S∉can-p-θ
       (subst (Signal.unwrap S ∈_)
         (cong proj₁ (sym (canθ-is-present (Env.sig θ) S'∈ Env.[]env p≐E⟦pin⟧ θS'≡present)) )
         S∈can-E⟦qin⟧-θ)))

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ qin ⟧e)} {.θ} {_} {E}
               {.(present _ ∣⇒ _ ∣⇒ qin)} {qin} {_} {_} {_} {_} {_} {_}
               {.(rabsence {θ} {p} {S} S∈ θS≡unknown S∉can-p-θ)}
               {.(ris-absent {θ} {S'} S'∈ θS'≡absent p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧}
               (CBρ cbp)
               (vabsence S S∈ θS≡unknown S∉can-p-θ)
               (vis-absent {.θ} {S'} {S∈ = S'∈} {θS'≡absent} {.p≐E⟦pin⟧})
  with S' Signal.≟ S
... | yes refl =
  ((Signal.unknown ≡ Signal.absent → _) ∋ λ ())
  (trans (trans (sym θS≡unknown) (Env.sig-stats-∈-irr {S} {θ} S∈ S'∈)) θS'≡absent)
... | no S'≠S =
  inj₂
  (_ , _ , _ ,
   ris-absent {θl} {S'}
     (Env.sig-set-mono' {S'} {S} {θ} {_} {S∈} S'∈)
     (Env.sig-putputget {S'} {S} {θ} S'≠S S'∈ S∈ _ θS'≡absent)
     p≐E⟦pin⟧ ,′
   rabsence {θ} {_} {S} S∈ θS≡unknown
     (λ S∈can-E⟦qin⟧-θ →
      S∉can-p-θ
       (subst (Signal.unwrap S ∈_)
         (cong proj₁ (sym (canθ-is-absent (Env.sig θ) S'∈ Env.[]env p≐E⟦pin⟧ θS'≡absent)))
         S∈can-E⟦qin⟧-θ)))

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ qin ⟧e)} {.θ} {_} {E}
               {.(present _ ∣⇒ qin ∣⇒ _)} {qin} {_} {_} {_} {_} {_} {_}
               {.(rreadyness {θ} {p} {s} s∈ θs≡old⊎θs≡new s∉can-p-θ)}
               {.(ris-present {θ} {S'} S'∈ θS'≡present p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧}
               (CBρ cbp)
               (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
               (vis-present {.θ} {S'} {S∈ = S'∈} {θS'≡present} {.p≐E⟦pin⟧}) =
  inj₂
  (_ , _ , _ ,
   ris-present {θl} {S'} S'∈ θS'≡present p≐E⟦pin⟧ ,′
   rreadyness {θ} {_} {s} s∈ θs≡old⊎θs≡new
     (λ s∈can-E⟦qin⟧-θ →
       s∉can-p-θ
         (subst (SharedVar.unwrap s ∈_)
           (cong (proj₂ ∘ proj₂)
             (sym (canθ-is-present (Env.sig θ) S'∈ Env.[]env p≐E⟦pin⟧ θS'≡present)))
           s∈can-E⟦qin⟧-θ)))

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ qin ⟧e)} {.θ} {_} {E}
               {.(present _ ∣⇒ _ ∣⇒ qin)} {qin} {_} {_} {_} {_} {_} {_}
               {.(rreadyness {θ} {p} {s} s∈ θs≡old⊎θs≡new s∉can-p-θ)}
               {.(ris-absent {θ} {S'} S'∈ θS'≡absent p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧}
               (CBρ cbp)
               (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
               (vis-absent {.θ} {S'} {S∈ = S'∈} {θS'≡absent} {.p≐E⟦pin⟧}) =
  inj₂
  (_ , _ , _ ,
   ris-absent {θl} {S'} S'∈ θS'≡absent p≐E⟦pin⟧ ,′
   rreadyness {θ} {_} {s} s∈ θs≡old⊎θs≡new
     (λ s∈can-E⟦qin⟧-θ →
       s∉can-p-θ
         (subst (SharedVar.unwrap s ∈_)
           (cong (proj₂ ∘ proj₂)
             (sym (canθ-is-absent (Env.sig θ) S'∈ Env.[]env p≐E⟦pin⟧ θS'≡absent)))
           s∈can-E⟦qin⟧-θ)))

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ nothin ⟧e)} {θr} {_} {E}
               {.(emit S')} {.nothin} {_} {_} {_} {_} {_} {_}
               {.(rreadyness {θ} {p} {s} s∈ θs≡old⊎θs≡new s∉can-p-θ)}
               {.(remit {θ} {p} {S'} S'∈ θS'≢absent p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧}
               (CBρ cbp)
               (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
               (vemit {.θ} {.p} {S'} {.E} {S'∈} {θS'≢absent} {.p≐E⟦pin⟧}) =
  inj₂
  (_ , _ , _ ,
   remit {θl} {_} {S'} S'∈ θS'≢absent p≐E⟦pin⟧ ,′
   rreadyness {θr} {_} {s} s∈ θs≡old⊎θs≡new
     (λ s∈can-E⟦nothin⟧-θr →
       s∉can-p-θ
         (canθₛₕ-emit θ S'∈ Env.[]env p≐E⟦pin⟧
           θS'≢absent
           (canθₛ-membership (Env.sig θ) 0 p Env.[]env S'
             (λ θ* → canₛ-capture-emit-signal θ* p≐E⟦pin⟧))
           s s∈can-E⟦nothin⟧-θr)))

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ nothin ⟧e)} {θr} {_} {E}
               {.(emit S')} {.nothin} {_} {_} {A} {Al} {Ar} {_}
               {.(rabsence {θ} {p} {S} S∈ θS≡unknown S∉can-p-θ)}
               {.(remit {θ} {p} {S'} S'∈ θS'≢absent p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧}
               (CBρ cbp)
               (vabsence S S∈ θS≡unknown S∉can-p-θ)
               (vemit {.θ} {.p} {S'} {.E} {S'∈} {θS'≢absent} {.p≐E⟦pin⟧})
  with S' Signal.≟ S
... | yes refl =
  ⊥-elim
    (S∉can-p-θ
      (canθₛ-membership (Env.sig θ) 0 p Env.[]env S'
        (λ θ* → canₛ-capture-emit-signal θ* p≐E⟦pin⟧)))
... | no S'≢S =
  inj₂
  (_ , _ , _ ,
   remit {θl} {_} {S'}
     (SigMap.insert-mono {_} {S'} {Env.sig θ} {S} {Signal.absent} S'∈)
     (θS'≢absent ∘
      trans
        (sym (SigMap.putputget {_} {Env.sig θ} {S'} {S}
               {_} {Signal.absent} S'≢S S'∈ S'∈Domθl refl)))
     p≐E⟦pin⟧ ,′
   subst (λ sig* → ρ⟨ θr , Ar ⟩· E ⟦ nothin ⟧e sn⟶₁ ρ⟨ (Θ sig* (Env.shr θ) (Env.var θ)) , Ar ⟩· E ⟦ nothin ⟧e)
     (SigMap.put-comm {_} {Env.sig θ} {_} {_} {Signal.present} {Signal.absent} S'≢S)
     (rabsence {θr} {_} {S}
       S∈Domθr
       (SigMap.putputget {_} {Env.sig θ} {S} {S'} {_} {Signal.present}
        (S'≢S ∘ sym) S∈ S∈Domθr θS≡unknown)
       (λ S''∈can-E⟦nothin⟧-θr →
         S∉can-p-θ
           (canθₛ-emit θ S'∈ Env.[]env p≐E⟦pin⟧
             θS'≢absent
             (canθₛ-membership (Env.sig θ) 0 p Env.[]env S'
               (λ θ* → canₛ-capture-emit-signal θ* p≐E⟦pin⟧))
             S S''∈can-E⟦nothin⟧-θr))))
  where S∈Domθr = SigMap.insert-mono {_} {S} {Env.sig θ} {S'} {Signal.present} S∈
        S'∈Domθl = SigMap.insert-mono {_} {S'} {Env.sig θ} {S} {Signal.absent} S'∈

ρ-pot-conf-rec {p} {θ} {.p} {θl}
               {.(E ⟦ ρ⟨ (Θ SigMap.empty ShrMap.[ s' ↦ (SharedVar.old , δ e') ] VarMap.empty) , WAIT ⟩· p' ⟧e)}
               {.θ} {_} {E}
               {.(shared s' ≔ e in: p')}
               {.(ρ⟨ (Θ SigMap.empty ShrMap.[ s' ↦ (SharedVar.old , δ e') ] VarMap.empty) , WAIT ⟩· p')}
               {_} {_} {A} {Al} {Ar} {_}
               {.(rabsence {θ} {p} {S} S∈ θS≡unknown S∉can-p-θ)}
               {.(rraise-shared e' p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧} (CBρ cbp)
               (vabsence S S∈ θS≡unknown S∉can-p-θ)
               (vraise-shared {.θ} {.p} {s'} {e} {p'} {.E} {e'} {.p≐E⟦pin⟧})
  with ready-maint/irr S S∈ Signal.absent e'
... | e'' , δe'≡δe'' =
  inj₂
  (_ , _ , _ ,
   subst (λ δe* →
           (ρ⟨ θl , Al ⟩· p) sn⟶₁
           (ρ⟨ θl , Al ⟩· E ⟦ ρ⟨ ([s,δe]-env s' δe*) , WAIT ⟩· p' ⟧e))
     (sym δe'≡δe'')
     (rraise-shared e'' p≐E⟦pin⟧) ,′
   rabsence {θ} {_} {S} S∈ θS≡unknown
     (λ S∈can-E⟦ρΘp'⟧-θ →
       S∉can-p-θ
         (canθₛ-subset (Env.sig θ) 0 (E ⟦ ρ⟨ ([s,δe]-env s' (δ e')) , WAIT ⟩· p' ⟧e) p Env.[]env
           (λ θ* S* → canₛ-raise θ* (tshared (δ e') s' e p') p≐E⟦pin⟧ S*)
           S S∈can-E⟦ρΘp'⟧-θ)))

ρ-pot-conf-rec {p} {θ} {.p} {θl}
               {.(E ⟦ ρ⟨ (Θ SigMap.empty ShrMap.[ s' ↦ (SharedVar.old , δ e') ] VarMap.empty) , WAIT ⟩· p' ⟧e)}
               {.θ} {_} {E}
               {.(shared s' ≔ e in: p')}
               {.(ρ⟨ (Θ SigMap.empty ShrMap.[ s' ↦ (SharedVar.old , δ e') ] VarMap.empty) , WAIT ⟩· p')}
               {_} {_} {A} {Al} {Ar} {_}
               {.(rreadyness {θ} {p} {s} s∈ θs≡old⊎θs≡new s∉can-p-θ)}
               {.(rraise-shared e' p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧} (CBρ cbp)
               (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
               (vraise-shared {.θ} {.p} {s'} {e} {p'} {.E} {e'} {.p≐E⟦pin⟧})
  with ready-irr-on-irr-s/ready {θ} {e} s (Env.shr-vals {s} θ s∈) s∈ (θs≢ready θs≡old⊎θs≡new)
         e'
  where θs≢ready : typeof θs≡old⊎θs≡new → ¬ (Env.shr-stats {s} θ s∈ ≡ SharedVar.ready)
        θs≢ready (inj₁ θs≡old) θs≡ready with trans (sym θs≡old) θs≡ready
        ... | ()
        θs≢ready (inj₂ θs≡new) θs≡ready with trans (sym θs≡new) θs≡ready
        ... | ()
... | e'' , δe'≡δe'' =
  inj₂
  (_ , _ , _ ,
   subst (λ δe* →
           (ρ⟨ θl , Al ⟩· p) sn⟶₁
           (ρ⟨ θl , Al ⟩· E ⟦ ρ⟨ ([s,δe]-env s' δe*) , WAIT ⟩· p' ⟧e))
     (sym δe'≡δe'')
     (rraise-shared e'' p≐E⟦pin⟧) ,′
   rreadyness {θ} {_} {s} s∈ θs≡old⊎θs≡new
     (λ s∈can-E⟦ρΘp'⟧-θ →
       s∉can-p-θ
         (canθₛₕ-subset (Env.sig θ) 0
           (E ⟦ ρ⟨ ([s,δe]-env s' (δ e')) , WAIT ⟩· p' ⟧e) p Env.[]env
           (λ θ* S* → canₛ-raise θ* (tshared (δ e') s' e p') p≐E⟦pin⟧ S*)
           (λ θ* s* → canₛₕ-raise θ* (tshared (δ e') s' e p') p≐E⟦pin⟧ s*)
           s s∈can-E⟦ρΘp'⟧-θ)))

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ nothin ⟧e)} {θr} {_} {E}
               {.(s' ⇐ e)} {.nothin} {_} {_} {GO} {GO} {GO} {_}
               {.(rabsence {θ} {p} {S} S∈ θS≡unknown S∉can-p-θ)}
               {.(rset-shared-value-old {θ} {p} {s'} e' s'∈ θs'≡old p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧} (CBρ cbp)
               (vabsence S S∈ θS≡unknown S∉can-p-θ)
               (vset-shared-value-old {.θ} {.p} {s'} {e} {.E} {e'} {s'∈} {θs'≡old})
  with ready-maint/irr S S∈ Signal.absent e'
... | e'' , δe'≡δe'' =
  inj₂
  (_ , _ , _ ,
   subst (λ δe* →
            ρ⟨ θl , GO ⟩· p sn⟶₁
            ρ⟨ (θl-set-shr δe*) , GO ⟩· E ⟦ nothin ⟧e)
     (sym δe'≡δe'')
     (rset-shared-value-old {θl} {_} {s'} e'' s'∈ θs'≡old p≐E⟦pin⟧) ,′
   rabsence {θr} {_} {S} S∈ θS≡unknown
     (λ S∈can-E⟦nothin⟧-θr →
       S∉can-p-θ
         (canθₛ-subset (Env.sig θ) 0 (E ⟦ nothin ⟧e) p Env.[]env
           (λ θ* S* → canₛ-term-nothin θ* θ* refl (tset-shr s' e) p≐E⟦pin⟧ S*)
           S S∈can-E⟦nothin⟧-θr)))
  where
    θl-set-shr : ℕ → Env
    θl-set-shr n = Env.set-shr {s'} θl s'∈ SharedVar.new n

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ nothin ⟧e)} {θr} {_} {E}
               {.(s' ⇐ e)} {.nothin} {_} {_} {GO} {GO} {GO} {_}
               {.(rreadyness {θ} {p} {s} s∈ θs≡old⊎θs≡new s∉can-p-θ)}
               {.(rset-shared-value-old {θ} {p} {s'} e' s'∈ θs'≡old p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧} (CBρ cbp)
               (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
               (vset-shared-value-old {.θ} {.p} {s'} {e} {.E} {e'} {s'∈} {θs'≡old})
  with s SharedVar.≟ s'
... | yes refl =
  ⊥-elim
    (s∉can-p-θ
      (canθₛₕ-membership (Env.sig θ) 0 p Env.[]env s
        (λ θ* → canₛₕ-capture-set-shared θ* p≐E⟦pin⟧)))
... | no  s≢s'
  with ready-irr-on-irr-s/ready {θ} {e} s (Env.shr-vals {s} θ s∈) s∈ (θs≢ready θs≡old⊎θs≡new)
         e'
  where θs≢ready : typeof θs≡old⊎θs≡new → ¬ (Env.shr-stats {s} θ s∈ ≡ SharedVar.ready)
        θs≢ready (inj₁ θs≡old) θs≡ready with trans (sym θs≡old) θs≡ready
        ... | ()
        θs≢ready (inj₂ θs≡new) θs≡ready with trans (sym θs≡new) θs≡ready
        ... | ()
... | e'' , δe'≡δe'' =
  inj₂
  (_ , _ , _ ,
   subst (λ shr* →
           ρ⟨ θl , GO ⟩· p sn⟶₁
           ρ⟨ (Θ (Env.sig θl) shr* (Env.var θl)) , GO ⟩·
             E ⟦ nothin ⟧e)
   (cong Env.shr
     (begin
       Env.set-shr {s'} θl s'∈Domθl SharedVar.new (δ e'')
         ≡⟨ cong (Env.set-shr {s'} θl s'∈Domθl SharedVar.new) (sym δe'≡δe'') ⟩
       Env.set-shr {s'} θl s'∈Domθl SharedVar.new (δ e')
         ≡⟨ cong (λ sig* → Θ (Env.sig θ) sig* (Env.var θ))
              (ShrMap.put-comm {_} {Env.shr θ} {_} {_}
                {SharedVar.ready ,′ θs}
                {SharedVar.new ,′ δ e'}
                s≢s') ⟩
       Env.set-shr {s} θr s∈Domθr SharedVar.ready θs
         ≡⟨ cong (Env.set-shr {s} θr s∈Domθr SharedVar.ready ∘ proj₂) (sym θrs≡θs) ⟩
       Env.set-shr {s} θr s∈Domθr SharedVar.ready
         (Env.shr-vals {s} θr s∈Domθr)                  ∎))
   (rset-shared-value-old {θl} {_} {s'} e'' s'∈Domθl
     (trans (cong proj₁ θls'≡θs') θs'≡old) p≐E⟦pin⟧) ,′
   rreadyness {θr} {_} {s} s∈Domθr
     (Data.Sum.map (trans (cong proj₁ θrs≡θs)) (trans (cong proj₁ θrs≡θs))
       θs≡old⊎θs≡new)
     (λ s∈can-E⟦nothin⟧-θr →
       s∉can-p-θ
         (canθₛₕ-subset (Env.sig θ) 0 (E ⟦ nothin ⟧e) p Env.[]env
           (λ θ* S* → canₛ-term-nothin θ* θ* refl (tset-shr s' e) p≐E⟦pin⟧ S*)
           (λ θ* s* → canₛₕ-term-nothin θ* θ* refl (tset-shr s' e) p≐E⟦pin⟧ s*)
           s s∈can-E⟦nothin⟧-θr)))
  where
    θs = Env.shr-vals {s} θ s∈
    s∈Domθr = Env.shr-set-mono' {s} {s'} {θ} {SharedVar.new} {δ e'} {s'∈} s∈
    θrs≡θs = ShrMap.putputget {_} {Env.shr θ} {_} {_} {_} {SharedVar.new ,′ δ e'}
               s≢s' s∈ s∈Domθr refl
    s'∈Domθl = Env.shr-set-mono' {s'} {s} {θ} {SharedVar.ready} {θs} {s∈} s'∈
    θls'≡θs' = ShrMap.putputget {_} {Env.shr θ} {_} {_} {_} {SharedVar.ready ,′ θs}
                (s≢s' ∘ sym) s'∈ s'∈Domθl refl

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ nothin ⟧e)} {θr} {_} {E}
               {.(s' ⇐ e)} {.nothin} {_} {_} {GO} {GO} {GO} {_}
               {.(rabsence {θ} {p} {S} S∈ θS≡unknown S∉can-p-θ)}
               {.(rset-shared-value-new {θ} {p} {s'} e' s'∈ θs'≡new p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧} (CBρ cbp)
               (vabsence S S∈ θS≡unknown S∉can-p-θ)
               (vset-shared-value-new {.θ} {.p} {s'} {e} {.E} {e'} {s'∈} {θs'≡new})
  with ready-maint/irr S S∈ Signal.absent e'
... | e'' , δe'≡δe'' =
  inj₂
  (_ , _ , _ ,
   subst (λ δe* →
            ρ⟨ θl , GO ⟩· p sn⟶₁
            ρ⟨ (θl-set-shr δe*) , GO ⟩· E ⟦ nothin ⟧e)
     (cong
       (Env.shr-vals {s'} θ s'∈ +_)
       (sym δe'≡δe''))
     (rset-shared-value-new {θl} {_} {s'} e'' s'∈ θs'≡new p≐E⟦pin⟧) ,′
   rabsence {θr} {_} {S} S∈ θS≡unknown
     (λ S∈can-E⟦nothin⟧-θr →
       S∉can-p-θ
         (canθₛ-subset (Env.sig θ) 0 (E ⟦ nothin ⟧e) p Env.[]env
           (λ θ* S* → canₛ-term-nothin θ* θ* refl (tset-shr s' e) p≐E⟦pin⟧ S*)
           S S∈can-E⟦nothin⟧-θr)))
  where
    θl-set-shr : ℕ → Env
    θl-set-shr n = Env.set-shr {s'} θl s'∈ SharedVar.new n

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ nothin ⟧e)} {θr} {_} {E}
               {.(s' ⇐ e)} {.nothin} {_} {_} {GO} {GO} {GO} {_}
               {.(rreadyness {θ} {p} {s} s∈ θs≡old⊎θs≡new s∉can-p-θ)}
               {.(rset-shared-value-new {θ} {p} {s'} e' s'∈ θs'≡new p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧} (CBρ cbp)
               (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
               (vset-shared-value-new {.θ} {.p} {s'} {e} {.E} {e'} {s'∈} {θs'≡new})
  with s SharedVar.≟ s'
... | yes refl =
  ⊥-elim
    (s∉can-p-θ
      (canθₛₕ-membership (Env.sig θ) 0 p Env.[]env s
        (λ θ* → canₛₕ-capture-set-shared θ* p≐E⟦pin⟧)))
... | no  s≢s'
  with ready-irr-on-irr-s/ready {θ} {e} s (Env.shr-vals {s} θ s∈) s∈ (θs≢ready θs≡old⊎θs≡new)
         e'
  where θs≢ready : typeof θs≡old⊎θs≡new → ¬ (Env.shr-stats {s} θ s∈ ≡ SharedVar.ready)
        θs≢ready (inj₁ θs≡old) θs≡ready with trans (sym θs≡old) θs≡ready
        ... | ()
        θs≢ready (inj₂ θs≡new) θs≡ready with trans (sym θs≡new) θs≡ready
        ... | ()
... | e'' , δe'≡δe'' =
  inj₂
  (_ , _ , _ ,
   subst (λ shr* →
           ρ⟨ θl , GO ⟩· p sn⟶₁
           ρ⟨ (Θ (Env.sig θl) shr* (Env.var θl)) , GO ⟩·
             E ⟦ nothin ⟧e)
   (cong Env.shr
     (begin
       Env.set-shr {s'} θl s'∈Domθl SharedVar.new (Env.shr-vals {s'} θl s'∈Domθl + δ e'')
         ≡⟨ cong
             (λ v* → Env.set-shr {s'} θl s'∈Domθl SharedVar.new (v* + δ e''))
             (cong proj₂ θls'≡θs') ⟩
       Env.set-shr {s'} θl s'∈Domθl SharedVar.new (θs' + δ e'')
         ≡⟨ cong (λ v* → Env.set-shr {s'} θl s'∈Domθl SharedVar.new
                   (θs' + v*))
                   (sym δe'≡δe'') ⟩
       Env.set-shr {s'} θl s'∈Domθl SharedVar.new (θs' + δ e')
         ≡⟨ cong (λ sig* → Θ (Env.sig θ) sig* (Env.var θ))
              (ShrMap.put-comm {_} {Env.shr θ} {_} {_}
                {SharedVar.ready ,′ θs}
                {SharedVar.new ,′ θs' + δ e'}
                s≢s') ⟩
       Env.set-shr {s} θr s∈Domθr SharedVar.ready θs
         ≡⟨ cong (Env.set-shr {s} θr s∈Domθr SharedVar.ready ∘ proj₂) (sym θrs≡θs) ⟩
       Env.set-shr {s} θr s∈Domθr SharedVar.ready
         (Env.shr-vals {s} θr s∈Domθr)                  ∎))
   (rset-shared-value-new {θl} {_} {s'} e'' s'∈Domθl
     (trans (cong proj₁ θls'≡θs') θs'≡new) p≐E⟦pin⟧) ,′
   rreadyness {θr} {_} {s} s∈Domθr
     (Data.Sum.map (trans (cong proj₁ θrs≡θs)) (trans (cong proj₁ θrs≡θs))
       θs≡old⊎θs≡new)
     (λ s∈can-E⟦nothin⟧-θr →
       s∉can-p-θ
         (canθₛₕ-subset (Env.sig θ) 0 (E ⟦ nothin ⟧e) p Env.[]env
           (λ θ* S* → canₛ-term-nothin θ* θ* refl (tset-shr s' e) p≐E⟦pin⟧ S*)
           (λ θ* s* → canₛₕ-term-nothin θ* θ* refl (tset-shr s' e) p≐E⟦pin⟧ s*)
           s s∈can-E⟦nothin⟧-θr)))
  where
    θs' = Env.shr-vals {s'} θ s'∈
    θs = Env.shr-vals {s} θ s∈
    s∈Domθr = Env.shr-set-mono' {s} {s'} {θ} {SharedVar.new} {θs' + δ e'} {s'∈} s∈
    θrs≡θs = ShrMap.putputget {_} {Env.shr θ} {_} {_} {_} {SharedVar.new ,′ θs' + δ e'}
               s≢s' s∈ s∈Domθr refl
    s'∈Domθl = Env.shr-set-mono' {s'} {s} {θ} {SharedVar.ready} {θs} {s∈} s'∈
    θls'≡θs' = ShrMap.putputget {_} {Env.shr θ} {_} {_} {_} {SharedVar.ready ,′ θs}
                (s≢s' ∘ sym) s'∈ s'∈Domθl refl

ρ-pot-conf-rec {p} {θ} {.p} {θl}
               {.(E ⟦ ρ⟨ (Θ SigMap.empty ShrMap.empty VarMap.[ x ↦ δ e' ]) , WAIT ⟩· p' ⟧e)}
               {.θ} {_} {E}
               {.(var x ≔ e in: p')}
               {.(ρ⟨ (Θ SigMap.empty ShrMap.empty VarMap.[ x ↦ δ e' ]) , WAIT ⟩· p')}
               {_} {_} {A} {.A} {.A} {_}
               {.(rabsence {θ} {p} {S} S∈ θS≡unknown S∉can-p-θ)}
               {.(rraise-var {θ} {p} {x} {p'} {e} e' p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧} (CBρ cbp)
               (vabsence S S∈ θS≡unknown S∉can-p-θ)
               (vraise-var {.θ} {.p} {x} {p'} {e} {.E} {e'} {.p≐E⟦pin⟧})
  with ready-maint/irr S S∈ Signal.absent e'
... | e'' , δe'≡δe'' =
  inj₂
  (_ , _ , _ ,
   subst (λ δe* →
           (ρ⟨ θl , A ⟩· p) sn⟶₁
           (ρ⟨ θl , A ⟩· E ⟦ ρ⟨ ([x,δe]-env x δe*) , WAIT ⟩· p' ⟧e))
    (sym δe'≡δe'')
    (rraise-var {θl} {_} {x} {p'} {e} e'' p≐E⟦pin⟧) ,′
   rabsence {θ} {_} {S} S∈ θS≡unknown
     (λ S∈can-E⟦ρΘp'⟧-θ →
       S∉can-p-θ
         (canθₛ-subset (Env.sig θ) 0 (E ⟦ ρ⟨ [x,δe]-env x (δ e') , WAIT ⟩· p' ⟧e) p Env.[]env
           (λ θ* S* → canₛ-raise θ* (tvar (δ e') x e p') p≐E⟦pin⟧ S*)
           S S∈can-E⟦ρΘp'⟧-θ)))

ρ-pot-conf-rec {p} {θ} {.p} {θl}
               {.(E ⟦ ρ⟨ (Θ SigMap.empty ShrMap.empty VarMap.[ x ↦ δ e' ]) , WAIT ⟩· p' ⟧e)}
               {.θ} {_} {E}
               {.(var x ≔ e in: p')}
               {.(ρ⟨ (Θ SigMap.empty ShrMap.empty VarMap.[ x ↦ δ e' ]) , WAIT ⟩· p')}
               {_} {_} {A} {.A} {.A} {_}
               {.(rreadyness {θ} {p} {s} s∈ θs≡old⊎θs≡new s∉can-p-θ)}
               {.(rraise-var {θ} {p} {x} {p'} {e} e' p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧} (CBρ cbp)
               (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
               (vraise-var {.θ} {.p} {x} {p'} {e} {.E} {e'} {.p≐E⟦pin⟧})
  with ready-irr-on-irr-s/ready {θ} {e} s (Env.shr-vals {s} θ s∈) s∈ (θs≢ready θs≡old⊎θs≡new)
         e'
  where θs≢ready : typeof θs≡old⊎θs≡new → ¬ (Env.shr-stats {s} θ s∈ ≡ SharedVar.ready)
        θs≢ready (inj₁ θs≡old) θs≡ready with trans (sym θs≡old) θs≡ready
        ... | ()
        θs≢ready (inj₂ θs≡new) θs≡ready with trans (sym θs≡new) θs≡ready
        ... | ()
... | e'' , δe'≡δe'' =
  inj₂
  (_ , _ , _ ,
   subst (λ δe* →
           (ρ⟨ θl , A ⟩· p) sn⟶₁
           (ρ⟨ θl , A ⟩· E ⟦ ρ⟨ ([x,δe]-env x δe*) , WAIT ⟩· p' ⟧e))
    (sym δe'≡δe'')
    (rraise-var {θl} {_} {x} {p'} {e} e'' p≐E⟦pin⟧) ,′
   rreadyness {θ} {_} {s} s∈ θs≡old⊎θs≡new
     (λ s∈can-E⟦ρΘp'⟧-θ →
       s∉can-p-θ
         (canθₛₕ-subset (Env.sig θ) 0 (E ⟦ ρ⟨ [x,δe]-env x (δ e') , WAIT ⟩· p' ⟧e) p Env.[]env
           (λ θ* S* → canₛ-raise θ* (tvar (δ e') x e p') p≐E⟦pin⟧ S*)
           (λ θ* s* → canₛₕ-raise θ* (tvar (δ e') x e p') p≐E⟦pin⟧ s*)
           s s∈can-E⟦ρΘp'⟧-θ)))

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ nothin ⟧e)} {θr}
               {_} {E} {.(x ≔ e)} {.nothin} {_} {_} {A} {.A} {.A} {_}
               {.(rabsence {θ} {p} {S} S∈ θS≡unknown S∉can-p-θ)}
               {.(rset-var {θ} {p} {x} {e} x∈ e' p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧} (CBρ cbp)
               (vabsence S S∈ θS≡unknown S∉can-p-θ)
               (vset-var {.θ} {.p} {x} {e} {.E} {x∈} {e'} {.p≐E⟦pin⟧})
  with ready-maint/irr S S∈ Signal.absent e'
... | e'' , δe'≡δe'' =
  inj₂
  (_ , _ , _ ,
   subst (λ δe* →
            ρ⟨ θl , A ⟩· p sn⟶₁
            ρ⟨ (θl-set-var δe*) , A ⟩· E ⟦ nothin ⟧e)
     (sym δe'≡δe'')
   (rset-var {θl} {_} {x} {e} x∈ e'' p≐E⟦pin⟧) ,′
   rabsence {θr} {_} {S} S∈ θS≡unknown
     (λ S∈can-E⟦nothin⟧-θ' →
       S∉can-p-θ
         (canθₛ-subset (Env.sig θ) 0 (E ⟦ nothin ⟧e) p Env.[]env
           (λ θ* S* → canₛ-term-nothin θ* θ* refl (tset-var x e) p≐E⟦pin⟧ S*)
           S S∈can-E⟦nothin⟧-θ')))
  where
    θl-set-var : ℕ → Env
    θl-set-var n = Env.set-var {x} θl x∈ n

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ nothin ⟧e)} {θr}
               {_} {E} {.(x ≔ e)} {.nothin} {_} {_} {A} {.A} {.A} {_}
               {.(rreadyness {θ} {p} {s} s∈ θs≡old⊎θs≡new s∉can-p-θ)}
               {.(rset-var {θ} {p} {x} {e} x∈ e' p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧} (CBρ cbp)
               (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
               (vset-var {.θ} {.p} {x} {e} {.E} {x∈} {e'} {.p≐E⟦pin⟧})
  with ready-irr-on-irr-s/ready {θ} {e} s (Env.shr-vals {s} θ s∈) s∈ (θs≢ready θs≡old⊎θs≡new)
         e'
  where θs≢ready : typeof θs≡old⊎θs≡new → ¬ (Env.shr-stats {s} θ s∈ ≡ SharedVar.ready)
        θs≢ready (inj₁ θs≡old) θs≡ready with trans (sym θs≡old) θs≡ready
        ... | ()
        θs≢ready (inj₂ θs≡new) θs≡ready with trans (sym θs≡new) θs≡ready
        ... | ()
... | e'' , δe'≡δe'' =
  inj₂
  (_ , _ , _ ,
   subst (λ δe* →
            ρ⟨ θl , A ⟩· p sn⟶₁
            ρ⟨ (θl-set-var δe*) , A ⟩· E ⟦ nothin ⟧e)
     (sym δe'≡δe'')
   (rset-var {θl} {_} {x} {e} x∈ e'' p≐E⟦pin⟧) ,′
   rreadyness {θr} {_} {s} s∈ θs≡old⊎θs≡new
     (λ s∈can-E⟦nothin⟧-θ' →
       s∉can-p-θ
         (canθₛₕ-subset (Env.sig θ) 0 (E ⟦ nothin ⟧e) p Env.[]env
           (λ θ* S* → canₛ-term-nothin θ* θ* refl (tset-var x e) p≐E⟦pin⟧ S*)
           (λ θ* s* → canₛₕ-term-nothin θ* θ* refl (tset-var x e) p≐E⟦pin⟧ s*)
           s s∈can-E⟦nothin⟧-θ')))
  where
    θl-set-var : ℕ → Env
    θl-set-var n = Env.set-var {x} θl x∈ n

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ qin ⟧e)} {.θ} {_} {E}
               {.(if x ∣⇒ th ∣⇒ qin)} {qin} {_} {_}  {_} {_} {_} {_}
               {.(rabsence {θ} {p} {S} S∈ θS≡unknown S∉can-p-θ)}
               {.(rif-false {x = x} x∈ θx≡zero p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧} (CBρ cbp)
               (vabsence S S∈ θS≡unknown S∉can-p-θ)
               (vif-false {.θ} {.p} {th} {.qin} {x} {.E} {x∈} {θx≡zero} {.p≐E⟦pin⟧}) =
  inj₂
  (_ , _ , _ ,
   rif-false {x = x} x∈ θx≡zero p≐E⟦pin⟧ ,′
   rabsence {θ} {_} {S} S∈ θS≡unknown
     (λ S∈can-E⟦qin⟧ →
       S∉can-p-θ
         (canθₛ-subset (Env.sig θ) 0 (E ⟦ qin ⟧e) p Env.[]env
           (λ θ* S* → canₛ-if-false θ* p≐E⟦pin⟧ S*)
           S S∈can-E⟦qin⟧)))

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ qin ⟧e)} {.θ} {_} {E}
               {.(if x ∣⇒ th ∣⇒ qin)} {qin} {_} {_} {_} {_} {_} {_}
               {.(rreadyness {θ} {p} {s} s∈ θs≡old⊎θs≡new s∉can-p-θ)}
               {.(rif-false {x = x} x∈ θx≡zero p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧} (CBρ cbp)
               (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
               (vif-false {.θ} {.p} {th} {.qin} {x} {.E} {x∈} {θx≡zero} {.p≐E⟦pin⟧}) =
  inj₂
  (_ , _ , _ ,
   rif-false {x = x} x∈ θx≡zero p≐E⟦pin⟧ ,′
   rreadyness {θ} {_} {s} s∈ θs≡old⊎θs≡new
     (λ s∈can-E⟦qin⟧ →
       s∉can-p-θ
        (canθₛₕ-subset (Env.sig θ) 0 (E ⟦ qin ⟧e) p Env.[]env
           (λ θ* S* → canₛ-if-false θ* p≐E⟦pin⟧ S*)
           (λ θ* s* → canₛₕ-if-false θ* p≐E⟦pin⟧ s*)
           s s∈can-E⟦qin⟧)))

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ qin ⟧e)} {.θ} {_} {E}
               {.(if x ∣⇒ qin ∣⇒ els)} {qin} {_} {_} {_} {_} {_} {_}
               {.(rabsence {θ} {p} {S} S∈ θS≡unknown S∉can-p-θ)}
               {.(rif-true {x = x} {E} {n} x∈ θx≡suc p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧} (CBρ cbp)
               (vabsence S S∈ θS≡unknown S∉can-p-θ)
               (vif-true {.θ} {.p} {.qin} {els} {x} {.E} {n} {x∈} {θx≡suc} {.p≐E⟦pin⟧}) =
  inj₂
  (_ , _ , _ ,
   rif-true {x = x} x∈ θx≡suc p≐E⟦pin⟧ ,′
   rabsence {θ} {_} {S} S∈ θS≡unknown
     (λ S∈can-E⟦qin⟧ →
       S∉can-p-θ
         (canθₛ-subset (Env.sig θ) 0 (E ⟦ qin ⟧e) p Env.[]env
           (λ θ* S* → canₛ-if-true θ* p≐E⟦pin⟧ S*)
           S  S∈can-E⟦qin⟧)))

ρ-pot-conf-rec {p} {θ} {.p} {θl} {.(E ⟦ qin ⟧e)} {.θ} {_} {E}
               {.(if x ∣⇒ qin ∣⇒ els)} {qin} {_} {_} {_} {_} {_} {_}
               {.(rreadyness {θ} {p} {s} s∈ θs≡old⊎θs≡new s∉can-p-θ)}
               {.(rif-true {x = x} {E} {n} x∈ θx≡suc p≐E⟦pin⟧)}
               {p≐E⟦pin⟧} {qr≐E⟦qin⟧} (CBρ cbp)
               (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
               (vif-true {.θ} {.p} {.qin} {els} {x} {.E} {n} {x∈} {θx≡suc} {.p≐E⟦pin⟧}) =
  inj₂
  (_ , _ , _ ,
   rif-true {x = x} x∈ θx≡suc p≐E⟦pin⟧ ,′
   rreadyness {θ} {_} {s} s∈ θs≡old⊎θs≡new
     (λ s∈can-E⟦qin⟧ →
       s∉can-p-θ
         (canθₛₕ-subset (Env.sig θ) 0 (E ⟦ qin ⟧e) p Env.[]env
           (λ θ* S* → canₛ-if-true θ* p≐E⟦pin⟧ S*)
           (λ θ* s* → canₛₕ-if-true θ* p≐E⟦pin⟧ s*)
           s s∈can-E⟦qin⟧)))

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

module _ {X : Set} {x : X} where

  test : (p q : Σ X (x ≡_)) → p ≡ q
  test (.x , refl) (z , q) = {!q!}

-- C-c C-c q RET:
-- WAS: test (_ , refl) (_ , refl)
-- WANT: preserved user-written pattern
--       test (.x , refl) (_ , refl)

  test' : (p q : Σ X (x ≡_)) → p ≡ q
  test' (x , refl) (z , q) = {!q!}

-- here it's fine!
-- C-c C-c q RET gives us:
-- test' (x , refl) (.x , refl) = {!!}


text:
open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Reflection

id : ∀ {a} {A : Set a} → A → A
id x = x

macro
  my-macro : Term → TC ⊤
  my-macro goal = bindTC
    (getType (quote id))
    λ idType → bindTC
      (reduce idType)
      λ _ → returnTC _

fails? : ⊤
fails? = my-macro

max_forks_repo_name: shlevy/agda


text:
-----------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the heterogeneous sublist relation
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.List.Relation.Binary.Sublist.Heterogeneous.Properties where

open import Level

open import Data.Bool.Base using (true; false)
open import Data.Empty
open import Data.List.Relation.Unary.All using (Null; []; _∷_)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Base as List hiding (map; _∷ʳ_)
import Data.List.Properties as Lₚ
open import Data.List.Relation.Unary.Any.Properties
  using (here-injective; there-injective)
open import Data.List.Relation.Binary.Pointwise as Pw using (Pointwise; []; _∷_)
open import Data.List.Relation.Binary.Sublist.Heterogeneous

open import Data.Maybe.Relation.Unary.All as MAll using (nothing; just)
open import Data.Nat.Base using (ℕ; _≤_; _≥_); open ℕ; open _≤_
import Data.Nat.Properties as ℕₚ
open import Data.Product using (∃₂; _×_; _,_; proj₂; uncurry)

open import Function.Base
open import Function.Bijection   using (_⤖_; bijection)
open import Function.Equivalence using (_⇔_ ; equivalence)

open import Relation.Nullary.Reflects using (invert)
open import Relation.Nullary using (Dec; does; _because_; yes; no; ¬_)
open import Relation.Nullary.Negation using (¬?)
import Relation.Nullary.Decidable as Dec
open import Relation.Unary as U using (Pred)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- Injectivity of constructors

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  ∷-injectiveˡ : ∀ {x y xs ys} {px qx : R x y} {pxs qxs : Sublist R xs ys} →
                 (Sublist R (x ∷ xs) (y ∷ ys) ∋ px ∷ pxs) ≡ (qx ∷ qxs) → px ≡ qx
  ∷-injectiveˡ P.refl = P.refl

  ∷-injectiveʳ : ∀ {x y xs ys} {px qx : R x y} {pxs qxs : Sublist R xs ys} →
                 (Sublist R (x ∷ xs) (y ∷ ys) ∋ px ∷ pxs) ≡ (qx ∷ qxs) → pxs ≡ qxs
  ∷-injectiveʳ P.refl = P.refl

  ∷ʳ-injective : ∀ {y xs ys} {pxs qxs : Sublist R xs ys} →
                 (Sublist R xs (y ∷ ys) ∋ y ∷ʳ pxs) ≡ (y ∷ʳ qxs) → pxs ≡ qxs
  ∷ʳ-injective P.refl = P.refl

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  length-mono-≤ : ∀ {as bs} → Sublist R as bs → length as ≤ length bs
  length-mono-≤ []        = z≤n
  length-mono-≤ (y ∷ʳ rs) = ℕₚ.≤-step (length-mono-≤ rs)
  length-mono-≤ (r ∷ rs)  = s≤s (length-mono-≤ rs)

------------------------------------------------------------------------
-- Conversion to and from Pointwise (proto-reflexivity)

  fromPointwise : Pointwise R ⇒ Sublist R
  fromPointwise []       = []
  fromPointwise (p ∷ ps) = p ∷ fromPointwise ps

  toPointwise : ∀ {as bs} → length as ≡ length bs →
                Sublist R as bs → Pointwise R as bs
  toPointwise {bs = []}     eq []         = []
  toPointwise {bs = b ∷ bs} eq (r ∷ rs)   = r ∷ toPointwise (ℕₚ.suc-injective eq) rs
  toPointwise {bs = b ∷ bs} eq (b ∷ʳ rs) =
    ⊥-elim $ ℕₚ.<-irrefl eq (s≤s (length-mono-≤ rs))

------------------------------------------------------------------------
-- Various functions' outputs are sublists

-- These lemmas are generalisations of results of the form `f xs ⊆ xs`.
-- (where _⊆_ stands for Sublist R). If R is reflexive then we can indeed
-- obtain `f xs ⊆ xs` from `xs ⊆ ys → f xs ⊆ ys`. The other direction is
-- only true if R is both reflexive and transitive.

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  tail-Sublist : ∀ {as bs} → Sublist R as bs →
                 MAll.All (λ as → Sublist R as bs) (tail as)
  tail-Sublist []        = nothing
  tail-Sublist (b ∷ʳ ps) = MAll.map (b ∷ʳ_) (tail-Sublist ps)
  tail-Sublist (p ∷ ps)  = just (_ ∷ʳ ps)

  take-Sublist : ∀ {as bs} n → Sublist R as bs → Sublist R (take n as) bs
  take-Sublist n       (y ∷ʳ rs) = y ∷ʳ take-Sublist n rs
  take-Sublist zero    rs        = minimum _
  take-Sublist (suc n) []        = []
  take-Sublist (suc n) (r ∷ rs)  = r ∷ take-Sublist n rs

  drop-Sublist : ∀ n → Sublist R ⇒ (Sublist R ∘′ drop n)
  drop-Sublist n       (y ∷ʳ rs) = y ∷ʳ drop-Sublist n rs
  drop-Sublist zero    rs        = rs
  drop-Sublist (suc n) []        = []
  drop-Sublist (suc n) (r ∷ rs)  = _ ∷ʳ drop-Sublist n rs

module _ {a b r p} {A : Set a} {B : Set b}
         {R : REL A B r} {P : Pred A p} (P? : U.Decidable P) where

  takeWhile-Sublist : ∀ {as bs} → Sublist R as bs → Sublist R (takeWhile P? as) bs
  takeWhile-Sublist []        = []
  takeWhile-Sublist (y ∷ʳ rs) = y ∷ʳ takeWhile-Sublist rs
  takeWhile-Sublist {a ∷ as} (r ∷ rs) with does (P? a)
  ... | true  = r ∷ takeWhile-Sublist rs
  ... | false = minimum _

  dropWhile-Sublist : ∀ {as bs} → Sublist R as bs → Sublist R (dropWhile P? as) bs
  dropWhile-Sublist []        = []
  dropWhile-Sublist (y ∷ʳ rs) = y ∷ʳ dropWhile-Sublist rs
  dropWhile-Sublist {a ∷ as} (r ∷ rs) with does (P? a)
  ... | true  = _ ∷ʳ dropWhile-Sublist rs
  ... | false = r ∷ rs

  filter-Sublist : ∀ {as bs} → Sublist R as bs → Sublist R (filter P? as) bs
  filter-Sublist []        = []
  filter-Sublist (y ∷ʳ rs) = y ∷ʳ filter-Sublist rs
  filter-Sublist {a ∷ as} (r ∷ rs) with does (P? a)
  ... | true  = r ∷ filter-Sublist rs
  ... | false = _ ∷ʳ filter-Sublist rs

------------------------------------------------------------------------
-- Various functions are increasing wrt _⊆_

-- We write f⁺ for the proof that `xs ⊆ ys → f xs ⊆ f ys`
-- and f⁻ for the one that `f xs ⊆ f ys → xs ⊆ ys`.

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

------------------------------------------------------------------------
-- _∷_

  ∷ˡ⁻ : ∀ {a as bs} → Sublist R (a ∷ as) bs → Sublist R as bs
  ∷ˡ⁻ (y ∷ʳ rs) = y ∷ʳ ∷ˡ⁻ rs
  ∷ˡ⁻ (r ∷  rs) = _ ∷ʳ rs

  ∷ʳ⁻ : ∀ {a as b bs} → ¬ R a b → Sublist R (a ∷ as) (b ∷ bs) →
        Sublist R (a ∷ as) bs
  ∷ʳ⁻ ¬r (y ∷ʳ rs) = rs
  ∷ʳ⁻ ¬r (r ∷  rs) = ⊥-elim (¬r r)

  ∷⁻ : ∀ {a as b bs} → Sublist R (a ∷ as) (b ∷ bs) → Sublist R as bs
  ∷⁻ (y ∷ʳ rs) = ∷ˡ⁻ rs
  ∷⁻ (x ∷  rs) = rs

module _ {a b c d r} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
         {R : REL C D r} where

------------------------------------------------------------------------
-- map

  map⁺ : ∀ {as bs} (f : A → C) (g : B → D) →
         Sublist (λ a b → R (f a) (g b)) as bs →
         Sublist R (List.map f as) (List.map g bs)
  map⁺ f g []        = []
  map⁺ f g (y ∷ʳ rs) = g y ∷ʳ map⁺ f g rs
  map⁺ f g (r ∷ rs)  = r ∷ map⁺ f g rs

  map⁻ : ∀ {as bs} (f : A → C) (g : B → D) →
         Sublist R (List.map f as) (List.map g bs) →
         Sublist (λ a b → R (f a) (g b)) as bs
  map⁻ {[]}     {bs}     f g rs        = minimum _
  map⁻ {a ∷ as} {b ∷ bs} f g (_ ∷ʳ rs) = b ∷ʳ map⁻ f g rs
  map⁻ {a ∷ as} {b ∷ bs} f g (r ∷ rs)  = r ∷ map⁻ f g rs

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

------------------------------------------------------------------------
-- _++_

  ++⁺ : ∀ {as bs cs ds} → Sublist R as bs → Sublist R cs ds →
        Sublist R (as ++ cs) (bs ++ ds)
  ++⁺ []         cds = cds
  ++⁺ (y ∷ʳ abs) cds = y ∷ʳ ++⁺ abs cds
  ++⁺ (ab ∷ abs) cds = ab ∷ ++⁺ abs cds

  ++⁻ : ∀ {as bs cs ds} → length as ≡ length bs →
        Sublist R (as ++ cs) (bs ++ ds) → Sublist R cs ds
  ++⁻ {[]}     {[]}     eq rs = rs
  ++⁻ {a ∷ as} {b ∷ bs} eq rs = ++⁻ (ℕₚ.suc-injective eq) (∷⁻ rs)

  ++ˡ : ∀ {as bs} (cs : List B) → Sublist R as bs → Sublist R as (cs ++ bs)
  ++ˡ zs = ++⁺ (minimum zs)

  ++ʳ : ∀ {as bs} (cs : List B) → Sublist R as bs → Sublist R as (bs ++ cs)
  ++ʳ cs []        = minimum cs
  ++ʳ cs (y ∷ʳ rs) = y ∷ʳ ++ʳ cs rs
  ++ʳ cs (r ∷ rs)  = r ∷ ++ʳ cs rs

------------------------------------------------------------------------
-- concat

  concat⁺ : ∀ {ass bss} → Sublist (Sublist R) ass bss →
            Sublist R (concat ass) (concat bss)
  concat⁺ []          = []
  concat⁺ (y  ∷ʳ rss) = ++ˡ y (concat⁺ rss)
  concat⁺ (rs ∷  rss) = ++⁺ rs (concat⁺ rss)

------------------------------------------------------------------------
-- take / drop

  take⁺ : ∀ {m n as bs} → m ≤ n → Pointwise R as bs →
          Sublist R (take m as) (take n bs)
  take⁺ z≤n       ps        = minimum _
  take⁺ (s≤s m≤n) []        = []
  take⁺ (s≤s m≤n) (p ∷  ps) = p ∷ take⁺ m≤n ps

  drop⁺ : ∀ {m n as bs} → m ≥ n → Sublist R as bs →
          Sublist R (drop m as) (drop n bs)
  drop⁺ {m} z≤n       rs        = drop-Sublist m rs
  drop⁺     (s≤s m≥n) []        = []
  drop⁺     (s≤s m≥n) (y ∷ʳ rs) = drop⁺ (ℕₚ.≤-step m≥n) rs
  drop⁺     (s≤s m≥n) (r ∷ rs)  = drop⁺ m≥n rs

  drop⁺-≥ : ∀ {m n as bs} → m ≥ n → Pointwise R as bs →
            Sublist R (drop m as) (drop n bs)
  drop⁺-≥ m≥n pw = drop⁺ m≥n (fromPointwise pw)

  drop⁺-⊆ : ∀ {as bs} m → Sublist R as bs →
            Sublist R (drop m as) (drop m bs)
  drop⁺-⊆ m = drop⁺ (ℕₚ.≤-refl {m})

module _ {a b r p q} {A : Set a} {B : Set b}
         {R : REL A B r} {P : Pred A p} {Q : Pred B q}
         (P? : U.Decidable P) (Q? : U.Decidable Q) where

  ⊆-takeWhile-Sublist : ∀ {as bs} →
    (∀ {a b} → R a b → P a → Q b) →
    Pointwise R as bs → Sublist R (takeWhile P? as) (takeWhile Q? bs)
  ⊆-takeWhile-Sublist rp⇒q [] = []
  ⊆-takeWhile-Sublist {a ∷ as} {b ∷ bs} rp⇒q (p ∷ ps) with P? a | Q? b
  ... | false because _ | _               = minimum _
  ... | true  because _ | true  because _ = p ∷ ⊆-takeWhile-Sublist rp⇒q ps
  ... | yes pa          | no ¬qb          = ⊥-elim $ ¬qb $ rp⇒q p pa

  ⊇-dropWhile-Sublist : ∀ {as bs} →
    (∀ {a b} → R a b → Q b → P a) →
    Pointwise R as bs → Sublist R (dropWhile P? as) (dropWhile Q? bs)
  ⊇-dropWhile-Sublist rq⇒p [] = []
  ⊇-dropWhile-Sublist {a ∷ as} {b ∷ bs} rq⇒p (p ∷ ps) with P? a | Q? b
  ... | true  because _ | true  because _ = ⊇-dropWhile-Sublist rq⇒p ps
  ... | true  because _ | false because _ =
    b ∷ʳ dropWhile-Sublist P? (fromPointwise ps)
  ... | false because _ | false because _ = p ∷ fromPointwise ps
  ... | no ¬pa          | yes qb          = ⊥-elim $ ¬pa $ rq⇒p p qb

  ⊆-filter-Sublist : ∀ {as bs} → (∀ {a b} → R a b → P a → Q b) →
                     Sublist R as bs → Sublist R (filter P? as) (filter Q? bs)
  ⊆-filter-Sublist rp⇒q [] = []
  ⊆-filter-Sublist rp⇒q (y ∷ʳ rs) with does (Q? y)
  ... | true  = y ∷ʳ ⊆-filter-Sublist rp⇒q rs
  ... | false = ⊆-filter-Sublist rp⇒q rs
  ⊆-filter-Sublist {a ∷ as} {b ∷ bs} rp⇒q (r ∷ rs) with P? a | Q? b
  ... | true  because _ | true  because _ = r ∷ ⊆-filter-Sublist rp⇒q rs
  ... | false because _ | true  because _ = _ ∷ʳ ⊆-filter-Sublist rp⇒q rs
  ... | false because _ | false because _ = ⊆-filter-Sublist rp⇒q rs
  ... | yes pa          | no ¬qb          = ⊥-elim $ ¬qb $ rp⇒q r pa

module _ {a r p} {A : Set a} {R : Rel A r} {P : Pred A p} (P? : U.Decidable P) where

  takeWhile-filter : ∀ {as} → Pointwise R as as →
                     Sublist R (takeWhile P? as) (filter P? as)
  takeWhile-filter [] = []
  takeWhile-filter {a ∷ as} (p ∷ ps) with does (P? a)
  ... | true  = p ∷ takeWhile-filter ps
  ... | false = minimum _

  filter-dropWhile : ∀ {as} → Pointwise R as as →
                     Sublist R (filter P? as) (dropWhile (¬? ∘ P?) as)
  filter-dropWhile [] = []
  filter-dropWhile {a ∷ as} (p ∷ ps) with does (P? a)
  ... | true  = p ∷ filter-Sublist P? (fromPointwise ps)
  ... | false = filter-dropWhile ps

------------------------------------------------------------------------
-- reverse

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  reverseAcc⁺ : ∀ {as bs cs ds} → Sublist R as bs → Sublist R cs ds →
                Sublist R (reverseAcc cs as) (reverseAcc ds bs)
  reverseAcc⁺ []         cds = cds
  reverseAcc⁺ (y ∷ʳ abs) cds = reverseAcc⁺ abs (y ∷ʳ cds)
  reverseAcc⁺ (r ∷ abs)  cds = reverseAcc⁺ abs (r ∷ cds)

  ʳ++⁺ : ∀ {as bs cs ds} →
         Sublist R as bs →
         Sublist R cs ds →
         Sublist R (as ʳ++ cs) (bs ʳ++ ds)
  ʳ++⁺ = reverseAcc⁺

  reverse⁺ : ∀ {as bs} → Sublist R as bs → Sublist R (reverse as) (reverse bs)
  reverse⁺ rs = reverseAcc⁺ rs []

  reverse⁻ : ∀ {as bs} → Sublist R (reverse as) (reverse bs) → Sublist R as bs
  reverse⁻ {as} {bs} p = cast (reverse⁺ p) where
    cast = P.subst₂ (Sublist R) (Lₚ.reverse-involutive as) (Lₚ.reverse-involutive bs)

------------------------------------------------------------------------
-- Inversion lemmas

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} {a as b bs} where

  ∷⁻¹ : R a b → Sublist R as bs ⇔ Sublist R (a ∷ as) (b ∷ bs)
  ∷⁻¹ r = equivalence (r ∷_) ∷⁻

  ∷ʳ⁻¹ : ¬ R a b → Sublist R (a ∷ as) bs ⇔ Sublist R (a ∷ as) (b ∷ bs)
  ∷ʳ⁻¹ ¬r = equivalence (_ ∷ʳ_) (∷ʳ⁻ ¬r)

------------------------------------------------------------------------
-- Irrelevant special case

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  Sublist-[]-irrelevant : U.Irrelevant (Sublist R [])
  Sublist-[]-irrelevant []       []        = P.refl
  Sublist-[]-irrelevant (y ∷ʳ p) (.y ∷ʳ q) = P.cong (y ∷ʳ_) (Sublist-[]-irrelevant p q)

------------------------------------------------------------------------
-- (to/from)Any is a bijection

  toAny-injective : ∀ {xs x} {p q : Sublist R [ x ] xs} → toAny p ≡ toAny q → p ≡ q
  toAny-injective {p = y ∷ʳ p} {y ∷ʳ q} =
    P.cong (y ∷ʳ_) ∘′ toAny-injective ∘′ there-injective
  toAny-injective {p = _ ∷ p}  {_ ∷ q}  =
    P.cong₂ (flip _∷_) (Sublist-[]-irrelevant p q) ∘′ here-injective

  fromAny-injective : ∀ {xs x} {p q : Any (R x) xs} →
                      fromAny {R = R} p ≡ fromAny q → p ≡ q
  fromAny-injective {p = here px} {here qx} = P.cong here ∘′ ∷-injectiveˡ
  fromAny-injective {p = there p} {there q} =
    P.cong there ∘′ fromAny-injective ∘′ ∷ʳ-injective

  toAny∘fromAny≗id : ∀ {xs x} (p : Any (R x) xs) → toAny (fromAny {R = R} p) ≡ p
  toAny∘fromAny≗id (here px) = P.refl
  toAny∘fromAny≗id (there p) = P.cong there (toAny∘fromAny≗id p)

  Sublist-[x]-bijection : ∀ {x xs} → (Sublist R [ x ] xs) ⤖ (Any (R x) xs)
  Sublist-[x]-bijection = bijection toAny fromAny toAny-injective toAny∘fromAny≗id

------------------------------------------------------------------------
-- Relational properties

module Reflexivity
    {a r} {A : Set a} {R : Rel A r}
    (R-refl : Reflexive R) where

  reflexive : _≡_ ⇒ Sublist R
  reflexive P.refl = fromPointwise (Pw.refl R-refl)

  refl : Reflexive (Sublist R)
  refl = reflexive P.refl

open Reflexivity public

module Transitivity
    {a b c r s t} {A : Set a} {B : Set b} {C : Set c}
    {R : REL A B r} {S : REL B C s} {T : REL A C t}
    (rs⇒t : Trans R S T) where

  trans : Trans (Sublist R) (Sublist S) (Sublist T)
  trans rs        (y ∷ʳ ss) = y ∷ʳ trans rs ss
  trans (y ∷ʳ rs) (s ∷ ss)  = _ ∷ʳ trans rs ss
  trans (r ∷ rs)  (s ∷ ss)  = rs⇒t r s ∷ trans rs ss
  trans []        []        = []

open Transitivity public

module Antisymmetry
    {a b r s e} {A : Set a} {B : Set b}
    {R : REL A B r} {S : REL B A s} {E : REL A B e}
    (rs⇒e : Antisym R S E) where

  open ℕₚ.≤-Reasoning

  antisym : Antisym (Sublist R) (Sublist S) (Pointwise E)
  antisym []        []        = []
  antisym (r ∷ rs)  (s ∷ ss)  = rs⇒e r s ∷ antisym rs ss
  -- impossible cases
  antisym (_∷ʳ_ {xs} {ys₁} y rs) (_∷ʳ_ {ys₂} {zs} z ss) =
    ⊥-elim $ ℕₚ.<-irrefl P.refl $ begin
    length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩
    length zs        ≤⟨ ℕₚ.n≤1+n (length zs) ⟩
    length (z ∷ zs)  ≤⟨ length-mono-≤ rs ⟩
    length ys₁       ∎
  antisym (_∷ʳ_ {xs} {ys₁} y rs) (_∷_ {y} {ys₂} {z} {zs} s ss)  =
    ⊥-elim $ ℕₚ.<-irrefl P.refl $ begin
    length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩
    length ys₁      ≤⟨ length-mono-≤ ss ⟩
    length zs       ∎
  antisym (_∷_ {x} {xs} {y} {ys₁} r rs)  (_∷ʳ_ {ys₂} {zs} z ss) =
    ⊥-elim $ ℕₚ.<-irrefl P.refl $ begin
    length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩
    length xs        ≤⟨ length-mono-≤ rs ⟩
    length ys₁       ∎

open Antisymmetry public

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} (R? : Decidable R) where

  sublist? : Decidable (Sublist R)
  sublist? []       ys       = yes (minimum ys)
  sublist? (x ∷ xs) []       = no λ ()
  sublist? (x ∷ xs) (y ∷ ys) with R? x y
  ... | true  because  [r] =
    Dec.map (∷⁻¹  (invert  [r])) (sublist? xs ys)
  ... | false because [¬r] =
    Dec.map (∷ʳ⁻¹ (invert [¬r])) (sublist? (x ∷ xs) ys)

module _ {a e r} {A : Set a} {E : Rel A e} {R : Rel A r} where

  isPreorder : IsPreorder E R → IsPreorder (Pointwise E) (Sublist R)
  isPreorder ER-isPreorder = record
    { isEquivalence = Pw.isEquivalence       ER.isEquivalence
    ; reflexive     = fromPointwise ∘ Pw.map ER.reflexive
    ; trans         = trans                  ER.trans
    } where module ER = IsPreorder ER-isPreorder

  isPartialOrder : IsPartialOrder E R → IsPartialOrder (Pointwise E) (Sublist R)
  isPartialOrder ER-isPartialOrder = record
    { isPreorder = isPreorder ER.isPreorder
    ; antisym    = antisym    ER.antisym
    } where module ER = IsPartialOrder ER-isPartialOrder

  isDecPartialOrder : IsDecPartialOrder E R →
                      IsDecPartialOrder (Pointwise E) (Sublist R)
  isDecPartialOrder ER-isDecPartialOrder = record
    { isPartialOrder = isPartialOrder ER.isPartialOrder
    ; _≟_            = Pw.decidable   ER._≟_
    ; _≤?_           = sublist?       ER._≤?_
    } where module ER = IsDecPartialOrder ER-isDecPartialOrder

module _ {a e r} where

  preorder : Preorder a e r → Preorder _ _ _
  preorder ER-preorder = record
    { isPreorder = isPreorder ER.isPreorder
    } where module ER = Preorder ER-preorder

  poset : Poset a e r → Poset _ _ _
  poset ER-poset = record
    { isPartialOrder = isPartialOrder ER.isPartialOrder
    } where module ER = Poset ER-poset

  decPoset : DecPoset a e r → DecPoset _ _ _
  decPoset ER-poset = record
    { isDecPartialOrder = isDecPartialOrder ER.isDecPartialOrder
    } where module ER = DecPoset ER-poset

------------------------------------------------------------------------
-- Properties of disjoint sublists

module Disjointness {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  private
    infix 4 _⊆_
    _⊆_ = Sublist R

  -- Forgetting the union

  DisjointUnion→Disjoint : ∀ {xs ys zs us} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : us ⊆ zs} →
    DisjointUnion τ₁ τ₂ τ → Disjoint τ₁ τ₂
  DisjointUnion→Disjoint []         = []
  DisjointUnion→Disjoint (y   ∷ₙ u) = y   ∷ₙ DisjointUnion→Disjoint u
  DisjointUnion→Disjoint (x≈y ∷ₗ u) = x≈y ∷ₗ DisjointUnion→Disjoint u
  DisjointUnion→Disjoint (x≈y ∷ᵣ u) = x≈y ∷ᵣ DisjointUnion→Disjoint u

  -- Reconstructing the union

  Disjoint→DisjointUnion : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
    Disjoint τ₁ τ₂ → ∃₂ λ us (τ : us ⊆ zs) → DisjointUnion τ₁ τ₂ τ
  Disjoint→DisjointUnion []         = _ , _ , []
  Disjoint→DisjointUnion (y   ∷ₙ u) = _ , _ , y   ∷ₙ proj₂ (proj₂ (Disjoint→DisjointUnion u))
  Disjoint→DisjointUnion (x≈y ∷ₗ u) = _ , _ , x≈y ∷ₗ proj₂ (proj₂ (Disjoint→DisjointUnion u))
  Disjoint→DisjointUnion (x≈y ∷ᵣ u) = _ , _ , x≈y ∷ᵣ proj₂ (proj₂ (Disjoint→DisjointUnion u))

  -- Disjoint is decidable

  ⊆-disjoint? : ∀ {xs ys zs} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → Dec (Disjoint τ₁ τ₂)
  ⊆-disjoint? [] [] = yes []
  -- Present in both sublists: not disjoint.
  ⊆-disjoint? (x≈z ∷ τ₁) (y≈z ∷ τ₂) = no λ()
  -- Present in either sublist: ok.
  ⊆-disjoint? (y ∷ʳ τ₁) (x≈y ∷ τ₂) =
    Dec.map′ (x≈y ∷ᵣ_) (λ{ (_ ∷ᵣ d) → d }) (⊆-disjoint? τ₁ τ₂)
  ⊆-disjoint? (x≈y ∷ τ₁) (y ∷ʳ τ₂) =
    Dec.map′ (x≈y ∷ₗ_) (λ{ (_ ∷ₗ d) → d }) (⊆-disjoint? τ₁ τ₂)
  -- Present in neither sublist: ok.
  ⊆-disjoint? (y ∷ʳ τ₁) (.y ∷ʳ τ₂) =
    Dec.map′ (y ∷ₙ_) (λ{ (_ ∷ₙ d) → d }) (⊆-disjoint? τ₁ τ₂)

  -- Disjoint is proof-irrelevant

  Disjoint-irrelevant : ∀{xs ys zs} → Irrelevant (Disjoint {R = R} {xs} {ys} {zs})
  Disjoint-irrelevant [] [] = P.refl
  Disjoint-irrelevant (y   ∷ₙ d₁) (.y   ∷ₙ d₂) = P.cong (y ∷ₙ_) (Disjoint-irrelevant d₁ d₂)
  Disjoint-irrelevant (x≈y ∷ₗ d₁) (.x≈y ∷ₗ d₂) = P.cong (x≈y ∷ₗ_) (Disjoint-irrelevant d₁ d₂)
  Disjoint-irrelevant (x≈y ∷ᵣ d₁) (.x≈y ∷ᵣ d₂) = P.cong (x≈y ∷ᵣ_) (Disjoint-irrelevant d₁ d₂)

  -- Note: DisjointUnion is not proof-irrelevant unless the underlying relation R is.
  -- The proof is not entirely trivial, thus, we leave it for future work:
  --
  -- DisjointUnion-irrelevant : Irrelevant R →
  --                            ∀{xs ys us zs} {τ : us ⊆ zs} →
  --                            Irrelevant (λ (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → DisjointUnion τ₁ τ₂ τ)

  -- Irreflexivity

  Disjoint-irrefl′ : ∀{xs ys} {τ : xs ⊆ ys} → Disjoint τ τ → Null xs
  Disjoint-irrefl′ []       = []
  Disjoint-irrefl′ (y ∷ₙ d) = Disjoint-irrefl′ d

  Disjoint-irrefl : ∀{x xs ys} → Irreflexive {A = x ∷ xs ⊆ ys } _≡_ Disjoint
  Disjoint-irrefl P.refl x with Disjoint-irrefl′ x
  ... | () ∷ _

  -- Symmetry

  DisjointUnion-sym : ∀ {xs ys xys} {zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : xys ⊆ zs} →
                            DisjointUnion τ₁ τ₂ τ → DisjointUnion τ₂ τ₁ τ
  DisjointUnion-sym []         = []
  DisjointUnion-sym (y   ∷ₙ d) = y ∷ₙ DisjointUnion-sym d
  DisjointUnion-sym (x≈y ∷ₗ d) = x≈y ∷ᵣ DisjointUnion-sym d
  DisjointUnion-sym (x≈y ∷ᵣ d) = x≈y ∷ₗ DisjointUnion-sym d

  Disjoint-sym : ∀ {xs ys} {zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
                 Disjoint τ₁ τ₂ → Disjoint τ₂ τ₁
  Disjoint-sym []         = []
  Disjoint-sym (y   ∷ₙ d) = y ∷ₙ Disjoint-sym d
  Disjoint-sym (x≈y ∷ₗ d) = x≈y ∷ᵣ Disjoint-sym d
  Disjoint-sym (x≈y ∷ᵣ d) = x≈y ∷ₗ Disjoint-sym d

  -- Empty sublist

  DisjointUnion-[]ˡ : ∀{xs ys} {ε : [] ⊆ ys} {τ : xs ⊆ ys} → DisjointUnion ε τ τ
  DisjointUnion-[]ˡ {ε = []}     {τ = []} = []
  DisjointUnion-[]ˡ {ε = y ∷ʳ ε} {τ = y  ∷ʳ τ} = y   ∷ₙ DisjointUnion-[]ˡ
  DisjointUnion-[]ˡ {ε = y ∷ʳ ε} {τ = x≈y ∷ τ} = x≈y ∷ᵣ DisjointUnion-[]ˡ

  DisjointUnion-[]ʳ : ∀{xs ys} {ε : [] ⊆ ys} {τ : xs ⊆ ys} → DisjointUnion τ ε τ
  DisjointUnion-[]ʳ {ε = []}     {τ = []} = []
  DisjointUnion-[]ʳ {ε = y ∷ʳ ε} {τ = y  ∷ʳ τ} = y   ∷ₙ DisjointUnion-[]ʳ
  DisjointUnion-[]ʳ {ε = y ∷ʳ ε} {τ = x≈y ∷ τ} = x≈y ∷ₗ DisjointUnion-[]ʳ

  -- A sublist τ : x∷xs ⊆ ys can be split into two disjoint sublists
  -- [x] ⊆ ys (canonical choice) and (∷ˡ⁻ τ) : xs ⊆ ys.

  DisjointUnion-fromAny∘toAny-∷ˡ⁻ : ∀ {x xs ys} (τ : (x ∷ xs) ⊆ ys) → DisjointUnion (fromAny (toAny τ)) (∷ˡ⁻ τ) τ
  DisjointUnion-fromAny∘toAny-∷ˡ⁻ (y  ∷ʳ τ) = y   ∷ₙ DisjointUnion-fromAny∘toAny-∷ˡ⁻ τ
  DisjointUnion-fromAny∘toAny-∷ˡ⁻ (xRy ∷ τ) = xRy ∷ₗ DisjointUnion-[]ˡ

  -- Disjoint union of three mutually disjoint lists.
  --
  -- τᵢⱼ denotes the disjoint union of τᵢ and τⱼ: DisjointUnion τᵢ τⱼ τᵢⱼ

  record DisjointUnion³
    {xs ys zs ts} (τ₁  : xs  ⊆ ts) (τ₂  : ys  ⊆ ts) (τ₃  : zs  ⊆ ts)
    {xys xzs yzs} (τ₁₂ : xys ⊆ ts) (τ₁₃ : xzs ⊆ ts) (τ₂₃ : yzs ⊆ ts) : Set (a ⊔ b ⊔ r) where
    field
      {union³} : List A
      sub³  : union³ ⊆ ts
      join₁ : DisjointUnion τ₁ τ₂₃ sub³
      join₂ : DisjointUnion τ₂ τ₁₃ sub³
      join₃ : DisjointUnion τ₃ τ₁₂ sub³

  infixr 5 _∷ʳ-DisjointUnion³_ _∷₁-DisjointUnion³_ _∷₂-DisjointUnion³_ _∷₃-DisjointUnion³_

  -- Weakening the target list ts of a disjoint union.

  _∷ʳ-DisjointUnion³_ :
    ∀ {xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts} →
    ∀ {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
    ∀ y →
    DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃ →
    DisjointUnion³ (y ∷ʳ τ₁) (y ∷ʳ τ₂) (y ∷ʳ τ₃) (y ∷ʳ τ₁₂) (y ∷ʳ τ₁₃) (y ∷ʳ τ₂₃)
  y ∷ʳ-DisjointUnion³ record{ sub³ = σ ; join₁ = d₁ ; join₂ = d₂ ; join₃ = d₃ } = record
    { sub³  = y ∷ʳ σ
    ; join₁ = y ∷ₙ d₁
    ; join₂ = y ∷ₙ d₂
    ; join₃ = y ∷ₙ d₃
    }

  -- Adding an element to the first list.

  _∷₁-DisjointUnion³_ :
    ∀ {xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts} →
    ∀ {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
    ∀ {x y} (xRy : R x y) →
    DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃ →
    DisjointUnion³ (xRy ∷ τ₁) (y ∷ʳ τ₂) (y ∷ʳ τ₃) (xRy ∷ τ₁₂) (xRy ∷ τ₁₃) (y ∷ʳ τ₂₃)
  xRy ∷₁-DisjointUnion³ record{ sub³ = σ ; join₁ = d₁ ; join₂ = d₂ ; join₃ = d₃ } = record
    { sub³  = xRy ∷ σ
    ; join₁ = xRy ∷ₗ d₁
    ; join₂ = xRy ∷ᵣ d₂
    ; join₃ = xRy ∷ᵣ d₃
    }

  -- Adding an element to the second list.

  _∷₂-DisjointUnion³_ :
    ∀ {xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts} →
    ∀ {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
    ∀ {x y} (xRy : R x y) →
    DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃ →
    DisjointUnion³ (y ∷ʳ τ₁) (xRy ∷ τ₂) (y ∷ʳ τ₃) (xRy ∷ τ₁₂) (y ∷ʳ τ₁₃) (xRy ∷ τ₂₃)
  xRy ∷₂-DisjointUnion³ record{ sub³ = σ ; join₁ = d₁ ; join₂ = d₂ ; join₃ = d₃ } = record
    { sub³  = xRy ∷ σ
    ; join₁ = xRy ∷ᵣ d₁
    ; join₂ = xRy ∷ₗ d₂
    ; join₃ = xRy ∷ᵣ d₃
    }

  -- Adding an element to the third list.

  _∷₃-DisjointUnion³_ :
    ∀ {xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts} →
    ∀ {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
    ∀ {x y} (xRy : R x y) →
    DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃ →
    DisjointUnion³ (y ∷ʳ τ₁) (y ∷ʳ τ₂) (xRy ∷ τ₃) (y ∷ʳ τ₁₂) (xRy ∷ τ₁₃) (xRy ∷ τ₂₃)
  xRy ∷₃-DisjointUnion³ record{ sub³ = σ ; join₁ = d₁ ; join₂ = d₂ ; join₃ = d₃ } = record
    { sub³  = xRy ∷ σ
    ; join₁ = xRy ∷ᵣ d₁
    ; join₂ = xRy ∷ᵣ d₂
    ; join₃ = xRy ∷ₗ d₃
    }

  -- Computing the disjoint union of three disjoint lists.

  disjointUnion³ : ∀{xs ys zs ts} {τ₁ : xs ⊆ ts} {τ₂ : ys ⊆ ts} {τ₃ : zs ⊆ ts}
    {xys xzs yzs} {τ₁₂ : xys ⊆ ts} {τ₁₃ : xzs ⊆ ts} {τ₂₃ : yzs ⊆ ts} →
    DisjointUnion τ₁ τ₂ τ₁₂ →
    DisjointUnion τ₁ τ₃ τ₁₃ →
    DisjointUnion τ₂ τ₃ τ₂₃ →
    DisjointUnion³ τ₁ τ₂ τ₃ τ₁₂ τ₁₃ τ₂₃
  disjointUnion³ [] [] [] = record { sub³ = [] ; join₁ = [] ; join₂ = [] ; join₃ = [] }
  disjointUnion³ (y   ∷ₙ d₁₂) (.y  ∷ₙ d₁₃) (.y   ∷ₙ d₂₃) = y ∷ʳ-DisjointUnion³ disjointUnion³ d₁₂ d₁₃ d₂₃
  disjointUnion³ (y   ∷ₙ d₁₂) (xRy ∷ᵣ d₁₃) (.xRy ∷ᵣ d₂₃) = xRy ∷₃-DisjointUnion³ disjointUnion³ d₁₂ d₁₃ d₂₃
  disjointUnion³ (xRy ∷ᵣ d₁₂) (y   ∷ₙ d₁₃) (.xRy ∷ₗ d₂₃) = xRy ∷₂-DisjointUnion³ disjointUnion³ d₁₂ d₁₃ d₂₃
  disjointUnion³ (xRy ∷ₗ d₁₂) (.xRy ∷ₗ d₁₃) (y    ∷ₙ d₂₃) = xRy ∷₁-DisjointUnion³ disjointUnion³ d₁₂ d₁₃ d₂₃
  disjointUnion³ (xRy ∷ᵣ d₁₂) (xRy′ ∷ᵣ d₁₃) ()

  -- If a sublist τ is disjoint to two lists σ₁ and σ₂,
  -- then also to their disjoint union σ.

  disjoint⇒disjoint-to-union : ∀{xs ys zs yzs ts}
    {τ : xs ⊆ ts} {σ₁ : ys ⊆ ts} {σ₂ : zs ⊆ ts} {σ : yzs ⊆ ts} →
    Disjoint τ σ₁ → Disjoint τ σ₂ → DisjointUnion σ₁ σ₂ σ → Disjoint τ σ
  disjoint⇒disjoint-to-union d₁ d₂ u = let
       _ , _ , u₁ = Disjoint→DisjointUnion d₁
       _ , _ , u₂ = Disjoint→DisjointUnion d₂
    in DisjointUnion→Disjoint (DisjointUnion³.join₁ (disjointUnion³ u₁ u₂ u))

open Disjointness public

-- Monotonicity of disjointness.

module DisjointnessMonotonicity
    {a b c r s t} {A : Set a} {B : Set b} {C : Set c}
    {R : REL A B r} {S : REL B C s} {T : REL A C t}
    (rs⇒t : Trans R S T) where

  -- We can enlarge and convert the target list of a disjoint union.

  weakenDisjointUnion : ∀ {xs ys xys zs ws}
    {τ₁ : Sublist R xs zs}
    {τ₂ : Sublist R ys zs}
    {τ : Sublist R xys zs} (σ : Sublist S zs ws) →
    DisjointUnion τ₁ τ₂ τ →
    DisjointUnion (trans rs⇒t τ₁ σ) (trans rs⇒t τ₂ σ) (trans rs⇒t τ σ)
  weakenDisjointUnion [] [] = []
  weakenDisjointUnion (w  ∷ʳ σ) d         = w ∷ₙ weakenDisjointUnion σ d
  weakenDisjointUnion (_   ∷ σ) (y   ∷ₙ d) = _ ∷ₙ weakenDisjointUnion σ d
  weakenDisjointUnion (zSw ∷ σ) (xRz ∷ₗ d) = rs⇒t xRz zSw ∷ₗ weakenDisjointUnion σ d
  weakenDisjointUnion (zSw ∷ σ) (yRz ∷ᵣ d) = rs⇒t yRz zSw ∷ᵣ weakenDisjointUnion σ d

  weakenDisjoint : ∀ {xs ys zs ws}
    {τ₁ : Sublist R xs zs}
    {τ₂ : Sublist R ys zs} (σ : Sublist S zs ws) →
    Disjoint τ₁ τ₂ →
    Disjoint (trans rs⇒t τ₁ σ) (trans rs⇒t τ₂ σ)
  weakenDisjoint [] [] = []
  weakenDisjoint (w  ∷ʳ σ) d         = w ∷ₙ weakenDisjoint σ d
  weakenDisjoint (_   ∷ σ) (y   ∷ₙ d) = _ ∷ₙ weakenDisjoint σ d
  weakenDisjoint (zSw ∷ σ) (xRz ∷ₗ d) = rs⇒t xRz zSw ∷ₗ weakenDisjoint σ d
  weakenDisjoint (zSw ∷ σ) (yRz ∷ᵣ d) = rs⇒t yRz zSw ∷ᵣ weakenDisjoint σ d

  -- Lists remain disjoint when elements are removed.

  shrinkDisjoint : ∀ {us vs xs ys zs}
                      (σ₁ : Sublist R us xs) {τ₁ : Sublist S xs zs}
                      (σ₂ : Sublist R vs ys) {τ₂ : Sublist S ys zs} →
                      Disjoint τ₁ τ₂ →
                      Disjoint (trans rs⇒t σ₁ τ₁) (trans rs⇒t σ₂ τ₂)
  shrinkDisjoint σ₁         σ₂ (y   ∷ₙ d) = y ∷ₙ shrinkDisjoint σ₁ σ₂ d
  shrinkDisjoint (x  ∷ʳ σ₁) σ₂ (xSz ∷ₗ d) = _ ∷ₙ shrinkDisjoint σ₁ σ₂ d
  shrinkDisjoint (uRx ∷ σ₁) σ₂ (xSz ∷ₗ d) = rs⇒t uRx xSz ∷ₗ shrinkDisjoint σ₁ σ₂ d
  shrinkDisjoint σ₁ (y  ∷ʳ σ₂) (ySz ∷ᵣ d) = _ ∷ₙ shrinkDisjoint σ₁ σ₂ d
  shrinkDisjoint σ₁ (vRy ∷ σ₂) (ySz ∷ᵣ d) = rs⇒t vRy ySz ∷ᵣ shrinkDisjoint σ₁ σ₂ d
  shrinkDisjoint [] []         []         = []

open DisjointnessMonotonicity public


text:
{-# OPTIONS --without-K #-}

open import HoTT
open import homotopy.JoinComm
open import homotopy.JoinAssocCubical

module homotopy.JoinSusp where

module _ {i} {A : Type i} where

  private

      module Into = PushoutRec {d = *-span (Lift {j = i} Bool) A}
        {D = Suspension A}
        (λ {(lift true) → north _;
            (lift false) → south _})
        (λ _ → south _)
        (λ {(lift true , a) → merid _ a;
            (lift false , a) → idp})

      into = Into.f

      module Out = SuspensionRec A {C = Lift {j = i} Bool * A}
        (left (lift true))
        (left (lift false))
        (λ a → glue (lift true , a) ∙ ! (glue (lift false , a)))

      out = Out.f

      into-out : ∀ σ → into (out σ) == σ
      into-out = Suspension-elim _
        idp
        idp
        (↓-∘=idf-from-square into out ∘ λ a → vert-degen-square $
           ap (ap into) (Out.glue-β a)
           ∙ ap-∙ into (glue (lift true , a)) (! (glue (lift false , a)))
           ∙ (Into.glue-β (lift true , a)
              ∙2 (ap-! into (glue (lift false , a))
                  ∙ ap ! (Into.glue-β (lift false , a))))
           ∙ ∙-unit-r _)

      out-into : ∀ j → out (into j) == j
      out-into = Pushout-elim
        (λ {(lift true) → idp;
            (lift false) → idp})
        (λ a → glue (lift false , a))
        (↓-∘=idf-from-square out into ∘
          λ {(lift true , a) →
                (ap (ap out) (Into.glue-β (lift true , a)) ∙ Out.glue-β a)
                ∙v⊡ (vid-square {p = glue (lift true , a)}
                      ⊡h rt-square (glue (lift false , a)))
                ⊡v∙ ∙-unit-r _;
             (lift false , a) →
               ap (ap out) (Into.glue-β (lift false , a)) ∙v⊡ connection})

  join-S⁰-equiv : Lift {j = i} Bool * A ≃ Suspension A
  join-S⁰-equiv = equiv into out into-out out-into

  join-S⁰-path = ua join-S⁰-equiv

module _ {i} (X : Ptd i) where

  join-S⁰-⊙path : ⊙Sphere {i} 0 ⊙* X == ⊙Susp X
  join-S⁰-⊙path = ⊙ua join-S⁰-equiv idp

module _ {i} {A B : Type i} where

  join-susp-shift : Suspension A * B == Suspension (A * B)
  join-susp-shift =
    ap (λ C → C * B) (! join-S⁰-path)
    ∙ join-rearrange-path
    ∙ ua swap-equiv
    ∙ join-S⁰-path
    ∙ ap Suspension (ua swap-equiv)

module _ {i} (X Y : Ptd i) where

  ⊙join-susp-shift : ⊙Susp X ⊙* Y == ⊙Susp (X ⊙* Y)
  ⊙join-susp-shift =
    ap (λ Z → Z ⊙* Y) (! (join-S⁰-⊙path X))
    ∙ join-rearrange-⊙path (⊙Sphere 0) X Y
    ∙ ⊙ua swap-equiv (! (glue _))
    ∙ join-S⁰-⊙path (Y ⊙* X)
    ∙ ap (λ A → (Suspension A , north _)) (ua swap-equiv)

module _ {i} (X : Ptd i) where

  ⊙join-sphere : (m : ℕ) → ⊙Sphere {i} m ⊙* X == ⊙Susp^ (S m) X
  ⊙join-sphere O = join-S⁰-⊙path X
  ⊙join-sphere (S m) = ⊙join-susp-shift (⊙Sphere m) X
                          ∙ ap ⊙Susp (⊙join-sphere m)

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Simple implementation of sets of ℕ.
--
-- Since ℕ is represented as unary numbers, simply having an ordered list of
-- numbers to represent a set is quite inefficient. For instance, to see if
-- 6 is in the set {1, 3, 4}, we have to do a comparison with 1, then 3, and
-- then 4. But 4 is equal to suc 3, so we should be able to share the work
-- accross those two comparisons.
--
-- This module defines a type that represents {1, 3, 4} as:
--
--   1 ∷ 1 ∷ 0 ∷ []
--
-- i.e. we only store the gaps. When checking if a number (the needle) is in the
-- set (the haystack), we subtract each successive member of the haystack from the
-- needle as we go. For example, to check if 6 is in the above set, we do the
-- following:
--
--   start:                  6 ∈? (1 ∷ 1 ∷ 0 ∷ [])
--   test head:              6 ≟ 1
--   not equal, so continue: (6 - 1 - 1) ∈? (1 ∷ 0 ∷ [])
--   compute:                4 ∈? (1 ∷ 0 ∷ [])
--   test head:              4 ≟ 1
--   not equal, so continue: (4 - 1 - 1) ∈? (0 ∷ [])
--   compute:                2 ∈? (0 ∷ [])
--   test head:              2 ≟ 0
--   not equal, so continue: (2 - 1 - 1) ∈? []
--   empty list:             false
--
-- In this way, we change the membership test from O(n²) to O(n).
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Tactic.RingSolver.Core.NatSet where

open import Data.Nat   as ℕ     using (ℕ; suc; zero)
open import Data.List  as List  using (List; _∷_; [])
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
open import Data.Bool  as Bool  using (Bool)
open import Function
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Helper methods

para : ∀ {a b} {A : Set a} {B : Set b} →
       (A → List A → B → B) → B → List A → B
para f b []       = b
para f b (x ∷ xs) = f x xs (para f b xs)

------------------------------------------------------------------------
-- Definition

NatSet : Set
NatSet = List ℕ

------------------------------------------------------------------------
-- Functions

insert : ℕ → NatSet → NatSet
insert x xs = para f (_∷ []) xs x
  where
  f : ℕ → NatSet → (ℕ → NatSet) → ℕ → NatSet
  f y ys c x with ℕ.compare x y
  ... | ℕ.less x k    = x ∷ k ∷ ys
  ... | ℕ.equal x     = x ∷ ys
  ... | ℕ.greater y k = y ∷ c k

delete : ℕ → NatSet → NatSet
delete x xs = para f (const []) xs x
  where
  f : ℕ → NatSet → (ℕ → NatSet) → ℕ → NatSet
  f y ys c x with ℕ.compare x y
  f y ys c x         | ℕ.less    x k = y ∷ ys
  f y [] c x         | ℕ.equal   x   = []
  f y₁ (y₂ ∷ ys) c x | ℕ.equal   x   = suc x ℕ.+ y₂ ∷ ys
  f y ys c x         | ℕ.greater y k = y ∷ c k

-- Returns the position of the element, if it's present.
lookup : ℕ → NatSet → Maybe ℕ
lookup x xs = List.foldr f (const (const nothing)) xs x 0
  where
  f : ℕ → (ℕ → ℕ → Maybe ℕ) → ℕ → ℕ → Maybe ℕ
  f y ys x i with ℕ.compare x y
  ... | ℕ.less     x k = nothing
  ... | ℕ.equal    y   = just i
  ... | ℕ.greater  y k = ys k (suc i)

member : ℕ → NatSet → Bool
member x = Maybe.is-just ∘ lookup x

fromList : List ℕ → NatSet
fromList = List.foldr insert []

toList : NatSet → List ℕ
toList = List.drop 1 ∘ List.map ℕ.pred ∘ List.scanl (λ x y → suc (y ℕ.+ x)) 0

------------------------------------------------------------------------
-- Tests

private
  example₁ : fromList (4 ∷ 3 ∷ 1 ∷ 0 ∷ 2 ∷ []) ≡ (0 ∷ 0 ∷ 0 ∷ 0 ∷ 0 ∷ [])
  example₁ = refl

  example₂ : lookup 3 (fromList (4 ∷ 3 ∷ 1 ∷ 0 ∷ 2 ∷ [])) ≡ just 3
  example₂ = refl

  example₃ : toList (fromList (4 ∷ 3 ∷ 1 ∷ 0 ∷ 2 ∷ [])) ≡ (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
  example₃ = refl

  example₄ : delete 3 (fromList (4 ∷ 3 ∷ 1 ∷ 2 ∷ [])) ≡ fromList (4 ∷ 1 ∷ 2 ∷ [])
  example₄ = refl

  example₅ : delete 3 (fromList (4 ∷ 1 ∷ 2 ∷ [])) ≡ fromList (4 ∷ 1 ∷ 2 ∷ [])
  example₅ = refl


text:
module Numeral.Natural.Relation.DivisibilityWithRemainder where

import      Lvl
open import Logic
open import Logic.Propositional
open import Numeral.Finite
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Type

-- Divisibility with a remainder.
-- `(y ∣ x)(r)` means that `y` is divisible by `x − r`.
-- Note: `(0 ∣ᵣₑₘ _)(_)` is impossible to construct (0 is never a divisor by this definition).
data _∣ᵣₑₘ_ : (y : ℕ) → ℕ → 𝕟(y) → Stmt{Lvl.𝟎} where
  DivRem𝟎 : ∀{y : ℕ}  {r : 𝕟(y)} → (y ∣ᵣₑₘ 𝕟-to-ℕ(r))(r)
  DivRem𝐒 : ∀{y x : ℕ}{r : 𝕟(y)} → (y ∣ᵣₑₘ x)(r) → (y ∣ᵣₑₘ (x + y))(r)

_∣₊_ : ℕ → ℕ → Stmt
𝟎    ∣₊ x = ⊥
𝐒(y) ∣₊ x = (𝐒(y) ∣ᵣₑₘ x)(𝟎)

-- The quotient extracted from the proof of divisibility.
[∣ᵣₑₘ]-quotient : ∀{y x}{r} → (y ∣ᵣₑₘ x)(r) → ℕ
[∣ᵣₑₘ]-quotient DivRem𝟎     = 𝟎
[∣ᵣₑₘ]-quotient (DivRem𝐒 p) = 𝐒([∣ᵣₑₘ]-quotient p)

-- The remainder extracted from the proof of divisibility.
[∣ᵣₑₘ]-remainder : ∀{y x}{r} → (y ∣ᵣₑₘ x)(r) → 𝕟(y)
[∣ᵣₑₘ]-remainder{r = r} _ = r

data _∣ᵣₑₘ₀_ : (y : ℕ) → ℕ → ℕ → Stmt{Lvl.𝟎} where
  base₀ : ∀{y}    → (y ∣ᵣₑₘ₀ 𝟎)(𝟎)
  base₊ : ∀{y r}  → (y ∣ᵣₑₘ₀ r)(r) → (𝐒(y) ∣ᵣₑₘ₀ 𝐒(r))(𝐒(r))
  step : ∀{y x r} → (y ∣ᵣₑₘ₀ x)(r) → (y ∣ᵣₑₘ₀ (x + y))(r)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Type
open import Logic.Classical as Logic using (Classical)
open import Logic.Predicate as Logic using ()

module Formalization.ClassicalPropositionalLogic.NaturalDeduction.Tree ⦃ classical : ∀{ℓ} → Logic.∀ₗ(Classical{ℓ}) ⦄ where

import      Lvl
open import Logic
open import Sets.PredicateSet using (PredSet ; _∈_ ; _∉_ ; _∪_ ; _∪•_ ; _∖_ ; _⊆_ ; _⊇_ ; ∅ ; [≡]-to-[⊆] ; [≡]-to-[⊇]) renaming (•_ to singleton ; _≡_ to _≡ₛ_)

private variable ℓₚ ℓ ℓ₁ ℓ₂ : Lvl.Level

open import Formalization.ClassicalPropositionalLogic.Syntax

module _ {ℓₚ} {P : Type{ℓₚ}} where
  {-# NO_POSITIVITY_CHECK #-}
  data Tree : Formula(P) → Stmt{Lvl.𝐒(ℓₚ)} where
    [⊤]-intro : Tree(⊤)

    [⊥]-intro : ∀{φ} → Tree(φ) → Tree(¬ φ) → Tree(⊥)
    [⊥]-elim  : ∀{φ} → Tree(⊥) → Tree(φ)

    [¬]-intro : ∀{φ} → (Tree(φ) → Tree(⊥)) → Tree(¬ φ)
    [¬]-elim  : ∀{φ} → (Tree(¬ φ) → Tree(⊥)) → Tree(φ)

    [∧]-intro : ∀{φ ψ} → Tree(φ) → Tree(ψ) → Tree(φ ∧ ψ)
    [∧]-elimₗ : ∀{φ ψ} → Tree(φ ∧ ψ) → Tree(φ)
    [∧]-elimᵣ : ∀{φ ψ} → Tree(φ ∧ ψ) → Tree(ψ)

    [∨]-introₗ : ∀{φ ψ} → Tree(φ) → Tree(φ ∨ ψ)
    [∨]-introᵣ : ∀{φ ψ} → Tree(ψ) → Tree(φ ∨ ψ)
    [∨]-elim   : ∀{φ ψ χ} → (Tree(φ) → Tree(χ)) → (Tree(ψ) → Tree(χ)) → Tree(φ ∨ ψ) → Tree(χ)

    [⟶]-intro : ∀{φ ψ} → (Tree(φ) → Tree(ψ)) → Tree(φ ⟶ ψ)
    [⟶]-elim  : ∀{φ ψ} → Tree(φ) → Tree(φ ⟶ ψ) → Tree(ψ)

    [⟷]-intro : ∀{φ ψ} → (Tree(ψ) → Tree(φ)) → (Tree(φ) → Tree(ψ)) → Tree(ψ ⟷ φ)
    [⟷]-elimₗ : ∀{φ ψ} → Tree(φ) → Tree(ψ ⟷ φ) → Tree(ψ)
    [⟷]-elimᵣ : ∀{φ ψ} → Tree(ψ) → Tree(ψ ⟷ φ) → Tree(φ)

  open import Formalization.ClassicalPropositionalLogic.NaturalDeduction

  module _ {ℓ} where
    Tree-to-[⊢]-tautologies : ∀{φ} → Tree(φ) → (∅{ℓ} ⊢ φ)
    Tree-to-[⊢]-tautologies {.⊤} [⊤]-intro = [⊤]-intro
    Tree-to-[⊢]-tautologies {.⊥} ([⊥]-intro tφ tφ₁) =
      ([⊥]-intro
        (Tree-to-[⊢]-tautologies tφ)
        (Tree-to-[⊢]-tautologies tφ₁)
      )
    Tree-to-[⊢]-tautologies {φ} ([⊥]-elim tφ) =
      ([⊥]-elim
        (Tree-to-[⊢]-tautologies tφ)
      )
    Tree-to-[⊢]-tautologies {.(¬ _)} ([¬]-intro x) = [¬]-intro {!!}
    Tree-to-[⊢]-tautologies {φ} ([¬]-elim x) = {!!}
    Tree-to-[⊢]-tautologies {.(_ ∧ _)} ([∧]-intro tφ tφ₁) =
      ([∧]-intro
        (Tree-to-[⊢]-tautologies tφ)
        (Tree-to-[⊢]-tautologies tφ₁)
      )
    Tree-to-[⊢]-tautologies {φ} ([∧]-elimₗ tφ) =
      ([∧]-elimₗ
        (Tree-to-[⊢]-tautologies tφ)
      )
    Tree-to-[⊢]-tautologies {φ} ([∧]-elimᵣ tφ) =
      ([∧]-elimᵣ
        (Tree-to-[⊢]-tautologies tφ)
      )
    Tree-to-[⊢]-tautologies {.(_ ∨ _)} ([∨]-introₗ tφ) =
      ([∨]-introₗ
        (Tree-to-[⊢]-tautologies tφ)
      )
    Tree-to-[⊢]-tautologies {.(_ ∨ _)} ([∨]-introᵣ tφ) =
      ([∨]-introᵣ
        (Tree-to-[⊢]-tautologies tφ)
      )
    Tree-to-[⊢]-tautologies {φ} ([∨]-elim x x₁ tφ) = {!!}
    Tree-to-[⊢]-tautologies {.(_ ⟶ _)} ([⟶]-intro x) = {!!}
    Tree-to-[⊢]-tautologies {φ} ([⟶]-elim tφ tφ₁) =
      ([⟶]-elim
        (Tree-to-[⊢]-tautologies tφ)
        (Tree-to-[⊢]-tautologies tφ₁)
      )
    Tree-to-[⊢]-tautologies {.(_ ⟷ _)} ([⟷]-intro x x₁) = {!!}
    Tree-to-[⊢]-tautologies {φ} ([⟷]-elimₗ tφ tφ₁) =
      ([⟷]-elimₗ
        (Tree-to-[⊢]-tautologies tφ)
        (Tree-to-[⊢]-tautologies tφ₁)
      )
    Tree-to-[⊢]-tautologies {φ} ([⟷]-elimᵣ tφ tφ₁) =
      ([⟷]-elimᵣ
        (Tree-to-[⊢]-tautologies tφ)
        (Tree-to-[⊢]-tautologies tφ₁)
      )

  --Tree-to-[⊢] : ∀{P : Type{ℓₚ}}{Γ : Formulas(P)}{φ} → ((Γ ⊆ Tree) → Tree(φ)) → (Γ ⊢ φ)
  --Tree-to-[⊢] {Γ} {φ} t = {!!}


text:
record R (A : Set) : Set where
  field
    f : A → A

open module R′ (@0 A : Set) (r : R A) = R {A = A} r

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module Impure.LFRef.Properties.Confluence where

open import Prelude
open import Data.List
open import Extensions.List
open import Extensions.Nat

open import Impure.LFRef.Syntax
open import Impure.LFRef.Eval

private
  val-lemma : ∀ {t} → (v v₁ : Val t)  → v ≡ v₁
  val-lemma loc loc = refl
  val-lemma unit unit = refl
  val-lemma con con = refl

-- A stronger property than Church-Rosser
deterministic : ∀ {𝕊 e e' e'' μ μ' μ''} →
                𝕊 ⊢ e , μ ≻ e' , μ' → 𝕊 ⊢ e , μ ≻ e'' , μ'' →
                ---------------------------------------------
                e' ≡ e'' × μ' ≡ μ''
deterministic (funapp-β x p₁) (funapp-β x' p) with []=-functional _ _ x x'
deterministic (funapp-β x refl) (funapp-β x' refl) | refl = refl , refl
deterministic {μ = μ} (ref-val p) (ref-val q) = refl , cong (λ v → μ ∷ʳ (, v)) (val-lemma p q)
deterministic (ref-val v) (ref-clos ())
deterministic (≔-val p v) (≔-val q w) with <-unique p q | val-lemma v w
... | refl | refl = refl , refl
deterministic (≔-val p v) (≔-clos₁ ())
deterministic (≔-val p v) (≔-clos₂ _ ())
deterministic {μ = μ} (!-val p) (!-val q) = (cong (λ v → tm (!load μ v)) (<-unique p q)) , refl
deterministic (!-val p) (!-clos ())
deterministic (ref-clos ()) (ref-val v)
deterministic (ref-clos p) (ref-clos q) with deterministic p q
... | refl , refl = refl , refl
deterministic (!-clos ()) (!-val p)
deterministic (!-clos p) (!-clos q) with deterministic p q
... | refl , refl = refl , refl
deterministic (≔-clos₁ ()) (≔-val p v)
deterministic (≔-clos₁ p) (≔-clos₁ q) with deterministic p q
... | refl , refl = refl , refl
deterministic (≔-clos₁ ()) (≔-clos₂ (tm x) q)
deterministic (≔-clos₂ (tm x) p) (≔-clos₁ ())
deterministic (≔-clos₂ _ ()) (≔-val p v)
deterministic (≔-clos₂ _ p) (≔-clos₂ _ q) with deterministic p q
... | refl , refl = refl , refl

deterministic-seq : ∀ {𝕊 e e' e'' μ μ' μ''} →
                𝕊 ⊢ e , μ ≻ₛ e' , μ' →
                𝕊 ⊢ e , μ ≻ₛ e'' , μ'' →
                ---------------------------------------------
                e' ≡ e'' × μ' ≡ μ''
deterministic-seq lett-β lett-β = refl , refl
deterministic-seq lett-β (lett-clos ())
deterministic-seq (lett-clos ()) lett-β
deterministic-seq (lett-clos p) (lett-clos q) with deterministic p q
... | refl , refl = refl , refl
deterministic-seq (ret-clos x) (ret-clos x') with deterministic x x'
... | refl , refl = refl , refl

open import Data.Star
confluence : ∀ {𝕊 e e' e'' μ μ' μ''} →
             𝕊 ⊢ e , μ ≻⋆ e' , μ' → 𝕊 ⊢ e , μ ≻⋆ e'' , μ'' →
             SeqExpVal e' → SeqExpVal e'' →
             -----------------------------------------------
             e' ≡ e'' × μ' ≡ μ''
confluence ε ε z y = refl , refl
confluence ε (ret-clos () ◅ _) (ret-tm _) _
confluence (ret-clos () ◅ _) ε _ (ret-tm _)
confluence (lett-β ◅ _) ε _ ()
confluence (lett-clos _ ◅ _) ε _ ()
confluence (x ◅ p) (x' ◅ p') v w with deterministic-seq x x'
... | refl , refl with confluence p p' v w
... | refl , refl = refl , refl


text:
{- Basic theory about transport:

- transport is invertible
- transport is an equivalence ([transportEquiv])

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Transport where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.GroupoidLaws

-- Direct definition of transport filler, note that we have to
-- explicitly tell Agda that the type is constant (like in CHM)
transpFill : ∀ {ℓ} {A : Type ℓ}
             (φ : I)
             (A : (i : I) → Type ℓ [ φ ↦ (λ _ → A) ])
             (u0 : outS (A i0))
           → --------------------------------------
             PathP (λ i → outS (A i)) u0 (transp (λ i → outS (A i)) φ u0)
transpFill φ A u0 i = transp (λ j → outS (A (i ∧ j))) (~ i ∨ φ) u0

transport⁻ : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → B → A
transport⁻ p = transport (λ i → p (~ i))

subst⁻ : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (B : A → Type ℓ') (p : x ≡ y) → B y → B x
subst⁻ B p pa = transport⁻ (λ i → B (p i)) pa

transport-fillerExt : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B)
                    → PathP (λ i → A → p i) (λ x → x) (transport p)
transport-fillerExt p i x = transport-filler p x i

transport⁻-fillerExt : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B)
                     → PathP (λ i → p i → A) (λ x → x) (transport⁻ p)
transport⁻-fillerExt p i x = transp (λ j → p (i ∧ ~ j)) (~ i) x

transport-fillerExt⁻ : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B)
                    → PathP (λ i → p i → B) (transport p) (λ x → x)
transport-fillerExt⁻ p = symP (transport⁻-fillerExt (sym p))

transport⁻-fillerExt⁻ : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B)
                     → PathP (λ i → B → p i) (transport⁻ p) (λ x → x)
transport⁻-fillerExt⁻ p = symP (transport-fillerExt (sym p))

transport⁻-filler : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) (x : B)
                   → PathP (λ i → p (~ i)) x (transport⁻ p x)
transport⁻-filler p x = transport-filler (λ i → p (~ i)) x

transport⁻Transport : ∀ {ℓ} {A B : Type ℓ} → (p : A ≡ B) → (a : A) →
                          transport⁻ p (transport p a) ≡ a
transport⁻Transport p a j = transport⁻-fillerExt p (~ j) (transport-fillerExt p (~ j) a)

transportTransport⁻ : ∀ {ℓ} {A B : Type ℓ} → (p : A ≡ B) → (b : B) →
                        transport p (transport⁻ p b) ≡ b
transportTransport⁻ p b j = transport-fillerExt⁻ p j (transport⁻-fillerExt⁻ p j b)

-- Transport is an equivalence
isEquivTransport : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) → isEquiv (transport p)
isEquivTransport {A = A} {B = B} p =
  transport (λ i → isEquiv (transport-fillerExt p i)) (idIsEquiv A)

transportEquiv : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → A ≃ B
transportEquiv p = (transport p , isEquivTransport p)

substEquiv : ∀ {ℓ ℓ'} {A B : Type ℓ} (P : Type ℓ → Type ℓ') (p : A ≡ B) → P A ≃ P B
substEquiv P p = (subst P p , isEquivTransport (λ i → P (p i)))

liftEquiv : ∀ {ℓ ℓ'} {A B : Type ℓ} (P : Type ℓ → Type ℓ') (e : A ≃ B) → P A ≃ P B
liftEquiv P e = substEquiv P (ua e)

transpEquiv : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) → ∀ i → p i ≃ B
transpEquiv P i .fst = transp (λ j → P (i ∨ j)) i
transpEquiv P i .snd
  = transp (λ k → isEquiv (transp (λ j → P (i ∨ (j ∧ k))) (i ∨ ~ k)))
      i (idIsEquiv (P i))

uaTransportη : ∀ {ℓ} {A B : Type ℓ} (P : A ≡ B) → ua (transportEquiv P) ≡ P
uaTransportη P i j
  = Glue (P i1) λ where
      (j = i0) → P i0 , transportEquiv P
      (i = i1) → P j , transpEquiv P j
      (j = i1) → P i1 , idEquiv (P i1)

pathToIso : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → Iso A B
pathToIso x = iso (transport x) (transport⁻ x) (transportTransport⁻ x) (transport⁻Transport x)

isInjectiveTransport : ∀ {ℓ : Level} {A B : Type ℓ} {p q : A ≡ B}
  → transport p ≡ transport q → p ≡ q
isInjectiveTransport {p = p} {q} α i =
  hcomp
    (λ j → λ
      { (i = i0) → secEq univalence p j
      ; (i = i1) → secEq univalence q j
      })
    (invEq univalence ((λ a → α i a) , t i))
  where
  t : PathP (λ i → isEquiv (λ a → α i a)) (pathToEquiv p .snd) (pathToEquiv q .snd)
  t = isProp→PathP (λ i → isPropIsEquiv (λ a → α i a)) _ _

transportUaInv : ∀ {ℓ} {A B : Type ℓ} (e : A ≃ B) → transport (ua (invEquiv e)) ≡ transport (sym (ua e))
transportUaInv e = cong transport (uaInvEquiv e)
-- notice that transport (ua e) would reduce, thus an alternative definition using EquivJ can give
-- refl for the case of idEquiv:
-- transportUaInv e = EquivJ (λ _ e → transport (ua (invEquiv e)) ≡ transport (sym (ua e))) refl e

isSet-subst : ∀ {ℓ ℓ′} {A : Type ℓ} {B : A → Type ℓ′}
                → (isSet-A : isSet A)
                → ∀ {a : A}
                → (p : a ≡ a) → (x : B a) → subst B p x ≡ x
isSet-subst {B = B} isSet-A p x = subst (λ p′ → subst B p′ x ≡ x) (isSet-A _ _ refl p) (substRefl {B = B} x)

-- substituting along a composite path is equivalent to substituting twice
substComposite : ∀ {ℓ ℓ′} {A : Type ℓ} → (B : A → Type ℓ′)
                 → {x y z : A} (p : x ≡ y) (q : y ≡ z) (u : B x)
                 → subst B (p ∙ q) u ≡ subst B q (subst B p u)
substComposite B p q Bx i =
  transport (cong B (compPath-filler' p q (~ i))) (transport-fillerExt (cong B p) i Bx)

-- substitution commutes with morphisms in slices
substCommSlice : ∀ {ℓ ℓ′} {A : Type ℓ}
                   → (B C : A → Type ℓ′)
                   → (F : ∀ i → B i → C i)
                   → {x y : A} (p : x ≡ y) (u : B x)
                   → subst C p (F x u) ≡ F y (subst B p u)
substCommSlice B C F p Bx i =
  transport-fillerExt⁻ (cong C p) i (F _ (transport-fillerExt (cong B p) i Bx))

-- transports between loop spaces preserve path composition
overPathFunct : ∀ {ℓ} {A : Type ℓ} {x y : A} (p q : x ≡ x) (P : x ≡ y)
           → transport (λ i → P i ≡ P i) (p ∙ q)
            ≡ transport (λ i → P i ≡ P i) p ∙ transport (λ i → P i ≡ P i) q
overPathFunct p q =
  J (λ y P → transport (λ i → P i ≡ P i) (p ∙ q) ≡ transport (λ i → P i ≡ P i) p ∙ transport (λ i → P i ≡ P i) q)
    (transportRefl (p ∙ q) ∙ cong₂ _∙_ (sym (transportRefl p)) (sym (transportRefl q)))

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical