text:
module Array.APL where

open import Array.Base
open import Array.Properties
open import Data.Nat
open import Data.Nat.DivMod hiding (_/_)
open import Data.Nat.Properties
open import Data.Fin using (Fin; zero; suc; raise; toℕ; fromℕ≤)
open import Data.Fin.Properties using (toℕ<n)
open import Data.Vec
open import Data.Vec.Properties
open import Data.Product
open import Agda.Builtin.Float
open import Function
open import Relation.Binary.PropositionalEquality hiding (Extensionality)
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Negation
--open import Relation.Binary

-- Now we start to introduce APL operators trying
-- to maintain syntactic rules and semantics.
-- We won't be able to mimic explicit concatenations
-- like 2 3 4 is a vector [2, 3, 4], as we would have
-- to overload the " " somehow.

-- This relation describes promotion of the scalar element in
-- dyadic operations.
data dy-args : ∀ n m k → (Vec ℕ n) → (Vec ℕ m) → (Vec ℕ k) → Set where
 instance
    n-n : ∀ {n}{s}    → dy-args n n n s s s
    n-0 : ∀ {n}{s}{s₁} → dy-args n 0 n s s₁ s
    0-n : ∀ {n}{s}{s₁} → dy-args 0 n n s s₁ s₁

dyadic-type : ∀ a → Set a → Set a
dyadic-type a X = ∀ {n m k}{s s₁ s₂}{{c : dy-args n m k s s₁ s₂}}
                  → Ar X n s → Ar X m s₁ → Ar X k s₂

lift-binary-op : ∀ {a}{X : Set a} → ∀ (op : X → X → X) → dyadic-type a X
lift-binary-op op ⦃ c = n-n ⦄ (imap f) (imap g) = imap λ iv → op (f iv) (g iv)
lift-binary-op op {s₁ = []} ⦃ c = n-0 ⦄ (imap f) (imap g) = imap λ iv → op (f iv) (g [])
lift-binary-op op {s = [] } ⦃ c = 0-n ⦄ (imap f) (imap g) = imap λ iv → op (f []) (g iv)

lift-unary-op : ∀ {a}{X : Set a} → ∀ (op : X → X)
              → ∀ {n s} → Ar X n s → Ar X n s
lift-unary-op f (imap g) = imap (λ iv → f (g iv))

dyadic-type-c : ∀ a → Set a → Set a
dyadic-type-c a X = ∀ {n m k}{s s₁ s₂}
                    → Ar X n s → dy-args n m k s s₁ s₂ → Ar X m s₁ → Ar X k s₂

-- Nat operations
infixr 20 _+ₙ_
infixr 20 _×ₙ_
_+ₙ_ = lift-binary-op _+_
_×ₙ_ = lift-binary-op _*_

_-safe-_ : (a : ℕ) → (b : ℕ) .{≥ : a ≥ b} → ℕ
a -safe- b = a ∸ b

-- FIXME As _-ₙ_ requires a proof, we won't consider yet
-- full dyadic types for _-ₙ_, as it would require us
-- to define dyadic types for ≥a.
infixr 20 _-ₙ_
_-ₙ_ : ∀ {n}{s}
     → (a : Ar ℕ n s) → (b : Ar ℕ n s)
     → .{≥ : a ≥a b}
     → Ar ℕ n s
(imap f -ₙ imap g) {≥} = imap λ iv → (f iv -safe- g iv) {≥ = ≥ iv}

--≢-sym : ∀ {X : Set}{a b : X} → a ≢ b → b ≢ a
--≢-sym pf = pf ∘ sym

infixr 20 _÷ₙ_
_÷ₙ_ : ∀ {n}{s}
     → (a : Ar ℕ n s) → (b : Ar ℕ n s)
     → {≥0 : cst 0 <a b}
     → Ar ℕ n s
_÷ₙ_ (imap f) (imap g) {≥0} = imap λ iv → (f iv div g iv) {≢0 = fromWitnessFalse (≢-sym $ <⇒≢ $ ≥0 iv) }

infixr 20 _+⟨_⟩ₙ_
infixr 20 _×⟨_⟩ₙ_
_+⟨_⟩ₙ_ : dyadic-type-c _ _
a +⟨ c ⟩ₙ b = _+ₙ_ {{c = c}} a b

_×⟨_⟩ₙ_ : dyadic-type-c _ _
a ×⟨ c ⟩ₙ b = _×ₙ_ {{c = c}} a b

-- Float operations
infixr 20 _+ᵣ_
_+ᵣ_ = lift-binary-op primFloatPlus
infixr 20 _-ᵣ_
_-ᵣ_ = lift-binary-op primFloatMinus
infixr 20 _×ᵣ_
_×ᵣ_ = lift-binary-op primFloatTimes

-- XXX we can request the proof that the right argument is not zero.
-- However, the current primFloatDiv has the type Float → Float → Float, so...
infixr 20 _÷ᵣ_
_÷ᵣ_ = lift-binary-op primFloatDiv

infixr 20 _×⟨_⟩ᵣ_
_×⟨_⟩ᵣ_ : dyadic-type-c _ _
a ×⟨ c ⟩ᵣ b = _×ᵣ_ {{c = c}} a b

infixr 20 _+⟨_⟩ᵣ_
_+⟨_⟩ᵣ_ : dyadic-type-c _ _
a +⟨ c ⟩ᵣ b = _+ᵣ_ {{c = c}} a b

infixr 20 _-⟨_⟩ᵣ_
_-⟨_⟩ᵣ_ : dyadic-type-c _ _
a -⟨ c ⟩ᵣ b = _-ᵣ_ {{c = c}} a b
infixr 20 _÷⟨_⟩ᵣ_
_÷⟨_⟩ᵣ_ : dyadic-type-c _ _
a ÷⟨ c ⟩ᵣ b = _÷ᵣ_ {{c = c}} a b

infixr 20 *ᵣ_
*ᵣ_ = lift-unary-op primFloatExp

module xx where
  a : Ar ℕ 2 (3 ∷ 3 ∷ [])
  a = cst 1

  s : Ar ℕ 0 []
  s = cst 2

  test₁ = a +ₙ a
  test₂ = a +ₙ s
  test₃ = s +ₙ a
  --test = (s +ₙ s)
  test₄ = s +⟨ n-n ⟩ₙ s

  test₅ : ∀ {n s} → Ar ℕ n s → Ar ℕ 0 [] → Ar ℕ n s
  test₅ = _+ₙ_

infixr 20 ρ_
ρ_ : ∀ {ℓ}{X : Set ℓ}{d s} → Ar X d s → Ar ℕ 1 (d ∷ [])
ρ_ {s = s} _  = s→a s

infixr 20 ,_
,_ : ∀ {a}{X : Set a}{n s} → Ar X n s → Ar X 1 (prod s ∷ [])
,_ {s = s} (p) = imap λ iv → unimap p (off→idx s iv)

-- Reshape
infixr 20 _ρ_
_ρ_ : ∀ {a}{X : Set a}{n}{sa}
    → (s : Ar ℕ 1 (n ∷ []))
    → (a  : Ar X n sa)
    -- if the `sh` is non-empty, `s` must be non-empty as well.
    → {s≢0⇒ρa≢0 : prod (a→s s) ≢ 0 → prod sa ≢ 0}
    → Ar X n (a→s s)
_ρ_ {sa = sa} s a {s≢0⇒ρa≢0} with  prod sa ≟ 0 | prod (a→s s) ≟ 0
_ρ_ {sa = sa} s a {s≢0⇒ρa≢0}     | _           | yes s≡0  = mkempty (a→s s) s≡0
_ρ_ {sa = sa} s a {s≢0⇒ρa≢0}     | yes ρa≡0    | no  s≢0  = contradiction ρa≡0 (s≢0⇒ρa≢0 s≢0)
_ρ_ {sa = sa} s a {s≢0⇒ρa≢0}     | no  ρa≢0    | _        = imap from-flat
  where
    from-flat : _
    from-flat iv = let
                     off  = idx→off (a→s s) iv --{!!} -- (ix-lookup iv zero)
                     flat = unimap $ , a
                     ix   = (toℕ (ix-lookup off zero) mod prod sa)
                            {≢0 = fromWitnessFalse ρa≢0}
                   in
                     flat (ix ∷ [])

reduce-1d : ∀ {a}{X : Set a}{n} → Ar X 1 (n ∷ []) → (X → X → X) → X → X
reduce-1d {n = zero}  (imap p) op neut = neut
reduce-1d {n = suc n} (imap p) op neut = op (p $ zero ∷ [])
                                            (reduce-1d (imap (λ iv → p (suc (ix-lookup iv zero) ∷ []))) op neut)

{-
  This goes right to left if we want to
  reduce-1d (imap λ iv → p ((raise 1 $ ix-lookup iv zero) ∷ []))
            op (op neut (p $ zero ∷ []))
-}

Scal : ∀ {a} → Set a → Set a
Scal X = Ar X 0 []

scal : ∀ {a}{X : Set a} → X → Scal X
scal = cst

unscal : ∀ {a}{X : Set a} → Scal X → X
unscal (imap f) = f []

module true-reduction where

  thm : ∀ {a}{X : Set a}{n m} → (s : Vec X (n + m)) → s ≡ take n s ++ drop n s
  thm {n = n} s  with splitAt n s
  thm {n = n} .(xs ++ ys) | xs , ys , refl = refl

  thm2 : ∀ {a}{X : Set a} → (v : Vec X 1) → v ≡ head v ∷ []
  thm2 (x ∷ []) = refl

  -- This is a variant with take
  _/⟨_⟩_ : ∀ {a}{X : Set a}{n}{s : Vec ℕ (n + 1)}
        → (X → X → X) → X
        → Ar X (n + 1) s
        → Ar X n (take n s)
  _/⟨_⟩_ {n = n} {s} f neut a = let
                x = nest {s = take n s} {s₁ = drop n s} $ subst (λ x → Ar _ _ x) (thm {n = n} s) a
                in imap λ iv → reduce-1d (subst (λ x → Ar _ _ x) (thm2 (drop n s)) $ unimap x iv) f neut

  _/₁⟨_⟩_ : ∀ {a}{X : Set a}{n}{s : Vec ℕ n}{m}
        → (X → X → X) → X
        → Ar X (n + 1) (s ++ (m ∷ []))
        → Ar X n s
  _/₁⟨_⟩_ {n = n} {s} f neut a = let
         x = nest {s = s} a
         in imap λ iv → reduce-1d (unimap x iv) f neut

  module test-reduce where
    a : Ar ℕ 2 (4 ∷ 4 ∷ [])
    a = cst 1

    b : Ar ℕ 1 (5 ∷ [])
    b = cst 2

    test₁ = _/⟨_⟩_ {n = 0} _+_ 0 (, a)
    test₂ = _/⟨_⟩_ {n = 0} _+_ 0 b

-- FIXME!  This reduction does not implement semantics of APL,
--         as it assumes that we always reduce to scalars!
--         Instead, in APL / reduce on the last axis only,
--         i.e. ⍴ +/3 4 5 ⍴ ⍳1 = 3 4

-- This is mimicing APL's f/ syntax, but with extra neutral
-- element.  We can later introduce the variant where certain
-- operations come with pre-defined neutral elements.
_/⟨_⟩_ : ∀ {a}{X : Set a}{n s}
      → (Scal X → Scal X → Scal X) → Scal X → Ar X n s → Scal X
f /⟨ neut ⟩ a = let
                    op x y = unscal $ f (scal x) (scal y)
                    a-1d = , a
                    neut = unscal neut
                in
                    scal $ reduce-1d a-1d op neut

-- XXX I somehow don't understand how to make X to be an arbitrary Set a...
data reduce-neut : {X : Set} → (Scal X → Scal X → Scal X) → Scal X → Set where
  instance
    plus-nat : reduce-neut  _+⟨ n-n ⟩ₙ_ (cst 0)
    mult-nat : reduce-neut _×⟨ n-n ⟩ₙ_ (cst 1)
    plus-flo : reduce-neut  (_+ᵣ_ {{c = n-n}}) (cst 0.0)
    mult-flo : reduce-neut  (_×ᵣ_ {{c = n-n}}) (cst 1.0)

infixr 20 _/_
_/_ : ∀ {X : Set}{n s neut}
      → (op : Scal X → Scal X → Scal X) → {{c : reduce-neut op neut}}
      → Ar X n s → Scal X
_/_ {neut = neut} f a = f /⟨ neut ⟩ a

module test-reduce where
  a = s→a $ 1 ∷ 2 ∷ 3 ∷ 4 ∷ []

  test₁ : reduce-1d a _+_ 0 ≡ 10
  test₁ = refl

  test₂ : _+⟨ n-n ⟩ₙ_ /⟨ scal 0 ⟩ a ≡ scal 10
  test₂ = refl

  test₃ : _+ₙ_ / a ≡ scal 10
  test₃ = refl

  -- This is somewhat semi-useful dot-product expressed
  -- pretty close to what you'd write in APL.
  dotp : ∀ {n s} → Ar ℕ n s → Ar ℕ n s → Scal ℕ
  dotp a b = _+ₙ_ / a ×ₙ b

  test₄ : dotp a a ≡ scal (1 + 4 + 9 + 16)
  test₄ = refl

-- The size of the leading axis.
infixr 20 ≢_
≢_ : ∀ {a}{X : Set a}{n s} → Ar X n s → Scal ℕ
≢_ {n = zero}      a = scal 1
≢_ {n = suc n} {s} a = scal $ head s

data iota-type : (d : ℕ) → (n : ℕ) → (Vec ℕ d) → Set where
  instance
    iota-scal : iota-type 0 1 []
    iota-vec  : ∀ {n} → iota-type 1 n (n ∷ [])

iota-res-t : ∀ {d n s} → iota-type d n s → (sh : Ar ℕ d s) → Set

iota-res-t {n = n} iota-scal sh = Ar (Σ ℕ λ x → x < unscal sh)
                                     1 (unscal sh ∷ [])

