text:
{-# OPTIONS --cubical --no-import-sorts #-}

module Number.Prelude.QuoInt where

open import Cubical.HITs.Ints.QuoInt public using
  ( ℤ
  ; HasFromNat
  ; HasFromNeg
  ; Int≡ℤ
  ; signed
  ; posneg
  ; ℤ→Int
  ; sucℤ
  ; predℤ
  ; pos
  ; neg
  ; sucℤ-+ʳ
  ; Sign
  ; spos
  ; sneg
  ) renaming
  ( isSetℤ         to is-setᶻ
  ; _+_            to _+ᶻ_
  ; _*_            to _·ᶻ_
  ; -_             to infixl 6 -ᶻ_
  ; *-comm         to ·ᶻ-comm
  ; *-assoc        to ·ᶻ-assoc
  ; +-comm         to +ᶻ-comm
  ; +-assoc        to +ᶻ-assoc
  ; sign           to signᶻ
  ; abs            to absᶻ
  ; _*S_           to _·ˢ_
  )

open import Number.Instances.QuoInt public using
  ( ℤlattice
  ; ⊕-identityʳ
  ) renaming
  ( is-LinearlyOrderedCommRing to is-LinearlyOrderedCommRingᶻ
  ; min                    to minᶻ
  ; max                    to maxᶻ
  ; _<_                    to _<ᶻ_
  ; ·-reflects-<           to ·ᶻ-reflects-<ᶻ
  ; ·-reflects-<ˡ          to ·ᶻ-reflects-<ᶻˡ
  ; 0<1                    to 0<1
  ; +-reflects-<           to +ᶻ-reflects-<ᶻ
  ; +-preserves-<          to +ᶻ-preserves-<ᶻ
  ; +-creates-<            to +ᶻ-creates-<ᶻ
  ; suc-creates-<          to suc-creates-<ᶻ
  ; +-creates-≤            to +ᶻ-creates-≤ᶻ
  ; ·-creates-<            to ·ᶻ-creates-<ᶻ
  ; ·-creates-≤            to ·ᶻ-creates-≤ᶻ
  ; ·-creates-≤-≡          to ·ᶻ-creates-≤ᶻ-≡
  ; ·-creates-<ˡ-≡         to ·ᶻ-creates-<ᶻˡ-≡
  ; ·-creates-<-flippedˡ-≡ to ·ᶻ-creates-<ᶻ-flippedˡ-≡
  ; ·-creates-<-flippedʳ-≡ to ·ᶻ-creates-<ᶻ-flippedʳ-≡
  ; ≤-dicho                to ≤ᶻ-dicho
  ; ≤-min-+                to ≤ᶻ-minᶻ-+ᶻ
  ; ≤-max-+                to ≤ᶻ-maxᶻ-+ᶻ
  ; ≤-min-·                to ≤ᶻ-minᶻ-·ᶻ
  ; ≤-max-·                to ≤ᶻ-maxᶻ-·ᶻ
  ; +-min-distribʳ         to +ᶻ-minᶻ-distribʳ
  ; ·-min-distribʳ         to ·ᶻ-minᶻ-distribʳ
  ; +-max-distribʳ         to +ᶻ-maxᶻ-distribʳ
  ; ·-max-distribʳ         to ·ᶻ-maxᶻ-distribʳ
  ; +-min-distribˡ         to +ᶻ-minᶻ-distribˡ
  ; ·-min-distribˡ         to ·ᶻ-minᶻ-distribˡ
  ; +-max-distribˡ         to +ᶻ-maxᶻ-distribˡ
  ; ·-max-distribˡ         to ·ᶻ-maxᶻ-distribˡ
  ; pos<pos[suc]           to pos<ᶻpos[suc]
  ; 0<ᶻpos[suc]            to 0<ᶻpos[suc]
  ; ·-nullifiesˡ           to ·ᶻ-nullifiesˡ
  ; ·-nullifiesʳ           to ·ᶻ-nullifiesʳ
  ; ·-preserves-0<         to ·ᶻ-preserves-0<ᶻ
  ; ·-reflects-0<          to ·ᶻ-reflects-0<ᶻ
  ; ·-creates-<-≡          to ·ᶻ-creates-<ᶻ-≡
  ; -flips-<0              to -flips-<ᶻ0
  ; -flips-<               to -ᶻ-flips-<ᶻ
  ; -identity-·            to -ᶻ-identity-·ᶻ
  ; -distˡ                 to -ᶻ-distˡ
  ; ·-reflects-<-flippedˡ  to ·ᶻ-reflects-<ᶻ-flippedˡ
  ; ·-reflects-<-flippedʳ  to ·ᶻ-reflects-<ᶻ-flippedʳ
  ; #-dicho                to #ᶻ-dicho
  ; ·-preserves-signˡ      to ·ᶻ-preserves-signᶻˡ
  ; #⇒≢                    to #ᶻ⇒≢
  ; <-split-pos            to <ᶻ-split-pos
  ; <-split-neg            to <ᶻ-split-neg
  ; <0-sign                to <ᶻ0-signᶻ
  ; 0<-sign                to 0<ᶻ-signᶻ
  ; sign-pos               to signᶻ-pos
  ; ·-reflects-≡ˡ          to ·ᶻ-reflects-≡ˡ
  ; ·-reflects-≡ʳ          to ·ᶻ-reflects-≡ʳ
  )

open import Number.Structures2
open IsLinearlyOrderedCommRing is-LinearlyOrderedCommRingᶻ public using () renaming
  ( _-_           to _-ᶻ_
  -- ; is-LinearlyOrderedCommSemiring to is-LinearlyOrderedCommSemiringᶻ
  ; _≤_           to _≤ᶻ_      -- NOTE: somehow this get an ugly prefix turning `0 ≤ᶻ aᶻ` into `(is-LinearlyOrderedCommSemiringᶻ IsLinearlyOrderedCommSemiring.≤ pos 0) aⁿᶻ`
  ; _#_           to _#ᶻ_      --       but some-other-how _#ᶻ_ works fine ... ?
  ; <-irrefl      to <ᶻ-irrefl --       turns out that this was due to `p = [ 0 ≤ᶻ aⁿᶻ ] ∋ is-0≤ⁿᶻ` instead of `p : [ 0 ≤ᶻ aⁿᶻ ]; p = is-0≤ⁿᶻ`
  ; <-trans       to <ᶻ-trans
  ; +-<-ext       to +ᶻ-<ᶻ-ext
  ; +-rinv        to +ᶻ-rinv
  ; +-identity    to +ᶻ-identity
  ; ·-preserves-< to ·ᶻ-preserves-<ᶻ
  ; <-tricho      to <ᶻ-tricho
  ; <-asym        to <ᶻ-asym
  ; ·-identity    to ·ᶻ-identity
  ; is-min        to is-minᶻ
  ; is-max        to is-maxᶻ
  ; is-dist       to is-distᶻ
  )

-- open IsLinearlyOrderedCommSemiring is-LinearlyOrderedCommSemiringᶻ public using () renaming
--   ( _≤_           to _≤ᶻ_ )

open import MorePropAlgebra.Properties.Lattice ℤlattice
open OnSet is-setᶻ public using () renaming
  ( min-≤              to minᶻ-≤ᶻ
  ; max-≤              to maxᶻ-≤ᶻ
  ; ≤-reflectsʳ-≡      to ≤ᶻ-reflectsʳ-≡
  ; ≤-reflectsˡ-≡      to ≤ᶻ-reflectsˡ-≡
  ; min-identity       to minᶻ-identity
  ; min-identity-≤     to minᶻ-identity-≤ᶻ
  ; max-identity-≤     to maxᶻ-identity-≤ᶻ
  ; min-comm           to minᶻ-comm
  ; min-assoc          to minᶻ-assoc
  ; max-identity       to maxᶻ-identity
  ; max-comm           to maxᶻ-comm
  ; max-assoc          to maxᶻ-assoc
  ; min-max-absorptive to minᶻ-maxᶻ-absorptive
  ; max-min-absorptive to maxᶻ-minᶻ-absorptive
  )

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
-- Andreas, 2015-07-18
-- Postpone checking of record expressions when type is blocked.
-- Guess type of record expressions when type is blocked.

open import Common.Product
open import Common.Prelude
open import Common.Equality

T : Bool → Set
T true  = Bool × Nat
T false = ⊥

works : (P : ∀{b} → b ≡ true → T b → Set) → Set
works P = P refl record{ proj₁ = true; proj₂ = 0 }

-- Guess or postpone.
test : (P : ∀{b} → T b → b ≡ true → Set) → Set
test P = P record{ proj₁ = true; proj₂ = 0 } refl

guess : (P : ∀{b} → T b → Set) → Set
guess P = P record{ proj₁ = true; proj₂ = 0 }

record R : Set where
  field
    f : Bool

record S : Set where
  field
    f : Bool

U : Bool → Set
U true = R
U false = S

postpone : (P : ∀{b} → U b → b ≡ true → Set) → Set
postpone P = P record{ f = false } refl

-- ambiguous : (P : ∀{b} → U b → Set) → Set
-- ambiguous P = P record{ f = false }

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Some tests for the Agda Abstract Machine.

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

_×_ : Set → Set → Set
A × B = Σ A λ _ → B

id : Nat → Nat
id x = x

-- Applying id should not break sharing
double : Nat → Nat
double n = id n + id n

pow : Nat → Nat
pow zero    = 1
pow (suc n) = double (pow n)

test-pow : pow 64 ≡ 18446744073709551616
test-pow = refl

-- Projections should not break sharing
addPair : Nat × Nat → Nat
addPair p = fst p + snd p

dup : Nat → Nat × Nat
dup x .fst = x
dup x .snd = x

smush : Nat × Nat → Nat × Nat
smush p = dup (addPair p)

iter : {A : Set} → (A → A) → Nat → A → A
iter f zero    x = x
iter f (suc n) x = f (iter f n x)

pow' : Nat → Nat
pow' n = addPair (iter smush n (0 , 1))

test-pow' : pow' 64 ≡ pow 64
test-pow' = refl

-- Should not be linear (not quadratic) for neutral n.
builtin : Nat → Nat → Nat
builtin k n = k + n - k

test-builtin : ∀ n → builtin 50000 n ≡ n
test-builtin n = refl


text:
module Oscar.Instance where

open import Oscar.Class.Associativity
open import Oscar.Class.Congruity
open import Oscar.Class.Equivalence
open import Oscar.Class.Extensionality
open import Oscar.Class.Injectivity
open import Oscar.Class.Preservativity
open import Oscar.Class.Reflexivity
open import Oscar.Class.Semifunctor
open import Oscar.Class.Semigroup
open import Oscar.Class.Symmetry
open import Oscar.Class.Transitivity
open import Oscar.Data.Equality
open import Oscar.Data.Fin
open import Oscar.Data.Nat
open import Oscar.Function
open import Oscar.Relation

open import Oscar.Data.Equality.properties
  using (≡̇-sym; ≡̇-trans)
  renaming (sym to ≡-sym
           ;trans to ≡-trans)

instance InjectivityFinSuc : ∀ {n} → Injectivity _≡_ _≡_ (Fin.suc {n}) suc
Injectivity.injectivity InjectivityFinSuc refl = refl

data D : Set where
  d1 : Nat → D
  d2 : Nat → Nat → D

pattern d2l r l = d2 l r

instance InjectivityDd1 : Injectivity _≡_ _≡_ d1 d1
Injectivity.injectivity InjectivityDd1 refl = refl

instance InjectivityD2l : ∀ {r1 r2} → Injectivity _≡_ _≡_ (d2l r1) (flip d2 r2)
Injectivity.injectivity InjectivityD2l refl = refl

instance InjectivityoidD2l : ∀ {r1} {r2} → Injectivityoid _ _ _ _ _
Injectivityoid.A InjectivityoidD2l = D
Injectivityoid.B InjectivityoidD2l = D
Injectivityoid._≋₁_ InjectivityoidD2l = _≡_
Injectivityoid.I InjectivityoidD2l = Nat
Injectivityoid._≋₂_ InjectivityoidD2l = _≡_
Injectivityoid.μₗ (InjectivityoidD2l {r1} {r2}) = d2l r1
Injectivityoid.μᵣ (InjectivityoidD2l {r1} {r2}) = flip d2 r2
Injectivityoid.`injectivity InjectivityoidD2l refl = refl

instance InjectivityoidD2r : ∀ {r1} {r2} → Injectivityoid _ _ _ _ _
Injectivityoid.A InjectivityoidD2r = D
Injectivityoid.B InjectivityoidD2r = D
Injectivityoid._≋₁_ InjectivityoidD2r = _≡_
Injectivityoid.I InjectivityoidD2r = Nat
Injectivityoid._≋₂_ InjectivityoidD2r = _≡_
Injectivityoid.μₗ (InjectivityoidD2r {r1} {r2}) = d2 r1
Injectivityoid.μᵣ (InjectivityoidD2r {r1} {r2}) = d2 r2
Injectivityoid.`injectivity InjectivityoidD2r refl = refl

open Injectivityoid ⦃ … ⦄ using (`injectivity)

instance InjectivityD2r : ∀ {l1 l2} → Injectivity _≡_ _≡_ (d2 l1) (d2 l2)
Injectivity.injectivity InjectivityD2r refl = refl

pattern d2' {l} r = d2 l r

injectivity-test : (k l m n : Nat) → (d2 k m ≡ d2 l n) → (d1 k ≡ d1 l)  → Set
injectivity-test k l m n eq1 eq2 with injectivity {_≋₁_ = _≡_} {_≋₂_ = _≡_} {f = d2'} eq1
injectivity-test k l m n eq1 eq2 | ref with injectivity {_≋₁_ = _≡_} {_≋₂_ = _≡_} {f = d1} eq2
… | ref2 = {!!}
-- with `injectivity ⦃ ? ⦄ eq2
-- … | ref3 = {!ref!}

instance

  ≡-Reflexivity : ∀
    {a} {A : Set a}
    → Reflexivity (_≡_ {A = A})
  Reflexivity.reflexivity ≡-Reflexivity = refl

  ≡̇-Reflexivity : ∀
    {a} {A : Set a} {b} {B : A → Set b}
    → Reflexivity (_≡̇_ {B = B})
  Reflexivity.reflexivity ≡̇-Reflexivity _ = refl

  ≡-flip≡-Extensionality : ∀
    {a} {A : Set a}
    → Extensionality {B = const A} _≡_ (λ ⋆ → flip _≡_ ⋆) id id
  Extensionality.extensionality ≡-flip≡-Extensionality = ≡-sym

  ≡̇-flip≡̇-Extensionality : ∀
    {a} {A : Set a} {b} {B : A → Set b}
    → Extensionality {B = const ((x : A) → B x)} _≡̇_ (λ ⋆ → flip _≡̇_ ⋆) id id
  Extensionality.extensionality ≡̇-flip≡̇-Extensionality = ≡̇-sym

  ≡-Transitivity : ∀ {a} {A : Set a} → Transitivity {A = A} _≡_
  Transitivity.transitivity ≡-Transitivity = λ ⋆ → ≡-trans ⋆

  ≡̇-Transitivity : ∀ {a} {A : Set a} {b} {B : A → Set b} → Transitivity {A = (x : A) → B x} _≡̇_
  Transitivity.transitivity ≡̇-Transitivity = ≡̇-trans

  ≡-Congruity : ∀
    {a} {A : Set a} {b} {B : Set b} {ℓ₂} {_≋₂_ : B → B → Set ℓ₂}
    ⦃ _ : Reflexivity _≋₂_ ⦄
    → Congruity (_≡_ {A = A}) _≋₂_
  Congruity.congruity ≡-Congruity μ refl = reflexivity

module Term {𝔣} (FunctionName : Set 𝔣) where

  open import Oscar.Data.Term FunctionName
  open import Oscar.Data.Term.internal.SubstituteAndSubstitution FunctionName as ⋆

  instance

    ◇-≡̇-Associativity : Associativity _◇_ _≡̇_
    Associativity.associativity ◇-≡̇-Associativity = ◇-associativity

    ∘-≡̇-Associativity : ∀ {a} {A : Set a} {b} {B : A → Set b} → Associativity {_►_ = _⟨ B ⟩→_} (λ ⋆ → _∘_ ⋆) _≡̇_
    Associativity.associativity ∘-≡̇-Associativity _ _ _ _ = refl

    ◇-∘-≡̇-◃-◃-◃-Preservativity : ∀ {l m n} → Preservativity (λ ⋆ → _◇_ (m ⊸ n ∋ ⋆)) (_∘′_ {A = Term l}) _≡̇_ _◃_ _◃_ _◃_
    Preservativity.preservativity ◇-∘-≡̇-◃-◃-◃-Preservativity g f τ = symmetry (◃-associativity τ f g)

    ≡̇-≡̇-◃-◃-Extensionality : ∀ {m n} → Extensionality _≡̇_ (λ ⋆ → _≡̇_ ⋆) (_◃_ {m} {n}) (λ ⋆ → _◃_ ⋆)
    Extensionality.extensionality ≡̇-≡̇-◃-◃-Extensionality = ◃-extensionality

  semifunctor-◃ : Semifunctor _◇_ _≡̇_ (λ ⋆ → _∘_ ⋆) _≡̇_ id _◃_
  semifunctor-◃ = it

  open import Oscar.Data.AList FunctionName

  postulate
    _++_ : ∀ {m n} → AList m n → ∀ {l} → AList l m → AList l n
    sub : ∀ {m n} → AList m n → m ⊸ n
    ++-assoc : ∀ {l m n o} (ρ : AList l m) (σ : AList n _) (τ : AList o _) → ρ ++ (σ ++ τ) ≡ (ρ ++ σ) ++ τ
    subfact1 : ∀ {l m n} (ρ : AList m n) (σ : AList l m) → sub (ρ ++ σ) ≡̇ (sub ρ ◇ sub σ)

  instance

    ++-≡-Associativity : Associativity _++_ _≡_
    Associativity.associativity ++-≡-Associativity f g h = ++-assoc h g f

    ++-◇-sub-sub-sub : ∀ {l m n} → Preservativity (λ ⋆ → _++_ (AList m n ∋ ⋆)) (λ ⋆ → _◇_ ⋆ {l = l}) _≡̇_ sub sub sub
    Preservativity.preservativity ++-◇-sub-sub-sub = subfact1

  semifunctor-sub : Semifunctor _++_ _≡_ _◇_ _≡̇_ id sub
  semifunctor-sub = it

--   ≡̇-extension : ∀
--       {a} {A : Set a} {b} {B : A → Set b}
--       {ℓ₁} {_≤₁_ : (x : A) → B x → Set ℓ₁}
--       {c} {C : Set c}
--       {d} {D : C → Set d}
--       {μ₁ : A → (z : C) → D z}
--       {μ₂ : ∀ {x} → B x → (z : C) → D z}
--     ⦃ _ : Extensionality _≤₁_ (λ ⋆ → _≡̇_ ⋆) μ₁ μ₂ ⦄
--       {x} {y : B x}
--     → x ≤₁ y → μ₁ x ≡̇ μ₂ y
--   ≡̇-extension = extension (λ ⋆ → _≡̇_ ⋆)

--   test-◃-extensionality : ∀ {m n} {f g : m ⊸ n} → f ≡̇ g → f ◃_ ≡̇ g ◃_
--   test-◃-extensionality = ≡̇-extension -- ≡̇-extension -- ⦃ ? ⦄ -- extension (λ ⋆ → _≡̇_ ⋆)

--   postulate
--     R : Set
--     S : Set
--     _◀_ : ∀ {m n} → m ⊸ n → R → S
--     _◀'_ : ∀ {m n} → m ⊸ n → R → S
--     _◆_ : ∀ {m n} → m ⊸ n → ∀ {l} → l ⊸ m → l ⊸ n

--     instance ≡̇-≡̇-◀-◀'-Extensionality : ∀ {m n} → Extensionality _≡̇_ (λ ⋆ → _≡̇_ ⋆) ((m ⊸ n → _) ∋ _◀_) _◀'_
--     instance ≡̇-≡̇-◀-◀-Extensionality : ∀ {m n} → Extensionality _≡̇_ (λ ⋆ → _≡̇_ ⋆) ((m ⊸ n → _) ∋ _◀_) _◀_
--     instance ◆-◇-≡̇-Associativity : ∀ {k} → Associativity _◆_ (λ ⋆ → _◇_ ⋆) ((k ⊸ _ → _) ∋ _≡̇_)
--     instance ◆-◇-≡̇-Associativity' : ∀ {k} → Associativity _◇_ (λ ⋆ → _◆_ ⋆) ((k ⊸ _ → _) ∋ _≡̇_)

--   test-◀-extensionality : ∀ {m n} {f g : m ⊸ n} → f ≡̇ g → f ◀_ ≡̇ g ◀_
--   test-◀-extensionality {m} {n} = ≡̇-extension
--   -- extensionality {_≤₁_ = _≡̇_} {μ₁ = ((m ⊸ n → _) ∋ _◀_)} {μ₂ = _◀_}

--   test-◀'-extensionality : ∀ {m n} {f g : m ⊸ n} → f ≡̇ g → f ◀_ ≡̇ g ◀'_
--   test-◀'-extensionality = ≡̇-extension

--   test-◃-associativity : ∀ {l} (t : Term l) {m} (f : l ⊸ m) {n} (g : m ⊸ n) → g ◃ (f ◃ t) ≡ (g ◇ f) ◃ t
--   test-◃-associativity = association _◇_ _≡_

--   test-◇-associativity : ∀ {k l} (f : k ⊸ l) {m} (g : l ⊸ m) {n} (h : m ⊸ n) → h ◇ (g ◇ f) ≡̇ (h ◇ g) ◇ f
--   test-◇-associativity = association _◇_ _≡̇_

--   test-◆-associativity : ∀ {k l} (f : k ⊸ l) {m} (g : l ⊸ m) {n} (h : m ⊸ n) → h ◇ (g ◇ f) ≡̇ (h ◆ g) ◇ f
--   test-◆-associativity = association _◆_ _≡̇_

--   test-◆-associativity' : ∀ {k l} (f : k ⊸ l) {m} (g : l ⊸ m) {n} (h : m ⊸ n) → h ◆ (g ◆ f) ≡̇ (h ◇ g) ◆ f
--   test-◆-associativity' = association _◇_ _≡̇_


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

open import Cubical.Core.Everything
open import Cubical.Relation.Binary.Raw

module Cubical.Relation.Binary.Raw.Construct.StrictToNonStrict
  {a ℓ} {A : Type a}
  (_<_ : RawRel A ℓ)
  where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Data.Prod
open import Cubical.Data.Sum.Base renaming (rec to ⊎-rec)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) using ()
open import Cubical.Relation.Binary.Raw.Properties
open import Cubical.Relation.Nullary

------------------------------------------------------------------------
-- Conversion

-- _<_ can be turned into _≤_ as follows:

_≤_ : RawRel A _
x ≤ y = (x < y) ⊎ (x ≡ y)

------------------------------------------------------------------------
-- The converted relations have certain properties
-- (if the original relations have certain other properties)

≤-isPropValued : isSet A → isPropValued _<_ → Irreflexive _<_ → isPropValued _≤_
≤-isPropValued isSetA propv irrefl x y (inl p) (inl q) = cong inl (propv x y p q)
≤-isPropValued isSetA propv irrefl x y (inl p) (inr q) = ⊥-elim (irrefl→tonoteq _<_ irrefl p q)
≤-isPropValued isSetA propv irrefl x y (inr p) (inl q) = ⊥-elim (irrefl→tonoteq _<_ irrefl q p)
≤-isPropValued isSetA propv irrefl x y (inr p) (inr q) = cong inr (isSetA x y p q)

<⇒≤ : _<_ ⇒ _≤_
<⇒≤ = inl

≤-fromEq : FromEq _≤_
≤-fromEq = inr

≤-reflexive : Reflexive _≤_
≤-reflexive = fromeq→reflx _≤_ ≤-fromEq

≤-antisym : Transitive _<_ → Irreflexive _<_ → Antisymmetric _≤_
≤-antisym transitive irrefl (inl x<y) (inl y<x) = ⊥-elim (trans∧irr→asym _<_ transitive irrefl x<y y<x)
≤-antisym _ _ _ (inr y≡x) = sym y≡x
≤-antisym _ _ (inr x≡y) _ = x≡y

≤-transitive : Transitive _<_ → Transitive _≤_
≤-transitive <-trans (inl x<y) (inl y<z) = inl $ <-trans x<y y<z
≤-transitive _       (inl x<y) (inr y≡z) = inl $ Respectsʳ≡ _<_ y≡z x<y
≤-transitive _       (inr x≡y) (inl y<z) = inl $ Respectsˡ≡ _<_ (sym x≡y) y<z
≤-transitive _       (inr x≡y) (inr y≡z) = inr $ x≡y ∙ y≡z

<-≤-trans : Transitive _<_ → Trans _<_ _≤_ _<_
<-≤-trans transitive x<y (inl y<z) = transitive x<y y<z
<-≤-trans transitive x<y (inr y≡z) = Respectsʳ≡ _<_ y≡z x<y

≤-<-trans : Transitive _<_ → Trans _≤_ _<_ _<_
≤-<-trans transitive (inl x<y) y<z = transitive x<y y<z
≤-<-trans transitive (inr x≡y) y<z = Respectsˡ≡ _<_ (sym x≡y) y<z

≤-total : Trichotomous _<_ → Total _≤_
≤-total <-tri x y with <-tri x y
... | tri< x<y x≢y x≯y = inl (inl x<y)
... | tri≡ x≮y x≡y x≯y = inl (inr x≡y)
... | tri> x≮y x≢y x>y = inr (inl x>y)

≤-decidable : Discrete A → Decidable _<_ → Decidable _≤_
≤-decidable _≟_ _<?_ x y with x ≟ y
... | yes p = yes (inr p)
... | no ¬p with x <? y
...     | yes q = yes (inl q)
...     | no ¬q = no (⊎-rec ¬q ¬p)

≤-decidable′ : Trichotomous _<_ → Decidable _≤_
≤-decidable′ compare x y with compare x y
... | tri< x<y _   _ = yes (inl x<y)
... | tri≡ _   x≡y _ = yes (inr x≡y)
... | tri> x≮y x≢y _ = no (⊎-rec x≮y x≢y)

------------------------------------------------------------------------
-- Converting structures

isPreorder : Transitive _<_ → IsPreorder _≤_
isPreorder transitive = record
  { reflexive  = ≤-reflexive
  ; transitive = ≤-transitive transitive
  }

isPartialOrder : IsStrictPartialOrder _<_ → IsPartialOrder _≤_
isPartialOrder spo = record
  { isPreorder = isPreorder S.transitive
  ; antisym    = ≤-antisym S.transitive S.irrefl
  }
  where module S = IsStrictPartialOrder spo

isTotalOrder : IsStrictTotalOrder _<_ → IsTotalOrder _≤_
isTotalOrder sto = record
  { isPartialOrder = isPartialOrder S.isStrictPartialOrder
  ; total          = λ x y → ∣ ≤-total S.compare x y ∣
  }
  where module S = IsStrictTotalOrder sto

isDecTotalOrder : IsStrictTotalOrder _<_ → IsDecTotalOrder _≤_
isDecTotalOrder sto = record
  { isTotalOrder = isTotalOrder sto
  ; _≤?_         = ≤-decidable′ S.compare
  }
  where module S = IsStrictTotalOrder sto


text:
------------------------------------------------------------------------
-- The "time complexity" of the compiled program matches the one
-- obtained from the instrumented interpreter
------------------------------------------------------------------------

open import Prelude hiding (_+_; _*_)

import Lambda.Syntax

module Lambda.Compiler-correctness.Steps-match
  {Name : Type}
  (open Lambda.Syntax Name)
  (def : Name → Tm 1)
  where

import Equality.Propositional as E
open import Logical-equivalence using (_⇔_)
import Tactic.By.Propositional as By
open import Prelude.Size

open import Conat E.equality-with-J as Conat
  using (Conat; zero; suc; force; ⌜_⌝; _+_; _*_; max;
         [_]_≤_; step-≤; step-∼≤; _∎≤)
open import Function-universe E.equality-with-J hiding (_∘_)
open import List E.equality-with-J using (_++_)
open import Monad E.equality-with-J using (return; _>>=_; _⟨$⟩_)
open import Vec.Data E.equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity
open import Delay-monad.Quantitative-weak-bisimilarity

open import Lambda.Compiler def
open import Lambda.Delay-crash
open import Lambda.Interpreter.Steps def
open import Lambda.Virtual-machine.Instructions Name hiding (crash)
open import Lambda.Virtual-machine comp-name

private
  module C = Closure Code
  module T = Closure Tm

------------------------------------------------------------------------
-- Some lemmas

-- A rearrangement lemma for ⟦_⟧.

⟦⟧-· :
  ∀ {n} (t₁ t₂ : Tm n) {ρ} {k : T.Value → Delay-crash C.Value ∞} →
  ⟦ t₁ · t₂ ⟧ ρ >>= k ∼
  ⟦ t₁ ⟧ ρ >>= λ v₁ → ⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ ∙ v₂ >>= k
⟦⟧-· t₁ t₂ {ρ} {k} =
  ⟦ t₁ · t₂ ⟧ ρ >>= k      ∼⟨⟩

  (do v₁ ← ⟦ t₁ ⟧ ρ
      v₂ ← ⟦ t₂ ⟧ ρ
      v₁ ∙ v₂) >>= k       ∼⟨ symmetric (associativity (⟦ t₁ ⟧ _) _ _) ⟩

  (do v₁ ← ⟦ t₁ ⟧ ρ
      (do v₂ ← ⟦ t₂ ⟧ ρ
          v₁ ∙ v₂) >>= k)  ∼⟨ (⟦ t₁ ⟧ _ ∎) >>=-cong (λ _ → symmetric (associativity (⟦ t₂ ⟧ _) _ _)) ⟩

  (do v₁ ← ⟦ t₁ ⟧ ρ
      v₂ ← ⟦ t₂ ⟧ ρ
      v₁ ∙ v₂ >>= k)       ∎

-- Lemmas related to conatural numbers.

private

  lemma₁ : ∀ {δ} → [ ∞ ] δ ≤ ⌜ 1 ⌝ + δ
  lemma₁ = Conat.≤suc

  lemma₂ : ∀ {δ} → [ ∞ ] δ ≤ max ⌜ 1 ⌝ δ
  lemma₂ = Conat.ʳ≤max ⌜ 1 ⌝ _

  lemma₃ : ∀ {δ} → [ ∞ ] max ⌜ 1 ⌝ δ ≤ max ⌜ 1 ⌝ δ + ⌜ 1 ⌝
  lemma₃ = Conat.m≤m+n

  lemma₄ : ∀ {δ} → [ ∞ ] δ ≤ max ⌜ 1 ⌝ δ + ⌜ 1 ⌝
  lemma₄ {δ} =
    δ                    ≤⟨ lemma₂ ⟩
    max ⌜ 1 ⌝ δ          ≤⟨ lemma₃ {δ = δ} ⟩
    max ⌜ 1 ⌝ δ + ⌜ 1 ⌝  ∎≤

  lemma₅ : ∀ {δ} → [ ∞ ] ⌜ 1 ⌝ + δ ≤ δ + ⌜ 1 ⌝
  lemma₅ {δ} =
    ⌜ 1 ⌝ + δ  ∼⟨ Conat.+-comm ⌜ 1 ⌝ ⟩≤
    δ + ⌜ 1 ⌝  ∎≤

  lemma₆ : ∀ {δ} → [ ∞ ] ⌜ 1 ⌝ + δ ≤ max ⌜ 1 ⌝ δ + ⌜ 1 ⌝
  lemma₆ {δ} =
    ⌜ 1 ⌝ + δ            ≤⟨ lemma₅ ⟩
    δ + ⌜ 1 ⌝            ≤⟨ lemma₂ Conat.+-mono (⌜ 1 ⌝ ∎≤) ⟩
    max ⌜ 1 ⌝ δ + ⌜ 1 ⌝  ∎≤

  lemma₇ : ∀ {δ} → [ ∞ ] max ⌜ 1 ⌝ (⌜ 1 ⌝ + δ) ≤ ⌜ 1 ⌝ + δ
  lemma₇ {δ} = suc λ { .force →
    δ  ∎≤ }

  lemma₈ : ∀ {δ} → [ ∞ ] max ⌜ 1 ⌝ (max ⌜ 1 ⌝ δ) ≤ max ⌜ 1 ⌝ δ
  lemma₈ {δ} = suc λ { .force →
    Conat.pred δ  ∎≤ }

  lemma₉ :
    ∀ {δ} → [ ∞ ] max ⌜ 1 ⌝ (max ⌜ 1 ⌝ (max ⌜ 1 ⌝ δ)) ≤ max ⌜ 1 ⌝ δ
  lemma₉ {δ} =
    max ⌜ 1 ⌝ (max ⌜ 1 ⌝ (max ⌜ 1 ⌝ δ)) ≤⟨ lemma₈ ⟩
    max ⌜ 1 ⌝ (max ⌜ 1 ⌝ δ)             ≤⟨ lemma₈ ⟩
    max ⌜ 1 ⌝ δ                         ∎≤

  lemma₁₀ : ∀ {δ} → [ ∞ ] ⌜ 1 ⌝ + ⌜ 0 ⌝ ≤ max ⌜ 1 ⌝ δ
  lemma₁₀ = suc λ { .force → zero }

  lemma₁₁ : Conat.[ ∞ ] max ⌜ 1 ⌝ ⌜ 1 ⌝ ∼ ⌜ 1 ⌝
  lemma₁₁ = suc λ { .force → zero }

  lemma₁₂ : Conat.[ ∞ ] ⌜ 1 ⌝ + ⌜ 1 ⌝ ∼ ⌜ 2 ⌝
  lemma₁₂ = Conat.symmetric-∼ (Conat.⌜⌝-+ 1)

------------------------------------------------------------------------
-- Well-formed continuations and stacks

-- A continuation is OK with respect to a certain state and conatural
-- number if the following property is satisfied.

Cont-OK :
  Size → State → (T.Value → Delay-crash C.Value ∞) → Conat ∞ → Type
Cont-OK i ⟨ c , s , ρ ⟩ k δ =
  ∀ v → [ i ∣ ⌜ 1 ⌝ ∣ δ ] exec ⟨ c , val (comp-val v) ∷ s , ρ ⟩ ≳ k v

-- If the In-tail-context parameter indicates that we are in a tail
-- context, then the stack must have a certain shape, and it must be
-- related to the continuation and the conatural number in a certain
-- way.

data Stack-OK
       (i : Size) (k : T.Value → Delay-crash C.Value ∞) (δ : Conat ∞) :
       In-tail-context → Stack → Type where
  unrestricted : ∀ {s} → Stack-OK i k δ false s
  restricted   : ∀ {s n} {c : Code n} {ρ : C.Env n} →
                 Cont-OK i ⟨ c , s , ρ ⟩ k δ →
                 Stack-OK i k δ true (ret c ρ ∷ s)

-- A lemma that can be used to show that certain stacks are OK.

ret-ok :
  ∀ {p i s n c} {ρ : C.Env n} {k δ} →
  Cont-OK i ⟨ c , s , ρ ⟩ k δ →
  Stack-OK i k (⌜ 1 ⌝ + δ) p (ret c ρ ∷ s)
ret-ok {true}  c-ok = restricted (weakenˡ lemma₁ ∘ c-ok)
ret-ok {false} _    = unrestricted

------------------------------------------------------------------------
-- The semantics of the compiled program matches that of the source
-- code

mutual

  -- Some lemmas making up the main part of the compiler correctness
  -- result.

  ⟦⟧-correct :
    ∀ {i n} (t : Tm n) (ρ : T.Env n) {c s}
      {k : T.Value → Delay-crash C.Value ∞} {tc δ} →
    Stack-OK i k δ tc s →
    Cont-OK i ⟨ c , s , comp-env ρ ⟩ k δ →
    [ i ∣ ⌜ 1 ⌝ ∣ max ⌜ 1 ⌝ δ ]
      exec ⟨ comp tc t c , s , comp-env ρ ⟩ ≳ ⟦ t ⟧ ρ >>= k

  ⟦⟧-correct (var x) ρ {c} {s} {k} _ c-ok =
    exec ⟨ var x ∷ c , s , comp-env ρ ⟩                              ≳⟨ later (λ { .force →
      exec ⟨ c , val By.⟨ index (comp-env ρ) x ⟩ ∷ s , comp-env ρ ⟩       ≡⟨ By.⟨by⟩ (comp-index ρ x) ⟩ˢ
      exec ⟨ c , val (comp-val (index ρ x)) ∷ s , comp-env ρ ⟩            ≳⟨ weakenˡ lemma₄ (c-ok (index ρ x)) ⟩ˢ
      k (index ρ x)                                                       ∎ }) ⟩ˢ
    ⟦ var x ⟧ ρ >>= k                                                ∎

  ⟦⟧-correct (lam t) ρ {c} {s} {k} _ c-ok =
    exec ⟨ clo (comp-body t) ∷ c , s , comp-env ρ ⟩             ≳⟨ later (λ { .force →
      exec ⟨ c , val (comp-val (T.lam t ρ)) ∷ s , comp-env ρ ⟩       ≳⟨ weakenˡ lemma₄ (c-ok (T.lam t ρ)) ⟩ˢ
      k (T.lam t ρ)                                                  ∎ }) ⟩ˢ
    ⟦ lam t ⟧ ρ >>= k                                           ∎

  ⟦⟧-correct (t₁ · t₂) ρ {c} {s} {k} _ c-ok =
    exec ⟨ comp false t₁ (comp false t₂ (app ∷ c))
         , s
         , comp-env ρ
         ⟩                                                   ≳⟨ weakenˡ lemma₉ (⟦⟧-correct t₁ _ unrestricted λ v₁ →

      exec ⟨ comp false t₂ (app ∷ c)
           , val (comp-val v₁) ∷ s
           , comp-env ρ
           ⟩                                                       ≳⟨ (⟦⟧-correct t₂ _ unrestricted λ v₂ →

        exec ⟨ app ∷ c
             , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s
             , comp-env ρ
             ⟩                                                           ≳⟨ ∙-correct v₁ v₂ c-ok ⟩ˢ

        v₁ ∙ v₂ >>= k                                                    ∎) ⟩ˢ

      (⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ ∙ v₂ >>= k)                          ∎) ⟩ˢ

    (⟦ t₁ ⟧ ρ >>= λ v₁ → ⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ ∙ v₂ >>= k)  ∼⟨ symmetric (⟦⟧-· t₁ t₂) ⟩

    ⟦ t₁ · t₂ ⟧ ρ >>= k                                      ∎

  ⟦⟧-correct (call f t) ρ {c} {s} {k} unrestricted c-ok =
    exec ⟨ comp false (call f t) c , s , comp-env ρ ⟩         ∼⟨⟩ˢ

    exec ⟨ comp false t (cal f ∷ c) , s , comp-env ρ ⟩        ≳⟨ (⟦⟧-correct t _ unrestricted λ v →

      exec ⟨ cal f ∷ c , val (comp-val v) ∷ s , comp-env ρ ⟩        ≳⟨ (later λ { .force → weakenˡ lemma₅ (

        exec ⟨ comp-name f
             , ret c (comp-env ρ) ∷ s
             , comp-val v ∷ []
             ⟩                                                            ≳⟨ body-lemma (def f) [] c-ok ⟩ˢ

        (⟦ def f ⟧ (v ∷ []) >>= k)                                        ∎) }) ⟩ˢ

      (T.lam (def f) [] ∙ v >>= k)                                  ∎) ⟩ˢ

    (⟦ t ⟧ ρ >>= λ v → T.lam (def f) [] ∙ v >>= k)            ∼⟨ associativity (⟦ t ⟧ ρ) _ _ ⟩

    (⟦ t ⟧ ρ >>= λ v → T.lam (def f) [] ∙ v) >>= k            ∼⟨⟩

    ⟦ call f t ⟧ ρ >>= k                                      ∎

  ⟦⟧-correct (call f t) ρ {c} {ret c′ ρ′ ∷ s} {k} (restricted c-ok) _ =
    exec ⟨ comp true (call f t) c , ret c′ ρ′ ∷ s , comp-env ρ ⟩    ∼⟨⟩ˢ

    exec ⟨ comp false t (tcl f ∷ c) , ret c′ ρ′ ∷ s , comp-env ρ ⟩  ≳⟨ (⟦⟧-correct t _ unrestricted λ v →

      exec ⟨ tcl f ∷ c
           , val (comp-val v) ∷ ret c′ ρ′ ∷ s
           , comp-env ρ
           ⟩                                                              ≳⟨ (later λ { .force → weakenˡ lemma₅ (

        exec ⟨ comp-name f
             , ret c′ ρ′ ∷ s
             , comp-val v ∷ []
             ⟩                                                                  ≳⟨ body-lemma (def f) [] c-ok ⟩ˢ

        ⟦ def f ⟧ (v ∷ []) >>= k                                                ∎) }) ⟩ˢ

      T.lam (def f) [] ∙ v >>= k                                          ∎) ⟩ˢ

    (⟦ t ⟧ ρ >>= λ v → T.lam (def f) [] ∙ v >>= k)                  ∼⟨ associativity (⟦ t ⟧ ρ) _ _ ⟩

    (⟦ t ⟧ ρ >>= λ v → T.lam (def f) [] ∙ v) >>= k                  ∼⟨⟩

    ⟦ call f t ⟧ ρ >>= k                                            ∎

  ⟦⟧-correct (con b) ρ {c} {s} {k} _ c-ok =
    exec ⟨ con b ∷ c , s , comp-env ρ ⟩                       ≳⟨ later (λ { .force →
      exec ⟨ c , val (comp-val (T.con b)) ∷ s , comp-env ρ ⟩       ≳⟨ weakenˡ lemma₄ (c-ok (T.con b)) ⟩ˢ
      k (T.con b)                                                  ∎ }) ⟩ˢ
    ⟦ con b ⟧ ρ >>= k                                         ∎

  ⟦⟧-correct (if t₁ t₂ t₃) ρ {c} {s} {k} {tc} s-ok c-ok =
    exec ⟨ comp false t₁ (bra (comp tc t₂ []) (comp tc t₃ []) ∷ c)
         , s
         , comp-env ρ
         ⟩                                                          ≳⟨ weakenˡ lemma₈
                                                                         (⟦⟧-correct t₁ _ unrestricted λ v₁ → ⟦if⟧-correct v₁ t₂ t₃ s-ok c-ok) ⟩ˢ

    (⟦ t₁ ⟧ ρ >>= λ v₁ → ⟦if⟧ v₁ t₂ t₃ ρ >>= k)                     ∼⟨ associativity (⟦ t₁ ⟧ ρ) _ _ ⟩

    (⟦ t₁ ⟧ ρ >>= λ v₁ → ⟦if⟧ v₁ t₂ t₃ ρ) >>= k                     ∼⟨⟩

    ⟦ if t₁ t₂ t₃ ⟧ ρ >>= k                                         ∎

  body-lemma :
    ∀ {i n n′} (t : Tm (suc n)) ρ {ρ′ : C.Env n′} {c s v}
      {k : T.Value → Delay-crash C.Value ∞} {δ} →
    Cont-OK i ⟨ c , s , ρ′ ⟩ k δ →
    [ i ∣ ⌜ 1 ⌝ ∣ ⌜ 1 ⌝ + δ ]
      exec ⟨ comp-body t , ret c ρ′ ∷ s , comp-val v ∷ comp-env ρ ⟩ ≳
      ⟦ t ⟧ (v ∷ ρ) >>= k
  body-lemma t ρ {ρ′} {c} {s} {v} {k} c-ok =
    exec ⟨ comp-body t , ret c ρ′ ∷ s , comp-val v ∷ comp-env ρ ⟩  ∼⟨⟩ˢ

    exec ⟨ comp-body t , ret c ρ′ ∷ s , comp-env (v ∷ ρ) ⟩         ≳⟨ weakenˡ lemma₇ (⟦⟧-correct t (_ ∷ _) (ret-ok c-ok) λ v′ →

      exec ⟨ ret ∷ []
           , val (comp-val v′) ∷ ret c ρ′ ∷ s
           , comp-env (v ∷ ρ)
           ⟩                                                            ≳⟨⟩ˢ

      exec ⟨ c , val (comp-val v′) ∷ s , ρ′ ⟩                           ≳⟨ c-ok v′ ⟩ˢ

      k v′                                                              ∎) ⟩ˢ

    ⟦ t ⟧ (v ∷ ρ) >>= k                                            ∎

  ∙-correct :
    ∀ {i n} v₁ v₂ {ρ : C.Env n} {c s}
      {k : T.Value → Delay-crash C.Value ∞} {δ} →
    Cont-OK i ⟨ c , s , ρ ⟩ k δ →
    [ i ∣ ⌜ 1 ⌝ ∣ max ⌜ 1 ⌝ δ ]
      exec ⟨ app ∷ c , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s , ρ ⟩ ≳
      v₁ ∙ v₂ >>= k

  ∙-correct (T.lam t₁ ρ₁) v₂ {ρ} {c} {s} {k} c-ok =
    exec ⟨ app ∷ c
         , val (comp-val v₂) ∷ val (comp-val (T.lam t₁ ρ₁)) ∷ s
         , ρ
         ⟩                                                             ≳⟨ later (λ { .force → weakenˡ lemma₆ (

      exec ⟨ comp-body t₁ , ret c ρ ∷ s , comp-val v₂ ∷ comp-env ρ₁ ⟩       ≳⟨ body-lemma t₁ _ c-ok ⟩ˢ

      ⟦ t₁ ⟧ (v₂ ∷ ρ₁) >>= k                                                ∎) }) ⟩ˢ

    T.lam t₁ ρ₁ ∙ v₂ >>= k                                             ∎

  ∙-correct (T.con b) v₂ {ρ} {c} {s} {k} _ = weakenˡ lemma₁₀ (
    exec ⟨ app ∷ c
         , val (comp-val v₂) ∷ val (comp-val (T.con b)) ∷ s
         , ρ
         ⟩                                                   ≳⟨⟩ˢ

    crash                                                    ∼⟨⟩ˢ

    T.con b ∙ v₂ >>= k                                       ∎ˢ)

  ⟦if⟧-correct :
    ∀ {i n} v₁ (t₂ t₃ : Tm n) {ρ : T.Env n} {c s}
      {k : T.Value → Delay-crash C.Value ∞} {tc δ} →
    Stack-OK i k δ tc s →
    Cont-OK i ⟨ c , s , comp-env ρ ⟩ k δ →
    [ i ∣ ⌜ 1 ⌝ ∣ max ⌜ 1 ⌝ δ ]
      exec ⟨ bra (comp tc t₂ []) (comp tc t₃ []) ∷ c
           , val (comp-val v₁) ∷ s
           , comp-env ρ
           ⟩ ≳
      ⟦if⟧ v₁ t₂ t₃ ρ >>= k

  ⟦if⟧-correct (T.lam t₁ ρ₁) t₂ t₃ {ρ} {c} {s} {k} {tc} _ _ =
    weakenˡ lemma₁₀ (

      exec ⟨ bra (comp tc t₂ []) (comp tc t₃ []) ∷ c
           , val (comp-val (T.lam t₁ ρ₁)) ∷ s
           , comp-env ρ
           ⟩                                          ≳⟨⟩ˢ

      crash                                           ∼⟨⟩ˢ

      ⟦if⟧ (T.lam t₁ ρ₁) t₂ t₃ ρ >>= k                ∎ˢ)

  ⟦if⟧-correct (T.con true) t₂ t₃ {ρ} {c} {s} {k} {tc} s-ok c-ok =
    exec ⟨ bra (comp tc t₂ []) (comp tc t₃ []) ∷ c
         , val (comp-val (T.con true)) ∷ s
         , comp-env ρ
         ⟩                                          ≳⟨ later (λ { .force → weakenˡ lemma₃ (

      exec ⟨ comp tc t₂ [] ++ c , s , comp-env ρ ⟩       ≡⟨ By.by (comp-++ _ t₂) ⟩ˢ

      exec ⟨ comp tc t₂ c , s , comp-env ρ ⟩             ≳⟨ ⟦⟧-correct t₂ _ s-ok c-ok ⟩ˢ

      ⟦ t₂ ⟧ ρ >>= k                                     ∎) }) ⟩ˢ

    ⟦if⟧ (T.con true) t₂ t₃ ρ >>= k                 ∎

  ⟦if⟧-correct (T.con false) t₂ t₃ {ρ} {c} {s} {k} {tc} s-ok c-ok =
    exec ⟨ bra (comp tc t₂ []) (comp tc t₃ []) ∷ c
         , val (comp-val (T.con false)) ∷ s
         , comp-env ρ
         ⟩                                          ≳⟨ later (λ { .force → weakenˡ lemma₃ (

      exec ⟨ comp tc t₃ [] ++ c , s , comp-env ρ ⟩       ≡⟨ By.by (comp-++ _ t₃) ⟩ˢ

      exec ⟨ comp tc t₃ c , s , comp-env ρ ⟩             ≳⟨ ⟦⟧-correct t₃ _ s-ok c-ok ⟩ˢ

      ⟦ t₃ ⟧ ρ >>= k                                     ∎) }) ⟩ˢ

    ⟦if⟧ (T.con false) t₂ t₃ ρ >>= k                ∎

-- The "time complexity" of the compiled program is linear in the time
-- complexity obtained from the instrumented interpreter, and vice
-- versa.

steps-match :
  (t : Tm 0) →
  [ ∞ ] steps (⟦ t ⟧ []) ≤ steps (exec ⟨ comp₀ t , [] , [] ⟩)
    ×
  [ ∞ ] steps (exec ⟨ comp₀ t , [] , [] ⟩) ≤
        ⌜ 1 ⌝ + ⌜ 2 ⌝ * steps (⟦ t ⟧ [])
steps-match t =                                                  $⟨ ⟦⟧-correct t [] unrestricted (λ v → laterˡ (return (comp-val v) ∎ˢ)) ⟩
  [ ∞ ∣ ⌜ 1 ⌝ ∣ max ⌜ 1 ⌝ ⌜ 1 ⌝ ]
    exec ⟨ comp₀ t , [] , [] ⟩ ≳ comp-val ⟨$⟩ ⟦ t ⟧ []           ↝⟨ proj₂ ∘ _⇔_.to ≳⇔≈×steps≤steps² ⟩

  [ ∞ ] steps (comp-val ⟨$⟩ ⟦ t ⟧ []) ≤
        steps (exec ⟨ comp₀ t , [] , [] ⟩) ×
  [ ∞ ] steps (exec ⟨ comp₀ t , [] , [] ⟩) ≤
        max ⌜ 1 ⌝ ⌜ 1 ⌝ +
        (⌜ 1 ⌝ + ⌜ 1 ⌝) * steps (comp-val ⟨$⟩ ⟦ t ⟧ [])          ↝⟨ _⇔_.to (steps-⟨$⟩ Conat.≤-cong-∼ (_ Conat.∎∼)
                                                                              ×-cong
                                                                            (_ Conat.∎∼)
                                                                              Conat.≤-cong-∼
                                                                            lemma₁₁ Conat.+-cong lemma₁₂ Conat.*-cong steps-⟨$⟩) ⟩□
  [ ∞ ] steps (⟦ t ⟧ []) ≤ steps (exec ⟨ comp₀ t , [] , [] ⟩) ×
  [ ∞ ] steps (exec ⟨ comp₀ t , [] , [] ⟩) ≤
        ⌜ 1 ⌝ + ⌜ 2 ⌝ * steps (⟦ t ⟧ [])                         □

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
module _ where

{- NOTE: To run move to adga directory or figure out how `agda -I` works -}

open import utility
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
open import Relation.Nullary
import Relation.Binary.PropositionalEquality as Prop
open import Data.Empty
open import calculus
open import context-properties
open import Esterel.Lang.Binding
open import Data.Maybe using (just ; nothing)
open import Esterel.Variable.Signal as Signal using (Signal ; _ₛ)
open import Esterel.Variable.Sequential as SeqVar using (SeqVar ; _ᵥ)
open import Esterel.Variable.Shared as ShVar using (SharedVar ; _ₛₕ)
open import Data.List.Any

S : Signal
S = 0 ₛ

start : Term
start = signl S ((emit S) >> (present S ∣⇒ pause ∣⇒ nothin))
step1 = ρ (Θ [ (just Signal.unknown) ] [] []) · ((emit S) >> (present S ∣⇒ pause ∣⇒ nothin))
step2 = ρ (Θ [ (just Signal.present) ] [] []) · (nothin >> (present S ∣⇒ pause ∣⇒ nothin))
step3 = ρ (Θ [ (just Signal.present) ] [] []) · (present S ∣⇒ pause ∣⇒ nothin)
end : Term
end   = ρ (Θ [ (just Signal.present) ] [] []) · pause

red : start ⟶* end
red = rstep{start}{step1}
          (⟶-inclusion (rraise-signal{((emit S) >> (present S ∣⇒ pause ∣⇒ nothin))}{S}) )
          (rstep {step1} {step2}
                 (⟶-inclusion (remit (Data.List.Any.Any.here Prop.refl)
                                      (deseq{p = (emit S)}{q = (present S ∣⇒ pause ∣⇒ nothin)} (dehole{emit S}))))
                 (rstep {step2} {step3}
                        (rcontext (cenv (Θ (just Signal.present ∷ []) [] []) ∷ [])
                           (dcenv dchole) rseq-done)
                        (rstep {step3} {end}
                        (rcontext [] dchole
                                    (ris-present (Data.List.Any.Any.here Prop.refl) Prop.refl dehole)) rrefl)))

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
postulate
  I : Set
  f : Set → I

mutual

  data P : I → Set where

  Q : I → Set
  Q x = P (f (P x))

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module WithoutK8 where

data I : Set where
  i : I

module M (x : I) where

  data D : Set where
    d : D

  data P : D → Set where

postulate x : I

open module M′ = M x

Foo : P d → Set
Foo ()

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Human.List where

open import Human.Nat

infixr 5 _,_
data List {a} (A : Set a) : Set a where
  end : List A
  _,_ : (x : A) (xs : List A) → List A

{-# BUILTIN LIST List #-}

{-# COMPILE JS  List = function(x,v) { if (x.length < 1) { return v["[]"](); } else { return v["_∷_"](x[0], x.slice(1)); } } #-}
{-# COMPILE JS end = Array() #-}
{-# COMPILE JS _,_ = function (x) { return function(y) { return Array(x).concat(y); }; } #-}

foldr : ∀ {A : Set} {B : Set} → (A → B → B) → B → List A → B
foldr c n end       = n
foldr c n (x , xs) = c x (foldr c n xs)

length : ∀ {A : Set} → List A → Nat
length = foldr (λ a n → suc n) zero

-- TODO --
-- filter
-- reduce

-- Receives a function that transforms each element of A, a function A and a new list, B.
map : ∀ {A : Set} {B : Set} → (f : A → B) → List A → List B
map f end      = end
map f (x , xs) = (f x) , (map f xs) -- f transforms element x, return map to do a new transformation

-- Sum all numbers in a list
sum : List Nat → Nat
sum end     = zero
sum (x , l) = x + (sum l)

remove-last : ∀ {A : Set} → List A → List A
remove-last end     = end
remove-last (x , l) = l

max_stars_repo_name: MaisaMilena/JuiceMaker

max_issues_repo_name: MaisaMilena/JuiceMaker

max_forks_repo_name: MaisaMilena/JuiceMaker


text:
{-# OPTIONS --safe #-}
module Cubical.Data.Vec.Properties where

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

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Unit
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Vec.Base
open import Cubical.Data.FinData
open import Cubical.Relation.Nullary

open Iso

private
  variable
    ℓ : Level
    A : Type ℓ

-- This is really cool!
-- Compare with: https://github.com/agda/agda-stdlib/blob/master/src/Data/Vec/Properties/WithK.agda#L32
++-assoc : ∀ {m n k} (xs : Vec A m) (ys : Vec A n) (zs : Vec A k) →
           PathP (λ i → Vec A (+-assoc m n k (~ i))) ((xs ++ ys) ++ zs) (xs ++ ys ++ zs)
++-assoc {m = zero} [] ys zs = refl
++-assoc {m = suc m} (x ∷ xs) ys zs i = x ∷ ++-assoc xs ys zs i

-- Equivalence between Fin n → A and Vec A n
FinVec→Vec : {n : ℕ} → FinVec A n → Vec A n
FinVec→Vec {n = zero}  xs = []
FinVec→Vec {n = suc _} xs = xs zero ∷ FinVec→Vec (λ x → xs (suc x))

Vec→FinVec : {n : ℕ} → Vec A n → FinVec A n
Vec→FinVec xs f = lookup f xs

FinVec→Vec→FinVec : {n : ℕ} (xs : FinVec A n) → Vec→FinVec (FinVec→Vec xs) ≡ xs
FinVec→Vec→FinVec {n = zero} xs = funExt λ f → ⊥.rec (¬Fin0 f)
FinVec→Vec→FinVec {n = suc n} xs = funExt goal
  where
  goal : (f : Fin (suc n))
       → Vec→FinVec (xs zero ∷ FinVec→Vec (λ x → xs (suc x))) f ≡ xs f
  goal zero = refl
  goal (suc f) i = FinVec→Vec→FinVec (λ x → xs (suc x)) i f

Vec→FinVec→Vec : {n : ℕ} (xs : Vec A n) → FinVec→Vec (Vec→FinVec xs) ≡ xs
Vec→FinVec→Vec {n = zero}  [] = refl
Vec→FinVec→Vec {n = suc n} (x ∷ xs) i = x ∷ Vec→FinVec→Vec xs i

FinVecIsoVec : (n : ℕ) → Iso (FinVec A n) (Vec A n)
FinVecIsoVec n = iso FinVec→Vec Vec→FinVec Vec→FinVec→Vec FinVec→Vec→FinVec

FinVec≃Vec : (n : ℕ) → FinVec A n ≃ Vec A n
FinVec≃Vec n = isoToEquiv (FinVecIsoVec n)

FinVec≡Vec : (n : ℕ) → FinVec A n ≡ Vec A n
FinVec≡Vec n = ua (FinVec≃Vec n)

isContrVec0 : isContr (Vec A 0)
isContrVec0 = [] , λ { [] → refl }

-- encode - decode Vec
module VecPath {A : Type ℓ}
  where

  code : {n : ℕ} → (v v' : Vec A n) → Type ℓ
  code [] [] = Unit*
  code (a ∷ v) (a' ∷ v') = (a ≡ a') × (v ≡ v')

  -- encode
  reflEncode : {n : ℕ} → (v : Vec A n) → code v v
  reflEncode [] = tt*
  reflEncode (a ∷ v) = refl , refl

  encode : {n : ℕ} → (v v' : Vec A n) → (v ≡ v') → code v v'
  encode v v' p = J (λ v' _ → code v v') (reflEncode v) p

  encodeRefl : {n : ℕ} → (v : Vec A n) → encode v v refl ≡ reflEncode v
  encodeRefl v = JRefl (λ v' _ → code v v') (reflEncode v)

  -- decode
  decode : {n : ℕ} → (v v' : Vec A n) → (r : code v v') → (v ≡ v')
  decode [] [] _ = refl
  decode (a ∷ v) (a' ∷ v') (p , q) = cong₂ _∷_ p q

  decodeRefl : {n : ℕ} → (v : Vec A n) → decode v v (reflEncode v) ≡ refl
  decodeRefl [] = refl
  decodeRefl (a ∷ v) = refl

  -- equiv
  ≡Vec≃codeVec : {n : ℕ} → (v v' : Vec A n) → (v ≡ v') ≃ (code v v')
  ≡Vec≃codeVec v v' = isoToEquiv is
    where
    is : Iso (v ≡ v') (code v v')
    fun is = encode v v'
    inv is = decode v v'
    rightInv is = sect v v'
      where
      sect : {n : ℕ} → (v v' : Vec A n) → (r : code v v')
             → encode v v' (decode v v' r) ≡ r
      sect [] [] tt* = encodeRefl []
      sect (a ∷ v) (a' ∷ v') (p , q) = J (λ a' p → encode (a ∷ v) (a' ∷ v') (decode (a ∷ v) (a' ∷ v') (p , q)) ≡ (p , q))
                                       (J (λ v' q → encode (a ∷ v) (a ∷ v') (decode (a ∷ v) (a ∷ v') (refl , q)) ≡ (refl , q))
                                       (encodeRefl (a ∷ v)) q) p
    leftInv is = retr v v'
      where
      retr : {n : ℕ} → (v v' : Vec A n) → (p : v ≡ v')
             → decode v v' (encode v v' p) ≡ p
      retr v v' p = J (λ v' p → decode v v' (encode v v' p) ≡ p)
                    (cong (decode v v) (encodeRefl v) ∙ decodeRefl v) p

  isOfHLevelVec : (h : HLevel) (n : ℕ)
                  → isOfHLevel (suc (suc h)) A → isOfHLevel (suc (suc h)) (Vec A n)
  isOfHLevelVec h zero ofLevelA [] [] = isOfHLevelRespectEquiv (suc h) (invEquiv (≡Vec≃codeVec [] []))
                                        (isOfHLevelUnit* (suc h))
  isOfHLevelVec h (suc n) ofLevelA (x ∷ v) (x' ∷ v') = isOfHLevelRespectEquiv (suc h) (invEquiv (≡Vec≃codeVec _ _))
                                                       (isOfHLevelΣ (suc h) (ofLevelA x x') (λ _ → isOfHLevelVec h n ofLevelA v v'))

  discreteA→discreteVecA : Discrete A → (n : ℕ) → Discrete (Vec A n)
  discreteA→discreteVecA DA zero [] [] = yes refl
  discreteA→discreteVecA DA (suc n) (a ∷ v) (a' ∷ v') with (DA a a') | (discreteA→discreteVecA DA n v v')
  ... | yes p | yes q = yes (invIsEq (snd (≡Vec≃codeVec (a ∷ v) (a' ∷ v'))) (p , q))
  ... | yes p | no ¬q = no (λ r → ¬q (snd (funIsEq (snd (≡Vec≃codeVec (a ∷ v) (a' ∷ v'))) r)))
  ... | no ¬p | yes q = no (λ r → ¬p (fst (funIsEq (snd (≡Vec≃codeVec (a ∷ v) (a' ∷ v'))) r)))
  ... | no ¬p | no ¬q = no (λ r → ¬q (snd (funIsEq (snd (≡Vec≃codeVec (a ∷ v) (a' ∷ v'))) r)))

  ≢-∷ : {m : ℕ} → (Discrete A) → (a : A) → (v : Vec A m) → (a' : A) → (v' : Vec A m) →
         (a ∷ v ≡ a' ∷ v' → ⊥.⊥) → (a ≡ a' → ⊥.⊥) ⊎ (v ≡ v' → ⊥.⊥)
  ≢-∷ {m} discreteA a v a' v' ¬r with (discreteA a a')
                        | (discreteA→discreteVecA discreteA m v v')
  ... | yes p | yes q = ⊥.rec (¬r (cong₂ _∷_ p q))
  ... | yes p | no ¬q = inr ¬q
  ... | no ¬p | y = inl ¬p

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Oscar.Data.AList where

open import Oscar.Data.Equality
open import Oscar.Data.Nat

open import Oscar.Level

module _ {a} (A : Nat → Set a) where

  data AList (n : Nat) : Nat → Set a where
    [] : AList n n
    _∷_ : ∀ {m} → A m → AList n m → AList n (suc m)

open import Oscar.Category

module Category' {a} {A : Nat → Set a} where

  _⊸_ = AList A

  infix 4 _≋_
  _≋_ : ∀ {m n} → m ⊸ n → m ⊸ n → Set a
  _≋_ = _≡_

  infixr 9 _∙_
  _∙_ : ∀ {m n} → m ⊸ n → ∀ {l} → l ⊸ m → l ⊸ n
  [] ∙ ρ = ρ
  (x ∷ σ) ∙ ρ = x ∷ (σ ∙ ρ)

  ∙-associativity : ∀ {k l} (f : k ⊸ l) {m} (g : l ⊸ m) {n} (h : m ⊸ n) → (h ∙ g) ∙ f ≋ h ∙ g ∙ f
  ∙-associativity f g [] = refl
  ∙-associativity f g (x ∷ h) = cong (x ∷_) (∙-associativity f g h)

  ε : ∀ {n} → n ⊸ n
  ε = []

  ∙-left-identity : ∀ {m n} (σ : m ⊸ n) → ε ∙ σ ≋ σ
  ∙-left-identity _ = refl

  ∙-right-identity : ∀ {m n} (σ : m ⊸ n) → σ ∙ ε ≋ σ
  ∙-right-identity [] = refl
  ∙-right-identity (x ∷ σ) = cong (x ∷_) (∙-right-identity σ)

  semigroupoidAList : Semigroupoid (AList A) (λ {x y} → ≡-setoid (AList A x y))
  Semigroupoid._∙_ semigroupoidAList = _∙_
  Semigroupoid.∙-extensionality semigroupoidAList refl refl = refl
  Semigroupoid.∙-associativity semigroupoidAList = ∙-associativity

  categoryAList : Category semigroupoidAList
  Category.ε categoryAList = ε
  Category.ε-left-identity categoryAList = ∙-left-identity _
  Category.ε-right-identity categoryAList = ∙-right-identity _

--   ∙-associativity σ _ [] = refl
--   ∙-associativity (τ asnoc t / x) ρ σ = cong (λ s → s asnoc t / x) (∙-associativity τ ρ σ)

-- -- semigroupoid : ∀ {a} (A : Nat → Set a) → Semigroupoid a a ∅̂
-- -- Semigroupoid._∙_ = semigroupoid

-- -- -- record Semigroupoid
-- -- --   {𝔬} {𝔒 :

-- -- -- -- module Oscar.Data.AList {𝔣} (FunctionName : Set 𝔣) where

-- -- -- -- open import Oscar.Data.Fin
-- -- -- -- open import Oscar.Data.Nat
-- -- -- -- open import Oscar.Data.Product
-- -- -- -- open import Oscar.Data.Term FunctionName
-- -- -- -- open import Oscar.Data.IList

-- -- -- -- pattern anil = []
-- -- -- -- pattern _asnoc_/_ σ t' x = (t' , x) ∷ σ

-- -- -- -- AList : Nat → Nat → Set 𝔣
-- -- -- -- AList m n = IList (λ m → Term m × Fin (suc m)) n m

-- -- -- -- -- data AList' (n : Nat) : Nat -> Set 𝔣 where
-- -- -- -- --   anil : AList' n n
-- -- -- -- --   _asnoc_/_ : ∀ {m} (σ : AList' n m) (t' : Term m) (x : Fin (suc m))
-- -- -- -- --                -> AList' n (suc m)

-- -- -- -- -- open import Oscar.Function
-- -- -- -- -- --AList = flip AList'

-- -- -- -- -- -- data AList : Nat -> Nat -> Set 𝔣 where
-- -- -- -- -- --   anil : ∀ {n} -> AList n n
-- -- -- -- -- --   _asnoc_/_ : ∀ {m n} (σ : AList m n) (t' : Term m) (x : Fin (suc m))
-- -- -- -- -- --                -> AList (suc m) n

-- -- -- -- -- -- -- open import Relation.Binary.PropositionalEquality renaming ([_] to [[_]])
-- -- -- -- -- -- -- open ≡-Reasoning

-- -- -- -- -- -- -- step-prop : ∀ {m n} (s t : Term (suc m)) (σ : AList m n) r z ->
-- -- -- -- -- -- --           (Unifies s t [-◇ sub (σ asnoc r / z) ]) ⇔ (Unifies ((r for z) ◃ s) ((r for z) ◃ t) [-◇ sub σ ])
-- -- -- -- -- -- -- step-prop s t σ r z f = to , from
-- -- -- -- -- -- --   where
-- -- -- -- -- -- --     lemma1 : ∀ t -> (f ◇ sub σ) ◃ ((r for z) ◃ t) ≡ (f ◇ (sub σ ◇ (r for z))) ◃ t
-- -- -- -- -- -- --     lemma1 t = bind-assoc f (sub σ) (r for z) t
-- -- -- -- -- -- --     to = λ a → begin
-- -- -- -- -- -- --                  (f ◇ sub σ) ◃ ((r for z) ◃ s) ≡⟨ lemma1 s ⟩
-- -- -- -- -- -- --                  (f ◇ (sub σ ◇ (r for z))) ◃ s ≡⟨ a ⟩
-- -- -- -- -- -- --                  (f ◇ (sub σ ◇ (r for z))) ◃ t ≡⟨ sym (lemma1 t) ⟩
-- -- -- -- -- -- --                  (f ◇ sub σ) ◃ ((r for z) ◃ t) ∎
-- -- -- -- -- -- --     from = λ a → begin
-- -- -- -- -- -- --                    (f ◇ (sub σ ◇ (r for z))) ◃ s ≡⟨ sym (lemma1 s) ⟩
-- -- -- -- -- -- --                    (f ◇ sub σ) ◃ ((r for z) ◃ s) ≡⟨ a ⟩
-- -- -- -- -- -- --                    (f ◇ sub σ) ◃ ((r for z) ◃ t) ≡⟨ lemma1 t ⟩
-- -- -- -- -- -- --                    (f ◇ (sub σ ◇ (r for z))) ◃ t ∎

-- -- -- -- -- -- -- record ⋆amgu (T : ℕ → Set) : Set where
-- -- -- -- -- -- --   field amgu : ∀ {m} (s t : T m) (acc : ∃ (AList m)) -> Maybe (∃ (AList m))

-- -- -- -- -- -- -- open ⋆amgu ⦃ … ⦄ public

-- -- -- -- -- -- -- open import Category.Monad using (RawMonad)
-- -- -- -- -- -- -- import Level
-- -- -- -- -- -- -- open RawMonad (Data.Maybe.monad {Level.zero})

-- -- -- -- -- -- -- open import Relation.Binary using (IsDecEquivalence)
-- -- -- -- -- -- -- open import Relation.Nullary using (Dec; yes; no)
-- -- -- -- -- -- -- open import Data.Nat using (ℕ; _≟_)
-- -- -- -- -- -- -- open import Data.Product using () renaming (Σ to Σ₁)
-- -- -- -- -- -- -- open Σ₁ renaming (proj₁ to π₁; proj₂ to π₂)
-- -- -- -- -- -- -- open import Data.Product using (Σ)
-- -- -- -- -- -- -- open Σ
-- -- -- -- -- -- -- open import Data.Sum
-- -- -- -- -- -- -- open import Function

-- -- -- -- -- -- -- NothingForkLeft : ∀ {m l} (s1 t1 : Term m) (ρ : AList m l) (s2 t2 : Term m) →
-- -- -- -- -- -- --                Nothing⋆ $ Unifies⋆ s1 t1 [-◇⋆ sub ρ ] →
-- -- -- -- -- -- --                Nothing⋆ $ Unifies⋆ (s1 fork s2) (t1 fork t2) [-◇⋆ sub ρ ]
-- -- -- -- -- -- -- NothingForkLeft s1 t1 ρ s2 t2 nounify = No[Q◇ρ]→No[P◇ρ] No[Q◇ρ]
-- -- -- -- -- -- --   where
-- -- -- -- -- -- --     P = Unifies⋆ (s1 fork s2) (t1 fork t2)
-- -- -- -- -- -- --     Q = (Unifies⋆ s1 t1 ∧⋆ Unifies⋆ s2 t2)
-- -- -- -- -- -- --     Q⇔P : Q ⇔⋆ P
-- -- -- -- -- -- --     Q⇔P = switch⋆ P Q (Properties.fact1' {_} {s1} {s2} {t1} {t2})
-- -- -- -- -- -- --     No[Q◇ρ]→No[P◇ρ] : Nothing⋆ (Q [-◇⋆ sub ρ ]) -> Nothing⋆ (P [-◇⋆ sub ρ ])
-- -- -- -- -- -- --     No[Q◇ρ]→No[P◇ρ] = Properties.fact2⋆ (Q [-◇⋆ sub ρ ]) (P [-◇⋆ sub ρ ]) (Properties.fact5⋆ Q P (sub ρ) Q⇔P)
-- -- -- -- -- -- --     No[Q◇ρ] : Nothing⋆ (Q [-◇⋆ sub ρ ])
-- -- -- -- -- -- --     No[Q◇ρ] = failure-propagation.first⋆ (sub ρ) (Unifies⋆ s1 t1) (Unifies⋆ s2 t2) nounify

-- -- -- -- -- -- -- NothingForkRight : ∀ {m l n} (σ : AList l n)
-- -- -- -- -- -- --                   (s1 s2 : Term m)
-- -- -- -- -- -- --                   (t1 t2 : Term m) →
-- -- -- -- -- -- --                   (ρ : AList m l) →
-- -- -- -- -- -- --                   Max⋆ (Unifies⋆ s1 t1 [-◇⋆ sub ρ ]) $ sub σ →
-- -- -- -- -- -- --                   Nothing⋆ $ Unifies⋆ s2 t2 [-◇⋆ sub (σ ++ ρ) ] →
-- -- -- -- -- -- --                   Nothing⋆ $ Unifies⋆ (s1 fork s2) (t1 fork t2) [-◇⋆ sub ρ ]
-- -- -- -- -- -- -- NothingForkRight σ s1 s2 t1 t2 ρ a nounify = No[Q◇ρ]→No[P◇ρ]⋆ No[Q◇ρ]⋆
-- -- -- -- -- -- --     where
-- -- -- -- -- -- --     P⋆ = Unifies⋆ (s1 fork s2) (t1 fork t2)
-- -- -- -- -- -- --     Q⋆ = (Unifies⋆ s1 t1 ∧⋆ Unifies⋆ s2 t2)
-- -- -- -- -- -- --     Q⇔P⋆ : Q⋆ ⇔⋆ P⋆
-- -- -- -- -- -- --     Q⇔P⋆ = switch⋆ P⋆ Q⋆ (Properties.fact1'⋆ {_} {s1} {s2} {t1} {t2})
-- -- -- -- -- -- --     No[Q◇ρ]→No[P◇ρ]⋆ : Nothing⋆ (Q⋆ [-◇⋆ sub ρ ]) -> Nothing⋆ (P⋆ [-◇⋆ sub ρ ])
-- -- -- -- -- -- --     No[Q◇ρ]→No[P◇ρ]⋆ = Properties.fact2⋆ (Q⋆ [-◇⋆ sub ρ ]) (P⋆ [-◇⋆ sub ρ ]) (Properties.fact5⋆ Q⋆ P⋆ (sub ρ) Q⇔P⋆)
-- -- -- -- -- -- --     No[Q◇ρ]⋆ : Nothing⋆ (Q⋆ [-◇⋆ sub ρ ])
-- -- -- -- -- -- --     No[Q◇ρ]⋆ = failure-propagation.second⋆ (sub ρ) (sub σ) (Unifies⋆ s1 t1) (Unifies s2 t2) a
-- -- -- -- -- -- --        (λ f → nounify f ∘ π₂ (Unifies s2 t2) (cong (f ◃_) ∘ sym ∘ SubList.fact1 σ ρ))

-- -- -- -- -- -- -- MaxFork : ∀ {m l n n1} (s1 s2 t1 t2 : Term m)
-- -- -- -- -- -- --                        (ρ : AList m l) (σ : AList l n) →
-- -- -- -- -- -- --                      Max⋆ (Unifies⋆ s1 t1 [-◇⋆ sub ρ ]) $ sub σ →
-- -- -- -- -- -- --                      (σ1 : AList n n1) →
-- -- -- -- -- -- --                      Max⋆ (Unifies⋆ s2 t2 [-◇⋆ sub (σ ++ ρ) ]) $ sub σ1 →
-- -- -- -- -- -- --                      Max⋆ (Unifies⋆ (s1 fork s2) (t1 fork t2) [-◇⋆ sub ρ ]) $ sub (σ1 ++ σ)
-- -- -- -- -- -- -- MaxFork s1 s2 t1 t2 ρ σ a σ1 b = Max[P∧Q◇ρ][σ1++σ]
-- -- -- -- -- -- --     where
-- -- -- -- -- -- --       P = Unifies s1 t1
-- -- -- -- -- -- --       Q = Unifies s2 t2
-- -- -- -- -- -- --       P∧Q = P ∧ Q
-- -- -- -- -- -- --       C = Unifies (s1 fork s2) (t1 fork t2)
-- -- -- -- -- -- --       Max[C◇ρ]⇔Max[P∧Q◇ρ] : Max (C [-◇ sub ρ ]) ⇔ Max (P∧Q [-◇ sub ρ ])
-- -- -- -- -- -- --       Max[C◇ρ]⇔Max[P∧Q◇ρ] = Max.fact (C [-◇ sub ρ ]) (P∧Q [-◇ sub ρ ]) (Properties.fact5 C P∧Q (sub ρ)
-- -- -- -- -- -- --                       (Properties.fact1' {_} {s1} {s2} {t1} {t2}))
-- -- -- -- -- -- --       Max[Q◇σ++ρ]⇔Max[Q◇σ◇ρ] : Max (Q [-◇ sub (σ ++ ρ)]) ⇔ Max (Q [-◇ sub σ ◇ sub ρ ])
-- -- -- -- -- -- --       Max[Q◇σ++ρ]⇔Max[Q◇σ◇ρ] = Max.fact (Q [-◇ sub (σ ++ ρ)]) (Q [-◇ sub σ ◇ sub ρ ]) (Properties.fact6 Q (SubList.fact1 σ ρ))
-- -- -- -- -- -- --       Max[P∧Q◇ρ][σ1++σ] : π₁ (Max (C [-◇ sub ρ ])) (sub (σ1 ++ σ))
-- -- -- -- -- -- --       Max[P∧Q◇ρ][σ1++σ] = π₂ (Max (C [-◇ sub ρ ])) (≐-sym (SubList.fact1 σ1 σ))
-- -- -- -- -- -- --                (proj₂ (Max[C◇ρ]⇔Max[P∧Q◇ρ] (sub σ1 ◇ sub σ))
-- -- -- -- -- -- --                       (optimist (sub ρ) (sub σ) (sub σ1) P Q (DClosed.fact1 s1 t1) a (proj₁ (Max[Q◇σ++ρ]⇔Max[Q◇σ◇ρ] (sub σ1)) b)))

-- -- -- -- -- -- -- NothingVecHead : ∀ {m l} (t₁ t₂ : Term m) (ρ : AList m l) {N} (ts₁ ts₂ : Vec (Term m) N) →
-- -- -- -- -- -- --                Nothing⋆ $ Unifies⋆ t₁ t₂ [-◇⋆ sub ρ ] →
-- -- -- -- -- -- --                Nothing⋆ $ Unifies⋆V (t₁ ∷ ts₁) (t₂ ∷ ts₂) [-◇⋆ sub ρ ]
-- -- -- -- -- -- -- NothingVecHead t₁ t₂ ρ ts₁ ts₂ nounify = No[Q◇ρ]→No[P◇ρ] No[Q◇ρ]
-- -- -- -- -- -- --   where
-- -- -- -- -- -- --     P = Unifies⋆V (t₁ ∷ ts₁) (t₂ ∷ ts₂)
-- -- -- -- -- -- --     Q = (Unifies⋆ t₁ t₂ ∧⋆ Unifies⋆V ts₁ ts₂)
-- -- -- -- -- -- --     Q⇔P : Q ⇔⋆ P
-- -- -- -- -- -- --     Q⇔P = switch⋆ P Q (Properties.fact1'V {_} {t₁} {t₂} {_} {ts₁} {ts₂})
-- -- -- -- -- -- --     No[Q◇ρ]→No[P◇ρ] : Nothing⋆ (Q [-◇⋆ sub ρ ]) -> Nothing⋆ (P [-◇⋆ sub ρ ])
-- -- -- -- -- -- --     No[Q◇ρ]→No[P◇ρ] = Properties.fact2⋆ (Q [-◇⋆ sub ρ ]) (P [-◇⋆ sub ρ ]) (Properties.fact5⋆ Q P (sub ρ) Q⇔P)
-- -- -- -- -- -- --     No[Q◇ρ] : Nothing⋆ (Q [-◇⋆ sub ρ ])
-- -- -- -- -- -- --     No[Q◇ρ] = failure-propagation.first⋆ (sub ρ) (Unifies⋆ t₁ t₂) (Unifies⋆V ts₁ ts₂) nounify

-- -- -- -- -- -- -- NothingVecTail : ∀ {m l n} (σ : AList l n)
-- -- -- -- -- -- --                   (t₁ t₂ : Term m)
-- -- -- -- -- -- --                   {N}
-- -- -- -- -- -- --                   (ts₁ ts₂ : Vec (Term m) N) →
-- -- -- -- -- -- --                   (ρ : AList m l) →
-- -- -- -- -- -- --                   Max⋆ (Unifies⋆ t₁ t₂ [-◇⋆ sub ρ ]) $ sub σ →
-- -- -- -- -- -- --                   Nothing⋆ $ Unifies⋆V ts₁ ts₂ [-◇⋆ sub (σ ++ ρ) ] →
-- -- -- -- -- -- --                   Nothing⋆ $ Unifies⋆V (t₁ ∷ ts₁) (t₂ ∷ ts₂) [-◇⋆ sub ρ ]
-- -- -- -- -- -- -- NothingVecTail σ t₁ t₂ ts₁ ts₂ ρ a nounify = No[Q◇ρ]→No[P◇ρ]⋆ No[Q◇ρ]⋆
-- -- -- -- -- -- --     where
-- -- -- -- -- -- --     P⋆ = Unifies⋆V (t₁ ∷ ts₁) (t₂ ∷ ts₂)
-- -- -- -- -- -- --     Q⋆ = (Unifies⋆ t₁ t₂ ∧⋆ Unifies⋆V ts₁ ts₂)
-- -- -- -- -- -- --     Q⇔P⋆ : Q⋆ ⇔⋆ P⋆
-- -- -- -- -- -- --     Q⇔P⋆ = switch⋆ P⋆ Q⋆ (Properties.fact1'V {_} {t₁} {t₂} {_} {ts₁} {ts₂})
-- -- -- -- -- -- -- --    Q⇔P⋆ = switch⋆ P⋆ Q⋆ (Properties.fact1'⋆ {_} {s1} {s2} {t1} {t2})
-- -- -- -- -- -- --     No[Q◇ρ]→No[P◇ρ]⋆ : Nothing⋆ (Q⋆ [-◇⋆ sub ρ ]) -> Nothing⋆ (P⋆ [-◇⋆ sub ρ ])
-- -- -- -- -- -- --     No[Q◇ρ]→No[P◇ρ]⋆ = Properties.fact2⋆ (Q⋆ [-◇⋆ sub ρ ]) (P⋆ [-◇⋆ sub ρ ]) (Properties.fact5⋆ Q⋆ P⋆ (sub ρ) Q⇔P⋆)
-- -- -- -- -- -- --     No[Q◇ρ]⋆ : Nothing⋆ (Q⋆ [-◇⋆ sub ρ ])
-- -- -- -- -- -- --     No[Q◇ρ]⋆ = failure-propagation.second⋆ (sub ρ) (sub σ) (Unifies⋆ t₁ t₂) (UnifiesV ts₁ ts₂) a
-- -- -- -- -- -- --        (λ f → nounify f ∘ π₂ (UnifiesV ts₁ ts₂) (cong (f ◃_) ∘ sym ∘ SubList.fact1 σ ρ))

-- -- -- -- -- -- -- MaxVec : ∀ {m l n n1} (t₁ t₂ : Term m) {N} (ts₁ ts₂ : Vec (Term m) N)
-- -- -- -- -- -- --                        (ρ : AList m l) (σ : AList l n) →
-- -- -- -- -- -- --                      Max⋆ (Unifies⋆ t₁ t₂ [-◇⋆ sub ρ ]) $ sub σ →
-- -- -- -- -- -- --                      (σ1 : AList n n1) →
-- -- -- -- -- -- --                      Max⋆ (Unifies⋆V ts₁ ts₂ [-◇⋆ sub (σ ++ ρ) ]) $ sub σ1 →
-- -- -- -- -- -- --                      Max⋆ (Unifies⋆V (t₁ ∷ ts₁) (t₂ ∷ ts₂) [-◇⋆ sub ρ ]) $ sub (σ1 ++ σ)
-- -- -- -- -- -- -- MaxVec t₁ t₂ ts₁ ts₂ ρ σ a σ1 b = Max[P∧Q◇ρ][σ1++σ]
-- -- -- -- -- -- --     where
-- -- -- -- -- -- --       P = Unifies t₁ t₂
-- -- -- -- -- -- --       Q = UnifiesV ts₁ ts₂
-- -- -- -- -- -- --       P∧Q = P ∧ Q
-- -- -- -- -- -- --       C = UnifiesV (t₁ ∷ ts₁) (t₂ ∷ ts₂)
-- -- -- -- -- -- --       Max[C◇ρ]⇔Max[P∧Q◇ρ] : Max (C [-◇ sub ρ ]) ⇔ Max (P∧Q [-◇ sub ρ ])
-- -- -- -- -- -- --       Max[C◇ρ]⇔Max[P∧Q◇ρ] = Max.fact (C [-◇ sub ρ ]) (P∧Q [-◇ sub ρ ]) (Properties.fact5 C P∧Q (sub ρ)
-- -- -- -- -- -- --                       (Properties.fact1'V {_} {t₁} {t₂} {_} {ts₁} {ts₂}))
-- -- -- -- -- -- --       Max[Q◇σ++ρ]⇔Max[Q◇σ◇ρ] : Max (Q [-◇ sub (σ ++ ρ)]) ⇔ Max (Q [-◇ sub σ ◇ sub ρ ])
-- -- -- -- -- -- --       Max[Q◇σ++ρ]⇔Max[Q◇σ◇ρ] = Max.fact (Q [-◇ sub (σ ++ ρ)]) (Q [-◇ sub σ ◇ sub ρ ]) (Properties.fact6 Q (SubList.fact1 σ ρ))
-- -- -- -- -- -- --       Max[P∧Q◇ρ][σ1++σ] : π₁ (Max (C [-◇ sub ρ ])) (sub (σ1 ++ σ))
-- -- -- -- -- -- --       Max[P∧Q◇ρ][σ1++σ] = π₂ (Max (C [-◇ sub ρ ])) (≐-sym (SubList.fact1 σ1 σ))
-- -- -- -- -- -- --                (proj₂ (Max[C◇ρ]⇔Max[P∧Q◇ρ] (sub σ1 ◇ sub σ))
-- -- -- -- -- -- --                       (optimist (sub ρ) (sub σ) (sub σ1) P Q (DClosed.fact1 t₁ t₂) a (proj₁ (Max[Q◇σ++ρ]⇔Max[Q◇σ◇ρ] (sub σ1)) b)))

-- -- -- -- -- -- -- NothingFor→NothingComposition : ∀ {m l} (s t : Term (suc m)) (ρ : AList m l)
-- -- -- -- -- -- --              (r : Term m) (z : Fin (suc m)) →
-- -- -- -- -- -- --            Nothing⋆ (Unifies⋆ ((r for z) ◃ s) ((r for z) ◃ t) [-◇⋆ sub ρ ]) →
-- -- -- -- -- -- --            Nothing⋆ (Unifies⋆ s t [-◇⋆ sub (ρ asnoc r / z) ])
-- -- -- -- -- -- -- NothingFor→NothingComposition s t ρ r z nounify = NoQ→NoP nounify
-- -- -- -- -- -- --       where
-- -- -- -- -- -- --         P = Unifies s t [-◇ sub (ρ asnoc r / z) ]
-- -- -- -- -- -- --         Q = Unifies ((r for z) ◃ s) ((r for z) ◃ t) [-◇ sub ρ ]
-- -- -- -- -- -- --         NoQ→NoP : Nothing Q → Nothing P
-- -- -- -- -- -- --         NoQ→NoP = Properties.fact2 Q P (switch P Q (step-prop s t ρ r z))

-- -- -- -- -- -- -- MaxFor→MaxComposition : ∀ {m l n} (s t : Term (suc m)) (ρ : AList m l)
-- -- -- -- -- -- --               (r : Term m) (z : Fin (suc m)) (σ : AList l n) →
-- -- -- -- -- -- --             Max⋆ (Unifies⋆ ((r for z) ◃ s) ((r for z) ◃ t) [-◇⋆ sub ρ ]) $ sub σ →
-- -- -- -- -- -- --             Max⋆ (Unifies⋆ s t [-◇⋆ sub (ρ asnoc r / z) ]) $ sub σ
-- -- -- -- -- -- -- MaxFor→MaxComposition s t ρ r z σ a = proj₂ (MaxP⇔MaxQ (sub σ)) a
-- -- -- -- -- -- --       where
-- -- -- -- -- -- --         P = Unifies s t [-◇ sub (ρ asnoc r / z) ]
-- -- -- -- -- -- --         Q = Unifies ((r for z) ◃ s) ((r for z) ◃ t) [-◇ sub ρ ]
-- -- -- -- -- -- --         MaxP⇔MaxQ : Max P ⇔ Max Q
-- -- -- -- -- -- --         MaxP⇔MaxQ = Max.fact P Q (step-prop s t ρ r z)

-- -- -- -- -- -- -- module _ ⦃ isDecEquivalenceA : IsDecEquivalence (_≡_ {A = FunctionName}) ⦄ where

-- -- -- -- -- -- --   open IsDecEquivalence isDecEquivalenceA using () renaming (_≟_ to _≟F_)

-- -- -- -- -- -- --   mutual

-- -- -- -- -- -- --     instance ⋆amguTerm : ⋆amgu Term
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguTerm leaf leaf acc = just acc
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguTerm leaf (function _ _) acc = nothing
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguTerm leaf (s' fork t') acc = nothing
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguTerm (s' fork t') leaf acc = nothing
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguTerm (s' fork t') (function _ _) acc = nothing
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguTerm (s1 fork s2) (t1 fork t2) acc =
-- -- -- -- -- -- --                       amgu s2 t2 =<< amgu s1 t1 acc
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguTerm (function fn₁ ts₁) leaf acc = nothing
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguTerm (function fn₁ {n₁} ts₁) (function fn₂ {n₂} ts₂) acc
-- -- -- -- -- -- --      with fn₁ ≟F fn₂
-- -- -- -- -- -- --     … | no _ = nothing
-- -- -- -- -- -- --     … | yes _ with n₁ ≟ n₂
-- -- -- -- -- -- --     … | no _ = nothing
-- -- -- -- -- -- --     … | yes refl = amgu ts₁ ts₂ acc
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguTerm (function fn₁ ts₁) (_ fork _) acc = nothing
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguTerm (i x) (i y) (m , anil) = just (flexFlex x y)
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguTerm (i x) t     (m , anil) = flexRigid x t
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguTerm t     (i x) (m , anil) = flexRigid x t
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguTerm s     t  (n , σ asnoc r / z) =
-- -- -- -- -- -- --              (λ σ -> σ ∃asnoc r / z) <$>
-- -- -- -- -- -- --                amgu ((r for z) ◃ s) ((r for z) ◃ t) (n , σ)

-- -- -- -- -- -- --     instance ⋆amguVecTerm : ∀ {N} → ⋆amgu (flip Vec N ∘ Term)
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguVecTerm [] [] acc = just acc
-- -- -- -- -- -- --     ⋆amgu.amgu ⋆amguVecTerm (t₁ ∷ t₁s) (t₂ ∷ t₂s) acc = amgu t₁s t₂s =<< amgu t₁ t₂ acc

-- -- -- -- -- -- --   mgu : ∀ {m} -> (s t : Term m) -> Maybe (∃ (AList m))
-- -- -- -- -- -- --   mgu {m} s t = amgu s t (m , anil)

-- -- -- -- -- -- --   mutual

-- -- -- -- -- -- --     -- We use a view so that we need to handle fewer cases in the main proof
-- -- -- -- -- -- --     data AmguT : {m : ℕ} -> (s t : Term m) -> ∃ (AList m) -> Maybe (∃ (AList m)) -> Set where
-- -- -- -- -- -- --       Flip : ∀ {m s t acc} -> amgu t s acc ≡ amgu s t acc ->
-- -- -- -- -- -- --         AmguT {m} t s acc (amgu t s acc) -> AmguT         s            t            acc        (amgu s t acc)
-- -- -- -- -- -- --       leaf-leaf : ∀ {m acc} ->             AmguT {m}     leaf         leaf         acc        (just acc)
-- -- -- -- -- -- --       fn-name   : ∀ {m fn₁ fn₂ N₁ N₂ acc} {ts₁ : Vec (Term m) N₁} {ts₂ : Vec (Term m) N₂} →
-- -- -- -- -- -- --                     fn₁ ≢ fn₂ →
-- -- -- -- -- -- --                                            AmguT {m}     (function fn₁ ts₁)
-- -- -- -- -- -- --                                                                      (function fn₂ ts₂)
-- -- -- -- -- -- --                                                                                acc        nothing
-- -- -- -- -- -- --       fn-size   : ∀ {m fn₁ fn₂ N₁ N₂ acc} {ts₁ : Vec (Term m) N₁} {ts₂ : Vec (Term m) N₂} →
-- -- -- -- -- -- --                     N₁ ≢ N₂ →
-- -- -- -- -- -- --                                            AmguT {m}     (function fn₁ ts₁)
-- -- -- -- -- -- --                                                                      (function fn₂ ts₂)
-- -- -- -- -- -- --                                                                                acc        nothing
-- -- -- -- -- -- --       fn-fn     : ∀ {m fn N acc} {ts₁ ts₂ : Vec (Term m) N} →
-- -- -- -- -- -- --                                            AmguT {m}     (function fn ts₁)
-- -- -- -- -- -- --                                                                      (function fn ts₂)
-- -- -- -- -- -- --                                                                                acc        (amgu ts₁ ts₂ acc)
-- -- -- -- -- -- --       leaf-fork : ∀ {m s t acc} ->         AmguT {m}     leaf         (s fork t)   acc        nothing
-- -- -- -- -- -- --       leaf-fn   : ∀ {m fn N} {ts : Vec (Term _) N} {acc} ->       AmguT {m}     leaf         (function fn ts)   acc        nothing
-- -- -- -- -- -- --       fork-fn   : ∀ {m s t fn N} {ts : Vec (Term _) N} {acc} ->   AmguT {m}     (s fork t)   (function fn ts)   acc        nothing
-- -- -- -- -- -- --       fork-fork : ∀ {m s1 s2 t1 t2 acc} -> AmguT {m}     (s1 fork s2) (t1 fork t2) acc        (amgu s2 t2 =<< amgu s1 t1 acc)
-- -- -- -- -- -- --       var-var   : ∀ {m x y} ->             AmguT         (i x)        (i y)        (m , anil) (just (flexFlex x y))
-- -- -- -- -- -- --       var-t : ∀ {m x t} -> i x ≢ t ->      AmguT         (i x)        t            (m , anil) (flexRigid x t)
-- -- -- -- -- -- --       s-t : ∀{m s t n σ r z} ->            AmguT {suc m} s            t            (n , σ asnoc r / z) ((λ σ -> σ ∃asnoc r / z) <$>
-- -- -- -- -- -- --                                                                                amgu ((r for z) ◃ s) ((r for z) ◃ t) (n , σ))

-- -- -- -- -- -- --     data AmguTV : {m : ℕ} -> ∀ {N} (ss ts : Vec (Term m) N) -> ∃ (AList m) -> Maybe (∃ (AList m)) -> Set where
-- -- -- -- -- -- --       fn0-fn0   : ∀ {m acc} →
-- -- -- -- -- -- --                                            AmguTV {m}     ([])
-- -- -- -- -- -- --                                                                      ([])
-- -- -- -- -- -- --                                                                                acc        (just acc)

-- -- -- -- -- -- --       fns-fns   : ∀ {m N acc} {t₁ t₂ : Term m} {ts₁ ts₂ : Vec (Term m) N} →
-- -- -- -- -- -- --                                            AmguTV {m}     ((t₁ ∷ ts₁))
-- -- -- -- -- -- --                                                                      ((t₂ ∷ ts₂))
-- -- -- -- -- -- --                                                                                acc        (amgu ts₁ ts₂ =<< amgu t₁ t₂ acc)

-- -- -- -- -- -- --   view : ∀ {m : ℕ} -> (s t : Term m) -> (acc : ∃ (AList m)) -> AmguT s t acc (amgu s t acc)
-- -- -- -- -- -- --   view leaf         leaf         acc        = leaf-leaf
-- -- -- -- -- -- --   view leaf         (s fork t)   acc        = leaf-fork
-- -- -- -- -- -- --   view (s fork t)   leaf         acc        = Flip refl leaf-fork
-- -- -- -- -- -- --   view (s1 fork s2) (t1 fork t2) acc        = fork-fork
-- -- -- -- -- -- --   view (function fn₁ {n₁} ts₁) (function fn₂ {n₂} ts₂) acc  with
-- -- -- -- -- -- --    fn₁ ≟F fn₂
-- -- -- -- -- -- --   … | no neq = fn-name neq
-- -- -- -- -- -- --   … | yes refl with n₁ ≟ n₂
-- -- -- -- -- -- --   … | yes refl = fn-fn
-- -- -- -- -- -- --   … | no neq = fn-size neq
-- -- -- -- -- -- --   view leaf         (function fn ts) acc    = leaf-fn
-- -- -- -- -- -- --   view (function fn ts) leaf         acc    = Flip refl leaf-fn
-- -- -- -- -- -- --   view (function fn ts) (_ fork _)   acc    = Flip refl fork-fn
-- -- -- -- -- -- --   view (s fork t)   (function fn ts) acc    = fork-fn
-- -- -- -- -- -- --   view (i x)        (i y)        (m , anil) = var-var
-- -- -- -- -- -- --   view (i x)        leaf         (m , anil) = var-t (λ ())
-- -- -- -- -- -- --   view (i x)        (s fork t)   (m , anil) = var-t (λ ())
-- -- -- -- -- -- --   view (i x)        (function fn ts)   (m , anil) = var-t (λ ())
-- -- -- -- -- -- --   view leaf         (i x)        (m , anil) = Flip refl (var-t (λ ()))
-- -- -- -- -- -- --   view (s fork t)   (i x)        (m , anil) = Flip refl (var-t (λ ()))
-- -- -- -- -- -- --   view (function fn ts) (i x)    (m , anil) = Flip refl (var-t (λ ()))
-- -- -- -- -- -- --   view (i x)        (i x')       (n , σ asnoc r / z) = s-t
-- -- -- -- -- -- --   view (i x)        leaf         (n , σ asnoc r / z) = s-t
-- -- -- -- -- -- --   view (i x)        (s fork t)   (n , σ asnoc r / z) = s-t
-- -- -- -- -- -- --   view leaf         (i x)        (n , σ asnoc r / z) = s-t
-- -- -- -- -- -- --   view (s fork t)   (i x)        (n , σ asnoc r / z) = s-t
-- -- -- -- -- -- --   view (function fn ts)   (i x)        (n , σ asnoc r / z) = s-t
-- -- -- -- -- -- --   view (i x) (function fn ts)          (n , σ asnoc r / z) = s-t

-- -- -- -- -- -- --   viewV : ∀ {m : ℕ} {N} -> (ss ts : Vec (Term m) N) -> (acc : ∃ (AList m)) -> AmguTV ss ts acc (amgu ss ts acc)
-- -- -- -- -- -- --   viewV []         []         acc        = fn0-fn0
-- -- -- -- -- -- --   viewV (t ∷ ts₁) (t₂ ∷ ts₂) acc         = fns-fns

-- -- -- -- -- -- --   amgu-Correctness : {m : ℕ} -> (s t : Term m) -> ∃ (AList m) -> Set
-- -- -- -- -- -- --   amgu-Correctness s t (l , ρ) =
-- -- -- -- -- -- --       (∃ λ n → ∃ λ σ → π₁ (Max (Unifies s t [-◇ sub ρ ])) (sub σ) × amgu s t (l , ρ) ≡ just (n , σ ++ ρ ))
-- -- -- -- -- -- --     ⊎ (Nothing ((Unifies s t) [-◇ sub ρ ]) ×  amgu s t (l , ρ) ≡ nothing)

-- -- -- -- -- -- --   amgu-Correctness⋆ : {m : ℕ} -> (s t : Term m) -> ∃ (AList m) -> Set
-- -- -- -- -- -- --   amgu-Correctness⋆ s t (l , ρ) =
-- -- -- -- -- -- --       (∃ λ n → ∃ λ σ → π₁ (Max (Unifies s t [-◇ sub ρ ])) (sub σ) × amgu s t (l , ρ) ≡ just (n , σ ++ ρ ))
-- -- -- -- -- -- --     ⊎ (Nothing ((Unifies s t) [-◇ sub ρ ]) ×  amgu s t (l , ρ) ≡ nothing)

-- -- -- -- -- -- --   amgu-Ccomm : ∀ {m} s t acc -> amgu {m = m} s t acc ≡ amgu t s acc -> amgu-Correctness s t acc -> amgu-Correctness t s acc
-- -- -- -- -- -- --   amgu-Ccomm s t (l , ρ) st≡ts = lemma
-- -- -- -- -- -- --     where
-- -- -- -- -- -- --       Unst = (Unifies s t) [-◇ sub ρ ]
-- -- -- -- -- -- --       Unts = (Unifies t s) [-◇ sub ρ ]

-- -- -- -- -- -- --       Unst⇔Unts : ((Unifies s t) [-◇ sub ρ ]) ⇔ ((Unifies t s) [-◇ sub ρ ])
-- -- -- -- -- -- --       Unst⇔Unts = Properties.fact5 (Unifies s t) (Unifies t s) (sub ρ) (Properties.fact1 {_} {s} {t})

-- -- -- -- -- -- --       lemma : amgu-Correctness s t (l , ρ) -> amgu-Correctness t s (l , ρ)
-- -- -- -- -- -- --       lemma (inj₁ (n , σ , MaxUnst , amgu≡just)) =
-- -- -- -- -- -- --         inj₁ (n , σ , proj₁ (Max.fact Unst Unts Unst⇔Unts (sub σ)) MaxUnst , trans (sym st≡ts) amgu≡just)
-- -- -- -- -- -- --       lemma (inj₂ (NoUnst , amgu≡nothing)) =
-- -- -- -- -- -- --         inj₂ ((λ {_} → Properties.fact2 Unst Unts Unst⇔Unts NoUnst) , trans (sym st≡ts) amgu≡nothing)

-- -- -- -- -- -- --   amgu-Ccomm⋆ : ∀ {m} s t acc -> amgu {m = m} s t acc ≡ amgu t s acc -> amgu-Correctness⋆ s t acc -> amgu-Correctness⋆ t s acc
-- -- -- -- -- -- --   amgu-Ccomm⋆ s t (l , ρ) st≡ts = lemma
-- -- -- -- -- -- --     where
-- -- -- -- -- -- --       Unst = (Unifies s t) [-◇ sub ρ ]
-- -- -- -- -- -- --       Unts = (Unifies t s) [-◇ sub ρ ]

-- -- -- -- -- -- --       Unst⇔Unts : ((Unifies s t) [-◇ sub ρ ]) ⇔ ((Unifies t s) [-◇ sub ρ ])
-- -- -- -- -- -- --       Unst⇔Unts = Properties.fact5 (Unifies s t) (Unifies t s) (sub ρ) (Properties.fact1 {_} {s} {t})

-- -- -- -- -- -- --       lemma : amgu-Correctness s t (l , ρ) -> amgu-Correctness t s (l , ρ)
-- -- -- -- -- -- --       lemma (inj₁ (n , σ , MaxUnst , amgu≡just)) =
-- -- -- -- -- -- --         inj₁ (n , σ , proj₁ (Max.fact Unst Unts Unst⇔Unts (sub σ)) MaxUnst , trans (sym st≡ts) amgu≡just)
-- -- -- -- -- -- --       lemma (inj₂ (NoUnst , amgu≡nothing)) =
-- -- -- -- -- -- --         inj₂ ((λ {_} → Properties.fact2 Unst Unts Unst⇔Unts NoUnst) , trans (sym st≡ts) amgu≡nothing)

-- -- -- -- -- -- --   mutual

-- -- -- -- -- -- --     amguV-c : ∀ {m N} {ss ts : Vec (Term m) N} {l ρ} -> AmguTV ss ts (l , ρ) (amgu ss ts (l , ρ)) ->
-- -- -- -- -- -- --                 (∃ λ n → ∃ λ σ → Max⋆ (Unifies⋆V ss ts [-◇⋆ sub ρ ]) (sub σ) × amgu {m = m} ss ts (l , ρ) ≡ just (n , σ ++ ρ ))
-- -- -- -- -- -- --               ⊎ (Nothing⋆ (Unifies⋆V ss ts [-◇⋆ sub ρ ])                     × amgu {m = m} ss ts (l , ρ) ≡ nothing)
-- -- -- -- -- -- --     amguV-c {m} {N} {ss} {ts} {l} {ρ} amg with amgu ss ts (l , ρ)
-- -- -- -- -- -- --     amguV-c {m} {0} {.[]} {.[]} {l} {ρ} fn0-fn0 | .(just (l , ρ)) = inj₁ (_ , anil , trivial-problemV {_} {_} {_} {[]} {sub ρ} , cong (just ∘ _,_ l) (sym (SubList.anil-id-l ρ)))
-- -- -- -- -- -- --     amguV-c {m} {.(suc _)} {(t₁ ∷ ts₁)} {(t₂ ∷ ts₂)} {l} {ρ} fns-fns | _  with amgu t₁ t₂ (l , ρ)  | amgu-c $ view t₁ t₂ (l , ρ)
-- -- -- -- -- -- --     amguV-c {m} {.(suc _)} {(t₁ ∷ ts₁)} {(t₂ ∷ ts₂)} {l} {ρ} fns-fns | _ | am | inj₂ (nounify , refl) = inj₂ ((λ {_} → NothingVecHead t₁ t₂ ρ _ _ nounify) , refl)
-- -- -- -- -- -- --     amguV-c {m} {.(suc _)} {(t₁ ∷ ts₁)} {(t₂ ∷ ts₂)} {l} {ρ} fns-fns | _ | am | inj₁ (n , σ , a , refl)
-- -- -- -- -- -- --      with amgu ts₁ ts₂ (n , σ ++ ρ) | amguV-c (viewV (ts₁) (ts₂) (n , (σ ++ ρ)))
-- -- -- -- -- -- --     … | _ | inj₂ (nounify , refl) = inj₂ ((λ {_} → NothingVecTail σ t₁ t₂ _ _ ρ a nounify) , refl)
-- -- -- -- -- -- --     … | _ | inj₁ (n1 , σ1 , a1 , refl) = inj₁ (n1 , σ1 ++ σ , MaxVec t₁ t₂ _ _ ρ σ a σ1 a1 , cong (λ σ -> just (n1 , σ)) (++-assoc σ1 σ ρ))

-- -- -- -- -- -- --     amgu-c : ∀ {m s t l ρ} -> AmguT s t (l , ρ) (amgu s t (l , ρ)) ->
-- -- -- -- -- -- --                (∃ λ n → ∃ λ σ → Max⋆ (Unifies⋆ s t [-◇⋆ sub ρ ]) (sub σ) × amgu {m = m} s t (l , ρ) ≡ just (n , σ ++ ρ ))
-- -- -- -- -- -- --              ⊎ (Nothing⋆ (Unifies⋆ s t [-◇⋆ sub ρ ])                     × amgu {m = m} s t (l , ρ) ≡ nothing)
-- -- -- -- -- -- --     amgu-c {m} {s} {t} {l} {ρ} amg with amgu s t (l , ρ)
-- -- -- -- -- -- --     amgu-c {l = l} {ρ} leaf-leaf | ._
-- -- -- -- -- -- --       = inj₁ (l , anil , trivial-problem {_} {_} {leaf} {sub ρ} , cong (λ x -> just (l , x)) (sym (SubList.anil-id-l ρ)) )
-- -- -- -- -- -- --     amgu-c (fn-name neq) | _ = inj₂ ((λ f x → neq (Term-function-inj-FunctionName x)) , refl)
-- -- -- -- -- -- --     amgu-c (fn-size neq) | _ = inj₂ ((λ f x → neq (Term-function-inj-VecSize x)) , refl)
-- -- -- -- -- -- --     amgu-c {s = function fn ts₁} {t = function .fn ts₂} {l = l} {ρ = ρ} fn-fn | _ with amgu ts₁ ts₂ | amguV-c (viewV ts₁ ts₂ (l , ρ))
-- -- -- -- -- -- --     … | _ | inj₂ (nounify , refl!) rewrite refl! = inj₂ ((λ {_} f feq → nounify f (Term-function-inj-Vector feq)) , refl)
-- -- -- -- -- -- --     … | _ | inj₁ (n , σ , (b , c) , refl!) rewrite refl! = inj₁ (_ , _ , ((cong (function fn) b) , (λ {_} f' feq → c f' (Term-function-inj-Vector feq))) , refl )
-- -- -- -- -- -- --     amgu-c leaf-fork | .nothing = inj₂ ((λ _ () ) , refl)
-- -- -- -- -- -- --     amgu-c leaf-fn | _ = inj₂ ((λ _ () ) , refl)
-- -- -- -- -- -- --     amgu-c fork-fn | _ = inj₂ ((λ _ () ) , refl)
-- -- -- -- -- -- --     amgu-c {m} {s1 fork s2} {t1 fork t2} {l} {ρ} fork-fork | ._
-- -- -- -- -- -- --      with amgu s1 t1 (l , ρ)  | amgu-c $ view s1 t1 (l , ρ)
-- -- -- -- -- -- --     … | .nothing             | inj₂ (nounify , refl) = inj₂ ((λ {_} -> NothingForkLeft s1 t1 ρ s2 t2 nounify) , refl)
-- -- -- -- -- -- --     … | .(just (n , σ ++ ρ)) | inj₁ (n , σ , a , refl)
-- -- -- -- -- -- --      with amgu s2 t2 (n , σ ++ ρ) | amgu-c (view s2 t2 (n , (σ ++ ρ)))
-- -- -- -- -- -- --     … | .nothing                | inj₂ (nounify , refl) = inj₂ ( (λ {_} -> NothingForkRight σ s1 s2 t1 t2 ρ a nounify) , refl)
-- -- -- -- -- -- --     … | .(just (n1 , σ1 ++ (σ ++ ρ))) | inj₁ (n1 , σ1 , b , refl)
-- -- -- -- -- -- --         = inj₁ (n1 , σ1 ++ σ , MaxFork s1 s2 t1 t2 ρ σ a σ1 b , cong (λ σ -> just (n1 , σ)) (++-assoc σ1 σ ρ))
-- -- -- -- -- -- --     amgu-c {suc l} {i x} {i y} (var-var) | .(just (flexFlex x y))
-- -- -- -- -- -- --      with thick? x y | Thick.fact1 x y (thick? x y) refl
-- -- -- -- -- -- --     …  | .(just y') | inj₂ (y' , thinxy'≡y , refl )
-- -- -- -- -- -- --       = inj₁ (l , anil asnoc i y' / x , var-elim-i-≡ x (i y) (sym (cong i thinxy'≡y)) , refl )
-- -- -- -- -- -- --     …  | .nothing | inj₁ ( x≡y , refl ) rewrite sym x≡y
-- -- -- -- -- -- --       = inj₁ (suc l , anil , trivial-problem {_} {_} {i x} {sub anil} , refl)
-- -- -- -- -- -- --     amgu-c {suc l} {i x} {t} (var-t ix≢t) | .(flexRigid x t)
-- -- -- -- -- -- --      with check x t | check-prop x t
-- -- -- -- -- -- --     … | .nothing  | inj₂ ( ps , r , refl) = inj₂ ( (λ {_} -> NothingStep x t ix≢t ps r )  , refl)
-- -- -- -- -- -- --     … | .(just t') | inj₁ (t' , r , refl) = inj₁ ( l , anil asnoc t' / x , var-elim-i-≡ x t r , refl )
-- -- -- -- -- -- --     amgu-c {suc m} {s} {t} {l} {ρ asnoc r / z} s-t
-- -- -- -- -- -- --       | .((λ x' → x' ∃asnoc r / z) <$>
-- -- -- -- -- -- --           (amgu ((r for z) ◃ s) ((r for z) ◃ t) (l , ρ)))
-- -- -- -- -- -- --      with amgu-c (view ((r for z) ◃ s) ((r for z) ◃ t) (l , ρ))
-- -- -- -- -- -- --     … | inj₂ (nounify , ra) = inj₂ ( (λ {_} -> NothingFor→NothingComposition s t ρ r z nounify) , cong (_<$>_ (λ x' → x' ∃asnoc r / z)) ra )
-- -- -- -- -- -- --     … | inj₁ (n , σ , a , ra)  = inj₁ (n , σ , MaxFor→MaxComposition s t ρ r z σ a , cong (_<$>_ (λ x' → x' ∃asnoc r / z)) ra)
-- -- -- -- -- -- --     amgu-c {m} {s} {t} {l} {ρ} (Flip amguts≡amgust amguts) | ._ = amgu-Ccomm⋆ t s (l , ρ) amguts≡amgust (amgu-c amguts)
-- -- -- -- -- -- --     amgu-c {zero} {i ()} _ | _

-- -- -- -- -- -- --   mgu-c : ∀ {m} (s t : Term m) ->
-- -- -- -- -- -- --              (∃ λ n → ∃ λ σ → (Max⋆ (Unifies⋆ s t)) (sub σ) × mgu s t ≡ just (n , σ))
-- -- -- -- -- -- --            ⊎ (Nothing⋆ (Unifies⋆ s t)                       × mgu s t ≡ nothing)
-- -- -- -- -- -- --   mgu-c {m} s t = amgu-c (view s t (m , anil))

-- -- -- -- -- -- --   unify : ∀ {m} (s t : Term m) ->
-- -- -- -- -- -- --              (∃ λ n → ∃ λ (σ : AList m n) → Max⋆ (Unifies⋆ s t) $ sub σ)
-- -- -- -- -- -- --              ⊎ Nothing⋆ (Unifies⋆ s t)
-- -- -- -- -- -- --   unify {m} s t with amgu-c (view s t (m , anil))
-- -- -- -- -- -- --   unify {m} s₁ t | inj₁ (proj₃ , proj₄ , proj₅ , proj₆) = inj₁ (proj₃ , proj₄ , proj₅)
-- -- -- -- -- -- --   unify {m} s t | inj₂ (proj₃ , _) = inj₂ proj₃

-- -- -- -- -- -- --   unifyV : ∀ {m N} (s t : Vec (Term m) N) ->
-- -- -- -- -- -- --              (∃ λ n → ∃ λ (σ : AList m n) → Max⋆ (Unifies⋆V s t) $ sub σ)
-- -- -- -- -- -- --              ⊎ Nothing⋆ (Unifies⋆V s t)
-- -- -- -- -- -- --   unifyV {m} {N} s t with amguV-c (viewV s t (m , anil))
-- -- -- -- -- -- --   … | inj₁ (proj₃ , proj₄ , proj₅ , proj₆) = inj₁ (proj₃ , proj₄ , proj₅)
-- -- -- -- -- -- --   … | inj₂ (proj₃ , _) = inj₂ proj₃

-- -- -- -- -- -- --   open import Oscar.Data.Permutation

-- -- -- -- -- -- --   unifyWith : ∀ {m N} (p q : Term m) (X Y : Vec (Term m) N) →
-- -- -- -- -- -- --               (∃ λ X* → X* ≡ordering' X × ∃ λ n → ∃ λ (σ : AList m n) → Max⋆ (Unifies⋆V (p ∷ X*) (q ∷ Y)) $ sub σ)
-- -- -- -- -- -- --               ⊎
-- -- -- -- -- -- --               (∀ X* → X* ≡ordering' X → Nothing⋆ (Unifies⋆V (p ∷ X*) (q ∷ Y)))
-- -- -- -- -- -- --   unifyWith p q X Y = {!!}


text:
module AKS.Primality where

open import AKS.Primality.Base public
open import AKS.Primality.Properties public

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


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

open import Categories.Category.Core using (Category)
open import Categories.Comonad

-- Verbatim dual of Categories.Adjoint.Construction.Kleisli
module Categories.Adjoint.Construction.CoKleisli {o ℓ e} {C : Category o ℓ e} (M : Comonad C) where

open import Categories.Category.Construction.CoKleisli
open import Categories.Adjoint
open import Categories.Functor
open import Categories.Functor.Properties
open import Categories.NaturalTransformation.Core
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_)
open import Categories.Morphism.Reasoning C

private
  module C = Category C
  module M = Comonad M
  open M.F
  open C
  open HomReasoning
  open Equiv

Forgetful : Functor (CoKleisli M) C
Forgetful =
 record
  { F₀           = λ X → F₀ X
  ; F₁           = λ f → F₁ f ∘ M.δ.η _
  ; identity     = Comonad.identityˡ M
  ; homomorphism = λ {X Y Z} {f g} → hom-proof {X} {Y} {Z} {f} {g}
  ; F-resp-≈     = λ eq → ∘-resp-≈ˡ (F-resp-≈ eq)
  }
  where
  trihom : {X Y Z W : Obj} {f : X ⇒ Y} {g : Y ⇒ Z} {h : Z ⇒ W} → F₁ (h ∘ g ∘ f) ≈ F₁ h ∘ F₁ g ∘ F₁ f
  trihom {X} {Y} {Z} {W} {f} {g} {h} = begin
   F₁ (h ∘ g ∘ f)     ≈⟨ homomorphism ⟩
   F₁ h ∘ F₁ (g ∘ f)  ≈⟨ refl⟩∘⟨ homomorphism ⟩
   F₁ h ∘ F₁ g ∘ F₁ f ∎
  hom-proof :
   {X Y Z : Obj} {f : F₀ X ⇒ Y} {g : F₀ Y ⇒ Z} →
   (F₁ (g ∘ F₁ f ∘ M.δ.η X)) ∘ M.δ.η X ≈ (F₁ g ∘ M.δ.η Y) ∘ F₁ f ∘ M.δ.η X
  hom-proof {X} {Y} {Z} {f} {g} = begin
   (F₁ (g ∘ F₁ f ∘ M.δ.η X)) ∘ M.δ.η X         ≈⟨ pushˡ trihom ⟩
   F₁ g ∘ (F₁ (F₁ f) ∘ F₁ (M.δ.η X)) ∘ M.δ.η X ≈⟨ refl⟩∘⟨ (pullʳ (sym M.assoc)) ⟩
   F₁ g ∘ F₁ (F₁ f) ∘ M.δ.η (F₀ X) ∘ M.δ.η X   ≈⟨ refl⟩∘⟨ pullˡ (sym (M.δ.commute f)) ⟩
   F₁ g ∘ (M.δ.η Y ∘ F₁ f) ∘ M.δ.η X           ≈⟨ assoc²'' ⟩
   (F₁ g ∘ M.δ.η Y) ∘ F₁ f ∘ M.δ.η X           ∎

Cofree : Functor C (CoKleisli M)
Cofree =
 record
  { F₀ = λ X → X
  ; F₁ = λ f → f ∘ M.ε.η _
  ; identity = λ {A} → identityˡ
  ; homomorphism = λ {X Y Z} {f g} → hom-proof {X} {Y} {Z} {f} {g}
  ; F-resp-≈ = λ x → ∘-resp-≈ˡ x
  }
  where
  hom-proof :
   {X Y Z : Obj} {f : X ⇒ Y} {g : Y ⇒ Z} →
   (g ∘ f) ∘ M.ε.η X ≈ (g ∘ M.ε.η Y) ∘ (F₁ (f ∘ M.ε.η X) ∘ M.δ.η X)
  hom-proof {X} {Y} {Z} {f} {g} = begin
   (g ∘ f) ∘ M.ε.η X                               ≈⟨ pullʳ (sym (M.ε.commute f)) ⟩
   g ∘ M.ε.η Y ∘ F₁ f                              ≈⟨ sym (pullʳ (refl⟩∘⟨ elimʳ (Comonad.identityˡ M))) ⟩
   (g ∘ M.ε.η Y) ∘ (F₁ f ∘ F₁ (M.ε.η X) ∘ M.δ.η X) ≈⟨ refl⟩∘⟨ pullˡ (sym homomorphism) ⟩
   (g ∘ M.ε.η Y) ∘ (F₁ (f ∘ M.ε.η X) ∘ M.δ.η X)    ∎

FC≃M : Forgetful ∘F Cofree ≃ M.F
FC≃M =
 record
  { F⇒G = ntHelper record
    { η = λ X → F₁ C.id
    ; commute = λ {X Y} f → to-commute {X} {Y} f
    }
  ; F⇐G = ntHelper record
    { η = λ X → F₁ C.id
    ; commute = λ {X Y} f → from-commute {X} {Y} f
    }
  ; iso = λ X → record
    { isoˡ = elimʳ identity ○ identity
    ; isoʳ = elimʳ identity ○ identity
    }
  }
  where
  to-commute : {X Y : Obj} → (f : X ⇒ Y) → F₁ C.id ∘ F₁ (f ∘ M.ε.η X) ∘ M.δ.η X ≈ F₁ f ∘ F₁ C.id
  to-commute {X} {Y} f = begin
   F₁ C.id ∘ F₁ (f ∘ M.ε.η X) ∘ M.δ.η X ≈⟨ elimˡ identity ⟩
   F₁ (f ∘ M.ε.η X) ∘ M.δ.η X           ≈⟨ pushˡ homomorphism ⟩
   F₁ f ∘ F₁ (M.ε.η X) ∘ M.δ.η X        ≈⟨ refl⟩∘⟨ Comonad.identityˡ M ⟩
   F₁ f ∘ C.id                          ≈⟨ refl⟩∘⟨ sym identity ⟩
   F₁ f ∘ F₁ C.id                       ∎
  from-commute : {X Y : Obj} → (f : X ⇒ Y) → F₁ C.id ∘ F₁ f ≈ (F₁ (f ∘ M.ε.η X) ∘ M.δ.η X) ∘ F₁ C.id
  from-commute {X} {Y} f = begin
      F₁ C.id ∘ F₁ f                            ≈⟨ [ M.F ]-resp-square id-comm-sym ⟩
      F₁ f ∘ F₁ C.id                            ≈⟨ introʳ (Comonad.identityˡ M) ⟩∘⟨refl ⟩
      (F₁ f ∘ F₁ (M.ε.η X) ∘ M.δ.η X) ∘ F₁ C.id ≈⟨ pullˡ (sym homomorphism) ⟩∘⟨refl ⟩
      (F₁ (f ∘ M.ε.η X) ∘ M.δ.η X) ∘ F₁ C.id    ∎

-- useful lemma:
FF1≈1 : {X : Obj} → F₁ (F₁ (C.id {X})) ≈ C.id
FF1≈1 {X} = begin
 F₁ (F₁ (C.id {X})) ≈⟨ F-resp-≈ identity ⟩
 F₁ (C.id)          ≈⟨ identity ⟩
 C.id               ∎

Forgetful⊣Cofree : Forgetful ⊣ Cofree
Forgetful⊣Cofree =
 record
  { unit = ntHelper record
    { η = λ X → F₁ C.id
    ; commute = λ {X Y} f → unit-commute {X} {Y} f
    }
  ; counit = ntHelper record
    { η = M.ε.η
    ; commute = λ {X Y} f → counit-commute {X} {Y} f
    }
  ; zig = λ {A} → zig-proof {A}
  ; zag = λ {B} → zag-proof {B}
  }
  where
  unit-commute : ∀ {X Y : Obj} →
   (f : F₀ X ⇒ Y) →
   F₁ C.id ∘ F₁ f ∘ M.δ.η X ≈ ((F₁ f ∘ M.δ.η X) ∘ M.ε.η (F₀ X)) ∘ F₁ (F₁ C.id) ∘ M.δ.η X
  unit-commute {X} {Y} f = begin
   F₁ C.id ∘ F₁ f ∘ M.δ.η X                                   ≈⟨ elimˡ identity ⟩
   F₁ f ∘  M.δ.η X                                            ≈⟨ introʳ (Comonad.identityʳ M) ⟩
   (F₁ f ∘ M.δ.η X) ∘ M.ε.η (F₀ X) ∘ M.δ.η X                  ≈⟨ sym assoc ⟩
   ((F₁ f ∘ M.δ.η X) ∘ M.ε.η (F₀ X)) ∘ M.δ.η X                ≈⟨ intro-center FF1≈1 ⟩
   ((F₁ f ∘ M.δ.η X) ∘ M.ε.η (F₀ X)) ∘ F₁ (F₁ C.id) ∘ M.δ.η X ∎
  counit-commute : ∀ {X Y : Obj} →
   (f : X ⇒ Y) →
   M.ε.η Y ∘ (F₁ (f ∘ M.ε.η X) ∘ M.δ.η X) ≈ f ∘ M.ε.η X
  counit-commute {X} {Y} f = begin
   M.ε.η Y ∘ F₁ (f ∘ M.ε.η X) ∘ M.δ.η X      ≈⟨ refl⟩∘⟨ pushˡ homomorphism ⟩
   M.ε.η Y ∘ (F₁ f ∘ F₁ (M.ε.η X) ∘ M.δ.η X) ≈⟨ refl⟩∘⟨ elimʳ (Comonad.identityˡ M) ⟩
   M.ε.η Y ∘ F₁ f                            ≈⟨ M.ε.commute f ⟩
   f ∘ M.ε.η X ∎
  zig-proof : {A : Obj} → M.ε.η (F₀ A) ∘ F₁ (F₁ C.id) ∘ M.δ.η _ ≈ C.id
  zig-proof {A} = begin
   M.ε.η (F₀ A) ∘ F₁ (F₁ C.id) ∘ M.δ.η _ ≈⟨ elim-center FF1≈1 ⟩
   M.ε.η (F₀ A) ∘ M.δ.η _                ≈⟨ Comonad.identityʳ M ⟩
   C.id                                  ∎
  zag-proof : {B : Obj} → (M.ε.η B ∘ M.ε.η (F₀ B)) ∘ (F₁ (F₁ C.id) ∘ M.δ.η _) ≈ M.ε.η B
  zag-proof {B} = begin
    (M.ε.η B ∘ M.ε.η (F₀ B)) ∘ (F₁ (F₁ C.id) ∘ M.δ.η _) ≈⟨ assoc ⟩
    M.ε.η B ∘ (M.ε.η (F₀ B) ∘ (F₁ (F₁ C.id) ∘ M.δ.η _)) ≈⟨ refl⟩∘⟨ elim-center FF1≈1 ⟩
    M.ε.η B ∘ (M.ε.η (F₀ B) ∘ M.δ.η _)                  ≈⟨ elimʳ (Comonad.identityʳ M) ⟩
    M.ε.η B                                             ∎

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --safe #-}
{-
  This uses ideas from Floris van Doorn's phd thesis and the code in
  https://github.com/cmu-phil/Spectral/blob/master/spectrum/basic.hlean
-}
module Cubical.Homotopy.Spectrum where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Unit.Pointed
open import Cubical.Foundations.Equiv

open import Cubical.Data.Int

open import Cubical.Homotopy.Prespectrum

private
  variable
    ℓ : Level

record Spectrum (ℓ : Level) : Type (ℓ-suc ℓ) where
  open GenericPrespectrum
  field
    prespectrum : Prespectrum ℓ
    equiv : (k : ℤ) → isEquiv (fst (map prespectrum k))
  open GenericPrespectrum prespectrum public


text:
{-

This file contains:
    - the abelianization of groups as a HIT as proposed in https://arxiv.org/abs/2007.05833

The definition of the abelianization is not as a set-quotient, since the relation of abelianization is cumbersome to work with.

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Abelianization.Base where

open import Cubical.Data.Sigma

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties

private
  variable
    ℓ : Level

module _ (G : Group ℓ) where
  open GroupStr {{...}}
  open GroupTheory G
  private
    instance
      _ = snd G

  {-
    The definition of the abelianization of a group as a higher inductive type.
    The generality of the comm relation will be needed to define the group structure on the abelianization.
  -}
  data Abelianization : Type ℓ where
    η : (g : fst G) → Abelianization
    comm : (a b c : fst G) → η (a · (b · c)) ≡ η (a · (c · b))
    isset : (x y : Abelianization) → (p q : x ≡ y) → p ≡ q


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

open import Categories.Category

module Categories.Category.Construction.Properties.Presheaves.Complete {o ℓ e} (C : Category o ℓ e) where

open import Data.Product
open import Function.Equality using (Π) renaming (_∘_ to _∙_)
open import Relation.Binary
open import Relation.Binary.Construct.Closure.SymmetricTransitive as ST using (Plus⇔)
open Plus⇔

open import Categories.Category.Complete
open import Categories.Category.Cocomplete
open import Categories.Category.Construction.Presheaves
open import Categories.Category.Instance.Setoids
open import Categories.Category.Instance.Properties.Setoids
open import Categories.Diagram.Limit as Lim
open import Categories.Diagram.Colimit
open import Categories.Functor
open import Categories.NaturalTransformation

import Categories.Category.Construction.Cones as Co
import Categories.Category.Construction.Cocones as Coc
import Relation.Binary.Reasoning.Setoid as SetoidR

private
  module C = Category C
  open C
  open Π using (_⟨$⟩_)

module _ o′ where
  private
    P = Presheaves′ o′ o′ C
    module P = Category P

    module _ {J : Category o′ o′ o′} (F : Functor J P) where
      module J = Category J
      module F = Functor F
      open F
      module F₀ j = Functor (F₀ j)
      module F₁ {a b} (f : a J.⇒ b) = NaturalTransformation (F₁ f)
      open Setoid using () renaming (_≈_ to [_]_≈_)

      F[-,_] : Obj → Functor J (Setoids o′ o′)
      F[-, X ] = record
        { F₀           = λ j → F₀.₀ j X
        ; F₁           = λ f → F₁.η f X
        ; identity     = identity
        ; homomorphism = homomorphism
        ; F-resp-≈     = λ eq → F-resp-≈ eq -- this application cannot be eta reduced
        }

      -- limit related definitions

      module LimFX X = Limit (Setoids-Complete _ _ _ o′ o′ F[-, X ])

      module FCone (K : Co.Cone F) where
        open Co.Cone F K public
        module N = Functor N
        module ψ j = NaturalTransformation (ψ j)

      module FCone⇒ {K K′ : Co.Cone F} (K⇒K′ : Co.Cone⇒ F K K′) where
        open Co.Cone⇒ F K⇒K′ public
        module arr = NaturalTransformation arr

      FXcone : ∀ X → (K : Co.Cone F) → Co.Cone F[-, X ]
      FXcone X K = record
        { N    = N.₀ X
        ; apex = record
          { ψ       = λ j → ψ.η j X
          ; commute = λ f → commute f -- this application cannot be eta reduced
          }
        }
        where open FCone K

      ⊤ : Co.Cone F
      ⊤ = record
        { N    = record
          { F₀           = λ X → LimFX.apex X
          ; F₁           = λ {A B} f → record
            { _⟨$⟩_ = λ { (S , eq) → (λ j → F₀.₁ j f ⟨$⟩ S j) , λ {X Y} g →
              let open SetoidR (F₀.₀ Y B)
              in begin
                F₁.η g B ⟨$⟩ (F₀.₁ X f ⟨$⟩ S X) ≈⟨ F₁.commute g f (Setoid.refl (F₀.₀ X A)) ⟩
                F₀.₁ Y f ⟨$⟩ (F₁.η g A ⟨$⟩ S X) ≈⟨ Π.cong (F₀.₁ Y f) (eq g) ⟩
                F₀.₁ Y f ⟨$⟩ S Y ∎ }
            ; cong  = λ eq j → Π.cong (F₀.₁ j f) (eq j)
            }
          ; identity     = λ eq j → F₀.identity j (eq j)
          ; homomorphism = λ eq j → F₀.homomorphism j (eq j)
          ; F-resp-≈     = λ eq eq′ j → F₀.F-resp-≈ j eq (eq′ j)
          }
        ; apex = record
          { ψ       = λ j → ntHelper record
            { η       = λ X → record
              { _⟨$⟩_ = λ { (S , eq) → S j }
              ; cong  = λ eq → eq j
              }
            ; commute = λ f eq → Π.cong (F₀.₁ j f) (eq j)
            }
          ; commute = λ { {Y} {Z} f {W} {S₁ , eq₁} {S₂ , eq₂} eq →
            let open SetoidR (F₀.₀ Z W)
            in begin
              F₁.η f W ⟨$⟩ S₁ Y ≈⟨ eq₁ f ⟩
              S₁ Z              ≈⟨ eq Z ⟩
              S₂ Z              ∎ }
          }
        }

      K⇒⊤′ : ∀ X {K} → Co.Cones F [ K , ⊤ ] → Co.Cones F[-, X ] [ FXcone X K , LimFX.limit X ]
      K⇒⊤′ X {K} K⇒⊤ = record
        { arr     = arr.η X
        ; commute = comm
        }
        where open FCone⇒ K⇒⊤ renaming (commute to comm)

      complete : Limit F
      complete = record
        { terminal = record
          { ⊤        = ⊤
          ; !        = λ {K} →
            let module K = FCone K
            in record
            { arr     = ntHelper record
              { η       = λ X → LimFX.rep X (FXcone X K)
              ; commute = λ {X Y} f eq j → K.ψ.commute j f eq
              }
            ; commute = λ eq → Π.cong (K.ψ.η _ _) eq
            }
          ; !-unique = λ K⇒⊤ {X} → LimFX.terminal.!-unique X (K⇒⊤′ X K⇒⊤)
          }
        }

      -- colimit related definitions

      module ColimFX X = Colimit (Setoids-Cocomplete _ _ _ o′ o′ F[-, X ])

      module FCocone (K : Coc.Cocone F) where
        open Coc.Cocone F K public
        module N = Functor N
        module ψ j = NaturalTransformation (ψ j)

      module FCocone⇒ {K K′ : Coc.Cocone F} (K⇒K′ : Coc.Cocone⇒ F K K′) where
        open Coc.Cocone⇒ F K⇒K′ public
        module arr = NaturalTransformation arr

      FXcocone : ∀ X → (K : Coc.Cocone F) → Coc.Cocone F[-, X ]
      FXcocone X K = record
        { N      = N.₀ X
        ; coapex = record
          { ψ       = λ j → ψ.η j X
          ; commute = λ f → commute f -- this application cannot be eta reduced
          }
        }
        where open FCocone K

      ⊥ : Coc.Cocone F
      ⊥ = record
        { N      = record
          { F₀           = λ X → ColimFX.coapex X
          ; F₁           = λ {A B} f → record
            { _⟨$⟩_ = λ { (j , Sj) → j , F₀.₁ j f ⟨$⟩ Sj  }
            ; cong  = λ { {a , Sa} {b , Sb} →
              ST.map (λ { (j , Sj) → j , F₀.₁ j f ⟨$⟩ Sj }) (helper f) }
            }
          ; identity     = λ { {A} {j , _} eq → forth⁺ (J.id , identity (F₀.identity j (Setoid.refl (F₀.₀ j A)))) eq }
          ; homomorphism = λ {X Y Z} {f g} → λ { {_} {j , Sj} eq →
            let open Setoid (F₀.₀ j Z)
            in ST.trans (coc o′ o′ F[-, Z ])
                        (ST.map (hom-map f g) (helper (f ∘ g)) eq)
                        (forth (J.id , trans (identity refl) (F₀.homomorphism j (Setoid.refl (F₀.₀ j X))))) }
          ; F-resp-≈     = λ {A B} {f g} eq → λ { {j , Sj} eq′ →
            let open Setoid (F₀.₀ j B)
            in ST.trans (coc o′ o′ F[-, B ])
                        (forth (J.id , trans (identity refl) (F₀.F-resp-≈ j eq (Setoid.refl (F₀.₀ j A)))))
                        (ST.map (λ { (j , Sj) → (j , F₀.₁ j g ⟨$⟩ Sj) }) (helper g) eq′) }
          }
        ; coapex = record
          { ψ       = λ j → ntHelper record
            { η       = λ X → record
              { _⟨$⟩_ = j ,_
              ; cong  = λ eq → forth (-, identity eq)
              }
            ; commute = λ {X Y} f eq → back (-, identity (Π.cong (F₀.₁ j f) (Setoid.sym (F₀.₀ j X) eq)))
            }
          ; commute = λ {a b} f {X} {x y} eq →
            let open ST.Plus⇔Reasoning (coc o′ o′ F[-, X ])
            in back (f , Π.cong (F₁.η f X) (Setoid.sym (F₀.₀ a X) eq))
          }
        }
        where helper : ∀ {A B} (f : B C.⇒ A) {a Sa b Sb} →
                         Σ (a J.⇒ b) (λ g → [ F₀.₀ b A ] F₁.η g A ⟨$⟩ Sa ≈ Sb) →
                         Σ (a J.⇒ b) λ h → [ F₀.₀ b B ] F₁.η h B ⟨$⟩ (F₀.₁ a f ⟨$⟩ Sa) ≈ F₀.₁ b f ⟨$⟩ Sb
              helper {A} {B} f {a} {Sa} {b} {Sb} (g , eq′) =
                let open SetoidR (F₀.₀ b B)
                in g , (begin
                  F₁.η g B ⟨$⟩ (F₀.₁ a f ⟨$⟩ Sa) ≈⟨ F₁.commute g f (Setoid.refl (F₀.₀ a A)) ⟩
                  F₀.₁ b f ⟨$⟩ (F₁.η g A ⟨$⟩ Sa) ≈⟨ Π.cong (F₀.₁ b f) eq′ ⟩
                  F₀.₁ b f ⟨$⟩ Sb ∎)

              hom-map : ∀ {X Y Z} → Y C.⇒ X → Z C.⇒ Y → Σ J.Obj (λ j → Setoid.Carrier (F₀.₀ j X)) → Σ J.Obj (λ j → Setoid.Carrier (F₀.₀ j Z))
              hom-map f g (j , Sj) = j , F₀.₁ j (f ∘ g) ⟨$⟩ Sj

      ⊥⇒K′ : ∀ X {K} → Coc.Cocones F [ ⊥ , K ] → Coc.Cocones F[-, X ] [ ColimFX.colimit X , FXcocone X K ]
      ⊥⇒K′ X {K} ⊥⇒K = record
        { arr     = arr.η X
        ; commute = comm
        }
        where open FCocone⇒ ⊥⇒K renaming (commute to comm)

      ! : {K : Coc.Cocone F} → Coc.Cocone⇒ F ⊥ K
      ! {K} = record
        { arr     = ntHelper record
          { η       = λ X → ColimFX.rep X (FXcocone X K)
          ; commute = λ {X Y} f → λ { {a , Sa} {b , Sb} eq →
            let open SetoidR (K.N.F₀ Y)
            in begin
              K.ψ.η a Y ⟨$⟩ (F₀.₁ a f ⟨$⟩ Sa) ≈⟨ K.ψ.commute a f (Setoid.refl (F₀.₀ a X)) ⟩
              K.N.F₁ f ⟨$⟩ (K.ψ.η a X ⟨$⟩ Sa) ≈⟨ Π.cong (K.N.F₁ f) (ST.minimal (coc o′ o′ F[-, X ]) (K.N.₀ X) (Kψ X) (helper X) eq) ⟩
              K.N.F₁ f ⟨$⟩ (K.ψ.η b X ⟨$⟩ Sb) ∎ }
          }
        ; commute = λ eq → Π.cong (K.ψ.η _ _) eq
        }
        where module K = FCocone K
              Kψ : ∀ X → Σ J.Obj (λ j → Setoid.Carrier (F₀.₀ j X)) → Setoid.Carrier (K.N.F₀ X)
              Kψ X (j , S) = K.ψ.η j X ⟨$⟩ S
              helper : ∀ X → coc o′ o′ F[-, X ] =[ Kψ X ]⇒ [ K.N.₀ X ]_≈_
              helper X {a , Sa} {b , Sb} (f , eq) = begin
                K.ψ.η a X ⟨$⟩ Sa                ≈˘⟨ K.commute f (Setoid.refl (F₀.₀ a X)) ⟩
                K.ψ.η b X ⟨$⟩ (F₁.η f X ⟨$⟩ Sa) ≈⟨ Π.cong (K.ψ.η b X) eq ⟩
                K.ψ.η b X ⟨$⟩ Sb                ∎
                where open SetoidR (K.N.₀ X)

      cocomplete : Colimit F
      cocomplete = record
        { initial = record
          { ⊥        = ⊥
          ; !        = !
          ; !-unique = λ ⊥⇒K {X} → ColimFX.initial.!-unique X (⊥⇒K′ X ⊥⇒K)
          }
        }

  Presheaves-Complete : Complete o′ o′ o′ P
  Presheaves-Complete F = complete F

  Presheaves-Cocomplete : Cocomplete o′ o′ o′ P
  Presheaves-Cocomplete F = cocomplete F

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


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

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

Test : Set
Test = ℕ

test : Test → ℕ
test zero = zero
test (suc n) = test n


text:
module Serializer where

open import Data.List
open import Data.Fin hiding (_+_)
open import Data.Nat
open import Data.Product
open import Data.Bool
open import Function using (_∘_ ; _$_ ; _∋_)
open import Function.Injection hiding (_∘_)
open import Function.Surjection hiding (_∘_)
open import Function.Bijection hiding (_∘_)
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import Reflection

open import Helper.Fin
open import Helper.CodeGeneration

-----------------------------------
-- Generic
-----------------------------------

-- Finite

record Serializer (T : Set) : Set where
  constructor serializer
  field
    size : ℕ
    from : T -> Fin size
    to : Fin size -> T
    bijection : Bijection (setoid T) (setoid (Fin size))

max_stars_repo_name: mathijsb/generic-in-agda

max_issues_repo_name: mathijsb/generic-in-agda

max_forks_repo_name: mathijsb/generic-in-agda


text:
------------------------------------------------------------------------------
-- Test the consistency of FOTC.Data.List
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

-- In the module FOTC.Data.List we declare Agda postulates as FOL
-- axioms. We test if it is possible to prove an unprovable theorem
-- from these axioms.

module FOTC.Data.List.Consistency.Axioms where

open import FOTC.Base
open import FOTC.Data.List

------------------------------------------------------------------------------

postulate impossible : ∀ d e → d ≡ e
{-# ATP prove impossible #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc