text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- List-related properties
------------------------------------------------------------------------

-- Note that the lemmas below could be generalised to work with other
-- equalities than _≡_.

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

module Data.List.Properties where

open import Algebra.Bundles
open import Algebra.Definitions as AlgebraicDefinitions using (Involutive)
import Algebra.Structures as AlgebraicStructures
open import Data.Bool.Base using (Bool; false; true; not; if_then_else_)
open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ; inject₁)
open import Data.List.Base as List
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Data.Nat.Base
open import Data.Nat.Properties
open import Data.Product as Prod hiding (map; zip)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Data.These.Base as These using (These; this; that; these)
open import Function
open import Level using (Level)
open import Relation.Binary as B using (DecidableEquality)
import Relation.Binary.Reasoning.Setoid as EqR
open import Relation.Binary.PropositionalEquality as P hiding ([_])
open import Relation.Binary as B using (Rel)
open import Relation.Nullary.Reflects using (invert)
open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no)
open import Relation.Nullary.Negation using (contradiction; ¬?)
open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋)
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Unary using (Pred; Decidable; ∁)
open import Relation.Unary.Properties using (∁?)

open ≡-Reasoning

private
  variable
    a b c d e p : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d
    E : Set e

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

module _ {x y : A} {xs ys : List A} where

  ∷-injective : x ∷ xs ≡ y List.∷ ys → x ≡ y × xs ≡ ys
  ∷-injective refl = (refl , refl)

  ∷-injectiveˡ : x ∷ xs ≡ y List.∷ ys → x ≡ y
  ∷-injectiveˡ refl = refl

  ∷-injectiveʳ : x ∷ xs ≡ y List.∷ ys → xs ≡ ys
  ∷-injectiveʳ refl = refl

  ∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x List.∷ xs ≡ y ∷ ys)
  ∷-dec x≟y xs≟ys = Decidable.map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys)

≡-dec : DecidableEquality A → DecidableEquality (List A)
≡-dec _≟_ []       []       = yes refl
≡-dec _≟_ (x ∷ xs) []       = no λ()
≡-dec _≟_ []       (y ∷ ys) = no λ()
≡-dec _≟_ (x ∷ xs) (y ∷ ys) = ∷-dec (x ≟ y) (≡-dec _≟_ xs ys)

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

map-id : map id ≗ id {A = List A}
map-id []       = refl
map-id (x ∷ xs) = cong (x ∷_) (map-id xs)

map-id₂ : ∀ {f : A → A} {xs} → All (λ x → f x ≡ x) xs → map f xs ≡ xs
map-id₂ []           = refl
map-id₂ (fx≡x ∷ pxs) = cong₂ _∷_ fx≡x (map-id₂ pxs)

map-++-commute : ∀ (f : A → B) xs ys →
                 map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++-commute f []       ys = refl
map-++-commute f (x ∷ xs) ys = cong (f x ∷_) (map-++-commute f xs ys)

map-cong : ∀ {f g : A → B} → f ≗ g → map f ≗ map g
map-cong f≗g []       = refl
map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (map-cong f≗g xs)

map-cong₂ : ∀ {f g : A → B} {xs} →
            All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs
map-cong₂ []                = refl
map-cong₂ (fx≡gx ∷ fxs≡gxs) = cong₂ _∷_ fx≡gx (map-cong₂ fxs≡gxs)

length-map : ∀ (f : A → B) xs → length (map f xs) ≡ length xs
length-map f []       = refl
length-map f (x ∷ xs) = cong suc (length-map f xs)

map-compose : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
map-compose []       = refl
map-compose (x ∷ xs) = cong (_ ∷_) (map-compose xs)

------------------------------------------------------------------------
-- mapMaybe

mapMaybe-just : (xs : List A) → mapMaybe just xs ≡ xs
mapMaybe-just []       = refl
mapMaybe-just (x ∷ xs) = cong (x ∷_) (mapMaybe-just xs)

mapMaybe-nothing : (xs : List A) →
                   mapMaybe {B = A} (λ _ → nothing) xs ≡ []
mapMaybe-nothing []       = refl
mapMaybe-nothing (x ∷ xs) = mapMaybe-nothing xs

module _ (f : A → Maybe B) where

  mapMaybe-concatMap : mapMaybe f ≗ concatMap (fromMaybe ∘ f)
  mapMaybe-concatMap [] = refl
  mapMaybe-concatMap (x ∷ xs) with f x
  ... | just y  = cong (y ∷_) (mapMaybe-concatMap xs)
  ... | nothing = mapMaybe-concatMap xs

  length-mapMaybe : ∀ xs → length (mapMaybe f xs) ≤ length xs
  length-mapMaybe []       = z≤n
  length-mapMaybe (x ∷ xs) with f x
  ... | just y  = s≤s (length-mapMaybe xs)
  ... | nothing = ≤-step (length-mapMaybe xs)

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

length-++ : ∀ (xs : List A) {ys} →
            length (xs ++ ys) ≡ length xs + length ys
length-++ []       = refl
length-++ (x ∷ xs) = cong suc (length-++ xs)

module _ {A : Set a} where

  open AlgebraicDefinitions {A = List A} _≡_
  open AlgebraicStructures  {A = List A} _≡_

  ++-assoc : Associative _++_
  ++-assoc []       ys zs = refl
  ++-assoc (x ∷ xs) ys zs = cong (x ∷_) (++-assoc xs ys zs)

  ++-identityˡ : LeftIdentity [] _++_
  ++-identityˡ xs = refl

  ++-identityʳ : RightIdentity [] _++_
  ++-identityʳ []       = refl
  ++-identityʳ (x ∷ xs) = cong (x ∷_) (++-identityʳ xs)

  ++-identity : Identity [] _++_
  ++-identity = ++-identityˡ , ++-identityʳ

  ++-identityʳ-unique : ∀ (xs : List A) {ys} → xs ≡ xs ++ ys → ys ≡ []
  ++-identityʳ-unique []       refl = refl
  ++-identityʳ-unique (x ∷ xs) eq   =
    ++-identityʳ-unique xs (proj₂ (∷-injective eq))

  ++-identityˡ-unique : ∀ {xs} (ys : List A) → xs ≡ ys ++ xs → ys ≡ []
  ++-identityˡ-unique               []       _  = refl
  ++-identityˡ-unique {xs = x ∷ xs} (y ∷ ys) eq
    with ++-identityˡ-unique (ys ++ [ x ]) (begin
         xs                  ≡⟨ proj₂ (∷-injective eq) ⟩
         ys ++ x ∷ xs        ≡⟨ sym (++-assoc ys [ x ] xs) ⟩
         (ys ++ [ x ]) ++ xs ∎)
  ++-identityˡ-unique {xs = x ∷ xs} (y ∷ []   ) eq | ()
  ++-identityˡ-unique {xs = x ∷ xs} (y ∷ _ ∷ _) eq | ()

  ++-cancelˡ : ∀ xs {ys zs : List A} → xs ++ ys ≡ xs ++ zs → ys ≡ zs
  ++-cancelˡ []       ys≡zs             = ys≡zs
  ++-cancelˡ (x ∷ xs) x∷xs++ys≡x∷xs++zs = ++-cancelˡ xs (∷-injectiveʳ x∷xs++ys≡x∷xs++zs)

  ++-cancelʳ : ∀ {xs : List A} ys zs → ys ++ xs ≡ zs ++ xs → ys ≡ zs
  ++-cancelʳ {_}  []       []       _             = refl
  ++-cancelʳ {xs} []       (z ∷ zs) eq =
    contradiction (trans (cong length eq) (length-++ (z ∷ zs))) (m≢1+n+m (length xs))
  ++-cancelʳ {xs} (y ∷ ys) []       eq =
    contradiction (trans (sym (length-++ (y ∷ ys))) (cong length eq)) (m≢1+n+m (length xs) ∘ sym)
  ++-cancelʳ {_}  (y ∷ ys) (z ∷ zs) eq =
    cong₂ _∷_ (∷-injectiveˡ eq) (++-cancelʳ ys zs (∷-injectiveʳ eq))

  ++-cancel : Cancellative _++_
  ++-cancel = ++-cancelˡ , ++-cancelʳ

  ++-conicalˡ : ∀ (xs ys : List A) → xs ++ ys ≡ [] → xs ≡ []
  ++-conicalˡ []       _ refl = refl

  ++-conicalʳ : ∀ (xs ys : List A) → xs ++ ys ≡ [] → ys ≡ []
  ++-conicalʳ []       _ refl = refl

  ++-conical : Conical [] _++_
  ++-conical = ++-conicalˡ , ++-conicalʳ

  ++-isMagma : IsMagma _++_
  ++-isMagma = record
    { isEquivalence = isEquivalence
    ; ∙-cong        = cong₂ _++_
    }

  ++-isSemigroup : IsSemigroup _++_
  ++-isSemigroup = record
    { isMagma = ++-isMagma
    ; assoc   = ++-assoc
    }

  ++-isMonoid : IsMonoid _++_ []
  ++-isMonoid = record
    { isSemigroup = ++-isSemigroup
    ; identity    = ++-identity
    }

module _ (A : Set a) where

  ++-semigroup : Semigroup a a
  ++-semigroup = record
    { Carrier     = List A
    ; isSemigroup = ++-isSemigroup
    }

  ++-monoid : Monoid a a
  ++-monoid = record
    { Carrier  = List A
    ; isMonoid = ++-isMonoid
    }

------------------------------------------------------------------------
-- alignWith

module _ {f g : These A B → C} where

  alignWith-cong : f ≗ g → ∀ as → alignWith f as ≗ alignWith g as
  alignWith-cong f≗g []         bs       = map-cong (f≗g ∘ that) bs
  alignWith-cong f≗g as@(_ ∷ _) []       = map-cong (f≗g ∘ this) as
  alignWith-cong f≗g (a ∷ as)   (b ∷ bs) =
    cong₂ _∷_ (f≗g (these a b)) (alignWith-cong f≗g as bs)

  length-alignWith : ∀ xs ys →
                   length (alignWith f xs ys) ≡ length xs ⊔ length ys
  length-alignWith []         ys       = length-map (f ∘′ that) ys
  length-alignWith xs@(_ ∷ _) []       = length-map (f ∘′ this) xs
  length-alignWith (x ∷ xs)   (y ∷ ys) = cong suc (length-alignWith xs ys)

  alignWith-map : (g : D → A) (h : E → B) →
                  ∀ xs ys → alignWith f (map g xs) (map h ys) ≡
                            alignWith (f ∘′ These.map g h) xs ys
  alignWith-map g h []         ys     = sym (map-compose ys)
  alignWith-map g h xs@(_ ∷ _) []     = sym (map-compose xs)
  alignWith-map g h (x ∷ xs) (y ∷ ys) =
    cong₂ _∷_ refl (alignWith-map g h xs ys)

  map-alignWith : ∀ (g : C → D) → ∀ xs ys →
                  map g (alignWith f xs ys) ≡
                  alignWith (g ∘′ f) xs ys
  map-alignWith g []         ys     = sym (map-compose ys)
  map-alignWith g xs@(_ ∷ _) []     = sym (map-compose xs)
  map-alignWith g (x ∷ xs) (y ∷ ys) =
    cong₂ _∷_ refl (map-alignWith g xs ys)

------------------------------------------------------------------------
-- zipWith

module _ (f : A → A → B) where

  zipWith-comm : (∀ x y → f x y ≡ f y x) →
                 ∀ xs ys → zipWith f xs ys ≡ zipWith f ys xs
  zipWith-comm f-comm []       []       = refl
  zipWith-comm f-comm []       (x ∷ ys) = refl
  zipWith-comm f-comm (x ∷ xs) []       = refl
  zipWith-comm f-comm (x ∷ xs) (y ∷ ys) =
    cong₂ _∷_ (f-comm x y) (zipWith-comm f-comm xs ys)

module _ (f : A → B → C) where

  zipWith-identityˡ : ∀ xs → zipWith f [] xs ≡ []
  zipWith-identityˡ []       = refl
  zipWith-identityˡ (x ∷ xs) = refl

  zipWith-identityʳ : ∀ xs → zipWith f xs [] ≡ []
  zipWith-identityʳ []       = refl
  zipWith-identityʳ (x ∷ xs) = refl

  length-zipWith : ∀ xs ys →
                   length (zipWith f xs ys) ≡ length xs ⊓ length ys
  length-zipWith []       []       = refl
  length-zipWith []       (y ∷ ys) = refl
  length-zipWith (x ∷ xs) []       = refl
  length-zipWith (x ∷ xs) (y ∷ ys) = cong suc (length-zipWith xs ys)

  zipWith-map : ∀ {d e} {D : Set d} {E : Set e} (g : D → A) (h : E → B) →
                ∀ xs ys → zipWith f (map g xs) (map h ys) ≡
                          zipWith (λ x y → f (g x) (h y)) xs ys
  zipWith-map g h []       []       = refl
  zipWith-map g h []       (y ∷ ys) = refl
  zipWith-map g h (x ∷ xs) []       = refl
  zipWith-map g h (x ∷ xs) (y ∷ ys) =
    cong₂ _∷_ refl (zipWith-map g h xs ys)

  map-zipWith : ∀ {d} {D : Set d} (g : C → D) → ∀ xs ys →
                map g (zipWith f xs ys) ≡
                zipWith (λ x y → g (f x y)) xs ys
  map-zipWith g []       []       = refl
  map-zipWith g []       (y ∷ ys) = refl
  map-zipWith g (x ∷ xs) []       = refl
  map-zipWith g (x ∷ xs) (y ∷ ys) =
    cong₂ _∷_ refl (map-zipWith g xs ys)

------------------------------------------------------------------------
-- unalignWith

unalignWith-this : unalignWith ((A → These A B) ∋ this) ≗ (_, [])
unalignWith-this []       = refl
unalignWith-this (a ∷ as) = cong (Prod.map₁ (a ∷_)) (unalignWith-this as)

unalignWith-that : unalignWith ((B → These A B) ∋ that) ≗ ([] ,_)
unalignWith-that []       = refl
unalignWith-that (b ∷ bs) = cong (Prod.map₂ (b ∷_)) (unalignWith-that bs)

module _ {f g : C → These A B} where

  unalignWith-cong : f ≗ g → unalignWith f ≗ unalignWith g
  unalignWith-cong f≗g []       = refl
  unalignWith-cong f≗g (c ∷ cs) with f c | g c | f≗g c
  ... | this a    | ._ | refl = cong (Prod.map₁ (a ∷_)) (unalignWith-cong f≗g cs)
  ... | that b    | ._ | refl = cong (Prod.map₂ (b ∷_)) (unalignWith-cong f≗g cs)
  ... | these a b | ._ | refl = cong (Prod.map (a ∷_) (b ∷_)) (unalignWith-cong f≗g cs)

module _ (f : C → These A B) where

  unalignWith-map : (g : D → C) → ∀ ds →
                    unalignWith f (map g ds) ≡ unalignWith (f ∘′ g) ds
  unalignWith-map g []       = refl
  unalignWith-map g (d ∷ ds) with f (g d)
  ... | this a    = cong (Prod.map₁ (a ∷_)) (unalignWith-map g ds)
  ... | that b    = cong (Prod.map₂ (b ∷_)) (unalignWith-map g ds)
  ... | these a b = cong (Prod.map (a ∷_) (b ∷_)) (unalignWith-map g ds)

  map-unalignWith : (g : A → D) (h : B → E) →
    Prod.map (map g) (map h) ∘′ unalignWith f ≗ unalignWith (These.map g h ∘′ f)
  map-unalignWith g h []       = refl
  map-unalignWith g h (c ∷ cs) with f c
  ... | this a    = cong (Prod.map₁ (g a ∷_)) (map-unalignWith g h cs)
  ... | that b    = cong (Prod.map₂ (h b ∷_)) (map-unalignWith g h cs)
  ... | these a b = cong (Prod.map (g a ∷_) (h b ∷_)) (map-unalignWith g h cs)

  unalignWith-alignWith : (g : These A B → C) → f ∘′ g ≗ id → ∀ as bs →
                          unalignWith f (alignWith g as bs) ≡ (as , bs)
  unalignWith-alignWith g g∘f≗id []         bs = begin
    unalignWith f (map (g ∘′ that) bs) ≡⟨ unalignWith-map (g ∘′ that) bs ⟩
    unalignWith (f ∘′ g ∘′ that) bs    ≡⟨ unalignWith-cong (g∘f≗id ∘ that) bs ⟩
    unalignWith that bs                ≡⟨ unalignWith-that bs ⟩
    [] , bs                            ∎
  unalignWith-alignWith g g∘f≗id as@(_ ∷ _) [] = begin
    unalignWith f (map (g ∘′ this) as) ≡⟨ unalignWith-map (g ∘′ this) as ⟩
    unalignWith (f ∘′ g ∘′ this) as    ≡⟨ unalignWith-cong (g∘f≗id ∘ this) as ⟩
    unalignWith this as                ≡⟨ unalignWith-this as ⟩
    as , []                            ∎
  unalignWith-alignWith g g∘f≗id (a ∷ as)   (b ∷ bs)
    rewrite g∘f≗id (these a b) =
    cong (Prod.map (a ∷_) (b ∷_)) (unalignWith-alignWith g g∘f≗id as bs)