iota-res-t {n = n} iota-vec  sh = Ar (Σ (Ar ℕ 1 (n ∷ []))
                                      λ v → v <a sh)
                                     n (a→s sh)

a<b⇒b≡c⇒a<c : ∀ {a b c} → a < b → b ≡ c → a < c
a<b⇒b≡c⇒a<c a<b refl = a<b

infixr 20 ι_
ι_ : ∀ {d n s}{{c : iota-type d n s}}
   → (sh : Ar ℕ d s)
   → iota-res-t c sh
ι_ ⦃ c = iota-scal ⦄ s = (imap λ iv → (toℕ $ ix-lookup iv zero) , toℕ<n (ix-lookup iv zero))
ι_ {n = n} {s = s ∷ []} ⦃ c = iota-vec ⦄ (imap sh) = imap cast-ix→a
  where
    cast-ix→a : _
    cast-ix→a iv = let
                     ix , pf = ix→a iv
                   in ix , λ jv → a<b⇒b≡c⇒a<c (pf jv) (s→a∘a→s (imap sh) jv)

-- Zilde and comma
⍬ : ∀ {a}{X : Set a} → Ar X 1 (0 ∷ [])
⍬ = imap λ iv → magic-fin $ ix-lookup iv zero

-- XXX We are going to use _·_ instead of _,_ as the
-- latter is a constructor of dependent sum.  Renaming
-- all the occurrences to something else would take
-- a bit of work which we should do later.
infixr 30 _·_
_·_ : ∀ {a}{X : Set a}{n} → X → Ar X 1 (n ∷ []) → Ar X 1 (suc n ∷ [])
x · (imap p) = imap λ iv → case ix-lookup iv zero of λ where
                             zero     → x
                             (suc j) → p (j ∷ [])

-- Note that two dots in an upper register combined with
-- the underscore form the _̈  symbol.  When the symbol is
-- used on its own, it looks like ̈ which is the correct
-- "spelling".
infixr 20 _̈_
_̈_ : ∀ {a}{X Y : Set a}{n s}
    → (X → Y)
    → Ar X n s
    → Ar Y n s
f ̈ imap p = imap λ iv → f $ p iv

-- Take and Drop
ax+sh<s : ∀ {n}
        → (ax sh s : Ar ℕ 1 (n ∷ []))
        → (s≥sh : s ≥a sh)
        → (ax <a (s -ₙ sh) {≥ = s≥sh})
        → (ax +ₙ sh) <a s
ax+sh<s (imap ax) (imap sh) (imap s) s≥sh ax<s-sh iv =
    let
      ax+sh<s-sh+sh = +-monoˡ-< (sh iv) (ax<s-sh iv)
      s-sh+sh≡s     = m∸n+n≡m (s≥sh iv)
    in a<b⇒b≡c⇒a<c ax+sh<s-sh+sh s-sh+sh≡s

_↑_ : ∀ {a}{X : Set a}{n s}
    → (sh : Ar ℕ 1 (n ∷ []))
    → (a : Ar X n s)
    → {pf : s→a s ≥a sh}
    → Ar X n $ a→s sh
_↑_ {s = s} sh       (imap f) {pf}   with (prod $ a→s sh) ≟ 0
_↑_ {s = s} sh       (imap f) {pf} | yes Πsh≡0 = mkempty _ Πsh≡0
_↑_ {s = s} (imap q) (imap f) {pf} | no  Πsh≢0 = imap mtake
  where
    mtake : _
    mtake iv = let
                  ai , ai< = ix→a iv
                  ix<q jv = a<b⇒b≡c⇒a<c (ai< jv) (s→a∘a→s (imap q) jv)
                  ix = a→ix ai (s→a s) λ jv → ≤-trans (ix<q jv) (pf jv)
               in f (subst-ix (a→s∘s→a s) ix)

_↓_ : ∀ {a}{X : Set a}{n s}
    → (sh : Ar ℕ 1 (n ∷ []))
    → (a : Ar X n s)
    → {pf : (s→a s) ≥a sh}
    → Ar X n $ a→s $ (s→a s -ₙ sh) {≥ = pf}
_↓_ {s = s} sh (imap x) {pf} with
                             let p = prod $ a→s $ (s→a s -ₙ sh) {≥ = pf}
                             in  p ≟ 0
_↓_ {s = s} sh       (imap f) {pf} | yes Π≡0 = mkempty _ Π≡0
_↓_ {s = s} (imap q) (imap f) {pf} | no  Π≢0 = imap mkdrop
  where
    mkdrop : _
    mkdrop iv = let
                  ai , ai< = ix→a iv
                  ax = ai +ₙ (imap q)
                  thmx = ax+sh<s
                           ai (imap q) (s→a s) pf
                           λ jv → a<b⇒b≡c⇒a<c (ai< jv)
                                  (s→a∘a→s ((s→a s -ₙ (imap q)) {≥ = pf}) jv)
                  ix = a→ix ax (s→a s) thmx
                in f (subst-ix (a→s∘s→a s) ix)

_̈⟨_⟩_ : ∀ {a}{X Y Z : Set a}{n s}
     → Ar X n s
     → (X → Y → Z)
     → Ar Y n s → Ar Z n s
--(imap p) ̈⟨ f ⟩ (imap p₁) = imap λ iv → f (p iv) (p₁ iv)
p ̈⟨ f ⟩ p₁ = imap λ iv → f (unimap p iv) (unimap p₁ iv)

max_stars_repo_name: ashinkarov/agda-array

max_issues_repo_name: ashinkarov/agda-array

max_forks_repo_name: ashinkarov/agda-array


text:
module Numeral.Natural.Coprime.Proofs where

open import Functional
open import Logic
open import Logic.Classical
open import Logic.Propositional
open import Logic.Propositional.Theorems
import      Lvl
open import Numeral.Finite
open import Numeral.Natural
open import Numeral.Natural.Coprime
open import Numeral.Natural.Decidable
open import Numeral.Natural.Function.GreatestCommonDivisor
open import Numeral.Natural.Relation.Divisibility.Proofs
open import Numeral.Natural.Oper
open import Numeral.Natural.Prime
open import Numeral.Natural.Prime.Proofs
open import Numeral.Natural.Relation.Divisibility
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Structure.Relator.Properties
open import Type.Properties.Decidable.Proofs
open import Type

private variable n x y d p : ℕ

-- 1 is the only number coprime to itself because it does not have any divisors except for itself.
Coprime-reflexivity-condition : Coprime(n)(n) ↔ (n ≡ 1)
Coprime-reflexivity-condition {n} = [↔]-intro l (r{n}) where
  l : Coprime(n)(n) ← (n ≡ 1)
  Coprime.proof(l [≡]-intro) {a} a1 _ = [1]-only-divides-[1] (a1)

  r : ∀{n} → Coprime(n)(n) → (n ≡ 1)
  r {𝟎}       (intro z1)   = z1 Div𝟎 Div𝟎
  r {𝐒(𝟎)}    _            = [≡]-intro
  r {𝐒(𝐒(n))} (intro ssn1) = ssn1 {𝐒(𝐒(n))} divides-reflexivity divides-reflexivity

instance
  Coprime-symmetry : Symmetry(Coprime)
  Coprime.proof(Symmetry.proof Coprime-symmetry (intro proof)) {n} nx ny = proof {n} ny nx

-- The only number coprime to 0 is 1 because while all numbers divide 0, only 1 divides 1.
Coprime-of-0-condition : ∀{x} → Coprime(0)(x) → (x ≡ 1)
Coprime-of-0-condition {0}       (intro n1) = n1 Div𝟎 Div𝟎
Coprime-of-0-condition {1}       (intro n1) = [≡]-intro
Coprime-of-0-condition {𝐒(𝐒(x))} (intro n1) = n1 Div𝟎 divides-reflexivity

-- 1 is coprime to all numbers because only 1 divides 1.
Coprime-of-1 : Coprime(1)(x)
Coprime.proof (Coprime-of-1 {x}) {n} n1 nx = [1]-only-divides-[1] n1

Coprime-of-[+] : Coprime(x)(y) → Coprime(x)(x + y)
Coprime.proof (Coprime-of-[+] {x}{y} (intro proof)) {n} nx nxy = proof {n} nx ([↔]-to-[→] (divides-without-[+] nxy) nx)

-- Coprimality is obviously equivalent to the greatest common divisor being 1 by definition.
Coprime-gcd : Coprime(x)(y) ↔ (gcd(x)(y) ≡ 1)
Coprime-gcd = [↔]-transitivity ([↔]-intro l r) Gcd-gcd-value where
  l : Coprime(x)(y) ← Gcd(x)(y) 1
  Coprime.proof (l p) nx ny = [1]-only-divides-[1] (Gcd.maximum₂ p nx ny)

  r : Coprime(x)(y) → Gcd(x)(y) 1
  Gcd.divisor(r (intro coprim)) 𝟎     = [1]-divides
  Gcd.divisor(r (intro coprim)) (𝐒 𝟎) = [1]-divides
  Gcd.maximum(r (intro coprim)) dv with [≡]-intro ← coprim (dv 𝟎) (dv(𝐒 𝟎)) = [1]-divides

-- A smaller number and a greater prime number is coprime.
-- If the greater number is prime, then no smaller number will divide it except for 1, and greater numbers never divide smaller ones.
-- Examples (y = 7):
--   The prime factors of 7 is only itself (because it is prime).
--   Then the only alternatives for x are:
--   x ∈ {1,2,3,4,5,6}
--   None of them is able to have 7 as a prime factor because it is greater:
--   1=1, 2=2, 3=3, 4=2⋅2, 5=5, 6=2⋅3
Coprime-of-Prime : (𝐒(x) < y) → Prime(y) → Coprime(𝐒(x))(y)
Coprime.proof (Coprime-of-Prime (succ(succ lt)) prim) nx ny with prime-only-divisors prim ny
Coprime.proof (Coprime-of-Prime (succ(succ lt)) prim) nx ny | [∨]-introₗ n1        = n1
Coprime.proof (Coprime-of-Prime (succ(succ lt)) prim) nx ny | [∨]-introᵣ [≡]-intro with () ← [≤]-to-[≯] lt ([≤]-without-[𝐒] (divides-upper-limit nx))

-- A prime number either divides a number or forms a coprime pair.
-- If a prime number does not divide a number, then it cannot share any divisors because by definition, a prime only has 1 as a divisor.
Prime-to-div-or-coprime : Prime(x) → ((x ∣ y) ∨ Coprime(x)(y))
Prime-to-div-or-coprime {y = y} (intro {x} prim) = [¬→]-disjunctive-formᵣ ⦃ decider-to-classical ⦄ (intro ∘ coprim) where
  coprim : (𝐒(𝐒(x)) ∤ y) → ∀{n} → (n ∣ 𝐒(𝐒(x))) → (n ∣ y) → (n ≡ 1)
  coprim nxy {𝟎}   nx ny with () ← [0]-divides-not nx
  coprim nxy {𝐒 n} nx ny with prim nx
  ... | [∨]-introₗ [≡]-intro = [≡]-intro
  ... | [∨]-introᵣ [≡]-intro with () ← nxy ny

divides-to-converse-coprime : ∀{x y z} → (x ∣ y) → Coprime(y)(z) → Coprime(x)(z)
divides-to-converse-coprime xy (intro yz) = intro(nx ↦ nz ↦ yz (transitivity(_∣_) nx xy) nz)

