text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of unique lists (setoid equality)
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.Unique.Propositional.Properties where

open import Data.Fin.Base using (Fin)
open import Data.List.Base
open import Data.List.Relation.Binary.Disjoint.Propositional
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
open import Data.List.Relation.Unary.Unique.Propositional
import Data.List.Relation.Unary.Unique.Setoid.Properties as Setoid
open import Data.Nat.Base
open import Data.Nat.Properties using (<⇒≢)
open import Function using (id; _∘_)
open import Relation.Binary using (Rel; Setoid)
open import Relation.Binary.PropositionalEquality
  using (_≡_; _≢_; sym; setoid)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary using (¬_)

------------------------------------------------------------------------
-- Introduction (⁺) and elimination (⁻) rules for list operations
------------------------------------------------------------------------
-- map

module _ {a b} {A : Set a} {B : Set b} where

  map⁺ : ∀ {f} → (∀ {x y} → f x ≡ f y → x ≡ y) →
         ∀ {xs} → Unique xs → Unique (map f xs)
  map⁺ = Setoid.map⁺ (setoid A) (setoid B)

------------------------------------------------------------------------
-- ++

module _ {a} {A : Set a} where

  ++⁺ : ∀ {xs ys} → Unique xs → Unique ys → Disjoint xs ys → Unique (xs ++ ys)
  ++⁺ = Setoid.++⁺ (setoid A)

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

module _ {a} {A : Set a} where

  concat⁺ : ∀ {xss} → All Unique xss → AllPairs Disjoint xss → Unique (concat xss)
  concat⁺ = Setoid.concat⁺ (setoid A)

------------------------------------------------------------------------
-- take & drop

module _ {a} {A : Set a} where

  drop⁺ : ∀ {xs} n → Unique xs → Unique (drop n xs)
  drop⁺ = Setoid.drop⁺ (setoid A)

  take⁺ : ∀ {xs} n → Unique xs → Unique (take n xs)
  take⁺ = Setoid.take⁺ (setoid A)

------------------------------------------------------------------------
-- applyUpTo & upTo

module _ {a} {A : Set a} where

  applyUpTo⁺₁ : ∀ f n → (∀ {i j} → i < j → j < n → f i ≢ f j) →
                Unique (applyUpTo f n)
  applyUpTo⁺₁ = Setoid.applyUpTo⁺₁ (setoid A)

  applyUpTo⁺₂ : ∀ f n → (∀ i j → f i ≢ f j) →
                Unique (applyUpTo f n)
  applyUpTo⁺₂ = Setoid.applyUpTo⁺₂  (setoid A)

------------------------------------------------------------------------
-- upTo

upTo⁺ : ∀ n → Unique (upTo n)
upTo⁺ n = applyUpTo⁺₁ id n (λ i<j _ → <⇒≢ i<j)

------------------------------------------------------------------------
-- applyDownFrom

module _ {a} {A : Set a} where

  applyDownFrom⁺₁ : ∀ f n → (∀ {i j} → j < i → i < n → f i ≢ f j) →
                    Unique (applyDownFrom f n)
  applyDownFrom⁺₁ = Setoid.applyDownFrom⁺₁ (setoid A)

  applyDownFrom⁺₂ : ∀ f n → (∀ i j → f i ≢ f j) →
                    Unique (applyDownFrom f n)
  applyDownFrom⁺₂ = Setoid.applyDownFrom⁺₂ (setoid A)

------------------------------------------------------------------------
-- downFrom

downFrom⁺ : ∀ n → Unique (downFrom n)
downFrom⁺ n = applyDownFrom⁺₁ id n (λ j<i _ → <⇒≢ j<i ∘ sym)

------------------------------------------------------------------------
-- tabulate

module _ {a} {A : Set a} where

  tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → f i ≡ f j → i ≡ j) →
              Unique (tabulate f)
  tabulate⁺ = Setoid.tabulate⁺ (setoid A)

------------------------------------------------------------------------
-- allFin

allFin⁺ : ∀ n → Unique (allFin n)
allFin⁺ n = tabulate⁺ id

------------------------------------------------------------------------
-- filter

module _ {a p} {A : Set a} {P : Pred _ p} (P? : Decidable P) where

  filter⁺ : ∀ {xs} → Unique xs → Unique (filter P? xs)
  filter⁺ = Setoid.filter⁺ (setoid A) P?


text:
------------------------------------------------------------------------
-- Properties of functions, such as associativity and commutativity
------------------------------------------------------------------------

-- These properties can (for instance) be used to define algebraic
-- structures.

open import Relation.Binary

-- The properties are specified using the following relation as
-- "equality".

module Algebra.FunctionProperties {A} (_≈_ : Rel A) where

open import Data.Product

------------------------------------------------------------------------
-- Unary and binary operations

open import Algebra.FunctionProperties.Core public

------------------------------------------------------------------------
-- Properties of operations

Associative : Op₂ A → Set
Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))

Commutative : Op₂ A → Set
Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x)

LeftIdentity : A → Op₂ A → Set
LeftIdentity e _∙_ = ∀ x → (e ∙ x) ≈ x

RightIdentity : A → Op₂ A → Set
RightIdentity e _∙_ = ∀ x → (x ∙ e) ≈ x

Identity : A → Op₂ A → Set
Identity e ∙ = LeftIdentity e ∙ × RightIdentity e ∙

LeftZero : A → Op₂ A → Set
LeftZero z _∙_ = ∀ x → (z ∙ x) ≈ z

RightZero : A → Op₂ A → Set
RightZero z _∙_ = ∀ x → (x ∙ z) ≈ z

Zero : A → Op₂ A → Set
Zero z ∙ = LeftZero z ∙ × RightZero z ∙

LeftInverse : A → Op₁ A → Op₂ A → Set
LeftInverse e _⁻¹ _∙_ = ∀ x → (x ⁻¹ ∙ x) ≈ e

RightInverse : A → Op₁ A → Op₂ A → Set
RightInverse e _⁻¹ _∙_ = ∀ x → (x ∙ (x ⁻¹)) ≈ e

Inverse : A → Op₁ A → Op₂ A → Set
Inverse e ⁻¹ ∙ = LeftInverse e ⁻¹ ∙ × RightInverse e ⁻¹ ∙

_DistributesOverˡ_ : Op₂ A → Op₂ A → Set
_*_ DistributesOverˡ _+_ =
  ∀ x y z → (x * (y + z)) ≈ ((x * y) + (x * z))

_DistributesOverʳ_ : Op₂ A → Op₂ A → Set
_*_ DistributesOverʳ _+_ =
  ∀ x y z → ((y + z) * x) ≈ ((y * x) + (z * x))

_DistributesOver_ : Op₂ A → Op₂ A → Set
* DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)

_IdempotentOn_ : Op₂ A → A → Set
_∙_ IdempotentOn x = (x ∙ x) ≈ x

Idempotent : Op₂ A → Set
Idempotent ∙ = ∀ x → ∙ IdempotentOn x

IdempotentFun : Op₁ A → Set
IdempotentFun f = ∀ x → f (f x) ≈ f x

_Absorbs_ : Op₂ A → Op₂ A → Set
_∙_ Absorbs _∘_ = ∀ x y → (x ∙ (x ∘ y)) ≈ x

Absorptive : Op₂ A → Op₂ A → Set
Absorptive ∙ ∘ = (∙ Absorbs ∘) × (∘ Absorbs ∙)

Involutive : Op₁ A → Set
Involutive f = ∀ x → f (f x) ≈ x

ext: agda

max_issues_repo_name: larrytheliquid/Lemmachine


text:
------------------------------------------------------------------------
-- A type soundness result
------------------------------------------------------------------------

open import Prelude
open import Prelude.Size

import Lambda.Syntax

module Lambda.Type-soundness
  {Name : Type}
  (open Lambda.Syntax Name)
  (open Closure Tm)
  (def : Name → Tm 1)
  (Σ : Name → Ty ∞ × Ty ∞)
  where

open import Equality.Propositional

open import Function-universe equality-with-J
open import Maybe equality-with-J
open import Monad equality-with-J
open import Vec.Data equality-with-J

open import Delay-monad.Always
open import Delay-monad.Bisimilarity

open import Lambda.Delay-crash
open import Lambda.Interpreter def

-- WF-Value, WF-Env and WF-MV specify when a
-- value/environment/potential value is well-formed with respect to a
-- given context (and type).

mutual

  data WF-Value : Ty ∞ → Value → Type where
    lam   : ∀ {n Γ σ τ} {t : Tm (1 + n)} {ρ} →
            Σ , force σ ∷ Γ ⊢ t ∈ force τ →
            WF-Env Γ ρ →
            WF-Value (σ ⇾′ τ) (lam t ρ)
    con   : ∀ b → WF-Value bool (con b)

  WF-Env : ∀ {n} → Ctxt n → Env n → Type
  WF-Env Γ ρ = ∀ x → WF-Value (index Γ x) (index ρ x)

WF-MV : Ty ∞ → Maybe Value → Type
WF-MV σ v = maybe (WF-Value σ) Prelude.⊥ v

-- Some "constructors" for WF-Env.

[]-wf : WF-Env [] []
[]-wf ()

infixr 5 _∷-wf_

_∷-wf_ : ∀ {n} {Γ : Ctxt n} {ρ σ v} →
         WF-Value σ v → WF-Env Γ ρ → WF-Env (σ ∷ Γ) (v ∷ ρ)
(v-wf ∷-wf ρ-wf) fzero    = v-wf
(v-wf ∷-wf ρ-wf) (fsuc x) = ρ-wf x

-- If we can prove □ ∞ (WF-MV σ) (run x), then x does not "go wrong".

does-not-go-wrong : ∀ {σ} {x : Delay-crash Value ∞} →
                    □ ∞ (WF-MV σ) x → ¬ x ≈ crash
does-not-go-wrong (now {x = nothing} ())
does-not-go-wrong (now {x = just x} x-wf) ()
does-not-go-wrong (later x-wf)            (laterˡ x↯) =
  does-not-go-wrong (force x-wf) x↯

-- A "constructor" for □ i ∘ WF-MV.

_>>=-wf_ :
  ∀ {i σ τ} {x : Delay-crash Value ∞} {f : Value → Delay-crash Value ∞} →
  □ i (WF-MV σ) x →
  (∀ {v} → WF-Value σ v → □ i (WF-MV τ) (f v)) →
  □ i (WF-MV τ) (x >>= f)
x-wf >>=-wf f-wf =
  □->>= x-wf λ { {nothing} ()
               ; {just v}  v-wf → f-wf v-wf
               }

-- Well-typed programs do not "go wrong".

module _ (def∈ : (f : Name) →
                 Σ , proj₁ (Σ f) ∷ [] ⊢ def f ∈ proj₂ (Σ f)) where

  mutual

    ⟦⟧-wf : ∀ {i n Γ} (t : Tm n) {σ} → Σ , Γ ⊢ t ∈ σ →
            ∀ {ρ} → WF-Env Γ ρ →
            □ i (WF-MV σ) (⟦ t ⟧ ρ)
    ⟦⟧-wf (var x)   var         ρ-wf = now (ρ-wf x)
    ⟦⟧-wf (lam t)   (lam t∈)    ρ-wf = now (lam t∈ ρ-wf)
    ⟦⟧-wf (t₁ · t₂) (t₁∈ · t₂∈) ρ-wf =
      ⟦⟧-wf t₁ t₁∈ ρ-wf >>=-wf λ f-wf →
      ⟦⟧-wf t₂ t₂∈ ρ-wf >>=-wf λ v-wf →
      ∙-wf f-wf v-wf
    ⟦⟧-wf (call f t) (call t∈) ρ-wf =
      ⟦⟧-wf t t∈ ρ-wf >>=-wf λ v-wf →
      ∙-wf {σ = λ { .force → proj₁ (Σ f) }}
           {τ = λ { .force → proj₂ (Σ f) }}
           (lam (def∈ f) []-wf) v-wf
    ⟦⟧-wf (con b)       con              ρ-wf = now (con b)
    ⟦⟧-wf (if t₁ t₂ t₃) (if t₁∈ t₂∈ t₃∈) ρ-wf =
      ⟦⟧-wf t₁ t₁∈ ρ-wf >>=-wf λ v₁-wf →
      ⟦if⟧-wf v₁-wf t₂∈ t₃∈ ρ-wf

    ∙-wf : ∀ {i σ τ f v} →
           WF-Value (σ ⇾′ τ) f → WF-Value (force σ) v →
           □ i (WF-MV (force τ)) (f ∙ v)
    ∙-wf (lam t₁∈ ρ₁-wf) v₂-wf =
      later λ { .force → ⟦⟧-wf _ t₁∈ (v₂-wf ∷-wf ρ₁-wf) }

    ⟦if⟧-wf : ∀ {i n Γ σ v} {t₂ t₃ : Tm n} →
              WF-Value bool v →
              Σ , Γ ⊢ t₂ ∈ σ →
              Σ , Γ ⊢ t₃ ∈ σ →
              ∀ {ρ} → WF-Env Γ ρ →
              □ i (WF-MV σ) (⟦if⟧ v t₂ t₃ ρ)
    ⟦if⟧-wf (con true)  t₂∈ t₃∈ ρ-wf = ⟦⟧-wf _ t₂∈ ρ-wf
    ⟦if⟧-wf (con false) t₂∈ t₃∈ ρ-wf = ⟦⟧-wf _ t₃∈ ρ-wf

  type-soundness : ∀ {t : Tm 0} {σ} →
                   Σ , [] ⊢ t ∈ σ → ¬ ⟦ t ⟧ [] ≈ crash
  type-soundness {t = t} {σ} =
    Σ , [] ⊢ t ∈ σ            ↝⟨ (λ t∈ → ⟦⟧-wf _ t∈ []-wf) ⟩
    □ ∞ (WF-MV σ) (⟦ t ⟧ [])  ↝⟨ does-not-go-wrong ⟩□
    ¬ ⟦ t ⟧ [] ≈ crash        □

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
open import Common.Prelude

test : Nat → Nat
test = __+ 2

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-

This file contains:

- Eliminator for propositional truncation

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.PropositionalTruncation.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation.Base

private
  variable
    ℓ : Level
    A B C : Type ℓ

∥∥-isPropDep : (P : A → Type ℓ) → isOfHLevelDep 1 (λ x → ∥ P x ∥)
∥∥-isPropDep P = isOfHLevel→isOfHLevelDep 1 (λ _ → squash)

rec : {P : Type ℓ} → isProp P → (A → P) → ∥ A ∥ → P
rec Pprop f ∣ x ∣ = f x
rec Pprop f (squash x y i) = Pprop (rec Pprop f x) (rec Pprop f y) i

rec2 : {P : Type ℓ} → isProp P → (A → B → P) → ∥ A ∥ → ∥ B ∥ → P
rec2 Pprop f ∣ x ∣ ∣ y ∣ = f x y
rec2 Pprop f ∣ x ∣ (squash y z i) = Pprop (rec2 Pprop f ∣ x ∣ y) (rec2 Pprop f ∣ x ∣ z) i
rec2 Pprop f (squash x y i) z = Pprop (rec2 Pprop f x z) (rec2 Pprop f y z) i

-- Old version
-- rec2 : ∀ {P : Type ℓ} → isProp P → (A → A → P) → ∥ A ∥ → ∥ A ∥ → P
-- rec2 Pprop f = rec (isProp→ Pprop) (λ a → rec Pprop (f a))

elim : {P : ∥ A ∥ → Type ℓ} → ((a : ∥ A ∥) → isProp (P a))
     → ((x : A) → P ∣ x ∣) → (a : ∥ A ∥) → P a
elim Pprop f ∣ x ∣ = f x
elim Pprop f (squash x y i) =
  isOfHLevel→isOfHLevelDep 1 Pprop
    (elim Pprop f x) (elim Pprop f y) (squash x y) i

elim2 : {P : ∥ A ∥ → ∥ A ∥ → Type ℓ}
        (Bset : ((x y : ∥ A ∥) → isProp (P x y)))
        (f : (a b : A) → P ∣ a ∣ ∣ b ∣)
        (x y : ∥ A ∥) → P x y
elim2 Pprop f = elim (λ _ → isPropΠ (λ _ → Pprop _ _))
                     (λ a → elim (λ _ → Pprop _ _) (f a))

elim3 : {P : ∥ A ∥ → ∥ A ∥ → ∥ A ∥ → Type ℓ}
        (Bset : ((x y z : ∥ A ∥) → isProp (P x y z)))
        (g : (a b c : A) → P (∣ a ∣) ∣ b ∣ ∣ c ∣)
        (x y z : ∥ A ∥) → P x y z
elim3 Pprop g = elim2 (λ _ _ → isPropΠ (λ _ → Pprop _ _ _))
                      (λ a b → elim (λ _ → Pprop _ _ _) (g a b))

propTruncIsProp : isProp ∥ A ∥
propTruncIsProp x y = squash x y

propTruncIdempotent≃ : isProp A → ∥ A ∥ ≃ A
propTruncIdempotent≃ {A = A} hA = isoToEquiv f
  where
  f : Iso ∥ A ∥ A
  Iso.fun f        = rec hA (idfun A)
  Iso.inv f x      = ∣ x ∣
  Iso.rightInv f _ = refl
  Iso.leftInv f    = elim (λ _ → isProp→isSet propTruncIsProp _ _) (λ _ → refl)

propTruncIdempotent : isProp A → ∥ A ∥ ≡ A
propTruncIdempotent hA = ua (propTruncIdempotent≃ hA)

-- We could also define the eliminator using the recursor
elim' : {P : ∥ A ∥ → Type ℓ} → ((a : ∥ A ∥) → isProp (P a)) →
        ((x : A) → P ∣ x ∣) → (a : ∥ A ∥) → P a
elim' {P = P} Pprop f a =
  rec (Pprop a) (λ x → transp (λ i → P (squash ∣ x ∣ a i)) i0 (f x)) a

map : (A → B) → (∥ A ∥ → ∥ B ∥)
map f = rec squash (∣_∣ ∘ f)

map2 : (A → B → C) → (∥ A ∥ → ∥ B ∥ → ∥ C ∥)
map2 f = rec (isPropΠ λ _ → squash) (map ∘ f)

-- The propositional truncation can be eliminated into non-propositional
-- types as long as the function used in the eliminator is 'coherently
-- constant.' The details of this can be found in the following paper:
--
--   https://arxiv.org/pdf/1411.2682.pdf
module SetElim (Bset : isSet B) where
  Bset' : isSet' B
  Bset' = isSet→isSet' Bset

  rec→Set : (f : A → B) (kf : 2-Constant f) → ∥ A ∥ → B
  helper  : (f : A → B) (kf : 2-Constant f) → (t u : ∥ A ∥)
          → rec→Set f kf t ≡ rec→Set f kf u

  rec→Set f kf ∣ x ∣ = f x
  rec→Set f kf (squash t u i) = helper f kf t u i

  helper f kf ∣ x ∣ ∣ y ∣ = kf x y
  helper f kf (squash t u i) v
    = Bset' (helper f kf t v) (helper f kf u v) (helper f kf t u) refl i
  helper f kf t (squash u v i)
    = Bset' (helper f kf t u) (helper f kf t v) refl (helper f kf u v) i

  kcomp : (f : ∥ A ∥ → B) → 2-Constant (f ∘ ∣_∣)
  kcomp f x y = cong f (squash ∣ x ∣ ∣ y ∣)

  Fset : isSet (A → B)
  Fset = isSetΠ (const Bset)

  Kset : (f : A → B) → isSet (2-Constant f)
  Kset f = isSetΠ (λ _ → isSetΠ (λ _ → isProp→isSet (Bset _ _)))

  setRecLemma
    : (f : ∥ A ∥ → B)
    → rec→Set (f ∘ ∣_∣) (kcomp f) ≡ f
  setRecLemma f i t
    = elim {P = λ t → rec→Set (f ∘ ∣_∣) (kcomp f) t ≡ f t}
        (λ t → Bset _ _) (λ x → refl) t i

  mkKmap : (∥ A ∥ → B) → Σ (A → B) 2-Constant
  mkKmap f = f ∘ ∣_∣ , kcomp f

  fib : (g : Σ (A → B) 2-Constant) → fiber mkKmap g
  fib (g , kg) = rec→Set g kg , refl

  eqv : (g : Σ (A → B) 2-Constant) → ∀ fi → fib g ≡ fi
  eqv g (f , p) =
    Σ≡Prop (λ f → isOfHLevelΣ 2 Fset Kset _ _)
      (cong (uncurry rec→Set) (sym p) ∙ setRecLemma f)

  trunc→Set≃ : (∥ A ∥ → B) ≃ (Σ (A → B) 2-Constant)
  trunc→Set≃ .fst = mkKmap
  trunc→Set≃ .snd .equiv-proof g = fib g , eqv g

  -- The strategy of this equivalence proof follows the paper more closely.
  -- It is used further down for the groupoid version, because the above
  -- strategy does not generalize so easily.
  e : B → Σ (A → B) 2-Constant
  e b = const b , λ _ _ → refl

  eval : A → (γ : Σ (A → B) 2-Constant) → B
  eval a₀ (g , _) = g a₀

  e-eval : ∀ (a₀ : A) γ → e (eval a₀ γ) ≡ γ
  e-eval a₀ (g , kg) i .fst a₁ = kg a₀ a₁ i
  e-eval a₀ (g , kg) i .snd a₁ a₂ = Bset' refl (kg a₁ a₂) (kg a₀ a₁) (kg a₀ a₂) i

  e-isEquiv : A → isEquiv (e {A = A})
  e-isEquiv a₀ = isoToIsEquiv (iso e (eval a₀) (e-eval a₀) λ _ → refl)

  preEquiv₁ : ∥ A ∥ → B ≃ Σ (A → B) 2-Constant
  preEquiv₁ t = e , rec (isPropIsEquiv e) e-isEquiv t

  preEquiv₂ : (∥ A ∥ → Σ (A → B) 2-Constant) ≃ Σ (A → B) 2-Constant
  preEquiv₂ = isoToEquiv (iso to const (λ _ → refl) retr)
    where
    to : (∥ A ∥ → Σ (A → B) 2-Constant) → Σ (A → B) 2-Constant
    to f .fst x = f ∣ x ∣ .fst x
    to f .snd x y i = f (squash ∣ x ∣ ∣ y ∣ i) .snd x y i

    retr : retract to const
    retr f i t .fst x = f (squash ∣ x ∣ t i) .fst x
    retr f i t .snd x y
      = Bset'
          (λ j → f (squash ∣ x ∣ ∣ y ∣ j) .snd x y j)
          (f t .snd x y)
          (λ j → f (squash ∣ x ∣ t j) .fst x)
          (λ j → f (squash ∣ y ∣ t j) .fst y)
          i

  trunc→Set≃₂ : (∥ A ∥ → B) ≃ Σ (A → B) 2-Constant
  trunc→Set≃₂ = compEquiv (equivΠCod preEquiv₁) preEquiv₂

open SetElim public using (rec→Set; trunc→Set≃)

elim→Set
  : {P : ∥ A ∥ → Type ℓ}
  → (∀ t → isSet (P t))
  → (f : (x : A) → P ∣ x ∣)
  → (kf : ∀ x y → PathP (λ i → P (squash ∣ x ∣ ∣ y ∣ i)) (f x) (f y))
  → (t : ∥ A ∥) → P t
elim→Set {A = A} {P = P} Pset f kf t
  = rec→Set (Pset t) g gk t
  where
  g : A → P t
  g x = transp (λ i → P (squash ∣ x ∣ t i)) i0 (f x)

  gk : 2-Constant g
  gk x y i = transp (λ j → P (squash (squash ∣ x ∣ ∣ y ∣ i) t j)) i0 (kf x y i)

RecHProp : (P : A → hProp ℓ) (kP : ∀ x y → P x ≡ P y) → ∥ A ∥ → hProp ℓ
RecHProp P kP = rec→Set isSetHProp P kP

module GpdElim (Bgpd : isGroupoid B) where
  Bgpd' : isGroupoid' B
  Bgpd' = isGroupoid→isGroupoid' Bgpd

  module _ (f : A → B) (3kf : 3-Constant f) where
    open 3-Constant 3kf

    rec→Gpd : ∥ A ∥ → B
    pathHelper : (t u : ∥ A ∥) → rec→Gpd t ≡ rec→Gpd u
    triHelper₁
      : (t u v : ∥ A ∥)
      → Square (pathHelper t u) (pathHelper t v) refl (pathHelper u v)
    triHelper₂
      : (t u v : ∥ A ∥)
      → Square (pathHelper t v) (pathHelper u v) (pathHelper t u) refl

    rec→Gpd ∣ x ∣ = f x
    rec→Gpd (squash t u i) = pathHelper t u i

    pathHelper ∣ x ∣ ∣ y ∣ = link x y
    pathHelper (squash t u j) v = triHelper₂ t u v j
    pathHelper ∣ x ∣ (squash u v j) = triHelper₁ ∣ x ∣ u v j

    triHelper₁ ∣ x ∣ ∣ y ∣ ∣ z ∣ = coh₁ x y z
    triHelper₁ (squash s t i) u v
      = Bgpd'
          (triHelper₁ s u v)
          (triHelper₁ t u v)
          (triHelper₂ s t u)
          (triHelper₂ s t v)
          (λ i → refl)
          (λ i → pathHelper u v)
          i
    triHelper₁ ∣ x ∣ (squash t u i) v
      = Bgpd'
          (triHelper₁ ∣ x ∣ t v)
          (triHelper₁ ∣ x ∣ u v)
          (triHelper₁ ∣ x ∣ t u)
          (λ i → pathHelper ∣ x ∣ v)
          (λ i → refl)
          (triHelper₂ t u v)
          i
    triHelper₁ ∣ x ∣ ∣ y ∣ (squash u v i)
      = Bgpd'
          (triHelper₁ ∣ x ∣ ∣ y ∣ u)
          (triHelper₁ ∣ x ∣ ∣ y ∣ v)
          (λ i → link x y)
          (triHelper₁ ∣ x ∣ u v)
          (λ i → refl)
          (triHelper₁ ∣ y ∣ u v)
          i

    triHelper₂ ∣ x ∣ ∣ y ∣ ∣ z ∣ = coh₂ x y z
    triHelper₂ (squash s t i) u v
      = Bgpd'
          (triHelper₂ s u v)
          (triHelper₂ t u v)
          (triHelper₂ s t v)
          (λ i → pathHelper u v)
          (triHelper₂ s t u)
          (λ i → refl)
          i
    triHelper₂ ∣ x ∣ (squash t u i) v
      = Bgpd'
          (triHelper₂ ∣ x ∣ t v)
          (triHelper₂ ∣ x ∣ u v)
          (λ i → pathHelper ∣ x ∣ v)
          (triHelper₂ t u v)
          (triHelper₁ ∣ x ∣ t u)
          (λ i → refl)
          i
    triHelper₂ ∣ x ∣ ∣ y ∣ (squash u v i)
      = Bgpd'
          (triHelper₂ ∣ x ∣ ∣ y ∣ u)
          (triHelper₂ ∣ x ∣ ∣ y ∣ v)
          (triHelper₁ ∣ x ∣ u v)
          (triHelper₁ ∣ y ∣ u v)
          (λ i → link x y)
          (λ i → refl)
          i

  preEquiv₁ : (∥ A ∥ → Σ (A → B) 3-Constant) ≃ Σ (A → B) 3-Constant
  preEquiv₁ = isoToEquiv (iso fn const (λ _ → refl) retr)
    where
    open 3-Constant

    fn : (∥ A ∥ → Σ (A → B) 3-Constant) → Σ (A → B) 3-Constant
    fn f .fst x = f ∣ x ∣ .fst x
    fn f .snd .link x y i = f (squash ∣ x ∣ ∣ y ∣ i) .snd .link x y i
    fn f .snd .coh₁ x y z i j
      = f (squash ∣ x ∣ (squash ∣ y ∣ ∣ z ∣ i) j) .snd .coh₁ x y z i j

    retr : retract fn const
    retr f i t .fst x = f (squash ∣ x ∣ t i) .fst x
    retr f i t .snd .link x y j
      = f (squash (squash ∣ x ∣ ∣ y ∣ j) t i) .snd .link x y j
    retr f i t .snd .coh₁ x y z
      = Bgpd'
          (λ k j → f (cb k j i0) .snd .coh₁ x y z k j )
          (λ k j → f (cb k j i1) .snd .coh₁ x y z k j)
          (λ k j → f (cb i0 j k) .snd .link x y j)
          (λ k j → f (cb i1 j k) .snd .link x z j)
          (λ _ → refl)
          (λ k j → f (cb j i1 k) .snd .link y z j)
          i
      where
      cb : I → I → I → ∥ _ ∥
      cb i j k = squash (squash ∣ x ∣ (squash ∣ y ∣ ∣ z ∣ i) j) t k

  e : B → Σ (A → B) 3-Constant
  e b .fst _ = b
  e b .snd = record
           { link = λ _ _ _ → b
           ; coh₁ = λ _ _ _ _ _ → b
           }

  eval : A → Σ (A → B) 3-Constant → B
  eval a₀ (g , _) = g a₀

  module _ where
    open 3-Constant
    e-eval : ∀(a₀ : A) γ → e (eval a₀ γ) ≡ γ
    e-eval a₀ (g , 3kg) i .fst x = 3kg .link a₀ x i
    e-eval a₀ (g , 3kg) i .snd .link x y = λ j → 3kg .coh₁ a₀ x y j i
    e-eval a₀ (g , 3kg) i .snd .coh₁ x y z
      = Bgpd'
          (λ _ _ → g a₀)
          (3kg .coh₁ x y z)
          (λ k j → 3kg .coh₁ a₀ x y j k)
          (λ k j → 3kg .coh₁ a₀ x z j k)
          (λ _ → refl)
          (λ k j → 3kg .coh₁ a₀ y z j k)
          i

  e-isEquiv : A → isEquiv (e {A = A})
  e-isEquiv a₀ = isoToIsEquiv (iso e (eval a₀) (e-eval a₀) λ _ → refl)

  preEquiv₂ : ∥ A ∥ → B ≃ Σ (A → B) 3-Constant
  preEquiv₂ t = e , rec (isPropIsEquiv e) e-isEquiv t

  trunc→Gpd≃ : (∥ A ∥ → B) ≃ Σ (A → B) 3-Constant
  trunc→Gpd≃ = compEquiv (equivΠCod preEquiv₂) preEquiv₁

open GpdElim using (rec→Gpd; trunc→Gpd≃) public

squashᵗ
  : ∀(x y z : A)
  → Square (squash ∣ x ∣ ∣ y ∣) (squash ∣ x ∣ ∣ z ∣) refl (squash ∣ y ∣ ∣ z ∣)
squashᵗ x y z i = squash ∣ x ∣ (squash ∣ y ∣ ∣ z ∣ i)

elim→Gpd
  : (P : ∥ A ∥ → Type ℓ)
  → (∀ t → isGroupoid (P t))
  → (f : (x : A) → P ∣ x ∣)
  → (kf : ∀ x y → PathP (λ i → P (squash ∣ x ∣ ∣ y ∣ i)) (f x) (f y))
  → (3kf : ∀ x y z
         → SquareP (λ i j → P (squashᵗ x y z i j)) (kf x y) (kf x z) refl (kf y z))
  → (t : ∥ A ∥) → P t
elim→Gpd {A = A} P Pgpd f kf 3kf t = rec→Gpd (Pgpd t) g 3kg t
  where
  g : A → P t
  g x = transp (λ i → P (squash ∣ x ∣ t i)) i0 (f x)

  open 3-Constant

  3kg : 3-Constant g
  3kg .link x y i
    = transp (λ j → P (squash (squash ∣ x ∣ ∣ y ∣ i) t j)) i0 (kf x y i)
  3kg .coh₁ x y z i j
    = transp (λ k → P (squash (squashᵗ x y z i j) t k)) i0 (3kf x y z i j)

RecHSet : (P : A → TypeOfHLevel ℓ 2) → 3-Constant P → ∥ A ∥ → TypeOfHLevel ℓ 2
RecHSet P 3kP = rec→Gpd (isOfHLevelTypeOfHLevel 2) P 3kP

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module OpBind where

postulate _∘_ : Set -> Set -> Set

Homomorphic₀ : Set → Set
Homomorphic₀ ∘ = ∘

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module _ where

open import Data.Nat using (ℕ ; _+_ ;  _≤′_ ; suc)
open import Induction.Nat using (<′-rec)
open import Esterel.Lang.CanFunction
open import Function using (_∋_ ; _∘_ ; id ; _$_)
open import Data.Nat.Properties.Simple using ( +-comm ; +-assoc)
open import utility
open import noetherian using (noetherian ; ∥_∥s)
open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Environment as Env
open import Esterel.Context
open import Data.Product
open import Data.Sum
open import Data.Bool
open import Data.List using ([] ; [_] ; _∷_ ; List ; _++_)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; subst ; cong ; trans ; module ≡-Reasoning ; cong₂ ; subst₂ ; inspect)
open import Data.Empty
open import sn-calculus
open import context-properties -- get view, E-views
open import Esterel.Lang.Binding
open import Data.Maybe using ( just )
-- open import coherence
open import Data.List.Any
open import Data.List.Any.Properties
open import Esterel.Lang.CanFunction.Base
open import eval
open import blocked
open import Data.List.All

open ≡-Reasoning using (_≡⟨_⟩_ ; _≡⟨⟩_ ; _∎)

open import Relation.Nullary.Decidable
  using (⌊_⌋)
open import Data.FiniteMap
import Data.OrderedListMap as OMap
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 Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import sn-calculus-compatconf using (1-step)

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

open import binding-preserve

{- definition of two relations commuting
   (wrt to Correct Binding) -}
CB-COMMUTE : (Term -> Term -> Set) ->
             (Term -> Term -> Set) ->
             Set
CB-COMMUTE R1 R2 =
  ∀ {p q r BV FV} ->
  CorrectBinding p BV FV ->
  R1 p q ->
  R2 p r ->
  ∃ λ {z → (R2 q z × R1 r z)}

