text:
------------------------------------------------------------------------
-- Properties relating Any to various list functions
------------------------------------------------------------------------

module Data.List.Any.Properties where

open import Category.Monad
open import Data.Bool
open import Data.Bool.Properties
open import Data.Function
open import Data.List as List
open RawMonad List.monad
open import Data.List.Any as Any using (Any; here; there)
import Data.List.Equality as ListEq
open import Data.Product as Prod hiding (map)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Relation.Unary using (Pred; _⟨×⟩_; _⟨→⟩_)
open import Relation.Binary
import Relation.Binary.EqReasoning as EqReasoning
open import Relation.Binary.FunctionSetoid
open import Relation.Binary.Product.Pointwise
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; inspect; _with-≡_)

------------------------------------------------------------------------
-- Lemmas related to Any

-- Introduction (⁺) and elimination (⁻) rules for map.

map⁺ : ∀ {A B} {P : Pred B} {f : A → B} {xs} →
       Any (P ∘₀ f) xs → Any P (map f xs)
map⁺ (here p)  = here p
map⁺ (there p) = there $ map⁺ p

map⁻ : ∀ {A B} {P : Pred B} {f : A → B} {xs} →
       Any P (map f xs) → Any (P ∘₀ f) xs
map⁻ {xs = []}     ()
map⁻ {xs = x ∷ xs} (here p)  = here p
map⁻ {xs = x ∷ xs} (there p) = there $ map⁻ p

-- Introduction and elimination rules for _++_.

++⁺ˡ : ∀ {A} {P : Pred A} {xs ys} →
       Any P xs → Any P (xs ++ ys)
++⁺ˡ (here p)  = here p
++⁺ˡ (there p) = there (++⁺ˡ p)

++⁺ʳ : ∀ {A} {P : Pred A} xs {ys} →
       Any P ys → Any P (xs ++ ys)
++⁺ʳ []       p = p
++⁺ʳ (x ∷ xs) p = there (++⁺ʳ xs p)

++⁻ : ∀ {A} {P : Pred A} xs {ys} →
      Any P (xs ++ ys) → Any P xs ⊎ Any P ys
++⁻ []       p         = inj₂ p
++⁻ (x ∷ xs) (here p)  = inj₁ (here p)
++⁻ (x ∷ xs) (there p) = Sum.map there id (++⁻ xs p)

-- Introduction and elimination rules for return.

return⁺ : ∀ {A} {P : Pred A} {x} →
          P x → Any P (return x)
return⁺ = here

return⁻ : ∀ {A} {P : Pred A} {x} →
          Any P (return x) → P x
return⁻ (here p)   = p
return⁻ (there ())

-- Introduction and elimination rules for concat.

concat⁺ : ∀ {A} {P : Pred A} {xss} →
          Any (Any P) xss → Any P (concat xss)
concat⁺ (here p)           = ++⁺ˡ p
concat⁺ (there {x = xs} p) = ++⁺ʳ xs (concat⁺ p)

concat⁻ : ∀ {A} {P : Pred A} xss →
          Any P (concat xss) → Any (Any P) xss
concat⁻ []               ()
concat⁻ ([]       ∷ xss) p         = there $ concat⁻ xss p
concat⁻ ((x ∷ xs) ∷ xss) (here p)  = here (here p)
concat⁻ ((x ∷ xs) ∷ xss) (there p)
  with concat⁻ (xs ∷ xss) p
... | here  p′ = here (there p′)
... | there p′ = there p′

-- Introduction and elimination rules for _>>=_.

>>=⁺ : ∀ {A B P xs} {f : A → List B} →
       Any (Any P ∘₀ f) xs → Any P (xs >>= f)
>>=⁺ = concat⁺ ∘ map⁺

>>=⁻ : ∀ {A B P} xs {f : A → List B} →
       Any P (xs >>= f) → Any (Any P ∘₀ f) xs
>>=⁻ _ = map⁻ ∘ concat⁻ _

-- Introduction and elimination rules for _⊛_.

⊛⁺ : ∀ {A B P} {fs : List (A → B)} {xs} →
     Any (λ f → Any (P ∘₀ f) xs) fs → Any P (fs ⊛ xs)
⊛⁺ = >>=⁺ ∘ Any.map (>>=⁺ ∘ Any.map return⁺)

⊛⁺′ : ∀ {A B P Q} {fs : List (A → B)} {xs} →
      Any (P ⟨→⟩ Q) fs → Any P xs → Any Q (fs ⊛ xs)
⊛⁺′ pq p = ⊛⁺ (Any.map (λ pq → Any.map (λ {x} → pq {x}) p) pq)

⊛⁻ : ∀ {A B P} (fs : List (A → B)) xs →
     Any P (fs ⊛ xs) → Any (λ f → Any (P ∘₀ f) xs) fs
⊛⁻ fs xs = Any.map (Any.map return⁻ ∘ >>=⁻ xs) ∘ >>=⁻ fs

-- Introduction and elimination rules for _⊗_.

⊗⁺ : ∀ {A B P} {xs : List A} {ys : List B} →
     Any (λ x → Any (λ y → P (x , y)) ys) xs → Any P (xs ⊗ ys)
⊗⁺ = ⊛⁺ ∘′ ⊛⁺ ∘′ return⁺

⊗⁺′ : ∀ {A B} {P : Pred A} {Q : Pred B} {xs ys} →
      Any P xs → Any Q ys → Any (P ⟨×⟩ Q) (xs ⊗ ys)
⊗⁺′ p q = ⊗⁺ (Any.map (λ p → Any.map (λ q → (p , q)) q) p)

⊗⁻ : ∀ {A B P} (xs : List A) (ys : List B) →
     Any P (xs ⊗ ys) → Any (λ x → Any (λ y → P (x , y)) ys) xs
⊗⁻ _ _ = return⁻ ∘ ⊛⁻ _ _ ∘ ⊛⁻ _ _

⊗⁻′ : ∀ {A B} {P : Pred A} {Q : Pred B} xs ys →
      Any (P ⟨×⟩ Q) (xs ⊗ ys) → Any P xs × Any Q ys
⊗⁻′ _ _ pq =
  (Any.map (proj₁ ∘ proj₂ ∘ Any.satisfied) lem ,
   (Any.map proj₂ $ proj₂ (Any.satisfied lem)))
  where lem = ⊗⁻ _ _ pq

-- Any and any are related via T.

any⁺ : ∀ {A} (p : A → Bool) {xs} →
       Any (T ∘₀ p) xs → T (any p xs)
any⁺ p (here  px)          = proj₂ T-∨ (inj₁ px)
any⁺ p (there {x = x} pxs) with p x
... | true  = _
... | false = any⁺ p pxs

any⁻ : ∀ {A} (p : A → Bool) xs →
       T (any p xs) → Any (T ∘₀ p) xs
any⁻ p []       ()
any⁻ p (x ∷ xs) px∷xs with inspect (p x)
any⁻ p (x ∷ xs) px∷xs | true  with-≡ eq = here (proj₂ T-≡ $
                                                  PropEq.sym eq)
any⁻ p (x ∷ xs) px∷xs | false with-≡ eq with p x
any⁻ p (x ∷ xs) pxs   | false with-≡ refl | .false =
  there (any⁻ p xs pxs)

------------------------------------------------------------------------
-- Lemmas related to _∈_, parameterised on underlying equalities

module Membership₁ (S : Setoid) where

  open Any.Membership S
  private
    open module S = Setoid S using (_≈_)
    open module [M] = Any.Membership (ListEq.Equality.setoid S)
      using () renaming (_∈_ to _[∈]_; _⊆_ to _[⊆]_)
    open module M≡ = Any.Membership-≡
      using () renaming (_∈_ to _∈≡_; _⊆_ to _⊆≡_)

  -- Any is monotone.

  mono : ∀ {P xs ys} →
         P Respects _≈_ → xs ⊆ ys → Any P xs → Any P ys
  mono resp xs⊆ys pxs with find pxs
  ... | (x , x∈xs , px) = lose resp (xs⊆ys x∈xs) px

  -- _++_ is monotone.

  _++-mono_ : ∀ {xs₁ xs₂ ys₁ ys₂} →
              xs₁ ⊆ ys₁ → xs₂ ⊆ ys₂ → xs₁ ++ xs₂ ⊆ ys₁ ++ ys₂
  _++-mono_ {ys₁ = ys₁} xs₁⊆ys₁ xs₂⊆ys₂ =
    [ ++⁺ˡ ∘ xs₁⊆ys₁ , ++⁺ʳ ys₁ ∘ xs₂⊆ys₂ ]′ ∘ ++⁻ _

  -- _++_ is idempotent.

  ++-idempotent : ∀ {xs} → xs ++ xs ⊆ xs
  ++-idempotent = [ id , id ]′ ∘ ++⁻ _

  -- Introduction and elimination rules for concat.

  concat-∈⁺ : ∀ {x xs xss} →
              x ∈ xs → xs [∈] xss → x ∈ concat xss
  concat-∈⁺ x∈xs xs∈xss =
    concat⁺ (Any.map (λ xs≈ys → P.reflexive xs≈ys x∈xs) xs∈xss)
    where module P = Preorder ⊆-preorder

  concat-∈⁻ : ∀ {x} xss → x ∈ concat xss →
              ∃ λ xs → x ∈ xs × xs [∈] xss
  concat-∈⁻ xss x∈ = Prod.map id swap $ [M].find (concat⁻ xss x∈)

  -- concat is monotone.

  concat-mono : ∀ {xss yss} →
                xss [⊆] yss → concat xss ⊆ concat yss
  concat-mono {xss = xss} xss⊆yss x∈ with concat-∈⁻ xss x∈
  ... | (xs , x∈xs , xs∈xss) = concat-∈⁺ x∈xs (xss⊆yss xs∈xss)

  -- any is monotone.

  any-mono : ∀ p → (T ∘₀ p) Respects _≈_ →
             ∀ {xs ys} → xs ⊆ ys → T (any p xs) → T (any p ys)
  any-mono p resp xs⊆ys = any⁺ p ∘ mono resp xs⊆ys ∘ any⁻ p _

  -- Introduction and elimination rules for map-with-∈.

  map-with-∈-∈⁺ : ∀ {A} {xs : List A}
                  (f : ∀ {x} → x ∈≡ xs → S.carrier) {x} →
                  (x∈xs : x ∈≡ xs) → f x∈xs ∈ M≡.map-with-∈ xs f
  map-with-∈-∈⁺ f (here refl)  = here S.refl
  map-with-∈-∈⁺ f (there x∈xs) = there $ map-with-∈-∈⁺ (f ∘ there) x∈xs

  map-with-∈-∈⁻ : ∀ {A} {xs : List A}
                  (f : ∀ {x} → x ∈≡ xs → S.carrier) {fx∈xs} →
                  fx∈xs ∈ M≡.map-with-∈ xs f →
                  ∃ λ x → Σ (x ∈≡ xs) λ x∈xs → fx∈xs ≈ f x∈xs
  map-with-∈-∈⁻ {xs = []}     f ()
  map-with-∈-∈⁻ {xs = y ∷ xs} f (here fx≈)   = (y , here refl , fx≈)
  map-with-∈-∈⁻ {xs = y ∷ xs} f (there x∈xs) =
    Prod.map id (Prod.map there id) $ map-with-∈-∈⁻ (f ∘ there) x∈xs

  -- map-with-∈ is monotone.

  map-with-∈-mono :
    ∀ {A} {xs : List A} {f : ∀ {x} → x ∈≡ xs → S.carrier}
          {ys : List A} {g : ∀ {x} → x ∈≡ ys → S.carrier} →
    (xs⊆ys : xs ⊆≡ ys) →
    (∀ {x} (x∈xs : x ∈≡ xs) → f x∈xs ≈ g (xs⊆ys x∈xs)) →
    M≡.map-with-∈ xs f ⊆ M≡.map-with-∈ ys g
  map-with-∈-mono {f = f} {g = g} xs⊆ys f≈g {fx∈xs} fx∈xs∈
    with map-with-∈-∈⁻ f fx∈xs∈
  ... | (x , x∈xs , fx∈xs≈) =
    Any.map (λ {y} g[xs⊆ys-x∈xs]≈y → begin
               fx∈xs           ≈⟨ fx∈xs≈ ⟩
               f x∈xs          ≈⟨ f≈g x∈xs ⟩
               g (xs⊆ys x∈xs)  ≈⟨ g[xs⊆ys-x∈xs]≈y ⟩
               y               ∎) $
            map-with-∈-∈⁺ g (xs⊆ys x∈xs)
    where open EqReasoning S