ext: agda

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 --universe-polymorphism #-}
-- {-# OPTIONS --verbose tc.records.ifs:15 #-}
-- {-# OPTIONS --verbose tc.constr.findInScope:15 #-}
-- {-# OPTIONS --verbose tc.term.args.ifs:15 #-}
-- {-# OPTIONS --verbose cta.record.ifs:15 #-}
-- {-# OPTIONS --verbose tc.section.apply:25 #-}
-- {-# OPTIONS --verbose tc.mod.apply:100 #-}
-- {-# OPTIONS --verbose scope.rec:15 #-}
-- {-# OPTIONS --verbose tc.rec.def:15 #-}

module 04-equality where

record ⊤ : Set where
  constructor tt

data Bool : Set where
  true : Bool
  false : Bool

or : Bool → Bool → Bool
or true _ = true
or _ true = true
or false false = false

and : Bool → Bool → Bool
and false _ = false
and _ false = false
and true true = false

not : Bool → Bool
not true = false
not false = true

id : {A : Set} → A → A
id v = v

primEqBool : Bool → Bool → Bool
primEqBool true = id
primEqBool false = not

record Eq (A : Set) : Set where
  field eq : A → A → Bool

eqBool : Eq Bool
eqBool = record { eq = primEqBool }

open Eq {{...}}

neq : {t : Set} → {{eqT : Eq t}} → t → t → Bool
neq a b = not (eq a b)

test = eq false false

-- Instance arguments will also resolve to candidate instances which
-- still require hidden arguments. This allows us to define a
-- reasonable instance for Fin types
data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ    #-}

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc : {n : ℕ} → Fin n → Fin (suc n)

primEqFin : {n : ℕ} → Fin n → Fin n → Bool
primEqFin zero zero = true
primEqFin zero (suc y) = false
primEqFin (suc y) zero = false
primEqFin (suc x) (suc y) = primEqFin x y

eqFin : {n : ℕ} → Eq (Fin n)
eqFin = record { eq = primEqFin }

-- eqFin′ : Eq (Fin 3)
-- eqFin′ = record { eq = primEqFin }

-- eqFinSpecial : {n : ℕ} → Prime n → Eq (Fin n)
-- eqFinSpecial

fin1 : Fin 3
fin1 = zero

fin2 : Fin 3
fin2 = suc (suc zero)

testFin : Bool
testFin = eq fin1 fin2

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Stream type and some operations
------------------------------------------------------------------------

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

module Codata.Stream where

open import Size
open import Codata.Thunk as Thunk using (Thunk; force)

open import Data.Nat.Base
open import Data.List.Base using (List; []; _∷_)
open import Data.List.NonEmpty using (List⁺; _∷_)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Product as P hiding (map)
open import Function

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

data Stream {ℓ} (A : Set ℓ) (i : Size) : Set ℓ where
  _∷_ : A → Thunk (Stream A) i → Stream A i

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

 repeat : ∀ {i} → A → Stream A i
 repeat a = a ∷ λ where .force → repeat a

 head : ∀ {i} → Stream A i → A
 head (x ∷ xs) = x

 tail : Stream A ∞ → Stream A ∞
 tail (x ∷ xs) = xs .force

 lookup : ℕ → Stream A ∞ → A
 lookup zero    xs = head xs
 lookup (suc k) xs = lookup k (tail xs)

 splitAt : (n : ℕ) → Stream A ∞ → Vec A n × Stream A ∞
 splitAt zero    xs       = [] , xs
 splitAt (suc n) (x ∷ xs) = P.map₁ (x ∷_) (splitAt n (xs .force))

 take : (n : ℕ) → Stream A ∞ → Vec A n
 take n xs = proj₁ (splitAt n xs)

 drop : ℕ → Stream A ∞ → Stream A ∞
 drop n xs = proj₂ (splitAt n xs)

 infixr 5 _++_ _⁺++_
 _++_ : ∀ {i} → List A → Stream A i → Stream A i
 []       ++ ys = ys
 (x ∷ xs) ++ ys = x ∷ λ where .force → xs ++ ys

 _⁺++_ : ∀ {i} → List⁺ A → Thunk (Stream A) i → Stream A i
 (x ∷ xs) ⁺++ ys = x ∷ λ where .force → xs ++ ys .force

 cycle : ∀ {i} → List⁺ A → Stream A i
 cycle xs = xs ⁺++ λ where .force → cycle xs

 concat : ∀ {i} → Stream (List⁺ A) i → Stream A i
 concat (xs ∷ xss) = xs ⁺++ λ where .force → concat (xss .force)

 interleave : ∀ {i} → Stream A i → Thunk (Stream A) i → Stream A i
 interleave (x ∷ xs) ys = x ∷ λ where .force → interleave (ys .force) xs

 chunksOf : (n : ℕ) → Stream A ∞ → Stream (Vec A n) ∞
 chunksOf n = chunksOfAcc n id module ChunksOf where

   chunksOfAcc : ∀ {i} k (acc : Vec A k → Vec A n) →
                 Stream A ∞ → Stream (Vec A n) i
   chunksOfAcc zero    acc xs       = acc [] ∷ λ where .force → chunksOfAcc n id xs
   chunksOfAcc (suc k) acc (x ∷ xs) = chunksOfAcc k (acc ∘ (x ∷_)) (xs .force)

module _ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} where

 map : ∀ {i} → (A → B) → Stream A i → Stream B i
 map f (x ∷ xs) = f x ∷ λ where .force → map f (xs .force)

 ap : ∀ {i} → Stream (A → B) i → Stream A i → Stream B i
 ap (f ∷ fs) (x ∷ xs) = f x ∷ λ where .force → ap (fs .force) (xs .force)

 unfold : ∀ {i} → (A → A × B) → A → Stream B i
 unfold next seed =
   let (seed′ , b) = next seed in
   b ∷ λ where .force → unfold next seed′

 scanl : ∀ {i} → (B → A → B) → B → Stream A i → Stream B i
 scanl c n (x ∷ xs) = n ∷ λ where .force → scanl c (c n x) (xs .force)

module _ {ℓ ℓ₁ ℓ₂} {A : Set ℓ} {B : Set ℓ₁} {C : Set ℓ₂} where

 zipWith : ∀ {i} → (A → B → C) → Stream A i → Stream B i → Stream C i
 zipWith f (a ∷ as) (b ∷ bs) = f a b ∷ λ where .force → zipWith f (as .force) (bs .force)

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

  iterate : (A → A) → A → Stream A ∞
  iterate f = unfold < f , id >


text:
------------------------------------------------------------------------------
-- ABP auxiliary lemma
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.ABP.StrongerInductionPrinciple.LemmaATP where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.PropertiesI
open import FOTC.Base.List
open import FOTC.Base.List.PropertiesATP
open import FOTC.Base.Loop
open import FOTC.Data.Bool
open import FOTC.Data.Bool.PropertiesATP
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesATP
open import FOTC.Program.ABP.ABP
open import FOTC.Program.ABP.Fair.Type
open import FOTC.Program.ABP.Fair.PropertiesATP
open import FOTC.Program.ABP.PropertiesI
open import FOTC.Program.ABP.Terms

------------------------------------------------------------------------------
-- Helper function for the auxiliary lemma

module Helper where
  -- 30 November 2013. If we don't have the following definitions
  -- outside the where clause, the ATPs cannot prove the theorems.

  as^ : ∀ b i' is' ds → D
  as^ b i' is' ds = await b i' is' ds
  {-# ATP definition as^ #-}

  bs^ : D → D → D → D → D → D
  bs^ b i' is' ds os₁^ = corrupt os₁^ · (as^ b i' is' ds)
  {-# ATP definition bs^ #-}

  cs^ : D → D → D → D → D → D
  cs^ b i' is' ds os₁^ = ack b · (bs^ b i' is' ds os₁^)
  {-# ATP definition cs^ #-}

  ds^ : D → D → D → D → D → D → D
  ds^ b i' is' ds os₁^ os₂^ = corrupt os₂^ · cs^ b i' is' ds os₁^
  {-# ATP definition ds^ #-}

  os₁^ : D → D → D
  os₁^ os₁' ft₁^ = ft₁^ ++ os₁'
  {-# ATP definition os₁^ #-}

  os₂^ : D → D
  os₂^ os₂ = tail₁ os₂
  {-# ATP definition os₂^ #-}

  helper : ∀ {b i' is' os₁ os₂ as bs cs ds js} →
           Bit b →
           Fair os₂ →
           S b (i' ∷ is') os₁ os₂ as bs cs ds js →
           ∀ ft₁ os₁' → F*T ft₁ → Fair os₁' → os₁ ≡ ft₁ ++ os₁' →
           ∃[ js' ] js ≡ i' ∷ js'
  helper {b} {i'} {is'} {os₁} {os₂} {as} {bs} {cs} {ds} {js} Bb Fos₂
         (asS , bsS , csS , dsS , jsS)
         .(T ∷ []) os₁' f*tnil Fos₁' os₁-eq = prf
    where
    postulate prf : ∃[ js' ] js ≡ i' ∷ js'
    {-# ATP prove prf #-}

  helper {b} {i'} {is'} {os₁} {os₂} {as} {bs} {cs} {ds} {js}
         Bb Fos₂ (asS , bsS , csS , dsS , jsS)
         .(F ∷ ft₁^) os₁' (f*tcons {ft₁^} FTft₁^) Fos₁' os₁-eq =
         helper Bb (tail-Fair Fos₂) ihS ft₁^ os₁' FTft₁^ Fos₁' refl
    where
    postulate os₁-eq-helper : os₁ ≡ F ∷ os₁^ os₁' ft₁^
    {-# ATP prove os₁-eq-helper #-}

    postulate as-eq : as ≡ < i' , b > ∷ (as^ b i' is' ds)
    {-# ATP prove as-eq #-}

    postulate bs-eq : bs ≡ error ∷ (bs^ b i' is' ds (os₁^ os₁' ft₁^))
    {-# ATP prove bs-eq os₁-eq-helper as-eq #-}

    postulate cs-eq : cs ≡ not b ∷ cs^ b i' is' ds (os₁^ os₁' ft₁^)
    {-# ATP prove cs-eq bs-eq #-}

    postulate
      ds-eq-helper₁ :
        os₂ ≡ T ∷ tail₁ os₂ →
        ds ≡ ok (not b) ∷ ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂)
    {-# ATP prove ds-eq-helper₁ cs-eq #-}

    postulate
      ds-eq-helper₂ : os₂ ≡ F ∷ tail₁ os₂ →
                      ds ≡ error ∷ ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂)
    {-# ATP prove ds-eq-helper₂ cs-eq #-}

    ds-eq : ds ≡ ok (not b) ∷ ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂)
            ∨ ds ≡ error ∷ ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂)
    ds-eq = case (λ h → inj₁ (ds-eq-helper₁ h))
                 (λ h → inj₂ (ds-eq-helper₂ h))
                 (head-tail-Fair Fos₂)

    postulate
      as^-eq-helper₁ :
        ds ≡ ok (not b) ∷ ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂) →
        as^ b i' is' ds ≡
          send b · (i' ∷ is') · ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂)
    {-# ATP prove as^-eq-helper₁ x≢not-x #-}

    postulate
      as^-eq-helper₂ :
        ds ≡ error ∷ ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂) →
        as^ b i' is' ds ≡
          send b · (i' ∷ is') · ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂)
    {-# ATP prove as^-eq-helper₂ #-}

    as^-eq : as^ b i' is' ds ≡
             send b · (i' ∷ is') · ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂)
    as^-eq = case as^-eq-helper₁ as^-eq-helper₂ ds-eq

    postulate js-eq : js ≡ out b · bs^ b i' is' ds (os₁^ os₁' ft₁^)
    {-# ATP prove js-eq bs-eq #-}

    ihS : S b
            (i' ∷ is')
            (os₁^ os₁' ft₁^)
            (os₂^ os₂)
            (as^ b i' is' ds)
            (bs^ b i' is' ds (os₁^ os₁' ft₁^))
            (cs^ b i' is' ds (os₁^ os₁' ft₁^))
            (ds^ b i' is' ds (os₁^ os₁' ft₁^) (os₂^ os₂))
            js
    ihS = as^-eq , refl , refl , refl , js-eq

------------------------------------------------------------------------------
-- From Dybjer and Sander's paper: From the assumption that os₁ ∈ Fair
-- and hence by unfolding Fair, we conclude that there are ft₁ :  F*T
-- and os₁' : Fair, such that os₁ = ft₁ ++ os₁'.
--
-- We proceed by induction on ft₁ : F*T using helper.

open Helper
lemma : ∀ {b i' is' os₁ os₂ as bs cs ds js} →
         Bit b →
         Fair os₁ →
         Fair os₂ →
         S b (i' ∷ is') os₁ os₂ as bs cs ds js →
         ∃[ js' ] js ≡ i' ∷ js'
lemma Bb Fos₁ Fos₂ s with Fair-out Fos₁
... | ft , os₁' , FTft , prf ,  Fos₁' = helper Bb Fos₂ s ft os₁' FTft Fos₁' prf

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Andreas, 2019-02-24, issue #3457
-- Error messages for illegal as-clause

import Agda.Builtin.Nat Fresh-name as _

-- Previously, this complained about a duplicate module definition
-- with unspeakable name.

-- Expected error:
-- Not in scope: Fresh-name

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Classes where

open import Agda.Primitive
open import Agda.Builtin.Equality
open import Relation.Binary.PropositionalEquality.Core

open ≡-Reasoning

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

_$_ : ∀ {ℓ} {A B : Set ℓ} → (A → B) → A → B
_$_ = id

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

record Functor {ℓ} (F : Set ℓ → Set ℓ) : Set (lsuc ℓ)  where
  field
    fmap : ∀ {A B} → (A → B) → F A → F B

    F-id : ∀ {A} → (a : F A) → fmap id a ≡ a
    F-∘ : ∀ {A B C} → (g : B → C) (f : A → B) (a : F A) → fmap (g ∘ f) a ≡ (fmap g ∘ fmap f) a

  _<$>_ : ∀ {A B} → (A → B) → F A → F B
  _<$>_ = fmap

  infixl 20 _<$>_

open Functor {{...}} public

record Applicative (F : Set → Set) : Set₁ where
  field
    {{funF}} : Functor F

    pure : {A : Set} → A → F A
    _<*>_ : {A B : Set} → F (A → B) → F A → F B

    A-id  : ∀ {A} → (v : F A) → pure id <*> v ≡ v
    A-∘   : ∀ {A B C} → (u : F (B →  C)) (v : F (A → B)) (w : F A) → pure _∘_ <*> u <*> v <*> w ≡ u <*> (v <*> w)
    A-hom : ∀ {A B} → (f : A → B) (x : A) → pure f <*> pure x ≡ pure (f x)
    A-ic  : ∀ {A B} → (u : F (A → B)) (y : A) → u <*> pure y ≡ pure (_$ y) <*> u

  infixl 20 _<*>_

open Applicative {{...}} public

postulate
  -- this is from parametricity: fmap is universal w.r.t. the functor laws
  appFun : ∀ {A B F} {{aF : Applicative F}} → (f : A → B) (x : F A) → pure f <*> x ≡ fmap f x

record Monad (F : Set → Set) : Set₁ where
  field
    {{appF}} : Applicative F
    _>>=_ : ∀ {A B} → F A → (A → F B) → F B

  return : ∀ {A} → A → F A
  return = pure

  _>=>_ : {A B C : Set} → (A → F B) → (B → F C) → A → F C
  f >=> g = λ a → f a >>= g

  infixl 10 _>>=_
  infixr 10 _>=>_

  field
    left-1  : ∀ {A B} → (a : A) (k : A → F B) → return a >>= k ≡ k a
    right-1 : ∀ {A} → (m : F A) → m >>= return ≡ m
    assoc : ∀ {A B C D} → (f : A → F B) (g : B → F C) (h : C → F D) (a : A) → (f >=> (g >=> h)) a ≡ ((f >=> g) >=> h) a

open Monad {{...}} public

max_stars_repo_name: samuelhklumpers/strong-vector

max_issues_repo_name: samuelhklumpers/strong-vector

max_forks_repo_name: samuelhklumpers/strong-vector


text:
data Bool : Set where
  true false : Bool

record Top : Set where

foo : Top
foo with true
... | true  = _
... | false = top
  where
    top = record{ }  -- the only purpose of this was to force
                     -- evaluation of the with function clauses
                     -- which were in an __IMPOSSIBLE__ state

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Prelude
open import Nat
open import dynamics-core
open import contexts

module lemmas-disjointness where
  -- disjointness is commutative
  ##-comm : {A : Set} {Δ1 Δ2 : A ctx} → Δ1 ## Δ2 → Δ2 ## Δ1
  ##-comm (π1 , π2) = π2 , π1

  -- the empty context is disjoint from any context
  empty-disj : {A : Set} (Γ : A ctx) → ∅ ## Γ
  empty-disj Γ = ed1 , ed2
   where
    ed1 : {A : Set} (n : Nat) → dom {A} ∅ n → n # Γ
    ed1 n (π1 , ())

    ed2 : {A : Set} (n : Nat) → dom Γ n →  _#_ {A} n ∅
    ed2 _ _ = refl

  -- two singleton contexts with different indices are disjoint
  disjoint-singles : {A : Set} {x y : A} {u1 u2 : Nat} →
                          u1 ≠ u2 →
                          (■ (u1 , x)) ## (■ (u2 , y))
  disjoint-singles {_} {x} {y} {u1} {u2} neq = ds1 , ds2
    where
      ds1 : (n : Nat) → dom (■ (u1 , x)) n → n # (■ (u2 , y))
      ds1 n d with lem-dom-eq d
      ds1 .u1 d | refl with natEQ u2 u1
      ds1 .u1 d | refl | Inl xx = abort (neq (! xx))
      ds1 .u1 d | refl | Inr x₁ = refl

      ds2 : (n : Nat) → dom (■ (u2 , y)) n → n # (■ (u1 , x))
      ds2 n d with lem-dom-eq d
      ds2 .u2 d | refl with natEQ u1 u2
      ds2 .u2 d | refl | Inl x₁ = abort (neq x₁)
      ds2 .u2 d | refl | Inr x₁ = refl

  apart-noteq : {A : Set} (p r : Nat) (q : A) → p # (■ (r , q)) → p ≠ r
  apart-noteq p r q apt with natEQ r p
  apart-noteq p .p q apt | Inl refl = abort (somenotnone apt)
  apart-noteq p r q apt | Inr x₁ = flip x₁

  -- if singleton contexts are disjoint, their indices must be disequal
  singles-notequal : {A : Set} {x y : A} {u1 u2 : Nat} →
                          (■ (u1 , x)) ## (■ (u2 , y)) →
                          u1 ≠ u2
  singles-notequal {A} {x} {y} {u1} {u2} (d1 , d2) = apart-noteq u1 u2 y (d1 u1 (lem-domsingle u1 x))

  -- dual of lem2 above; if two indices are disequal, then either is apart
  -- from the singleton formed with the other
  apart-singleton : {A : Set} → ∀{x y} → {τ : A} →
                          x ≠ y →
                          x # (■ (y , τ))
  apart-singleton {A} {x} {y} {τ} neq with natEQ y x
  apart-singleton neq | Inl x₁ = abort ((flip neq) x₁)
  apart-singleton neq | Inr x₁ = refl

  -- if an index is apart from two contexts, it's apart from their union as
  -- well. used below and in other files, so it's outside the local scope.
  apart-parts : {A : Set} (Γ1 Γ2 : A ctx) (n : Nat) → n # Γ1 → n # Γ2 → n # (Γ1 ∪ Γ2)
  apart-parts Γ1 Γ2 n apt1 apt2 with Γ1 n
  apart-parts _ _ n refl apt2 | .None = apt2

  -- this is just for convenience; it shows up a lot.
  apart-extend1 : {A : Set} → ∀{x y τ} → (Γ : A ctx) → x ≠ y → x # Γ → x # (Γ ,, (y , τ))
  apart-extend1 {A} {x} {y} {τ} Γ neq apt with natEQ y x
  ... | Inl refl = abort (neq refl)
  ... | Inr y≠x  = apt

  -- if an index is in the domain of a union, it's in the domain of one or
  -- the other unand
  dom-split : {A : Set} → (Γ1 Γ2 : A ctx) (n : Nat) → dom (Γ1 ∪ Γ2) n → dom Γ1 n + dom Γ2 n
  dom-split Γ4 Γ5 n (π1 , π2) with Γ4 n
  dom-split Γ4 Γ5 n (π1 , π2) | Some x = Inl (x , refl)
  dom-split Γ4 Γ5 n (π1 , π2) | None = Inr (π1 , π2)

  -- if both parts of a union are disjoint with a target, so is the union
  disjoint-parts : {A : Set} {Γ1 Γ2 Γ3 : A ctx} → Γ1 ## Γ3 → Γ2 ## Γ3 → (Γ1 ∪ Γ2) ## Γ3
  disjoint-parts {_} {Γ1} {Γ2} {Γ3} D13 D23 = d31 , d32
    where
      d31 : (n : Nat) → dom (Γ1 ∪ Γ2) n → n # Γ3
      d31 n D with dom-split Γ1 Γ2 n D
      d31 n D | Inl x = π1 D13 n x
      d31 n D | Inr x = π1 D23 n x

      d32 : (n : Nat) → dom Γ3 n → n # (Γ1 ∪ Γ2)
      d32 n D = apart-parts Γ1 Γ2 n (π2 D13 n D) (π2 D23 n D)

  apart-union1 : {A : Set} (Γ1 Γ2 : A ctx) (n : Nat) → n # (Γ1 ∪ Γ2) → n # Γ1
  apart-union1 Γ1 Γ2 n aprt with Γ1 n
  apart-union1 Γ1 Γ2 n () | Some x
  apart-union1 Γ1 Γ2 n aprt | None = refl

  apart-union2 : {A : Set} (Γ1 Γ2 : A ctx) (n : Nat) → n # (Γ1 ∪ Γ2) → n # Γ2
  apart-union2 Γ1 Γ2 n aprt with Γ1 n
  apart-union2 Γ3 Γ4 n () | Some x
  apart-union2 Γ3 Γ4 n aprt | None = aprt

  -- if a union is disjoint with a target, so is the left unand
  disjoint-union1 : {A : Set} {Γ1 Γ2 Δ : A ctx} → (Γ1 ∪ Γ2) ## Δ → Γ1 ## Δ
  disjoint-union1 {Γ1 = Γ1} {Γ2 = Γ2} {Δ = Δ} (ud1 , ud2) = du11 , du12
    where
      dom-union1 : {A : Set} (Γ1 Γ2 : A ctx) (n : Nat) → dom Γ1 n → dom (Γ1 ∪ Γ2) n
      dom-union1 Γ1 Γ2 n (π1 , π2) with Γ1 n
      dom-union1 Γ1 Γ2 n (π1 , π2) | Some x = x , refl
      dom-union1 Γ1 Γ2 n (π1 , ()) | None

      du11 : (n : Nat) → dom Γ1 n → n # Δ
      du11 n dom = ud1 n (dom-union1 Γ1 Γ2 n dom)

      du12 : (n : Nat) → dom Δ n → n # Γ1
      du12 n dom = apart-union1 Γ1 Γ2 n (ud2 n dom)

  -- if a union is disjoint with a target, so is the right unand
  disjoint-union2 : {A : Set} {Γ1 Γ2 Δ : A ctx} → (Γ1 ∪ Γ2) ## Δ → Γ2 ## Δ
  disjoint-union2 {Γ1 = Γ1} {Γ2 = Γ2} {Δ = Δ} (ud1 , ud2) = du21 , du22
    where
      dom-union2 : {A : Set} (Γ1 Γ2 : A ctx) (n : Nat) → dom Γ2 n → dom (Γ1 ∪ Γ2) n
      dom-union2 Γ1 Γ2 n (π1 , π2) with Γ1 n
      dom-union2 Γ3 Γ4 n (π1 , π2) | Some x = x , refl
      dom-union2 Γ3 Γ4 n (π1 , π2) | None = π1 , π2

      du21 : (n : Nat) → dom Γ2 n → n # Δ
      du21 n dom = ud1 n (dom-union2 Γ1  Γ2 n dom)

      du22 : (n : Nat) → dom Δ n → n # Γ2
      du22 n dom = apart-union2 Γ1 Γ2 n (ud2 n dom)

  -- if x isn't in a context and y is then they can't be equal
  lem-dom-apt : {A : Set} {G : A ctx} {x y : Nat} → x # G → dom G y → x ≠ y
  lem-dom-apt {x = x} {y = y} apt dom with natEQ x y
  lem-dom-apt apt dom | Inl refl = abort (somenotnone (! (π2 dom) · apt))
  lem-dom-apt apt dom | Inr x₁ = x₁

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.GroupoidLaws hiding (assoc)
open import Cubical.Data.Sigma

open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid.Base

open import Cubical.Algebra.Group.Base

private
  variable
    ℓ : Level
    G : Type ℓ

isPropIsGroup : (1g : G) (_·_ : G → G → G) (inv : G → G)
              → isProp (IsGroup 1g _·_ inv)
isPropIsGroup 1g _·_ inv =
  isOfHLevelRetractFromIso 1 IsGroupIsoΣ
    (isPropΣ (isPropIsMonoid 1g _·_)
             λ mono → isProp× (isPropΠ λ _ → mono .is-set _ _)
             (isPropΠ λ _ → mono .is-set _ _))
    where
    open IsMonoid

module GroupTheory (G : Group ℓ) where
  open GroupStr (snd G)
  abstract
    ·CancelL : (a : ⟨ G ⟩) {b c : ⟨ G ⟩} → a · b ≡ a · c → b ≡ c
    ·CancelL a {b} {c} p =
       b               ≡⟨ sym (·IdL b) ∙ cong (_· b) (sym (·InvL a)) ∙ sym (·Assoc _ _ _) ⟩
      inv a · (a · b)  ≡⟨ cong (inv a ·_) p ⟩
      inv a · (a · c)  ≡⟨ ·Assoc _ _ _ ∙ cong (_· c) (·InvL a) ∙ ·IdL c ⟩
      c ∎

    ·CancelR : {a b : ⟨ G ⟩} (c : ⟨ G ⟩) → a · c ≡ b · c → a ≡ b
    ·CancelR {a} {b} c p =
      a                ≡⟨ sym (·IdR a) ∙ cong (a ·_) (sym (·InvR c)) ∙ ·Assoc _ _ _ ⟩
      (a · c) · inv c  ≡⟨ cong (_· inv c) p ⟩
      (b · c) · inv c  ≡⟨ sym (·Assoc _ _ _) ∙ cong (b ·_) (·InvR c) ∙ ·IdR b ⟩
      b ∎

    invInv : (a : ⟨ G ⟩) → inv (inv a) ≡ a
    invInv a = ·CancelL (inv a) (·InvR (inv a) ∙ sym (·InvL a))

    inv1g : inv 1g ≡ 1g
    inv1g = ·CancelL 1g (·InvR 1g ∙ sym (·IdL 1g))

    1gUniqueL : {e : ⟨ G ⟩} (x : ⟨ G ⟩) → e · x ≡ x → e ≡ 1g
    1gUniqueL {e} x p = ·CancelR x (p ∙ sym (·IdL _))

    1gUniqueR : (x : ⟨ G ⟩) {e : ⟨ G ⟩} → x · e ≡ x → e ≡ 1g
    1gUniqueR x {e} p = ·CancelL x (p ∙ sym (·IdR _))

    invUniqueL : {g h : ⟨ G ⟩} → g · h ≡ 1g → g ≡ inv h
    invUniqueL {g} {h} p = ·CancelR h (p ∙ sym (·InvL h))

    invUniqueR : {g h : ⟨ G ⟩} → g · h ≡ 1g → h ≡ inv g
    invUniqueR {g} {h} p = ·CancelL g (p ∙ sym (·InvR g))

    invDistr : (a b : ⟨ G ⟩) → inv (a · b) ≡ inv b · inv a
    invDistr a b = sym (invUniqueR γ) where
      γ : (a · b) · (inv b · inv a) ≡ 1g
      γ = (a · b) · (inv b · inv a)
            ≡⟨ sym (·Assoc _ _ _) ⟩
          a · b · (inv b) · (inv a)
            ≡⟨ cong (a ·_) (·Assoc _ _ _ ∙ cong (_· (inv a)) (·InvR b)) ⟩
          a · (1g · inv a)
            ≡⟨ cong (a ·_) (·IdL (inv a)) ∙ ·InvR a ⟩
          1g ∎

congIdLeft≡congIdRight : (_·G_ : G → G → G) (-G_ : G → G)
            (0G : G)
            (rUnitG : (x : G) → x ·G 0G ≡ x)
            (lUnitG : (x : G) → 0G ·G x ≡ x)
          → (r≡l : rUnitG 0G ≡ lUnitG 0G)
          → (p : 0G ≡ 0G) →
            cong (0G ·G_) p ≡ cong (_·G 0G) p
congIdLeft≡congIdRight _·G_ -G_ 0G rUnitG lUnitG r≡l p =
            rUnit (cong (0G ·G_) p)
         ∙∙ ((λ i → (λ j → lUnitG 0G (i ∧ j)) ∙∙ cong (λ x → lUnitG x i) p ∙∙ λ j → lUnitG 0G (i ∧ ~ j))
         ∙∙ cong₂ (λ x y → x ∙∙ p ∙∙ y) (sym r≡l) (cong sym (sym r≡l))
         ∙∙ λ i → (λ j → rUnitG 0G (~ i ∧ j)) ∙∙ cong (λ x → rUnitG x (~ i)) p ∙∙ λ j → rUnitG 0G (~ i ∧ ~ j))
         ∙∙ sym (rUnit (cong (_·G 0G) p))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import Cubical.HITs.Cost.Base

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


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 Level using (0ℓ)
open import Util.Prelude

-- This module incldes various Agda lemmas that are independent of the project's domain

module Util.Lemmas where

 cong₃ : ∀{a b c d}{A : Set a}{B : Set b}{C : Set c}{D : Set d}
       → (f : A → B → C → D) → ∀{x y u v m n} → x ≡ y → u ≡ v → m ≡ n
       → f x u m ≡ f y v n
 cong₃ f refl refl refl = refl

 ≡-pi : ∀{a}{A : Set a}{x y : A}(p q : x ≡ y) → p ≡ q
 ≡-pi refl refl = refl

 Unit-pi : {u1 u2 : Unit}
         → u1 ≡ u2
 Unit-pi {unit} {unit} = refl

 ++-inj : ∀{a}{A : Set a}{m n o p : List A}
        → length m ≡ length n → m ++ o ≡ n ++ p
        → m ≡ n × o ≡ p
 ++-inj {m = []}     {x ∷ n} () hip
 ++-inj {m = x ∷ m}  {[]}    () hip
 ++-inj {m = []}     {[]}     lhip hip
   = refl , hip
 ++-inj {m = m ∷ ms} {n ∷ ns} lhip hip
   with ++-inj {m = ms} {ns} (suc-injective lhip) (proj₂ (∷-injective hip))
 ...| (mn , op) rewrite proj₁ (∷-injective hip)
    = cong (n ∷_) mn , op

 ++-abs : ∀{a}{A : Set a}{n : List A}(m : List A)
        → 1 ≤ length m → [] ≡ m ++ n → ⊥
 ++-abs [] ()
 ++-abs (x ∷ m) imp ()

 filter-++-[]
   : ∀ {a p} {A : Set a} {P : (a : A) → Set p}
     → ∀ xs ys (p : (a : A) → Dec (P a))
     → List-filter p xs ≡ [] → List-filter p ys ≡ []
     → List-filter p (xs ++ ys) ≡ []
 filter-++-[] xs ys p pf₁ pf₂ rewrite List-filter-++ p xs ys | pf₁ | pf₂ = refl

 filter-∪?-[]₁
   : ∀ {a p} {A : Set a} {P Q : (a : A) → Set p}
     → ∀ xs (p : (a : A) → Dec (P a)) (q : (a : A) → Dec (Q a))
     → List-filter (p ∪? q) xs ≡ []
     → List-filter p xs ≡ []
 filter-∪?-[]₁ [] p q pf = refl
 filter-∪?-[]₁ (x ∷ xs) p q pf
   with p x
 ...| no  proof₁
   with q x
 ...| no  proof₂ = filter-∪?-[]₁ xs p q pf
 filter-∪?-[]₁ (x ∷ xs) p q () | no proof₁ | yes proof₂
 filter-∪?-[]₁ (x ∷ xs) p q () | yes proof

 filter-∪?-[]₂
   : ∀ {a p} {A : Set a} {P Q : (a : A) → Set p}
     → ∀ xs (p : (a : A) → Dec (P a)) (q : (a : A) → Dec (Q a))
     → List-filter (p ∪? q) xs ≡ []
     → List-filter q xs ≡ []
 filter-∪?-[]₂ [] p q pf = refl
 filter-∪?-[]₂ (x ∷ xs) p q pf
   with p x
 ...| no  proof₁
   with q x
 ...| no  proof₂ = filter-∪?-[]₂ xs p q pf
 filter-∪?-[]₂ (x ∷ xs) p q () | no proof₁ | yes proof₂
 filter-∪?-[]₂ (x ∷ xs) p q () | yes proof

 noneOfKind⇒¬Any
   : ∀ {a p} {A : Set a} {P : A → Set p}
       xs (p : (a : A) → Dec (P a))
     → NoneOfKind xs p
     → ¬ Any P xs
 noneOfKind⇒¬Any (x ∷ xs) p none ∈xs
    with p x
 noneOfKind⇒¬Any (x ∷ xs) p none (here   px) | no ¬px = ¬px px
 noneOfKind⇒¬Any (x ∷ xs) p none (there ∈xs) | no ¬px =
   noneOfKind⇒¬Any xs p none ∈xs

 noneOfKind⇒All¬
   : ∀ {a p} {A : Set a} {P : A → Set p}
       xs (p : (a : A) → Dec (P a))
     → NoneOfKind xs p
     → All (¬_ ∘ P) xs
 noneOfKind⇒All¬ xs p none = ¬Any⇒All¬ xs (noneOfKind⇒¬Any xs p none)

 ++-NoneOfKind : ∀ {ℓA} {A : Set ℓA} {ℓ} {P : A → Set ℓ} xs ys (p : (a : A) → Dec (P a))
                 → NoneOfKind xs p → NoneOfKind ys p → NoneOfKind (xs ++ ys) p
 ++-NoneOfKind xs ys p nok₁ nok₂ = filter-++-[] xs ys p nok₁ nok₂

 data All-vec {ℓ} {A : Set ℓ} (P : A → Set ℓ) : ∀ {n} → Vec {ℓ} A n → Set (Level.suc ℓ) where
   []  : All-vec P []
   _∷_ : ∀ {x n} {xs : Vec A n} (px : P x) (pxs : All-vec P xs) → All-vec P (x ∷ xs)

 ≤-unstep : ∀{m n} → suc m ≤ n → m ≤ n
 ≤-unstep (s≤s ss) = ≤-step ss

 ≡⇒≤ : ∀{m n} → m ≡ n → m ≤ n
 ≡⇒≤ refl = ≤-refl

 ∈-cong : ∀{a b}{A : Set a}{B : Set b}{x : A}{l : List A}
        → (f : A → B) → x ∈ l → f x ∈ List-map f l
 ∈-cong f (here px) = here (cong f px)
 ∈-cong f (there hyp) = there (∈-cong f hyp)

 All-self : ∀{a}{A : Set a}{xs : List A} → All (_∈ xs) xs
 All-self = All-tabulate (λ x → x)

 All-reduce⁺
   : ∀{a b}{A : Set a}{B : Set b}{Q : A → Set}{P : B → Set}
   → { xs : List A }
   → (f : ∀{x} → Q x → B)
   → (∀{x} → (prf : Q x) → P (f prf))
   → (all : All Q xs)
   → All P (All-reduce f all)
 All-reduce⁺ f hyp []         = []
 All-reduce⁺ f hyp (ax ∷ axs) = (hyp ax) ∷ All-reduce⁺ f hyp axs

 All-reduce⁻
   : ∀{a b}{A : Set a}{B : Set b}
     {Q : A → Set}
   → { xs : List A }
   → ∀ {vdq}
   → (f : ∀{x} → Q x → B)
   → (all : All Q xs)
   → vdq ∈ All-reduce f all
   → ∃[ v ] ∃[ v∈xs ] (vdq ≡ f {v} v∈xs)
 All-reduce⁻ {Q = Q} {(h ∷ _)} {vdq} f (px ∷ pxs) (here refl)  = h , px , refl
 All-reduce⁻ {Q = Q} {(_ ∷ t)} {vdq} f (px ∷ pxs) (there vdq∈) = All-reduce⁻ {xs = t} f pxs vdq∈

 List-index : ∀ {A : Set} → (_≟A_ : (a₁ a₂ : A) → Dec (a₁ ≡ a₂)) → A → (l : List A) → Maybe (Fin (length l))
 List-index _≟A_ x l with break (_≟A x) l
 ...| not≡ , _ with length not≡ <? length l
 ...| no  _     = nothing
 ...| yes found = just ( fromℕ< {length not≡} {length l} found)

 nats : ℕ → List ℕ
 nats 0 = []
 nats (suc n) = (nats n) ++ (n ∷ [])

 _ : nats 4 ≡ 0 ∷ 1 ∷ 2 ∷ 3 ∷ []
 _ = refl

 _ : Maybe-map toℕ (List-index _≟_ 2 (nats 4)) ≡ just 2
 _ = refl

 _ : Maybe-map toℕ (List-index _≟_ 4 (nats 4)) ≡ nothing
 _ = refl

 allDistinct : ∀ {A : Set} → List A → Set
 allDistinct l = ∀ (i j : Fin (length l))
                 → i ≡ j ⊎ List-lookup l i ≢ List-lookup l j

 postulate -- TODO-1: currently unused; prove it, if needed
   allDistinct? : ∀ {A : Set} → {≟A : (a₁ a₂ : A) → Dec (a₁ ≡ a₂)} → (l : List A) → Dec (allDistinct l)

  -- Extends an arbitrary relation to work on the head of
  -- the supplied list, if any.
 data OnHead {A : Set}(P : A → A → Set) (x : A) : List A → Set where
    []   : OnHead P x []
    on-∷ : ∀{y ys} → P x y → OnHead P x (y ∷ ys)

  -- Establishes that a list is sorted according to the supplied
  -- relation.
 data IsSorted {A : Set}(_<_ : A → A → Set) : List A → Set where
    []  : IsSorted _<_ []
    _∷_ : ∀{x xs} → OnHead _<_ x xs → IsSorted _<_ xs → IsSorted _<_ (x ∷ xs)

 OnHead-prop : ∀{A}(P : A → A → Set)(x : A)(l : List A)
             → Irrelevant P
             → isPropositional (OnHead P x l)
 OnHead-prop P x [] hyp [] [] = refl
 OnHead-prop P x (x₁ ∷ l) hyp (on-∷ x₂) (on-∷ x₃) = cong on-∷ (hyp x₂ x₃)

 IsSorted-prop : ∀{A}(_<_ : A → A → Set)(l : List A)
               → Irrelevant _<_
               → isPropositional (IsSorted _<_ l)
 IsSorted-prop _<_ [] hyp [] []                  = refl
 IsSorted-prop _<_ (x ∷ l) hyp (x₁ ∷ a) (x₂ ∷ b)
   = cong₂ _∷_ (OnHead-prop _<_ x l hyp x₁ x₂)
               (IsSorted-prop _<_ l hyp a b)

 IsSorted-map⁻ : {A : Set}{_≤_ : A → A → Set}
               → {B : Set}(f : B → A)(l : List B)
               → IsSorted (λ x y → f x ≤ f y) l
               → IsSorted _≤_ (List-map f l)
 IsSorted-map⁻ f .[] [] = []
 IsSorted-map⁻ f .(_ ∷ []) (x ∷ []) = [] ∷ []
 IsSorted-map⁻ f .(_ ∷ _ ∷ _) (on-∷ x ∷ (x₁ ∷ is)) = (on-∷ x) ∷ IsSorted-map⁻ f _ (x₁ ∷ is)

 transOnHead : ∀ {A} {l : List A} {y x : A} {_<_ : A → A → Set}
              → Transitive _<_
              → OnHead _<_ y l
              → x < y
              → OnHead _<_ x l
 transOnHead _ [] _ = []
 transOnHead trans (on-∷ y<f) x<y = on-∷ (trans x<y y<f)

 ++-OnHead : ∀ {A} {xs ys : List A} {y : A} {_<_ : A → A → Set}
           → OnHead _<_ y xs
           → OnHead _<_ y ys
           → OnHead _<_ y (xs ++ ys)
 ++-OnHead []         y<y₁ = y<y₁
 ++-OnHead (on-∷ y<x) _    = on-∷ y<x

 h∉t : ∀ {A} {t : List A} {h : A} {_<_ : A → A → Set}
     → Irreflexive _<_ _≡_ → Transitive _<_
     → IsSorted _<_ (h ∷ t)
     → h ∉ t
 h∉t irfl trans (on-∷ h< ∷ sxs) (here refl) = ⊥-elim (irfl h< refl)
 h∉t irfl trans (on-∷ h< ∷ (x₁< ∷ sxs)) (there h∈t)
   = h∉t irfl trans ((transOnHead trans x₁< h<) ∷ sxs) h∈t

 ≤-head : ∀ {A} {l : List A} {x y : A} {_<_ : A → A → Set} {_≤_ : A → A → Set}
        → Reflexive _≤_ → Trans _<_ _≤_ _≤_
        → y ∈ (x ∷ l) → IsSorted _<_ (x ∷ l)
        → _≤_ x y
 ≤-head ref≤ trans (here refl) _ = ref≤
 ≤-head ref≤ trans (there y∈) (on-∷ x<x₁ ∷ sl) = trans x<x₁ (≤-head ref≤ trans y∈ sl)

 -- TODO-1 : Better name and/or replace with library property
 Any-sym : ∀ {a b}{A : Set a}{B : Set b}{tgt : B}{l : List A}{f : A → B}
         → Any (λ x → tgt ≡ f x) l
         → Any (λ x → f x ≡ tgt) l
 Any-sym (here x)  = here (sym x)
 Any-sym (there x) = there (Any-sym x)

 Any-lookup-correct :  ∀ {a b}{A : Set a}{B : Set b}{tgt : B}{l : List A}{f : A → B}
                    → (p : Any (λ x → f x ≡ tgt) l)
                    → Any-lookup p ∈ l
 Any-lookup-correct (here px) = here refl
 Any-lookup-correct (there p) = there (Any-lookup-correct p)

 Any-lookup-correctP :  ∀ {a}{A : Set a}{l : List A}{P : A → Set}
                     → (p : Any P l)
                     → Any-lookup p ∈ l
 Any-lookup-correctP (here px) = here refl
 Any-lookup-correctP (there p) = there (Any-lookup-correctP p)

 Any-witness : ∀ {a b} {A : Set a} {l : List A} {P : A → Set b}
             → (p : Any P l) → P (Any-lookup p)
 Any-witness (here px) = px
 Any-witness (there x) = Any-witness x

 -- TODO-1: there is probably a library property for this.
 ∈⇒Any : ∀ {A : Set}{x : A}
       → {xs : List A}
       → x ∈ xs
       → Any (_≡ x) xs
 ∈⇒Any {x = x} (here refl) = here refl
 ∈⇒Any {x = x} {h ∷ t} (there xxxx) = there (∈⇒Any {xs = t} xxxx)

 false≢true : false ≢ true
 false≢true ()

 witness : {A : Set}{P : A → Set}{x : A}{xs : List A}
         → x ∈ xs → All P xs → P x
 witness x y = All-lookup y x

 maybe-⊥ : ∀{a}{A : Set a}{x : A}{y : Maybe A}
         → y ≡ just x
         → y ≡ nothing
         → ⊥
 maybe-⊥ () refl

 Maybe-map-cool : ∀ {S S₁ : Set} {f : S → S₁} {x : Maybe S} {z}
                → Maybe-map f x ≡ just z
                → x ≢ nothing
 Maybe-map-cool {x = nothing} ()
 Maybe-map-cool {x = just y} prf = λ x → ⊥-elim (maybe-⊥ (sym x) refl)

 Maybe-map-cool-1 : ∀ {S S₁ : Set} {f : S → S₁} {x : Maybe S} {z}
                  → Maybe-map f x ≡ just z
                  → Σ S (λ x' → f x' ≡ z)
 Maybe-map-cool-1 {x = nothing} ()
 Maybe-map-cool-1 {x = just y} {z = z} refl = y , refl

 Maybe-map-cool-2 : ∀ {S S₁ : Set} {f : S → S₁} {x : S} {z}
                  → f x ≡ z
                  → Maybe-map f (just x) ≡ just z
 Maybe-map-cool-2 {S}{S₁}{f}{x}{z} prf rewrite prf = refl

 T⇒true : ∀ {a : Bool} → T a → a ≡ true
 T⇒true {true} _ = refl

 isJust : ∀ {A : Set}{aMB : Maybe A}{a : A}
        → aMB ≡ just a
        → Is-just aMB
 isJust refl = just tt

 to-witness-isJust-≡ : ∀ {A : Set}{aMB : Maybe A}{a prf}
                     → to-witness (isJust {aMB = aMB} {a} prf) ≡ a
 to-witness-isJust-≡ {aMB = just a'} {a} {prf}
    with to-witness-lemma (isJust {aMB = just a'} {a} prf) refl
 ...| xxx = just-injective (trans (sym xxx) prf)

 deMorgan : ∀ {A B : Set} → (¬ A) ⊎ (¬ B) → ¬ (A × B)
 deMorgan (inj₁ ¬a) = λ a×b → ¬a (proj₁ a×b)
 deMorgan (inj₂ ¬b) = λ a×b → ¬b (proj₂ a×b)

 ¬subst : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {P : A → Set ℓ₂}
        → {x y : A}
        → ¬ (P x)
        → y ≡ x
        → ¬ (P y)
 ¬subst px refl = px

 ∸-suc-≤ : ∀ (x w : ℕ) → suc x ∸ w ≤ suc (x ∸ w)
 ∸-suc-≤ x zero = ≤-refl
 ∸-suc-≤ zero (suc w) rewrite 0∸n≡0 w = z≤n
 ∸-suc-≤ (suc x) (suc w) = ∸-suc-≤ x w

 m∸n≤o⇒m∸o≤n : ∀ (x z w : ℕ) → x ∸ z ≤ w → x ∸ w ≤ z
 m∸n≤o⇒m∸o≤n x zero w p≤ rewrite m≤n⇒m∸n≡0 p≤ = z≤n
 m∸n≤o⇒m∸o≤n zero (suc z) w p≤ rewrite 0∸n≡0 w = z≤n
 m∸n≤o⇒m∸o≤n (suc x) (suc z) w p≤ = ≤-trans (∸-suc-≤ x w) (s≤s (m∸n≤o⇒m∸o≤n x z w p≤))

 tail-⊆ : ∀ {A : Set} {x} {xs ys : List A}
        → (x ∷ xs) ⊆List ys
        → xs ⊆List ys
 tail-⊆ xxs⊆ys x∈xs = xxs⊆ys (there x∈xs)

 allDistinctTail : ∀ {A : Set} {x} {xs : List A}
                 → allDistinct (x ∷ xs)
                 → allDistinct xs
 allDistinctTail allDist i j
   with allDist (suc i) (suc j)
 ...| inj₁ refl    = inj₁ refl
 ...| inj₂ lookup≢ = inj₂ lookup≢

 ∈-Any-Index-elim : ∀ {A : Set} {x y} {ys : List A} (x∈ys : x ∈ ys)
                  → x ≢ y → y ∈ ys
                  → y ∈ ys ─ Any-index x∈ys
 ∈-Any-Index-elim (here refl)  x≢y (here refl)  = ⊥-elim (x≢y refl)
 ∈-Any-Index-elim (here refl)  _   (there y∈ys) = y∈ys
 ∈-Any-Index-elim (there _)    _   (here refl)  = here refl
 ∈-Any-Index-elim (there x∈ys) x≢y (there y∈ys) = there (∈-Any-Index-elim x∈ys x≢y y∈ys)

 ∉∧⊆List⇒∉ : ∀ {A : Set} {x} {xs ys : List A}
           → x ∉ xs → ys ⊆List xs
           → x ∉ ys
 ∉∧⊆List⇒∉ x∉xs ys∈xs x∈ys = ⊥-elim (x∉xs (ys∈xs x∈ys))

 allDistinctʳʳ : ∀ {A : Set} {x x₁ : A} {xs : List A}
               → allDistinct (x ∷ x₁ ∷ xs)
               → allDistinct (x ∷ xs)
 allDistinctʳʳ _ zero zero = inj₁ refl
 allDistinctʳʳ allDist zero (suc j)
   with allDist zero (suc (suc j))
 ...| inj₂ x≢lookup
      = inj₂ λ x≡lkpxs → ⊥-elim (x≢lookup x≡lkpxs)
 allDistinctʳʳ allDist (suc i) zero
   with allDist (suc (suc i)) zero
 ...| inj₂ x≢lookup
      = inj₂ λ x≡lkpxs → ⊥-elim (x≢lookup x≡lkpxs)
 allDistinctʳʳ allDist (suc i) (suc j)
   with allDist (suc (suc i)) (suc (suc j))
 ...| inj₁ refl    = inj₁ refl
 ...| inj₂ lookup≡ = inj₂ lookup≡

 allDistinct⇒∉ : ∀ {A : Set} {x} {xs : List A}
               → allDistinct (x ∷ xs)
               → x ∉ xs
 allDistinct⇒∉ allDist (here x≡x₁)
   with allDist zero (suc zero)
 ... | inj₂ x≢x₁ = ⊥-elim (x≢x₁ x≡x₁)
 allDistinct⇒∉ allDist (there x∈xs)
   = allDistinct⇒∉ (allDistinctʳʳ allDist) x∈xs

 sumListMap : ∀ {A : Set} {x} {xs : List A} (f : A → ℕ) → (x∈xs : x ∈ xs)
            → f-sum f xs ≡ f x + f-sum f (xs ─ Any-index x∈xs)
 sumListMap _ (here refl)  = refl
 sumListMap {_} {x} {x₁ ∷ xs} f (there x∈xs)
   rewrite sumListMap f x∈xs
         | sym (+-assoc (f x) (f x₁) (f-sum f (xs ─ Any-index x∈xs)))
         | +-comm (f x) (f x₁)
         | +-assoc (f x₁) (f x) (f-sum f (xs ─ Any-index x∈xs)) = refl

 lookup⇒Any : ∀ {A : Set} {xs : List A} {P : A → Set} (i : Fin (length xs))
            → P (List-lookup xs i) → Any P xs
 lookup⇒Any {_} {_ ∷ _} zero    px = here px
 lookup⇒Any {_} {_ ∷ _} (suc i) px = there (lookup⇒Any i px)

 x∉→AllDistinct : ∀ {A : Set} {x} {xs : List A}
                → allDistinct xs
                → x ∉ xs
                → allDistinct (x ∷ xs)
 x∉→AllDistinct _ _ zero zero = inj₁ refl
 x∉→AllDistinct _ x∉xs zero (suc j)
   = inj₂ λ x≡lkp → x∉xs (lookup⇒Any j x≡lkp)
 x∉→AllDistinct _ x∉xs (suc i) (zero)
   = inj₂ λ x≡lkp → x∉xs (lookup⇒Any i (sym x≡lkp))
 x∉→AllDistinct allDist x∉xs (suc i) (suc j)
   with allDist i j
 ...| inj₁ refl  = inj₁ refl
 ...| inj₂ lkup≢ = inj₂ lkup≢

 cast-injective : ∀ {n m} {i j : Fin n} {eq : n ≡ m}
                → cast eq i ≡ cast eq j → i ≡ j
 cast-injective {_} {_} {zero} {zero}   {refl} _ = refl
 cast-injective {_} {_} {suc i} {suc j} {refl} ci≡cj
   = cong suc (cast-injective {eq = refl} (Fin-suc-injective ci≡cj))

 List-lookup-map : ∀ {A B : Set} (xs : List A) (f : A → B) (α : Fin (length xs))
                 → let cα = cast (sym (List-length-map f xs)) α
                   in f (List-lookup xs α) ≡ List-lookup (List-map f xs) cα
 List-lookup-map (x ∷ xs) f zero = refl
 List-lookup-map (x ∷ xs) f (suc α) = List-lookup-map xs f α

 allDistinct-Map : ∀ {A B : Set} {xs : List A} {α₁ α₂ : Fin (length xs)} (f : A → B)
                 → allDistinct (List-map f xs) → α₁ ≢ α₂
                 → f (List-lookup xs α₁) ≢ f (List-lookup xs α₂)
 allDistinct-Map {_} {_} {xs} {α₁} {α₂} f all≢ α₁≢α₂ flkp≡
    with all≢ (cast (sym (List-length-map f xs)) α₁)
             (cast (sym (List-length-map f xs)) α₂)
 ...| inj₁ cα₁≡cα₂  = ⊥-elim (α₁≢α₂ (cast-injective {eq = sym (List-length-map f xs)} cα₁≡cα₂))
 ...| inj₂ lkpα₁α₂≢ = ⊥-elim (lkpα₁α₂≢ (trans (sym (List-lookup-map xs f α₁))
                                               (trans flkp≡ (List-lookup-map xs f α₂))))

 filter⊆ : ∀ {A : Set} {P : A → Set} {P? : (a : A) → Dec (P a)} {xs : List A}
         → List-filter P? xs ⊆List xs
 filter⊆ {P? = P?} x∈fxs = Any-filter⁻ P? x∈fxs

 ⊆⇒filter⊆ : ∀ {A : Set} {P : A → Set} {P? : (a : A) → Dec (P a)} {xs ys : List A}
           → xs ⊆List ys
           → List-filter P? xs ⊆List List-filter P? ys
 ⊆⇒filter⊆ {P? = P?} {xs = xs} {ys = ys} xs∈ys x∈fxs
   with List-∈-filter⁻ P? {xs = xs} x∈fxs
 ...| x∈xs , px = List-∈-filter⁺ P? (xs∈ys x∈xs) px

 map∘filter : ∀ {A B : Set} (xs : List A) (ys : List B) (f : A → B)
                {P : B → Set} (P? : (b : B) → Dec (P b))
            → List-map f xs ≡ ys
            → List-map f (List-filter (P? ∘ f) xs) ≡ List-filter P? ys
 map∘filter [] [] _ _ _ = refl
 map∘filter (x ∷ xs) (.(f x) ∷ .(List-map f xs)) f P? refl
    with P? (f x)
 ...| yes prf = cong (f x ∷_) (map∘filter xs (List-map f xs) f P? refl)
 ...| no imp = map∘filter xs (List-map f xs) f P? refl

 allDistinct-Filter : ∀ {A : Set} {P : A → Set} {P? : (a : A) → Dec (P a)} {xs : List A}
                    → allDistinct xs
                    → allDistinct (List-filter P? xs)
 allDistinct-Filter {P? = P?} {xs = x ∷ xs} all≢ i j
    with P? x
 ...| no imp = allDistinct-Filter {P? = P?} {xs = xs} (allDistinctTail all≢) i j
 ...| yes prf = let all≢Tail = allDistinct-Filter {P? = P?} {xs = xs} (allDistinctTail all≢)
                    x∉Tail = allDistinct⇒∉ all≢
                in x∉→AllDistinct all≢Tail (∉∧⊆List⇒∉ x∉Tail filter⊆) i j

 sum-f∘g : ∀ {A B : Set} (xs : List A) (g : B → ℕ) (f : A → B)
         → f-sum (g ∘ f) xs ≡ f-sum g (List-map f xs)
 sum-f∘g xs g f = cong sum (List-map-compose xs)

 map-lookup-allFin : ∀ {A : Set} (xs : List A)
                   → List-map (List-lookup xs) (allFin (length xs)) ≡ xs
 map-lookup-allFin xs = trans (map-tabulate id (List-lookup xs)) (tabulate-lookup xs)

 list-index : ∀ {A B : Set} {P : A → B → Set} (_∼_ : Decidable P)
              (xs : List A) → B → Maybe (Fin (length xs))
 list-index _∼_ [] x = nothing
 list-index _∼_ (x ∷ xs) y
    with x ∼ y
 ...| yes x≡y = just zero
 ...| no  x≢y
    with list-index _∼_ xs y
 ...| nothing = nothing
 ...| just i  = just (suc i)

 module DecLemmas {A : Set} (_≟D_ : Decidable {A = A} (_≡_)) where

   _∈?_ : ∀ (x : A) → (xs : List A) → Dec (Any (x ≡_) xs)
   x ∈? xs = Any-any (x ≟D_) xs

   y∉xs⇒Allxs≢y : ∀ {xs : List A} {x y}
                → y ∉ (x ∷ xs)
                → x ≢ y × y ∉ xs
   y∉xs⇒Allxs≢y {xs} {x} {y} y∉
     with y ∈? xs
   ...| yes y∈xs = ⊥-elim (y∉ (there y∈xs))
   ...| no  y∉xs
     with x ≟D y
   ...| yes x≡y = ⊥-elim (y∉ (here (sym x≡y)))
   ...| no  x≢y = x≢y , y∉xs

   ⊆List-Elim :  ∀ {x} {xs ys : List A} (x∈ys : x ∈ ys)
              → x ∉ xs → xs ⊆List ys
              → xs ⊆List ys ─ Any-index x∈ys
   ⊆List-Elim (here refl) x∉xs xs∈ys x₂∈xs
     with xs∈ys x₂∈xs
   ...| here refl  = ⊥-elim (x∉xs x₂∈xs)
   ...| there x∈xs = x∈xs
   ⊆List-Elim (there x∈ys) x∉xs xs∈ys x₂∈xxs
     with x₂∈xxs
   ...| there x₂∈xs
         = ⊆List-Elim (there x∈ys) (proj₂ (y∉xs⇒Allxs≢y x∉xs)) (tail-⊆ xs∈ys) x₂∈xs
   ...| here refl
     with xs∈ys x₂∈xxs
   ...| here refl = here refl
   ...| there x₂∈ys
         = there (∈-Any-Index-elim x∈ys (≢-sym (proj₁ (y∉xs⇒Allxs≢y x∉xs))) x₂∈ys)

   sum-⊆-≤ : ∀ {ys} (xs : List A) (f : A → ℕ)
           → allDistinct xs
           → xs ⊆List ys
           → f-sum f xs ≤ f-sum f ys
   sum-⊆-≤ [] _ _ _ = z≤n
   sum-⊆-≤ (x ∷ xs) f dxs xs⊆ys
      rewrite sumListMap f (xs⊆ys (here refl))
      = let x∉xs    = allDistinct⇒∉ dxs
            xs⊆ysT  = tail-⊆ xs⊆ys
            xs⊆ys-x = ⊆List-Elim (xs⊆ys (here refl)) x∉xs xs⊆ysT
            disTail = allDistinctTail dxs
       in +-monoʳ-≤ (f x) (sum-⊆-≤ xs f disTail xs⊆ys-x)

   ⊆-allFin : ∀ {n} {xs : List (Fin n)} → xs ⊆List allFin n
   ⊆-allFin {x = x} _ = Any-tabulate⁺ x refl

   intersect : List A → List A → List A
   intersect xs [] = []
   intersect xs (y ∷ ys)
     with y ∈? xs
   ...| yes _ = y ∷ intersect xs ys
   ...| no  _ = intersect xs ys

   union : List A → List A → List A
   union xs [] = xs
   union xs (y ∷ ys)
     with y ∈? xs
   ...| yes _ = union xs ys
   ...| no  _ = y ∷ union xs ys

   ∈-intersect : ∀ (xs ys : List A) {α}
               → α ∈ intersect xs ys
               → α ∈ xs × α ∈ ys
   ∈-intersect xs (y ∷ ys) α∈int
     with y ∈? xs  | α∈int
   ...| no  y∉xs   | α∈        = ×-map₂ there (∈-intersect xs ys α∈)
   ...| yes y∈xs   | here refl = y∈xs , here refl
   ...| yes y∈xs   | there α∈  = ×-map₂ there (∈-intersect xs ys α∈)

   x∉⇒x∉intersect : ∀ {x} {xs ys : List A}
                    → x ∉ xs ⊎ x ∉ ys
                    → x ∉ intersect xs ys
   x∉⇒x∉intersect {x} {xs} {ys} x∉ x∈int
     = contraposition (∈-intersect xs ys) (deMorgan x∉) x∈int

   intersectDistinct : ∀ (xs ys : List A)
                     → allDistinct xs → allDistinct ys
                     → allDistinct (intersect xs ys)
   intersectDistinct xs (y ∷ ys) dxs dys
     with y ∈? xs
   ...| yes y∈xs = let distTail  = allDistinctTail dys
                       intDTail  = intersectDistinct xs ys dxs distTail
                       y∉intTail = x∉⇒x∉intersect (inj₂ (allDistinct⇒∉ dys))
                   in x∉→AllDistinct intDTail y∉intTail
   ...| no  y∉xs = intersectDistinct xs ys dxs (allDistinctTail dys)

   x∉⇒x∉union : ∀ {x} {xs ys : List A}
              → x ∉ xs × x ∉ ys
              → x ∉ union xs ys
   x∉⇒x∉union {_} {_} {[]} (x∉xs , _) x∈∪ = ⊥-elim (x∉xs x∈∪)
   x∉⇒x∉union {x} {xs} {y ∷ ys} (x∉xs , x∉ys) x∈union
     with y ∈? xs  | x∈union
   ...| yes y∈xs   | x∈∪
        = ⊥-elim (x∉⇒x∉union (x∉xs , (proj₂ (y∉xs⇒Allxs≢y x∉ys))) x∈∪)
   ...| no y∉xs    | here refl
        = ⊥-elim (proj₁ (y∉xs⇒Allxs≢y x∉ys) refl)
   ...| no y∉xs    | there x∈∪
        = ⊥-elim (x∉⇒x∉union (x∉xs , (proj₂ (y∉xs⇒Allxs≢y x∉ys))) x∈∪)

   unionDistinct : ∀ (xs ys : List A)
               → allDistinct xs → allDistinct ys
               → allDistinct (union xs ys)
   unionDistinct xs [] dxs dys = dxs
   unionDistinct xs (y ∷ ys) dxs dys
      with y ∈? xs
   ...| yes y∈xs = unionDistinct xs ys dxs (allDistinctTail dys)
   ...| no  y∉xs = let distTail  = allDistinctTail dys
                       uniDTail  = unionDistinct xs ys dxs distTail
                       y∉intTail = x∉⇒x∉union (y∉xs , allDistinct⇒∉ dys)
                   in x∉→AllDistinct uniDTail y∉intTail

   sumIntersect≤ : ∀ (xs ys : List A) (f : A → ℕ)
                 → f-sum f (intersect xs ys) ≤ f-sum f (xs ++ ys)
   sumIntersect≤ _ [] _ = z≤n
   sumIntersect≤ xs (y ∷ ys) f
     with y ∈? xs
   ...| yes y∈xs rewrite map-++-commute f xs (y ∷ ys)
                       | sum-++-commute (List-map f xs) (List-map f (y ∷ ys))
                       | sym (+-assoc (f-sum f xs) (f y) (f-sum f ys))
                       | +-comm (f-sum f xs) (f y)
                       | +-assoc (f y) (f-sum f xs) (f-sum f ys)
                       | sym (sum-++-commute (List-map f xs) (List-map f ys))
                       | sym (map-++-commute f xs ys)
                         = +-monoʳ-≤ (f y) (sumIntersect≤ xs ys f)
   ...| no  y∉xs rewrite map-++-commute f xs (y ∷ ys)
                       | sum-++-commute (List-map f xs) (List-map f (y ∷ ys))
                       | +-comm (f y) (f-sum f ys)
                       | sym (+-assoc (f-sum f xs) (f-sum f ys) (f y))
                       | sym (sum-++-commute (List-map f xs) (List-map f ys))
                       | sym (map-++-commute f xs ys)
                         = ≤-stepsʳ (f y) (sumIntersect≤ xs ys f)

   index∘lookup-id : ∀ {B : Set} (xs : List B) (f : B → A)
                   → allDistinct (List-map f xs) → {α : Fin (length xs)}
                   → list-index (_≟D_ ∘ f) xs ((f ∘ List-lookup xs) α) ≡ just α
   index∘lookup-id (x ∷ xs) f all≢ {zero}
      with f x ≟D f x
   ...| yes fx≡fx = refl
   ...| no  fx≢fx = ⊥-elim (fx≢fx refl)
   index∘lookup-id (x ∷ xs) f all≢ {suc α}
      with f x ≟D f (List-lookup xs α)
   ...| yes fx≡lkp = ⊥-elim (allDistinct⇒∉ all≢ (Any-map⁺ (lookup⇒Any α fx≡lkp)))
   ...| no  fx≢lkp
      with list-index (_≟D_ ∘ f) xs (f (List-lookup xs α))
         | index∘lookup-id xs f (allDistinctTail all≢) {α}
   ...| just .α | refl = refl

   lookup∘index-id : ∀ {B : Set} (xs : List B) (f : B → A)
                   → allDistinct (List-map f xs) → {α : Fin (length xs)} {x : A}
                   → list-index (_≟D_ ∘ f) xs x ≡ just α
                   → (f ∘ List-lookup xs) α ≡ x
   lookup∘index-id (x₁ ∷ xs) f all≢ {α} {x} lkp≡α
      with f x₁ ≟D x
   ...| yes fx≡nId rewrite sym (just-injective lkp≡α) = fx≡nId
   ...| no  fx≢nId
      with list-index (_≟D_ ∘ f) xs x | inspect (list-index (_≟D_ ∘ f) xs) x
   ...| just _ | [ eq ] rewrite sym (just-injective lkp≡α)
        = lookup∘index-id xs f (allDistinctTail all≢) eq


text:
module Cats.Category.Setoids.Facts where

open import Cats.Category
open import Cats.Category.Setoids using (Setoids)
open import Cats.Category.Setoids.Facts.Exponentials using (hasExponentials)
open import Cats.Category.Setoids.Facts.Initial using (hasInitial)
open import Cats.Category.Setoids.Facts.Products
  using (hasProducts ; hasBinaryProducts)
open import Cats.Category.Setoids.Facts.Terminal using (hasTerminal)

instance
  isCCC : ∀ l → IsCCC (Setoids l l)
  isCCC l = record { hasFiniteProducts = record {} } -- [1]

-- [1] For no discernible reason, `record {}` doesn't work.

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
module AML where

open import Level
open import Data.Product

data satisfied (a : Set) (m : Set → Set) : Set where
  s : m a → satisfied a m

data reachability (m₀ : Set → Set) (m : Set → Set) : Set where
  tt : reachability m₀ m

data necessarity (m₀ : Set → Set) (a : Set) : Set₁ where
  n : ∀ m → (reachability m₀ m) → satisfied a m → necessarity m₀ a

□_ : Set → Set₁
□_ = necessarity {!!}

data posibility (m₀ : Set → Set) (a : Set) : Set₁ where
  p : ∃[ m ](reachability m₀ m → satisfied a m) → posibility m₀ a

◇_ : Set → Set₁
◇_ = posibility {!!}

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
module Array.Properties where

open import Array.Base
open import Data.Fin using (Fin; zero; suc; raise; fromℕ≤; fromℕ<; fromℕ)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Vec
open import Data.Vec.Properties
open import Relation.Binary.PropositionalEquality
open import Function using (_$_; _∘_; case_of_)

open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Negation
open import Relation.Binary using (Decidable; Rel)

open import Data.Maybe
open import Data.Sum

sel-ext : ∀ {a}{X : Set a}{d s} → (f : Ix d s → X)
        → (iv jv : Ix d s)
        → iv =ix jv
        → f iv ≡ f jv
sel-ext {d = zero}  f [] [] pf = refl
sel-ext {d = suc d} f (i ∷ iv) (j ∷ jv) pf rewrite (pf zero) = sel-ext (f ∘ (j ∷_)) iv jv (pf ∘ suc)

s→a∘a→s : ∀ {n} → (a : Ar ℕ 1 (n ∷ [])) → s→a (a→s a) =a a
s→a∘a→s (imap x) (i ∷ []) = lookup∘tabulate _ i

a→s∘s→a : ∀ {n} → (v : Vec ℕ n) → a→s (s→a v) =s v
a→s∘s→a v i = lookup∘tabulate _ i

refl-=a : ∀ {a}{X : Set a}{d s}{x : Ar X d s}
        → x =a x
refl-=a {x = imap x} iv = refl

sym-=a : ∀ {a}{X : Set a}{d s}{l r : Ar X d s}
       → l =a r → r =a l
sym-=a {l = imap f} {imap g} l=r = sym ∘ l=r

trans-=a : ∀ {a}{X : Set a}{d s}{x y z : Ar X d s}
         → x =a y → y =a z → x =a z
trans-=a {x = imap x} {imap y} {imap z} x=y y=z iv
  = trans (x=y iv) (y=z iv)

_<v?_ : ∀ {n} → Decidable (_<s_ {n = n})
[] <v? [] = yes λ ()
(x ∷ xs) <v? (y ∷ ys) = case _,_ {B = λ x₂ → Dec (xs <s ys) }(x <? y) (xs <v? ys) of λ where
                         (yes pf-xy , yes pf-xsys) → yes λ where
                                                         zero    → pf-xy
                                                         (suc i) → pf-xsys i
                         (no pf-xy , _) → no (not-head pf-xy)
                         (_ , no pf-xsys) → no (not-tail pf-xsys)
  where
    p1 : ∀ {n}{x y}{xs ys : Vec ℕ n} → (x ∷ xs) <s (y ∷ ys) → x < y
    p1 pf = pf zero

    p2 : ∀ {n}{x y}{xs ys : Vec ℕ n} → (x ∷ xs) <s (y ∷ ys) → xs <s ys
    p2 pf = pf ∘ (raise 1)

    not-head : ∀ {n}{x y}{xs ys : Vec ℕ n} → ¬ (x < y) → ¬ ((x ∷ xs) <s (y ∷ ys))
    not-head pf-xy pf-xxs-yys = contradiction (p1 pf-xxs-yys) pf-xy

    not-tail : ∀ {n}{x y}{xs ys : Vec ℕ n} → ¬ (xs <s ys) → ¬ ((x ∷ xs) <s (y ∷ ys))
    not-tail pf-xsys pf-xxs-yys = contradiction (p2 pf-xxs-yys) pf-xsys

-- Index curry makes it possible to fix the first position of
-- the index vector and select a sub-array.
ix-curry : ∀ {a}{X : Set a}{d s ss} → (f : Ix (suc d) (s ∷ ss) → X) → (Fin s) → (Ix d ss → X)
ix-curry f x xs = f (x ∷ xs)

ARel : ∀ {a}{A : Set a} → (P : Rel A a) -- → Decidable P
     → ∀ {d s} → Ar A d s → Ar A d s → Set a
ARel p (imap x) (imap y) = ∀ iv → p (x iv) (y iv)

--test = ARel _≥_

-- If a < b, then sub-arays a[i] < b[i], where a[i] and b[i]
-- is non-scalar selection where the head of index-vector is
-- fixed to i.
all-subarrays : ∀ {d s ss}{a}{X : Set a}{_~_ : Rel X a}
              → let _~a_ = ARel _~_ in
                (a b : Ix (suc d) (suc s ∷ ss) → X)
              → imap a ~a imap b
              → ∀ i → (imap (ix-curry a i) ~a imap (ix-curry b i))
all-subarrays a b pf i iv = pf (i ∷ iv)

-- If all a[i] < b[i], then a < b.
from-subarrays : ∀ {d s ss}{a}{X : Set a}{_~_ : Rel X a}
               → let _~a_ = ARel _~_ in
                 (a b : Ix (suc d) (suc s ∷ ss) → X)
               → (∀ i → (imap (ix-curry a i) ~a imap (ix-curry b i)))
               → imap a ~a imap b
from-subarrays a b pf (x ∷ iv) = pf x iv

-- If there exists i such that ¬ a[i] < b[i], then ¬ a < b.
not-subarrays : ∀ {d s ss}{a}{X : Set a}{_~_ : Rel X a}
              → let _~a_ = ARel _~_ in
                (a b : Ix (suc d) (suc s ∷ ss) → X)
              → (i : Fin (suc s))
              → ¬ imap (ix-curry a i) ~a imap (ix-curry b i)
              → ¬ imap a ~a imap b
not-subarrays a b i ¬p pp = contradiction pp λ z → ¬p (λ iv → z (i ∷ iv))

module not-needed where
  unmaybe : ∀ {a}{X : Set a}{n}
          → (x : Vec (Maybe X) n)
          → (∀ i → lookup x i ≢ nothing)
          → Vec X n
  unmaybe {n = zero} x pf = []
  unmaybe {n = suc n} (just x ∷ xs) pf = x ∷ unmaybe xs (pf ∘ suc)
  unmaybe {n = suc n} (nothing ∷ x₁) pf = contradiction refl $ pf zero

  check-all-nothing : ∀ {a}{X : Set a}{n}
                    → (x : Vec (Maybe X) n)
                    → Maybe ((i : Fin n) → lookup x i ≢ nothing)
  check-all-nothing {n = zero} x = nothing
  check-all-nothing {n = suc n} (just x  ∷ xs) with check-all-nothing xs
  check-all-nothing {n = suc n} (just x ∷ xs) | just f = just λ { zero → λ () ; (suc k) → f k }
  check-all-nothing {n = suc n} (just x ∷ xs) | nothing = nothing
  check-all-nothing {n = suc n}  _  = nothing

check-all-subarrays : ∀ {d s ss}{a}{X : Set a}{_~_ : Rel X a}
                    → let _~a_ = ARel _~_ in
                      (a b : Ix (suc d) (suc s ∷ ss) → X)
                    → (∀ i → Dec (imap (ix-curry a i) ~a imap (ix-curry b i)))
                    → (Σ (Fin (suc s)) λ i → ¬ (imap (ix-curry a i) ~a imap (ix-curry b i)))
                    ⊎ (∀ i → (imap (ix-curry a i) ~a imap (ix-curry b i)))
check-all-subarrays {s = zero}  a b pf with (pf zero)
check-all-subarrays {_} {zero}  a b pf | yes p = inj₂ λ { zero → p }
check-all-subarrays {_} {zero}  a b pf | no ¬p = inj₁ (zero , ¬p)
check-all-subarrays {s = suc s} {_~_ = _~_} a b pf with check-all-subarrays {_~_ = _~_}
                                                                (λ { (i ∷ iv) → a (suc i ∷ iv)})
                                                                (λ { (i ∷ iv) → b (suc i ∷ iv)})
                                                                (pf ∘ suc)
                                         -- If we have a subarray that is not <
                                         -- simply propagate it further, updating the index
check-all-subarrays {_} {suc s} a b pf | inj₁ (i , a≁b) = inj₁ (suc i , a≁b)
check-all-subarrays {_} {suc s} a b pf | inj₂ y with (pf zero)
check-all-subarrays {_} {suc s} a b pf | inj₂ y | yes p = inj₂ λ { zero → p ; (suc k) → y k }
check-all-subarrays {_} {suc s} a b pf | inj₂ y | no ¬p = inj₁ (zero , ¬p)

{-
-- For arrays a and b, if f : ∀ i → Dec (a[i] < b[i]),
-- check whether:
--   1. There exists i, for which ¬ a[i] < b[i]
--   2. Otherwise construct a function of type ∀ i → a[i] < b[i]
check-all-subarrays : ∀ {d s ss}
                    → (a b : Ix (suc d) (suc s ∷ ss) → ℕ)
                    → (∀ i → Dec (imap (ix-curry a i) <a imap (ix-curry b i)))
                    → (Σ (Fin (suc s)) λ i → ¬ (imap (ix-curry a i) <a imap (ix-curry b i)))
                    ⊎ (∀ i → (imap (ix-curry a i) <a imap (ix-curry b i)))
check-all-subarrays {s = zero}  a b pf with (pf zero)
check-all-subarrays {_} {zero}  a b pf | yes p = inj₂ λ { zero → p }
check-all-subarrays {_} {zero}  a b pf | no ¬p = inj₁ (zero , ¬p)
check-all-subarrays {s = suc s} a b pf with check-all-subarrays (λ { (i ∷ iv) → a (suc i ∷ iv)})
                                                                (λ { (i ∷ iv) → b (suc i ∷ iv)})
                                                                (pf ∘ suc)
                                         -- If we have a subarray that is not <
                                         -- simply propagate it further, updating the index
check-all-subarrays {_} {suc s} a b pf | inj₁ (i , a≮b) = inj₁ (suc i , a≮b)
check-all-subarrays {_} {suc s} a b pf | inj₂ y with (pf zero)
check-all-subarrays {_} {suc s} a b pf | inj₂ y | yes p = inj₂ λ { zero → p ; (suc k) → y k }
check-all-subarrays {_} {suc s} a b pf | inj₂ y | no ¬p = inj₁ (zero , ¬p)
-}

mk-dec-arel : ∀ {a}{X : Set a} → (p : Rel X a) → Decidable p → ∀ {d s} → Decidable (ARel p {d = d} {s = s})
mk-dec-arel _~_ _~?_ {zero} {[]} (imap x) (imap x₁) with x [] ~? x₁ []
mk-dec-arel _~_ _~?_ {zero} {[]} (imap x) (imap x₁) | yes p = yes λ { [] → p }
mk-dec-arel _~_ _~?_ {zero} {[]} (imap x) (imap x₁) | no ¬p =  no λ p → contradiction (p []) ¬p
mk-dec-arel _~_ _~?_ {suc d} {zero  ∷ ss} (imap x) (imap x₁) = yes λ iv → magic-fin $ ix-lookup iv zero
mk-dec-arel _~_ _~?_ {suc d} {suc s ∷ ss} (imap x) (imap x₁) = case-analysis
  where
    case-analysis : _ -- Dec ((i : Ix (suc d) (suc s ∷ ss)) → suc (x i) ≤ x₁ i)
    case-analysis = let _~a?_ = mk-dec-arel _~_ _~?_
                    in case check-all-subarrays {_~_ = _~_}
                          x x₁ (λ i → imap (ix-curry x i)
                                      ~a? imap (ix-curry x₁ i)) of λ where
                       -- In this case we have an index and a proof that
                       -- subarray at this index is not <
                       (inj₁ (i , x≁x₁)) → no $ not-subarrays {_~_ = _~_} x x₁ i x≁x₁
                       -- In this case we have a function that for every index
                       -- returns a proof that sub-arrays are <
                       (inj₂ f) → yes (from-subarrays {_~_ = _~_} x x₁ f)

_<a?_ = mk-dec-arel _<_ _<?_
_≥a?_ = mk-dec-arel _≥_ _≥?_

{-
_<a?_ : ∀ {d s} → Decidable (_<a_ {d = d} {s = s})
_<a?_ {zero} {[]} (imap x) (imap x₁) with x [] <? x₁ []
_<a?_ {zero} {[]} (imap x) (imap x₁) | yes p = yes λ { [] → p }
_<a?_ {zero} {[]} (imap x) (imap x₁) | no ¬p = no λ p → contradiction (p []) ¬p
_<a?_ {suc d} {0 ∷ ss} (imap x) (imap x₁) = yes λ iv → magic-fin $ ix-lookup iv zero
_<a?_ {suc d} {(suc s) ∷ ss} (imap x) (imap x₁) = case-analysis
  where
    case-analysis : _ -- Dec ((i : Ix (suc d) (suc s ∷ ss)) → suc (x i) ≤ x₁ i)
    case-analysis =  case check-all-subarrays {_~_ = _<_}
                          x x₁ (λ i → imap (ix-curry x i)
                                      <a? imap (ix-curry x₁ i)) of λ where
                       -- In this case we have an index and a proof that
                       -- subarray at this index is not <
                       (inj₁ (i , x≮x₁)) → no $ not-subarrays {_~_ = _<_} x x₁ i x≮x₁
                       -- In this case we have a function that for every index
                       -- returns a proof that sub-arrays are <
                       (inj₂ f) → yes (from-subarrays {_~_ = _<_} x x₁ f)

_≥a?_ : ∀ {d s} → Decidable (_≥a_ {d = d} {s = s})
_≥a?_ {zero} {[]} (imap x) (imap x₁) with x [] ≥? x₁ []
_≥a?_ {zero} {[]} (imap x) (imap x₁) | yes p = yes λ { [] → p }
_≥a?_ {zero} {[]} (imap x) (imap x₁) | no ¬p = no λ p → contradiction (p []) ¬p
_≥a?_ {suc d} {s} (imap x) (imap x₁) = {!!}
-}

private
  thm : ∀ { i s } → i < s → s ∸ i ∸ 1 + suc i ≡ s
  thm {i} {s} pf = begin
                      s ∸ i ∸ 1 + suc i ≡⟨ cong (_+ (suc i)) (∸-+-assoc s i 1) ⟩
                      s ∸ (i + 1) + suc i ≡⟨ cong (_+ (suc i)) (cong (s ∸_) (+-comm i 1))  ⟩
                      s ∸ suc i + suc i ≡⟨ m∸n+n≡m pf ⟩
                      s
                   ∎
                 where open ≡-Reasoning

-- XXX can we do this simpler?
≮a⇒∃ : ∀ {d s}{a b : Ar _ d s} → ¬ a <a b → Σ (Ix d s) λ iv → ¬ (unimap a iv < unimap b iv)
≮a⇒∃ {zero} {[]} {imap f} {imap g} ¬a<b with f [] <? g []
≮a⇒∃ {zero} {[]} {imap f} {imap g} ¬a<b | yes p = contradiction (λ { [] → p}) ¬a<b
≮a⇒∃ {zero} {[]} {imap f} {imap g} ¬a<b | no ¬p = [] , ¬p
≮a⇒∃ {suc d} {zero ∷ ss} {imap f} {imap g} ¬a<b = contradiction (λ iv → magic-fin $ ix-lookup iv zero) ¬a<b
≮a⇒∃ {suc d} {suc s ∷ ss} {imap f} {imap g} ¬a<b = case-analysis
  where
    case-analysis : _
    case-analysis =  case check-all-subarrays {_~_ = _<_}
                          f g (λ i → imap (ix-curry f i)
                                      <a? imap (ix-curry g i)) of λ where
                          (inj₁ (i , f≮g)) → let
                                               iv , pf = ≮a⇒∃ f≮g
                                             in (i ∷ iv) , λ pp → contradiction pp pf
                          (inj₂ pf) → contradiction (from-subarrays {_~_ = _<_} f g pf) ¬a<b

module try-irrelevant where
  -- XXX this shouldn't be here, this is for now to avoid
  -- dependencies in the modules.
  -- Inverse of the above
  a→ix : ∀ {d} --{s : Fin d → ℕ}
       → (ax sh : Ar ℕ 1 (d ∷ []))
       -- XXX we can make this inequality irrelevant
       -- and recompute it when it is needed, as <a
       -- is decideable.
       → .(ax <a sh)
       → Ix d (a→s sh)
  a→ix {d} (imap axf) (imap shf) ax<sh = ix-tabulate from-pf
    where
      pf : _
      pf = recompute (imap axf <a? imap shf) ax<sh

      from-pf : _
      from-pf i rewrite (lookup∘tabulate (shf ∘ (_∷ [])) i)
        = let
            ix : Ix 1 (d ∷ [])
            ix = i ∷ []
            r = raise (shf ix ∸ axf ix ∸ 1) $ fromℕ (axf ix)

           in subst Fin (thm (pf ix)) r --fromℕ≤ (ax<sh (i ∷ []))

a→ix : ∀ {d} --{s : Fin d → ℕ}
     → (ax sh : Ar ℕ 1 (d ∷ []))
     → (ax <a sh)
     → Ix d (a→s sh)
a→ix {d} (imap axf) (imap shf) ax<sh = ix-tabulate from-pf
  where
    from-pf : _
    from-pf i rewrite (lookup∘tabulate (shf ∘ (_∷ [])) i)
      = fromℕ< (ax<sh (i ∷ []))


text:
module Oscar.Class.Symmetry where

open import Oscar.Class.Extensionality
open import Oscar.Function
open import Oscar.Level

record Symmetry {a} {A : Set a} {ℓ} (_≤_ : A → A → Set ℓ) : Set (a ⊔ ℓ) where
  field
    ⦃ ′extensionality ⦄ : Extensionality _≤_ (λ ⋆ → flip _≤_ ⋆) id id

  symmetry : ∀ {x y} → x ≤ y → y ≤ x
  symmetry = extension (λ ⋆ → flip _≤_ ⋆)

open Symmetry ⦃ … ⦄ public hiding (′extensionality)

instance

  Symmetry⋆ : ∀
    {a} {A : Set a} {ℓ} {_≤_ : A → A → Set ℓ}
    ⦃ _ : Extensionality _≤_ (λ ⋆ → flip _≤_ ⋆) id id ⦄
    → Symmetry _≤_
  Symmetry.′extensionality Symmetry⋆ = it