{- a relation that commutes with itself is confluent -}
CB-CONFLUENT : (Term -> Term -> Set) -> Set
CB-CONFLUENT R = CB-COMMUTE R R

sn⟶*-confluent : CB-CONFLUENT _sn⟶*_
sn⟶*-confluent {p} {q} {r} {BV} {FV} CB =
  newman ∥ p ∥s p q r BV FV refl CB where

  {-
    Proof of Newman's lemma from:
    _Confluent Reductions: Abstract Properties and Applications to Term
    Rewriting Systems_ by Gérard Huet. Oct 1980; JACM volume 27 issue 4
    https://dl.acm.org/citation.cfm?id=322230
   -}

  newmantype : ℕ -> Set
  newmantype c = ∀ p q r BV FV ->
    ∥ p ∥s ≡ c ->
    CorrectBinding p BV FV ->
    p sn⟶* q ->
    p sn⟶* r ->
    Σ[ z ∈ Term ] (q sn⟶* z × r sn⟶* z)

  step : ∀ (c : ℕ) ->
    ((c′ : ℕ) → suc c′ ≤′ c → newmantype c′)
    -> (newmantype c)
  step c rec x .x z BV FV nsx≡c CB rrefl s*xz = z , (s*xz , rrefl)
  step c rec x y .x BV FV nsx≡c CB s*xy rrefl = y , (rrefl , s*xy)
  step c rec x y z  BV FV refl  CB
    (rstep {.x} {y1} {.y} sxy1 s*y1y)
    (rstep {.x} {z1} {.z} sxz1 s*z1z)
    with 1-step {x} {y1} {z1} {BV} {FV} CB sxy1 sxz1
  ... | (u , s*y1u , s*z1u)        with sn⟶-maintains-binding CB sxy1
  ... | (BVy1 , FVy1) , (CBy1 , _) with sn⟶-maintains-binding CB sxz1
  ... | (BVz1 , FVz1) , (CBz1 , _) with rec ∥ y1 ∥s (noetherian{x}{y1} sxy1)
                                            y1 y u BVy1 FVy1 refl CBy1 s*y1y s*y1u
  ... | (v , s*yv , s*uv)          with rec ∥ z1 ∥s (noetherian{x}{z1} sxz1)
                                            z1 v z BVz1 FVz1 refl CBz1 (sn⟶*+ s*z1u s*uv) s*z1z
  ... | (t , s*vt , s*zt) = t , (sn⟶*+ s*yv s*vt) , s*zt

  newman : ∀ c -> newmantype c
  newman = <′-rec _ step

lift-sn⟶* : ∀ {p q} → (P : Term → Set) → (∀ {p q} → P p → p sn⟶ q → P q) → P p → p sn⟶* q → P q
lift-sn⟶* P P-respects-sn⟶ Pp rrefl = Pp
lift-sn⟶* P P-respects-sn⟶ Pp (rstep psn⟶r rsn⟶*q) =
  lift-sn⟶* P P-respects-sn⟶ (P-respects-sn⟶ Pp psn⟶r) rsn⟶*q

sn≡ₑ-preserve-cb : ∀{p q BV FV} → CorrectBinding p BV FV → p sn≡ₑ q → Σ (VarList × VarList) λ {(BVq , FVq) → CorrectBinding q BVq FVq}
sn≡ₑ-preserve-cb cb (rstp x) with sn⟶-maintains-binding cb x
... | (bv,fv , cbq , _)= _ , cbq
sn≡ₑ-preserve-cb cb (rsym psn≡ₑq x) = _ , x
sn≡ₑ-preserve-cb cb rref = _ , cb
sn≡ₑ-preserve-cb cb (rtrn psn≡ₑq psn≡ₑq₁) = sn≡ₑ-preserve-cb (proj₂ (sn≡ₑ-preserve-cb cb psn≡ₑq)) psn≡ₑq₁

sn≡ₑ-consistent : ∀{p q BV FV} → CorrectBinding p BV FV → p sn≡ₑ q → Σ[ r ∈ Term ] p sn⟶* r ×  q sn⟶* r
sn≡ₑ-consistent cb (rstp x) = _ , rstep x rrefl , rrefl
sn≡ₑ-consistent cb (rsym qsn≡ₑp cbq) with sn≡ₑ-consistent cbq qsn≡ₑp
... | (r , qsn⟶r , psn⟶r ) = (r , psn⟶r , qsn⟶r)
sn≡ₑ-consistent cb rref = _ , rrefl , rrefl
sn≡ₑ-consistent cb (rtrn psn≡ₑs ssn≡ₑq) with (sn≡ₑ-preserve-cb cb psn≡ₑs)
... | (_ , cbs) with sn≡ₑ-consistent cb psn≡ₑs | sn≡ₑ-consistent cbs ssn≡ₑq
... | (rl , psn⟶*rl , ssn⟶*rl) | (rr , ssn⟶*rr , qsn⟶*rr) with sn⟶*-confluent cbs ssn⟶*rl ssn⟶*rr
... | (r , rlsn⟶*r , rrsn⟶*r) = r , (sn⟶*+ psn⟶*rl rlsn⟶*r , sn⟶*+ qsn⟶*rr rrsn⟶*r )

irreducibility-of-complete-sn⟶₁ : ∀{p q} → complete p → p sn⟶₁ q → ⊥
irreducibility-of-complete-sn⟶₁ (codone p/done) psn⟶₁q = done-¬sn⟶₁ p/done psn⟶₁q
irreducibility-of-complete-sn⟶₁ (coenv {θ} (θcomplete x x₁) p/done) ρθpsn⟶₁ρθ'q
  with ρ-stays-ρ-sn⟶₁ ρθpsn⟶₁ρθ'q
... | θ' , q , A' , refl with get-view ρθpsn⟶₁ρθ'q
irreducibility-of-complete-sn⟶₁ (coenv {θ} (θcomplete x x₁) p/done) ρθpsn⟶₁ρθ'q
  | θ' , q , A' , refl | inj₁ (E , pin , qin , p≐E⟦pin⟧ , q≐E⟦qin⟧ , e-view) =
  ⊥-elim
    (done-E-view-term-disjoint
      (done-⟦⟧e p/done p≐E⟦pin⟧)
      (->E-view-inner-term e-view))
irreducibility-of-complete-sn⟶₁ (coenv {θ} (θcomplete x x₁) p/done) ρθpsn⟶₁ρθ'q
  | θ' , q , A' ,  refl | inj₂ (refl , refl , vabsence S S∈ x₂ x₃)
   with x S S∈
... | inj₁ S≡ = lookup-S-eq θ S S∈ S∈ S≡ x₂ (λ ())
... | inj₂ S≡ = lookup-S-eq θ S S∈ S∈ S≡ x₂ (λ ())
irreducibility-of-complete-sn⟶₁ (coenv {θ} (θcomplete x x₁) p/done) ρθpsn⟶₁ρθ'q
  | θ' , q , A' , refl | inj₂ (refl , refl , vreadyness s s∈ x₂ x₃)
   with x₁ s s∈
... | s≡ with x₂
... | inj₁ s2≡ = lookup-s-eq θ s s∈ s∈ s≡ s2≡ (λ ())
... | inj₂ s2≡ = lookup-s-eq θ s s∈ s∈ s≡ s2≡ (λ ())

inescapability-of-paused-sn⟶ : ∀ {p q} ->
  paused p ->
  p sn⟶ q ->
  paused q
inescapability-of-paused-sn⟶ ppause (rcontext .[] dchole ())
inescapability-of-paused-sn⟶ (pseq ()) (rcontext .[] dchole rseq-done)
inescapability-of-paused-sn⟶ (pseq ()) (rcontext .[] dchole rseq-exit)
inescapability-of-paused-sn⟶ (pseq pausedp) (rcontext _ (dcseq₁ dc) psn⟶₁p')
  = pseq (inescapability-of-paused-sn⟶ pausedp (rcontext _ dc psn⟶₁p'))
inescapability-of-paused-sn⟶ (pseq pausedp) (rcontext _ (dcseq₂ dc) psn⟶₁p')
  = pseq pausedp
inescapability-of-paused-sn⟶ (ploopˢ ()) (rcontext .[] dchole rloopˢ-exit)
inescapability-of-paused-sn⟶ (ploopˢ pausedp) (rcontext _ (dcloopˢ₁ dc) psn⟶₁p')
  = ploopˢ (inescapability-of-paused-sn⟶ pausedp (rcontext _ dc psn⟶₁p'))
inescapability-of-paused-sn⟶ (ploopˢ pausedp) (rcontext _ (dcloopˢ₂ dc) psn⟶₁p')
  = ploopˢ pausedp
inescapability-of-paused-sn⟶ (ppar pausedp _) (rcontext .[] dchole (rpar-done-right p' q'))
  = ⊥-elim (halted-paused-disjoint p' pausedp)
inescapability-of-paused-sn⟶ (ppar _ pausedq) (rcontext .[] dchole (rpar-done-left p' q'))
  = ⊥-elim (halted-paused-disjoint q' pausedq)
inescapability-of-paused-sn⟶ (ppar pausedp pausedq) (rcontext _ (dcpar₁ dc) psn⟶₁p')
  = ppar (inescapability-of-paused-sn⟶ pausedp (rcontext _ dc psn⟶₁p')) pausedq
inescapability-of-paused-sn⟶ (ppar pausedp pausedq) (rcontext _ (dcpar₂ dc) psn⟶₁p')
  = ppar pausedp (inescapability-of-paused-sn⟶ pausedq (rcontext _ dc psn⟶₁p'))
inescapability-of-paused-sn⟶ (psuspend pausedp) (rcontext .[] dchole (rsuspend-done haltedp))
  = ⊥-elim (halted-paused-disjoint haltedp pausedp)
inescapability-of-paused-sn⟶ (psuspend pausedp) (rcontext _ (dcsuspend dc) psn⟶₁p')
  = psuspend (inescapability-of-paused-sn⟶ pausedp (rcontext _ dc psn⟶₁p'))
inescapability-of-paused-sn⟶ (ptrap ()) (rcontext .[] dchole (rtrap-done hnothin))
inescapability-of-paused-sn⟶ (ptrap ()) (rcontext .[] dchole (rtrap-done (hexit n)))
inescapability-of-paused-sn⟶ (ptrap pausedp) (rcontext _ (dctrap dc) psn⟶₁p')
  = ptrap (inescapability-of-paused-sn⟶ pausedp (rcontext _ dc psn⟶₁p'))

inescapability-of-paused-sn⟶* : ∀ {p q} ->
  paused p ->
  p sn⟶* q ->
  paused q
inescapability-of-paused-sn⟶* pausedp rrefl = pausedp
inescapability-of-paused-sn⟶* pausedp (rstep psn⟶r r⟶q)
  = inescapability-of-paused-sn⟶* (inescapability-of-paused-sn⟶ pausedp psn⟶r) r⟶q

inescapability-of-complete-sn⟶ : ∀{p q} → complete p → p sn⟶ q → complete q
inescapability-of-complete-sn⟶ c@(codone p-done) psn⟶q = codone (done-sn⟶ p-done psn⟶q)
inescapability-of-complete-sn⟶ c@(coenv x x₁) (rcontext .[] dchole psn⟶₁p') = ⊥-elim (irreducibility-of-complete-sn⟶₁ c psn⟶₁p')
inescapability-of-complete-sn⟶ (coenv x (dhalted hnothin)) (rcontext .(cenv _ _ ∷ []) (dcenv dchole) psn⟶₁p')
   = ⊥-elim (irreducibility-of-complete-sn⟶₁ (codone (dhalted hnothin)) psn⟶₁p')
inescapability-of-complete-sn⟶ (coenv x (dhalted (hexit n))) (rcontext .(cenv _ _ ∷ []) (dcenv dchole) psn⟶₁p')
   = ⊥-elim (irreducibility-of-complete-sn⟶₁ (codone (dhalted (hexit n))) psn⟶₁p')
inescapability-of-complete-sn⟶ (coenv x (dpaused p/paused)) (rcontext .(cenv _ _ ∷ _) (dcenv dc) psn⟶₁p')
 with (inescapability-of-complete-sn⟶ (codone (dpaused p/paused)) (rcontext _ dc psn⟶₁p'))
inescapability-of-complete-sn⟶ (coenv x (dpaused ppause)) (rcontext .(cenv _ _ ∷ _) (dcenv dchole) psn⟶₁p') | rec
   =  ⊥-elim (irreducibility-of-complete-sn⟶₁ (codone (dpaused ppause)) psn⟶₁p')

inescapability-of-complete-sn⟶ (coenv x₁ (dpaused (ploopˢ p/paused))) (rcontext .(cenv _ _ ∷ []) (dcenv dchole) psn⟶₁p') | rec
   =  ⊥-elim (irreducibility-of-complete-sn⟶₁ (codone (dpaused (ploopˢ p/paused))) psn⟶₁p')
inescapability-of-complete-sn⟶ (coenv x₁ (dpaused (ploopˢ p/paused))) (rcontext .(cenv _ _ ∷ ceval (eloopˢ _) ∷ _) (dcenv (dcloopˢ₁ dc)) psn⟶₁p') | codone x
  = coenv x₁ x
inescapability-of-complete-sn⟶ (coenv x₁ (dpaused (ploopˢ p/paused))) (rcontext .(cenv _ _ ∷ cloopˢ₂ _ ∷ _) (dcenv (dcloopˢ₂ dc)) psn⟶₁p') | codone x
  = coenv x₁ x

inescapability-of-complete-sn⟶ (coenv x₁ (dpaused (pseq p/paused))) (rcontext .(cenv _ _ ∷ []) (dcenv dchole) psn⟶₁p') | rec
   =  ⊥-elim (irreducibility-of-complete-sn⟶₁ (codone (dpaused (pseq p/paused))) psn⟶₁p')
inescapability-of-complete-sn⟶ (coenv x₁ (dpaused (pseq p/paused))) (rcontext .(cenv _ _ ∷ ceval (eseq _) ∷ _) (dcenv (dcseq₁ dc)) psn⟶₁p') | codone x
  = coenv x₁ x
inescapability-of-complete-sn⟶ (coenv x₁ (dpaused (pseq p/paused))) (rcontext .(cenv _ _ ∷ cseq₂ _ ∷ _) (dcenv (dcseq₂ dc)) psn⟶₁p') | codone x
  = coenv x₁ x

inescapability-of-complete-sn⟶ (coenv x (dpaused (ppar p/paused p/paused₁))) (rcontext .(cenv _ _ ∷ []) (dcenv dchole) psn⟶₁p') | rec
   =  ⊥-elim (irreducibility-of-complete-sn⟶₁ (codone (dpaused (ppar p/paused p/paused₁))) psn⟶₁p')
inescapability-of-complete-sn⟶ (coenv x₁ (dpaused (ppar p/paused p/paused₁))) (rcontext .(cenv _ _ ∷ ceval (epar₁ _) ∷ _) (dcenv (dcpar₁ dc)) psn⟶₁p') | codone x
  = coenv x₁ x
inescapability-of-complete-sn⟶ (coenv x₁ (dpaused (ppar p/paused p/paused₁))) (rcontext .(cenv _ _ ∷ ceval (epar₂ _) ∷ _) (dcenv (dcpar₂ dc)) psn⟶₁p') | codone x = coenv x₁ x
inescapability-of-complete-sn⟶ (coenv x (dpaused (psuspend p/paused))) (rcontext .(cenv _ _ ∷ []) (dcenv dchole) psn⟶₁p') | rec
   =  ⊥-elim (irreducibility-of-complete-sn⟶₁ (codone (dpaused (psuspend p/paused))) psn⟶₁p')
inescapability-of-complete-sn⟶ (coenv x₁ (dpaused (psuspend p/paused))) (rcontext .(cenv _ _ ∷ ceval (esuspend _) ∷ _) (dcenv (dcsuspend dc)) psn⟶₁p') | codone x = coenv x₁ x
inescapability-of-complete-sn⟶ (coenv x (dpaused (ptrap p/paused))) (rcontext .(cenv _ _ ∷ []) (dcenv dchole) psn⟶₁p') | rec
   =  ⊥-elim (irreducibility-of-complete-sn⟶₁ (codone (dpaused (ptrap p/paused))) psn⟶₁p')
inescapability-of-complete-sn⟶ (coenv x₁ (dpaused (ptrap p/paused))) (rcontext .(cenv _ _ ∷ ceval etrap ∷ _) (dcenv (dctrap dc)) psn⟶₁p') | codone x = coenv x₁ x

inescapability-of-complete-sn : ∀{p q} → complete p → p sn⟶* q → complete q
inescapability-of-complete-sn = lift-sn⟶* complete inescapability-of-complete-sn⟶

equality-of-complete-sn⟶* : ∀{θ θ' p q A A'} →
  complete (ρ⟨ θ , A ⟩·  p) →
  (ρ⟨ θ , A ⟩· p) sn⟶* (ρ⟨ θ' , A' ⟩· q) →
  θ ≡ θ' × A ≡ A'
equality-of-complete-sn⟶* ρθp/complete rrefl = refl , refl
equality-of-complete-sn⟶* ρθp/complete (rstep (rcontext _ dchole ρθpsn⟶₁ρθ''r) ρθ''rsn⟶*ρθ'q)
  with irreducibility-of-complete-sn⟶₁ ρθp/complete ρθpsn⟶₁ρθ''r
... | ()
equality-of-complete-sn⟶* ρθp/complete (rstep (rcontext _ (dcenv ρθp≐C⟦p'⟧) p'sn⟶₁r) ρθrsn⟶*ρθ'q) =
  equality-of-complete-sn⟶*
    (inescapability-of-complete-sn⟶ ρθp/complete (rcontext _ (dcenv ρθp≐C⟦p'⟧) p'sn⟶₁r))
    ρθrsn⟶*ρθ'q

get-view/blocked : ∀{θ θ' p q A A'} →
  blocked θ A p →
  (ρθpsn⟶₁ρθ'q  :  ρ⟨ θ , A ⟩· p sn⟶₁ ρ⟨ θ' , A' ⟩· q) →
  ∃ (λ a → ∃ (->pot-view ρθpsn⟶₁ρθ'q a))
get-view/blocked p/blocked ρθpsn⟶₁ρθ'q with get-view ρθpsn⟶₁ρθ'q
... | inj₂ refl-pot-view = refl-pot-view
... | inj₁ (E , pin , qin , p≐E⟦pin⟧ , q≐E⟦qin⟧ , e-view)
  with blocked-⟦⟧e p/blocked p≐E⟦pin⟧ | ->E-view-inner-term e-view
... | inj₂ pin/done | e-view-term =
  ⊥-elim
    (done-E-view-term-disjoint
      pin/done
      (->E-view-inner-term e-view))
... | (inj₁ (bpar-both pin'/blocked qin'/blocked)) | ()
... | (inj₁ (bpar-left pin'/blocked qin'/done))    | ()
... | (inj₁ (bpar-right pin'/done qin'/blocked))   | ()
... | (inj₁ (bloopˢ pin/blocked))                  | ()
... | (inj₁ (bseq pin/blocked))                    | ()
... | (inj₁ (bsusp pin/blocked))                   | ()
... | (inj₁ (btrap pin/blocked))                   | ()
get-view/blocked {θ} p/blocked (ris-present S∈' θS≡present .p≐E⟦pin⟧)
  | inj₁ (E , pin , qin , p≐E⟦pin⟧ , q≐E⟦qin⟧ , vis-present)
  | (inj₁ (bsig-exists S S∈ θS≡unknown)) | evt-present
  with trans (sym θS≡present) (trans (Env.sig-stats-∈-irr {S} {θ} S∈' S∈) θS≡unknown)
... | ()
get-view/blocked {θ} p/blocked (ris-absent S∈' θS≡absent .p≐E⟦pin⟧)
  | inj₁ (E ,  pin , qin , p≐E⟦pin⟧ , q≐E⟦qin⟧ , vis-absent)
  | (inj₁ (bsig-exists S S∈ θS≡unknown)) | evt-present
  with trans (sym θS≡absent) (trans (Env.sig-stats-∈-irr {S} {θ} S∈' S∈) θS≡unknown)
... | ()
get-view/blocked p/blocked (rraise-shared {s = s} e' .p≐E⟦pin⟧)
  | inj₁ (E , pin , qin , p≐E⟦pin⟧ , q≐E⟦qin⟧ , vraise-shared)
  | (inj₁ (bshared e/blocked)) | evt-raise-shared =
  ⊥-elim (all-ready-blocked-disjoint (e' , e/blocked))
get-view/blocked p/blocked (rset-shared-value-old {s = s} e' s∈ θs≡old .p≐E⟦pin⟧)
  | inj₁ (E , pin , qin , p≐E⟦pin⟧ , q≐E⟦qin⟧ , vset-shared-value-old)
  | (inj₁ (bsset e/blocked)) | evt-set-shared =
  ⊥-elim (all-ready-blocked-disjoint (e' , e/blocked))
get-view/blocked p/blocked (rset-shared-value-new {s = s} e' s∈ θs≡new .p≐E⟦pin⟧)
  | inj₁ (E , pin , qin , p≐E⟦pin⟧ , q≐E⟦qin⟧ , vset-shared-value-new)
  | (inj₁ (bsset e/blocked)) | evt-set-shared =
  ⊥-elim (all-ready-blocked-disjoint (e' , e/blocked))
get-view/blocked p/blocked (rraise-var {x = x} e' .p≐E⟦pin⟧)
  | inj₁ (E , pin , qin , p≐E⟦pin⟧ , q≐E⟦qin⟧ , vraise-var)
  | (inj₁ (bvar e/blocked)) | evt-raise-var =
  ⊥-elim (all-ready-blocked-disjoint (e' , e/blocked))
get-view/blocked p/blocked (rset-var {x = x} x∈ e' .p≐E⟦pin⟧)
  | inj₁ (E , pin , qin , p≐E⟦pin⟧ , q≐E⟦qin⟧ , vset-var)
  | (inj₁ (bxset e/blocked)) | evt-set-var =
  ⊥-elim (all-ready-blocked-disjoint (e' , e/blocked))
get-view/blocked {A = .WAIT} p/blocked ρθpsn⟶₁ρθ'q | inj₁ (E , s ⇐ e , qin , p≐E⟦pin⟧ , q≐E⟦qin⟧ , ())
  | inj₁ bwset | evt-set-shared
get-view/blocked {A = .WAIT} p/blocked ρθpsn⟶₁ρθ'q | inj₁ (E , emit S , qin , p≐E⟦pin⟧ , q≐E⟦qin⟧ , ())
  | inj₁ bwemit | evt-emit

irreducibility-of-blocked-sn⟶₁ : ∀ {θ p q A} → blocked θ A p → p sn⟶₁ q → ⊥
irreducibility-of-blocked-sn⟶₁ (bsig-exists S S∈ θS≡unknown) ()
irreducibility-of-blocked-sn⟶₁ (bshared e/blocked)           ()
irreducibility-of-blocked-sn⟶₁ (bsset e/blocked)             ()
irreducibility-of-blocked-sn⟶₁ (bvar e/blocked)              ()
irreducibility-of-blocked-sn⟶₁ (bxset e/blocked)             ()
irreducibility-of-blocked-sn⟶₁ {p = s ⇐ e} {A = WAIT} bwset ()
irreducibility-of-blocked-sn⟶₁ {p = emit S} {A = WAIT} bwemit ()
irreducibility-of-blocked-sn⟶₁ (bpar-both p/blocked q/blocked)
  (rpar-done-right p/halted q/done)   =
  halted-blocked-disjoint p/halted p/blocked
irreducibility-of-blocked-sn⟶₁ (bpar-left p/blocked q/done)
  (rpar-done-right p/halted q/done')  =
  halted-blocked-disjoint p/halted p/blocked
irreducibility-of-blocked-sn⟶₁ (bpar-right p/done q/blocked)
  (rpar-done-right p/halted q/done)   =
  done-blocked-disjoint q/done q/blocked
irreducibility-of-blocked-sn⟶₁ (bpar-both p/blocked q/blocked)
  (rpar-done-left  p/done   q/halted) =
  halted-blocked-disjoint q/halted q/blocked
irreducibility-of-blocked-sn⟶₁ (bpar-left p/blocked q/done)
  (rpar-done-left  p/done   q/halted) =
  done-blocked-disjoint p/done p/blocked
irreducibility-of-blocked-sn⟶₁ (bpar-right p/done q/blocked)
  (rpar-done-left  p/done'  q/halted) =
  halted-blocked-disjoint q/halted q/blocked
irreducibility-of-blocked-sn⟶₁ (bseq ())
  rseq-done
irreducibility-of-blocked-sn⟶₁ (bseq ())
  rseq-exit
irreducibility-of-blocked-sn⟶₁ (bloopˢ ())
  rloopˢ-exit
irreducibility-of-blocked-sn⟶₁ (bsusp p/blocked)
  (rsuspend-done p/halted) =
  halted-blocked-disjoint p/halted p/blocked
irreducibility-of-blocked-sn⟶₁ (btrap p/blocked)
  (rtrap-done p/halted) =
  halted-blocked-disjoint p/halted p/blocked

irreducibility-of-halted-sn⟶ : ∀ {p q} ->
  halted p ->
  p sn⟶ q ->
  ⊥
irreducibility-of-halted-sn⟶ hnothin (rcontext [] dchole ())
irreducibility-of-halted-sn⟶ (hexit n) (rcontext [] dchole ())

-- not sure if it's worthwhile for now to also prove this for ρ θ · p sn⟶₁ ρ θ' · p
inescapability-of-blocked-inside-sn⟶ : ∀{θ p q A} →
  blocked θ A p →
  p sn⟶ q →
  blocked θ A q
inescapability-of-blocked-inside-sn⟶ p/blocked (rcontext _ dchole psn⟶₁p') =
  ⊥-elim (irreducibility-of-blocked-sn⟶₁ p/blocked psn⟶₁p')
inescapability-of-blocked-inside-sn⟶ (bpar-both p/blocked q/blocked)
  (rcontext _ (dcpar₁ p≐C⟦pin⟧) pinsn⟶₁pin') =
  bpar-both
    (inescapability-of-blocked-inside-sn⟶ p/blocked
     (rcontext _ p≐C⟦pin⟧ pinsn⟶₁pin'))
    q/blocked
inescapability-of-blocked-inside-sn⟶ (bpar-both p/blocked q/blocked)
  (rcontext _ (dcpar₂ p≐C⟦pin⟧) pinsn⟶₁pin') =
  bpar-both p/blocked
    (inescapability-of-blocked-inside-sn⟶ q/blocked
     (rcontext _ p≐C⟦pin⟧ pinsn⟶₁pin'))
inescapability-of-blocked-inside-sn⟶ (bpar-left p/blocked q/done)
  (rcontext _ (dcpar₁ p≐C⟦pin⟧) pinsn⟶₁pin') =
  bpar-left
    (inescapability-of-blocked-inside-sn⟶ p/blocked
     (rcontext _ p≐C⟦pin⟧ pinsn⟶₁pin'))
    q/done
inescapability-of-blocked-inside-sn⟶ (bpar-left p/blocked q/done)
  (rcontext _ (dcpar₂ p≐C⟦pin⟧) pinsn⟶₁pin') =
  bpar-left p/blocked
    (done-sn⟶ q/done (rcontext _ p≐C⟦pin⟧ pinsn⟶₁pin'))
inescapability-of-blocked-inside-sn⟶ (bpar-right p/done q/blocked)
  (rcontext _ (dcpar₁ p≐C⟦pin⟧) pinsn⟶₁pin') =
  bpar-right (done-sn⟶ p/done (rcontext _ p≐C⟦pin⟧ pinsn⟶₁pin'))
    q/blocked
inescapability-of-blocked-inside-sn⟶ (bpar-right p/done q/blocked)
  (rcontext _ (dcpar₂ p≐C⟦pin⟧) pinsn⟶₁pin') =
  bpar-right p/done
    (inescapability-of-blocked-inside-sn⟶ q/blocked
     (rcontext _ p≐C⟦pin⟧ pinsn⟶₁pin'))

inescapability-of-blocked-inside-sn⟶ (bseq p/blocked)
  (rcontext _ (dcseq₁ p≐C⟦pin⟧) pinsn⟶₁pin') =
  bseq
    (inescapability-of-blocked-inside-sn⟶ p/blocked
     (rcontext _ p≐C⟦pin⟧ pinsn⟶₁pin'))
inescapability-of-blocked-inside-sn⟶ (bseq p/blocked)
  (rcontext _ (dcseq₂ p≐C⟦pin⟧) pinsn⟶₁pin') =
  bseq p/blocked

inescapability-of-blocked-inside-sn⟶ (bloopˢ p/blocked)
  (rcontext _ (dcloopˢ₁ p≐C⟦pin⟧) pinsn⟶₁pin') =
  bloopˢ
    (inescapability-of-blocked-inside-sn⟶ p/blocked
     (rcontext _ p≐C⟦pin⟧ pinsn⟶₁pin'))
inescapability-of-blocked-inside-sn⟶ (bloopˢ p/blocked)
  (rcontext _ (dcloopˢ₂ p≐C⟦pin⟧) pinsn⟶₁pin') =
  bloopˢ p/blocked

inescapability-of-blocked-inside-sn⟶ (bsusp p/blocked)
  (rcontext _ (dcsuspend p≐C⟦pin⟧) pinsn⟶₁pin') =
  bsusp
    (inescapability-of-blocked-inside-sn⟶ p/blocked
     (rcontext _ p≐C⟦pin⟧ pinsn⟶₁pin'))
inescapability-of-blocked-inside-sn⟶ (btrap p/blocked)
  (rcontext _ (dctrap p≐C⟦pin⟧) pinsn⟶₁pin') =
  btrap
    (inescapability-of-blocked-inside-sn⟶ p/blocked
     (rcontext _ p≐C⟦pin⟧ pinsn⟶₁pin'))
inescapability-of-blocked-inside-sn⟶ (bshared e/blocked)
  (rcontext _ (dcshared p≐C⟦pin⟧) pinsn⟶₁pin') =
  bshared e/blocked
inescapability-of-blocked-inside-sn⟶ (bvar e/blocked)
  (rcontext _ (dcvar p≐C⟦pin⟧) pinsn⟶₁pin') =
  bvar e/blocked
inescapability-of-blocked-inside-sn⟶ {θ} {A = A}(bsig-exists S S∈ θS≡unknown)
  (rcontext _ S?p:q≐C⟦pin⟧ pinsn⟶₁pin') with S?p:q≐C⟦pin⟧
-- we still have the dchole case here since Agda can't determine that it cannot happen
... | dchole = ⊥-elim (irreducibility-of-blocked-sn⟶₁ {A = A} (bsig-exists {θ} S S∈ θS≡unknown) pinsn⟶₁pin')
... | dcpresent₁ p≐C⟦pin⟧ = bsig-exists S S∈ θS≡unknown
... | dcpresent₂ p≐C⟦pin⟧ = bsig-exists S S∈ θS≡unknown

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


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

open import HoTT
open import groups.ProductRepr
open import cohomology.Theory
open import homotopy.WedgeCofiber

{- For the cohomology group of a suspension ΣX, the group inverse has the
 - explicit form Cⁿ(flip-susp) : Cⁿ(ΣX) → Cⁿ(ΣX).
 -}

module cohomology.InverseInSusp {i} (CT : CohomologyTheory i)
  (n : ℤ) {X : Ptd i} where

open CohomologyTheory CT
open import cohomology.Wedge CT n

private
  module Subtract = SuspRec {C = de⊙ (⊙Susp X ⊙∨ ⊙Susp X)}
    (winl south)
    (winr south)
    (λ x → ap winl (! (merid x)) ∙ wglue ∙ ap winr (merid x))

  subtract = Subtract.f

  ⊙subtract : ⊙Susp X ⊙→ ⊙Susp X ⊙∨ ⊙Susp X
  ⊙subtract = (subtract , ! (ap winl (merid (pt X))))

  projl-subtract : ∀ σ → projl (subtract σ) == Susp-flip σ
  projl-subtract = Susp-elim idp idp $
    ↓-='-from-square ∘ vert-degen-square ∘ λ x →
      ap-∘ projl subtract (merid x)
      ∙ ap (ap projl) (Subtract.merid-β x)
      ∙ ap-∙ projl (ap winl (! (merid x))) (wglue ∙ ap winr (merid x))
      ∙ ((∘-ap projl winl (! (merid x))
          ∙ ap-idf _)
         ∙2 (ap-∙ projl wglue (ap winr (merid x))
             ∙ (Projl.glue-β
                ∙2 (∘-ap projl winr (merid x) ∙ ap-cst _ _))))
      ∙ ∙-unit-r _
      ∙ ! (SuspFlip.merid-β x)

  projr-subtract : ∀ σ → projr (subtract σ) == σ
  projr-subtract = Susp-elim idp idp $
    ↓-∘=idf-in' projr subtract ∘ λ x →
      ap (ap projr) (Subtract.merid-β x)
      ∙ ap-∙ projr (ap winl (! (merid x))) (wglue ∙ ap winr (merid x))
      ∙ ((∘-ap projr winl (! (merid x)) ∙ ap-cst _ _)
         ∙2 (ap-∙ projr wglue (ap winr (merid x))
             ∙ (Projr.glue-β
                ∙2 (∘-ap projr winr (merid x) ∙ ap-idf _))))

  fold-subtract : ∀ σ → fold (subtract σ) == south
  fold-subtract = Susp-elim idp idp $
    ↓-app=cst-in ∘ ! ∘ λ x →
      ∙-unit-r _
      ∙ ap-∘ fold subtract (merid x)
      ∙ ap (ap fold) (Subtract.merid-β x)
      ∙ ap-∙ fold (ap winl (! (merid x))) (wglue ∙ ap winr (merid x))
      ∙ ((∘-ap fold winl (! (merid x)) ∙ ap-idf _)
         ∙2 (ap-∙ fold wglue (ap winr (merid x))
             ∙ (Fold.glue-β
                ∙2 (∘-ap fold winr (merid x) ∙ ap-idf _))))
      ∙ !-inv-l (merid x)

  abstract
    cancel : ∀ x
      → GroupHom.f (×ᴳ-fanin (C-is-abelian n _) (C-fmap n (⊙Susp-flip X)) (idhom _)) (x , x)
      == Cident n (⊙Susp X)
    cancel x =
        ap2 (Group.comp (C n (⊙Susp X)))
          (! (CEl-fmap-base-indep n projl-subtract x))
          (! (CEl-fmap-idf n x) ∙ ! (CEl-fmap-base-indep n projr-subtract x))
      ∙ (C-Wedge-in-comm-sqr' (⊙Susp X) (⊙Susp X) ⊙subtract □$ᴳ (x , x))
      ∙ ap (CEl-fmap n ⊙subtract)
          ( ap (GroupIso.g (C-Wedge (⊙Susp X) (⊙Susp X)) ∘ diag) (! (CEl-fmap-idf n x))
          ∙ (C-Wedge-rec-comm-sqr' (⊙Susp X) (⊙Susp X) (⊙idf _) (⊙idf _) □$ᴳ x))
      ∙ ∘-CEl-fmap n ⊙subtract ⊙fold x
      ∙ CEl-fmap-base-indep n (λ σ → fold-subtract σ ∙ ! (merid (pt X))) x
      ∙ CEl-fmap-cst n x

abstract
  C-Susp-flip-is-inv : ∀ x → CEl-fmap n (⊙Susp-flip X) x == Group.inv (C n (⊙Susp X)) x
  C-Susp-flip-is-inv x = ! (Group.inv-unique-l (C n (⊙Susp X)) _ x (cancel x))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- A type for values that should be erased at run-time
------------------------------------------------------------------------

-- This module reexports definitions that do not depend on an
-- implementation of []-cong.

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

open import Equality

module Erased.Without-box-cong
  {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

-- Re-exported definitions.

open import Erased.Level-1 eq public
  hiding (module Erased-cong;
          module []-cong;
          module []-cong₁;
          module []-cong₂; module []-cong₂-⊔;
          module Extensionality)
open import Erased.Stability eq public
  hiding (module []-cong;
          module []-cong₁; module []-cong₁-lsuc;
          module []-cong₂; module []-cong₂-⊔₁; module []-cong₂-⊔₂;
          module Extensionality)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Dave.Functions where

    _∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
    (g ∘ f) a = g (f a)

    _∘´_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
    (g ∘´ f) = λ x → g (f x)


text:
{-# OPTIONS --no-positivity-check
  #-}
{-

  Data, Deliberately

  Conor McBride

  Workshop in Dependently Typed Programming
  Nottingham, 2008

  (Agda rendering by Ulf Norell)

-}
module Talk where

open import SomeBasicStuff

-- Codes for (first order) inductive families.
data Code (I : Set) : Set1 where
  arg : (A : Set) -> (A -> Code I) -> Code I
  rec : I -> Code I -> Code I
  out : I -> Code I

-- The semantics of a code is a functor.
⟦_⟧ : {I : Set} -> Code I -> (I -> Set) -> I -> Set
⟦ out i   ⟧ X j = i == j
⟦ arg A B ⟧ X j = Σ A \a -> ⟦ B a ⟧ X j
⟦ rec i C ⟧ X j = X i × ⟦ C ⟧ X j

map : {I : Set}{X Y : I -> Set}(C : Code I) ->
      ({i : I} -> X i -> Y i) ->
      {i : I} -> ⟦ C ⟧ X i -> ⟦ C ⟧ Y i
map (out i)   f x       = x
map (arg A B) f (a , b) = a , map (B a) f b
map (rec i C) f (a , b) = f a , map C f b

-- Tying the recursive knot. The positivity checker won't spot that
-- ⟦ C ⟧ X i is strictly positive i X, so we've switched it off.
data μ {I : Set}(C : Code I) : I -> Set where
  <_> : forall {i} -> ⟦ C ⟧ (μ C) i -> μ C i

-- Who needs a primitive case-construct anyway?
case_of_ : {A : Set1}{ts : Enumeration} -> Enum ts -> Table A ts -> A
case t of tbl = lookup tbl t

-- The code for lists
`List` : Set -> Code True
`List` X = arg _ \t ->
           case t of
             "nil"  ↦ out _
           ∣ "cons" ↦ arg X (\_ -> rec _ (out _))
           ∣ []

-- The actual list type
List : Set -> Set
List A = μ (`List` A) _

-- We can define the code for vectors directly. However, the point is
-- that we won't have to.
`VecD` : Set -> Code Nat
`VecD` X = arg _ \t ->
           case t of
             "nil"  ↦ out zero
           ∣ "cons" ↦ ( arg Nat \n ->
                        arg X   \_ ->
                        rec n (out (suc n))
                      )
           ∣ []

-- An ornamentation of a datatype adds some new indexing.
data Orn {I : Set}(J : I -> Set) : Code I -> Set1 where
  arg : forall {A B} -> ((a : A) -> Orn J (B a)) -> Orn J (arg A B)
  rec : forall {i C} -> J i -> Orn J C -> Orn J  (rec i C)
  out : forall {i} -> J i -> Orn J (out i)
  new : forall {C} -> (A : Set) -> (A -> Orn J C) -> Orn J C

-- An ornamented datatype is indexed by pairs of the old and the new index.
orn : {I : Set}{J : I -> Set}{C : Code I} -> Orn J C -> Code (Σ I J)
orn (out j)   = out (_ , j)
orn (arg B)   = arg _ \a -> orn (B a)
orn (new A B) = arg A \a -> orn (B a)
orn (rec j C) = rec (_ , j) (orn C)

-- We can forget the ornamentation and recover an element of the original type.
forget' : {I : Set}{J : I -> Set}{C : Code I}{i : I}{j : J i}
          {X : Σ I J -> Set}{Y : I -> Set} ->
          ({i : I}{j : J i} -> X (i , j) -> Y i) ->
          (ΔC : Orn J C) -> ⟦ orn ΔC ⟧ X (i , j) -> ⟦ C ⟧ Y i
forget' φ (out j)   refl    = refl
forget' φ (arg B)   (a , b) = a , forget' φ (B a) b
forget' φ (new A B) (a , b) = forget' φ (B a) b
forget' φ (rec j C) (a , b) = φ a , forget' φ C b

-- The termination checker runs into the same problem as the positivity
-- checker--it can't tell that forget' φ C x is only applying φ to
-- things smaller than x.
forget : {I : Set}{J : I -> Set}{C : Code I}{i : I}{j : J i}
         (ΔC : Orn J C) -> μ (orn ΔC) (i , j) -> μ C i
forget ΔC < x > = < forget' (forget ΔC) ΔC x >

-- A C-algebra over X takes us from ⟦ C ⟧ X i to X i.
Alg : {I : Set} -> Code I -> (I -> Set) -> Set
Alg C X = forall i -> ⟦ C ⟧ X i -> X i

-- We can fold by an algebra.
fold : {I : Set}{X : I -> Set}{C : Code I} ->
       Alg C X -> {i : I} -> μ C i -> X i
fold {C = C} φ < x > = φ _ (map C (fold φ) x)

-- A type can be ornamented an arbitrary algebra over its functor.
decorate : {I : Set}{X : I -> Set}(C : Code I)
           (φ : Alg C X) -> Orn X C
decorate         (out i)   φ = out (φ i refl)
decorate         (arg A B) φ = arg \a -> decorate (B a) (\i b -> φ i (a , b))
decorate {X = X} (rec i C) φ = new (X i) \x -> rec x (decorate C \i b -> φ i (x , b))

-- Main theorem: If you have an element in a type decorated by φ, you
-- can recover forgotten decorations by folding with φ. Specialised to
-- lists and vectors we get
--   ∀ xs : Vec A n. length (forget xs) == n.
-- Two-level definition as usual.
thm' : {I : Set}{X J : I -> Set}{Y : Σ I J -> Set}
       (C : Code I){i : I}{j : J i}(φ : Alg C J)
       (F : {i : I} -> X i -> J i)
       (ψ : {i : I}{j : J i} -> Y (i , j) -> X i) ->
       ({i : I}{j : J i}(z : Y (i , j)) -> F (ψ z) == j) ->
       let ΔC = decorate C φ in
       (x : ⟦ orn ΔC ⟧ Y (i , j)) ->
       φ i (map C F (forget' ψ ΔC x)) == j
thm' (out i)   φ F ψ ih refl        = refl
thm' (arg A B) φ F ψ ih (a , b)     = thm' (B a) (\i b -> φ i (a , b)) F ψ ih b
thm' (rec i C) {i = i0}{j = j0} φ F ψ ih (j , x , c)
  with F (ψ x) | ih x | thm' C (\i b -> φ i (j , b)) F ψ ih c
... | .j | refl | rest = rest

thm : {I : Set}{J : I -> Set}(C : Code I){i : I}{j : J i}(φ : Alg C J) ->
      (x : μ (orn (decorate C φ)) (i , j)) ->
      fold φ (forget (decorate C φ) x) == j
thm C φ < x > = thm' C φ (fold φ) (forget (decorate C φ)) (thm C φ) x

-- Vectors as decorated lists.

lengthAlg : {A : Set} -> Alg (`List` A) (\_ -> Nat)
lengthAlg _ (enum ."nil"  zero , _)               = zero
lengthAlg _ (enum ."cons" (suc zero) , x , n , _) = suc n
lengthAlg _ (enum _ (suc (suc ())) , _)

length : {A : Set} -> List A -> Nat
length = fold lengthAlg

-- Now vectors are really lists decorated by their length.
`Vec` : (A : Set) -> Orn (\_ -> Nat) (`List` A)
`Vec` A = decorate (`List` A) lengthAlg

Vec : Set -> Nat -> Set
Vec A n = μ (orn (`Vec` A)) (_ , n)

nil : {A : Set} -> Vec A zero
nil = < enum "nil" zero , refl >

cons : {A : Set}{n : Nat} -> A -> Vec A n -> Vec A (suc n)
cons {n = n} x xs = < enum "cons" (suc zero) , x , n , xs , refl >

-- The proof that the index of the vector is really the length follows directly
-- from our main theorem.
corollary : {A : Set}{n : Nat}(xs : Vec A n) ->
            length (forget (`Vec` _) xs) == n
corollary = thm (`List` _) lengthAlg


text:
------------------------------------------------------------------------
-- An implementation of the Thue-Morse sequence
------------------------------------------------------------------------

-- The paper "Productivity of stream definitions" by Endrullis et al.
-- (TCS 2010) uses a certain definition of the Thue-Morse sequence as
-- a running example.

-- Note that the code below makes use of the fact that Agda's
-- termination checker allows "swapping of arguments", which was not
-- mentioned when the termination checker was described in the paper
-- "Beating the Productivity Checker Using Embedded Languages".
-- However, it is easy to rewrite the code into a form which does not
-- make use of swapping, at the cost of some code duplication.

module ThueMorse where

open import Codata.Musical.Notation
open import Codata.Musical.Stream as S using (Stream; _≈_)
open S.Stream; open S._≈_
open import Data.Bool using (Bool; not); open Data.Bool.Bool
open import Function
open import Relation.Binary
import Relation.Binary.PropositionalEquality as P
import Relation.Binary.Reasoning.Setoid as EqReasoning

private
  module SS {A : Set} = Setoid (S.setoid A)
  open module SR {A : Set} = EqReasoning (S.setoid A)
    using (begin_; _∎)

------------------------------------------------------------------------
-- Chunks

-- A value of type Chunks describes how a stream is generated. Note
-- that an infinite sequence of empty chunks is not allowed.

data Chunks : Set where
  -- Start the next chunk.
  next : (m :   Chunks) → Chunks
  -- Cons an element to the current chunk.
  cons : (m : ∞ Chunks) → Chunks

-- Equality of chunks.

infix 4 _≈C_

data _≈C_ : Chunks → Chunks → Set where
  next : ∀ {m m′} (m≈m′ :      m ≈C   m′ ) → next m ≈C next m′
  cons : ∀ {m m′} (m≈m′ : ∞ (♭ m ≈C ♭ m′)) → cons m ≈C cons m′

------------------------------------------------------------------------
-- Chunk transformers

tailC : Chunks → Chunks
tailC (next m) = next (tailC m)
tailC (cons m) = ♭ m

mutual

  evensC : Chunks → Chunks
  evensC (next m) = next (evensC m)
  evensC (cons m) = cons (♯ oddsC (♭ m))

  oddsC : Chunks → Chunks
  oddsC (next m) = next (oddsC m)
  oddsC (cons m) = evensC (♭ m)

infixr 5 _⋎C_

-- Note that care is taken to create as few and large chunks as
-- possible (see also _⋎W_).

_⋎C_ : Chunks → Chunks → Chunks
next m ⋎C next m′ = next (m ⋎C      m′)   -- Two chunks in, one out.
next m ⋎C cons m′ = next (m ⋎C cons m′)
cons m ⋎C      m′ = cons (♯ (m′ ⋎C ♭ m))

------------------------------------------------------------------------
-- Stream programs

-- StreamP m A encodes programs which generate streams with chunk
-- sizes given by m.

infixr 5 _∷_ _⋎_

data StreamP : Chunks → Set → Set₁ where
  [_]     : ∀ {m A} (xs : ∞ (StreamP m A)) → StreamP (next m) A
  _∷_     : ∀ {m A} (x : A) (xs : StreamP (♭ m) A) → StreamP (cons m) A
  tail    : ∀ {m A} (xs : StreamP m A) → StreamP (tailC m) A
  evens   : ∀ {m A} (xs : StreamP m A) → StreamP (evensC m) A
  odds    : ∀ {m A} (xs : StreamP m A) → StreamP (oddsC m) A
  _⋎_     : ∀ {m m′ A} (xs : StreamP m A) (ys : StreamP m′ A) →
            StreamP (m ⋎C m′) A
  map     : ∀ {m A B} (f : A → B) (xs : StreamP m A) → StreamP m B
  cast    : ∀ {m m′ A} (ok : m ≈C m′) (xs : StreamP m A) → StreamP m′ A

data StreamW : Chunks → Set → Set₁ where
  [_] : ∀ {m A} (xs : StreamP m A) → StreamW (next m) A
  _∷_ : ∀ {m A} (x : A) (xs : StreamW (♭ m) A) → StreamW (cons m) A

program : ∀ {m A} → StreamW m A → StreamP m A
program [ xs ]   = [ ♯ xs ]
program (x ∷ xs) = x ∷ program xs

tailW : ∀ {m A} → StreamW m A → StreamW (tailC m) A
tailW [ xs ]   = [ tail xs ]
tailW (x ∷ xs) = xs

mutual

  evensW : ∀ {m A} → StreamW m A → StreamW (evensC m) A
  evensW [ xs ]   = [ evens xs ]
  evensW (x ∷ xs) = x ∷ oddsW xs

  oddsW : ∀ {m A} → StreamW m A → StreamW (oddsC m) A
  oddsW [ xs ]   = [ odds xs ]
  oddsW (x ∷ xs) = evensW xs

infixr 5 _⋎W_

-- Note: Uses swapping of arguments.

_⋎W_ : ∀ {m m′ A} → StreamW m A → StreamW m′ A → StreamW (m ⋎C m′) A
[ xs ]   ⋎W [ ys ]   = [ xs ⋎ ys ]
[ xs ]   ⋎W (y ∷ ys) = [ xs ⋎ program (y ∷ ys) ]
(x ∷ xs) ⋎W ys       = x ∷ ys ⋎W xs

mapW : ∀ {m A B} → (A → B) → StreamW m A → StreamW m B
mapW f [ xs ]   = [ map f xs ]
mapW f (x ∷ xs) = f x ∷ mapW f xs

castW : ∀ {m m′ A} → m ≈C m′ → StreamW m A → StreamW m′ A
castW (next m≈m′) [ xs ]   = [ cast m≈m′ xs ]
castW (cons m≈m′) (x ∷ xs) = x ∷ castW (♭ m≈m′) xs

whnf : ∀ {m A} → StreamP m A → StreamW m A
whnf [ xs ]         = [ ♭ xs ]
whnf (x ∷ xs)       = x ∷ whnf xs
whnf (tail xs)      = tailW (whnf xs)
whnf (evens xs)     = evensW (whnf xs)
whnf (odds xs)      = oddsW (whnf xs)
whnf (xs ⋎ ys)      = whnf xs ⋎W whnf ys
whnf (map f xs)     = mapW f (whnf xs)
whnf (cast m≈m′ xs) = castW m≈m′ (whnf xs)

mutual

  ⟦_⟧W : ∀ {m A} → StreamW m A → Stream A
  ⟦ [ xs ] ⟧W = ⟦ xs ⟧P
  ⟦ x ∷ xs ⟧W = x ∷ ♯ ⟦ xs ⟧W

  ⟦_⟧P : ∀ {m A} → StreamP m A → Stream A
  ⟦ xs ⟧P = ⟦ whnf xs ⟧W

------------------------------------------------------------------------
-- The Thue-Morse sequence

[ccn]ω : Chunks
[ccn]ω = cons (♯ cons (♯ next [ccn]ω))

[cn]²[ccn]ω : Chunks
[cn]²[ccn]ω = cons (♯ next (cons (♯ next [ccn]ω)))

[cn]³[ccn]ω : Chunks
[cn]³[ccn]ω = cons (♯ next [cn]²[ccn]ω)

-- Explanation of the proof of lemma₁:
--
-- odds [ccn]ω ≈ [cn]ω
--
-- [cn]ω ⋎ [ccn]ω ≈
-- c ([ccn]ω ⋎ n[cn]ω) ≈
-- c c (n[cn]ω ⋎ cn[ccn]ω) ≈
-- c c n ([cn]ω ⋎ cn[ccn]ω) ≈
-- c c n c (cn[ccn]ω ⋎ n[cn]ω) ≈
-- c c n c c (n[cn]ω ⋎ n[ccn]ω) ≈
-- c c n c c n ([cn]ω ⋎ [ccn]ω)

lemma₁ : oddsC [ccn]ω ⋎C [ccn]ω ≈C [ccn]ω
lemma₁ = cons (♯ cons (♯ next (cons (♯ cons (♯ next lemma₁)))))

-- Explanation of the proof of lemma:
--
-- evens [cn]³[ccn]ω ≈ cnn[cn]ω
-- tail  [cn]³[ccn]ω ≈ n[cn]²[ccn]ω
--
-- cnn[cn]ω ⋎ n[cn]²[ccn]ω ≈
-- c (n[cn]²[ccn]ω ⋎ nn[cn]ω) ≈
-- c n ([cn]²[ccn]ω ⋎ n[cn]ω) ≈
-- c n c (n[cn]ω ⋎ ncn[ccn]ω) ≈
-- c n c n ([cn]ω ⋎ cn[ccn]ω) ≈
-- c n c n c (cn[ccn]ω ⋎ n[cn]ω) ≈
-- c n c n c c (n[cn]ω ⋎ n[ccn]ω) ≈
-- c n c n c c n ([cn]ω ⋎ [ccn]ω)

lemma : evensC [cn]³[ccn]ω ⋎C tailC [cn]³[ccn]ω ≈C [cn]²[ccn]ω
lemma = cons (♯ next (cons (♯ next (cons (♯ cons (♯ next lemma₁))))))

thueMorse : StreamP [cn]³[ccn]ω Bool
thueMorse =
  false ∷ [ ♯ cast lemma (map not (evens thueMorse) ⋎ tail thueMorse) ]

------------------------------------------------------------------------
-- Equality programs

infix  4 _≈[_]P_ _≈[_]W_
infixr 2 _≈⟨_⟩P_ _≈⟨_⟩_

data _≈[_]P_ : {A : Set} → Stream A → Chunks → Stream A → Set₁ where
  [_]     : ∀ {m A} {xs ys : Stream A}
            (xs≈ys : ∞ (xs ≈[ m ]P ys)) → xs ≈[ next m ]P ys
  _∷_     : ∀ {m A} (x : A) {xs ys}
            (xs≈ys : ♭ xs ≈[ ♭ m ]P ♭ ys) → x ∷ xs ≈[ cons m ]P x ∷ ys
  tail    : ∀ {m A} {xs ys : Stream A} (xs≈ys : xs ≈[ m ]P ys) →
            S.tail xs ≈[ tailC m ]P S.tail ys
  evens   : ∀ {m A} {xs ys : Stream A} (xs≈ys : xs ≈[ m ]P ys) →
            S.evens xs ≈[ evensC m ]P S.evens ys
  odds    : ∀ {m A} {xs ys : Stream A} (xs≈ys : xs ≈[ m ]P ys) →
            S.odds xs ≈[ oddsC m ]P S.odds ys
  _⋎_     : ∀ {m m′ A} {xs xs′ ys ys′ : Stream A}
            (xs≈ys : xs ≈[ m ]P ys) (xs′≈ys′ : xs′ ≈[ m′ ]P ys′) →
            (xs ⟨ S._⋎_ ⟩ xs′) ≈[ m ⋎C m′ ]P (ys ⟨ S._⋎_ ⟩ ys′)
  map     : ∀ {m A B} (f : A → B) {xs ys : Stream A}
            (xs≈ys : xs ≈[ m ]P ys) → S.map f xs ≈[ m ]P S.map f ys
  cast    : ∀ {m m′ A} (ok : m ≈C m′) {xs ys : Stream A}
            (xs≈ys : xs ≈[ m ]P ys) → xs ≈[ m′ ]P ys
  _≈⟨_⟩P_ : ∀ {m A} xs {ys zs : Stream A}
            (xs≈ys : xs ≈[ m ]P ys) (ys≈zs : ys ≈ zs) → xs ≈[ m ]P zs
  _≈⟨_⟩_  : ∀ {m A} xs {ys zs : Stream A}
            (xs≈ys : xs ≈ ys) (ys≈zs : ys ≈[ m ]P zs) → xs ≈[ m ]P zs

data _≈[_]W_ : {A : Set} → Stream A → Chunks → Stream A → Set₁ where
  [_]     : ∀ {m A} {xs ys : Stream A}
            (xs≈ys : xs ≈[ m ]P ys) → xs ≈[ next m ]W ys
  _∷_     : ∀ {m A} (x : A) {xs ys}
            (xs≈ys : ♭ xs ≈[ ♭ m ]W ♭ ys) → x ∷ xs ≈[ cons m ]W x ∷ ys

program≈ : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]W ys → xs ≈[ m ]P ys
program≈ [ xs≈ys ]   = [ ♯ xs≈ys ]
program≈ (x ∷ xs≈ys) = x ∷ program≈ xs≈ys

tail-congW : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]W ys →
             S.tail xs ≈[ tailC m ]W S.tail ys
tail-congW [ xs≈ys ]   = [ tail xs≈ys ]
tail-congW (x ∷ xs≈ys) = xs≈ys

mutual

  evens-congW : ∀ {m A} {xs ys : Stream A} →
                xs ≈[ m ]W ys → S.evens xs ≈[ evensC m ]W S.evens ys
  evens-congW [ xs≈ys ]   = [ evens xs≈ys ]
  evens-congW (x ∷ xs≈ys) = x ∷ odds-congW xs≈ys

  odds-congW : ∀ {m A} {xs ys : Stream A} →
               xs ≈[ m ]W ys → S.odds xs ≈[ oddsC m ]W S.odds ys
  odds-congW [ xs≈ys ]   = [ odds xs≈ys ]
  odds-congW (x ∷ xs≈ys) = evens-congW xs≈ys

infixr 5 _⋎-congW_

-- Note: Uses swapping of arguments.

_⋎-congW_ : ∀ {m m′ A} {xs xs′ ys ys′ : Stream A} →
            xs ≈[ m ]W ys → xs′ ≈[ m′ ]W ys′ →
            (xs ⟨ S._⋎_ ⟩ xs′) ≈[ m ⋎C m′ ]W (ys ⟨ S._⋎_ ⟩ ys′)
[ xs≈ys ]   ⋎-congW [ xs′≈ys′ ]   = [ xs≈ys ⋎ xs′≈ys′ ]
[ xs≈ys ]   ⋎-congW (y ∷ xs′≈ys′) = [ xs≈ys ⋎ program≈ (y ∷ xs′≈ys′) ]
(x ∷ xs≈ys) ⋎-congW xs′≈ys′       = x ∷ xs′≈ys′ ⋎-congW xs≈ys

map-congW : ∀ {m A B} (f : A → B) {xs ys : Stream A} →
            xs ≈[ m ]W ys → S.map f xs ≈[ m ]W S.map f ys
map-congW f [ xs≈ys ]   = [ map f xs≈ys ]
map-congW f (x ∷ xs≈ys) = f x ∷ map-congW f xs≈ys

cast-congW : ∀ {m m′ A} (ok : m ≈C m′) {xs ys : Stream A} →
             xs ≈[ m ]W ys → xs ≈[ m′ ]W ys
cast-congW (next m≈m′) [ xs≈ys ]   = [ cast m≈m′ xs≈ys ]
cast-congW (cons m≈m′) (x ∷ xs≈ys) = x ∷ cast-congW (♭ m≈m′) xs≈ys

transPW : ∀ {m A} {xs ys zs : Stream A} →
          xs ≈[ m ]W ys → ys ≈ zs → xs ≈[ m ]W zs
transPW [ xs≈ys ]   ys≈zs            = [ _ ≈⟨ xs≈ys ⟩P ys≈zs ]
transPW (x ∷ xs≈ys) (P.refl ∷ ys≈zs) = x ∷ transPW xs≈ys (♭ ys≈zs)

transW : ∀ {m A} {xs ys zs : Stream A} →
         xs ≈ ys → ys ≈[ m ]W zs → xs ≈[ m ]W zs
transW (x ∷ xs≈ys)      [ ys≈zs ]   = [ _ ≈⟨ x ∷ xs≈ys ⟩ ys≈zs ]
transW (P.refl ∷ xs≈ys) (x ∷ ys≈zs) = x ∷ transW (♭ xs≈ys) ys≈zs

whnf≈ : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]P ys → xs ≈[ m ]W ys
whnf≈ [ xs ]                 = [ ♭ xs ]
whnf≈ (x ∷ xs)               = x ∷ whnf≈ xs
whnf≈ (tail xs)              = tail-congW (whnf≈ xs)
whnf≈ (evens xs)             = evens-congW (whnf≈ xs)
whnf≈ (odds xs)              = odds-congW (whnf≈ xs)
whnf≈ (xs ⋎ ys)              = whnf≈ xs ⋎-congW whnf≈ ys
whnf≈ (map f xs)             = map-congW f (whnf≈ xs)
whnf≈ (cast m≈m′ xs)         = cast-congW m≈m′ (whnf≈ xs)
whnf≈ (xs ≈⟨ xs≈ys ⟩P ys≈zs) = transPW (whnf≈ xs≈ys) ys≈zs
whnf≈ (xs ≈⟨ xs≈ys ⟩  ys≈zs) = transW xs≈ys (whnf≈ ys≈zs)

mutual

  soundW : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]W ys → xs ≈ ys
  soundW [ xs≈ys ]   = soundP xs≈ys
  soundW (x ∷ xs≈ys) = P.refl ∷ ♯ soundW xs≈ys

  soundP : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]P ys → xs ≈ ys
  soundP xs≈ys = soundW (whnf≈ xs≈ys)

------------------------------------------------------------------------
-- The definition is correct

-- The proof consists mostly of boiler-plate code.

program-hom : ∀ {m A} (xs : StreamW m A) → ⟦ program xs ⟧P ≈ ⟦ xs ⟧W
program-hom [ xs ]   = SS.refl
program-hom (x ∷ xs) = P.refl ∷ ♯ program-hom xs

mutual

  tailW-hom : ∀ {A : Set} {m} (xs : StreamW m A) →
               ⟦ tailW xs ⟧W ≈ S.tail ⟦ xs ⟧W
  tailW-hom [ xs ]   = tail-hom xs
  tailW-hom (x ∷ xs) = SS.refl

  tail-hom : ∀ {A : Set} {m} (xs : StreamP m A) →
              ⟦ tail xs ⟧P ≈ S.tail ⟦ xs ⟧P
  tail-hom xs = tailW-hom (whnf xs)

mutual

  infixr 5 _⋎W-hom_ _⋎-hom_

  -- Note: Uses swapping of arguments.

  _⋎W-hom_ : ∀ {A : Set} {m m′} (xs : StreamW m A) (ys : StreamW m′ A) →
             ⟦ xs ⋎W ys ⟧W ≈[ m ⋎C m′ ]P (⟦ xs ⟧W ⟨ S._⋎_ ⟩ ⟦ ys ⟧W)
  (x ∷ xs) ⋎W-hom ys        = x ∷ ys ⋎W-hom xs
  [ xs ]   ⋎W-hom [ ys ]    = [ ♯ (xs ⋎-hom ys) ]
  [ xs ]   ⋎W-hom (y ∷ ys′) =
    [ ♯ (⟦ xs ⋎ program ys ⟧P                 ≈⟨ xs ⋎-hom program ys ⟩P (begin
         (⟦ xs ⟧P ⟨ S._⋎_ ⟩ ⟦ program ys ⟧P)  SR.≈⟨ SS.refl ⟨ S._⋎-cong_ ⟩ program-hom ys ⟩
         (⟦ xs ⟧P ⟨ S._⋎_ ⟩ ⟦ ys ⟧W)          ∎)) ]
    where ys = y ∷ ys′

  _⋎-hom_ : ∀ {A : Set} {m m′} (xs : StreamP m A) (ys : StreamP m′ A) →
            ⟦ xs ⋎ ys ⟧P ≈[ m ⋎C m′ ]P (⟦ xs ⟧P ⟨ S._⋎_ ⟩ ⟦ ys ⟧P)
  xs ⋎-hom ys = whnf xs ⋎W-hom whnf ys

mutual

  evensW-hom : ∀ {A : Set} {m} (xs : StreamW m A) →
               ⟦ evensW xs ⟧W ≈ S.evens ⟦ xs ⟧W
  evensW-hom [ xs ]   = evens-hom xs
  evensW-hom (x ∷ xs) = P.refl ∷ ♯ oddsW-hom xs

  evens-hom : ∀ {A : Set} {m} (xs : StreamP m A) →
              ⟦ evens xs ⟧P ≈ S.evens ⟦ xs ⟧P
  evens-hom xs = evensW-hom (whnf xs)

  oddsW-hom : ∀ {A : Set} {m} (xs : StreamW m A) →
              ⟦ oddsW xs ⟧W ≈ S.odds ⟦ xs ⟧W
  oddsW-hom [ xs ]   = odds-hom xs
  oddsW-hom (x ∷ xs) = evensW-hom xs

  odds-hom : ∀ {A : Set} {m} (xs : StreamP m A) →
             ⟦ odds xs ⟧P ≈ S.odds ⟦ xs ⟧P
  odds-hom xs = oddsW-hom (whnf xs)

mutual

  mapW-hom : ∀ {A B : Set} {m} (f : A → B) (xs : StreamW m A) →
             ⟦ mapW f xs ⟧W ≈ S.map f ⟦ xs ⟧W
  mapW-hom f [ xs ]   = map-hom f xs
  mapW-hom f (x ∷ xs) = P.refl ∷ ♯ mapW-hom f xs

  map-hom : ∀ {A B : Set} {m} (f : A → B) (xs : StreamP m A) →
            ⟦ map f xs ⟧P ≈ S.map f ⟦ xs ⟧P
  map-hom f xs = mapW-hom f (whnf xs)

mutual

  castW-hom : ∀ {m m′ A} (m≈m′ : m ≈C m′) (xs : StreamW m A) →
              ⟦ castW m≈m′ xs ⟧W ≈ ⟦ xs ⟧W
  castW-hom (next m≈m′) [ xs ]   = cast-hom m≈m′ xs
  castW-hom (cons m≈m′) (x ∷ xs) = P.refl ∷ ♯ castW-hom (♭ m≈m′) xs

  cast-hom : ∀ {m m′ A} (m≈m′ : m ≈C m′) (xs : StreamP m A) →
             ⟦ cast m≈m′ xs ⟧P ≈ ⟦ xs ⟧P
  cast-hom m≈m′ xs = castW-hom m≈m′ (whnf xs)

-- The intended definition of the Thue-Morse sequence is bs = rhs bs.

rhs : Stream Bool → Stream Bool
rhs bs = false ∷ ♯ (S.map not (S.evens bs) ⟨ S._⋎_ ⟩ S.tail bs)

-- The definition above satisfies the intended defining equation.

correct : ⟦ thueMorse ⟧P ≈[ [cn]³[ccn]ω ]P rhs ⟦ thueMorse ⟧P
correct = false ∷ [ ♯ cast lemma (
  ⟦ cast lemma (map not (evens thueMorse) ⋎ tail thueMorse) ⟧P          ≈⟨ cast-hom lemma (map not (evens thueMorse) ⋎ tail thueMorse) ⟩
  ⟦ map not (evens thueMorse) ⋎ tail thueMorse ⟧P                       ≈⟨ map not (evens thueMorse) ⋎-hom tail thueMorse ⟩P (begin
  (⟦ map not (evens thueMorse) ⟧P ⟨ S._⋎_ ⟩ ⟦ tail thueMorse ⟧P)        SR.≈⟨ SS.trans (map-hom not (evens thueMorse))
                                                                                (S.map-cong not (evens-hom thueMorse))
                                                                             ⟨ S._⋎-cong_ ⟩
                                                                           tail-hom thueMorse ⟩
  (S.map not (S.evens ⟦ thueMorse ⟧P) ⟨ S._⋎_ ⟩ S.tail ⟦ thueMorse ⟧P)  ∎ )) ]

-- The defining equation has at most one solution.

unique : ∀ bs bs′ → bs ≈ rhs bs → bs′ ≈ rhs bs′ → bs ≈[ [cn]³[ccn]ω ]P bs′
unique bs bs′ bs≈ bs′≈ =
  bs      ≈⟨ bs≈ ⟩
  rhs bs  ≈⟨ false ∷ [ ♯ cast lemma
                           (map not (evens (unique bs bs′ bs≈ bs′≈))
                              ⋎
                            tail (unique bs bs′ bs≈ bs′≈)) ] ⟩P (begin
  rhs bs′ SR.≈⟨ SS.sym bs′≈ ⟩
  bs′     ∎)

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
-- {-# OPTIONS -v tc.proj.like:30 #-}

open import Common.Bool
open import Common.Equality

abstract
  Id : Set → Set
  Id A = A

f : ∀ A → Id A → Id A
f A x = x

postulate
  foo : ∀{X : Set} (x y : X) → x ≡ y → Set

abstract
  bla : Set
  bla = foo (f Bool true) false refl

-- WAS:
-- true != false of type Bool
-- when checking that the expression refl has type f _ true ≡ false

-- EXPECTED:
-- true != false of type Bool
-- when checking that the expression refl has type f Bool true ≡ false

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
-- Andreas, 2019-07-04, issue #3886
-- Override forcing with explicit quantity attributes.

open import Common.Prelude

pattern [_] x = x ∷ []

module _ {a} {A : Set a} where

  variable
    x y z : A
    @0 xs ys zs : List A

  data FSet : List A → Set a where
    ∅   : FSet []
    _∪_ : FSet xs → FSet ys → FSet (xs ++ ys)
    sg  : (@ω x : A) → FSet [ x ]
    -- x is forced here, but this is not wanted.
    -- With an explicit quantity attribute we tell the forcing machinery not to erase x.

  -- Since xs is erased, we cannot get x from sg x : FSet xs (with xs = [ x ])
  -- unless x is retained in sg x.
  elements : {@0 xs : List A} → FSet xs → List A
  elements ∅       = []
  elements (s ∪ t) = elements s ++ elements t
  elements (sg x)  = [ x ]

-- ERROR WAS:
-- Variable x is declared erased, so it cannot be used here
-- when checking that the expression x has type A

mySet = (sg 1 ∪ sg 2) ∪ (sg 3 ∪ sg 4)

sum : List Nat → Nat
sum [] = 0
sum (n ∷ ns) = n + sum ns

test = elements mySet

main = printNat (sum (elements mySet))

-- Should print 10.


text:
{-# OPTIONS --cubical --safe #-}

module Data.List.Syntax where

open import Data.List
open import Prelude

record ListSyntax {a b} (A : Type a) (B : Type b) : Type (a ℓ⊔ b) where
  field [_] : B → List A

open ListSyntax ⦃ ... ⦄ public

instance
  cons : ⦃ _ : ListSyntax A B ⦄ →  ListSyntax A (A × B)
  [_] ⦃ cons ⦄ (x , xs) = x ∷ [ xs ]

instance
  sing : ListSyntax A A
  [_] ⦃ sing ⦄ = _∷ []

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
open import Level using () renaming (zero to ℓ₀)
open import Relation.Binary using (DecSetoid)

module Bidir (A : DecSetoid ℓ₀ ℓ₀) where

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)
import Level
import Category.Monad
import Category.Functor
open import Data.Maybe using (Maybe ; nothing ; just ; maybe′ ; drop-just) renaming (setoid to MaybeSetoid ; Eq to MaybeEq)
open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
open import Data.List using (List)
open import Data.List.All using (All)
open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map ; allFin) renaming (lookup to lookupVec)
open import Data.Vec.Equality using () renaming (module Equality to VecEq)
open import Data.Vec.Properties using (lookup∘tabulate ; map-cong ; map-∘ ; map-lookup-allFin)
open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂)
open import Function using (id ; _∘_ ; flip)
open import Relation.Binary.Core using (refl ; _≡_)
open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid)
open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans ; cong₂ ; decSetoid ; module ≡-Reasoning) renaming (setoid to EqSetoid)
open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid)
import Relation.Binary.EqReasoning as EqR

open import Structures using (Functor ; IsFunctor ; Shaped ; module Shaped)
open import Instances using (MaybeFunctor ; ShapedISetoid)
import GetTypes
open GetTypes.PartialShapeShape using (Get ; module Get)
open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid ; just-injective)
open import FinMap
import CheckInsert
open CheckInsert A
import BFF
open BFF.PartialShapeBFF A using (assoc ; enumerate ; denumerate ; bff)
open Setoid using () renaming (_≈_ to _∋_≈_)
open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)

lemma-1 : {m n : ℕ} → (f : Fin n → Carrier) → (is : Vec (Fin n) m) → assoc is (map f is) ≡ just (restrict f is)
lemma-1 f []        = refl
lemma-1 f (i ∷ is′) = begin
  (assoc is′ (map f is′) >>= checkInsert i (f i))
    ≡⟨ cong (λ m → m >>= checkInsert i (f i)) (lemma-1 f is′) ⟩
  checkInsert i (f i) (restrict f is′)
    ≡⟨ lemma-checkInsert-restrict f i is′ ⟩
  just (restrict f (i ∷ is′)) ∎
  where open ≡-Reasoning

lemma-lookupM-checkInserted : {n : ℕ} → (i : Fin n) → (x : Carrier) → (h : FinMapMaybe n Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert i x h ≡ just h' → MaybeSetoid A.setoid ∋ lookupM i h' ≈ just x
lemma-lookupM-checkInserted i x h p with checkInsert i x h | insertionresult i x h
lemma-lookupM-checkInserted i x h refl | ._ | same x' x≈x' pl = begin
  lookupM i h
    ≡⟨ pl ⟩
  just x'
    ≈⟨ MaybeEq.just (Setoid.sym A.setoid x≈x') ⟩
  just x ∎
  where open EqR (MaybeSetoid A.setoid)
lemma-lookupM-checkInserted i x h refl | ._ | new _ = Setoid.reflexive (MaybeSetoid A.setoid) (lemma-lookupM-insert i x h)
lemma-lookupM-checkInserted i x h () | ._ | wrong _ _ _

_in-domain-of_ : {m n : ℕ} {A : Set} → (is : Vec (Fin m) n) → (FinMapMaybe m A) → Set
_in-domain-of_ is h = All (λ i → ∃ λ x → lookupM i h ≡ just x) (toList is)

lemma-assoc-domain : {m n : ℕ} → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → is in-domain-of h
lemma-assoc-domain []         []         ph = Data.List.All.[]
lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph with assoc is' xs' | inspect (assoc is') xs'
lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | nothing | [ ph' ]
lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph | just h' | [ ph' ] with checkInsert i' x' h' | inspect (checkInsert i' x') h' | insertionresult i' x' h'
lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' ph')
lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_
  (x' , lemma-lookupM-insert i' x' h')
  (Data.List.All.map
    (λ {i} p → proj₁ p , lemma-lookupM-checkInsert i i' h' (proj₂ p) x' cI≡)
    (lemma-assoc-domain is' xs' ph'))
lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | just h' | [ ph' ] | ._ | _ | wrong _ _ _

lemma-map-lookupM-assoc : {m : ℕ} → (i : Fin m) → (x : Carrier) → (h : FinMapMaybe m Carrier) → {h' : FinMapMaybe m Carrier} → checkInsert i x h ≡ just h' → {n : ℕ} → (js : Vec (Fin m) n) → js in-domain-of h → map (flip lookupM h') js ≡ map (flip lookupM h) js
lemma-map-lookupM-assoc i x h ph [] pj = refl
lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) = cong₂ _∷_
  (trans (lemma-lookupM-checkInsert j i h pl x ph) (sym pl))
  (lemma-map-lookupM-assoc i x h ph js pj)

lemma-2 : {m n : ℕ} → (is : Vec (Fin n) m) → (v : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is v ≡ just h → VecISetoid (MaybeSetoid A.setoid) at _ ∋ map (flip lookupM h) is ≈ map just v
lemma-2 []       []       h p = ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))
lemma-2 (i ∷ is) (x ∷ xs) h p with assoc is xs | inspect (assoc is) xs
lemma-2 (i ∷ is) (x ∷ xs) h () | nothing | _
lemma-2 (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin
  lookupM i h ∷ map (flip lookupM h) is
    ≈⟨ VecEq._∷-cong_ (lemma-lookupM-checkInserted i x h' p) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩
  just x ∷ map (flip lookupM h) is
    ≡⟨  cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h' p is (lemma-assoc-domain is xs ir)) ⟩
  just x ∷ map (flip lookupM h') is
    ≈⟨ VecEq._∷-cong_ (Setoid.refl (MaybeSetoid A.setoid)) (lemma-2 is xs h' ir) ⟩
  just x ∷ map just xs ∎
  where open EqR (VecISetoid (MaybeSetoid A.setoid) at _)

lemma-fmap-denumerate-enumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {α : Set} {s : S} → (c : C α s) → Shaped.fmap ShapeT (denumerate ShapeT c) (enumerate ShapeT s) ≡ c
lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin
  fmap (denumerate ShapeT c) (fill s (allFin (arity s)))
    ≡⟨ fill-fmap (denumerate ShapeT c) s (allFin (arity s)) ⟩
  fill s (map (flip lookupVec (content c)) (allFin (arity s)))
    ≡⟨ cong (fill s) (map-lookup-allFin (content c)) ⟩
  fill s (content c)
    ≡⟨ content-fill c ⟩
  c ∎
  where open ≡-Reasoning
        open Shaped ShapeT

theorem-1 : (G : Get) → {i : Get.I G} → (s : Get.SourceContainer G Carrier (Get.gl₁ G i)) → bff G i s (Get.get G s) ≡ just (Get.fmapS G just s)
theorem-1 G {i} s = begin
  bff G i s (get s)
    ≡⟨ cong (bff G i s ∘ get) (sym (lemma-fmap-denumerate-enumerate SourceShapeT s)) ⟩
  bff G i s (get (fmapS f t))
    ≡⟨ cong (bff G i s) (free-theorem f t) ⟩
  bff G i s (fmapV f (get t))
    ≡⟨ refl ⟩
  h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT (fmapV f (get t)))))
    ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′ ∘ assoc (Shaped.content ViewShapeT (get t))) (Shaped.fmap-content ViewShapeT f (get t)) ⟩
  h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (map f (Shaped.content ViewShapeT (get t)))))
    ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (Shaped.content ViewShapeT (get t))) ⟩
  (Maybe.just ∘ h′↦r ∘ h↦h′) (restrict f (Shaped.content ViewShapeT (get t)))
    ≡⟨ cong just (begin
      h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) (reshape g′ (Shaped.arity SourceShapeT (gl₁ i))))
        ≡⟨ cong (h′↦r ∘ union (restrict f (Shaped.content ViewShapeT (get t)))) (lemma-reshape-id g′) ⟩
      h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) g′)
        ≡⟨ cong h′↦r (lemma-disjoint-union f (Shaped.content ViewShapeT (get t))) ⟩
      h′↦r (fromFunc f)
        ≡⟨ refl ⟩
      fmapS (flip lookupM (fromFunc f)) t
        ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc f) t ⟩
      fmapS (Maybe.just ∘ f) t
        ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (gl₁ i)) just f t ⟩
      fmapS just (fmapS f t)
        ≡⟨ cong (fmapS just) (lemma-fmap-denumerate-enumerate SourceShapeT s) ⟩
      fmapS just s ∎) ⟩ _ ∎
    where open ≡-Reasoning
          open Get G
          t    = enumerate SourceShapeT (gl₁ i)
          f    = denumerate SourceShapeT s
          g′   = delete-many (Shaped.content ViewShapeT (get t)) (fromFunc f)
          h↦h′ = flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ i)))
          h′↦r = (λ f′ → fmapS f′ t) ∘ flip lookupM

lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a
lemma-<$>-just (just x) f<$>ma≡just-b = x , refl
lemma-<$>-just nothing  ()

lemma-union-not-used : {n : ℕ} → {A : Set} → (h h′ : FinMapMaybe n A) → (i : Fin n) → ∃ (λ x → lookupM i h ≡ just x) → lookupM i (union h h′) ≡ lookupM i h
lemma-union-not-used h h′ i (x , px) = begin
  lookupM i (union h h′)
    ≡⟨ lookup∘tabulate (λ j → maybe′ just (lookupM j h′) (lookupM j h)) i ⟩
  maybe′ just (lookupM i h′) (lookupM i h)
    ≡⟨ cong (maybe′ just (lookupM i h′)) px ⟩
  maybe′ just (lookupM i h′) (just x)
    ≡⟨ sym px ⟩
  lookupM i h ∎
  where open ≡-Reasoning

lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma >>= f) ≡ just b → ∃ λ a → ma ≡ just a
lemma->>=-just (just a) p = a , refl
lemma->>=-just nothing  ()

lemma-just-sequenceV : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v
lemma-just-sequenceV []       = refl
lemma-just-sequenceV (x ∷ xs) = cong (_<$>_ (_∷_ x)) (lemma-just-sequenceV xs)

lemma-just-sequence : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {A : Set} {s : S} → (c : C A s) → Shaped.sequence ShapeT (Shaped.fmap ShapeT just c) ≡ just c
lemma-just-sequence ShapeT {s = s} c = begin
  fill s <$> sequenceV (content (fmap just c))
    ≡⟨ cong (_<$>_ (fill s) ∘ sequenceV) (fmap-content just c) ⟩
  fill s <$> sequenceV (map just (content c))
    ≡⟨ cong (_<$>_ (fill s)) (lemma-just-sequenceV (content c)) ⟩
  fill s <$> just (content c)
    ≡⟨ cong just (content-fill c) ⟩
  just c ∎
  where open ≡-Reasoning
        open Shaped ShapeT

lemma-sequenceV-successful : {A : Set} {n : ℕ} → (v : Vec (Maybe A) n) → {r : Vec A n} → sequenceV v ≡ just r → v ≡ map just r
lemma-sequenceV-successful []             {r = []}       p = refl
lemma-sequenceV-successful (just x ∷ xs)                 p with sequenceV xs | inspect sequenceV xs
lemma-sequenceV-successful (just x ∷ xs)                 () | nothing | _
lemma-sequenceV-successful (just x ∷ xs)  {r = .x ∷ .ys} refl  | just ys | [ p′ ] = cong (_∷_ (just x)) (lemma-sequenceV-successful xs p′)
lemma-sequenceV-successful (nothing ∷ xs)                ()

lemma-sequence-successful : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {A : Set} {s : S} → (c : C (Maybe A) s) → {r : C A s} → Shaped.sequence ShapeT c ≡ just r → c ≡ Shaped.fmap ShapeT just r
lemma-sequence-successful ShapeT {s = s} c {r} p = just-injective (sym (begin
  fill s <$> (map just <$> (content <$> just r))
    ≡⟨ cong (_<$>_ (fill s) ∘ _<$>_ (map just)) (begin
      content <$> just r
        ≡⟨ cong (_<$>_ content) (sym p) ⟩
      content <$> (fill s <$> sequenceV (content c))
        ≡⟨ sym (Functor.composition MaybeFunctor content (fill s) (sequenceV (content c))) ⟩
      content ∘ fill s <$> sequenceV (content c)
        ≡⟨ Functor.cong MaybeFunctor (fill-content s) (sequenceV (content c)) ⟩
      id <$> sequenceV (content c)
        ≡⟨ Functor.identity MaybeFunctor (sequenceV (content c)) ⟩
      sequenceV (content c)
        ≡⟨ cong sequenceV (lemma-sequenceV-successful (content c) (proj₂ wp)) ⟩
      sequenceV (map just (proj₁ wp))
        ≡⟨ lemma-just-sequenceV (proj₁ wp) ⟩
      just (proj₁ (lemma-<$>-just (sequenceV (content c)) p)) ∎) ⟩
  fill s <$> (map just <$> just (proj₁ (lemma-<$>-just (sequenceV (content c)) p)))
    ≡⟨ cong (_<$>_ (fill s) ∘ just) (sym (lemma-sequenceV-successful (content c) (proj₂ wp))) ⟩
  fill s <$> just (content c)
    ≡⟨ cong just (content-fill c) ⟩
  just c ∎))
  where open ≡-Reasoning
        open Shaped ShapeT
        wp = lemma-<$>-just (sequenceV (content c)) p

module _ (G : Get) where
  open ≡-Reasoning
  open Get G
  open Shaped SourceShapeT using () renaming (sequence to sequenceSource)
  open Shaped ViewShapeT using () renaming (sequence to sequenceView)

  lemma-get-sequence : {A : Set} → {i : I} {v : SourceContainer (Maybe A) (gl₁ i)} {r : SourceContainer A (gl₁ i)} → sequenceSource v ≡ just r → get <$> sequenceSource v ≡ sequenceView (get v)
  lemma-get-sequence {v = v} {r = r} p = begin
    get <$> sequenceSource v
      ≡⟨ cong (_<$>_ get ∘ sequenceSource) (lemma-sequence-successful SourceShapeT v p) ⟩
    get <$> sequenceSource (fmapS just r)
      ≡⟨ cong (_<$>_ get) (lemma-just-sequence SourceShapeT r) ⟩
    get <$> just r
      ≡⟨ sym (lemma-just-sequence ViewShapeT (get r)) ⟩
    sequenceView (fmapV just (get r))
      ≡⟨ cong sequenceView (sym (free-theorem just r)) ⟩
    sequenceView (get (fmapS just r))
      ≡⟨ cong (sequenceView ∘ get) (sym (lemma-sequence-successful SourceShapeT v p)) ⟩
    sequenceView (get v) ∎

sequenceV-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) at n)} → VecISetoid (MaybeSetoid S) at _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S at n) ∋ sequenceV m₁ ≈ sequenceV m₂
sequenceV-cong {S}                                       VecEq.[]-cong = Setoid.refl (MaybeSetoid (VecISetoid S at _))
sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) with sequenceV xs | sequenceV ys | sequenceV-cong xs≈ys
sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | just sys | just p = MaybeEq.just (VecEq._∷-cong_ x≈y p)
sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | just sys | ()
sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | nothing | ()
sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _))
sequenceV-cong {S}                                       (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _))

sequence-cong : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Setoid ℓ₀ ℓ₀) → {s : S} {x y : C (Maybe (Setoid.Carrier α)) s} → ShapedISetoid (EqSetoid S) ShapeT (MaybeSetoid α) at _ ∋ x ≈ y → MaybeSetoid (ShapedISetoid (EqSetoid S) ShapeT α at _) ∋ Shaped.sequence ShapeT x ≈ Shaped.sequence ShapeT y
sequence-cong ShapeT α {x = x} {y = y} (shape≈ , content≈) with sequenceV (Shaped.content ShapeT x) | sequenceV (Shaped.content ShapeT y) | sequenceV-cong content≈
sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | just {x} {y} x≈y = just (refl , (begin
  content (fill s x)
    ≡⟨ fill-content s x ⟩
  x
    ≈⟨ x≈y ⟩
  y
    ≡⟨ sym (fill-content s y) ⟩
  content (fill s y) ∎))
  where open EqR (VecISetoid α at _)
        open Shaped ShapeT
sequence-cong ShapeT α (shape≈ , content≈) | .nothing  | .nothing  | nothing = nothing

module _ (G : Get) where
  open Get G
  open Shaped SourceShapeT using () renaming (arity to arityS)
  open Shaped ViewShapeT using () renaming (content to contentV)

  theorem-2 : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer (Maybe Carrier) (gl₁ j)) → bff G j s v ≡ just u → ShapedISetoid (EqSetoid _) ViewShapeT (MaybeSetoid A.setoid) at _ ∋ get u ≈ Get.fmapV G just v
  theorem-2 {i} j s v u p with lemma-<$>-just ((flip union (reshape (delete-many (contentV (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s))) (arityS (gl₁ j)))) <$> assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v)) p
  theorem-2 {i} j s v u p | h′ , ph′ with lemma-<$>-just (assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v)) ph′
  theorem-2 {i} j s v u p | h′ , ph′ | h , ph = refl , (begin
    contentV (get u)
      ≡⟨ cong contentV (just-injective (trans (cong (_<$>_ get) (sym p))
                                              (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph))) ⟩
    contentV (get (h′↦r (h↦h′ h)))
      ≡⟨ refl ⟩
    contentV (get (fmapS (flip lookupM (h↦h′ h)) t))
      ≡⟨ cong contentV (free-theorem (flip lookupM (h↦h′ h)) t) ⟩
    contentV (fmapV (flip lookupM (h↦h′ h)) (get t))
      ≡⟨ Shaped.fmap-content ViewShapeT (flip lookupM (h↦h′ h)) (get t) ⟩
    map (flip lookupM (h↦h′ h)) (contentV (get t))
      ≡⟨ lemma-exchange-maps (lemma-union-not-used h (reshape g′ (arityS (gl₁ j)))) (lemma-assoc-domain (contentV (get t)) (contentV v) ph) ⟩
    map (flip lookupM h) (contentV (get t))
      ≈⟨ lemma-2 (contentV (get t)) (contentV v) h ph ⟩
    map just (contentV v)
      ≡⟨ sym (Shaped.fmap-content ViewShapeT just v) ⟩
    contentV (fmapV just v) ∎)
      where open EqR (VecISetoid (MaybeSetoid A.setoid) at _)
            s′   = enumerate SourceShapeT (gl₁ i)
            g    = fromFunc (denumerate SourceShapeT s)
            g′   = delete-many (contentV (get s′)) g
            t    = enumerate SourceShapeT (gl₁ j)
            h↦h′ = flip union (reshape g′ (arityS (gl₁ j)))
            h′↦r = (λ f → fmapS f t) ∘ flip lookupM

module _ (G : Get) where
  open Get G

  theorem-2′ : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → (u : SourceContainer Carrier (gl₁ j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (EqSetoid _) ViewShapeT A.setoid at _ ∋ get u ≈ v
  theorem-2′ j s v u p = drop-just (begin
    get <$> just u
      ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence SourceShapeT u)) ⟩
    get <$> Shaped.sequence SourceShapeT (fmapS just u)
      ≡⟨ lemma-get-sequence G (lemma-just-sequence SourceShapeT u) ⟩
    Shaped.sequence ViewShapeT (get (fmapS just u))
      ≈⟨ sequence-cong ViewShapeT A.setoid (theorem-2 G j s v (fmapS just u) p) ⟩
    Shaped.sequence ViewShapeT (fmapV just v)
      ≡⟨ lemma-just-sequence ViewShapeT v ⟩
    just v ∎)
    where open EqR (MaybeSetoid (ShapedISetoid (EqSetoid _) ViewShapeT A.setoid at _))

max_stars_repo_name: jvoigtlaender/bidiragda

max_issues_repo_name: jvoigtlaender/bidiragda

max_forks_repo_name: jvoigtlaender/bidiragda


text:
------------------------------------------------------------------------
-- A bunch of properties
------------------------------------------------------------------------

module Data.Bool.Properties where

open import Data.Bool as Bool
open import Data.Fin
open import Data.Function
open import Algebra
open import Algebra.Structures
import Algebra.RingSolver.Simple as Solver
import Algebra.RingSolver.AlmostCommutativeRing as ACR
open import Relation.Nullary using (_⇔_)
open import Relation.Binary.PropositionalEquality
import Algebra.FunctionProperties as P; open P _≡_
open import Data.Product
open import Data.Sum
open import Data.Empty

import Relation.Binary.EqReasoning as EqR; open EqR Bool.setoid

------------------------------------------------------------------------
-- Duality

-- Can we take advantage of duality in some (nice) way?

------------------------------------------------------------------------
-- (Bool, ∨, ∧, false, true) forms a commutative semiring

private

  ∨-assoc : Associative _∨_
  ∨-assoc true  y z = refl
  ∨-assoc false y z = refl

  ∧-assoc : Associative _∧_
  ∧-assoc true  y z = refl
  ∧-assoc false y z = refl

  ∨-comm : Commutative _∨_
  ∨-comm true  true  = refl
  ∨-comm true  false = refl
  ∨-comm false true  = refl
  ∨-comm false false = refl

  ∧-comm : Commutative _∧_
  ∧-comm true  true  = refl
  ∧-comm true  false = refl
  ∧-comm false true  = refl
  ∧-comm false false = refl

  ∨-identity : Identity false _∨_
  ∨-identity = (λ _ → refl) , (λ x → ∨-comm x false)

  ∧-identity : Identity true _∧_
  ∧-identity = (λ _ → refl) , (λ x → ∧-comm x true)

  zero-∧ : Zero false _∧_
  zero-∧ = (λ _ → refl) , (λ x → ∧-comm x false)

  distrib-∧-∨ : _∧_ DistributesOver _∨_
  distrib-∧-∨ = distˡ , distʳ
    where
    distˡ : _∧_ DistributesOverˡ _∨_
    distˡ true  y z = refl
    distˡ false y z = refl

    distʳ : _∧_ DistributesOverʳ _∨_
    distʳ x y z =
                      begin
       (y ∨ z) ∧ x
                      ≈⟨ ∧-comm (y ∨ z) x ⟩
       x ∧ (y ∨ z)
                      ≈⟨ distˡ x y z ⟩
       x ∧ y ∨ x ∧ z
                      ≈⟨ cong₂ _∨_ (∧-comm x y) (∧-comm x z) ⟩
       y ∧ x ∨ z ∧ x
                      ∎

isCommutativeSemiring-∨-∧
  : IsCommutativeSemiring _≡_ _∨_ _∧_ false true
isCommutativeSemiring-∨-∧ = record
  { isSemiring = record
    { isSemiringWithoutAnnihilatingZero = record
      { +-isCommutativeMonoid = record
        { isMonoid = record
          { isSemigroup = record
            { isEquivalence = isEquivalence
            ; assoc         = ∨-assoc
            ; ∙-pres-≈      = cong₂ _∨_
            }
          ; identity = ∨-identity
          }
        ; comm = ∨-comm
        }
      ; *-isMonoid = record
        { isSemigroup = record
          { isEquivalence = isEquivalence
          ; assoc         = ∧-assoc
          ; ∙-pres-≈      = cong₂ _∧_
          }
        ; identity = ∧-identity
        }
      ; distrib = distrib-∧-∨
      }
    ; zero = zero-∧
    }
  ; *-comm = ∧-comm
  }

commutativeSemiring-∨-∧ : CommutativeSemiring
commutativeSemiring-∨-∧ = record
  { _+_                   = _∨_
  ; _*_                   = _∧_
  ; 0#                    = false
  ; 1#                    = true
  ; isCommutativeSemiring = isCommutativeSemiring-∨-∧
  }

module RingSolver =
  Solver (ACR.fromCommutativeSemiring commutativeSemiring-∨-∧)

------------------------------------------------------------------------
-- (Bool, ∧, ∨, true, false) forms a commutative semiring

private

  zero-∨ : Zero true _∨_
  zero-∨ = (λ _ → refl) , (λ x → ∨-comm x true)

  distrib-∨-∧ : _∨_ DistributesOver _∧_
  distrib-∨-∧ = distˡ , distʳ
    where
    distˡ : _∨_ DistributesOverˡ _∧_
    distˡ true  y z = refl
    distˡ false y z = refl

    distʳ : _∨_ DistributesOverʳ _∧_
    distʳ x y z =
                          begin
       (y ∧ z) ∨ x
                          ≈⟨ ∨-comm (y ∧ z) x ⟩
       x ∨ (y ∧ z)
                          ≈⟨ distˡ x y z ⟩
       (x ∨ y) ∧ (x ∨ z)
                          ≈⟨ cong₂ _∧_ (∨-comm x y) (∨-comm x z) ⟩
       (y ∨ x) ∧ (z ∨ x)
                          ∎

isCommutativeSemiring-∧-∨
  : IsCommutativeSemiring _≡_ _∧_ _∨_ true false
isCommutativeSemiring-∧-∨ = record
  { isSemiring = record
    { isSemiringWithoutAnnihilatingZero = record
      { +-isCommutativeMonoid = record
        { isMonoid = record
          { isSemigroup = record
            { isEquivalence = isEquivalence
            ; assoc         = ∧-assoc
            ; ∙-pres-≈      = cong₂ _∧_
            }
          ; identity = ∧-identity
          }
        ; comm = ∧-comm
        }
      ; *-isMonoid = record
        { isSemigroup = record
          { isEquivalence = isEquivalence
          ; assoc         = ∨-assoc
          ; ∙-pres-≈      = cong₂ _∨_
          }
        ; identity = ∨-identity
        }
      ; distrib = distrib-∨-∧
      }
    ; zero = zero-∨
    }
  ; *-comm = ∨-comm
  }

commutativeSemiring-∧-∨ : CommutativeSemiring
commutativeSemiring-∧-∨ = record
  { _+_                   = _∧_
  ; _*_                   = _∨_
  ; 0#                    = true
  ; 1#                    = false
  ; isCommutativeSemiring = isCommutativeSemiring-∧-∨
  }

------------------------------------------------------------------------
-- (Bool, ∨, ∧, not, true, false) is a boolean algebra

private

  absorptive : Absorptive _∨_ _∧_
  absorptive = abs-∨-∧ , abs-∧-∨
    where
    abs-∨-∧ : _∨_ Absorbs _∧_
    abs-∨-∧ true  y = refl
    abs-∨-∧ false y = refl

    abs-∧-∨ : _∧_ Absorbs _∨_
    abs-∧-∨ true  y = refl
    abs-∧-∨ false y = refl

  not-∧-inverse : Inverse false not _∧_
  not-∧-inverse =
    ¬x∧x≡⊥ , (λ x → ∧-comm x (not x) ⟨ trans ⟩ ¬x∧x≡⊥ x)
    where
    ¬x∧x≡⊥ : LeftInverse false not _∧_
    ¬x∧x≡⊥ false = refl
    ¬x∧x≡⊥ true  = refl

  not-∨-inverse : Inverse true not _∨_
  not-∨-inverse =
    ¬x∨x≡⊤ , (λ x → ∨-comm x (not x) ⟨ trans ⟩ ¬x∨x≡⊤ x)
    where
    ¬x∨x≡⊤ : LeftInverse true not _∨_
    ¬x∨x≡⊤ false = refl
    ¬x∨x≡⊤ true  = refl

isBooleanAlgebra : IsBooleanAlgebra _≡_ _∨_ _∧_ not true false
isBooleanAlgebra = record
  { isDistributiveLattice = record
      { isLattice = record
          { isEquivalence = isEquivalence
          ; ∨-comm        = ∨-comm
          ; ∨-assoc       = ∨-assoc
          ; ∨-pres-≈      = cong₂ _∨_
          ; ∧-comm        = ∧-comm
          ; ∧-assoc       = ∧-assoc
          ; ∧-pres-≈      = cong₂ _∧_
          ; absorptive    = absorptive
          }
      ; ∨-∧-distribʳ = proj₂ distrib-∨-∧
      }
  ; ∨-complementʳ = proj₂ not-∨-inverse
  ; ∧-complementʳ = proj₂ not-∧-inverse
  ; ¬-pres-≈      = cong not
  }

booleanAlgebra : BooleanAlgebra
booleanAlgebra = record
  { _∨_              = _∨_
  ; _∧_              = _∧_
  ; ¬_               = not
  ; ⊤                = true
  ; ⊥                = false
  ; isBooleanAlgebra = isBooleanAlgebra
  }

------------------------------------------------------------------------
-- (Bool, xor, ∧, id, false, true) forms a commutative ring

private

  xor-is-ok : ∀ x y → x xor y ≡ (x ∨ y) ∧ not (x ∧ y)
  xor-is-ok true  y = refl
  xor-is-ok false y = sym $ proj₂ ∧-identity _

commutativeRing-xor-∧ : CommutativeRing
commutativeRing-xor-∧ = commutativeRing
  where
  import Algebra.Props.BooleanAlgebra as BA
  open BA booleanAlgebra
  open XorRing _xor_ xor-is-ok

module XorRingSolver =
  Solver (ACR.fromCommutativeRing commutativeRing-xor-∧)

------------------------------------------------------------------------
-- Miscellaneous other properties

not-involutive : Involutive not
not-involutive true  = refl
not-involutive false = refl

not-¬ : ∀ {x y} → x ≡ y → x ≢ not y
not-¬ {true}  refl ()
not-¬ {false} refl ()

¬-not : ∀ {x y} → x ≢ y → x ≡ not y
¬-not {true}  {true}  x≢y = ⊥-elim (x≢y refl)
¬-not {true}  {false} _   = refl
¬-not {false} {true}  _   = refl
¬-not {false} {false} x≢y = ⊥-elim (x≢y refl)

⇔→≡ : {b₁ b₂ b : Bool} → b₁ ≡ b ⇔ b₂ ≡ b → b₁ ≡ b₂
⇔→≡ {true } {true }         hyp = refl
⇔→≡ {true } {false} {true } hyp = sym (proj₁ hyp refl)
⇔→≡ {true } {false} {false} hyp = proj₂ hyp refl
⇔→≡ {false} {true } {true } hyp = proj₂ hyp refl
⇔→≡ {false} {true } {false} hyp = sym (proj₁ hyp refl)
⇔→≡ {false} {false}         hyp = refl

T-≡ : ∀ {b} → T b ⇔ b ≡ true
T-≡ {false} = ((λ ())     , λ ())
T-≡ {true}  = (const refl , const _)

T-∧ : ∀ {b₁ b₂} → T (b₁ ∧ b₂) ⇔ (T b₁ × T b₂)
T-∧ {true}  {true}  = (const (_ , _) , const _)
T-∧ {true}  {false} = ((λ ()) , proj₂)
T-∧ {false} {_}     = ((λ ()) , proj₁)

T-∨ : ∀ {b₁ b₂} → T (b₁ ∨ b₂) ⇔ (T b₁ ⊎ T b₂)
T-∨ {true}  {b₂}    = (inj₁ , const _)
T-∨ {false} {true}  = (inj₂ , const _)
T-∨ {false} {false} = (inj₁ , [ id , id ])

proof-irrelevance : ∀ {b} (p q : T b) → p ≡ q
proof-irrelevance {true}  _  _  = refl
proof-irrelevance {false} () ()