------------------------------------------------------------------------
-- unzipWith

module _ (f : A → B × C) where

  length-unzipWith₁ : ∀ xys →
                     length (proj₁ (unzipWith f xys)) ≡ length xys
  length-unzipWith₁ []        = refl
  length-unzipWith₁ (x ∷ xys) = cong suc (length-unzipWith₁ xys)

  length-unzipWith₂ : ∀ xys →
                     length (proj₂ (unzipWith f xys)) ≡ length xys
  length-unzipWith₂ []        = refl
  length-unzipWith₂ (x ∷ xys) = cong suc (length-unzipWith₂ xys)

  zipWith-unzipWith : (g : B → C → A) → uncurry′ g ∘ f ≗ id →
                      uncurry′ (zipWith g) ∘ (unzipWith f)  ≗ id
  zipWith-unzipWith g f∘g≗id []       = refl
  zipWith-unzipWith g f∘g≗id (x ∷ xs) =
    cong₂ _∷_ (f∘g≗id x) (zipWith-unzipWith g f∘g≗id xs)

------------------------------------------------------------------------
-- foldr

foldr-universal : ∀ (h : List A → B) f e → (h [] ≡ e) →
                  (∀ x xs → h (x ∷ xs) ≡ f x (h xs)) →
                  h ≗ foldr f e
foldr-universal h f e base step []       = base
foldr-universal h f e base step (x ∷ xs) = begin
  h (x ∷ xs)          ≡⟨ step x xs ⟩
  f x (h xs)          ≡⟨ cong (f x) (foldr-universal h f e base step xs) ⟩
  f x (foldr f e xs)  ∎

foldr-cong : ∀ {f g : A → B → B} {d e : B} →
             (∀ x y → f x y ≡ g x y) → d ≡ e →
             foldr f d ≗ foldr g e
foldr-cong f≗g refl []      = refl
foldr-cong f≗g d≡e (x ∷ xs) rewrite foldr-cong f≗g d≡e xs = f≗g x _

foldr-fusion : ∀ (h : B → C) {f : A → B → B} {g : A → C → C} (e : B) →
               (∀ x y → h (f x y) ≡ g x (h y)) →
               h ∘ foldr f e ≗ foldr g (h e)
foldr-fusion h {f} {g} e fuse =
  foldr-universal (h ∘ foldr f e) g (h e) refl
                  (λ x xs → fuse x (foldr f e xs))

id-is-foldr : id {A = List A} ≗ foldr _∷_ []
id-is-foldr = foldr-universal id _∷_ [] refl (λ _ _ → refl)

++-is-foldr : (xs ys : List A) → xs ++ ys ≡ foldr _∷_ ys xs
++-is-foldr xs ys = begin
  xs ++ ys                ≡⟨ cong (_++ ys) (id-is-foldr xs) ⟩
  foldr _∷_ [] xs ++ ys   ≡⟨ foldr-fusion (_++ ys) [] (λ _ _ → refl) xs ⟩
  foldr _∷_ ([] ++ ys) xs ≡⟨⟩
  foldr _∷_ ys xs         ∎

foldr-++ : ∀ (f : A → B → B) x ys zs →
           foldr f x (ys ++ zs) ≡ foldr f (foldr f x zs) ys
foldr-++ f x []       zs = refl
foldr-++ f x (y ∷ ys) zs = cong (f y) (foldr-++ f x ys zs)

map-is-foldr : {f : A → B} → map f ≗ foldr (λ x ys → f x ∷ ys) []
map-is-foldr {f = f} xs = begin
  map f xs                        ≡⟨ cong (map f) (id-is-foldr xs) ⟩
  map f (foldr _∷_ [] xs)         ≡⟨ foldr-fusion (map f) [] (λ _ _ → refl) xs ⟩
  foldr (λ x ys → f x ∷ ys) [] xs ∎

foldr-∷ʳ : ∀ (f : A → B → B) x y ys →
           foldr f x (ys ∷ʳ y) ≡ foldr f (f y x) ys
foldr-∷ʳ f x y []       = refl
foldr-∷ʳ f x y (z ∷ ys) = cong (f z) (foldr-∷ʳ f x y ys)

-- Interaction with predicates

module _ {P : Pred A p} {f : A → A → A} where

  foldr-forcesᵇ : (∀ x y → P (f x y) → P x × P y) →
                  ∀ e xs → P (foldr f e xs) → All P xs
  foldr-forcesᵇ _      _ []       _     = []
  foldr-forcesᵇ forces _ (x ∷ xs) Pfold with forces _ _ Pfold
  ... | (px , pfxs) = px ∷ foldr-forcesᵇ forces _ xs pfxs

  foldr-preservesᵇ : (∀ {x y} → P x → P y → P (f x y)) →
                     ∀ {e xs} → P e → All P xs → P (foldr f e xs)
  foldr-preservesᵇ _    Pe []         = Pe
  foldr-preservesᵇ pres Pe (px ∷ pxs) = pres px (foldr-preservesᵇ pres Pe pxs)

  foldr-preservesʳ : (∀ x {y} → P y → P (f x y)) →
                     ∀ {e} → P e → ∀ xs → P (foldr f e xs)
  foldr-preservesʳ pres Pe []       = Pe
  foldr-preservesʳ pres Pe (_ ∷ xs) = pres _ (foldr-preservesʳ pres Pe xs)

  foldr-preservesᵒ : (∀ x y → P x ⊎ P y → P (f x y)) →
                     ∀ e xs → P e ⊎ Any P xs → P (foldr f e xs)
  foldr-preservesᵒ pres e []       (inj₁ Pe)          = Pe
  foldr-preservesᵒ pres e (x ∷ xs) (inj₁ Pe)          =
    pres _ _ (inj₂ (foldr-preservesᵒ pres e xs (inj₁ Pe)))
  foldr-preservesᵒ pres e (x ∷ xs) (inj₂ (here px))   = pres _ _ (inj₁ px)
  foldr-preservesᵒ pres e (x ∷ xs) (inj₂ (there pxs)) =
    pres _ _ (inj₂ (foldr-preservesᵒ pres e xs (inj₂ pxs)))

------------------------------------------------------------------------
-- foldl

foldl-++ : ∀ (f : A → B → A) x ys zs →
           foldl f x (ys ++ zs) ≡ foldl f (foldl f x ys) zs
foldl-++ f x []       zs = refl
foldl-++ f x (y ∷ ys) zs = foldl-++ f (f x y) ys zs

foldl-∷ʳ : ∀ (f : A → B → A) x y ys →
           foldl f x (ys ∷ʳ y) ≡ f (foldl f x ys) y
foldl-∷ʳ f x y []       = refl
foldl-∷ʳ f x y (z ∷ ys) = foldl-∷ʳ f (f x z) y ys

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

concat-map : ∀ {f : A → B} → concat ∘ map (map f) ≗ map f ∘ concat
concat-map {f = f} xss = begin
  concat (map (map f) xss)                   ≡⟨ cong concat (map-is-foldr xss) ⟩
  concat (foldr (λ xs → map f xs ∷_) [] xss) ≡⟨ foldr-fusion concat [] (λ _ _ → refl) xss ⟩
  foldr (λ ys → map f ys ++_) [] xss         ≡⟨ sym (foldr-fusion (map f) [] (map-++-commute f) xss) ⟩
  map f (concat xss)                         ∎

------------------------------------------------------------------------
-- sum

sum-++-commute : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys
sum-++-commute []       ys = refl
sum-++-commute (x ∷ xs) ys = begin
  x + sum (xs ++ ys)     ≡⟨ cong (x +_) (sum-++-commute xs ys) ⟩
  x + (sum xs + sum ys)  ≡⟨ sym (+-assoc x _ _) ⟩
  (x + sum xs) + sum ys  ∎

------------------------------------------------------------------------
-- replicate

length-replicate : ∀ n {x : A} → length (replicate n x) ≡ n
length-replicate zero    = refl
length-replicate (suc n) = cong suc (length-replicate n)

------------------------------------------------------------------------
-- scanr

scanr-defn : ∀ (f : A → B → B) (e : B) →
             scanr f e ≗ map (foldr f e) ∘ tails
scanr-defn f e []             = refl
scanr-defn f e (x ∷ [])       = refl
scanr-defn f e (x ∷ y ∷ xs)
  with scanr f e (y ∷ xs) | scanr-defn f e (y ∷ xs)
... | []     | ()
... | z ∷ zs | eq with ∷-injective eq
...   | z≡fy⦇f⦈xs , _ = cong₂ (λ z → f x z ∷_) z≡fy⦇f⦈xs eq

------------------------------------------------------------------------
-- scanl

scanl-defn : ∀ (f : A → B → A) (e : A) →
             scanl f e ≗ map (foldl f e) ∘ inits
scanl-defn f e []       = refl
scanl-defn f e (x ∷ xs) = cong (e ∷_) (begin
   scanl f (f e x) xs
 ≡⟨ scanl-defn f (f e x) xs ⟩
   map (foldl f (f e x)) (inits xs)
 ≡⟨ refl ⟩
   map (foldl f e ∘ (x ∷_)) (inits xs)
 ≡⟨ map-compose (inits xs) ⟩
   map (foldl f e) (map (x ∷_) (inits xs))
 ∎)

------------------------------------------------------------------------
-- applyUpTo

length-applyUpTo : ∀ (f : ℕ → A) n → length (applyUpTo f n) ≡ n
length-applyUpTo f zero    = refl
length-applyUpTo f (suc n) = cong suc (length-applyUpTo (f ∘ suc) n)

lookup-applyUpTo : ∀ (f : ℕ → A) n i → lookup (applyUpTo f n) i ≡ f (toℕ i)
lookup-applyUpTo f (suc n) zero    = refl
lookup-applyUpTo f (suc n) (suc i) = lookup-applyUpTo (f ∘ suc) n i

------------------------------------------------------------------------
-- applyUpTo

module _ (f : ℕ → A) where

  length-applyDownFrom : ∀ n → length (applyDownFrom f n) ≡ n
  length-applyDownFrom zero    = refl
  length-applyDownFrom (suc n) = cong suc (length-applyDownFrom n)

  lookup-applyDownFrom : ∀ n i → lookup (applyDownFrom f n) i ≡ f (n ∸ (suc (toℕ i)))
  lookup-applyDownFrom (suc n) zero    = refl
  lookup-applyDownFrom (suc n) (suc i) = lookup-applyDownFrom n i

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

length-upTo : ∀ n → length (upTo n) ≡ n
length-upTo = length-applyUpTo id

lookup-upTo : ∀ n i → lookup (upTo n) i ≡ toℕ i
lookup-upTo = lookup-applyUpTo id

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

length-downFrom : ∀ n → length (downFrom n) ≡ n
length-downFrom = length-applyDownFrom id

lookup-downFrom : ∀ n i → lookup (downFrom n) i ≡ n ∸ (suc (toℕ i))
lookup-downFrom = lookup-applyDownFrom id

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

tabulate-cong : ∀ {n} {f g : Fin n → A} →
                f ≗ g → tabulate f ≡ tabulate g
tabulate-cong {n = zero}  p = refl
tabulate-cong {n = suc n} p = cong₂ _∷_ (p zero) (tabulate-cong (p ∘ suc))

tabulate-lookup : ∀ (xs : List A) → tabulate (lookup xs) ≡ xs
tabulate-lookup []       = refl
tabulate-lookup (x ∷ xs) = cong (_ ∷_) (tabulate-lookup xs)

length-tabulate : ∀ {n} → (f : Fin n → A) →
                  length (tabulate f) ≡ n
length-tabulate {n = zero} f = refl
length-tabulate {n = suc n} f = cong suc (length-tabulate (λ z → f (suc z)))

lookup-tabulate : ∀ {n} → (f : Fin n → A) →
                  ∀ i → let i′ = cast (sym (length-tabulate f)) i
                        in lookup (tabulate f) i′ ≡ f i
lookup-tabulate f zero    = refl
lookup-tabulate f (suc i) = lookup-tabulate (f ∘ suc) i

map-tabulate : ∀ {n} (g : Fin n → A) (f : A → B) →
               map f (tabulate g) ≡ tabulate (f ∘ g)
map-tabulate {n = zero}  g f = refl
map-tabulate {n = suc n} g f = cong (_ ∷_) (map-tabulate (g ∘ suc) f)

------------------------------------------------------------------------
-- _[_]%=_

length-%= : ∀ xs k (f : A → A) → length (xs [ k ]%= f) ≡ length xs
length-%= (x ∷ xs) zero    f = refl
length-%= (x ∷ xs) (suc k) f = cong suc (length-%= xs k f)

------------------------------------------------------------------------
-- _[_]∷=_

length-∷= : ∀ xs k (v : A) → length (xs [ k ]∷= v) ≡ length xs
length-∷= xs k v = length-%= xs k (const v)

map-∷= : ∀ xs k (v : A) (f : A → B) →
         let eq = sym (length-map f xs) in
         map f (xs [ k ]∷= v) ≡ map f xs [ cast eq k ]∷= f v
map-∷= (x ∷ xs) zero    v f = refl
map-∷= (x ∷ xs) (suc k) v f = cong (f x ∷_) (map-∷= xs k v f)

------------------------------------------------------------------------
-- _─_

length-─ : ∀ (xs : List A) k → length (xs ─ k) ≡ pred (length xs)
length-─ (x ∷ xs) zero        = refl
length-─ (x ∷ y ∷ xs) (suc k) = cong suc (length-─ (y ∷ xs) k)

map-─ : ∀ xs k (f : A → B) →
        let eq = sym (length-map f xs) in
        map f (xs ─ k) ≡ map f xs ─ cast eq k
map-─ (x ∷ xs) zero    f = refl
map-─ (x ∷ xs) (suc k) f = cong (f x ∷_) (map-─ xs k f)

------------------------------------------------------------------------
-- take

length-take : ∀ n (xs : List A) → length (take n xs) ≡ n ⊓ (length xs)
length-take zero    xs       = refl
length-take (suc n) []       = refl
length-take (suc n) (x ∷ xs) = cong suc (length-take n xs)

------------------------------------------------------------------------
-- drop

length-drop : ∀ n (xs : List A) → length (drop n xs) ≡ length xs ∸ n
length-drop zero    xs       = refl
length-drop (suc n) []       = refl
length-drop (suc n) (x ∷ xs) = length-drop n xs

take++drop : ∀ n (xs : List A) → take n xs ++ drop n xs ≡ xs
take++drop zero    xs       = refl
take++drop (suc n) []       = refl
take++drop (suc n) (x ∷ xs) = cong (x ∷_) (take++drop n xs)

------------------------------------------------------------------------
-- splitAt

splitAt-defn : ∀ n → splitAt {A = A} n ≗ < take n , drop n >
splitAt-defn zero    xs       = refl
splitAt-defn (suc n) []       = refl
splitAt-defn (suc n) (x ∷ xs) with splitAt n xs | splitAt-defn n xs
... | (ys , zs) | ih = cong (Prod.map (x ∷_) id) ih