module Membership₂ (S₁ S₂ : Setoid) where

  private
    open module S₁ = Setoid S₁ using () renaming (_≈_ to _≈₁_)
    open module S₂ = Setoid S₂ using () renaming (_≈_ to _≈₂_)
    module L₂      = ListEq.Equality S₂
    open module M₁ = Any.Membership S₁
      using () renaming (_∈_ to _∈₁_; _⊆_ to _⊆₁_)
    open module M₂ = Any.Membership S₂
      using () renaming (_∈_ to _∈₂_; _⊆_ to _⊆₂_)
    open module M₁₂ = Any.Membership (S₁ ⇨ S₂)
      using () renaming (_∈_ to _∈₁₂_; _⊆_ to _⊆₁₂_)
    open Any.Membership (S₁ ×-setoid S₂)
      using () renaming (_⊆_ to _⊆₁,₂_)

  -- Introduction and elimination rules for map.

  map-∈⁺ : ∀ (f : S₁ ⟶ S₂) {x xs} →
          x ∈₁ xs → f ⟨$⟩ x ∈₂ map (_⟨$⟩_ f) xs
  map-∈⁺ f = map⁺ ∘ Any.map (pres f)

  map-∈⁻ : ∀ {f fx} xs →
           fx ∈₂ map f xs → ∃ λ x → x ∈₁ xs × fx ≈₂ f x
  map-∈⁻ _ fx∈ = M₁.find (map⁻ fx∈)

  -- map is monotone.

  map-mono : ∀ (f : S₁ ⟶ S₂) {xs ys} →
             xs ⊆₁ ys → map (_⟨$⟩_ f) xs ⊆₂ map (_⟨$⟩_ f) ys
  map-mono f xs⊆ys fx∈ with map-∈⁻ _ fx∈
  ... | (x , x∈ , eq) = Any.map (S₂.trans eq) (map-∈⁺ f (xs⊆ys x∈))

  -- Introduction and elimination rules for _>>=_.

  >>=-∈⁺ : ∀ (f : S₁ ⟶ L₂.setoid) {x y xs} →
           x ∈₁ xs → y ∈₂ f ⟨$⟩ x → y ∈₂ (xs >>= _⟨$⟩_ f)
  >>=-∈⁺ f x∈xs y∈fx =
    >>=⁺ (Any.map (flip M₂.∈-resp-list-≈ y∈fx ∘ pres f) x∈xs)

  >>=-∈⁻ : ∀ (f : S₁ ⟶ L₂.setoid) {y} xs →
           y ∈₂ (xs >>= _⟨$⟩_ f) → ∃ λ x → x ∈₁ xs × y ∈₂ f ⟨$⟩ x
  >>=-∈⁻ f xs y∈ = M₁.find (>>=⁻ xs y∈)

  -- _>>=_ is monotone.

  >>=-mono : ∀ (f g : S₁ ⟶ L₂.setoid) {xs ys} →
             xs ⊆₁ ys → (∀ {x} → f ⟨$⟩ x ⊆₂ g ⟨$⟩ x) →
             (xs >>= _⟨$⟩_ f) ⊆₂ (ys >>= _⟨$⟩_ g)
  >>=-mono f g {xs} xs⊆ys f⊆g z∈ with >>=-∈⁻ f xs z∈
  ... | (x , x∈xs , z∈fx) = >>=-∈⁺ g (xs⊆ys x∈xs) (f⊆g z∈fx)

  -- Introduction and elimination rules for _⊛_.

  private

    infixl 4 _⟨⊛⟩_

    _⟨⊛⟩_ : List (S₁ ⟶ S₂) → List S₁.carrier → List S₂.carrier
    fs ⟨⊛⟩ xs = map _⟨$⟩_ fs ⊛ xs

  ⊛-∈⁺ : ∀ f {fs x xs} →
         f ∈₁₂ fs → x ∈₁ xs → f ⟨$⟩ x ∈₂ fs ⟨⊛⟩ xs
  ⊛-∈⁺ _ f∈fs x∈xs =
    ⊛⁺′ (map⁺ (Any.map (λ f≈g x≈y → f≈g x≈y) f∈fs)) x∈xs

  ⊛-∈⁻ : ∀ fs xs {fx} → fx ∈₂ fs ⟨⊛⟩ xs →
         ∃₂ λ f x → f ∈₁₂ fs × x ∈₁ xs × fx ≈₂ f ⟨$⟩ x
  ⊛-∈⁻ fs xs fx∈ with M₁₂.find $ map⁻ (⊛⁻ (map _⟨$⟩_ fs) xs fx∈)
  ... | (f , f∈fs , x∈) with M₁.find x∈
  ...   | (x , x∈xs , fx≈fx) = (f , x , f∈fs , x∈xs , fx≈fx)

  -- _⊛_ is monotone.

  _⊛-mono_ : ∀ {fs gs xs ys} →
             fs ⊆₁₂ gs → xs ⊆₁ ys → fs ⟨⊛⟩ xs ⊆₂ gs ⟨⊛⟩ ys
  _⊛-mono_ {fs = fs} {xs = xs} fs⊆gs xs⊆ys fx∈ with ⊛-∈⁻ fs xs fx∈
  ... | (f , x , f∈fs , x∈xs , fx≈fx) =
    Any.map (S₂.trans fx≈fx) $ ⊛-∈⁺ f (fs⊆gs {f} f∈fs) (xs⊆ys x∈xs)

  -- _⊗_ is monotone.

  _⊗-mono_ : ∀ {xs₁ xs₂ ys₁ ys₂} →
             xs₁ ⊆₁ ys₁ → xs₂ ⊆₂ ys₂ → (xs₁ ⊗ xs₂) ⊆₁,₂ (ys₁ ⊗ ys₂)
  _⊗-mono_ {xs₁ = xs₁} {xs₂} xs₁⊆ys₁ xs₂⊆ys₂ {x , y} x,y∈
    with ⊗⁻′ {P = _≈₁_ x} {Q = _≈₂_ y} xs₁ xs₂ x,y∈
  ... | (x∈ , y∈) = ⊗⁺′ (xs₁⊆ys₁ x∈) (xs₂⊆ys₂ y∈)

------------------------------------------------------------------------
-- Lemmas related to the variant of _∈_ which is defined using
-- propositional equality

module Membership-≡ where

  open Any.Membership-≡
  private
    module P {A} = ListEq.PropositionalEquality {A}
    open module M₁ {A} = Membership₁ (PropEq.setoid A) public
      using (_++-mono_; ++-idempotent;
             map-with-∈-∈⁺; map-with-∈-∈⁻; map-with-∈-mono)
    open module M₂ {A} {B} =
      Membership₂ (PropEq.setoid A) (PropEq.setoid B) public
      using (map-∈⁻)

  -- Any is monotone.

  mono : ∀ {A xs ys} {P : Pred A} → xs ⊆ ys → Any P xs → Any P ys
  mono {P = P} = M₁.mono (PropEq.subst P)

  -- Introduction and elimination rules for concat.

  concat-∈⁺ : ∀ {A} {x : A} {xs xss} →
              x ∈ xs → xs ∈ xss → x ∈ concat xss
  concat-∈⁺ x∈xs = M₁.concat-∈⁺ x∈xs ∘ Any.map P.reflexive

  concat-∈⁻ : ∀ {A} {x : A} xss →
              x ∈ concat xss → ∃ λ xs → x ∈ xs × xs ∈ xss
  concat-∈⁻ xss x∈ =
    Prod.map id (Prod.map id (Any.map P.≈⇒≡)) $ M₁.concat-∈⁻ xss x∈

  -- concat is monotone.

  concat-mono : ∀ {A} {xss yss : List (List A)} →
                xss ⊆ yss → concat xss ⊆ concat yss
  concat-mono xss⊆yss =
    M₁.concat-mono (Any.map P.reflexive ∘ xss⊆yss ∘ Any.map P.≈⇒≡)

  -- any is monotone.

  any-mono : ∀ {A} (p : A → Bool) {xs ys} →
             xs ⊆ ys → T (any p xs) → T (any p ys)
  any-mono p = M₁.any-mono p (PropEq.subst (T ∘₀ p))

  -- Introduction rule for map.

  map-∈⁺ : ∀ {A B} {f : A → B} {x xs} →
           x ∈ xs → f x ∈ map f xs
  map-∈⁺ {f = f} = M₂.map-∈⁺ (PropEq.→-to-⟶ f)

  -- map is monotone.

  map-mono : ∀ {A B} {f : A → B} {xs ys} →
             xs ⊆ ys → map f xs ⊆ map f ys
  map-mono {f = f} = M₂.map-mono (PropEq.→-to-⟶ f)

  -- Introduction and elimination rules for _>>=_.

  private

    [→-to-⟶] : ∀ {A B} → (A → List B) →
               PropEq.setoid A ⟶
               ListEq.Equality.setoid (PropEq.setoid B)
    [→-to-⟶] f =
      record { _⟨$⟩_ = f; pres = P.reflexive ∘ PropEq.cong f }

  >>=-∈⁺ : ∀ {A B} (f : A → List B) {x y xs} →
           x ∈ xs → y ∈ f x → y ∈ (xs >>= f)
  >>=-∈⁺ f = M₂.>>=-∈⁺ ([→-to-⟶] f)

  >>=-∈⁻ : ∀ {A B} (f : A → List B) {y} xs →
           y ∈ (xs >>= f) → ∃ λ x → x ∈ xs × y ∈ f x
  >>=-∈⁻ f = M₂.>>=-∈⁻ ([→-to-⟶] f)

  -- _>>=_ is monotone.

  _>>=-mono_ : ∀ {A B} {f g : A → List B} {xs ys} →
               xs ⊆ ys → (∀ {x} → f x ⊆ g x) →
               (xs >>= f) ⊆ (ys >>= g)
  _>>=-mono_ {f = f} {g} = M₂.>>=-mono ([→-to-⟶] f) ([→-to-⟶] g)

  -- Introduction and elimination rules for _⊛_.

  ⊛-∈⁺ : ∀ {A B} {fs : List (A → B)} {xs f x} →
         f ∈ fs → x ∈ xs → f x ∈ fs ⊛ xs
  ⊛-∈⁺ f∈fs x∈xs =
    ⊛⁺′ (Any.map (λ f≡g x≡y → PropEq.cong₂ _$_ f≡g x≡y) f∈fs) x∈xs

  ⊛-∈⁻ : ∀ {A B} (fs : List (A → B)) xs {fx} →
         fx ∈ fs ⊛ xs → ∃₂ λ f x → f ∈ fs × x ∈ xs × fx ≡ f x
  ⊛-∈⁻ fs xs fx∈ with find $ ⊛⁻ fs xs fx∈
  ... | (f , f∈fs , x∈) with find x∈
  ...   | (x , x∈xs , fx≡fx) = (f , x , f∈fs , x∈xs , fx≡fx)

  -- _⊛_ is monotone.

  _⊛-mono_ : ∀ {A B} {fs gs : List (A → B)} {xs ys} →
             fs ⊆ gs → xs ⊆ ys → fs ⊛ xs ⊆ gs ⊛ ys
  _⊛-mono_ {fs = fs} {xs = xs} fs⊆gs xs⊆ys fx∈ with ⊛-∈⁻ fs xs fx∈
  ... | (f , x , f∈fs , x∈xs , refl) =
    ⊛-∈⁺ (fs⊆gs f∈fs) (xs⊆ys x∈xs)

  -- Introduction and elimination rules for _⊗_.

  private

    lemma₁ : ∀ {A B} {p q : A × B} →
             (p ⟨ _≡_ on₁ proj₁ ⟩₁ q) × (p ⟨ _≡_ on₁ proj₂ ⟩₁ q) → p ≡ q
    lemma₁ {p = (x , y)} {q = (.x , .y)} (refl , refl) = refl

    lemma₂ : ∀ {A B} {p q : A × B} →
             p ≡ q → (p ⟨ _≡_ on₁ proj₁ ⟩₁ q) × (p ⟨ _≡_ on₁ proj₂ ⟩₁ q)
    lemma₂ = < PropEq.cong proj₁ , PropEq.cong proj₂ >

  ⊗-∈⁺ : ∀ {A B} {xs : List A} {ys : List B} {x y} →
         x ∈ xs → y ∈ ys → (x , y) ∈ (xs ⊗ ys)
  ⊗-∈⁺ x∈xs y∈ys = Any.map lemma₁ (⊗⁺′ x∈xs y∈ys)

  ⊗-∈⁻ : ∀ {A B} (xs : List A) (ys : List B) {p} →
         p ∈ (xs ⊗ ys) → proj₁ p ∈ xs × proj₂ p ∈ ys
  ⊗-∈⁻ xs ys = ⊗⁻′ xs ys ∘ Any.map lemma₂

  -- _⊗_ is monotone.

  _⊗-mono_ : ∀ {A B} {xs₁ ys₁ : List A} {xs₂ ys₂ : List B} →
             xs₁ ⊆ ys₁ → xs₂ ⊆ ys₂ → (xs₁ ⊗ xs₂) ⊆ (ys₁ ⊗ ys₂)
  _⊗-mono_ xs₁⊆ys₁ xs₂⊆ys₂ {p} =
    Any.map lemma₁ ∘ M₂._⊗-mono_ xs₁⊆ys₁ xs₂⊆ys₂ {p} ∘ Any.map lemma₂

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- Andreas, 2021-08-18, issue #5506 reported by alexarice