------------------------------------------------------------------------
-- takeWhile, dropWhile, and span

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

  takeWhile++dropWhile : ∀ xs → takeWhile P? xs ++ dropWhile P? xs ≡ xs
  takeWhile++dropWhile []       = refl
  takeWhile++dropWhile (x ∷ xs) with does (P? x)
  ... | true  = cong (x ∷_) (takeWhile++dropWhile xs)
  ... | false = refl

  span-defn : span P? ≗ < takeWhile P? , dropWhile P? >
  span-defn []       = refl
  span-defn (x ∷ xs) with does (P? x)
  ... | true  = cong (Prod.map (x ∷_) id) (span-defn xs)
  ... | false = refl

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

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

  length-filter : ∀ xs → length (filter P? xs) ≤ length xs
  length-filter []       = z≤n
  length-filter (x ∷ xs) with does (P? x)
  ... | false = ≤-step (length-filter xs)
  ... | true  = s≤s (length-filter xs)

  filter-all : ∀ {xs} → All P xs → filter P? xs ≡ xs
  filter-all {[]}     []         = refl
  filter-all {x ∷ xs} (px ∷ pxs) with P? x
  ... | no          ¬px = contradiction px ¬px
  ... | true  because _ = cong (x ∷_) (filter-all pxs)

  filter-notAll : ∀ xs → Any (∁ P) xs → length (filter P? xs) < length xs
  filter-notAll (x ∷ xs) (here ¬px) with P? x
  ... | false because _ = s≤s (length-filter xs)
  ... | yes          px = contradiction px ¬px
  filter-notAll (x ∷ xs) (there any) with does (P? x)
  ... | false = ≤-step (filter-notAll xs any)
  ... | true  = s≤s (filter-notAll xs any)

  filter-some : ∀ {xs} → Any P xs → 0 < length (filter P? xs)
  filter-some {x ∷ xs} (here px)   with P? x
  ... | true because _ = s≤s z≤n
  ... | no         ¬px = contradiction px ¬px
  filter-some {x ∷ xs} (there pxs) with does (P? x)
  ... | true  = ≤-step (filter-some pxs)
  ... | false = filter-some pxs

  filter-none : ∀ {xs} → All (∁ P) xs → filter P? xs ≡ []
  filter-none {[]}     []           = refl
  filter-none {x ∷ xs} (¬px ∷ ¬pxs) with P? x
  ... | false because _ = filter-none ¬pxs
  ... | yes          px = contradiction px ¬px

  filter-complete : ∀ {xs} → length (filter P? xs) ≡ length xs →
                    filter P? xs ≡ xs
  filter-complete {[]}     eq = refl
  filter-complete {x ∷ xs} eq with does (P? x)
  ... | false = contradiction eq (<⇒≢ (s≤s (length-filter xs)))
  ... | true  = cong (x ∷_) (filter-complete (suc-injective eq))

  filter-accept : ∀ {x xs} → P x → filter P? (x ∷ xs) ≡ x ∷ (filter P? xs)
  filter-accept {x} Px with P? x
  ... | true because _ = refl
  ... | no         ¬Px = contradiction Px ¬Px

  filter-reject : ∀ {x xs} → ¬ P x → filter P? (x ∷ xs) ≡ filter P? xs
  filter-reject {x} ¬Px with P? x
  ... | yes          Px = contradiction Px ¬Px
  ... | false because _ = refl

  filter-idem : filter P? ∘ filter P? ≗ filter P?
  filter-idem []       = refl
  filter-idem (x ∷ xs) with does (P? x) | inspect does (P? x)
  ... | false | _                   = filter-idem xs
  ... | true  | P.[ eq ] rewrite eq = cong (x ∷_) (filter-idem xs)

  filter-++ : ∀ xs ys → filter P? (xs ++ ys) ≡ filter P? xs ++ filter P? ys
  filter-++ []       ys = refl
  filter-++ (x ∷ xs) ys with does (P? x)
  ... | true  = cong (x ∷_) (filter-++ xs ys)
  ... | false = filter-++ xs ys

------------------------------------------------------------------------
-- derun and deduplicate

module _ {R : Rel A p} (R? : B.Decidable R) where

  length-derun : ∀ xs → length (derun R? xs) ≤ length xs
  length-derun [] = ≤-refl
  length-derun (x ∷ []) = ≤-refl
  length-derun (x ∷ y ∷ xs) with does (R? x y) | length-derun (y ∷ xs)
  ... | true  | r = ≤-step r
  ... | false | r = s≤s r

  length-deduplicate : ∀ xs → length (deduplicate R? xs) ≤ length xs
  length-deduplicate [] = z≤n
  length-deduplicate (x ∷ xs) = ≤-begin
    1 + length (filter (¬? ∘ R? x) r) ≤⟨ s≤s (length-filter (¬? ∘ R? x) r) ⟩
    1 + length r                      ≤⟨ s≤s (length-deduplicate xs) ⟩
    1 + length xs                     ≤-∎
    where
    open ≤-Reasoning renaming (begin_ to ≤-begin_; _∎ to _≤-∎)
    r = deduplicate R? xs

  derun-reject : ∀ {x y} xs → R x y → derun R? (x ∷ y ∷ xs) ≡ derun R? (y ∷ xs)
  derun-reject {x} {y} xs Rxy with R? x y
  ... | yes _    = refl
  ... | no  ¬Rxy = contradiction Rxy ¬Rxy

  derun-accept : ∀ {x y} xs → ¬ R x y → derun R? (x ∷ y ∷ xs) ≡ x ∷ derun R? (y ∷ xs)
  derun-accept {x} {y} xs ¬Rxy with R? x y
  ... | yes Rxy = contradiction Rxy ¬Rxy
  ... | no  _   = refl

------------------------------------------------------------------------
-- partition

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

  partition-defn : partition P? ≗ < filter P? , filter (∁? P?) >
  partition-defn []       = refl
  partition-defn (x ∷ xs) with does (P? x)
  ...  | true  = cong (Prod.map (x ∷_) id) (partition-defn xs)
  ...  | false = cong (Prod.map id (x ∷_)) (partition-defn xs)

------------------------------------------------------------------------
-- _ʳ++_

ʳ++-defn : ∀ (xs : List A) {ys} → xs ʳ++ ys ≡ reverse xs ++ ys
ʳ++-defn [] = refl
ʳ++-defn (x ∷ xs) {ys} = begin
  (x ∷ xs)             ʳ++ ys   ≡⟨⟩
  xs         ʳ++   x     ∷ ys   ≡⟨⟩
  xs         ʳ++ [ x ]  ++ ys   ≡⟨ ʳ++-defn xs  ⟩
  reverse xs  ++ [ x ]  ++ ys   ≡⟨ sym (++-assoc (reverse xs) _ _) ⟩
  (reverse xs ++ [ x ]) ++ ys   ≡⟨ cong (_++ ys) (sym (ʳ++-defn xs)) ⟩
  (xs ʳ++ [ x ])        ++ ys   ≡⟨⟩
  reverse (x ∷ xs)      ++ ys   ∎

-- Reverse-append of append is reverse-append after reverse-append.

ʳ++-++ : ∀ (xs {ys zs} : List A) → (xs ++ ys) ʳ++ zs ≡ ys ʳ++ xs ʳ++ zs
ʳ++-++ [] = refl
ʳ++-++ (x ∷ xs) {ys} {zs} = begin
  (x ∷ xs ++ ys) ʳ++ zs   ≡⟨⟩
  (xs ++ ys) ʳ++ x ∷ zs   ≡⟨ ʳ++-++ xs ⟩
  ys ʳ++ xs ʳ++ x ∷ zs    ≡⟨⟩
  ys ʳ++ (x ∷ xs) ʳ++ zs  ∎

-- Reverse-append of reverse-append is commuted reverse-append after append.

ʳ++-ʳ++ : ∀ (xs {ys zs} : List A) → (xs ʳ++ ys) ʳ++ zs ≡ ys ʳ++ xs ++ zs
ʳ++-ʳ++ [] = refl
ʳ++-ʳ++ (x ∷ xs) {ys} {zs} = begin
  ((x ∷ xs) ʳ++ ys) ʳ++ zs   ≡⟨⟩
  (xs ʳ++ x ∷ ys) ʳ++ zs     ≡⟨ ʳ++-ʳ++ xs ⟩
  (x ∷ ys) ʳ++ xs ++ zs      ≡⟨⟩
  ys ʳ++ (x ∷ xs) ++ zs      ∎

-- Length of reverse-append

length-ʳ++ : ∀ (xs {ys} : List A) →
             length (xs ʳ++ ys) ≡ length xs + length ys
length-ʳ++ [] = refl
length-ʳ++ (x ∷ xs) {ys} = begin
  length ((x ∷ xs) ʳ++ ys)      ≡⟨⟩
  length (xs ʳ++ x ∷ ys)        ≡⟨ length-ʳ++ xs ⟩
  length xs + length (x ∷ ys)   ≡⟨ +-suc _ _ ⟩
  length (x ∷ xs) + length ys   ∎

-- map distributes over reverse-append.

map-ʳ++ : (f : A → B) (xs {ys} : List A) →
          map f (xs ʳ++ ys) ≡ map f xs ʳ++ map f ys
map-ʳ++ f []            = refl
map-ʳ++ f (x ∷ xs) {ys} = begin
  map f ((x ∷ xs) ʳ++ ys)         ≡⟨⟩
  map f (xs ʳ++ x ∷ ys)           ≡⟨ map-ʳ++ f xs ⟩
  map f xs ʳ++ map f (x ∷ ys)     ≡⟨⟩
  map f xs ʳ++ f x ∷ map f ys     ≡⟨⟩
  (f x ∷ map f xs) ʳ++ map f ys   ≡⟨⟩
  map f (x ∷ xs)   ʳ++ map f ys   ∎

-- A foldr after a reverse is a foldl.

foldr-ʳ++ : ∀ (f : A → B → B) b xs {ys} →
            foldr f b (xs ʳ++ ys) ≡ foldl (flip f) (foldr f b ys) xs
foldr-ʳ++ f b []       {_}  = refl
foldr-ʳ++ f b (x ∷ xs) {ys} = begin
  foldr f b ((x ∷ xs) ʳ++ ys)              ≡⟨⟩
  foldr f b (xs ʳ++ x ∷ ys)                ≡⟨ foldr-ʳ++ f b xs ⟩
  foldl (flip f) (foldr f b (x ∷ ys)) xs   ≡⟨⟩
  foldl (flip f) (f x (foldr f b ys)) xs   ≡⟨⟩
  foldl (flip f) (foldr f b ys) (x ∷ xs)   ∎

-- A foldl after a reverse is a foldr.

foldl-ʳ++ : ∀ (f : B → A → B) b xs {ys} →
            foldl f b (xs ʳ++ ys) ≡ foldl f (foldr (flip f) b xs) ys
foldl-ʳ++ f b []       {_}  = refl
foldl-ʳ++ f b (x ∷ xs) {ys} = begin
  foldl f b ((x ∷ xs) ʳ++ ys)              ≡⟨⟩
  foldl f b (xs ʳ++ x ∷ ys)                ≡⟨ foldl-ʳ++ f b xs ⟩
  foldl f (foldr (flip f) b xs) (x ∷ ys)   ≡⟨⟩
  foldl f (f (foldr (flip f) b xs) x) ys   ≡⟨⟩
  foldl f (foldr (flip f) b (x ∷ xs)) ys   ∎

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

-- reverse of cons is snoc of reverse.

unfold-reverse : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
unfold-reverse x xs = ʳ++-defn xs

-- reverse is an involution with respect to append.

reverse-++-commute : (xs ys : List A) →
                     reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++-commute xs ys = begin
  reverse (xs ++ ys)         ≡⟨⟩
  (xs ++ ys) ʳ++ []          ≡⟨ ʳ++-++ xs ⟩
  ys ʳ++ xs ʳ++ []           ≡⟨⟩
  ys ʳ++ reverse xs          ≡⟨ ʳ++-defn ys ⟩
  reverse ys ++ reverse xs   ∎

-- reverse is involutive.

reverse-involutive : Involutive {A = List A} _≡_ reverse
reverse-involutive xs = begin
  reverse (reverse xs)  ≡⟨⟩
  (xs ʳ++ []) ʳ++ []    ≡⟨ ʳ++-ʳ++ xs ⟩
  [] ʳ++  xs ++ []      ≡⟨⟩
  xs ++ []              ≡⟨ ++-identityʳ xs ⟩
  xs                    ∎

-- reverse preserves length.

length-reverse : ∀ (xs : List A) → length (reverse xs) ≡ length xs
length-reverse xs = begin
  length (reverse xs)   ≡⟨⟩
  length (xs ʳ++ [])    ≡⟨ length-ʳ++ xs ⟩
  length xs + 0         ≡⟨ +-identityʳ _ ⟩
  length xs             ∎

reverse-map-commute : (f : A → B) → map f ∘ reverse ≗ reverse ∘ map f
reverse-map-commute f xs = begin
  map f (reverse xs) ≡⟨⟩
  map f (xs ʳ++ [])  ≡⟨ map-ʳ++ f xs ⟩
  map f xs ʳ++ []    ≡⟨⟩
  reverse (map f xs) ∎

reverse-foldr : ∀ (f : A → B → B) b →
                foldr f b ∘ reverse ≗ foldl (flip f) b
reverse-foldr f b xs = foldr-ʳ++ f b xs

reverse-foldl : ∀ (f : B → A → B) b xs →
                foldl f b (reverse xs) ≡ foldr (flip f) b xs
reverse-foldl f b xs = foldl-ʳ++ f b xs

------------------------------------------------------------------------
-- _∷ʳ_

module _ {x y : A} where

  ∷ʳ-injective : ∀ xs ys → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
  ∷ʳ-injective []          []          refl = (refl , refl)
  ∷ʳ-injective (x ∷ xs)    (y  ∷ ys)   eq   with ∷-injective eq
  ... | refl , eq′ = Prod.map (cong (x ∷_)) id (∷ʳ-injective xs ys eq′)
  ∷ʳ-injective []          (_ ∷ _ ∷ _) ()
  ∷ʳ-injective (_ ∷ _ ∷ _) []          ()

  ∷ʳ-injectiveˡ : ∀ (xs ys : List A) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys
  ∷ʳ-injectiveˡ xs ys eq = proj₁ (∷ʳ-injective xs ys eq)

  ∷ʳ-injectiveʳ : ∀ (xs ys : List A) → xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
  ∷ʳ-injectiveʳ xs ys eq = proj₂ (∷ʳ-injective xs ys eq)

------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

gfilter-just      = mapMaybe-just
{-# WARNING_ON_USAGE gfilter-just
"Warning: gfilter-just was deprecated in v0.15.
Please use mapMaybe-just instead."
#-}
gfilter-nothing   = mapMaybe-nothing
{-# WARNING_ON_USAGE gfilter-nothing
"Warning: gfilter-nothing was deprecated in v0.15.
Please use mapMaybe-nothing instead."
#-}
gfilter-concatMap = mapMaybe-concatMap
{-# WARNING_ON_USAGE gfilter-concatMap
"Warning: gfilter-concatMap was deprecated in v0.15.
Please use mapMaybe-concatMap instead."
#-}
length-gfilter    = length-mapMaybe
{-# WARNING_ON_USAGE length-gfilter
"Warning: length-gfilter was deprecated in v0.15.
Please use length-mapMaybe instead."
#-}
right-identity-unique = ++-identityʳ-unique
{-# WARNING_ON_USAGE right-identity-unique
"Warning: right-identity-unique was deprecated in v0.15.
Please use ++-identityʳ-unique instead."
#-}
left-identity-unique  = ++-identityˡ-unique
{-# WARNING_ON_USAGE left-identity-unique
"Warning: left-identity-unique was deprecated in v0.15.
Please use ++-identityˡ-unique instead."
#-}

-- Version 0.16

module _ (p : A → Bool) where

  boolTakeWhile++boolDropWhile : ∀ xs → boolTakeWhile p xs ++ boolDropWhile p xs ≡ xs
  boolTakeWhile++boolDropWhile []       = refl
  boolTakeWhile++boolDropWhile (x ∷ xs) with p x
  ... | true  = cong (x ∷_) (boolTakeWhile++boolDropWhile xs)
  ... | false = refl
  {-# WARNING_ON_USAGE boolTakeWhile++boolDropWhile
  "Warning: boolTakeWhile and boolDropWhile were deprecated in v0.16.
  Please use takeWhile and dropWhile instead."
  #-}
  boolSpan-defn : boolSpan p ≗ < boolTakeWhile p , boolDropWhile p >
  boolSpan-defn []       = refl
  boolSpan-defn (x ∷ xs) with p x
  ... | true  = cong (Prod.map (x ∷_) id) (boolSpan-defn xs)
  ... | false = refl
  {-# WARNING_ON_USAGE boolSpan-defn
  "Warning: boolSpan, boolTakeWhile and boolDropWhile were deprecated in v0.16.
  Please use span, takeWhile and dropWhile instead."
  #-}
  length-boolFilter : ∀ xs → length (boolFilter p xs) ≤ length xs
  length-boolFilter xs =
    length-mapMaybe (λ x → if p x then just x else nothing) xs
  {-# WARNING_ON_USAGE length-boolFilter
  "Warning: boolFilter was deprecated in v0.16.
  Please use filter instead."
  #-}
  boolPartition-defn : boolPartition p ≗ < boolFilter p , boolFilter (not ∘ p) >
  boolPartition-defn []       = refl
  boolPartition-defn (x ∷ xs) with p x
  ...  | true  = cong (Prod.map (x ∷_) id) (boolPartition-defn xs)
  ...  | false = cong (Prod.map id (x ∷_)) (boolPartition-defn xs)
  {-# WARNING_ON_USAGE boolPartition-defn
  "Warning: boolPartition and boolFilter were deprecated in v0.16.
  Please use partition and filter instead."
  #-}

module _ (P : A → Set p) (P? : Decidable P) where

  boolFilter-filters : ∀ xs → All P (boolFilter (isYes ∘ P?) xs)
  boolFilter-filters []       = []
  boolFilter-filters (x ∷ xs) with P? x
  ... | true  because [px] = invert [px] ∷ boolFilter-filters xs
  ... | false because  _   = boolFilter-filters xs
  {-# WARNING_ON_USAGE boolFilter-filters
  "Warning: boolFilter was deprecated in v0.16.
  Please use filter instead."
  #-}

-- Version 0.17

idIsFold  = id-is-foldr
{-# WARNING_ON_USAGE idIsFold
"Warning: idIsFold was deprecated in v0.17.
Please use id-is-foldr instead."
#-}
++IsFold  = ++-is-foldr
{-# WARNING_ON_USAGE ++IsFold
"Warning: ++IsFold was deprecated in v0.17.
Please use ++-is-foldr instead."
#-}
mapIsFold = map-is-foldr
{-# WARNING_ON_USAGE mapIsFold
"Warning: mapIsFold was deprecated in v0.17.
Please use map-is-foldr instead."
#-}


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

module Cardinality.Finite.ManifestEnumerable.Isomorphism where

open import Prelude

import Cardinality.Finite.ManifestEnumerable.Container as ℒ
import Cardinality.Finite.ManifestEnumerable.Inductive as 𝕃

open import Container.List.Isomorphism
open import Data.Fin
open import HITs.PropositionalTruncation.Sugar
open import Data.List using (_∷_; [])
open import HITs.PropositionalTruncation
open import Cardinality.Finite.SplitEnumerable.Isomorphism
open import Data.Sigma.Properties

𝕃⇔ℒ⟨ℰ⟩ : 𝕃.ℰ A ⇔ ℒ.ℰ A
𝕃⇔ℒ⟨ℰ⟩ .fun (sup , cov) = 𝕃→ℒ sup , cov
𝕃⇔ℒ⟨ℰ⟩ .inv (sup , cov) = ℒ→𝕃 sup , λ x → ∈ℒ⇒∈𝕃 x sup ∥$∥ cov x
𝕃⇔ℒ⟨ℰ⟩ .rightInv (sup , cov) = ΣProp≡ (λ xs x y i t → squash (x t) (y t) i) (𝕃⇔ℒ .rightInv sup)
𝕃⇔ℒ⟨ℰ⟩ .leftInv  (sup , cov) = ΣProp≡ (λ xs x y i t → squash (x t) (y t) i) (𝕃⇔ℒ .leftInv sup)

ext: agda

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
data Tree : Set where
  leaf : Tree
  _∣_ : Tree → Tree → Tree

{-# FOREIGN GHC data Tree = Leaf | Tree :| Tree #-}

{-# COMPILE GHC Tree = data Tree (Leaf | (:|)) #-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Finite sets
------------------------------------------------------------------------

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

module Data.Fin where

open import Relation.Nullary.Decidable.Core
open import Data.Nat.Base using (suc)
import Data.Nat.Properties as ℕₚ

------------------------------------------------------------------------
-- Publicly re-export the contents of the base module

open import Data.Fin.Base public

------------------------------------------------------------------------
-- Publicly re-export queries

open import Data.Fin.Properties public
  using (_≟_; _≤?_; _<?_)

-- # m = "m".

infix 10 #_

#_ : ∀ m {n} {m<n : True (suc m ℕₚ.≤? n)} → Fin n
#_ _ {m<n = m<n} = fromℕ< (toWitness m<n)


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

module Definition.Conversion.Universe where

open import Definition.Untyped hiding (_∷_)
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.RedSteps
open import Definition.Conversion
open import Definition.Conversion.Reduction
open import Definition.Conversion.Lift

open import Tools.Nat
import Tools.PropositionalEquality as PE

private
  variable
    n : Nat
    Γ : Con Term n

-- Algorithmic equality of terms in WHNF of type U are equal as types.
univConv↓ : ∀ {A B}
          → Γ ⊢ A [conv↓] B ∷ U
          → Γ ⊢ A [conv↓] B
univConv↓ (ne-ins t u () x)
univConv↓ (univ x x₁ x₂) = x₂

-- Algorithmic equality of terms of type U are equal as types.
univConv↑ : ∀ {A B}
      → Γ ⊢ A [conv↑] B ∷ U
      → Γ ⊢ A [conv↑] B
univConv↑ ([↑]ₜ B₁ t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u)
      rewrite PE.sym (whnfRed* D Uₙ) =
  reductionConv↑ (univ* d) (univ* d′) (liftConv (univConv↓ t<>u))

max_stars_repo_name: fhlkfy/logrel-mltt

max_issues_repo_name: fhlkfy/logrel-mltt

max_forks_repo_name: fhlkfy/logrel-mltt


text:
------------------------------------------------------------------------
-- Morphisms between algebraic structures
------------------------------------------------------------------------

module Algebra.Morphism where

open import Relation.Binary
open import Algebra
open import Algebra.FunctionProperties
open import Data.Function

------------------------------------------------------------------------
-- Basic definitions

module Definitions (From To : Set) (_≈_ : Rel To) where
  Morphism : Set
  Morphism = From → To

  Homomorphic₀ : Morphism → From → To → Set
  Homomorphic₀ ⟦_⟧ ∙ ∘ = ⟦ ∙ ⟧ ≈ ∘

  Homomorphic₁ : Morphism → Fun₁ From → Op₁ To → Set
  Homomorphic₁ ⟦_⟧ ∙_ ∘_ = ∀ x → ⟦ ∙ x ⟧ ≈ ∘ ⟦ x ⟧

  Homomorphic₂ : Morphism → Fun₂ From → Op₂ To → Set
  Homomorphic₂ ⟦_⟧ _∙_ _∘_ =
    ∀ x y → ⟦ x ∙ y ⟧ ≈ (⟦ x ⟧ ∘ ⟦ y ⟧)

------------------------------------------------------------------------
-- Some specific morphisms

-- Other morphisms could of course be defined.

record _-RawRing⟶_ (From To : RawRing) : Set where
  open RawRing
  open Definitions (carrier From) (carrier To) (_≈_ To)
  field
    ⟦_⟧    : Morphism
    +-homo : Homomorphic₂ ⟦_⟧ (_+_ From) (_+_ To)
    *-homo : Homomorphic₂ ⟦_⟧ (_*_ From) (_*_ To)
    -‿homo : Homomorphic₁ ⟦_⟧ (-_  From) (-_  To)
    0-homo : Homomorphic₀ ⟦_⟧ (0#  From) (0#  To)
    1-homo : Homomorphic₀ ⟦_⟧ (1#  From) (1#  To)

_-Ring⟶_ : Ring → Ring → Set
From -Ring⟶ To = rawRing From -RawRing⟶ rawRing To
  where open Ring

max_issues_repo_name: larrytheliquid/Lemmachine


text:
{-# OPTIONS --type-in-type #-}  -- yes, there will be some cheating in this lecture

module Lec3Done where

open import Lec1Done
open import Lec2Done

postulate
  extensionality : {S : Set}{T : S -> Set}
                   {f g : (x : S) -> T x} ->
                   ((x : S) -> f x == g x) ->
                   f == g

imp : {S : Set}{T : S -> Set}(f : (x : S) -> T x){x : S} -> T x
imp f {x} = f x

extensionality' : {S : Set}{T : S -> Set}
                   {f g : {x : S} -> T x} ->
                   ((x : S) -> f {x} == g {x}) ->
                   _==_ {forall {x : S} -> T x} f g
extensionality' {f = f}{g = g} q =
  refl imp =$= extensionality {f = \ x -> f {x}}{g = \ x -> g {x}}
    q

_[QED] : {X : Set}(x : X) -> x == x
x [QED] = refl x
_=[_>=_ : {X : Set}(x : X){y z : X} -> x == y -> y == z -> x == z
x =[ refl .x >= q = q
_=<_]=_ : {X : Set}(x : X){y z : X} -> y == x -> y == z -> x == z
x =< refl .x ]= q = q
infixr 1 _=[_>=_ _=<_]=_
infixr 2 _[QED]

record Category : Set where
  field

    -- two types of thing
    Obj  : Set                  -- "objects"
    _~>_ : Obj -> Obj -> Set    -- "arrows" or "morphisms"
                                -- or "homomorphisms"

    -- two operations
    id~>        : {T : Obj} ->      T ~> T
    _>~>_       : {R S T : Obj} ->  R ~> S  ->  S ~> T  ->  R ~> T

    -- three laws
    law-id~>>~> : {S T : Obj}     (f : S ~> T) ->
                    (id~> >~> f) == f
    law->~>id~> : {S T : Obj}     (f : S ~> T) ->
                    (f >~> id~>) == f
    law->~>>~>  : {Q R S T : Obj} (f : Q ~> R)(g : R ~> S)(h : S ~> T) ->
                    ((f >~> g) >~> h) == (f >~> (g >~> h))

  assocn : {Q R R' S T : Obj}
            {f  : Q ~> R} {g : R ~> S}
            {f' : Q ~> R'}{g' : R' ~> S}
            {h : S ~> T} ->
            (f >~> g) == (f' >~> g') ->
            (f >~> g >~> h) == (f' >~> g' >~> h)
  assocn {f = f} {g = g} {f' = f'} {g' = g'} {h = h} q =
    f >~> g >~> h
      =< law->~>>~> _ _ _ ]=
    (f >~> g) >~> h
      =[ refl _>~>_ =$= q =$= refl h >=
    (f' >~> g') >~> h
      =[ law->~>>~> _ _ _ >=
    f' >~> g' >~> h
      [QED]

  infixr 3 _>~>_

-- Sets and functions are the classic example of a category.
SET : Category
SET = record
        { Obj         = Set
        ; _~>_        = \ S T -> S -> T
        ; id~>        = id
        ; _>~>_       = _>>_
        ; law-id~>>~> = \ f -> refl f
        ; law->~>id~> = \ f -> refl f
        ; law->~>>~>  = \ f g h -> refl (f >> (g >> h))
        }

-- A PREORDER is a category where there is at most one arrow between
-- any two objects. (So arrows are unique.)
NAT->= : Category
unique->= : (m n : Nat)(p q : m >= n) -> p == q
unique->= m zero p q = refl <>
unique->= zero (suc n) () q
unique->= (suc m) (suc n) p q = unique->= m n p q

NAT->= = record
           { Obj         = Nat
           ; _~>_        = _>=_
           ; id~>        = \ {n} -> refl->= n
           ; _>~>_       = \ {m}{n}{p} m>=n n>=p -> trans->= m n p m>=n n>=p
           ; law-id~>>~> = \ {m}{n} m>=n -> unique->= m n _ _
           ; law->~>id~> = \ {m}{n} m>=n -> unique->= m n _ _
           ; law->~>>~>  = \ {m}{n}{p}{q} m>n n>=p p>=q -> unique->= m q _ _
           } where

-- A MONOID is a category with Obj = One.
-- The values in the monoid are the *arrows*.
ONE-Nat : Category
ONE-Nat = record
            { Obj         = One
            ; _~>_        = \ _ _ -> Nat
            ; id~>        = 0
            ; _>~>_       = _+N_
            ; law-id~>>~> = \ n -> zero-+N n
            ; law->~>id~> = \ n -> +N-zero n
            ; law->~>>~>  = \ m n p -> assocLR-+N m n p
            }

eqUnique : {X : Set}{x y : X}(p q : x == y) -> p == q
eqUnique (refl x) (refl .x) = refl (refl x)

-- A DISCRETE category is one where the only arrows are the identities.
DISCRETE : (X : Set) -> Category
DISCRETE X = record
               { Obj         = X
               ; _~>_        = _==_
               ; id~>        = refl _
               ; _>~>_       = \ { {x} (refl .x) (refl .x) -> refl x }
               ; law-id~>>~> = \ _ -> eqUnique _ _
               ; law->~>id~> = \ _ -> eqUnique _ _
               ; law->~>>~>  = \ _ _ _ -> eqUnique _ _
               }

module FUNCTOR where
  open Category

  record _=>_ (C D : Category) : Set where  -- "Functor from C to D"
    field
      -- two actions
      F-Obj : Obj C -> Obj D
      F-map : {S T : Obj C} -> _~>_ C S T -> _~>_ D (F-Obj S) (F-Obj T)

      -- two laws
      F-map-id~> : {T : Obj C} -> F-map (id~> C {T}) == id~> D {F-Obj T}
      F-map->~>  : {R S T : Obj C}(f : _~>_ C R S)(g : _~>_ C S T) ->
                     F-map (_>~>_ C f g) == _>~>_ D (F-map f) (F-map g)

open FUNCTOR public

postulate homework : {A : Set} -> A

VEC : Nat -> SET => SET
VEC n = record
  { F-Obj       = \ X -> Vec X n
  ; F-map       = homework
  ; F-map-id~>  = homework
  ; F-map->~>   = homework
  }

VTAKE : Set -> NAT->= => SET
VTAKE X = record
  { F-Obj      = Vec X
  ; F-map      = \ {m}{n} m>=n xs -> vTake m n m>=n xs
  ; F-map-id~> = \ {n} -> extensionality \ xs -> vTakeIdFact n xs
  ; F-map->~>  = \ {m}{n}{p} m>=n n>=p -> extensionality \ xs ->
     vTakeCpFact m n p m>=n n>=p xs
  }

ADD : Nat -> NAT->= => NAT->=
ADD d = record { F-Obj = (d +N_)
               ; F-map = \ {m}{n} -> help d m n
               ; F-map-id~> = \ {n} -> unique->= (d +N n) (d +N n) _ _
               ; F-map->~> = \ {m}{n}{p} x y ->
                  unique->= (d +N m) (d +N p) _ _
               } where
  help : (d m n : Nat) -> m >= n -> (d +N m) >= (d +N n)
  help zero m n m>=n = m>=n
  help (suc d) m n m>=n = help d m n m>=n

Thing : {C D : Category}(F G : C => D) -> Set
Thing {C}{D}
      (record { F-Obj = F-Obj ; F-map = F-map
              ; F-map-id~> = F-map-id~> ; F-map->~> = F-map->~> })
      (record { F-Obj = G-Obj ; F-map = G-map
              ; F-map-id~> = G-map-id~> ; F-map->~> = G-map->~> })
  = Sg (F-Obj == G-Obj)
     \ { (refl _) ->
    Sg (_==_ {forall {S T : Category.Obj C} →
          (C Category.~> S) T → (D Category.~> F-Obj S) (F-Obj T)}
          F-map  G-map)
     \ { (refl _) ->
       _==_ {forall {T : Category.Obj C} →
      F-map (Category.id~> C {T}) == Category.id~> D} F-map-id~> G-map-id~>
       *
       _==_ {forall {R S T : Category.Obj C} (f : (C Category.~> R) S)
      (g : (C Category.~> S) T) →
      F-map ((C Category.>~> f) g) == (D Category.>~> F-map f) (F-map g)}
        F-map->~>  G-map->~>
     }}

Lemma : {C D : Category}{F G : C => D} -> Thing F G -> F == G
Lemma (refl _ , (refl _ , (refl _ , refl _))) = refl _

CATEGORY : Category
CATEGORY = record
             { Obj = Category
             ; _~>_ = _=>_
             ; id~> = record { F-Obj = \ X -> X
                             ; F-map = \ a -> a
                             ; F-map-id~> = refl _
                             ; F-map->~> = \ _ _ -> refl _ }
             ; _>~>_ = \ {R}{S}{T} F G -> record
               { F-Obj = F-Obj F >> F-Obj G
               ; F-map = F-map F >> F-map G
               ; F-map-id~> = F-map G (F-map F (Category.id~> R))
                                =[ refl (F-map G) =$= F-map-id~> F >=
                              F-map G (Category.id~> S)
                                =[ F-map-id~> G >=
                              Category.id~> T
                                [QED]
               ; F-map->~> = \ f g ->
                   F-map G (F-map F (Category._>~>_ R f g))
                     =[ refl (F-map G) =$= F-map->~> F f g >=
                   F-map G (Category._>~>_ S (F-map F f) (F-map F g))
                     =[ F-map->~> G (F-map F f) (F-map F g) >=
                   Category._>~>_ T (F-map G (F-map F f))
                                    (F-map G (F-map F g))
                     [QED]
               }
             ; law-id~>>~> = \ F -> Lemma
                 ((refl _) , ((refl _) ,
                    (extensionality' (\ x -> eqUnique _ _) ,
                    extensionality' (\ x ->
                      extensionality' \ y -> extensionality' \ z ->
                        extensionality \ f -> extensionality \ g ->
                          eqUnique _ _))))
             ; law->~>id~> = \ F -> Lemma
                 ((refl _) , ((refl _) ,
                    (extensionality' (\ x -> eqUnique _ _) ,
                    extensionality' (\ x ->
                      extensionality' \ y -> extensionality' \ z ->
                        extensionality \ f -> extensionality \ g ->
                          eqUnique _ _))))
             ; law->~>>~> = \ F G H ->  Lemma
                 ((refl _) , ((refl _) ,
                    (extensionality' (\ x -> eqUnique _ _) ,
                    extensionality' (\ x ->
                      extensionality' \ y -> extensionality' \ z ->
                        extensionality \ f -> extensionality \ g ->
                          eqUnique _ _))))
             } where
             open _=>_

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommAlgebra.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Reflection.StrictEquiv

open import Cubical.Structures.Axioms
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Algebra
open import Cubical.Algebra.CommAlgebra.Base

private
  variable
    ℓ ℓ′ : Level

-- An R-algebra is the same as a CommRing A with a CommRingHom φ : R → A
module CommAlgChar (R : CommRing ℓ) where
 open Iso
 open IsRingHom
 open CommRingTheory

 CommRingWithHom : Type (ℓ-suc ℓ)
 CommRingWithHom = Σ[ A ∈ CommRing ℓ ] CommRingHom R A

 toCommAlg : CommRingWithHom → CommAlgebra R ℓ
 toCommAlg (A , φ , φIsHom) = ⟨ A ⟩ , ACommAlgStr
  where
  open CommRingStr (snd A)
  ACommAlgStr : CommAlgebraStr R ⟨ A ⟩
  CommAlgebraStr.0a ACommAlgStr = 0r
  CommAlgebraStr.1a ACommAlgStr = 1r
  CommAlgebraStr._+_ ACommAlgStr = _+_
  CommAlgebraStr._·_ ACommAlgStr = _·_
  CommAlgebraStr.- ACommAlgStr = -_
  CommAlgebraStr._⋆_ ACommAlgStr r a = (φ r) · a
  CommAlgebraStr.isCommAlgebra ACommAlgStr = makeIsCommAlgebra
   is-set +Assoc +Rid +Rinv +Comm ·Assoc ·Lid ·Ldist+ ·Comm
   (λ _ _ x → cong (λ y →  y · x) (pres· φIsHom _ _) ∙ sym (·Assoc _ _ _))
   (λ _ _ x → cong (λ y → y · x) (pres+ φIsHom _ _) ∙ ·Ldist+ _ _ _)
   (λ _ _ _ → ·Rdist+ _ _ _)
   (λ x → cong (λ y → y · x) (pres1 φIsHom) ∙ ·Lid x)
   (λ _ _ _ → sym (·Assoc _ _ _))

 fromCommAlg : CommAlgebra R ℓ → CommRingWithHom
 fromCommAlg A = (CommAlgebra→CommRing A) , φ , φIsHom
  where
  open CommRingStr (snd R) renaming (_·_ to _·r_) hiding (·Lid)
  open CommAlgebraStr (snd A)
  open AlgebraTheory (CommRing→Ring R) (CommAlgebra→Algebra A)
  φ : ⟨ R ⟩ → ⟨ A ⟩
  φ r = r ⋆ 1a
  φIsHom : IsRingHom (CommRing→Ring R .snd) φ (CommRing→Ring (CommAlgebra→CommRing A) .snd)
  φIsHom = makeIsRingHom (⋆-lid _) (λ _ _ → ⋆-ldist _ _ _)
           λ x y → cong (λ a → (x ·r y) ⋆ a) (sym (·Lid _)) ∙ ⋆Dist· _ _ _ _

 CommRingWithHomRoundTrip : (Aφ : CommRingWithHom) → fromCommAlg (toCommAlg Aφ) ≡ Aφ
 CommRingWithHomRoundTrip (A , φ) = ΣPathP (APath , φPathP)
  where
  open CommRingStr
  -- note that the proofs of the axioms might differ!
  APath : fst (fromCommAlg (toCommAlg (A , φ))) ≡ A
  fst (APath i) = ⟨ A ⟩
  0r (snd (APath i)) = 0r (snd A)
  1r (snd (APath i)) = 1r (snd A)
  _+_ (snd (APath i)) = _+_ (snd A)
  _·_ (snd (APath i)) = _·_ (snd A)
  -_ (snd (APath i)) = -_ (snd A)
  isCommRing (snd (APath i)) = isProp→PathP (λ i → isPropIsCommRing _ _ _ _ _ )
             (isCommRing (snd (fst (fromCommAlg (toCommAlg (A , φ)))))) (isCommRing (snd A)) i

  -- this only works because fst (APath i) = fst A definitionally!
  φPathP : PathP (λ i → CommRingHom R (APath i)) (snd (fromCommAlg (toCommAlg (A , φ)))) φ
  φPathP = RingHomPathP _ _ _ _ _ _ λ i x → ·Rid (snd A) (fst φ x) i

 CommAlgRoundTrip : (A : CommAlgebra R ℓ) → toCommAlg (fromCommAlg A) ≡ A
 CommAlgRoundTrip A = ΣPathP (refl , AlgStrPathP)
  where
  open CommAlgebraStr ⦃...⦄
  instance
   _ = snd A
  AlgStrPathP : PathP (λ i → CommAlgebraStr R ⟨ A ⟩) (snd (toCommAlg (fromCommAlg A))) (snd A)
  CommAlgebraStr.0a (AlgStrPathP i) = 0a
  CommAlgebraStr.1a (AlgStrPathP i) = 1a
  CommAlgebraStr._+_ (AlgStrPathP i) = _+_
  CommAlgebraStr._·_ (AlgStrPathP i) = _·_
  CommAlgebraStr.-_ (AlgStrPathP i) = -_
  CommAlgebraStr._⋆_ (AlgStrPathP i) r x = (⋆-lassoc r 1a x ∙ cong (r ⋆_) (·Lid x)) i
  CommAlgebraStr.isCommAlgebra (AlgStrPathP i) = isProp→PathP
    (λ i → isPropIsCommAlgebra _ _ _ _ _ _ (CommAlgebraStr._⋆_ (AlgStrPathP i)))
    (CommAlgebraStr.isCommAlgebra (snd (toCommAlg (fromCommAlg A)))) isCommAlgebra i

 CommAlgIso : Iso (CommAlgebra R ℓ) CommRingWithHom
 fun CommAlgIso = fromCommAlg
 inv CommAlgIso = toCommAlg
 rightInv CommAlgIso = CommRingWithHomRoundTrip
 leftInv CommAlgIso = CommAlgRoundTrip


text:
module Krivine (Atom Const : Set) where

open import Data.Nat
open import Data.Sum
open import Data.Vec as Vec using (Vec; _∷_; [])

data Type : Set where
  atom : Atom → Type
  _⇒_  : Type → Type → Type

Basis : ℕ → Set
Basis = Vec Type

data Var : ∀ {n} → Basis n → Type → Set where
  vzero : ∀ {n} {Γ : Basis n} {τ}   → Var (τ ∷ Γ) τ
  vsuc  : ∀ {n} {Γ : Basis n} {σ τ} → Var Γ τ → Var (σ ∷ Γ) τ

data Term (Σ : Const → Type) {n} (Γ : Basis n) : Type → Set where
  app : ∀ {σ τ} → Term Σ Γ (σ ⇒ τ) → Term Σ Γ σ → Term Σ Γ τ
  lam : ∀ {σ τ} → Term Σ (σ ∷ Γ) τ → Term Σ Γ (σ ⇒ τ)
  var : ∀ {τ}   → Var Γ τ → Term Σ Γ τ

mutual
  data Subst (A : ∀ {n} (Γ : Basis n) → Type → Set) : ∀ {n₁} (Γ₁ : Basis n₁) {n₂} (Γ₂ : Basis n₂) → Set where
    comp  : ∀ {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} {n₃} {Γ₃ : Basis n₃} → Subst A Γ₁ Γ₂ → Subst A Γ₂ Γ₃ → Subst A Γ₁ Γ₃
    cons  : ∀ {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} {τ}                  → A Γ₂ τ → Subst A Γ₁ Γ₂ → Subst A (τ ∷ Γ₁) Γ₂
    id    : ∀ {n} {Γ : Basis n}                                              → Subst A Γ Γ
    lift  : ∀ {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} {τ}                  → Subst A Γ₁ Γ₂ → Subst A (τ ∷ Γ₁) (τ ∷ Γ₂)
    shift : ∀ {n} {Γ : Basis n} {τ}                                          → Subst A Γ (τ ∷ Γ)

  data Thunk (A : ∀ {n} (Γ : Basis n) → Type → Set) {n} (Γ : Basis n) τ : Set where
    thunk : ∀ {n'} {Γ' : Basis n'} → A Γ' τ → Subst (Thunk A) Γ' Γ → Thunk A Γ τ

lookup : ∀ {A : ∀ {n} (Γ : Basis n) → Type → Set} → (∀ {n} {Γ : Basis n} {σ} → Var Γ σ → Thunk A Γ σ) → (∀ {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} {τ}
       → Thunk A Γ₁ τ → Subst (Thunk A) Γ₁ Γ₂ → Thunk A Γ₂ τ) → ∀ {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} {τ} → Var Γ₁ τ → Subst (Thunk A) Γ₁ Γ₂ → Thunk A Γ₂ τ
lookup {A} box under = lookup'
  where
    lookup' : ∀ {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} {τ} → Var Γ₁ τ → Subst (Thunk A) Γ₁ Γ₂ → Thunk A Γ₂ τ
    lookup' v        (comp ρ σ) = under (lookup' v ρ) σ
    lookup' vzero    (cons x _) = x
    lookup' (vsuc v) (cons _ σ) = lookup' v σ
    lookup' v        id         = box v
    lookup' vzero    (lift _)   = box vzero
    lookup' (vsuc v) (lift σ)   = under (lookup' v σ) shift
    lookup' v        shift      = box (vsuc v)

boxvar : ∀ {Σ : Const → Type} {n} {Γ : Basis n} {τ} → Var Γ τ → Thunk (Term Σ) Γ τ
boxvar v = thunk (var v) id

close : ∀ {Σ : Const → Type} {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} {τ} → Thunk (Term Σ) Γ₁ τ → Subst (Thunk (Term Σ)) Γ₁ Γ₂ → Thunk (Term Σ) Γ₂ τ
close (thunk t ρ) σ = thunk t (comp ρ σ)

mutual
  subst : ∀ {Σ : Const → Type} {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} {τ} → Term Σ Γ₁ τ → Subst (Thunk (Term Σ)) Γ₁ Γ₂ → Term Σ Γ₂ τ
  subst (app s t) σ  = app (subst s σ) (subst t σ)
  subst (lam t)   σ  = lam (subst t (lift σ))
  subst (var v)   id = var v
  subst (var v)   σ  = force (lookup boxvar close v σ)

  force : ∀ {Σ : Const → Type} {n} {Γ : Basis n} {τ} → Thunk (Term Σ) Γ τ → Term Σ Γ τ
  force (thunk t ρ) = subst t ρ

data Context (A : ∀ {n} (Γ : Basis n) → Type → Set) : ∀ {n₁} (Γ₁ : Basis n₁) {n₂} (Γ₂ : Basis n₂) → Type → Type → Set where
  app₁ : ∀ {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} {ρ σ τ} → Context A Γ₁ Γ₂ σ τ → A Γ₁ ρ → Context A Γ₁ Γ₂ (ρ ⇒ σ) τ
  app₂ : ∀ {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} {ρ σ τ} → A Γ₁ (ρ ⇒ σ) → Context A Γ₁ Γ₂ σ τ → Context A Γ₁ Γ₂ ρ τ
  lam₁ : ∀ {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} {ρ σ τ} → Context A Γ₁ Γ₂ (ρ ⇒ σ) τ → Context A (ρ ∷ Γ₁) Γ₂ σ τ
  top  : ∀ {n} {Γ : Basis n} {τ}                             → Context A Γ Γ τ τ

foldctx : ∀ {A : ∀ {n} (Γ : Basis n) → Type → Set} {Σ : Const → Type} {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} {σ τ}
        → (∀ {n} {Γ : Basis n} {ρ} → A Γ ρ → Term Σ Γ ρ) → Term Σ Γ₁ σ → Context A Γ₁ Γ₂ σ τ → Term Σ Γ₂ τ
foldctx f z (app₁ ctx y) = foldctx f (app z (f y)) ctx
foldctx f z (app₂ x ctx) = foldctx f (app (f x) z) ctx
foldctx f z (lam₁ ctx)   = foldctx f (lam z)       ctx
foldctx _ z top          = z

data Head (Σ : Const → Type) {n} (Γ : Basis n) : Type → Set where
  var : ∀ {τ} → Var Γ τ → Head Σ Γ τ

data Spine (Σ : Const → Type) (A : (∀ {n} (Γ : Basis n) → Type → Set) → ∀ {n} (Γ : Basis n) → Type → Set) {n} (Γ : Basis n) τ : Set where
  spine : ∀ {n'} {Γ' : Basis n'} {σ} → Head Σ Γ' σ → Context (A (Term Σ)) Γ' Γ σ τ → Spine Σ A Γ τ

eval : ∀ {Σ : Const → Type} {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} {σ τ} → Thunk (Term Σ) Γ₁ σ → Context (Thunk (Term Σ)) Γ₁ Γ₂ σ τ → Spine Σ Thunk Γ₂ τ
eval (thunk (app s t) σ)  ctx         = eval (thunk s σ) (app₁ ctx (thunk t σ))
eval (thunk (lam t)   σ) (app₁ ctx x) = eval (thunk t (cons x σ)) ctx
eval (thunk (lam t)   σ)  ctx         = eval (thunk t (lift σ)) (lam₁ ctx)
eval (thunk (var v)   id) ctx         = spine (var v) ctx
eval (thunk (var v)   σ)  ctx         = eval (lookup boxvar close v σ) ctx

data Subst' (A : ∀ {n} (Γ : Basis n) → Type → Set) : ∀ {n₁} (Γ₁ : Basis n₁) {n₂} (Γ₂ : Basis n₂) → Set where
  comp  : ∀ {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} {n₃} {Γ₃ : Basis n₃} → Subst A Γ₁ Γ₂ → Subst' A Γ₂ Γ₃ → Subst' A Γ₁ Γ₃
  id    : ∀ {n} {Γ : Basis n}                                              → Subst' A Γ Γ

data Thunk' (A : ∀ {n} (Γ : Basis n) → Type → Set) {n} (Γ : Basis n) τ : Set where
  thunk : ∀ {n'} {Γ' : Basis n'} → A Γ' τ → Subst' (Thunk' A) Γ' Γ → Thunk' A Γ τ

data Machine (Σ : Const → Type) {n} (Γ : Basis n) τ : Set where
  machine : ∀ {n'} {Γ' : Basis n'} {σ} → Thunk' (Term Σ) Γ' σ → Context (Thunk' (Term Σ)) Γ' Γ σ τ → Machine Σ Γ τ

coerce : ∀ {A : ∀ {n} (Γ : Basis n) → Type → Set} {n₁} {Γ₁ : Basis n₁} {n₂} {Γ₂ : Basis n₂} → Subst' A Γ₁ Γ₂ → Subst A Γ₁ Γ₂
coerce (comp ρ σ) = comp ρ (coerce σ)
coerce id         = id

step : ∀ {Σ : Const → Type} {n} {Γ : Basis n} {τ} → Machine Σ Γ τ → Spine Σ Thunk' Γ τ ⊎ Machine Σ Γ τ
step (machine (thunk (var v)         (comp shift                σ)) ctx) = inj₂ (machine (thunk (var (vsuc v)) σ)                                    ctx)
step (machine (thunk (var vzero)     (comp (cons (thunk u π) _) σ)) ctx) = inj₂ (machine (thunk u              (comp (coerce π) σ))                  ctx)
step (machine (thunk (var vzero)     (comp (lift _)             σ)) ctx) = inj₂ (machine (thunk (var vzero)    σ)                                    ctx)
step (machine (thunk (var (vsuc v))  (comp (cons (thunk _ _) ρ) σ)) ctx) = inj₂ (machine (thunk (var v)        (comp ρ          σ))                  ctx)
step (machine (thunk (var (vsuc v))  (comp (lift ρ)             σ)) ctx) = inj₂ (machine (thunk (var v)        (comp ρ (comp shift σ)))              ctx)
step (machine (thunk t               (comp (comp π ρ)           σ)) ctx) = inj₂ (machine (thunk t              (comp π (comp ρ σ)))                  ctx)
step (machine (thunk t               (comp id                   σ)) ctx) = inj₂ (machine (thunk t              σ)                                    ctx)
step (machine (thunk t               σ)          (app₂ (thunk s ρ) ctx)) = inj₂ (machine (thunk s              ρ)                 (app₁ ctx (thunk t σ)))
step (machine (thunk (app s (var v)) σ)                             ctx) = inj₂ (machine (thunk (var v)        σ)                 (app₂ (thunk s σ) ctx))
step (machine (thunk (app s t)       σ)                             ctx) = inj₂ (machine (thunk s              σ)                 (app₁ ctx (thunk t σ)))
step (machine (thunk (lam t)         σ)                    (app₁ ctx x)) = inj₂ (machine (thunk t              (comp (cons x (coerce σ)) id))        ctx)
step (machine (thunk (lam t)         σ)                             ctx) = inj₂ (machine (thunk t              (comp (lift (coerce σ)) id))   (lam₁ ctx))
step (machine (thunk (var v)         id)                            ctx) = inj₁ (spine (var v) ctx)

reduce : ∀ {Σ : Const → Type} {n} {Γ : Basis n} {τ} → Machine Σ Γ τ → Spine Σ Thunk' Γ τ
reduce m with step m
...      | inj₁ x  = x
...      | inj₂ m' = reduce m'

max_stars_repo_name: cls/strong-krivine

max_issues_repo_name: cls/strong-krivine

max_forks_repo_name: cls/strong-krivine


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import Sets.EquivalenceRelations
open import Functions.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_; Setω)
open import Setoids.Setoids
open import Groups.Definition
open import LogicalFormulae
open import Orders.WellFounded.Definition
open import Numbers.Naturals.Semiring
open import Groups.Lemmas

module Groups.FreeProduct.Definition {i : _} {I : Set i} (decidableIndex : (x y : I) → ((x ≡ y) || ((x ≡ y) → False))) {a b : _} {A : I → Set a} {S : (i : I) → Setoid {a} {b} (A i)} {_+_ : (i : I) → (A i) → (A i) → A i} (decidableGroups : (i : I) → (x y : A i) → ((Setoid._∼_ (S i) x y)) || ((Setoid._∼_ (S i) x y) → False)) (G : (i : I) → Group (S i) (_+_ i)) where

data ReducedSequenceBeginningWith : I → Set (a ⊔ b ⊔ i) where
  ofEmpty : (i : I) → (g : A i) → .(nonZero : (Setoid._∼_ (S i) g (Group.0G (G i))) → False) → ReducedSequenceBeginningWith i
  prependLetter : (i : I) → (g : A i) → .(nonZero : Setoid._∼_ (S i) g (Group.0G (G i)) → False) → {j : I} → ReducedSequenceBeginningWith j → ((i ≡ j) → False) → ReducedSequenceBeginningWith i

data ReducedSequence : Set (a ⊔ b ⊔ i) where
  empty : ReducedSequence
  nonempty : (i : I) → ReducedSequenceBeginningWith i → ReducedSequence

injection : {i : I} (x : A i) .(nonzero : (Setoid._∼_ (S i) x (Group.0G (G i))) → False) → ReducedSequence
injection {i} x nonzero = nonempty i (ofEmpty i x nonzero)


text:
open import Data.Product using ( _,_ )
open import Web.Semantic.DL.ABox using ( ε )
open import Web.Semantic.DL.Category.Object using ( Object ; _,_ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.Util using ( False ; False∈Fin )

module Web.Semantic.DL.Category.Unit {Σ : Signature} where

I : ∀ {S T : TBox Σ} → Object S T
I = (False , False∈Fin , ε)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
-- Andreas, 2016-07-29 issue #707, comment of 2012-10-31

data Bool : Set where true false : Bool

mutual

  data D : Bool → Set where
    c d : D ?

  fixIx : (b : Bool) → D b → D b
  fixIx true  c = c
  fixIx false d = d

-- Works, but maybe questionable.
-- The _ is duplicated into two different internal metas.

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


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

module TypeTheory.HoTT.Relation.Nullary.Negation.Properties where

-- agda-stdlib
open import Axiom.Extensionality.Propositional
open import Level renaming (zero to lzero)
open import Relation.Nullary

-- agda-misc
open import TypeTheory.HoTT.Base
open import TypeTheory.HoTT.Data.Empty.Properties
open import TypeTheory.HoTT.Function.Properties

private
  variable
    a b : Level
    A : Set a
    B : Set b

module _ {a} {A : Set a} where
  isProp-¬ : Extensionality a lzero → isProp (¬ A)
  isProp-¬ ext = isProp-→ ext isProp-⊥


text:
module Function.Inverse where

open import Data.Tuple as Tuple using (_⨯_ ; _,_)
import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Functional
open import Function.Equals
open import Function.Equals.Proofs
open import Function.Inverseₗ
open import Function.Inverseᵣ
open import Structure.Setoid
open import Structure.Setoid.Uniqueness
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Function.Domain.Proofs
open import Structure.Operator
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type

module _ {ℓ₁ ℓ₂ ℓₑ₁ ℓₑ₂} {A : Type{ℓ₁}} ⦃ eqA : Equiv{ℓₑ₁}(A) ⦄ {B : Type{ℓ₂}} ⦃ eqB : Equiv{ℓₑ₂}(B) ⦄ where
  private variable f : A → B

  -- The inverse function of a bijective function f.
  inv : (f : A → B) → ⦃ inver : Invertible(f) ⦄ → (B → A)
  inv(f) ⦃ inver ⦄ = [∃]-witness inver

  module _ {f : A → B} ⦃ inver : Invertible(f) ⦄ where
    inv-inverse : Inverse(f)(inv f)
    inv-inverse = [∧]-elimᵣ([∃]-proof inver)

    inv-inverseₗ : Inverseₗ(f)(inv f)
    inv-inverseₗ = [∧]-elimₗ inv-inverse

    inv-inverseᵣ : Inverseᵣ(f)(inv f)
    inv-inverseᵣ = [∧]-elimᵣ inv-inverse

    inv-function : Function(inv f)
    inv-function = [∧]-elimₗ([∃]-proof inver)

    inv-surjective : Surjective(inv f)
    inv-surjective = inverse-surjective ⦃ inver = [∧]-elimᵣ([∃]-proof inver) ⦄

    module _ ⦃ func : Function(f) ⦄ where
      inv-injective : Injective(inv f)
      inv-injective = inverse-injective ⦃ inver = [∧]-elimᵣ([∃]-proof inver) ⦄

      inv-bijective : Bijective(inv f)
      inv-bijective = inverse-bijective ⦃ inver = [∧]-elimᵣ([∃]-proof inver) ⦄

{-
  module _ {f : A → B} ⦃ inver : Invertible(f) ⦄ ⦃ inv-func : Function(inv f) ⦄ where
    inv-sides-equality : (invₗ(f) ⊜ invᵣ(f))
    inv-sides-equality =
      invₗ(f)                 🝖[ _⊜_ ]-[]
      invₗ(f) ∘ id            🝖[ _⊜_ ]-[ [⊜][∘]-binaryOperator-raw {f₁ = invₗ(f)} ⦃ func₂ = {!!} ⦄ (reflexivity(_⊜_)) (intro(inverseᵣ(f)(invᵣ f) ⦃ inv-inverseᵣ ⦄)) ]-sym
      invₗ(f) ∘ (f ∘ invᵣ(f)) 🝖[ _⊜_ ]-[]
      (invₗ(f) ∘ f) ∘ invᵣ(f) 🝖[ _⊜_ ]-[ {!!} ]
      id ∘ invᵣ(f)            🝖[ _⊜_ ]-[]
      invᵣ(f)                 🝖-end

-- congruence₂ᵣ(_∘_)(invₗ(f)) ?

    -- x₁ ≡ x₂
    -- inv f(y₁) ≡ inv f(y₂)

    --f(x₁) ≡ f(x₂)
    --invᵣ f(f(x₁)) ≡ invᵣ f(f(x₂))
    --invᵣ f(f(x₁))

-}

{-
    -- inv is a left inverse function to a bijective f.
    inv-inverseₗ : Inverseₗ(f)(inv f)
    inv-inverseₗ = invᵣ-inverseₗ ⦃ inj = {!invertibleₗ-to-injective!} ⦄
    -- [∃!]-existence-eq-any (bijective(f)) (reflexivity(_≡_))

    inv-injective : Injective(inv f)
    inv-injective = {!invᵣ-injective!}-}

{-
    -- inv(f) is surjective when f is bijective.
    inv-surjective : Surjective(inv(f))
    Surjective.proof(inv-surjective) {x} = [∃]-intro(f(x)) ⦃ inv-inverseₗ ⦄

    inv-unique-inverseᵣ : ∀{f⁻¹} → (f ∘ f⁻¹ ⊜ id) → (f⁻¹ ⊜ inv(f))
    inv-unique-inverseᵣ = invᵣ-unique-inverseᵣ ⦃ surj = bijective-to-surjective(f) ⦄ ⦃ inj = bijective-to-injective(f) ⦄

    inv-unique-inverseₗ : ∀{f⁻¹} → ⦃ _ : Function(f⁻¹) ⦄ → (f⁻¹ ∘ f ⊜ id) → (f⁻¹ ⊜ inv(f))
    inv-unique-inverseₗ = invᵣ-unique-inverseₗ ⦃ surj = bijective-to-surjective(f) ⦄

    -- inv(f) is a function when f is a function.
    inv-function : Function(inv(f))
    inv-function = invᵣ-function ⦃ surj = bijective-to-surjective(f) ⦄ ⦃ inj = bijective-to-injective(f) ⦄

    module _ ⦃ func : Function(f) ⦄ where
      -- inv(f) is injective when f is a function and is bijective.
      inv-injective : Injective(inv f)
      inv-injective = invᵣ-injective ⦃ surj = bijective-to-surjective(f) ⦄

      -- inv(f) is bijective when f is a function and is bijective.
      inv-bijective : Bijective(inv(f))
      inv-bijective = injective-surjective-to-bijective(inv(f)) ⦃ inv-injective ⦄ ⦃ inv-surjective ⦄
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Luau.Value where

open import Luau.Addr using (Addr)
open import Luau.Syntax using (Block; Expr; nil; addr; function⟨_⟩_end)
open import Luau.Var using (Var)

data Value : Set where
  nil : Value
  addr : Addr → Value

val : Value → Expr
val nil = nil
val (addr a) = addr a

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Binary.Raw.Construct.Constant where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels using (hProp)

open import Cubical.Relation.Binary.Raw

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

Const : ∀ {a b c} {A : Type a} {B : Type b} → Type c → RawREL A B c
Const I = λ _ _ → I

------------------------------------------------------------------------
-- Properties

module _ {a c} {A : Type a} {C : Type c} where

  reflexive : C → Reflexive {A = A} (Const C)
  reflexive c = c

  symmetric : Symmetric {A = A} (Const C)
  symmetric c = c

  transitive : Transitive {A = A} (Const C)
  transitive c d = c

  isPartialEquivalence : IsPartialEquivalence {A = A} (Const C)
  isPartialEquivalence = record
    { symmetric  = λ {x} {y} → symmetric {x} {y}
    ; transitive = λ {x} {y} {z} → transitive {x} {y} {z}
    }

  partialEquivalence : PartialEquivalence A c
  partialEquivalence = record { isPartialEquivalence = isPartialEquivalence }

  isEquivalence : C → IsEquivalence {A = A} (Const C)
  isEquivalence c = record
    { isPartialEquivalence = isPartialEquivalence
    ; reflexive            = λ {x} → reflexive c {x}
    }

  equivalence : C → Equivalence A c
  equivalence x = record { isEquivalence = isEquivalence x }


text:
{-# OPTIONS --allow-unsolved-metas #-}
module MGU-revised where

--open import Agda.Builtin.Nat using () renaming (Nat to ℕ)
open import Agda.Primitive
open import Agda.Builtin.Equality

open import Prelude.Product using (Σ; _,_; fst; snd; _×_; curry; uncurry)
open import Prelude.Equality using (eqReasoningStep; _∎; sym; trans; cong)
open import Prelude.Function using (_∘_)
open import Prelude.Empty using (⊥)
open import Prelude.Sum using (left; right) renaming (Either to _⊎_)
open import Prelude.Maybe using (Maybe; just; nothing)

private
  ∃ : ∀ {a b} {A : Set a} (B : A → Set b) → Set (a ⊔ b)
  ∃ = Σ _

open import Prelude using (_$_)

open import Relation.Binary

open import Prolegomenon

import Relation.Binary.Indexed as I

open import Algebra

mcbrideMonoidTransformer : MonoidTransformer lzero lzero lzero lzero
Setoid.Carrier (MonoidTransformer.base mcbrideMonoidTransformer) = {!!}
Setoid._≈_ (MonoidTransformer.base mcbrideMonoidTransformer) = {!!}
Setoid.isEquivalence (MonoidTransformer.base mcbrideMonoidTransformer) = {!!}
Monoid.Carrier (MonoidTransformer.exponent mcbrideMonoidTransformer) = {!!}
Monoid._≈_ (MonoidTransformer.exponent mcbrideMonoidTransformer) = {!!}
Monoid._∙_ (MonoidTransformer.exponent mcbrideMonoidTransformer) = {!!}
Monoid.ε (MonoidTransformer.exponent mcbrideMonoidTransformer) = {!!}
Monoid.isMonoid (MonoidTransformer.exponent mcbrideMonoidTransformer) = {!!}
MonoidTransformer._◃_ mcbrideMonoidTransformer = {!!}
MonoidTransformer.isMonoidTransformer mcbrideMonoidTransformer = {!!}

record Unificationoid ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ : Set (lsuc (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
  field
    monoidTransformer : MonoidTransformer ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ

  open module MT = MonoidTransformer monoidTransformer public
{-
  open MonoidTransformer monoidTransformer public renaming
    (_≈ˢ_ to _=ᵗ_
    ;Carrierˢ to T
    ;Carrierᵐ to S
    ;_≈ᵐ_ to _=ˢ_)
-}
  Property : ∀ {ℓ} → Set (ℓˢ ⊔ lsuc ℓ)
  Property {ℓ} = E.Carrier → Set ℓ

  Nothing : ∀ {ℓ} → (P : Property {ℓ}) → Set (ℓ ⊔ ℓˢ)
  Nothing P = ∀ s → P s → ⊥

  IsUnifier : (t₁ t₂ : B.Carrier) → Property
  IsUnifier t₁ t₂ s = s ◃ t₁ B.≈ s ◃ t₂

  field
    unify : (t₁ t₂ : B.Carrier) → Nothing (IsUnifier t₁ t₂) ⊎ ∃ (IsUnifier t₁ t₂)

record MostGeneralUnificationoid ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ : Set (lsuc (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
  --infix 4 _≠ᵗ_
  field
    unificationoid : Unificationoid ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ

  open Unificationoid unificationoid public

  _≤_ : (s₋ : E.Carrier) (s₊ : E.Carrier) → Set (ℓˢ ⊔ ℓ⁼ˢ)
  _≤_ s₋ s₊ = ∃ λ s → s E.∙ s₊ E.≈ s₋

  _≠ᵗ_ : B.Carrier → B.Carrier → Set ℓ⁼ᵗ
  _≠ᵗ_ t₁ t₂ = t₁ B.≈ t₂ → ⊥
{-
  _<_ : (s₋ : E.Carrier) (s₊ : E.Carrier) → Set (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)
  _<_ s₋ s₊ = s₋ ≤ s₊ × (∀ t → (s₊ ◃ t) ≠ᵗ t → (s₋ ◃ t) ≠ᵗ t) × ∃ λ t → (s₋ ◃ t) ≠ᵗ t × (s₊ ◃ t) B.≈ t
  --the set of T that are changed by a applying substitution is strictly less with s₊ than with s₋. That is, s₋ makes more changes than s₊.
  --that is, if s₊ makes a change to t then so does s₋, but there is some t s.t. s₋ makes a change but s₊ does not
-}
  MostGenerally : ∀ {ℓ} (P : Property {ℓ}) → Property
  MostGenerally P s₊ = P s₊ × ∀ s₋ → P s₋ → s₋ ≤ s₊

  field
    isMguIfUnifier : (t₁ t₂ : B.Carrier) → (ru : ∃ λ s → unify t₁ t₂ ≡ right s) →
      Prelude.case ru of (λ {((u , _) , _) → MostGenerally (IsUnifier t₁ t₂) u})

  mgu : (t₁ t₂ : B.Carrier) → Nothing (IsUnifier t₁ t₂) ⊎ ∃ (MostGenerally $ IsUnifier t₁ t₂)
  mgu t₁ t₂ with unify t₁ t₂ | Prelude.graphAt (unify t₁) t₂
  mgu t₁ t₂ | left x | ef = left x
  mgu t₁ t₂ | right x | Prelude.ingraph eq with isMguIfUnifier t₁ t₂ (x , eq)
  mgu t₁ t₂ | right (fst₁ , snd₁) | (Prelude.ingraph eq) | dfsd = right (fst₁ , dfsd)

record PairMostGeneralUnificationoid ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ : Set (lsuc (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
  field
    mostGeneralUnificationoid : MostGeneralUnificationoid ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ

  open MostGeneralUnificationoid mostGeneralUnificationoid public

  field
    separateExponents : E.Carrier → E.Carrier × E.Carrier

  IsPairUnifier : (t₁ t₂ : B.Carrier) → Property
  IsPairUnifier t₁ t₂ u = let (s₁ , s₂) = separateExponents u in s₁ ◃ t₁ B.≈ s₂ ◃ t₂

  field
    pair-mgu : (t₁ t₂ : B.Carrier)
               → Nothing (IsPairUnifier t₁ t₂) ⊎ ∃ (MostGenerally (IsPairUnifier t₁ t₂))

record MakePairFromRegular ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ : Set (lsuc (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
  field
    mostGeneralUnificationoid : MostGeneralUnificationoid ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ

  open MostGeneralUnificationoid mostGeneralUnificationoid public

  field
    left-exponent : E.Carrier → E.Carrier
    right-exponent : E.Carrier → E.Carrier
    left-base : B.Carrier → B.Carrier
    right-base : B.Carrier → B.Carrier
    exponent-to-base : ∀ {s t₁ t₂} → left-exponent s ◃ t₁ B.≈ right-exponent s ◃ t₂ → s ◃ left-base t₁ B.≈ s ◃ right-base t₂
    base-to-exponent : ∀ {s t₁ t₂} → s ◃ left-base t₁ B.≈ s ◃ right-base t₂ → left-exponent s ◃ t₁ B.≈ right-exponent s ◃ t₂

  pairMostGeneralUnificationoid : PairMostGeneralUnificationoid ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ
  PairMostGeneralUnificationoid.mostGeneralUnificationoid pairMostGeneralUnificationoid = mostGeneralUnificationoid
  PairMostGeneralUnificationoid.separateExponents pairMostGeneralUnificationoid x = left-exponent x , right-exponent x
  PairMostGeneralUnificationoid.pair-mgu pairMostGeneralUnificationoid t₁ t₂ with mgu (left-base t₁) (right-base t₂)
  PairMostGeneralUnificationoid.pair-mgu pairMostGeneralUnificationoid t₁ t₂ | left notunifier = left (λ s x → notunifier s (exponent-to-base x))
  PairMostGeneralUnificationoid.pair-mgu pairMostGeneralUnificationoid t₁ t₂ | right (s , x-base , unified-correct) = right (s , base-to-exponent x-base , (λ s₋ x-exponent → unified-correct s₋ (exponent-to-base x-exponent)))

  --(s , base-to-exponent x , (λ s₋ x₁ → s₋ , {!snd (snd₁ s x)!}))

-- -- open import Algebra

-- -- record PairUnificationoid ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ : Set (lsuc (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
-- --   field
-- --     monoidTransformer : MonoidTransformer ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ

-- --   open module MT = MonoidTransformer monoidTransformer public -- renaming (module E to Exponent)

-- -- {-
-- --   open MonoidTransformer monoidTransformer public renaming
-- --     (_≈ˢ_ to _=ᵗ_
-- --     ;Carrierˢ to T
-- --     ;Carrierᵐ to S
-- --     ;_≈ᵐ_ to _=ˢ_)
-- -- -}

-- --   Property : ∀ {ℓ} → Set (ℓˢ ⊔ lsuc ℓ)
-- --   Property {ℓ} = E.Carrier × E.Carrier → Set ℓ

-- --   Nothing : ∀ {ℓ} → (P : Property {ℓ}) → Set (ℓ ⊔ ℓˢ)
-- --   Nothing P = ∀ u → P u → ⊥

-- --   IsUnifier : ∀ t₁ t₂ → Property
-- --   IsUnifier t₁ t₂ u = let (s₁ , s₂) = u in s₁ ◃ t₁ B.≈ s₂ ◃ t₂

-- --   field
-- --     unify : ∀ t₁ t₂
-- --           → Nothing (IsUnifier t₁ t₂) ⊎ ∃ (IsUnifier t₁ t₂)

-- -- module MakePairUnificationoidFromUnificationoid where

-- --   postulate
-- --     ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ : Level
-- --     unificationoid : Unificationoid ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ

-- --   open Unificationoid unificationoid

-- --   pairUnificationoid : PairUnificationoid ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ
-- --   PairUnificationoid.monoidTransformer pairUnificationoid = monoidTransformer
-- --   PairUnificationoid.unify pairUnificationoid t₁ t₂ with unify t₁ t₂
-- --   PairUnificationoid.unify pairUnificationoid t₁ t₂ | left x = left (λ {(s₁ , s₂) x₁ → x {!!} {!x₁!}})
-- --   PairUnificationoid.unify pairUnificationoid t₁ t₂ | right (s₁ , snd₁) = {!!}

-- --   {-
-- --     s ◃ swap ◃ t₁ = s ◃ t₂
-- --     swap ∙ swap = ε
-- --     want: x , y s.t. x ◃ t₁ = x ◃ t₂
-- --     easy: x = s ∙ swap, y = s

-- --     harder:
-- --     s₁ ◃ t₁ = s₂ ◃ t₂
-- --     want: x s.t. x ◃ t₁ = x ◃ t₂
-- --   -}

-- -- -- record Isomorphic {a} {A : Set a} {ℓᵃ} {_=ᵃ_ : A → A → Set ℓᵃ} (isEquivalenceᵃ : IsEquivalence _=ᵃ_)  {b} {B : Set b} {ℓᵇ} {_=ᵇ_ : B → B → Set ℓᵇ} (isEquivalenceᵇ : IsEquivalence _=ᵇ_) : Set (a ⊔ ℓᵃ ⊔ b ⊔ ℓᵇ) where
-- -- --   field
-- -- --     toA : B → A
-- -- --     toB : A → B
-- -- --     rtA : (x : A) → toA (toB x) =ᵃ x
-- -- --     rtB : (x : B) → toB (toA x) =ᵇ x
-- -- --     isoA : (x₁ x₂ : A) → x₁ =ᵃ x₂ → toB x₁ =ᵇ toB x₂
-- -- --     isoB : (x₁ x₂ : B) → x₁ =ᵇ x₂ → toA x₁ =ᵃ toA x₂

-- -- -- record Splittable ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ : Set (lsuc (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
-- -- --   field
-- -- --     mostGeneralUnificationoid : MostGeneralUnificationoid ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ

-- -- --   open MostGeneralUnificationoid mostGeneralUnificationoid public

-- -- --   S-independent : (t₁ t₂ : T) → Set (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)
-- -- --   S-independent t₁ t₂ = ∀ t₁s s → s ◃ t₁ =ᵗ t₁s → MostGenerally (λ s → s ◃ t₁ =ᵗ t₁s) s → s ◃ t₂ =ᵗ t₂

-- -- --   S-Invertable : Property
-- -- --   S-Invertable s = s ∙ s =ˢ ε

-- -- --   Swapifies : (t₁ t₂ : T) → Property
-- -- --   Swapifies t₁ t₂ s = s ◃ t₁ =ᵗ t₂ × s ◃ t₂ =ᵗ t₁

-- -- --   UnifiesOnLeft : (t₁ t₂ : T) → Property
-- -- --   UnifiesOnLeft t₁ t₂ s = s ◃ t₁ =ᵗ t₂

-- -- --   RelativeIdentity : T → Property
-- -- --   RelativeIdentity t s = s ◃ t =ᵗ t

-- -- --   field
-- -- --     make-S-independent :
-- -- --       (t₁ t₂ : T) →
-- -- --         ∃ λ swap₁ → S-Invertable swap₁ ×
-- -- --                     ∃ λ t₁′ → MostGenerally (Swapifies t₁ t₁′) swap₁ ×
-- -- --                               ∃ λ s₁ → MostGenerally (UnifiesOnLeft t₁ t₁′) s₁ ×
-- -- --                                        RelativeIdentity t₂ s₁

-- -- --     Tᵢ : Prelude.List Prelude.Nat → Set
-- -- --     toTᵢ : T → ∃ Tᵢ

-- -- --   pairUnification : PairMostGeneralUnificationoid ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ
-- -- --   PairMostGeneralUnificationoid.monoidTransformer pairUnification = monoidTransformer
-- -- --   PairMostGeneralUnificationoid.mgu pairUnification t₁ t₂ with make-S-independent t₁ t₂
-- -- --   PairMostGeneralUnificationoid.mgu pairUnification t₁ t₂ | (swap₁ , swap₁∙swap₁=ε , t₁′ , ((swap₁◃t₁=t₁′ , swap₁◃t₁′=t₁) , mgswap) , slip₁ , (slip₁◃t₁=t₁′ , mgleft) , slip₁◃t₂=t₂) with mgu t₁′ t₂
-- -- -- --  … | (left NoT₁T₂) =
-- -- --   PairMostGeneralUnificationoid.mgu pairUnification t₁ t₂ | (swap₁ , swap₁∙swap₁=ε , t₁′ , ((swap₁◃t₁=t₁′ , swap₁◃t₁′=t₁) , mgswap) , slip₁ , (slip₁◃t₁=t₁′ , mgleft) , slip₁◃t₂=t₂) | (left NoT₁T₂) =
-- -- --     left
-- -- --     λ {(s₁ , s₂) s₁◃t₁=s₂◃t₂ →
-- -- --     {!let (s₁′ , s₂′ , s₁′◃t₁=s₂′◃t₂ , s₁′∙swap₁◃t₂=swap₁◃t₂ , s₂′∙swap₁∙s₂′◃t₂=swap₁∙s₂′◃t₂) = helper!}}
-- -- --     {-
-- -- --     NoT₁T₂ (slip₁ ∙ s₂ ∙ swap₁ ∙ s₁ ∙ swap₁)
-- -- --       (let t₁′▹s₂=t₁′ : {!!} -- s₂ ◃ t₁′ =ᵗ t₁′
-- -- --            t₁′▹s₂=t₁′ = {!!} in {!!})}
-- -- --     -}
-- -- --          -- ? s₂ (s₁ ◃ t₁) (symˢ t₁▹s₁=t₂▹s₂ , (λ s₁₋ t₂▹s₁₋=t₁▹s₁ → {!!} , {!!})) in {!!})}) -- mgur s₂ (t₁ ▹ s₁) (symˢ t₁▹s₁=t₂▹s₂ , ?)
-- -- --   PairMostGeneralUnificationoid.mgu pairUnification t₁ t₂ | (swap₁ , swap₁∙swap₁=ε , t₁′ , ((swap₁◃t₁=t₁′ , swap₁◃t₁′=t₁) , mgswap) , slip₁ , (slip₁◃t₁=t₁′ , mgleft) , slip₁◃t₂=t₂) | (right (s , s◃t₁′=s◃t₂ , mgur)) = right $ (s ∙ slip₁ , s) , {!!} , (λ {(s₁′ , s₂′) s₁′◃t₁=s₂′◃t₂ → {!!}})

-- -- --   {-
-- -- --   goal
-- -- --   slip₁ ∙ s₂ ∙ swap₁ ∙ s₁ ∙ swap₁ ◃ t₁′        =ᵗ slip₁ ∙ s₂ ∙ swap₁ ∙ s₁ ∙ swap₁ ◃ t₂
-- -- --   by slip₁◃t₁=t₁′
-- -- --   slip₁ ∙ s₂ ∙ swap₁ ∙ s₁ ∙ swap₁ ∙ slip₁ ◃ t₁ =ᵗ slip₁ ∙ s₂ ∙ swap₁ ∙ s₁ ∙ swap₁ ◃ t₂
-- -- --   conjecture: swap₁ ∙ slip₁ ◃ t₁ = t₁
-- -- --   conjecture: s₁ ∙ swap₁ ◃ t₂ = swap₁ ◃ t₂
-- -- --   slip₁ ∙ s₂ ∙ swap₁ ∙ s₁ ◃ t₁ =ᵗ slip₁ ∙ s₂ ∙ swap₁ ∙ swap₁ ◃ t₂
-- -- --   by swap₁∙swap₁=ε
-- -- --   slip₁ ∙ s₂ ∙ swap₁ ∙ s₁ ◃ t₁ =ᵗ slip₁ ∙ s₂ ◃ t₂
-- -- --   by s₁◃t₁=s₂◃t₂
-- -- --   slip₁ ∙ s₂ ∙ swap₁ ∙ s₂ ◃ t₂ =ᵗ slip₁ ∙ s₂ ◃ t₂
-- -- --   conjecture: s₂ ∙ swap₁ ∙ s₂ ◃ t₂ = swap₁ ∙ s₂ ◃ t₂
-- -- --   slip₁ ∙ swap₁ ∙ s₂ ◃ t₂ =ᵗ slip₁ ∙ s₂ ◃ t₂
-- -- --   conjecture: swap₁ ∙ s₂ ◃ t₂ = slip₁ ∙ s₂ ◃ t₂
-- -- --   slip₁ ∙ slip₁ ∙ s₂ ◃ t₂ =ᵗ slip₁ ∙ s₂ ◃ t₂
-- -- --   conjecture: slip₁ ∙ slip₁ = slip₁
-- -- --   slip₁ ∙ s₂ ◃ t₂ =ᵗ slip₁ ∙ s₂ ◃ t₂

-- -- --   goal : ?0 ◃ t₁′ = ?0 ◃ t₂

-- -- --   e.g.
-- -- --   f(x,g(y),z) = f(g(y),x,h(z))
-- -- --   s₁ = x → g(y) , z → h(z) ; s₂ = x → g(y)
-- -- --   s = x → a ; y → b ; z → c
-- -- --   t₁′ = f(a,g(b),c)
-- -- --   S = a → g(y) , x → g(b) , c → h(z)
-- -- --   s⁻¹ = a → x , b → y , c → z
-- -- --   s₁ ∙ s⁻¹ = a → g(y) , b → y , c → h(z)
-- -- --   s₂ ∙ s₁ ∙ s⁻¹ = a → g(y) , b → y , c → h(z) , x → g(y)
-- -- --   S = s ∙ s₂ ∙ s₁ ∙ s⁻¹ = a → g(b) , b → b , c → h(c) , x → g(b) , y → b , z → c
-- -- --   t₁′ ▹ S = f(g(b),g(b),h(c))
-- -- --   t₂ ▹ S = f(g(b),g(b),h(c))

-- -- --   f(x,g(y),z) = f(g(y),x,h(z))
-- -- --   s₁ = x → g(x) , y → x , z → h(z) ; s₂ = y → x , x → g(x)
-- -- --   s = x → a ; y → b ; z → c
-- -- --   t₁′ = f(a,g(b),c)
-- -- --   s⁻¹ = a → x , b → y , c → z
-- -- --   s₁ ∙ s⁻¹ = a → g(x) , b → x , c → h(z) , x → g(x) , y → x , z → h(z)
-- -- --   s₂ ∙ s₁ ∙ s⁻¹ = a → g(g(x)) , b → g(x) , c → h(z) , x → g(g(x)) , y → g(x) , z → h(z)
-- -- --   s ∙ s₂ ∙ s₁ ∙ s⁻¹ = a → g(g(a)) , b → g(a) , c → h(c) , x → g(g(a)) , y → g(a) , z → h(c)

-- -- --   s⁻¹          = a → x    , b → y , c → z
-- -- --   s₁ ∙ s⁻¹     = a → g(x) , b → x , c → h(z) , x → g(x) , y → x , z → h(z)
-- -- --   s ∙ s₁ ∙ s⁻¹ = a → g(a) , b → a , c → h(c) , x → g(a) , y → a , z → h(c)

-- -- --   s₁′          = a → g(a) , b → a , c → h(c)
-- -- --   s₂′          = y → a , x → g(a) , z → c

-- -- --   let swap₁ = x → a , y → b , z → c , a → x , b → y , c → z -- take variables common to t₁ and t₂, and swap them for variables outside of either (and outside of s₁ or s₂?)
-- -- --         s₁ ∙ swap₁ = x → a , y → b , z → c , a → g(x) , b → x , c → h(z)
-- -- --   s₁′ = swap₁ ∙ s₁ ∙ swap₁ = a → g(a) , b → a , c → h(c)
-- -- --   s₁′ = swap₁ ∙ s₁ ∙ swap₁
-- -- --   let slip₁ = x → a , y → b , z → c
-- -- --   let s₂′ = slip₁ ∙ s₂ = y → a , x → g(a) , z → c
-- -- --   s₂′ ∙ s₁′ = a → g(a) , b → a , c → h(c) , y → a , x → g(a) , z → c
-- -- --   slip₁ ∙ s₂ ∙ swap₁ ∙ s₁ ∙ swap₁

-- -- --   f(g(g(a)),g(g(a)),h(c)) = f(g(g(a)),g(g(a)),h(h(c)))

-- -- --   f(x,g(y),z) = f(g(y),x,h(z))
-- -- --   -}
-- -- --   {-
-- -- --   … | (t₁' , s-independent , s , t₁'= , s⁻¹ , t₁=) with mgu t₁' t₂
-- -- --   … | (left NoT₁T₂) = left $ λ {(s₁ , s₂) t₁▹s₁=t₂▹s₂ → NoT₁T₂ {!≈ˢ-over-▹-⟶-≈ᵐ!} {!isMonoidTransformer!}}
-- -- --   … | (right x) = right {!!}
-- -- --   -}

-- -- -- {-
-- -- --   suppose t₁ ▹ s₁ = t₂ ▹ s₂
-- -- --   given:
-- -- --     t₁' ▹ * ≠ t₂ ▹ *

-- -- --   t₁ = t₁' ▹ s
-- -- --   try s = the most general such

-- -- --   t₁ = t₁' ▹ s⁻¹
-- -- --   t₁' = t₁ ▹ s
-- -- --   t₁ ▹ s₁ = t₂ ▹ s₂
-- -- --   s ∙ s⁻¹ = ε

-- -- --   t₁' ▹ s⁻¹ ▹ s₁ = t₂ ▹ s₂

-- -- --   finx x = s₁

-- -- --   t₁ ▹ x = t₂ ▹ s⁻¹ ▹ x
-- -- --   t₁' ▹ x = t₂ ▹ x
-- -- --   t₁ ▹ s ▹ x = t₂ ▹ x
-- -- --   t₁ ▹ s ▹ x = t₂ ▹ s⁻¹ ▹ s ▹ x
-- -- -- -}

-- -- -- data STerm (A : Set) : Set where
-- -- --   ι : A → STerm A
-- -- --   _fork_ : STerm A → STerm A → STerm A
-- -- --   leaf : STerm A

-- -- -- sub : {V : Set} → (V → Maybe (STerm V)) → STerm V → STerm V
-- -- -- sub σ (ι x) with σ x
-- -- -- sub σ (ι x) | nothing = ι x
-- -- -- sub σ (ι x) | just x₁ = x₁
-- -- -- sub σ (t fork t₁) = sub σ t fork sub σ t₁
-- -- -- sub σ leaf = leaf

-- -- -- {-
-- -- --   Sᵢ : List (V × T) → S
-- -- --   Tᵢ : List V → T
-- -- --   indexS : S → ∃ Sᵢ
-- -- --   indexT : T → ∃ Tᵢ
-- -- --   _▹ᵢ_ : {vs : List V} {vts : List (V × T)} → Tᵢ vs → Sᵢ vts → ∃ λ
-- -- --   (t : T) (s : S) → t ▹ s
-- -- --   (V → T) → T → T

-- -- --   getTermIndexedByAVariable : (v : V) (t : T) → T → T
-- -- --   getTermFromIndexedTerm :

-- -- --   v ∈ variables s → t ▹ s
-- -- -- -}

-- -- -- record IsSeparableInto {sx s x} (SX : Set sx) (S : Set s) (X : Set x) : Set (s ⊔ x ⊔ sx) where
-- -- --   field
-- -- --     separate : SX → S × X
-- -- --     combine : S × X → SX
-- -- --     iso : ∀ sx → combine (separate sx) ≡ sx

-- -- -- record IsSeparableInto₂ {sx s x} (SX : Set sx) (X : Set x) (S : X → Set s) : Set (s ⊔ x ⊔ sx) where
-- -- --   field
-- -- --     separate : SX → Σ X S
-- -- --     combine : Σ X S → SX
-- -- --     iso : ∀ sx → combine (separate sx) ≡ sx

-- -- -- record Separableoid sx s x : Set (lsuc (sx ⊔ s ⊔ x)) where
-- -- --   field
-- -- --     SX : Set sx
-- -- --     S : Set s
-- -- --     X : Set x
-- -- --     separable : IsSeparableInto SX S X

-- -- -- -- record FreeVariableoid ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ ℓᵛ ℓ : Set (lsuc (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
-- -- -- --   field
-- -- -- --     monoidTransformer : MonoidTransformer ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ

-- -- -- --   open MonoidTransformer monoidTransformer public renaming
-- -- -- --     (_≈ˢ_ to _=ᵗ_
-- -- -- --     ;Carrierˢ to T
-- -- -- --     ;Carrierᵐ to S
-- -- -- --     ;_≈ᵐ_ to _=ˢ_)

-- -- -- --   field
-- -- -- --     termVariableoid : Setoid ℓᵛ ℓ⁼ᵛ
-- -- -- --     termStructureoid :

-- -- -- --   open Setoid Variable public using () renaming
-- -- -- --     (Carrier to V
-- -- -- --     ;_≈_ to _=ᵛ_)

-- -- -- --   field
-- -- -- --     termVariables : Term → Pred Variable ℓᵛ


text:
open import Prelude
open import Nat
open import core
open import contexts
open import weakening
open import exchange
open import lemmas-disjointness
open import binders-disjoint-checks

module lemmas-subst-ta where
  -- this is what makes the binders-unique assumption below good enough: it
  -- tells us that we can pick fresh variables
  mutual
    binders-envfresh : ∀{Δ Γ Γ' y σ} → Δ , Γ ⊢ σ :s: Γ' → y # Γ → unbound-in-σ y σ → binders-unique-σ σ → envfresh y σ
    binders-envfresh {Γ' = Γ'} {y = y} (STAId x) apt unbound unique with ctxindirect Γ' y
    binders-envfresh {Γ' = Γ'} {y = y} (STAId x₁) apt unbound unique | Inl x = abort (somenotnone (! (x₁ y (π1 x) (π2 x)) · apt))
    binders-envfresh (STAId x₁) apt unbound unique | Inr x = EFId x
    binders-envfresh {Γ = Γ} {y = y} (STASubst  {y = z} subst x₁) apt (UBσSubst x₂ unbound neq) (BUσSubst zz x₃ x₄) =
                                                                                EFSubst (binders-fresh {y = y} x₁ zz x₂ apt)
                                                                                (binders-envfresh subst (apart-extend1 Γ neq apt) unbound x₃)
                                                                                neq

    binders-fresh : ∀{ Δ Γ d2 τ y} → Δ , Γ ⊢ d2 :: τ
                                      → binders-unique d2
                                      → unbound-in y d2
                                      → Γ y == None
                                      → fresh y d2
    binders-fresh TAConst BUHole UBConst apt = FConst
    binders-fresh {y = y} (TAVar {x = x} x₁)  BUVar UBVar apt with natEQ y x
    binders-fresh (TAVar x₂) BUVar UBVar apt | Inl refl = abort (somenotnone (! x₂ · apt))
    binders-fresh (TAVar x₂) BUVar UBVar apt | Inr x₁ = FVar x₁
    binders-fresh {y = y} (TALam {x = x} x₁ wt) bu2 ub apt  with natEQ y x
    binders-fresh (TALam x₂ wt) bu2 (UBLam2 x₁ ub) apt | Inl refl = abort (x₁ refl)
    binders-fresh {Γ = Γ} (TALam {x = x} x₂ wt) (BULam bu2 x₃) (UBLam2 x₄ ub) apt | Inr x₁ =  FLam x₁ (binders-fresh wt bu2 ub (apart-extend1 Γ x₄ apt))
    binders-fresh (TAAp wt wt₁)  (BUAp bu2 bu3 x) (UBAp ub ub₁) apt = FAp (binders-fresh wt bu2 ub apt) (binders-fresh wt₁ bu3 ub₁ apt)
    binders-fresh (TAEHole x₁ x₂) (BUEHole x) (UBHole x₃) apt = FHole (binders-envfresh x₂ apt x₃ x )
    binders-fresh (TANEHole x₁ wt x₂) (BUNEHole bu2 x) (UBNEHole x₃ ub) apt = FNEHole (binders-envfresh x₂ apt x₃ x) (binders-fresh wt bu2  ub apt)
    binders-fresh (TACast wt x₁) (BUCast bu2) (UBCast ub) apt = FCast (binders-fresh wt  bu2  ub apt)
    binders-fresh (TAFailedCast wt x x₁ x₂) (BUFailedCast bu2) (UBFailedCast ub) apt = FFailedCast (binders-fresh wt  bu2  ub apt)

  -- the substition lemma for preservation
  lem-subst : ∀{Δ Γ x τ1 d1 τ d2 } →
                  x # Γ →
                  binders-disjoint d1 d2 →
                  binders-unique d2 →
                  Δ , Γ ,, (x , τ1) ⊢ d1 :: τ →
                  Δ , Γ ⊢ d2 :: τ1 →
                  Δ , Γ ⊢ [ d2 / x ] d1 :: τ
  lem-subst apt bd bu2  TAConst wt2 = TAConst
  lem-subst {x = x} apt bd bu2  (TAVar {x = x'} x₂) wt2 with natEQ x' x
  lem-subst {Γ = Γ} apt bd bu2 (TAVar x₃) wt2 | Inl refl with lem-apart-union-eq {Γ = Γ} apt x₃
  lem-subst apt bd bu2  (TAVar x₃) wt2 | Inl refl | refl = wt2
  lem-subst {Γ = Γ} apt bd bu2  (TAVar x₃) wt2 | Inr x₂ = TAVar (lem-neq-union-eq {Γ = Γ} x₂ x₃)
  lem-subst {Δ = Δ} {Γ = Γ} {x = x} {d2 = d2} x#Γ (BDLam bd bd') bu2 (TALam {x = y} {τ1 = τ1} {d = d} {τ2 = τ2} x₂ wt1) wt2
    with lem-union-none {Γ = Γ} x₂
  ... |  x≠y , y#Γ with natEQ y x
  ... | Inl eq = abort (x≠y (! eq))
  ... | Inr _  = TALam y#Γ (lem-subst {Δ = Δ} {Γ = Γ ,, (y , τ1)} {x = x} {d1 = d} (apart-extend1 Γ x≠y x#Γ) bd bu2 (exchange-ta-Γ {Γ = Γ} x≠y wt1)
                                         (weaken-ta (binders-fresh wt2 bu2 bd' y#Γ) wt2))
  lem-subst apt (BDAp bd bd₁) bu3 (TAAp wt1 wt2) wt3 = TAAp (lem-subst apt bd bu3 wt1 wt3) (lem-subst apt bd₁ bu3 wt2 wt3)
  lem-subst apt bd bu2 (TAEHole inΔ sub) wt2 = TAEHole inΔ (STASubst sub wt2)
  lem-subst apt (BDNEHole x₁ bd) bu2 (TANEHole x₃ wt1 x₄) wt2 = TANEHole x₃ (lem-subst apt bd bu2 wt1 wt2) (STASubst x₄ wt2)
  lem-subst apt (BDCast bd) bu2 (TACast wt1 x₁) wt2 = TACast (lem-subst apt bd bu2 wt1 wt2) x₁
  lem-subst apt (BDFailedCast bd) bu2 (TAFailedCast wt1 x₁ x₂ x₃) wt2 = TAFailedCast (lem-subst apt bd bu2 wt1 wt2) x₁ x₂ x₃

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
open import OutsideIn.Prelude
open import OutsideIn.X
module OutsideIn(x : X) where
  open X (x) public
  open import OutsideIn.Prelude public
  open import Data.Vec public hiding ([_])
  import OutsideIn.Constraints as C
  import OutsideIn.TypeSchema as TS
  import OutsideIn.Expressions as E
  import OutsideIn.Environments as V
  import OutsideIn.TopLevel as TL
  import OutsideIn.Inference as I
  open E (x) public
  open TL(x) public
  open TS(x) public
  open I (x) public
  open V (x) public
  open C (x)

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


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

module Karatsuba where

open import Prelude

open import Data.List
open import Data.List.Syntax

open import TreeFold

open import Data.Integer

import Data.Nat as ℕ

open import Literals.Number
open import Data.Integer.Literals

Diff : Type a → Type a
Diff A = List A → List A

⌈⌉ : Diff A
⌈⌉ = id

⌈_⌉ : A → Diff A
⌈_⌉ = _∷_

⌊_⌋ : Diff A → List A
⌊ xs ⌋ = xs []

record K (A : Type a) : Type a where
  constructor k
  field
    sh lo hi : Diff A
    out : List A
open K

infixl 6 _⊕_ _⊝_
_⊕_ : List ℤ → List ℤ → List ℤ
[]       ⊕ ys       = ys
xs       ⊕ []       = xs
(x ∷ xs) ⊕ (y ∷ ys) = (x + y) ∷ (xs ⊕ ys)

_⍟_ : List ℤ → List ℤ → List (K ℤ)
[]       ⍟ ys       = map (λ y → k ⌈ 0 ⌉ ⌈⌉ ⌈ y ⌉ []) ys
xs       ⍟ []       = map (λ x → k ⌈ 0 ⌉ ⌈ x ⌉ ⌈⌉ []) xs
(x ∷ xs) ⍟ (y ∷ ys) = k ⌈ 0 ⌉ ⌈ x ⌉ ⌈ y ⌉ [ x * y ] ∷ xs ⍟ ys

_⊝_ : List ℤ → List ℤ → List ℤ
xs ⊝ ys = xs ⊕ map negate ys

-- The first parameter in these functions is just used for termination checking.
mutual
  infixl 7 ⟨_⟩_⊛_
  ⟨_⟩_⊛_ : ℕ → List ℤ → List ℤ → List ℤ
  ⟨ n ⟩ []       ⊛ _        = []
  ⟨ n ⟩ _        ⊛ []       = []
  ⟨ n ⟩ (x ∷ []) ⊛ ys       = map (x *_) ys
  ⟨ n ⟩ xs       ⊛ (y ∷ []) = map (y *_) xs
  ⟨ n ⟩ xs       ⊛ ys       = maybe [] out (treeFoldMay ⟨ n ⟩_◆_ (xs ⍟ ys))

  ⟨_⟩_◆_ : ℕ → K ℤ → K ℤ → K ℤ
  (⟨ _     ⟩ xs           ◆ ys          ) .sh  = xs .sh ∘ ys .sh
  (⟨ _     ⟩ xs           ◆ ys          ) .lo  = xs .lo ∘ ys .lo
  (⟨ _     ⟩ xs           ◆ ys          ) .hi  = xs .hi ∘ ys .hi
  (⟨ zero  ⟩ _            ◆ _           ) .out = [] -- should not happen
  (⟨ suc t ⟩ k p x₀ y₀ z₀ ◆ k _ x₁ y₁ z₂) .out =
    let z₁ = ⟨ t ⟩ (⌊ x₀ ⌋ ⊕ ⌊ x₁ ⌋) ⊛ (⌊ y₀ ⌋ ⊕ ⌊ y₁ ⌋)
    in  p (p z₂ ⊕ z₁ ⊝ (z₀ ⊕ z₂)) ⊕ z₀

_⊛_ : List ℤ → List ℤ → List ℤ
xs ⊛ ys = ⟨ length xs ℕ.+ length ys ⟩ xs ⊛ ys

_ : [ 2 , 5 ] ⊛ [ 1 , 1 ] ≡ [ 2 , 7 , 5 ]
_ = refl

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
open import Level using (Level; suc; zero; _⊔_)
open import Algebra.Structures
open import Algebra.FunctionProperties as FunctionProperties using (Op₁; Op₂)
open import Relation.Binary

-- Definition of an ordered monoid, which adds the law that ∙ must
-- preserve the partial order ≤ (or, equivalently, that an ordering x
-- ≤ y must allow for the substitution of y for x in a more complex
-- ordering) to an existing monoid and partial order.
module Algebra.OrderedMonoid where

record IsOrderedMonoid {a ℓ₁ ℓ₂} {A : Set a} (≈ : Rel A ℓ₁) (≤ : Rel A ℓ₂) (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isMonoid       : IsMonoid ≈ ∙ ε
    isPartialOrder : IsPartialOrder ≈ ≤
    compatibility  : ∙ Preserves₂ ≤ ⟶ ≤ ⟶ ≤

  open IsMonoid isMonoid public
       hiding (isEquivalence)
  open IsPartialOrder isPartialOrder public
       renaming (refl to ≤-refl; trans to ≤-trans; reflexive to ≤-reflexive)

record OrderedMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infixl 7 _∙_
  infix  4 _≈_
  infix  4 _≤_
  field
    Carrier         : Set c
    _≈_             : Rel Carrier ℓ₁
    _≤_             : Rel Carrier ℓ₂
    _∙_             : Op₂ Carrier
    ε               : Carrier
    isOrderedMonoid : IsOrderedMonoid _≈_ _≤_ _∙_ ε

  open IsOrderedMonoid isOrderedMonoid public

  substitutivity : ∀ {x y z w} → x ≤ y → z ∙ x ∙ w ≤ z ∙ y ∙ w
  substitutivity x≤y = compatibility (compatibility ≤-refl x≤y) ≤-refl

max_stars_repo_name: wenkokke/agda-pregroup

max_issues_repo_name: wenkokke/agda-pregroup

max_forks_repo_name: wenkokke/agda-pregroup