-- A crash in the forcing methodology introduced in 2.6.1
-- that surfaced with the removal of auto-inlining in 2.6.2.

-- {-# OPTIONS --no-forcing #-}   -- fixes
-- {-# OPTIONS --auto-inline #-}  -- fixes

{-# OPTIONS -v tc.lhs.unify.force:100 #-}

open import Agda.Builtin.Nat

data Unit : Set where
  unit : Unit

data Ctx : Nat → Set where  -- index needed
  cons : (m : Nat) (A : Unit) → Ctx (suc m)

mutual

  data P : (n : Nat) (Γ : Ctx n) → Set

  -- Needs to be mutual
  {-# NOINLINE getFocus #-}
  getFocus : (n : Nat) (A : Unit) → Unit
  getFocus n A = A  -- needs to be A, not unit

  data P where
    c : (n : Nat)  -- n is forced
        (A : Unit)
      → P (suc n) (cons n (getFocus n A))

test : (n : Nat) (Γ : Ctx n) → P n Γ → Nat
test n Γ (c m A) = n + m
  -- ^ n := suc m fixes the issue

-- WAS:
-- Panic: Pattern match failure in do expression at
-- src/full/Agda/TypeChecking/Rules/LHS/Unify.hs:1313:7-14
-- when checking that the pattern c _ _ _ _ has type P n Γ

-- Expect: type-checks without errors.

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Library.Data.Either where

open import Light.Level using (Level ; Setω ; _⊔_)
open import Light.Variable.Sets
open import Light.Variable.Levels

record Dependencies : Setω where

record Library (dependencies : Dependencies) : Setω where
      field
            ℓf : Level → Level → Level
            Either : Set aℓ → Set bℓ → Set (ℓf aℓ bℓ)
            left : 𝕒 → Either 𝕒 𝕓
            right : 𝕓 → Either 𝕒 𝕓
open Library ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
f : Set → Set

module _ (A : Set) where

  mutual

    g : Set
    g = h

    h : Set
    h = A

f = g

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

-- The One Category is also a -2-Category
module Categories.Minus2-Category.Instance.One where

open import Categories.Minus2-Category
open import Categories.Category.Instance.One

-- Proof is trivial
⊤-is-2-Category : ∀ {o ℓ e} → -2-Category {o} {ℓ} {e}
⊤-is-2-Category = record  { cat = One }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Oscar.Data.Term {𝔣} (FunctionName : Set 𝔣) where

open import Oscar.Data.Equality
open import Oscar.Data.Fin
open import Oscar.Data.Nat
open import Oscar.Data.Vec
open import Oscar.Function
open import Oscar.Relation

mutual

  Terms : Nat → Nat → Set 𝔣
  Terms N m = Vec (Term m) N

  data Term (m : Nat) : Set 𝔣 where
    i : (x : Fin m) → Term m
    leaf : Term m
    _fork_ : (s t : Term m) → Term m
    function : FunctionName → ∀ {N} → Terms N m → Term m


text:
module L.Base.Sigma.Properties where

open import L.Base.Sigma.Core

choice : ∀{a b c} {A : Set a} {B : Set b} → {C : A → B → Set c}
         → ((x : A) → Σ B (λ y → C x y)) → Σ (A → B) (λ f → (a : A) → C a (f a))
choice = λ F → ((λ x → fst (F x)) , λ a → snd (F a))

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
open import Data.Product using ( ∃ ; _×_ ; _,_ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
open import Relation.Nullary using ( ¬_ )
open import Relation.Unary using ( _∈_ ; ∅ )
open import Web.Semantic.DL.Signature using ( Signature ; CN ; RN )
open import Web.Semantic.Util using ( Setoid ; Subset ; _∘_ ; False )

module Web.Semantic.DL.TBox.Interp where

data Interp (Σ : Signature) : Set₁ where
  interp :
    (Δ : Set) →
    (_≈_ : Δ → Δ → Set) →
    (ref : ∀ {x} → (x ≈ x)) →
    (sym : ∀ {x y} → (x ≈ y) → (y ≈ x)) →
    (trans : ∀ {x y z} → (x ≈ y) → (y ≈ z) → (x ≈ z)) →
    (con : CN Σ → Subset Δ) →
    (rol : RN Σ → Subset (Δ × Δ)) →
    (con-≈ : ∀ {x y} c → (x ∈ con c) → (x ≈ y) → (y ∈ con c)) →
    (rol-≈ : ∀ {w x y z} r → (w ≈ x) → ((x , y) ∈ rol r) → (y ≈ z) → ((w , z) ∈ rol r)) →
    Interp Σ

Δ : ∀ {Σ} → Interp Σ → Set
Δ (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = Δ

_⊨_≈_ : ∀ {Σ} → (I : Interp Σ) → (Δ I) → (Δ I) → Set
_⊨_≈_ (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = _≈_

≈-refl : ∀ {Σ} → (I : Interp Σ) → ∀ {x} → (I ⊨ x ≈ x)
≈-refl (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = ref

≈-sym : ∀ {Σ} → (I : Interp Σ) → ∀ {x y} → (I ⊨ x ≈ y) → (I ⊨ y ≈ x)
≈-sym (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = sym

≈-trans : ∀ {Σ} → (I : Interp Σ) → ∀ {x y z} → (I ⊨ x ≈ y) → (I ⊨ y ≈ z) → (I ⊨ x ≈ z)
≈-trans (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = trans

con : ∀ {Σ} → (I : Interp Σ) → CN Σ → Subset (Δ I)
con (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = con

rol : ∀ {Σ} → (I : Interp Σ) → RN Σ → Subset (Δ I × Δ I)
rol (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = rol

con-≈ : ∀ {Σ} → (I : Interp Σ) → ∀ {x y} c → (x ∈ con I c) → (I ⊨ x ≈ y) → (y ∈ con I c)
con-≈ (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = con-≈

rol-≈ : ∀ {Σ} → (I : Interp Σ) → ∀ {w x y z} r → (I ⊨ w ≈ x) → ((x , y) ∈ rol I r) → (I ⊨ y ≈ z) → ((w , z) ∈ rol I r)
rol-≈ (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = rol-≈

_⊨_≉_ : ∀ {Σ} → (I : Interp Σ) → (Δ I) → (Δ I) → Set
I ⊨ x ≉ y = ¬(I ⊨ x ≈ y)

emp : ∀ {Σ} → Interp Σ
emp = interp False (λ ()) (λ {}) (λ {}) (λ {}) (λ c → ∅) (λ r → ∅) (λ {}) (λ {})

≈-refl′ : ∀ {Σ} (I : Interp Σ) → ∀ {x y} → (x ≡ y) → (I ⊨ x ≈ y)
≈-refl′ I refl = ≈-refl I

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
module InductiveAndCoinductiveConstructors where

open import Common.Coinduction

record ⊤ : Set where

data _×_ (A : Set) (B : Set) : Set where
  _,_ : (x : A) (y : B) → A × B

data Stream (A : Set) : Set where
  _≺_ : (x : A) (xs : ∞ (Stream A)) → Stream A

data U : Set where
  stream : (a : U) → U
  _⊗_    : (a b : U) → U
  unit   : U

El : U → Set
El (stream a) = Stream (El a)
El (a ⊗ b)    = El a × El b
El unit       = ⊤

mutual

  data WHNF : U → Set where
    _≺_  : ∀ {a} → El a → Prog (stream a) → WHNF (stream a)
    _,_  : ∀ {a b} → WHNF a → WHNF b → WHNF (a ⊗ b)

  data Prog : U → Set where
    ↓_  : ∀ {a} → ∞ (WHNF a) → Prog a
    fst : ∀ {a b} → Prog (a ⊗ b) → Prog a
    snd : ∀ {a b} → Prog (a ⊗ b) → Prog b
    lab : Prog (stream unit) → Prog (stream (stream unit)) →
          Prog (stream unit ⊗ stream (stream unit))

whnf : ∀ {a} → Prog a → WHNF a
whnf (↓ w) = ♭ w
whnf (fst p) with whnf p
... | (x , y) = x
whnf (snd p) with whnf p
... | (x , y) = y
whnf (lab xs lss) with whnf xs | whnf lss
... | _ ≺ xs′ | (x ≺ ls) ≺ lss′ =
  ((_ ≺ fst (lab xs′ lss′)) , (♭ ls ≺ snd (lab xs′ lss′)))

⟦_⟧ : Prog (stream unit) → Stream ⊤
⟦ p ⟧ with whnf p
... | x ≺ xs = x ≺ ♯ ⟦ xs ⟧

data _≈_ : Stream ⊤ → Stream ⊤ → Set where
  cons : ∀ {xs xs′} → ∞ ((♭ xs) ≈ (♭ xs′)) → (_ ≺ xs) ≈ (_ ≺ xs′)

lemma : ∀ xs lss → ⟦ fst (lab xs lss) ⟧ ≈ ⟦ xs ⟧
lemma xs lss with whnf xs | whnf lss
... | _ ≺ xs′ | (x ≺ ls) ≺ lss′ = cons (♯ lemma xs′ lss′)

label : Prog (stream unit) → Stream ⊤ →
        Prog (stream unit ⊗ stream (stream unit))
label xs ls = lab xs (↓ (♯ (ls ≺ snd (label xs ls))))

shape-preserved : ∀ xs ls → ⟦ fst (label xs ls) ⟧ ≈ ⟦ xs ⟧
shape-preserved xs ls = lemma xs _

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
open import Agda.Builtin.Bool

f : Bool → Bool
f x =
  let id : Bool → Bool
      id b = {!!}
  in id x


text:
module Aexamples where

open import Data.List hiding (reverse)
open import Data.List.All
open import Data.Nat

open import Typing
open import Syntax
open import Async

{-
Lithmus test for asynchronous operations
A thread send something to an asynchronous channel and receives it afterwards.
-}
aex1 : Expr [] TUnit
aex1 = letbind [] (anew [] (delay send!))
       (letpair (left []) (here [])
       (letbind (left (rght [])) (aclose (here []))
       (await (there UUnit (here [])))))

-- just replace synchronous operations by the asynchronous ones
asyncex1 : Expr [] TUnit
asyncex1 =
  letbind [] (anew [] (delay send!))
  (letpair (left []) (here [])
  (letbind (rght (left []))
           (fork (await (here [])))
  (aclose (there UUnit (here [])))))

-- sending and receiving
asyncex2 : Expr [] TUnit
asyncex2 =
  letbind [] (anew [] (delay (send TInt (delay send!))))
  (letpair (left []) (here [])
  (letbind (left (rght []))
           (fork (letbind (rght []) (nat [] 42)
                 (letbind (left (left [])) (asend (rght (left [])) (here []) (here []))
                 (letbind (left []) (aclose (here []))
                 (var (here []))))))
  (letbind (rght (left [])) (arecv (here []))
  (letpair (left (rght [])) (here [])
  (letbind (left (left (rght []))) (await (here (UInt ∷ [])))
  (var (here (UUnit ∷ []))))))))

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


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

open import LogicalFormulae
open import Orders.WellFounded.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Semirings.Definition

module Numbers.Naturals.Order.WellFounded where
open Semiring ℕSemiring

<NWellfounded : WellFounded _<N_
<NWellfounded = λ x → access (go x)
  where
    lemma : {a b c : ℕ} → a <N b → b <N succ c → a <N c
    lemma {a} {b} {c} (le y succYAeqB) (le z zbEqC') = le (y +N z) p
      where
        zbEqC : z +N b ≡ c
        zSuccYAEqC : z +N (succ y +N a) ≡ c
        zSuccYAEqC' : z +N (succ (y +N a)) ≡ c
        zSuccYAEqC'' : succ (z +N (y +N a)) ≡ c
        zSuccYAEqC''' : succ ((z +N y) +N a) ≡ c
        p : succ ((y +N z) +N a) ≡ c
        p = identityOfIndiscernablesLeft _≡_ zSuccYAEqC''' (applyEquality (λ n → succ (n +N a)) (commutative z y))
        zSuccYAEqC''' = identityOfIndiscernablesLeft _≡_ zSuccYAEqC'' (applyEquality succ (+Associative z y a))
        zSuccYAEqC'' = identityOfIndiscernablesLeft _≡_ zSuccYAEqC' (succExtracts z (y +N a))
        zSuccYAEqC' = identityOfIndiscernablesLeft _≡_ zSuccYAEqC (applyEquality (λ r → z +N r) refl)
        zbEqC = succInjective zbEqC'
        zSuccYAEqC = identityOfIndiscernablesLeft _≡_ zbEqC (applyEquality (λ r → z +N r) (equalityCommutative succYAeqB))
    go : ∀ n m → m <N n → Accessible _<N_ m
    go zero m (le x ())
    go (succ n) zero mLessN = access (λ y ())
    go (succ n) (succ m) smLessSN = access (λ o (oLessSM : o <N succ m) → go n o (lemma oLessSM smLessSN))


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Base.PKCS

open import LibraBFT.Yasm.Types

-- This module defines the types used to define a SystemModel.
module LibraBFT.Yasm.Base (ℓ-PeerState : Level) where
 -- Our system is configured through a value of type
 -- SystemParameters where we specify:
 record SystemParameters : Set (ℓ+1 ℓ-PeerState) where
  constructor mkSysParms
  field
    PeerId    : Set
    _≟PeerId_ : ∀ (p₁ p₂ : PeerId) → Dec (p₁ ≡ p₂)
    Genesis   : Set
    genInfo   : Genesis    -- The same genesis information is given to any uninitialised peer before
                           -- it can handle any messages.
    PeerState : Set ℓ-PeerState
    initPS    : PeerState  -- Represents an uninitialised PeerState, about which we know nothing whatsoever
    Msg       : Set
    Part      : Set -- Types of interest that can be represented in Msgs

    -- The messages must be able to carry signatures
    instance Part-sig : WithSig Part

    -- A relation specifying what Parts are included in a Msg.
    _⊂Msg_       : Part → Msg → Set

    -- A relation specifying what Signatures are included in genInfo
    ∈GenInfo     : Signature → Set

    -- Initializes a potentially-empty state with an EpochConfig
    init : PeerId → Genesis → PeerState × List (Action Msg)

    -- Handles a message on a previously initialized peer.
    handle : PeerId → Msg → PeerState → PeerState × List (Action Msg)

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
module NotLeqSort where

data Err : Set where
  err : (A : Set) -> Err


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Direct-Sum.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Algebra.AbGroup

-- Conventions :
-- Elements of the index are named r, s, t...
-- Elements of the groups are called a, b, c...
-- Elements of the direct sum are named x, y, z...
-- Elements in the fiber of Q x, Q y are called xs, ys...

private variable
  ℓ ℓ' ℓ'' : Level

data ⊕ (Idx : Type ℓ) (P : Idx → Type ℓ') (AGP : (r : Idx) → AbGroupStr (P r)) : Type (ℓ-max ℓ ℓ')  where
  -- elements
  neutral      : ⊕ Idx P AGP
  base         : (r : Idx) → (P r) → ⊕ Idx P AGP
  _add_        : ⊕ Idx P AGP → ⊕ Idx P AGP → ⊕ Idx P AGP
  -- eq group
  addAssoc     : (x y z : ⊕ Idx P AGP) → x add (y add z) ≡ (x add y) add z
  addRid       : (x : ⊕ Idx P AGP)     → x add neutral ≡ x
  addComm      : (x y : ⊕ Idx P AGP)   → x add y ≡ y add x
  -- eq base
  base-neutral : (r : Idx)                → base r (AbGroupStr.0g (AGP r)) ≡ neutral
  base-add     : (r : Idx) → (a b : P r) → (base r a) add (base r b) ≡ base r (AbGroupStr._+_ (AGP r) a b)
  -- set
  trunc        : isSet (⊕ Idx P AGP)

module _ (Idx : Type ℓ) (P : Idx → Type ℓ') (AGP : (r : Idx) → AbGroupStr (P r)) where

  module DS-Ind-Set
    (Q            : (x : ⊕ Idx P AGP) → Type ℓ'')
    (issd         : (x : ⊕ Idx P AGP) → isSet (Q x))
    -- elements
    (neutral*     : Q neutral)
    (base*        : (r : Idx) → (a : P r) → Q (base r a))
    (_add*_       : {x y : ⊕ Idx P AGP} → Q x → Q y → Q (x add y))
    -- eq group
    (addAssoc*    : {x y z : ⊕ Idx P AGP} → (xs : Q x) → (ys : Q y) → (zs : Q z)
                    → PathP ( λ i →  Q ( addAssoc x y z i)) (xs add* (ys add* zs)) ((xs add* ys) add* zs))
    (addRid*      : {x : ⊕ Idx P AGP} → (xs : Q x)
                    → PathP (λ i → Q (addRid x i)) (xs add* neutral*) xs )
    (addComm*     : {x y : ⊕ Idx P AGP} → (xs : Q x) → (ys : Q y)
                    → PathP (λ i → Q (addComm x y i)) (xs add* ys) (ys add* xs))
    -- -- eq base
    (base-neutral* : (r : Idx)
                     → PathP (λ i → Q (base-neutral r i)) (base* r (AbGroupStr.0g (AGP r))) neutral*)
    (base-add*     : (r : Idx) → (a b : P r)
                     → PathP (λ i → Q (base-add r a b i)) ((base* r a) add* (base* r b)) (base* r (AbGroupStr._+_ (AGP r) a b)))
    where

    f : (x : ⊕ Idx P AGP) → Q x
    f neutral    = neutral*
    f (base r a) = base* r a
    f (x add y)  = (f x) add* (f y)
    f (addAssoc x y z i)  = addAssoc* (f x) (f y) (f z) i
    f (addRid x i)        = addRid* (f x) i
    f (addComm x y i)     = addComm* (f x) (f y) i
    f (base-neutral r i)  = base-neutral* r i
    f (base-add r a b i)  = base-add* r a b i
    f (trunc x y p q i j) = isOfHLevel→isOfHLevelDep 2 (issd)  (f x) (f y) (cong f p) (cong f q) (trunc x y p q) i j

  module DS-Rec-Set
    (B : Type ℓ'')
    (iss : isSet(B))
    (neutral* : B)
    (base*    : (r : Idx) → P r → B)
    (_add*_   : B → B → B)
    (addAssoc*     : (xs ys zs : B) → (xs add* (ys add* zs)) ≡ ((xs add* ys) add* zs))
    (addRid*       : (xs : B)       → xs add* neutral* ≡ xs)
    (addComm*      : (xs ys : B)    → xs add* ys ≡ ys add* xs)
    (base-neutral* : (r : Idx)                → base* r (AbGroupStr.0g (AGP r)) ≡ neutral*)
    (base-add*     : (r : Idx) → (a b : P r) → (base* r a) add* (base* r b) ≡ base* r (AbGroupStr._+_ (AGP r) a b))
    where

    f : ⊕ Idx P AGP → B
    f z = DS-Ind-Set.f (λ _ → B) (λ _ → iss) neutral* base* _add*_ addAssoc* addRid* addComm* base-neutral* base-add* z

  module DS-Ind-Prop
    (Q            : (x : ⊕ Idx P AGP) → Type ℓ'')
    (ispd         : (x : ⊕ Idx P AGP) → isProp (Q x))
    -- elements
    (neutral*     : Q neutral)
    (base*        : (r : Idx) → (a : P r) → Q (base r a))
    (_add*_       : {x y : ⊕ Idx P AGP} → Q x → Q y → Q (x add y))
    where

    f : (x : ⊕ Idx P AGP) → Q x
    f x = DS-Ind-Set.f Q (λ x → isProp→isSet (ispd x)) neutral* base* _add*_
          (λ {x} {y} {z} xs ys zs → toPathP (ispd _ (transport (λ i → Q (addAssoc x y z i)) (xs add* (ys add* zs))) ((xs add* ys) add* zs)))
          (λ {x} xs               → toPathP (ispd _ (transport (λ i → Q (addRid x i))       (xs add* neutral*)) xs))
          (λ {x} {y} xs ys        → toPathP (ispd _ (transport (λ i → Q (addComm x y i))    (xs add* ys)) (ys add* xs)))
          (λ r                    → toPathP (ispd _ (transport (λ i → Q (base-neutral r i)) (base* r (AbGroupStr.0g (AGP r)))) neutral*))
          (λ r a b                → toPathP (ispd _ (transport (λ i → Q (base-add r a b i)) ((base* r a) add* (base* r b))) (base* r (AbGroupStr._+_ (AGP r) a b)  )))
          x

  module DS-Rec-Prop
    (B        : Type ℓ'')
    (isp      : isProp B)
    (neutral* : B)
    (base*    : (r : Idx) → P r → B)
    (_add*_   : B → B → B)
    where

    f : ⊕ Idx P AGP → B
    f x = DS-Ind-Prop.f (λ _ → B) (λ _ → isp) neutral* base* _add*_ x

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{-# OPTIONS --safe #-}
module CF.Syntax.Hoisted where

open import Level
open import Data.List

open import Relation.Unary hiding (_⊢_)
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax

open import CF.Types
open import CF.Contexts.Lexical
open import CF.Syntax using (module Statements)
open import CF.Syntax using (Exp) public

mutual
  Stmt = Statements.Statement Block

  {- This is Bigstar, but Agda cannot termination check that -}
  data Block (r : Ty) : Pred Ctx 0ℓ where
    nil  : ε[ Block r ]
    cons : ∀[ Stmt r ✴ Block r ⇒ Block r ]

open import Relation.Unary.PredicateTransformer hiding (_⍮_)
open import Data.Product

-- make constructors visible
open Exp public
open Statements Block public
open CoDeBruijn public
open import CF.Contexts.Lexical using (_⊢_) public


text:
------------------------------------------------------------------------------
-- Incompatible options
------------------------------------------------------------------------------

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

-- The @--schematic-propositional-functions@ and
-- @--without-predicate-symbols@ options are incompatible.

module SchematicPropositionalFunctionsWithoutPredicateSymbols where

postulate D : Set

postulate id : {P : D → Set}{x : D} → P x → P x
{-# ATP prove id #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Structure.Type.Identity.Proofs.Multi where

open import Data.Tuple.Raise
open import Data.Tuple.RaiseTypeᵣ
import      Data.Tuple.RaiseTypeᵣ.Functions as RaiseType
import      Lvl
open import Functional using (_→ᶠ_ ; id ; _on₂_ ; swap ; _$_ ; apply)
open import Function.Multi
import      Function.Multi.Functions as Multi
open import Logic
open import Logic.Propositional
open import Logic.Propositional.Proofs.Structures
open import Numeral.Natural
open import Structure.Function
open import Structure.Function.Multi
open import Structure.Setoid using (Equiv ; intro) renaming (_≡_ to _≡ₛ_)
open import Structure.Relator.Equivalence
import      Structure.Relator.Names as Names
open import Structure.Relator.Properties
open import Structure.Relator.Properties.Proofs
open import Structure.Relator
open import Structure.Type.Identity
open import Structure.Type.Identity.Proofs
open import Syntax.Function
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ₁ ℓₑ₂ ℓₑ ℓₘₑ ℓₚ ℓₒ : Lvl.Level
private variable T A B : Type{ℓ}
private variable x y : T
private variable _≡_ _▫_ : T → T → Stmt{ℓ}

module _
  {B : Type{ℓ}}
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  -- {_≡_ : ∀{ℓ}{T : Type{ℓ}} → T → T → Stmt{ℓₑ}}
  -- ⦃ minRefl : ∀{ℓ}{T : Type{ℓ}} → MinimalReflexiveRelation{ℓₚ = ℓₑ₂}(_≡_ {T = T}) ⦄ -- TODO: Temporary
  where

  minimal-reflection-to-function₊ : ∀{n}{ℓ𝓈 ℓ𝓈ₑ}{As : Types{n}(ℓ𝓈)}{f : As ⇉ B} → Multi.quantifier₊ᵢₙₛₜ(n) {!!} (Multi.composeᵢₙₛₜ(n) (apply f) (Names.Function₊ ⦃ equiv-B = equiv-B ⦄ (n) {ℓ𝓈ₑ = ℓ𝓈ₑ} {As = As}))
  {-minimal-reflection-to-function₊ {0}       {f = f} = reflexivity(_≡ₛ_)
  minimal-reflection-to-function₊ {1}       {f = f} = congruence₁(f) ⦃ minimal-reflection-to-function ⦃ minRefl = {!!} ⦄ ⦄
  minimal-reflection-to-function₊ {𝐒(𝐒(n))} {f = f} = {!!}
-}

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:
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Multidimensional.Data.Extra.Nat.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat
open import Cubical.Data.Empty

open import Cubical.Relation.Nullary

open import Multidimensional.Data.Extra.Nat.Base

sucnsuc : (n m : ℕ) → sucn n (suc m) ≡ suc (sucn n m)
sucnsuc zero m = refl
sucnsuc (suc n) m =
    sucn (suc n) (suc m) ≡⟨ refl ⟩
    suc (sucn n (suc m)) ≡⟨ cong suc (sucnsuc n m) ⟩
    suc (suc (sucn n m)) ∎

doublePred : (n : ℕ) → doubleℕ (predℕ n) ≡ predℕ (predℕ (doubleℕ n))
doublePred zero = refl
doublePred (suc n) = refl

sucPred : (n : ℕ) → ¬ (n ≡ zero) → suc (predℕ n) ≡ n
sucPred zero 0≠0 = ⊥-elim (0≠0 refl)
sucPred (suc n) sucn≠0 = refl

doubleDoubles : (n m : ℕ) → doubleℕ (doublesℕ n m) ≡ doublesℕ (suc n) m
doubleDoubles zero m = refl
doubleDoubles (suc n) m = doubleDoubles n (doubleℕ m)

doublePos : (n : ℕ) → ¬ (n ≡ 0) → ¬ (doubleℕ n ≡ 0)
doublePos zero 0≠0 = ⊥-elim (0≠0 refl)
doublePos (suc n) sn≠0 = snotz

doublesPos : (n m : ℕ) → ¬ (m ≡ 0) → ¬ (doublesℕ n m ≡ 0)
doublesPos zero m m≠0 = m≠0
doublesPos (suc n) m m≠0 = doublesPos n (doubleℕ m) (doublePos m (m≠0))

predDoublePos : (n : ℕ) → ¬ (n ≡ 0) → ¬ (predℕ (doubleℕ n)) ≡ 0
predDoublePos zero n≠0 = ⊥-elim (n≠0 refl)
predDoublePos (suc n) sn≠0 = snotz

doubleDoublesOne≠0 : (n : ℕ) → ¬ (doubleℕ (doublesℕ n (suc zero)) ≡ 0)
doubleDoublesOne≠0 zero = snotz
doubleDoublesOne≠0 (suc n) = doublePos (doublesℕ n 2) (doublesPos n 2 (snotz))

predDoubleDoublesOne≠0 : (n : ℕ) → ¬ (predℕ (doubleℕ (doublesℕ n (suc zero))) ≡ 0)
predDoubleDoublesOne≠0 zero = snotz
predDoubleDoublesOne≠0 (suc n) = predDoublePos (doublesℕ n 2) (doublesPos n 2 snotz)

doublesZero : (n : ℕ) → doublesℕ n zero ≡ zero
doublesZero zero = refl
doublesZero (suc n) = doublesZero n

doubleSucn : (i n : ℕ) →  doubleℕ (sucn i n) ≡ sucn (doubleℕ i) (doubleℕ n)
doubleSucn zero n = refl
doubleSucn (suc i) n =
    suc (suc (doubleℕ (sucn i n)))
  ≡⟨ cong (λ z → suc (suc z)) (doubleSucn i n) ⟩
    suc (suc (sucn (doubleℕ i) (doubleℕ n)))
  ≡⟨ refl ⟩
    suc (sucn (suc (doubleℕ i)) (doubleℕ n))
  ≡⟨ cong suc refl ⟩
    sucn (suc (suc (doubleℕ i))) (doubleℕ n)
  ∎

doublesSucn : (i n m : ℕ) → doublesℕ n (sucn i m) ≡ sucn (doublesℕ n i) (doublesℕ n m)
doublesSucn i zero m = refl
doublesSucn i (suc n) m =
    doublesℕ n (doubleℕ (sucn i m))
  ≡⟨  cong (doublesℕ n) (doubleSucn i m) ⟩
    doublesℕ n (sucn (doubleℕ i) (doubleℕ m))
  ≡⟨ doublesSucn (doubleℕ i) n (doubleℕ m) ⟩
     sucn (doublesℕ n (doubleℕ i)) (doublesℕ n (doubleℕ m))
  ∎

-- 2^n * (m + 2) =
doublesSucSuc : (n m : ℕ) → doublesℕ n (suc (suc m)) ≡ sucn (doublesℕ (suc n) 1) (doublesℕ n m)
doublesSucSuc zero m = refl
doublesSucSuc (suc n) m =
    doublesℕ (suc n) (suc (suc m))
  ≡⟨ refl ⟩
    doublesℕ n (sucn 4 (doubleℕ m))
  ≡⟨ doublesSucn 4 n (doubleℕ m) ⟩
    sucn (doublesℕ n 4) (doublesℕ n (doubleℕ m))
  ∎

n+n≡2n : (n : ℕ) → sucn n n ≡ doubleℕ n
n+n≡2n zero = refl
n+n≡2n (suc n) =
    sucn (suc n) (suc n)
  ≡⟨ sucnsuc (suc n) n ⟩
    suc (sucn (suc n) n)
  ≡⟨ refl ⟩
   suc (suc (sucn n n))
  ≡⟨ cong (λ z → suc (suc z)) (n+n≡2n n) ⟩
   suc (suc (doubleℕ n))
  ∎

max_stars_repo_name: wrrnhttn/agda-cubical-multidimensional

max_issues_repo_name: wrrnhttn/agda-cubical-multidimensional

max_forks_repo_name: wrrnhttn/agda-cubical-multidimensional


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Coprimality
------------------------------------------------------------------------

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

module Data.Integer.Coprimality where

open import Data.Integer
open import Data.Integer.Divisibility
open import Data.Integer.Properties
import Data.Nat.Coprimality as ℕ
import Data.Nat.Divisibility as ℕ
open import Function using (_on_)
open import Level using (0ℓ)
open import Relation.Binary using (Rel; Decidable; Symmetric)
open import Relation.Binary.PropositionalEquality using (subst)

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

Coprime : Rel ℤ 0ℓ
Coprime = ℕ.Coprime on ∣_∣

------------------------------------------------------------------------
-- Properties of coprimality

sym : Symmetric Coprime
sym = ℕ.sym

coprime? : Decidable Coprime
coprime? x y = ℕ.coprime? ∣ x ∣ ∣ y ∣

coprime-divisor : ∀ i j k → Coprime i j → i ∣ j * k → i ∣ k
coprime-divisor i j k c eq =
  ℕ.coprime-divisor c (subst (∣ i ∣ ℕ.∣_ ) (abs-*-commute j k) eq)


text:
open import Relation.Nullary.Decidable using (False)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; cong₂)
open import Relation.Binary.PropositionalEquality.WithK using (≡-erase)

module AKS.Nat.Divisibility where

open import Data.Nat.Divisibility using (_∣_) public
open import Agda.Builtin.Nat using () renaming (mod-helper to modₕ; div-helper to divₕ) public
open import Data.Nat.DivMod using (_/_; _%_; %-distribˡ-+) public
open import Data.Nat.DivMod.Core using (a≤n⇒a[modₕ]n≡a)
open import Data.Nat.DivMod using (/-congˡ; /-congʳ) renaming (m≡m%n+[m/n]*n to div-lemma)

open import AKS.Nat.Base using (ℕ; _+_; _*_; _∸_; _≟_; lte; _≤_; _<_)
open ℕ
open import AKS.Nat.Properties using (+-suc)
open import AKS.Nat.Properties using (m≤m+n; m≤n+m; suc-mono-≤; ∸-mono-≤ˡ; +-lower-≤; ≤-refl; ≢⇒¬≟; module ≤-Reasoning)
open import AKS.Nat.Properties using (*-comm; +-identityʳ)
open ≤-Reasoning
import Data.Nat.DivMod as Nat
import Data.Nat.Properties as Nat
open import Data.Nat.Properties using (*-zeroʳ)

open import Polynomial.Simple.AlmostCommutativeRing.Instances using (module Nat)
open import Polynomial.Simple.Reflection using (solve)

a[modₕ]n≤n : ∀ acc d n → modₕ acc (acc + n) d n ≤ acc + n
a[modₕ]n≤n acc zero n = m≤m+n
a[modₕ]n≤n acc (suc d) zero = a[modₕ]n≤n zero d (acc + 0)
a[modₕ]n≤n acc (suc d) (suc n) rewrite +-suc acc n = a[modₕ]n≤n (suc acc) d n

n%m<m : ∀ n m {≢0 : False (m ≟ 0)} → (n % m) {≢0} < m
n%m<m n (suc m) = suc-mono-≤ (a[modₕ]n≤n 0 n m)

a[modₕ]n≤a : ∀ acc a n → modₕ acc (acc + n) a n ≤ acc + a
a[modₕ]n≤a acc zero n rewrite +-identityʳ acc = ≤-refl
a[modₕ]n≤a acc (suc a) (suc n) = begin
  modₕ acc (acc + suc n) (suc a) (suc n) ≡⟨ cong (λ v → modₕ acc v (suc a) (suc n)) (+-suc acc n) ⟩
  modₕ acc (suc acc + n) (suc a) (suc n) ≤⟨ a[modₕ]n≤a (suc acc) a n ⟩
  suc acc + a                            ≡⟨ sym (+-suc acc a) ⟩
  acc + suc a                            ∎
a[modₕ]n≤a acc (suc a) zero    = begin
  modₕ acc (acc + 0) (suc a) 0 ≡⟨ cong (λ v → modₕ acc v (suc a) 0) (+-identityʳ acc) ⟩
  modₕ acc acc (suc a) 0       ≤⟨ a[modₕ]n≤a 0 a acc ⟩
  a                            ≤⟨ m≤n+m ⟩
  suc a                        ≤⟨ m≤n+m ⟩
  acc + suc a                  ∎

n%m≤n : ∀ n m {≢0} → (n % m) {≢0} ≤ n
n%m≤n n (suc m) = a[modₕ]n≤a 0 n m

n<m⇒n%m≡n : ∀ {n m} {≢0 : False (m ≟ 0)} → n < m → (n % m) {≢0} ≡ n
n<m⇒n%m≡n {n} {suc m} (lte k refl) = ≡-erase (a≤n⇒a[modₕ]n≡a 0 (n + k) n k)

0%m≡0 : ∀ m {≢0 : False (m ≟ 0)} → (0 % m) {≢0} ≡ 0
0%m≡0 (suc m) = refl

1%m≡1 : ∀ {m} {≢0} → 1 < m → (1 % m) {≢0} ≡ 1
1%m≡1 {suc (suc m)} 1<m = refl

record Euclidean (n : ℕ) (m : ℕ) : Set where
  constructor Euclidean✓
  field
    q : ℕ
    r : ℕ
    division : n ≡ r + m * q
    r<m : r < m

m≡m%n+[m/n]*n : ∀ m n {n≢0 : False (n ≟ 0)} → m ≡ (m % n) {n≢0} + (m / n) {n≢0} * n
m≡m%n+[m/n]*n m (suc n) = div-lemma m n

m%n≡m∸m/n*n : ∀ m n {n≢0 : False (n ≟ 0)} → (m % n) {n≢0} ≡ m ∸ (m / n) {n≢0} * n
m%n≡m∸m/n*n m (suc n) = Nat.m%n≡m∸m/n*n m n

m%n%n≡m%n : ∀ m n {n≢0 : False (n ≟ 0)} → ((m % n) {n≢0} % n) {n≢0} ≡ (m % n) {n≢0}
m%n%n≡m%n m (suc n) = Nat.m%n%n≡m%n m n

n%n≡0 : ∀ n {n≢0 : False (n ≟ 0)} → (n % n) {n≢0} ≡ 0
n%n≡0 (suc n) = Nat.n%n≡0 n

[m+kn]%n≡m%n : ∀ m k n {n≢0 : False (n ≟ 0)} → ((m + k * n) % n) {n≢0} ≡ (m % n) {n≢0}
[m+kn]%n≡m%n m k (suc n) = Nat.[m+kn]%n≡m%n m k n

%-distribˡ-* : ∀ m n d {≢0} → ((m * n) % d) {≢0} ≡ (((m % d) {≢0} * (n % d) {≢0}) % d) {≢0}
%-distribˡ-* m n (suc d) = begin-equality
  (m * n) % suc d                                                           ≡⟨ cong (λ x → (x * n) % suc d) (m≡m%n+[m/n]*n m (suc d)) ⟩
  ((m % suc d + m / suc d * suc d) * n) % suc d                             ≡⟨ cong (λ x → x % suc d) (Nat.*-distribʳ-+ n (m % suc d) (m / suc d * suc d)) ⟩
  ((m % suc d) * n + (m / suc d * suc d) * n) % suc d                       ≡⟨ cong (λ x → ((m % suc d) * n + x) % suc d) (lemma (m / suc d) (suc d) n) ⟩
  ((m % suc d) * n + (m / suc d * n) * suc d) % suc d                       ≡⟨ Nat.[m+kn]%n≡m%n ((m % suc d) * n) (m / suc d * n) d ⟩
  ((m % suc d) * n) % suc d                                                 ≡⟨ cong (λ x → ((m % suc d) * x) % suc d) (m≡m%n+[m/n]*n n (suc d)) ⟩
  ((m % suc d) * (n % suc d + n / suc d * suc d)) % suc d                   ≡⟨ cong (λ x → x % suc d) (Nat.*-distribˡ-+ (m % suc d) (n % suc d) (n / suc d * suc d)) ⟩
  ((m % suc d) * (n % suc d) + (m % suc d) * (n / suc d * suc d)) % suc d   ≡⟨ cong (λ x → ((m % suc d) * (n % suc d) + x) % suc d) (sym (Nat.*-assoc (m % suc d) (n / suc d) (suc d))) ⟩
  ((m % suc d) * (n % suc d) + ((m % suc d) * (n / suc d)) * suc d) % suc d ≡⟨ Nat.[m+kn]%n≡m%n ((m % suc d) * (n % suc d)) ((m % suc d) * (n / suc d)) d ⟩
  ((m % suc d) * (n % suc d)) % suc d                                       ∎
  where
  lemma : ∀ x y z → (x * y) * z ≡ (x * z) * y
  lemma = solve Nat.ring

[m∸n]%n≡m%n : ∀ m n {n≢0 : False (n ≟ 0)} → n ≤ m → ((m ∸ n) % n) {n≢0} ≡ (m % n) {n≢0}
[m∸n]%n≡m%n (suc .(n + k)) (suc n) (lte k refl) = begin-equality
  ((suc n + k) ∸ suc n) % suc n ≡⟨ cong (λ t → t % suc n) (Nat.m+n∸m≡n (suc n) k) ⟩
  k % suc n                     ≡⟨ sym (Nat.[m+n]%n≡m%n k n) ⟩
  (k + suc n) % suc n           ≡⟨ cong (λ t → t % suc n) (Nat.+-comm k (suc n)) ⟩
  (suc n + k) % suc n           ∎

[m∸kn]%n≡m%n : ∀ m k n {n≢0 : False (n ≟ 0)} → k * n ≤ m → ((m ∸ k * n) % n) {n≢0} ≡ (m % n) {n≢0}
[m∸kn]%n≡m%n m zero (suc n) n≤m = refl
[m∸kn]%n≡m%n m (suc k) (suc n) k*n≤m = begin-equality
  (m ∸ (suc n + k * suc n)) % suc n ≡⟨ cong (λ t → t % suc n) (sym (Nat.∸-+-assoc m (suc n) (k * suc n)))  ⟩
  ((m ∸ suc n) ∸ k * suc n) % suc n ≡⟨ [m∸kn]%n≡m%n (m ∸ suc n) k (suc n) k*n≤m∸n ⟩
  (m ∸ suc n) % suc n               ≡⟨ [m∸n]%n≡m%n m (suc n) (+-lower-≤ (k * suc n) k*n≤m) ⟩
  m % suc n                         ∎
  where
  k*n≤m∸n : k * suc n ≤ m ∸ suc n
  k*n≤m∸n = begin
    k * suc n                   ≡⟨ sym (Nat.m+n∸m≡n (suc n) (k * suc n)) ⟩
    (suc n + k * suc n) ∸ suc n ≤⟨ ∸-mono-≤ˡ {suc n} m≤m+n k*n≤m ⟩
    m ∸ suc n                   ∎

%-distribˡ-∸ : ∀ m n d {≢0} → n ≤ m → ((m ∸ n) % d) {≢0} ≡ ((m ∸ (n % d) {≢0}) % d) {≢0}
%-distribˡ-∸ m n (suc d) n≤m = begin-equality
  (m ∸ n) % suc d                               ≡⟨ cong (λ t → (m ∸ t) % suc d) (m≡m%n+[m/n]*n n (suc d)) ⟩
  (m ∸ (n % suc d + n / suc d * suc d)) % suc d ≡⟨ cong (λ t → t % suc d) (sym (Nat.∸-+-assoc m (n % suc d) (n / suc d * suc d))) ⟩
  ((m ∸ n % suc d) ∸ n / suc d * suc d) % suc d ≡⟨ [m∸kn]%n≡m%n (m ∸ n % suc d) (n / suc d) (suc d) n/d*d≤m∸n%d ⟩
  (m ∸ n % suc d) % suc d                       ∎
  where
  n/d*d≤m∸n%d : n / suc d * suc d ≤ m ∸ n % suc d
  n/d*d≤m∸n%d = begin
    n / suc d * suc d                           ≡⟨ sym (Nat.m+n∸m≡n (n % suc d) (n / suc d * suc d)) ⟩
    (n % suc d + n / suc d * suc d) ∸ n % suc d ≡⟨ cong (λ t → t ∸ n % suc d) (sym (m≡m%n+[m/n]*n n (suc d))) ⟩
    n ∸ n % suc d                               ≤⟨ ∸-mono-≤ˡ {n % suc d} (n%m≤n n (suc d)) n≤m ⟩
    m ∸ n % suc d                               ∎

open import AKS.Unsafe using (trustMe)

/-cancelˡ : ∀ c a b {b≢0} {b*c≢0} → ((c * a) / (c * b)) {b*c≢0} ≡ (a / b) {b≢0}
/-cancelˡ (suc c) a (suc b) {b≢0} {b*c≢0} = trustMe

/-cancelʳ : ∀ c a b {b≢0} {b*c≢0} → ((a * c) / (b * c)) {b*c≢0} ≡ (a / b) {b≢0}
/-cancelʳ c a b {b≢0} {b*c≢0} = begin-equality
  (a * c) / (b * c) ≡⟨ /-congˡ {o≢0 = b*c≢0} (*-comm a c) ⟩
  (c * a) / (b * c) ≡⟨ /-congʳ (*-comm b c) ⟩
  (c * a) / (c * b) ≡⟨ /-cancelˡ c a b {b≢0} {c*b≢0} ⟩
  a / b ∎
  where
  c*b≢0 : False (c * b ≟ 0)
  c*b≢0 rewrite *-comm b c = b*c≢0

_div_ : ∀ n m {≢0 : False (m ≟ 0)} → Euclidean n m
n div suc m = Euclidean✓ (n / suc m) (n % suc m) (≡-erase div-proof) (n%m<m n (suc m))
  where
  div-proof : n ≡ n % suc m + suc m * (n / suc m)
  div-proof rewrite *-comm (suc m) (n / suc m) = m≡m%n+[m/n]*n n (suc m)

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


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

module Tools.Embedding where

open import Agda.Primitive

data ι {ℓ : Level} (A : Set ℓ) : Set (lsuc ℓ) where
  ιx : A → ι A

data ι′ {ℓ : Level} (A : Set) : Set ℓ where
  ιx : A → ι′ A

data ι″ {ℓ} (A : Set ℓ) : Setω where
  ιx : A → ι″ A

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


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

module Everything where

import Examples
import Properties
import PrettyPrinter
import Interpreter

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.AssocList.Properties where

open import Cubical.HITs.AssocList.Base as AL
open import Cubical.Foundations.Everything
open import Cubical.Foundations.SIP
open import Cubical.HITs.FiniteMultiset as FMS
  hiding (_++_; unitl-++; unitr-++; assoc-++; cons-++; comm-++)
open import Cubical.Data.Nat   using (ℕ; zero; suc; _+_; +-assoc; isSetℕ)
open import Cubical.Structures.MultiSet
open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq

private
  variable
    ℓ : Level
    A : Type ℓ

multiPer : (a b : A) (m n : ℕ) (xs : AssocList A)
          → ⟨ a , m ⟩∷ ⟨ b , n ⟩∷ xs ≡ ⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs
multiPer a b zero n xs = del a (⟨ b , n ⟩∷ xs) ∙ cong (λ ys → ⟨ b , n ⟩∷ ys) (sym (del a xs))
multiPer a b (suc m) zero xs = cong (λ ys → ⟨ a , suc m ⟩∷ ys) (del b xs) ∙ sym (del b (⟨ a , suc m ⟩∷ xs))
multiPer a b (suc m) (suc n) xs =

 ⟨ a , suc m ⟩∷ ⟨ b , suc n ⟩∷ xs               ≡⟨ sym (agg a 1 m (⟨ b , suc n ⟩∷ xs)) ⟩
 ⟨ a , 1 ⟩∷ ⟨ a , m ⟩∷ ⟨ b , suc n ⟩∷ xs        ≡⟨ cong (λ ys → ⟨ a , 1 ⟩∷ ys) (multiPer a b m (suc n) xs) ⟩
 ⟨ a , 1 ⟩∷ ⟨ b , suc n ⟩∷ ⟨ a , m ⟩∷ xs        ≡⟨ cong (λ ys → ⟨ a , 1 ⟩∷ ys) (sym (agg b 1 n (⟨ a , m ⟩∷ xs))) ⟩
 ⟨ a , 1 ⟩∷ ⟨ b , 1 ⟩∷ ⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs ≡⟨ per a b (⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs) ⟩
 ⟨ b , 1 ⟩∷ ⟨ a , 1 ⟩∷ ⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs ≡⟨ cong (λ ys → ⟨ b , 1 ⟩∷ ⟨ a , 1 ⟩∷ ys) (multiPer b a n m xs) ⟩
 ⟨ b , 1 ⟩∷ ⟨ a , 1 ⟩∷ ⟨ a , m ⟩∷ ⟨ b , n ⟩∷ xs ≡⟨ cong (λ ys → ⟨ b , 1 ⟩∷ ys) (agg a 1 m (⟨ b , n ⟩∷ xs)) ⟩
 ⟨ b , 1 ⟩∷ ⟨ a , suc m ⟩∷ ⟨ b , n ⟩∷ xs        ≡⟨ cong (λ ys → ⟨ b , 1 ⟩∷ ys) (multiPer a b (suc m) n xs) ⟩
 ⟨ b , 1 ⟩∷ ⟨ b , n ⟩∷ ⟨ a , suc m ⟩∷ xs        ≡⟨ agg b 1 n (⟨ a , suc m ⟩∷ xs) ⟩
 ⟨ b , suc n ⟩∷ ⟨ a , suc m ⟩∷ xs               ∎

-- Show that association lists and finite multisets are equivalent
multi-∷ : A → ℕ → FMSet A → FMSet A
multi-∷ x zero xs = xs
multi-∷ x (suc n) xs = x ∷ multi-∷ x n xs

multi-∷-agg : (x : A) (m n : ℕ) (b : FMSet A) → multi-∷ x m (multi-∷ x n b) ≡ multi-∷ x (m + n) b
multi-∷-agg x zero n b = refl
multi-∷-agg x (suc m) n b i = x ∷ (multi-∷-agg x m n b i)

infixr 30 _++_

_++_ : (xs ys : AssocList A) → AssocList A
⟨⟩ ++ ys = ys
(⟨ a , n ⟩∷ xs) ++ ys = ⟨ a , n ⟩∷ (xs ++ ys)
per a b xs i ++ ys = per a b (xs ++ ys) i
agg a m n xs i ++ ys = agg a m n (xs ++ ys) i
del a xs i ++ ys = del a (xs ++ ys) i
trunc xs ys p q i j ++ zs =
  trunc (xs ++ zs) (ys ++ zs) (cong (_++ _) p) (cong (_++ _) q) i j

unitl-++ : (xs : AssocList A) → ⟨⟩ ++ xs ≡ xs
unitl-++ xs = refl

unitr-++ : (xs : AssocList A) → xs ++ ⟨⟩ ≡ xs
unitr-++ = AL.ElimProp.f (trunc _ _) refl λ _ _ → cong (⟨ _ , _ ⟩∷_)

assoc-++ : (xs ys zs : AssocList A) → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
assoc-++ = AL.ElimProp.f (isPropΠ2 (λ _ _ → trunc _ _))
                      (λ ys zs → refl)
                      λ x n p ys zs → cong (⟨ _ , _ ⟩∷_) (p ys zs)

cons-++ : ∀ x n (xs : AssocList A) → ⟨ x , n ⟩∷ xs ≡ xs ++ (⟨ x , n ⟩∷ ⟨⟩)
cons-++ x n = AL.ElimProp.f (trunc _ _) refl
  λ y m p → multiPer _ _ _ _ _ ∙ cong (⟨ _ , _ ⟩∷_) p

comm-++ : (xs ys : AssocList A) → xs ++ ys ≡ ys ++ xs
comm-++ = AL.ElimProp.f (isPropΠ (λ _ → trunc _ _))
  (sym ∘ unitr-++)
  λ x n {xs} p ys → cong (⟨ _ , _ ⟩∷_) (p ys)
                  ∙ cong (_++ _) (cons-++ x n ys)
                  ∙ sym (assoc-++ ys _ xs)

AL→FMS : AssocList A → FMSet A
AL→FMS = AL.Rec.f FMS.trunc [] multi-∷ comm multi-∷-agg λ _ _ → refl

FMS→AL : FMSet A → AssocList A
FMS→AL = FMS.Rec.f AL.trunc ⟨⟩ (λ x xs → ⟨ x , 1 ⟩∷ xs) per

AL→FMS∘FMS→AL≡id : section {A = AssocList A} AL→FMS FMS→AL
AL→FMS∘FMS→AL≡id = FMS.ElimProp.f (FMS.trunc _ _) refl (λ x p → cong (λ ys → x ∷ ys) p)

-- need a little lemma for other direction
multi-∷-id : (x : A) (n : ℕ) (u : FMSet A)
            → FMS→AL (multi-∷ x n u) ≡ ⟨ x , n ⟩∷ FMS→AL u
multi-∷-id x zero u = sym (del x (FMS→AL u))
multi-∷-id x (suc n) u = FMS→AL (multi-∷ x (suc n) u)     ≡⟨ cong (λ ys → ⟨ x , 1 ⟩∷ ys) (multi-∷-id x n u) ⟩
                         ⟨ x , 1 ⟩∷ ⟨ x , n ⟩∷ (FMS→AL u) ≡⟨ agg x 1 n (FMS→AL u) ⟩
                         ⟨ x , (suc n) ⟩∷ (FMS→AL u)      ∎

FMS→AL∘AL→FMS≡id : retract {A = AssocList A} AL→FMS FMS→AL
FMS→AL∘AL→FMS≡id = AL.ElimProp.f (AL.trunc _ _) refl (λ x n {xs} p → (multi-∷-id x n (AL→FMS xs)) ∙ cong (λ ys → ⟨ x , n ⟩∷ ys) p)

AssocList≃FMSet : AssocList A ≃ FMSet A
AssocList≃FMSet = isoToEquiv (iso AL→FMS FMS→AL AL→FMS∘FMS→AL≡id FMS→AL∘AL→FMS≡id)

FMSet≃AssocList : FMSet A ≃ AssocList A
FMSet≃AssocList = isoToEquiv (iso FMS→AL AL→FMS FMS→AL∘AL→FMS≡id AL→FMS∘FMS→AL≡id)

AssocList≡FMSet : AssocList A ≡ FMSet A
AssocList≡FMSet = ua AssocList≃FMSet

-- We want to define a multiset structure on AssocList A, we use the recursor to define the count-function

module _(discA : Discrete A) where
 setA = Discrete→isSet discA

 ALcount-⟨,⟩∷* : A → A → ℕ → ℕ → ℕ
 ALcount-⟨,⟩∷* a x n xs with discA a x
 ... | yes a≡x = n + xs
 ... | no  a≢x = xs

 ALcount-per* :  (a x y : A) (xs : ℕ)
                →  ALcount-⟨,⟩∷* a x 1 (ALcount-⟨,⟩∷* a y 1 xs)
                 ≡ ALcount-⟨,⟩∷* a y 1 (ALcount-⟨,⟩∷* a x 1 xs)
 ALcount-per* a x y xs with discA a x | discA a y
 ALcount-per* a x y xs | yes a≡x | yes a≡y = refl
 ALcount-per* a x y xs | yes a≡x | no  a≢y = refl
 ALcount-per* a x y xs | no  a≢x | yes a≡y = refl
 ALcount-per* a x y xs | no  a≢x | no  a≢y = refl

 ALcount-agg* :  (a x : A) (m n xs : ℕ)
                →  ALcount-⟨,⟩∷* a x m (ALcount-⟨,⟩∷* a x n xs)
                 ≡ ALcount-⟨,⟩∷* a x (m + n) xs
 ALcount-agg* a x m n xs with discA a x
 ... | yes _ = +-assoc m n xs
 ... | no  _ = refl

 ALcount-del* :  (a x : A) (xs : ℕ) → ALcount-⟨,⟩∷* a x 0 xs ≡ xs
 ALcount-del* a x xs with discA a x
 ... | yes _ = refl
 ... | no  _ = refl

 ALcount : A → AssocList A → ℕ
 ALcount a = AL.Rec.f isSetℕ 0 (ALcount-⟨,⟩∷* a) (ALcount-per* a) (ALcount-agg* a) (ALcount-del* a)

 AL-with-str : MultiSet A setA
 AL-with-str = (AssocList A , ⟨⟩ , ⟨_, 1 ⟩∷_ , ALcount)

-- We want to show that Al-with-str ≅ FMS-with-str as multiset-structures
 FMS→AL-EquivStr : MultiSetEquivStr A setA (FMS-with-str discA) (AL-with-str) FMSet≃AssocList
 FMS→AL-EquivStr = refl , (λ a xs → refl) , φ
  where
  φ : ∀ a xs → FMScount discA a xs ≡ ALcount a (FMS→AL xs)
  φ a = FMS.ElimProp.f (isSetℕ _ _) refl ψ
   where
   ψ :  (x : A) {xs : FMSet A}
      → FMScount discA a xs ≡ ALcount a (FMS→AL xs)
      → FMScount discA a (x ∷ xs) ≡ ALcount a (FMS→AL (x ∷ xs))
   ψ x {xs} p = subst B α θ
    where
    B = λ ys → FMScount discA a (x ∷ xs) ≡ ALcount a ys

    α : ⟨ x , 1 ⟩∷ FMS→AL xs ≡ FMS→AL (x ∷ xs)
    α = sym (multi-∷-id x 1 xs)

    θ : FMScount discA a (x ∷ xs) ≡ ALcount a (⟨ x , 1 ⟩∷ (FMS→AL xs))
    θ with discA a x
    ... | yes _ = cong suc p
    ... | no ¬p = p

 FMS-with-str≡AL-with-str : FMS-with-str discA ≡ AL-with-str
 FMS-with-str≡AL-with-str = sip (multiSetUnivalentStr A setA)
                                (FMS-with-str discA) AL-with-str
                                (FMSet≃AssocList , FMS→AL-EquivStr)


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

module DivModAlt where

open import Cubical.Core.Everything using (_≡_; Level; Type; Σ; _,_; fst; snd; _≃_; ~_)

open import Cubical.Foundations.Prelude     using (refl; sym; _∙_; cong; transport; subst; funExt; transp; I; i0; i1; hcomp; primPOr; _∨_)
open import Cubical.Foundations.Function    using (_∘_)
open import Cubical.Foundations.Isomorphism using (iso; Iso; isoToPath; section; retract; isoToEquiv)

open import Data.Empty      using (⊥)
open import Data.Fin        using (Fin; toℕ; fromℕ<; #_; _≟_) renaming (zero to fz; suc to fs)
open import Data.Nat        using (ℕ; zero; suc; _+_; _*_; _≤_ ; _>_; _<_; _≥_; z≤n; s≤s; NonZero)
open import Data.Product    using (_×_)
open import Data.Sum        using (_⊎_; inj₁; inj₂)
open import Data.Unit       using (⊤; tt)

open import Fin

+-assoc : (m n o : ℕ) → (m + n) + o ≡ m + (n + o)
+-assoc zero    _ _ = refl
+-assoc (suc m) n o = cong suc (+-assoc m n o)

≤-refl : {n : ℕ} → n ≤ n
≤-refl {zero}  = z≤n
≤-refl {suc n} = s≤s (≤-refl {n})

≤-trans : {m n o : ℕ} → m ≤ n → n ≤ o → m ≤ o
≤-trans z≤n     _       = z≤n
≤-trans (s≤s x) (s≤s y) = s≤s (≤-trans x y)

≤-step : {m n : ℕ} → m ≤ n → m ≤ 1 + n
≤-step z≤n       = z≤n
≤-step (s≤s m≤n) = s≤s (≤-step m≤n)

n≤1+n : (n : ℕ) → n ≤ 1 + n
n≤1+n _ = ≤-step ≤-refl

≤-pred : {m n : ℕ} → suc m ≤ suc n → m ≤ n
≤-pred (s≤s m≤n) = m≤n

_-_ : (n m : ℕ) → {m ≤ n} → ℕ
(n     - zero)  {z≤n}   = n
(suc n - suc m) {s≤s p} = _-_ n m {p}

<-∨-≥ : (m n : ℕ) → m < n ⊎ m ≥ n
<-∨-≥ zero    zero    = inj₂ z≤n
<-∨-≥ zero    (suc n) = inj₁ (s≤s z≤n)
<-∨-≥ (suc m) zero    = inj₂ z≤n
<-∨-≥ (suc m) (suc n) with <-∨-≥ m n
... | inj₁ m<n = inj₁ (s≤s m<n)
... | inj₂ m≥n = inj₂ (s≤s m≥n)

sucn-1 : (n : ℕ) → (suc n - 1) {s≤s z≤n} ≡ n
sucn-1 n = refl

-decreasing : (n m : ℕ) → (m≤n : suc m ≤ n) → ((n - suc m) {m≤n}) < n
-decreasing (suc n) zero    (s≤s z≤n) = ≤-refl
-decreasing (suc n) (suc m) (s≤s m≤n) = ≤-trans (-decreasing n m m≤n) (n≤1+n n)

-decreasing1 : (c n m : ℕ) → (m≤n : suc m ≤ n) → (n ≤ suc c) → ((n - suc m) {m≤n}) ≤ c
-decreasing1 c (suc n) m (s≤s m≤n) (s≤s n≤c) = ≤-trans (≤-pred (-decreasing (suc n) m (s≤s m≤n))) n≤c

lemma1 : (n m : ℕ) → {m≤n : m ≤ n} → m + ((n - m) {m≤n}) ≡ n
lemma1 n       zero    {z≤n}   = refl
lemma1 (suc n) (suc m) {s≤s p} = cong suc (lemma1 n m {p})

lemma2 : (n m a : ℕ) → {m≤n : m ≤ n} → (n - m) {m≤n} ≡ a → n ≡ m + a
lemma2 n m a {m≤n} x = subst (λ y → y ≡ m + a) (lemma1 n m {m≤n} ) (cong (m +_) x)

lemma3 : (n m d r : ℕ) → {m≤n : m ≤ n} → (n - m) {m≤n} ≡ d * m + r → n ≡ (suc d) * m + r
lemma3 n m d r {m≤n} x = lemma2 n m (d * m + r) x ∙ sym (+-assoc m (d * m) r)

--infixl 7 _div_ _mod_ _mod'_

record DivMod (n m : ℕ) : Type where
  constructor divMod
  field
    q         : ℕ
    r         : Fin m
    n=q*m+r   : n ≡ q * m + toℕ r

record DivMod0 (n m : ℕ) : Type where
  constructor divMod0
  field
    q       : ℕ
    r       : ℕ
    r<m     : r < m
    n=q*m+r : n ≡ q * m + r

record DivMod1 (n m : ℕ) : Type where
  constructor divMod1
  field
    q       : ℕ
    r       : Fin1 m
    n=q*m+r : n ≡ q * m + Fin1.r r

divmod1 : (c n m : ℕ) → (n ≤ c) → {m > 0} → DivMod n m
divmod1 zero zero (suc m) z≤n = divMod 0 (# 0) refl
divmod1 (suc c) n (suc m) n≤c with <-∨-≥ n (suc m)
... | inj₁ n<m = divMod 0 (fromℕ< n<m) (sym (toℕ-fromℕ< n<m))
... | inj₂ n≥m =
  let (divMod q r n-m≡q*m+r) = divmod1 c ((n - (suc m)) {n≥m}) (suc m) (-decreasing1 c n m n≥m n≤c ) {s≤s z≤n}
  in divMod (suc q) r (lemma3 n (suc m) q (toℕ r) n-m≡q*m+r)

divmod : (n m : ℕ) → {m > 0} → DivMod n m
divmod n (suc m) = divmod1 n n (suc m) ≤-refl {s≤s z≤n}

-- NOTE: We can't use {m > 0} here because Agda can't figure out
-- the implicit proof (even for constants), so use {NonZero m} instead.

_div_   : (n m : ℕ) → {NonZero m} → ℕ
n div (suc m) = DivMod.q (divmod n (suc m) {s≤s z≤n})

_mod_ : (n m : ℕ) → {NonZero m} → Fin m
n mod (suc m) = DivMod.r (divmod n (suc m) {s≤s z≤n})

_mod'_ : (n m : ℕ) → {NonZero m} → ℕ
n mod' (suc m) = toℕ (n mod (suc m))

---------

dm0→dm1 : {m n : ℕ} → DivMod0 n m → DivMod1 n m
dm0→dm1 {m} {n} (divMod0 q r r<m n=q*m+r) =
  divMod1 q (fin1 r r<m) n=q*m+r

dm1→dm0 : {m n : ℕ} → DivMod1 n m → DivMod0 n m
dm1→dm0 (divMod1 q r n=q*m+r) = divMod0 q (Fin1.r r) (Fin1.r<n r) n=q*m+r

dm0→dm1→dm0 : {m n : ℕ} → (dm0 : DivMod0 n m) → (dm1→dm0 ∘ dm0→dm1) dm0 ≡ dm0
dm0→dm1→dm0 _ = refl

dm1→dm0→dm1 : {m n : ℕ} → (dm1 : DivMod1 n m) → (dm0→dm1 ∘ dm1→dm0) dm1 ≡ dm1
dm1→dm0→dm1 _ = refl

dm0≃dm1 : {n m : ℕ} → Iso (DivMod0 n m) (DivMod1 n m)
dm0≃dm1 = iso dm0→dm1 dm1→dm0 dm1→dm0→dm1 dm0→dm1→dm0

dm0≡dm1 : {n m : ℕ} → DivMod0 n m ≡ DivMod1 n m
dm0≡dm1 = isoToPath dm0≃dm1

---------

dm1→dm : {m n : ℕ} → DivMod1 n m → DivMod n m
dm1→dm {m} {n} (divMod1 q r n=q*m+r) =
  divMod q (fin1→fin r) (subst (λ x → n ≡ q * m + x) (sym (Fin1r≡toℕ1 r)) n=q*m+r)

dm→dm1 : {m n : ℕ} → DivMod n m → DivMod1 n m
dm→dm1 {m} {n} (divMod q r n=q*m+r) = divMod1 q (fin→fin1 r) (subst (λ x → n ≡ q * m + x) (toℕ≡Fin1r1 r) n=q*m+r)

dm1→dm→dm1 : {m n : ℕ} → (dm1 : DivMod1 n m) → (dm→dm1 ∘ dm1→dm) dm1 ≡ dm1
dm1→dm→dm1 {m} {n} (divMod1 q r n=q*m+r) i = divMod1 q (fin1→fin→fin1 r i) {!!}

dm→dm1→dm : {m n : ℕ} → (dm : DivMod n m) → (dm1→dm ∘ dm→dm1) dm ≡ dm
dm→dm1→dm (divMod q r n=q*m+r) i = divMod q (fin→fin1→fin r i)
  (λ j → {!n=q*m+r j!})

dm1≃dm : {n m : ℕ} → Iso (DivMod1 n m) (DivMod n m)
dm1≃dm = iso dm1→dm dm→dm1 dm→dm1→dm dm1→dm→dm1

dm1≡dm : {n m : ℕ} → DivMod1 n m ≡ DivMod n m
dm1≡dm = isoToPath dm1≃dm

---------

dm0≡dm : {n m : ℕ} → DivMod0 n m ≡ DivMod n m
dm0≡dm = dm0≡dm1 ∙ dm1≡dm

---------

n%m<m : (n m : ℕ) {m≠0 : NonZero m} → toℕ ((n mod m) {m≠0})  < m
n%m<m n (suc m) = toℕ<n (DivMod.r (divmod n (suc m) {s≤s z≤n}))

n≡divmod : (n m : ℕ) {m≠0 : NonZero m} → n ≡ ((n div m) {m≠0}) * m + toℕ ((n mod m) {m≠0})
n≡divmod n (suc m) = DivMod.n=q*m+r (divmod n (suc m) {s≤s z≤n})

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools