text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
{-
This module develops Lehmer codes, i.e. an encoding of permutations as finite integers.

-}
module Cubical.Data.Fin.LehmerCode where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport

open import Cubical.Functions.Embedding
open import Cubical.Functions.Surjection

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq

open import Cubical.Data.Unit as ⊤
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Fin.Base as F
open import Cubical.Data.Fin.Properties
  renaming (punchOut to punchOutPrim)
open import Cubical.Data.Sigma
open import Cubical.Data.Sum as Sum using (_⊎_; inl; inr)

private
  variable
    n : ℕ

FinExcept : (i : Fin n) → Type₀
FinExcept i = Σ[ j ∈ Fin _ ] ¬ (i ≡ j)

isSetFinExcept : {i : Fin n} → isSet (FinExcept i)
isSetFinExcept = isOfHLevelΣ 2 isSetFin (λ _ → isProp→isSet (isPropΠ (λ _ → ⊥.isProp⊥)))

fsucExc : {i : Fin n} → FinExcept i → FinExcept (fsuc i)
fsucExc {i = i} j = fsuc (fst j) , snd j ∘ fsuc-inj

toFinExc : {i : Fin n} → FinExcept i → Fin n
toFinExc = fst

toFinExc-injective : {i : Fin n} → {j k : FinExcept i} → toFinExc j ≡ toFinExc k → j ≡ k
toFinExc-injective = Σ≡Prop (λ _ → isPropΠ λ _ → ⊥.isProp⊥)

toℕExc : {i : Fin n} → FinExcept i → ℕ
toℕExc = toℕ ∘ toFinExc

toℕExc-injective : {i : Fin n} → {j k : FinExcept i} → toℕExc j ≡ toℕExc k → j ≡ k
toℕExc-injective = toFinExc-injective ∘ toℕ-injective

projectionEquiv : {i : Fin n} → (Unit ⊎ FinExcept i) ≃ Fin n
projectionEquiv {n = n} {i = i} = isoToEquiv goal where
  goal : Iso (Unit ⊎ FinExcept i) (Fin n)
  goal .Iso.fun (inl _) = i
  goal .Iso.fun (inr m) = fst m
  goal .Iso.inv m = case discreteFin i m of λ { (yes _) → inl tt ; (no n) → inr (m , n) }
  goal .Iso.rightInv m with discreteFin i m
  ... | (yes p) = p
  ... | (no _) = toℕ-injective refl
  goal .Iso.leftInv (inl tt) with discreteFin i i
  ... | (yes _) = refl
  ... | (no ¬ii) = ⊥.rec (¬ii refl)
  goal .Iso.leftInv (inr m) with discreteFin i (fst m)
  ... | (yes p) = ⊥.rec (snd m p)
  ... | (no _) = cong inr (toℕExc-injective refl)

punchOut : (i : Fin (suc n)) → FinExcept i → Fin n
punchOut i ¬i = punchOutPrim (snd ¬i)

punchOut-injective : (i : Fin (suc n)) → ∀ j k → punchOut i j ≡ punchOut i k → j ≡ k
punchOut-injective i j k = toFinExc-injective ∘ punchOut-inj (snd j) (snd k)

punchIn : (i : Fin (suc n)) → Fin n → FinExcept i
punchIn {_} i j with fsplit i
...             | inl iz = fsuc j , fznotfs ∘ (iz ∙_)
punchIn {n} i j | inr (i′ , is) with n
...                 | zero = ⊥.rec (¬Fin0 j)
...                 | suc n′ with fsplit j
...                     | inl jz = fzero , fznotfs ∘ sym ∘ (is ∙_)
...                     | inr (j′ , _) =
                            let (k , ¬k≡i′) = punchIn i′ j′
                            in fsuc k , ¬k≡i′ ∘ fsuc-inj ∘ (is ∙_)

punchOut∘In :(i : Fin (suc n)) → ∀ j → punchOut i (punchIn i j) ≡ j
punchOut∘In {_} i j with fsplit i
...                 | inl iz = toℕ-injective refl
punchOut∘In {n} i j | inr (i′ , _) with n
...                     | zero = ⊥.rec (¬Fin0 j)
...                     | suc n′ with fsplit j
...                         | inl jz = toℕ-injective (cong toℕ jz)
...                         | inr (j′ , prfj) =
                              -- the following uses a definitional equality of punchIn but I don't see
                              -- how to sidestep this while using with-abstractions
                              fsuc (punchOut i′ _)               ≡⟨ cong (λ j → fsuc (punchOut i′ j)) (toℕExc-injective refl) ⟩
                              fsuc (punchOut i′ (punchIn i′ j′)) ≡⟨ cong fsuc (punchOut∘In i′ j′) ⟩
                              fsuc j′                            ≡⟨ toℕ-injective (cong toℕ prfj) ⟩
                              j                                  ∎

isEquivPunchOut : {i : Fin (suc n)} → isEquiv (punchOut i)
isEquivPunchOut {i = i} = isEmbedding×isSurjection→isEquiv (isEmbPunchOut , isSurPunchOut) where
  isEmbPunchOut : isEmbedding (punchOut i)
  isEmbPunchOut = injEmbedding isSetFinExcept isSetFin λ {_} {_} → punchOut-injective i _ _
  isSurPunchOut : isSurjection (punchOut i)
  isSurPunchOut b = ∣ _ , punchOut∘In i b ∣

punchOutEquiv : {i : Fin (suc n)} → FinExcept i ≃ Fin n
punchOutEquiv = _ , isEquivPunchOut

infixr 4 _∷_
data LehmerCode : (n : ℕ) → Type₀ where
  [] : LehmerCode zero
  _∷_ : ∀ {n} → Fin (suc n) → LehmerCode n → LehmerCode (suc n)

isContrLehmerZero : isContr (LehmerCode 0)
isContrLehmerZero = [] , λ { [] → refl }

lehmerSucEquiv : Fin (suc n) × LehmerCode n ≃ LehmerCode (suc n)
lehmerSucEquiv = isoToEquiv (iso (λ (e , c) → e ∷ c)
                                 (λ { (e ∷ c) → (e , c) })
                                 (λ { (e ∷ c) → refl })
                                 (λ (e , c) → refl))

lehmerEquiv : (Fin n ≃ Fin n) ≃ LehmerCode n
lehmerEquiv {zero} = isContr→Equiv contrFF isContrLehmerZero where
  contrFF : isContr (Fin zero ≃ Fin zero)
  contrFF = idEquiv _ , λ y → equivEq (funExt λ f → ⊥.rec (¬Fin0 f))

lehmerEquiv {suc n} =
  (Fin (suc n) ≃ Fin (suc n))                            ≃⟨ isoToEquiv i ⟩
  (Σ[ k ∈ Fin (suc n) ] (FinExcept fzero ≃ FinExcept k)) ≃⟨ Σ-cong-equiv-snd ii ⟩
  (Fin (suc n) × (Fin n ≃ Fin n))                        ≃⟨ Σ-cong-equiv-snd (λ _ → lehmerEquiv) ⟩
  (Fin (suc n) × LehmerCode n)                           ≃⟨ lehmerSucEquiv ⟩
  LehmerCode (suc n) ■ where
    equivIn : (f : Fin (suc n) ≃ Fin (suc n))
            → FinExcept fzero ≃ FinExcept (equivFun f fzero)
    equivIn f =
      FinExcept fzero
        ≃⟨ Σ-cong-equiv-snd (λ _ → preCompEquiv (invEquiv (congEquiv f))) ⟩
      (Σ[ x ∈ Fin (suc n) ] ¬ ffun fzero ≡ ffun x)
        ≃⟨ Σ-cong-equiv-fst f ⟩
      FinExcept (ffun fzero)
        ■ where ffun = equivFun f

--    equivInChar : ∀ {f} x → fst (equivFun (equivIn f) x) ≡ equivFun f (fst x)
--    equivInChar x = refl

    equivOut : ∀ {k} → FinExcept (fzero {k = n}) ≃ FinExcept k
             → Fin (suc n) ≃ Fin (suc n)
    equivOut {k = k} f =
      Fin (suc n)
        ≃⟨ invEquiv projectionEquiv ⟩
      Unit ⊎ FinExcept fzero
        ≃⟨ isoToEquiv (Sum.⊎Iso idIso (equivToIso f)) ⟩
      Unit ⊎ FinExcept k
        ≃⟨ projectionEquiv ⟩
      Fin (suc n)
        ■

    equivOutChar : ∀ {k} {f} (x : FinExcept fzero) → equivFun (equivOut {k = k} f) (fst x) ≡ fst (equivFun f x)
    equivOutChar {f = f} x with discreteFin fzero (fst x)
    ... | (yes y) = ⊥.rec (x .snd y)
    ... | (no n) = cong (λ x′ → fst (equivFun f x′)) (toℕExc-injective refl)

    i : Iso (Fin (suc n) ≃ Fin (suc n))
            (Σ[ k ∈ Fin (suc n) ] (FinExcept (fzero {k = n}) ≃ FinExcept k))
    Iso.fun i f = equivFun f fzero , equivIn f
    Iso.inv i (k , f) = equivOut f
    Iso.rightInv i (k , f) = ΣPathP (refl , equivEq (funExt λ x →
       toℕExc-injective (cong toℕ (equivOutChar {f = f} x))))
    Iso.leftInv i f = equivEq (funExt goal) where
      goal : ∀ x → equivFun (equivOut (equivIn f)) x ≡ equivFun f x
      goal x = case fsplit x return (λ _ → equivFun (equivOut (equivIn f)) x ≡ equivFun f x) of λ
        { (inl xz) → subst (λ x → equivFun (equivOut (equivIn f)) x ≡ equivFun f x) xz refl
        ; (inr (_ , xn)) → equivOutChar {f = equivIn f} (x , fznotfs ∘ (_∙ sym xn))
        }

    ii : ∀ k → (FinExcept fzero ≃ FinExcept k) ≃ (Fin n ≃ Fin n)
    ii k = (FinExcept fzero ≃ FinExcept k) ≃⟨ cong≃ (λ R → FinExcept fzero ≃ R) punchOutEquiv ⟩
           (FinExcept fzero ≃ Fin n)       ≃⟨ cong≃ (λ L → L ≃ Fin n) punchOutEquiv  ⟩
           (Fin n ≃ Fin n)                 ■

encode : (Fin n ≃ Fin n) → LehmerCode n
encode = equivFun lehmerEquiv

decode : LehmerCode n → Fin n ≃ Fin n
decode = invEq lehmerEquiv

factorial : ℕ → ℕ
factorial zero = 1
factorial (suc n) = suc n · factorial n

lehmerFinEquiv : LehmerCode n ≃ Fin (factorial n)
lehmerFinEquiv {zero} = isContr→Equiv isContrLehmerZero isContrFin1
lehmerFinEquiv {suc n} = _ ≃⟨ invEquiv lehmerSucEquiv ⟩
                         _ ≃⟨ ≃-× (idEquiv _) lehmerFinEquiv ⟩
                         _ ≃⟨ factorEquiv ⟩
                         _ ■

private
  -- this example is copied from wikipedia, using the permutation of the letters A-G
  -- B,F,A,G,D,E,C
  -- given by the corresponding Lehmer code of
  -- 1 4 0 3 1 1 0
  exampleCode : LehmerCode 7
  exampleCode = (1 , (5 , refl)) ∷ (4 , (1 , refl)) ∷ (0 , (4 , refl)) ∷ (3 , (0 , refl)) ∷ (1 , (1 , refl)) ∷ (1 , (0 , refl)) ∷ (0 , (0 , refl)) ∷ []

  example : Fin 7 ≃ Fin 7
  example = decode exampleCode

  -- C should decode to G
  computation : fst (equivFun example (3 , (3 , refl))) ≡ 6
  computation = refl

  _ : toℕ (equivFun lehmerFinEquiv exampleCode) ≡ 4019
  _ = refl

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


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

-- A Logical Relation for Dependent Type Theory Formalized in Agda

module Logrel-MLTT where

-- README
import README

-- Minimal library
import Tools.Empty
import Tools.Unit
import Tools.Nat
import Tools.Sum
import Tools.Product
import Tools.Function
import Tools.Nullary
import Tools.List
import Tools.PropositionalEquality
import Tools.Fin

-- Grammar of the language
import Definition.Untyped
import Definition.Untyped.Properties

-- Typing and conversion rules of language
import Definition.Typed
import Definition.Typed.Properties
import Definition.Typed.Weakening
import Definition.Typed.Reduction
import Definition.Typed.RedSteps
import Definition.Typed.EqualityRelation
import Definition.Typed.EqRelInstance

-- Logical relation
import Definition.LogicalRelation
import Definition.LogicalRelation.ShapeView
import Definition.LogicalRelation.Irrelevance
import Definition.LogicalRelation.Weakening
import Definition.LogicalRelation.Properties
import Definition.LogicalRelation.Application

import Definition.LogicalRelation.Substitution
import Definition.LogicalRelation.Substitution.Properties
import Definition.LogicalRelation.Substitution.Irrelevance
import Definition.LogicalRelation.Substitution.Conversion
import Definition.LogicalRelation.Substitution.Reduction
import Definition.LogicalRelation.Substitution.Reflexivity
import Definition.LogicalRelation.Substitution.Weakening
import Definition.LogicalRelation.Substitution.Reducibility
import Definition.LogicalRelation.Substitution.Escape
import Definition.LogicalRelation.Substitution.MaybeEmbed
import Definition.LogicalRelation.Substitution.Introductions

import Definition.LogicalRelation.Fundamental
import Definition.LogicalRelation.Fundamental.Reducibility

-- Consequences of the logical relation for typing and conversion
import Definition.Typed.Consequences.Canonicity
import Definition.Typed.Consequences.Injectivity
import Definition.Typed.Consequences.Syntactic
import Definition.Typed.Consequences.Inversion
import Definition.Typed.Consequences.Inequality
import Definition.Typed.Consequences.Substitution
import Definition.Typed.Consequences.Equality
import Definition.Typed.Consequences.InverseUniv
import Definition.Typed.Consequences.Reduction
import Definition.Typed.Consequences.NeTypeEq
import Definition.Typed.Consequences.SucCong
import Definition.Typed.Consequences.Consistency

-- Algorithmic equality with lemmas that depend on typing consequences
import Definition.Conversion
import Definition.Conversion.Conversion
import Definition.Conversion.Lift
import Definition.Conversion.Reduction
import Definition.Conversion.Soundness
import Definition.Conversion.Stability
import Definition.Conversion.Symmetry
import Definition.Conversion.Transitivity
import Definition.Conversion.Universe
import Definition.Conversion.Weakening
import Definition.Conversion.Whnf
import Definition.Conversion.Decidable
import Definition.Conversion.EqRelInstance
import Definition.Conversion.FullReduction

-- Consequences of the logical relation for algorithmic equality
import Definition.Conversion.Consequences.Completeness

-- Decidability of conversion
import Definition.Typed.Decidable

ext: agda

max_stars_repo_name: fhlkfy/logrel-mltt

max_issues_repo_name: fhlkfy/logrel-mltt

max_forks_repo_name: fhlkfy/logrel-mltt


text:
module Prelude.Int.Core where

open import Prelude.Unit
open import Prelude.Empty
open import Prelude.Nat
open import Prelude.Number
open import Prelude.Semiring
open import Prelude.Ord

open import Agda.Builtin.Int public

neg : Nat → Int
neg zero    = pos zero
neg (suc n) = negsuc n
{-# INLINE neg #-}

-- Integers are numbers --

instance
  NumInt : Number Int
  Number.Constraint NumInt _ = ⊤
  Number.fromNat    NumInt n = pos n

  NegInt : Negative Int
  Negative.Constraint NegInt _ = ⊤
  Negative.fromNeg    NegInt n = neg n

-- Arithmetic --

_-NZ_ : Nat → Nat → Int
a -NZ b with compare a b
... | less (diff k _)    = negsuc k
... | equal _            = pos (a - b)  -- a - b instead of 0 makes it compile to Integer minus
... | greater (diff k _) = pos (suc k)
{-# INLINE _-NZ_ #-}

_+Z_ : Int → Int → Int
pos    a +Z pos    b = pos (a + b)
pos    a +Z negsuc b = a -NZ suc b
negsuc a +Z pos    b = b -NZ suc a
negsuc a +Z negsuc b = negsuc (suc a + b)
{-# INLINE _+Z_ #-}

{-# DISPLAY _+Z_ a b = a + b #-}

negateInt : Int → Int
negateInt (pos    n) = neg n
negateInt (negsuc n) = pos (suc n)
{-# INLINE negateInt #-}

{-# DISPLAY negateInt a = negate a #-}

_-Z_ : Int → Int → Int
a -Z b = a +Z negateInt b
{-# INLINE _-Z_ #-}

abs : Int → Nat
abs (pos n) = n
abs (negsuc n) = suc n

_*Z_ : Int → Int → Int
pos    a *Z pos    b = pos (a * b)
pos    a *Z negsuc b = neg (a * suc b)
negsuc a *Z pos    b = neg (suc a * b)
negsuc a *Z negsuc b = pos (suc a * suc b)
{-# INLINE _*Z_ #-}

{-# DISPLAY _*Z_ a b = a * b #-}

instance
  SemiringInt : Semiring Int
  Semiring.zro SemiringInt = 0
  Semiring.one SemiringInt = 1
  Semiring._+_ SemiringInt = _+Z_
  Semiring._*_ SemiringInt = _*Z_

  SubInt : Subtractive Int
  Subtractive._-_    SubInt = _-Z_
  Subtractive.negate SubInt = negateInt

NonZeroInt : Int → Set
NonZeroInt (pos zero) = ⊥
NonZeroInt _ = ⊤

infixl 7 quotInt-by remInt-by

syntax quotInt-by b a = a quot b
quotInt-by : (b : Int) {{_ : NonZeroInt b}} → Int → Int
quotInt-by (pos zero) {{}} _
quotInt-by (pos (suc n)) (pos m)    = pos (m div suc n)
quotInt-by (pos (suc n)) (negsuc m) = neg (suc m div suc n)
quotInt-by (negsuc n)    (pos m)    = neg (m div suc n)
quotInt-by (negsuc n)    (negsuc m) = pos (suc m div suc n)
{-# INLINE quotInt-by #-}

syntax remInt-by b a = a rem b
remInt-by : (b : Int) {{_ : NonZeroInt b}} → Int → Int
remInt-by (pos zero) {{}} _
remInt-by (pos (suc n)) (pos m)    = pos (    m mod suc n)
remInt-by (pos (suc n)) (negsuc m) = neg (suc m mod suc n)
remInt-by (negsuc n)    (pos m)    = pos (    m mod suc n)
remInt-by (negsuc n)    (negsuc m) = neg (suc m mod suc n)
{-# INLINE remInt-by #-}

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
open import Oscar.Prelude

module Oscar.Data.Maybe where

data Maybe {a} (A : Ø a) : Ø a where
  ∅ : Maybe A
  ↑_ : A → Maybe A

-- A dependent eliminator.

maybe : ∀ {a b} {A : Set a} {B : Maybe A → Set b} →
        ((x : A) → B (↑ x)) → B ∅ → (x : Maybe A) → B x
maybe j n (↑ x) = j x
maybe j n ∅  = n

-- A non-dependent eliminator.

maybe′ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → B → Maybe A → B
maybe′ = maybe


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
-}

module Dijkstra.EitherD where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Haskell.Prelude

data EitherD (E : Set) : Set → Set₁ where
  -- Primitive combinators
  EitherD-return : ∀ {A} → A → EitherD E A
  EitherD-bind   : ∀ {A B} → EitherD E A → (A → EitherD E B) → EitherD E B
  EitherD-bail   : ∀ {A} → E → EitherD E A
  -- Branching conditionals (used for creating more convenient contracts)
  EitherD-if     : ∀ {A} → Guards (EitherD E A) → EitherD E A
  EitherD-either : ∀ {A B C}
                   → (B → EitherD E A) → (C → EitherD E A) → Either B C → EitherD E A
  EitherD-maybe  : ∀ {A B} → EitherD E B → (A → EitherD E B) → Maybe A → EitherD E B

pattern LeftD  x = EitherD-bail   x
pattern RightD x = EitherD-return x

private
  variable
    E : Set
    A B C : Set

EitherD-run : EitherD E A → Either E A
EitherD-run (EitherD-return x) = Right x
EitherD-run (EitherD-bind m f)
  with EitherD-run m
... | Left x = Left x
... | Right y = EitherD-run (f y)
EitherD-run (EitherD-bail x) = Left x
EitherD-run (EitherD-if (clause (b ≔ c) gs)) =
  if toBool b then EitherD-run c else EitherD-run (EitherD-if gs)
EitherD-run (EitherD-if (otherwise≔ c)) =
  EitherD-run c
EitherD-run (EitherD-either f₁ f₂ (Left x))  = EitherD-run (f₁ x)
EitherD-run (EitherD-either f₁ f₂ (Right y)) = EitherD-run (f₂ y)
EitherD-run (EitherD-maybe n s nothing ) = EitherD-run n
EitherD-run (EitherD-maybe n s (just x)) = EitherD-run (s x)

EitherD-Pre : (E A : Set) → Set₁
EitherD-Pre E A = Set

EitherD-Post : (E A : Set) → Set₁
EitherD-Post E A = Either E A → Set

EitherD-Post-⇒ : ∀ {E} {A} → (P Q : EitherD-Post E A) → Set
EitherD-Post-⇒ P Q = ∀ r → P r → Q r

EitherD-PredTrans : (E A : Set) → Set₁
EitherD-PredTrans E A = EitherD-Post E A → EitherD-Pre E A

EitherD-weakestPre-bindPost : (f : A → EitherD E B) → EitherD-Post E B → EitherD-Post E A

EitherD-weakestPre : (m : EitherD E A) → EitherD-PredTrans E A
EitherD-weakestPre (EitherD-return x) P = P (Right x)
EitherD-weakestPre (EitherD-bind m f) P =
  EitherD-weakestPre m (EitherD-weakestPre-bindPost f P)
EitherD-weakestPre (EitherD-bail x) P = P (Left x)
EitherD-weakestPre (EitherD-if (clause (b ≔ c) gs)) P =
  (toBool b ≡ true → EitherD-weakestPre c P)
  × (toBool b ≡ false → EitherD-weakestPre (EitherD-if gs) P)
EitherD-weakestPre (EitherD-if (otherwise≔ x)) P =
  EitherD-weakestPre x P
EitherD-weakestPre (EitherD-either f₁ f₂ e) P =
  (∀ x → e ≡ Left x → EitherD-weakestPre (f₁ x) P)
  × (∀ y → e ≡ Right y → EitherD-weakestPre (f₂ y) P)
EitherD-weakestPre (EitherD-maybe n s m) P =
  (m ≡ nothing → EitherD-weakestPre n P)
  × (∀ j → m ≡ just j → EitherD-weakestPre (s j) P)

EitherD-weakestPre-bindPost f P (Left x) =
  P (Left x)
EitherD-weakestPre-bindPost f P (Right y) =
  ∀ c → c ≡ y → EitherD-weakestPre (f c) P

EitherD-Contract : (m : EitherD E A) → Set₁
EitherD-Contract{E}{A} m =
  (P : EitherD-Post E A)
  → EitherD-weakestPre m P → P (EitherD-run m)

EitherD-contract : (m : EitherD E A) → EitherD-Contract m
EitherD-contract (EitherD-return x) P wp = wp
EitherD-contract (EitherD-bind m f) P wp
   with EitherD-contract m _ wp
...| wp'
   with EitherD-run m
... | Left x = wp'
... | Right y = EitherD-contract (f y) P (wp' y refl)
EitherD-contract (EitherD-bail x) P wp = wp
EitherD-contract{E}{A} (EitherD-if gs) P wp =
  EitherD-contract-if gs P wp
  where
  EitherD-contract-if : (gs : Guards (EitherD E A)) → EitherD-Contract (EitherD-if gs)
  EitherD-contract-if (clause (b ≔ c) gs) P wp
     with toBool b
  ... | false = EitherD-contract-if gs P (proj₂ wp refl)
  ... | true = EitherD-contract c P (proj₁ wp refl)
  EitherD-contract-if (otherwise≔ x) P wp = EitherD-contract x P wp
EitherD-contract (EitherD-either f₁ f₂ (Left x)) P wp =
  EitherD-contract (f₁ x) P (proj₁ wp x refl)
EitherD-contract (EitherD-either f₁ f₂ (Right y)) P wp =
  EitherD-contract (f₂ y) P (proj₂ wp y refl)
EitherD-contract (EitherD-maybe f₁ f₂ nothing) P wp =
  EitherD-contract f₁ P (proj₁ wp refl)
EitherD-contract (EitherD-maybe f₁ f₂ (just x)) P wp =
  EitherD-contract (f₂ x) P (proj₂ wp x refl)

EitherD-⇒
  : ∀ {E A} {P Q : EitherD-Post E A}
  → ∀ m → EitherD-weakestPre m P
  → (EitherD-Post-⇒ P Q)
  → EitherD-weakestPre m Q
EitherD-⇒ {P = Post₁} {Post₂} (LeftD x )         pre pf = pf (Left x ) pre
EitherD-⇒ {P = Post₁} {Post₂} (RightD x)         pre pf = pf (Right x) pre
EitherD-⇒ {P = Post₁} {Post₂} (EitherD-bind m x) pre pf =
  EitherD-⇒ m pre P⇒Q
  where
    P⇒Q : EitherD-Post-⇒ (EitherD-weakestPre-bindPost x Post₁)
                         (EitherD-weakestPre-bindPost x Post₂)
    P⇒Q (Left  rL) Pr = pf (Left rL) Pr
    P⇒Q (Right rR) Pr .rR refl = EitherD-⇒ (x rR) (Pr rR refl) pf
EitherD-⇒ {Post₁} {Post₂} (EitherD-if (otherwise≔ x)) pre pf = EitherD-⇒ x pre pf
EitherD-⇒ {Post₁} {Post₂} (EitherD-if (clause (x ≔ x₂) x₁)) (pre₁ , pre₂) pf =
    (λ x≡true  → EitherD-⇒ x₂ (pre₁ x≡true) pf)
  , (λ x≡false → EitherD-⇒ (EitherD-if x₁) (pre₂ x≡false) pf)
proj₁ (EitherD-⇒ {Post₁} {Post₂} (EitherD-either x₁ x₂ (Left  x)) (pre₁ , pre₂) pf) .x refl =
       EitherD-⇒ (x₁ x) (pre₁ x refl) pf
proj₂ (EitherD-⇒ {Post₁} {Post₂} (EitherD-either x₁ x₂ (Right x)) (pre₁ , pre₂) pf) .x refl =
       EitherD-⇒ (x₂ x) (pre₂ x refl) pf
proj₁ (EitherD-⇒ {Post₁} {Post₂} (EitherD-maybe m x₁ .nothing) (pre₁ , pre₂) pf) refl   =
       EitherD-⇒ m      (pre₁   refl) pf
proj₂ (EitherD-⇒ {Post₁} {Post₂} (EitherD-maybe m x₁ (just x)) (pre₁ , pre₂) pf) j refl =
       EitherD-⇒ (x₁ j) (pre₂ j refl) pf

EitherD-⇒-bind :
    ∀ {E} {A} {P : EitherD-Post E A}
    → {Q : EitherD-Post E B}
    → {f : A → EitherD E B}
    → ∀ m → EitherD-weakestPre m P
    → EitherD-Post-⇒ P (EitherD-weakestPre-bindPost f Q)
    → EitherD-weakestPre (EitherD-bind m f) Q
EitherD-⇒-bind = EitherD-⇒

EitherD-vacuous : ∀ (m : EitherD E A) → EitherD-weakestPre m (const Unit)
EitherD-vacuous (LeftD x)                        = unit
EitherD-vacuous (RightD x)                       = unit
EitherD-vacuous (EitherD-if (otherwise≔ x))      = EitherD-vacuous x
EitherD-vacuous (EitherD-if (clause (b ≔ x) x₁)) = (const (EitherD-vacuous x)) , (const (EitherD-vacuous (EitherD-if x₁)))
EitherD-vacuous (EitherD-either x₁ x₂ x)         = (λ x₃ _ → EitherD-vacuous (x₁ x₃)) , (λ y _ → EitherD-vacuous (x₂ y))
EitherD-vacuous (EitherD-maybe m x₁ x)           = (const (EitherD-vacuous m)) , λ j _ → EitherD-vacuous (x₁ j)
EitherD-vacuous (EitherD-bind m x)               = EitherD-⇒-bind m (EitherD-vacuous m) λ { (Left  _) _ → unit
                                                                                ; (Right _) _ → λ c _ → EitherD-vacuous (x c) }


text:
module Structure.Category.NaturalTransformation where

open import Functional           using () renaming (id to idᶠⁿ)
open import Functional.Dependent using () renaming (_∘_ to _∘ᶠⁿ_)
import      Lvl
open import Logic
open import Logic.Predicate
open import Structure.Category
open import Structure.Category.Functor
open import Structure.Category.Proofs
open import Structure.Categorical.Properties
open import Structure.Setoid
open import Syntax.Function
open import Type

open Category.ArrowNotation ⦃ … ⦄
open Category ⦃ … ⦄ hiding (identity)
open CategoryObject ⦃ … ⦄
open Functor ⦃ … ⦄

module _
  {ℓₗₒ ℓₗₘ ℓₗₑ ℓᵣₒ ℓᵣₘ ℓᵣₑ}
  {Cₗ : CategoryObject{ℓₗₒ}{ℓₗₘ}{ℓₗₑ}}
  {Cᵣ : CategoryObject{ℓᵣₒ}{ℓᵣₘ}{ℓᵣₑ}}
  where

  private instance _ = Cₗ
  private instance _ = Cᵣ

  module _ (([∃]-intro F₁ ⦃ functor₁ ⦄) ([∃]-intro F₂ ⦃ functor₂ ⦄) : Cₗ →ᶠᵘⁿᶜᵗᵒʳ Cᵣ) where
    -- A natural transformation is a family of morphisms on
    record NaturalTransformation(η : ∀(x) → (F₁(x) ⟶ F₂(x))) : Type{Lvl.of(Type.of(Cₗ)) Lvl.⊔ Lvl.of(Type.of(Cᵣ))} where
      constructor intro
      field natural : ∀{x y}{f : x ⟶ y} → (η(y) ∘ map(f) ≡ map(f) ∘ η(x))

    record NaturalIsomorphism(η : ∀(x) → (F₁(x) ⟶ F₂(x))) : Type{Lvl.of(Type.of(Cₗ)) Lvl.⊔ Lvl.of(Type.of(Cᵣ))} where -- TODO: Consider defining this by two natural tranformations instead
      constructor intro
      field
        ⦃ naturalTransformation ⦄ : NaturalTransformation(η)
        ⦃ components-isomorphism ⦄ : ∀{x} → Morphism.Isomorphism{Morphism = Morphism ⦃ Cᵣ ⦄}(_∘_)(id) (η(x))

    _→ᴺᵀ_ = ∃(NaturalTransformation)
    _↔ᴺᵀ_ = ∃(NaturalIsomorphism)

  module _ (F₁ F₂ : Cₗ →ᶠᵘⁿᶜᵗᵒʳ Cᵣ) where
    open NaturalIsomorphism ⦃ … ⦄

    NaturalIsomorphism-inverse : ∀{η} → ⦃ ni : NaturalIsomorphism(F₁)(F₂)(η) ⦄ → NaturalIsomorphism(F₂)(F₁)(x ↦ Morphism.inv(_∘_)(id) (η(x))) -- TODO: Should not be an instance parameter
    NaturalTransformation.natural (NaturalIsomorphism.naturalTransformation NaturalIsomorphism-inverse) {x} {y} {f} = a where
      postulate a : ∀{a} → a -- TODO: Prove, and also move natural isomorphisms to a new file
    NaturalIsomorphism.components-isomorphism (NaturalIsomorphism-inverse {η}) {x} = inverse-isomorphism category (η(x))

  module _ {F₁ F₂ : Cₗ →ᶠᵘⁿᶜᵗᵒʳ Cᵣ} where
    open NaturalIsomorphism ⦃ … ⦄

    invᴺᵀ : (F₁ ↔ᴺᵀ F₂) → (F₂ ↔ᴺᵀ F₁)
    invᴺᵀ ([∃]-intro _) = [∃]-intro _ ⦃ NaturalIsomorphism-inverse 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:
module UniDB.Morph.Pair where

open import UniDB.Spec

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

infixl 5 _⊗_
data Pair (Ξ Ζ : MOR) : MOR where
  _⊗_ : {γ₁ γ₂ γ₃ : Dom} (ξ : Ξ γ₁ γ₂) (ζ : Ζ γ₂ γ₃) →
    Pair Ξ Ζ γ₁ γ₃

instance
  iHCompPair : {Ξ Ζ : MOR} → HComp Ξ Ζ (Pair Ξ Ζ)
  _⊡_ {{iHCompPair}} = _⊗_

module _
  {Ξ : MOR} {{upΞ : Up Ξ}}
  {Ζ : MOR} {{upΖ : Up Ζ}}
  where

  instance
    iUpPair : Up (Pair Ξ Ζ)
    _↑₁ {{iUpPair}} (ξ ⊗ ζ) = ξ ↑₁ ⊗ ζ ↑₁
    _↑_ {{iUpPair}} (ξ ⊗ ζ) δ = (ξ ↑ δ) ⊗ (ζ ↑ δ)
    ↑-zero {{iUpPair}} (ξ ⊗ ζ) rewrite ↑-zero ξ | ↑-zero ζ = refl
    ↑-suc {{iUpPair}} (ξ ⊗ ζ) δ⁺ rewrite ↑-suc ξ δ⁺ | ↑-suc ζ δ⁺ = refl

    iUpHCompPair : UpHComp Ξ Ζ (Pair Ξ Ζ)
    ⊡-↑₁ {{iUpHCompPair}} ξ ζ = refl

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

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
-- Andreas, 2015-11-28  Check that postfix constructors are fine.
-- There was a TODO in Agda.Syntax.Concrete.Operators which claimed
-- there would be an ambiguity between `true` applied to variable `wrap`
-- and (_wrap true), and arity of constructors would have to be checked.
-- Parsing works fine, so I removed this TODO.

data Bool : Set where true false : Bool

record Wrap A : Set where
  constructor _wrap
  field wrapped : A

test : Wrap Bool → Set
test (true wrap) = Bool
test (false wrap) = Bool

test2 : {A : Set} → Wrap A → A
test2 y = let x wrap = y in x


text:
open import Agda.Builtin.Nat

data B {A : Set} : A → Set where
  b : (a : A) → B a

data C {A : Set} : ∀ {a} → B {A} a → Set where
  c : {a : A} → C (b a)

id : ∀ {b} → C b → B 0
id c = {!!}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --includeC=helloworld.c #-}
module Prelude.FFI where

open import Prelude.IO
open import Prelude.String
open import Prelude.Unit

postulate
  helloworld : IO Unit
  test : IO String

{-# COMPILED_EPIC helloworld (u : Unit) -> Unit = foreign Unit "hello_world" () #-}
{-# COMPILED_EPIC test (u : Unit) -> Unit = foreign String "test" () #-}

main : IO Unit
main =
  helloworld ,,
  x <- test ,
  putStrLn x


text:
-- Σ-Terms
module Terms where

open import Data.Vec hiding (_++_)
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.List
open import Data.List.All
open import Data.Fin.Base

open import Size

-- Ranked alphabet: Vector of natural numbers, where vec[i] denotes the arity of symbol i
RankAlph : ℕ → Set
RankAlph n = Vec ℕ n

-- Types
data Type : Set where
  TTerm : ∀ {n} → RankAlph n → Type
  TFun  : Type → Type → Type

-- Type environment
Env : Set
Env = List Type

-- Environment lookup
data _∈`_ : Type → Env → Set where
  here  : ∀ {φ A}    → A ∈` (A ∷ φ)
  there : ∀ {φ A A'} → A ∈` φ → A ∈` (A' ∷ φ)

-- Bind a type n times on top of an environment
bind : Env → (A : Type) → ℕ → Env
bind φ A zero    = φ
bind φ A (suc n) = A ∷ (bind φ A n)

-- Zero & Successor, Variables, prim. recursion on Σ-Nat, Abstraction, Application
data Expr : Env → Type → Set where
  -- Given terms σ₁, ..., σₘ and a term σ with arity α(σ) = m, we get a new term σ(σ₁, ..., σₘ); Special case: m = 0
  Term    : ∀ {φ n vec} {i : Fin n} {m} {eq : Data.Vec.lookup vec i ≡ m} → (∀ (l : Fin m) → Expr φ (TTerm vec)) → Expr φ (TTerm vec)
  -- Recursion on Terms: For every term σ ∈ Σ with arity α(σ) = m, we have an expression of type A in an environment that binds m variables of type A
  --                     Together with an expression of type Σ, by recursion on the correct expression we get an expression of type A
  Term-Rec  : ∀ {φ n vec A} → (∀ {l : Fin n} {m} {eq : (Data.Vec.lookup vec l) ≡ m} → Expr (bind φ A m) A) → Expr φ (TTerm vec) → Expr φ A
  Var    : ∀ {φ A}   → A ∈` φ → Expr φ A
  Abs    : ∀ {φ A B} → Expr (A ∷ φ) B → Expr φ (TFun A B)
  App    : ∀ {φ A B} → Expr φ (TFun A B) → Expr φ A → Expr φ B

----- Big step semantics using Agda semantics -----
-- Data type for terms
data TTerm' {n} : RankAlph n →  Set where
  Term' : ∀ {vec m} {i : Fin n} {eq : (Data.Vec.lookup vec i) ≡ m} → (∀ (l : Fin m) → (TTerm' vec)) → (TTerm' vec)

data TTerm'' {n} (ra : RankAlph n) : {i : Size} → Set where
  mk : ∀ {i} → (symb : Fin n) → Vec (TTerm'' ra {i}) (Data.Vec.lookup ra symb) → TTerm'' ra {↑ i}

-- From data type to expression
conversion : ∀ {φ n} {vec : RankAlph n} → TTerm' vec → Expr φ (TTerm vec)
conversion (Term'{m = zero}{eq = eq} x)   = Term{eq = eq} λ ()
conversion (Term'{m = suc n}{eq = eq} x)  = Term{eq = eq} (λ l → conversion (x l))

-- Value definition
Value : Type → Set
Value (TTerm vec) = TTerm' vec
Value (TFun A B)  = Value A → Value B

-- Lookup in environment of values
access : ∀ {A φ} → A ∈` φ → All Value φ → Value A
access here      (px ∷ p) = px
access (there x) (px ∷ p) = access x p

-- Given a map from Fin (suc m) to anything; we can derive a map from Fin m to anything
-- (make the Urbild smaller)
urbild : ∀ {m} {A : Set} → (Fin (suc m) → A) → (Fin m → A)
urbild l = λ x → l (raise 1 x)

nary : (A : Set) → ℕ → Set
nary A zero = A
nary A (suc n) = A → nary A n

algebra : ∀ {n} → RankAlph n → (A : Set) → Vec Set n
algebra vec A = Data.Vec.map (nary A) vec

term-rec : ∀ {A : Set} {n : ℕ} {vec : RankAlph n} → (alg : Vec Set n) → TTerm' vec → A
term-rec v (Term'{m = zero}   x)  = {!!}
term-rec v (Term'{m = suc m}  x)  = {!!}

-- Evaluation
eval : ∀ {φ A} → Expr φ A → All Value φ → Value A
--
eval (Term{m = zero}{eq = eq} x) ϱ    = Term'{eq = eq} λ ()
eval (Term{m = suc n}{eq = eq} x) ϱ   = Term'{eq = eq} (λ l → eval (x l) ϱ)
eval (Term-Rec σ-exprs eₛ) ϱ          = {!!}
eval (Var x) ϱ                        = access x ϱ
eval (Abs e) ϱ                        = λ x → eval e (x ∷ ϱ)
eval (App e e₁) ϱ                     = (eval e ϱ) (eval e₁ ϱ)
-----

{--
-- eval (Σ-Rec σ-exprs eₛ)  with (eval eₛ ϱ)
-- ... | σ∈Σ⁰ i x    = eval (σ-exprs i x) ϱ
-- ... | σ∈Σᵐ i x x₁ = eval (σ-exprs i x₁) (rec σ-exprs ϱ x)
-- rec  : ∀ {φ A n m} {vec : Vec ℕ n} → (∀ (l : Fin n) → ∀ {m} → (Data.Vec.lookup vec l) ≡ m → Expr (bind φ A m) A) → All Value φ → (∀ (l : Fin m) → (Σ' vec)) → All Value (bind φ A m)
-- rec {m = zero} σ-exprs ϱ terms  = ϱ
-- rec {m = suc m} σ-exprs ϱ terms = eval (Σ-Rec σ-exprs (conversion (terms (fromℕ m)))) ϱ ∷ (rec{m = m} σ-exprs ϱ (urbild terms))

-- Example: ℕ; Σ = {Z⁰, S¹} (where ⁿ defines arity)
Nat : Type
Nat = TTerm (0 ∷ 1 ∷ [])

--- Natural number to expression
ℕtoE : ℕ → Expr [] Nat

--- Cases
plus-exprs : ℕ → (∀ (l : Fin 2) → ∀ {m} → (Data.Vec.lookup (0 ∷ 1 ∷ []) l) ≡ m → Expr (bind [] (Nat) m) Nat)
-- base case for n + zero = n
plus-exprs n zero       {zero}        0≡0  = ℕtoE n
-- suc case, n + (suc m) = suc (n + m); (n + m) recursively calculated and put ontop of the environemnt, hence Var here
-- plus-exprs n (suc zero) {suc zero}    1≡1  = Term{m = 1} (suc zero) (λ l → Var here) refl

_plus_ : ℕ → ℕ → Expr [] (Nat)
n plus m = Term-Rec (plus-exprs n) (ℕtoE m)

-- Example with explanation
--
--}
----- Small step semantics -----
----- Substitution: See SystemT.agda for a more detailed description
insdebr : ∀ {φ φ'} {A B} → B ∈` (φ' ++ φ) → B ∈` (φ' ++ (A ∷ φ))
insdebr {φ' = []} here           = there here
insdebr {φ' = []} (there x)      = there (there x)
insdebr {φ' = y ∷ ys} here      = here
insdebr {φ' = y ∷ ys} (there x) = there (insdebr x)

-- Extract the ℕ m from proof that vector contains it at index l
extr : ∀ {n l m} {vec : RankAlph n} → (Data.Vec.lookup vec l ≡ m) → ℕ
extr {m} refl = m

-- Proof that (A' ∷ ... ∷ A' ∷ (φ' ++ A ∷ φ)) is "equal to itself", Agda cannot see this
-- from the definition of bind
insbind : ∀ (φ' : Env)  (φ : Env)  (A' : Type) (m : ℕ) → bind (φ' ++ φ) A' m ≡  bind φ' A' m ++ φ
insbind [] φ' A' zero          = refl
insbind [] φ' A' (suc m)       = cong (_∷_ A') (insbind [] φ' A' m)
insbind (x ∷ φ) φ' A' zero    = refl
insbind (x ∷ φ) φ' A' (suc m) = cong (_∷_ A') (insbind (x ∷ φ) φ' A' m)

ins : ∀ {φ φ'} {A B} → Expr (φ' ++ φ) B → Expr (φ' ++ A ∷ φ) B
ins (Var x)                             = Var (insdebr x)
ins (Term{m = zero}{eq = eq} x)         = Term{eq = eq} (λ ())
ins (Term{m = suc m}{eq = eq} x)        = Term{eq = eq} λ l → ins (x l)
-- Direct rewriting does not work since arity (m) is not in scope
-- ins {φ} {φ'} {A} {B} (Term-Rec{n = n}{vec = vec}{A = .B} x x₁) rewrite (insbind φ' φ B {!!})
ins {φ} {φ'} {A} {B} (Term-Rec{n = n}{vec = vec}{A = .B} x x₁)
    = Term-Rec (λ {l : Fin n} {m} {eq : Data.Vec.lookup vec l ≡ m} → ϱ{vec = vec} l m eq (x {l} {m} {eq})) (ins x₁)
    where
    ϱ : ∀ {vec} → (l : Fin n) → (m : ℕ) → (Data.Vec.lookup vec l) ≡ m → Expr (bind (φ' ++ φ) B m) B → Expr (bind (φ' ++ (A ∷ φ)) B m) B
    ϱ l m eq ex rewrite (insbind φ' φ B m) | (insbind φ' (A ∷ φ) B m) = ins{φ = φ}{φ' = bind φ' B m}{A = A} ex
ins {φ' = φ'} (Abs{A = A'} x)           = Abs (ins{φ' = A' ∷ φ'}  x)
ins (App x y)                           = App (ins x) (ins y)

varsub : ∀ {φ φ'} {A B} → A ∈` (φ' ++ B ∷ φ) → Expr φ B → Expr (φ' ++ φ) A
varsub {φ' = []} here M           = M
varsub {φ' = []} (there x) M      = Var x
varsub {φ' = z ∷ zs} here M      = Var here
varsub {φ' = z ∷ zs} (there x) M = ins{φ' = []} (varsub x M)

_[[_]] : ∀ {φ φ'} {A B : Type} → Expr (φ' ++ B ∷ φ) A → Expr φ B → Expr (φ' ++ φ) A
Var x [[ M ]]                      = varsub x M
Term{m = zero}{eq = eq} x [[ M ]]  = Term{eq = eq} (λ ())
Term{m = suc m}{eq = eq} x [[ M ]] = Term{eq = eq} λ l → x l [[ M ]]
_[[_]] {φ} {φ'} {A} {B} (Term-Rec{n = n}{vec = vec}{A = A'} trms e) M
  = Term-Rec (λ {l} {m} {eq} → ϱ{vec = vec} l m eq (trms {l} {m} {eq})) (e [[ M ]])
  where
  ϱ : ∀ {vec} → (l : Fin n) → (m : ℕ) → (Data.Vec.lookup vec l) ≡ m → Expr (bind (φ' ++ B ∷ φ) A m) A → Expr (bind (φ' ++ φ) A m) A
  ϱ l m eq expr rewrite (insbind φ' (B ∷ φ) A m) | (insbind φ' φ A m) = _[[_]] {φ} {bind φ' A m} {A} {B} expr M
Abs N [[ M ]]                      = Abs (N [[ M ]])
App N N' [[ M ]]                   = App (N [[ M ]]) (N' [[ M ]])

-- Values
data Value' {φ} : (t : Type) → Expr φ t → Set where
  VTerm : ∀ {n} {vec : Vec ℕ n} {i : Fin n} {m} {eq : Data.Vec.lookup vec i ≡ m}
    → (subt : Fin m → Expr φ (TTerm vec))
    → (∀ {l : Fin m} → Value' (TTerm vec) (subt l))
    → Value' (TTerm vec) (Term {i = i}{m}{eq} subt)
  VFun  : ∀ {A B expr} → Value' (TFun A B) (Abs expr)

---- Functions required for Term-Rec
-- Select term for recursion
termsel : ∀ {φ A n m vec} → (∀ {l : Fin n} {m'} {eq : Data.Vec.lookup vec l ≡ m'} → Expr (bind φ A m') A) → Expr φ (TTerm vec) → Expr (bind φ A m) A
termsel {m = m} {vec = vec} trms (Term{i = i}{m = m'}{eq = eq} x) = {!!}
termsel trms (Term-Rec x trm) = {!!}
termsel trms (Var x)          = {!!}
termsel trms (App trm trm₁)   = {!!}

-- Proof that (bind (A ∷ φ) A m) ≡ (A ∷ bind φ A m)
bindapp : ∀ {φ A m} → bind (A ∷ φ) A m ≡ (A ∷ bind φ A m)
bindapp {m = zero}  = refl
bindapp {A = A} {m = suc m} = cong (_∷_ A) bindapp

-- Looks more complicated than it is:
-- Given a Term-Rec expression - including a map that for each term t' in our ranked alphabet with arity α(t') = m'
-- defines an expression with m' bound variables - and a specific Term t with arity α(t) = m:
-- Recursively, on m from "right-to-left", bind a Term-Rec expression with the same map using the topmost subterm on top of the environment
-- Term-Rec trms σ(t₁, ..., tₘ) →
-- ( ... ((trms(σ) [y₁ ↦ Term-Rec trms t₁]) [y₂ ↦ Term-Rec trms t₂]) ...) [yₘ ↦ Term-Rec trms tₘ]
bindtosubs : ∀ {m n φ A} {vec : RankAlph n} →
  (trms : (∀ {l : Fin n} {m'} {eq : Data.Vec.lookup vec l ≡ m'} → Expr (bind φ A m') A)) →
  (subtrms : (∀ (l : Fin m) → Expr φ (TTerm vec))) →
  Expr (bind φ A m) A →
  Expr φ A
bindtosubs {zero} trms subtrms e  = e
bindtosubs {suc m} {n = n} {φ} {A} {vec = vec} trms subtrms e rewrite sym (bindapp {φ} {A} {m})
                                  = (bindtosubs{m = m}{n = n}{vec = vec} (λ {l} {m'} {eq} → ϱ l m' eq (trms {l} {m'} {eq})) (λ l → ins{φ' = []}{A = A} ((urbild subtrms) l)) e)
                                    [[ Term-Rec (λ {l} {m'} {eq} → trms {l} {m'} {eq}) (subtrms (fromℕ m)) ]]
                                    where -- Adjustement of environment/DeBruijn indices: In the recursion step, we have to adjust the term map (∀ t' with α(t') = m' we get an Expr with m' bound vars)
                                          --                                              by adding another bound variable. If we for example have a "Var here" in σ, this adjustement leads to the correct
                                          --                                              substitution with evaluated σ₁ that has m bound variables.
                                    ϱ : (l : Fin n) → (m' : ℕ) → (Data.Vec.lookup vec l) ≡ m' → Expr (bind φ A m') A → Expr (bind (A ∷ φ) A m') A
                                    ϱ l m' eq ex rewrite (bindapp {φ} {A} {m'}) = ins{φ' = []}{A = A} ex

data _↠_ {φ} : {A : Type} → Expr φ A → Expr φ A → Set where
  -- Basic call-by-value λ-calc. stuff
  -- Application: Elimination & Reduction
  ξ-App1 : ∀ {A B} {L L' : Expr φ (TFun B A)} {M}
           → L ↠ L'
           → App L M ↠ App L' M

  ξ-App2 : ∀ {A B} {M M' : Expr φ A} {L : Expr φ (TFun A B)}
           → Value' (TFun A B) L
           → M ↠ M'
           → App L M ↠ App L M'

  β-App : ∀ {A B M exp}
          → Value' B M
          → App{B = A} (Abs exp) M ↠ (exp [[ M ]])

  -- Term elimination
  ξ-TermRec : ∀ {A} {n} {vec : RankAlph n} {e e'}
               {trms : (∀ {l : Fin n} {m : ℕ} {eq : (Data.Vec.lookup vec l ≡ m)} → Expr (bind φ A m) A)}
              → e ↠ e'
              → Term-Rec{n = n}{vec = vec} (λ {l} {m'} {eq} → trms {l} {m'} {eq}) e ↠ Term-Rec (λ {l} {m'} {eq} → trms {l} {m'} {eq}) e'

{-
  β-TermRec : ∀ {A} {n i} {vec : Vec ℕ n} {e}
               {trms : (∀ {l : Fin n} {m : ℕ} {eq : (Data.Vec.lookup vec i ≡ m)} → Expr (bind φ A m) A)}
             → Value' (TTerm vec) e
             → {!!}
-}

max_stars_repo_name: kcaliban/ldlc

max_issues_repo_name: kcaliban/ldlc

max_forks_repo_name: kcaliban/ldlc


text:
-- Andreas, 2017-08-28, issue #2723, reported by Andrea

{-# OPTIONS --allow-unsolved-metas #-}

-- {-# OPTIONS --warning=error #-}
-- {-# OPTIONS -v tc.cover:30 #-}

record Test : Set1 where
  field
    one two : Set
open Test

foo : Test
foo .one = {!!}
foo = {!!}
foo .two = {!!}

-- WAS: internal error in clause compiler

-- NOW: warning about unreachable clause


text:
module huffman where

open import lib

open import huffman-types public
----------------------------------------------------------------------------------
-- Run-rewriting rules
----------------------------------------------------------------------------------

data gratr2-nt : Set where
  _ws-plus-10 : gratr2-nt
  _ws : gratr2-nt
  _words : gratr2-nt
  _word : gratr2-nt
  _start : gratr2-nt
  _posinfo : gratr2-nt
  _ows-star-11 : gratr2-nt
  _ows : gratr2-nt
  _digit : gratr2-nt
  _codes : gratr2-nt
  _code : gratr2-nt
  _cmd : gratr2-nt
  _character-range-2 : gratr2-nt
  _character-range-1 : gratr2-nt
  _character-bar-7 : gratr2-nt
  _character-bar-6 : gratr2-nt
  _character-bar-5 : gratr2-nt
  _character-bar-4 : gratr2-nt
  _character-bar-3 : gratr2-nt
  _character : gratr2-nt
  _bvlit : gratr2-nt
  _aws-bar-9 : gratr2-nt
  _aws-bar-8 : gratr2-nt
  _aws : gratr2-nt

gratr2-nt-eq : gratr2-nt → gratr2-nt → 𝔹
gratr2-nt-eq  _ws-plus-10 _ws-plus-10 = tt
gratr2-nt-eq  _ws _ws = tt
gratr2-nt-eq  _words _words = tt
gratr2-nt-eq  _word _word = tt
gratr2-nt-eq  _start _start = tt
gratr2-nt-eq  _posinfo _posinfo = tt
gratr2-nt-eq  _ows-star-11 _ows-star-11 = tt
gratr2-nt-eq  _ows _ows = tt
gratr2-nt-eq  _digit _digit = tt
gratr2-nt-eq  _codes _codes = tt
gratr2-nt-eq  _code _code = tt
gratr2-nt-eq  _cmd _cmd = tt
gratr2-nt-eq  _character-range-2 _character-range-2 = tt
gratr2-nt-eq  _character-range-1 _character-range-1 = tt
gratr2-nt-eq  _character-bar-7 _character-bar-7 = tt
gratr2-nt-eq  _character-bar-6 _character-bar-6 = tt
gratr2-nt-eq  _character-bar-5 _character-bar-5 = tt
gratr2-nt-eq  _character-bar-4 _character-bar-4 = tt
gratr2-nt-eq  _character-bar-3 _character-bar-3 = tt
gratr2-nt-eq  _character _character = tt
gratr2-nt-eq  _bvlit _bvlit = tt
gratr2-nt-eq  _aws-bar-9 _aws-bar-9 = tt
gratr2-nt-eq  _aws-bar-8 _aws-bar-8 = tt
gratr2-nt-eq  _aws _aws = tt
gratr2-nt-eq _ _ = ff

open import rtn gratr2-nt

huffman-start : gratr2-nt → 𝕃 gratr2-rule
huffman-start _ws-plus-10 = (just "P71" , nothing , just _ws-plus-10 , inj₁ _aws :: inj₁ _ws-plus-10 :: []) :: (just "P70" , nothing , just _ws-plus-10 , inj₁ _aws :: []) :: []
huffman-start _ws = (just "P72" , nothing , just _ws , inj₁ _ws-plus-10 :: []) :: []
huffman-start _words = (just "WordsStart" , nothing , just _words , inj₁ _word :: []) :: (just "WordsNext" , nothing , just _words , inj₁ _word :: inj₁ _ws :: inj₁ _words :: []) :: []
huffman-start _word = (just "P1" , nothing , just _word , inj₁ _character :: inj₁ _word :: []) :: (just "P0" , nothing , just _word , inj₁ _character :: []) :: []
huffman-start _start = (just "File" , nothing , just _start , inj₁ _ows :: inj₁ _cmd :: inj₁ _ows :: []) :: []
huffman-start _posinfo = (just "Posinfo" , nothing , just _posinfo , []) :: []
huffman-start _ows-star-11 = (just "P74" , nothing , just _ows-star-11 , inj₁ _aws :: inj₁ _ows-star-11 :: []) :: (just "P73" , nothing , just _ows-star-11 , []) :: []
huffman-start _ows = (just "P75" , nothing , just _ows , inj₁ _ows-star-11 :: []) :: []
huffman-start _digit = (just "Zero" , nothing , just _digit , inj₂ '0' :: []) :: (just "One" , nothing , just _digit , inj₂ '1' :: []) :: []
huffman-start _codes = (just "CodesStart" , nothing , just _codes , inj₁ _code :: []) :: (just "CodesNext" , nothing , just _codes , inj₁ _code :: inj₁ _ws :: inj₁ _codes :: []) :: []
huffman-start _code = (just "Code" , nothing , just _code , inj₁ _word :: inj₁ _ws :: inj₂ '<' :: inj₂ '-' :: inj₁ _ws :: inj₁ _bvlit :: []) :: []
huffman-start _cmd = (just "Encode" , nothing , just _cmd , inj₁ _words :: []) :: (just "Decode" , nothing , just _cmd , inj₂ '!' :: inj₁ _ws :: inj₁ _codes :: inj₁ _ws :: inj₁ _bvlit :: []) :: []
huffman-start _character-range-2 = (just "P53" , nothing , just _character-range-2 , inj₂ 'Z' :: []) :: (just "P52" , nothing , just _character-range-2 , inj₂ 'Y' :: []) :: (just "P51" , nothing , just _character-range-2 , inj₂ 'X' :: []) :: (just "P50" , nothing , just _character-range-2 , inj₂ 'W' :: []) :: (just "P49" , nothing , just _character-range-2 , inj₂ 'V' :: []) :: (just "P48" , nothing , just _character-range-2 , inj₂ 'U' :: []) :: (just "P47" , nothing , just _character-range-2 , inj₂ 'T' :: []) :: (just "P46" , nothing , just _character-range-2 , inj₂ 'S' :: []) :: (just "P45" , nothing , just _character-range-2 , inj₂ 'R' :: []) :: (just "P44" , nothing , just _character-range-2 , inj₂ 'Q' :: []) :: (just "P43" , nothing , just _character-range-2 , inj₂ 'P' :: []) :: (just "P42" , nothing , just _character-range-2 , inj₂ 'O' :: []) :: (just "P41" , nothing , just _character-range-2 , inj₂ 'N' :: []) :: (just "P40" , nothing , just _character-range-2 , inj₂ 'M' :: []) :: (just "P39" , nothing , just _character-range-2 , inj₂ 'L' :: []) :: (just "P38" , nothing , just _character-range-2 , inj₂ 'K' :: []) :: (just "P37" , nothing , just _character-range-2 , inj₂ 'J' :: []) :: (just "P36" , nothing , just _character-range-2 , inj₂ 'I' :: []) :: (just "P35" , nothing , just _character-range-2 , inj₂ 'H' :: []) :: (just "P34" , nothing , just _character-range-2 , inj₂ 'G' :: []) :: (just "P33" , nothing , just _character-range-2 , inj₂ 'F' :: []) :: (just "P32" , nothing , just _character-range-2 , inj₂ 'E' :: []) :: (just "P31" , nothing , just _character-range-2 , inj₂ 'D' :: []) :: (just "P30" , nothing , just _character-range-2 , inj₂ 'C' :: []) :: (just "P29" , nothing , just _character-range-2 , inj₂ 'B' :: []) :: (just "P28" , nothing , just _character-range-2 , inj₂ 'A' :: []) :: []
huffman-start _character-range-1 = (just "P9" , nothing , just _character-range-1 , inj₂ 'h' :: []) :: (just "P8" , nothing , just _character-range-1 , inj₂ 'g' :: []) :: (just "P7" , nothing , just _character-range-1 , inj₂ 'f' :: []) :: (just "P6" , nothing , just _character-range-1 , inj₂ 'e' :: []) :: (just "P5" , nothing , just _character-range-1 , inj₂ 'd' :: []) :: (just "P4" , nothing , just _character-range-1 , inj₂ 'c' :: []) :: (just "P3" , nothing , just _character-range-1 , inj₂ 'b' :: []) :: (just "P27" , nothing , just _character-range-1 , inj₂ 'z' :: []) :: (just "P26" , nothing , just _character-range-1 , inj₂ 'y' :: []) :: (just "P25" , nothing , just _character-range-1 , inj₂ 'x' :: []) :: (just "P24" , nothing , just _character-range-1 , inj₂ 'w' :: []) :: (just "P23" , nothing , just _character-range-1 , inj₂ 'v' :: []) :: (just "P22" , nothing , just _character-range-1 , inj₂ 'u' :: []) :: (just "P21" , nothing , just _character-range-1 , inj₂ 't' :: []) :: (just "P20" , nothing , just _character-range-1 , inj₂ 's' :: []) :: (just "P2" , nothing , just _character-range-1 , inj₂ 'a' :: []) :: (just "P19" , nothing , just _character-range-1 , inj₂ 'r' :: []) :: (just "P18" , nothing , just _character-range-1 , inj₂ 'q' :: []) :: (just "P17" , nothing , just _character-range-1 , inj₂ 'p' :: []) :: (just "P16" , nothing , just _character-range-1 , inj₂ 'o' :: []) :: (just "P15" , nothing , just _character-range-1 , inj₂ 'n' :: []) :: (just "P14" , nothing , just _character-range-1 , inj₂ 'm' :: []) :: (just "P13" , nothing , just _character-range-1 , inj₂ 'l' :: []) :: (just "P12" , nothing , just _character-range-1 , inj₂ 'k' :: []) :: (just "P11" , nothing , just _character-range-1 , inj₂ 'j' :: []) :: (just "P10" , nothing , just _character-range-1 , inj₂ 'i' :: []) :: []
huffman-start _character-bar-7 = (just "P63" , nothing , just _character-bar-7 , inj₁ _character-bar-6 :: []) :: (just "P62" , nothing , just _character-bar-7 , inj₁ _character-range-1 :: []) :: []
huffman-start _character-bar-6 = (just "P61" , nothing , just _character-bar-6 , inj₁ _character-bar-5 :: []) :: (just "P60" , nothing , just _character-bar-6 , inj₁ _character-range-2 :: []) :: []
huffman-start _character-bar-5 = (just "P59" , nothing , just _character-bar-5 , inj₁ _character-bar-4 :: []) :: (just "P58" , nothing , just _character-bar-5 , inj₂ '(' :: []) :: []
huffman-start _character-bar-4 = (just "P57" , nothing , just _character-bar-4 , inj₁ _character-bar-3 :: []) :: (just "P56" , nothing , just _character-bar-4 , inj₂ ')' :: []) :: []
huffman-start _character-bar-3 = (just "P55" , nothing , just _character-bar-3 , inj₂ '.' :: []) :: (just "P54" , nothing , just _character-bar-3 , inj₂ ',' :: []) :: []
huffman-start _character = (just "P64" , nothing , just _character , inj₁ _character-bar-7 :: []) :: []
huffman-start _bvlit = (just "BvlitStart" , nothing , just _bvlit , inj₁ _digit :: []) :: (just "BvlitCons" , nothing , just _bvlit , inj₁ _digit :: inj₁ _bvlit :: []) :: []
huffman-start _aws-bar-9 = (just "P68" , nothing , just _aws-bar-9 , inj₁ _aws-bar-8 :: []) :: (just "P67" , nothing , just _aws-bar-9 , inj₂ '\n' :: []) :: []
huffman-start _aws-bar-8 = (just "P66" , nothing , just _aws-bar-8 , inj₂ ' ' :: []) :: (just "P65" , nothing , just _aws-bar-8 , inj₂ '\t' :: []) :: []
huffman-start _aws = (just "P69" , nothing , just _aws , inj₁ _aws-bar-9 :: []) :: []

huffman-return : maybe gratr2-nt → 𝕃 gratr2-rule
huffman-return _ = []

huffman-rtn : gratr2-rtn
huffman-rtn = record { start = _start ; _eq_ = gratr2-nt-eq ; gratr2-start = huffman-start ; gratr2-return = huffman-return }

open import run ptr
open noderiv

------------------------------------------
-- Length-decreasing rules
------------------------------------------

len-dec-rewrite : Run → maybe (Run × ℕ)
len-dec-rewrite {- BvlitCons-} ((Id "BvlitCons") :: (ParseTree (parsed-digit x0)) :: _::_(ParseTree (parsed-bvlit x1)) rest) = just (ParseTree (parsed-bvlit (norm-bvlit (BvlitCons x0 x1))) ::' rest , 3)
len-dec-rewrite {- BvlitStart-} ((Id "BvlitStart") :: _::_(ParseTree (parsed-digit x0)) rest) = just (ParseTree (parsed-bvlit (norm-bvlit (BvlitStart x0))) ::' rest , 2)
len-dec-rewrite {- Code-} ((Id "Code") :: (ParseTree (parsed-word x0)) :: (ParseTree parsed-ws) :: (InputChar '<') :: (InputChar '-') :: (ParseTree parsed-ws) :: _::_(ParseTree (parsed-bvlit x1)) rest) = just (ParseTree (parsed-code (norm-code (Code x0 x1))) ::' rest , 7)
len-dec-rewrite {- CodesNext-} ((Id "CodesNext") :: (ParseTree (parsed-code x0)) :: (ParseTree parsed-ws) :: _::_(ParseTree (parsed-codes x1)) rest) = just (ParseTree (parsed-codes (norm-codes (CodesNext x0 x1))) ::' rest , 4)
len-dec-rewrite {- CodesStart-} ((Id "CodesStart") :: _::_(ParseTree (parsed-code x0)) rest) = just (ParseTree (parsed-codes (norm-codes (CodesStart x0))) ::' rest , 2)
len-dec-rewrite {- Decode-} ((Id "Decode") :: (InputChar '!') :: (ParseTree parsed-ws) :: (ParseTree (parsed-codes x0)) :: (ParseTree parsed-ws) :: _::_(ParseTree (parsed-bvlit x1)) rest) = just (ParseTree (parsed-cmd (norm-cmd (Decode x0 x1))) ::' rest , 6)
len-dec-rewrite {- Encode-} ((Id "Encode") :: _::_(ParseTree (parsed-words x0)) rest) = just (ParseTree (parsed-cmd (norm-cmd (Encode x0))) ::' rest , 2)
len-dec-rewrite {- File-} ((Id "File") :: (ParseTree parsed-ows) :: (ParseTree (parsed-cmd x0)) :: _::_(ParseTree parsed-ows) rest) = just (ParseTree (parsed-start (norm-start (File x0))) ::' rest , 4)
len-dec-rewrite {- One-} ((Id "One") :: _::_(InputChar '1') rest) = just (ParseTree (parsed-digit (norm-digit One)) ::' rest , 2)
len-dec-rewrite {- P0-} ((Id "P0") :: _::_(ParseTree (parsed-character x0)) rest) = just (ParseTree (parsed-word (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P1-} ((Id "P1") :: (ParseTree (parsed-character x0)) :: _::_(ParseTree (parsed-word x1)) rest) = just (ParseTree (parsed-word (string-append 1 x0 x1)) ::' rest , 3)
len-dec-rewrite {- P10-} ((Id "P10") :: _::_(InputChar 'i') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'i'))) ::' rest , 2)
len-dec-rewrite {- P11-} ((Id "P11") :: _::_(InputChar 'j') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'j'))) ::' rest , 2)
len-dec-rewrite {- P12-} ((Id "P12") :: _::_(InputChar 'k') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'k'))) ::' rest , 2)
len-dec-rewrite {- P13-} ((Id "P13") :: _::_(InputChar 'l') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'l'))) ::' rest , 2)
len-dec-rewrite {- P14-} ((Id "P14") :: _::_(InputChar 'm') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'm'))) ::' rest , 2)
len-dec-rewrite {- P15-} ((Id "P15") :: _::_(InputChar 'n') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'n'))) ::' rest , 2)
len-dec-rewrite {- P16-} ((Id "P16") :: _::_(InputChar 'o') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'o'))) ::' rest , 2)
len-dec-rewrite {- P17-} ((Id "P17") :: _::_(InputChar 'p') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'p'))) ::' rest , 2)
len-dec-rewrite {- P18-} ((Id "P18") :: _::_(InputChar 'q') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'q'))) ::' rest , 2)
len-dec-rewrite {- P19-} ((Id "P19") :: _::_(InputChar 'r') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'r'))) ::' rest , 2)
len-dec-rewrite {- P2-} ((Id "P2") :: _::_(InputChar 'a') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'a'))) ::' rest , 2)
len-dec-rewrite {- P20-} ((Id "P20") :: _::_(InputChar 's') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 's'))) ::' rest , 2)
len-dec-rewrite {- P21-} ((Id "P21") :: _::_(InputChar 't') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 't'))) ::' rest , 2)
len-dec-rewrite {- P22-} ((Id "P22") :: _::_(InputChar 'u') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'u'))) ::' rest , 2)
len-dec-rewrite {- P23-} ((Id "P23") :: _::_(InputChar 'v') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'v'))) ::' rest , 2)
len-dec-rewrite {- P24-} ((Id "P24") :: _::_(InputChar 'w') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'w'))) ::' rest , 2)
len-dec-rewrite {- P25-} ((Id "P25") :: _::_(InputChar 'x') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'x'))) ::' rest , 2)
len-dec-rewrite {- P26-} ((Id "P26") :: _::_(InputChar 'y') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'y'))) ::' rest , 2)
len-dec-rewrite {- P27-} ((Id "P27") :: _::_(InputChar 'z') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'z'))) ::' rest , 2)
len-dec-rewrite {- P28-} ((Id "P28") :: _::_(InputChar 'A') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'A'))) ::' rest , 2)
len-dec-rewrite {- P29-} ((Id "P29") :: _::_(InputChar 'B') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'B'))) ::' rest , 2)
len-dec-rewrite {- P3-} ((Id "P3") :: _::_(InputChar 'b') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'b'))) ::' rest , 2)
len-dec-rewrite {- P30-} ((Id "P30") :: _::_(InputChar 'C') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'C'))) ::' rest , 2)
len-dec-rewrite {- P31-} ((Id "P31") :: _::_(InputChar 'D') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'D'))) ::' rest , 2)
len-dec-rewrite {- P32-} ((Id "P32") :: _::_(InputChar 'E') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'E'))) ::' rest , 2)
len-dec-rewrite {- P33-} ((Id "P33") :: _::_(InputChar 'F') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'F'))) ::' rest , 2)
len-dec-rewrite {- P34-} ((Id "P34") :: _::_(InputChar 'G') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'G'))) ::' rest , 2)
len-dec-rewrite {- P35-} ((Id "P35") :: _::_(InputChar 'H') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'H'))) ::' rest , 2)
len-dec-rewrite {- P36-} ((Id "P36") :: _::_(InputChar 'I') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'I'))) ::' rest , 2)
len-dec-rewrite {- P37-} ((Id "P37") :: _::_(InputChar 'J') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'J'))) ::' rest , 2)
len-dec-rewrite {- P38-} ((Id "P38") :: _::_(InputChar 'K') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'K'))) ::' rest , 2)
len-dec-rewrite {- P39-} ((Id "P39") :: _::_(InputChar 'L') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'L'))) ::' rest , 2)
len-dec-rewrite {- P4-} ((Id "P4") :: _::_(InputChar 'c') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'c'))) ::' rest , 2)
len-dec-rewrite {- P40-} ((Id "P40") :: _::_(InputChar 'M') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'M'))) ::' rest , 2)
len-dec-rewrite {- P41-} ((Id "P41") :: _::_(InputChar 'N') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'N'))) ::' rest , 2)
len-dec-rewrite {- P42-} ((Id "P42") :: _::_(InputChar 'O') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'O'))) ::' rest , 2)
len-dec-rewrite {- P43-} ((Id "P43") :: _::_(InputChar 'P') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'P'))) ::' rest , 2)
len-dec-rewrite {- P44-} ((Id "P44") :: _::_(InputChar 'Q') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'Q'))) ::' rest , 2)
len-dec-rewrite {- P45-} ((Id "P45") :: _::_(InputChar 'R') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'R'))) ::' rest , 2)
len-dec-rewrite {- P46-} ((Id "P46") :: _::_(InputChar 'S') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'S'))) ::' rest , 2)
len-dec-rewrite {- P47-} ((Id "P47") :: _::_(InputChar 'T') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'T'))) ::' rest , 2)
len-dec-rewrite {- P48-} ((Id "P48") :: _::_(InputChar 'U') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'U'))) ::' rest , 2)
len-dec-rewrite {- P49-} ((Id "P49") :: _::_(InputChar 'V') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'V'))) ::' rest , 2)
len-dec-rewrite {- P5-} ((Id "P5") :: _::_(InputChar 'd') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'd'))) ::' rest , 2)
len-dec-rewrite {- P50-} ((Id "P50") :: _::_(InputChar 'W') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'W'))) ::' rest , 2)
len-dec-rewrite {- P51-} ((Id "P51") :: _::_(InputChar 'X') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'X'))) ::' rest , 2)
len-dec-rewrite {- P52-} ((Id "P52") :: _::_(InputChar 'Y') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'Y'))) ::' rest , 2)
len-dec-rewrite {- P53-} ((Id "P53") :: _::_(InputChar 'Z') rest) = just (ParseTree (parsed-character-range-2 (string-append 0 (char-to-string 'Z'))) ::' rest , 2)
len-dec-rewrite {- P54-} ((Id "P54") :: _::_(InputChar ',') rest) = just (ParseTree (parsed-character-bar-3 (string-append 0 (char-to-string ','))) ::' rest , 2)
len-dec-rewrite {- P55-} ((Id "P55") :: _::_(InputChar '.') rest) = just (ParseTree (parsed-character-bar-3 (string-append 0 (char-to-string '.'))) ::' rest , 2)
len-dec-rewrite {- P56-} ((Id "P56") :: _::_(InputChar ')') rest) = just (ParseTree (parsed-character-bar-4 (string-append 0 (char-to-string ')'))) ::' rest , 2)
len-dec-rewrite {- P57-} ((Id "P57") :: _::_(ParseTree (parsed-character-bar-3 x0)) rest) = just (ParseTree (parsed-character-bar-4 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P58-} ((Id "P58") :: _::_(InputChar '(') rest) = just (ParseTree (parsed-character-bar-5 (string-append 0 (char-to-string '('))) ::' rest , 2)
len-dec-rewrite {- P59-} ((Id "P59") :: _::_(ParseTree (parsed-character-bar-4 x0)) rest) = just (ParseTree (parsed-character-bar-5 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P6-} ((Id "P6") :: _::_(InputChar 'e') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'e'))) ::' rest , 2)
len-dec-rewrite {- P60-} ((Id "P60") :: _::_(ParseTree (parsed-character-range-2 x0)) rest) = just (ParseTree (parsed-character-bar-6 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P61-} ((Id "P61") :: _::_(ParseTree (parsed-character-bar-5 x0)) rest) = just (ParseTree (parsed-character-bar-6 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P62-} ((Id "P62") :: _::_(ParseTree (parsed-character-range-1 x0)) rest) = just (ParseTree (parsed-character-bar-7 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P63-} ((Id "P63") :: _::_(ParseTree (parsed-character-bar-6 x0)) rest) = just (ParseTree (parsed-character-bar-7 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P64-} ((Id "P64") :: _::_(ParseTree (parsed-character-bar-7 x0)) rest) = just (ParseTree (parsed-character (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P65-} ((Id "P65") :: _::_(InputChar '\t') rest) = just (ParseTree parsed-aws-bar-8 ::' rest , 2)
len-dec-rewrite {- P66-} ((Id "P66") :: _::_(InputChar ' ') rest) = just (ParseTree parsed-aws-bar-8 ::' rest , 2)
len-dec-rewrite {- P67-} ((Id "P67") :: _::_(InputChar '\n') rest) = just (ParseTree parsed-aws-bar-9 ::' rest , 2)
len-dec-rewrite {- P68-} ((Id "P68") :: _::_(ParseTree parsed-aws-bar-8) rest) = just (ParseTree parsed-aws-bar-9 ::' rest , 2)
len-dec-rewrite {- P69-} ((Id "P69") :: _::_(ParseTree parsed-aws-bar-9) rest) = just (ParseTree parsed-aws ::' rest , 2)
len-dec-rewrite {- P7-} ((Id "P7") :: _::_(InputChar 'f') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'f'))) ::' rest , 2)
len-dec-rewrite {- P70-} ((Id "P70") :: _::_(ParseTree parsed-aws) rest) = just (ParseTree parsed-ws-plus-10 ::' rest , 2)
len-dec-rewrite {- P71-} ((Id "P71") :: (ParseTree parsed-aws) :: _::_(ParseTree parsed-ws-plus-10) rest) = just (ParseTree parsed-ws-plus-10 ::' rest , 3)
len-dec-rewrite {- P72-} ((Id "P72") :: _::_(ParseTree parsed-ws-plus-10) rest) = just (ParseTree parsed-ws ::' rest , 2)
len-dec-rewrite {- P74-} ((Id "P74") :: (ParseTree parsed-aws) :: _::_(ParseTree parsed-ows-star-11) rest) = just (ParseTree parsed-ows-star-11 ::' rest , 3)
len-dec-rewrite {- P75-} ((Id "P75") :: _::_(ParseTree parsed-ows-star-11) rest) = just (ParseTree parsed-ows ::' rest , 2)
len-dec-rewrite {- P8-} ((Id "P8") :: _::_(InputChar 'g') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'g'))) ::' rest , 2)
len-dec-rewrite {- P9-} ((Id "P9") :: _::_(InputChar 'h') rest) = just (ParseTree (parsed-character-range-1 (string-append 0 (char-to-string 'h'))) ::' rest , 2)
len-dec-rewrite {- WordsNext-} ((Id "WordsNext") :: (ParseTree (parsed-word x0)) :: (ParseTree parsed-ws) :: _::_(ParseTree (parsed-words x1)) rest) = just (ParseTree (parsed-words (norm-words (WordsNext x0 x1))) ::' rest , 4)
len-dec-rewrite {- WordsStart-} ((Id "WordsStart") :: _::_(ParseTree (parsed-word x0)) rest) = just (ParseTree (parsed-words (norm-words (WordsStart x0))) ::' rest , 2)
len-dec-rewrite {- Zero-} ((Id "Zero") :: _::_(InputChar '0') rest) = just (ParseTree (parsed-digit (norm-digit Zero)) ::' rest , 2)
len-dec-rewrite {- P73-} (_::_(Id "P73") rest) = just (ParseTree parsed-ows-star-11 ::' rest , 1)
len-dec-rewrite {- Posinfo-} (_::_(Posinfo n) rest) = just (ParseTree (parsed-posinfo (ℕ-to-string n)) ::' rest , 1)
len-dec-rewrite x = nothing

rrs : rewriteRules
rrs = record { len-dec-rewrite = len-dec-rewrite }

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


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

module Data.Binary.Tests.Subtraction where

open import Data.List as List using (List; _∷_; [])
open import Data.Product
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Binary.Definitions
open import Data.Binary.Operations.Semantics as Pos using (⟦_⇓⟧⁺)
open import Relation.Binary.PropositionalEquality
open import Data.Maybe as Maybe using (Maybe; just; nothing)

ℤ : Set
ℤ = Bit × ℕ

⟦_⇓⟧ : 𝔹± → ℤ
⟦ 0< (O , snd) ⇓⟧ = O , ⟦ snd ⇓⟧⁺
⟦ 0< (I , snd) ⇓⟧ = I , ℕ.pred ⟦ snd ⇓⟧⁺
⟦ 0ᵇ ⇓⟧ = O , 0

- : ℕ → ℤ
- zero = O , zero
- (suc snd) = I , snd

+⇑ : ℕ → ℤ
+⇑ = O ,_

⟦_⇑⟧ : ℤ → 𝔹±
⟦ O , snd ⇑⟧ = Maybe.map (O ,_) Pos.⟦ snd ⇑⟧
⟦ I , snd ⇑⟧ = Maybe.map (I ,_) Pos.⟦ suc snd ⇑⟧

-- _≡⌈_⌉≡_ : (𝔹 → 𝔹) → ℕ → (ℕ → ℕ) → Set
-- fᵇ ≡⌈ n ⌉≡ fⁿ = let xs = List.upTo n in List.map (λ x → ⟦ fᵇ ⟦ x ⇑⟧ ⇓⟧ ) xs ≡ List.map fⁿ xs

prod : ∀ {a b} {A : Set a} {B : Set b} → List A → List B → List (A × B)
prod [] ys = []
prod (x ∷ xs) ys = List.foldr (λ y ys → (x , y) ∷ ys) (prod xs ys) ys

_≡⌈_⌉₂≡_ : (𝔹± → 𝔹± → 𝔹±) → ℕ → (ℤ → ℤ → ℤ) → Set
fᵇ ≡⌈ n ⌉₂≡ fⁿ = List.map (λ { (x , y) → ⟦ fᵇ ⟦ x ⇑⟧ ⟦ y ⇑⟧ ⇓⟧ }) zs ≡ List.map (uncurry fⁿ) zs
  where
  xs : List ℕ
  xs = List.upTo n
  ys = List.map (I ,_) xs List.++ List.map (O ,_) xs
  zs = prod ys ys

_ℤ-_ : ℕ → ℕ → ℤ
x ℤ- y with y ℕ.<ᵇ x
(x ℤ- y) | I = O , (x ℕ.∸ suc y)
(x ℤ- y) | O = I , (y ℕ.∸ x)

_z+_ : ℤ → ℤ → ℤ
(O , x) z+ (O , y) = O , (x ℕ.+ y)
(O , x) z+ (I , y) = x ℤ- y
(I , x) z+ (O , y) = y ℤ- x
(I , x) z+ (I , y) = I , (suc x ℕ.+ y)

{-# DISPLAY _,_ I xn = - (suc xn) #-}
{-# DISPLAY _,_ O xn = +⇑ xn #-}

open import Data.Binary.Operations.Subtraction

-- _ : ⟦ ⟦ (- 3) ⇑⟧ + ⟦ +⇑ 2 ⇑⟧ ⇓⟧ ≡ (- 1)
-- _ = refl

-- _ : _+_ ≡⌈ 3 ⌉₂≡ _z+_
-- _ = refl

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
module NoSig where

open import Data.Nat

myFun : ℕ
myFun = (\ x y -> y ) (\ x -> x) 0

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Induction over Subset
------------------------------------------------------------------------

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

module Data.Fin.Subset.Induction where

open import Data.Nat.Base using (ℕ)
open import Data.Nat.Induction using (<-wellFounded)
open import Data.Fin.Subset using (Subset; _⊂_; ∣_∣)
open import Data.Fin.Subset.Properties
open import Induction
open import Induction.WellFounded as WF

------------------------------------------------------------------------
-- Re-export accessability

open WF public using (Acc; acc)

------------------------------------------------------------------------
-- Complete induction based on _⊂_

⊂-Rec : ∀ {n ℓ} → RecStruct (Subset n) ℓ ℓ
⊂-Rec = WfRec _⊂_

⊂-wellFounded : ∀ {n} → WellFounded (_⊂_ {n})
⊂-wellFounded {n} = Subrelation.wellFounded p⊂q⇒∣p∣<∣q∣ (InverseImage.wellFounded ∣_∣ <-wellFounded)


text:
module Data.QuadTree.LensProofs.Valid-LensWrappedTree where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Lens.Lens
open import Data.Logic
open import Data.QuadTree.InternalAgda
open import Agda.Primitive
open import Data.Lens.Proofs.LensLaws
open import Data.Lens.Proofs.LensPostulates
open import Data.Lens.Proofs.LensComposition
open import Data.QuadTree.Implementation.QuadrantLenses
open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.ValidTypes
open import Data.QuadTree.Implementation.SafeFunctions
open import Data.QuadTree.Implementation.PublicFunctions
open import Data.QuadTree.Implementation.DataLenses

---- Lens laws for lensWrappedTree

ValidLens-WrappedTree-ViewSet :
    {t : Set} {{eqT : Eq t}} {dep : Nat}
    -> ViewSet (lensWrappedTree {t} {dep})
ValidLens-WrappedTree-ViewSet (CVQuadrant qdi) (CVQuadTree (Wrapper (w , h) qdo)) = refl

ValidLens-WrappedTree-SetView :
    {t : Set} {{eqT : Eq t}} {dep : Nat}
    -> SetView (lensWrappedTree {t} {dep})
ValidLens-WrappedTree-SetView (CVQuadTree (Wrapper (w , h) qdo)) = refl

ValidLens-WrappedTree-SetSet :
    {t : Set} {{eqT : Eq t}} {dep : Nat}
    -> SetSet (lensWrappedTree {t} {dep})
ValidLens-WrappedTree-SetSet (CVQuadrant qd1) (CVQuadrant qd2) (CVQuadTree (Wrapper (w , h) qdo)) = refl

ValidLens-WrappedTree :
    {t : Set} {{eqT : Eq t}} {dep : Nat}
    -> ValidLens (VQuadTree t {dep}) (VQuadrant t {dep})
ValidLens-WrappedTree = CValidLens lensWrappedTree (ValidLens-WrappedTree-ViewSet) (ValidLens-WrappedTree-SetView) (ValidLens-WrappedTree-SetSet)

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
module LRTree {A : Set} where

open import Data.List

data Tag : Set where
  left : Tag
  right : Tag

data LRTree : Set where
  empty : LRTree
  leaf : A → LRTree
  node : Tag → LRTree → LRTree → LRTree

insert : A → LRTree → LRTree
insert x empty = leaf x
insert x (leaf y) = node left (leaf y) (leaf x)
insert x (node left l r) = node right (insert x l) r
insert x (node right l r) = node left l (insert x r)

flatten : LRTree → List A
flatten empty = []
flatten (leaf x) = x ∷ []
flatten (node _ l r) = flatten l ++ flatten r

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Issue206 where

postulate
  I : Set
  P : I → Set
  i : I
  Q : P i → Set

Foo : (p : P i) → Q p → Set₁
Foo p q with i
Foo p q | i′ = Set

-- Now better error message:
-- Issue206.agda:11,1-19
-- w != i of type I
-- when checking that the type of the generated with function
-- (w : I) (p : P w) (q : Q p) → Set₁ is well-formed

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import LogicalFormulae
open import Groups.Definition
open import Groups.Abelian.Definition
open import Setoids.Setoids
open import Vectors
open import Numbers.Naturals.Semiring
open import Sets.EquivalenceRelations

module Groups.Vector {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where

open Setoid S
open Equivalence eq
open Group G

vecEquiv : {n : ℕ} → Vec A n → Vec A n → Set b
vecEquiv {zero} [] [] = True'
vecEquiv {succ n} (x ,- v1) (y ,- v2) = (x ∼ y) && vecEquiv v1 v2

private
  vecEquivRefl : {n : ℕ} → (x : Vec A n) → vecEquiv x x
  vecEquivRefl [] = record {}
  vecEquivRefl (x ,- xs) = reflexive ,, vecEquivRefl xs

  vecEquivSymm : {n : ℕ} → (x y : Vec A n) → vecEquiv x y → vecEquiv y x
  vecEquivSymm [] [] record {} = record {}
  vecEquivSymm (x ,- xs) (y ,- ys) (fst ,, snd) = symmetric fst ,, vecEquivSymm _ _ snd

  vecEquivTrans : {n : ℕ} → (x y z : Vec A n) → vecEquiv x y → vecEquiv y z → vecEquiv x z
  vecEquivTrans [] [] [] x=y y=z = record {}
  vecEquivTrans (x ,- xs) (y ,- ys) (z ,- zs) (fst1 ,, snd1) (fst2 ,, snd2) = transitive fst1 fst2 ,, vecEquivTrans xs ys zs snd1 snd2

vectorSetoid : (n : ℕ) → Setoid (Vec A n)
Setoid._∼_ (vectorSetoid n) = vecEquiv {n}
Equivalence.reflexive (Setoid.eq (vectorSetoid n)) {x} = vecEquivRefl x
Equivalence.symmetric (Setoid.eq (vectorSetoid n)) {x} {y} = vecEquivSymm x y
Equivalence.transitive (Setoid.eq (vectorSetoid n)) {x} {y} {z} = vecEquivTrans x y z

vectorAdd : {n : ℕ} → Vec A n → Vec A n → Vec A n
vectorAdd [] [] = []
vectorAdd (x ,- v1) (y ,- v2) = (x + y) ,- (vectorAdd v1 v2)

private
  addWellDefined : {n : ℕ} → (m k x y : Vec A n) → Setoid._∼_ (vectorSetoid n) m x → Setoid._∼_ (vectorSetoid n) k y → Setoid._∼_ (vectorSetoid n) (vectorAdd m k) (vectorAdd x y)
  addWellDefined [] [] [] [] m=x k=y = record {}
  addWellDefined (m ,- ms) (k ,- ks) (x ,- xs) (y ,- ys) (m=x ,, ms=xs) (k=y ,, ks=ys) = +WellDefined m=x k=y ,, addWellDefined ms ks xs ys ms=xs ks=ys

  addAssoc : {n : ℕ} → (x y z : Vec A n) → Setoid._∼_ (vectorSetoid n) (vectorAdd x (vectorAdd y z)) (vectorAdd (vectorAdd x y) z)
  addAssoc [] [] [] = record {}
  addAssoc (x ,- xs) (y ,- ys) (z ,- zs) = +Associative ,, addAssoc xs ys zs

  vecIdentRight : {n : ℕ} → (a : Vec A n) → Setoid._∼_ (vectorSetoid n) (vectorAdd a (vecPure 0G)) a
  vecIdentRight [] = record {}
  vecIdentRight (x ,- a) = identRight ,, vecIdentRight a

  vecIdentLeft : {n : ℕ} → (a : Vec A n) → Setoid._∼_ (vectorSetoid n) (vectorAdd (vecPure 0G) a) a
  vecIdentLeft [] = record {}
  vecIdentLeft (x ,- a) = identLeft ,, vecIdentLeft a

  vecInvLeft : {n : ℕ} → (a : Vec A n) → Setoid._∼_ (vectorSetoid n) (vectorAdd (vecMap inverse a) a) (vecPure 0G)
  vecInvLeft [] = record {}
  vecInvLeft (x ,- a) = invLeft ,, vecInvLeft a

  vecInvRight : {n : ℕ} → (a : Vec A n) → Setoid._∼_ (vectorSetoid n) (vectorAdd a (vecMap inverse a)) (vecPure 0G)
  vecInvRight [] = record {}
  vecInvRight (x ,- a) = invRight ,, vecInvRight a

vectorGroup : {n : ℕ} → Group (vectorSetoid n) (vectorAdd {n})
Group.+WellDefined vectorGroup {m} {n} {x} {y} = addWellDefined m n x y
Group.0G vectorGroup = vecPure 0G
Group.inverse vectorGroup x = vecMap inverse x
Group.+Associative vectorGroup {x} {y} {z} = addAssoc x y z
Group.identRight vectorGroup {a} = vecIdentRight a
Group.identLeft vectorGroup {a} = vecIdentLeft a
Group.invLeft vectorGroup {a} = vecInvLeft a
Group.invRight vectorGroup {a} = vecInvRight a

abelianVectorGroup : {n : ℕ} → AbelianGroup G → AbelianGroup (vectorGroup {n})
AbelianGroup.commutative (abelianVectorGroup grp) {[]} {[]} = record {}
AbelianGroup.commutative (abelianVectorGroup grp) {x ,- xs} {y ,- ys} = AbelianGroup.commutative grp ,, AbelianGroup.commutative (abelianVectorGroup grp) {xs} {ys}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Operations on and properties of decidable relations
------------------------------------------------------------------------

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

module Relation.Nullary.Decidable where

open import Data.Bool.Base using (Bool; false; true; not; T)
open import Data.Empty
open import Data.Product hiding (map)
open import Data.Unit
open import Function
open import Function.Equality using (_⟨$⟩_; module Π)
open import Function.Equivalence
  using (_⇔_; equivalence; module Equivalence)
open import Function.Injection using (Injection; module Injection)
open import Level using (Lift)
open import Relation.Binary using (Setoid; module Setoid; Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

⌊_⌋ : ∀ {p} {P : Set p} → Dec P → Bool
⌊ yes _ ⌋ = true
⌊ no  _ ⌋ = false

True : ∀ {p} {P : Set p} → Dec P → Set
True Q = T ⌊ Q ⌋

False : ∀ {p} {P : Set p} → Dec P → Set
False Q = T (not ⌊ Q ⌋)

-- Gives a witness to the "truth".

toWitness : ∀ {p} {P : Set p} {Q : Dec P} → True Q → P
toWitness {Q = yes p} _  = p
toWitness {Q = no  _} ()

-- Establishes a "truth", given a witness.

fromWitness : ∀ {p} {P : Set p} {Q : Dec P} → P → True Q
fromWitness {Q = yes p} = const _
fromWitness {Q = no ¬p} = ¬p

-- Variants for False.

toWitnessFalse : ∀ {p} {P : Set p} {Q : Dec P} → False Q → ¬ P
toWitnessFalse {Q = yes _}  ()
toWitnessFalse {Q = no  ¬p} _  = ¬p

fromWitnessFalse : ∀ {p} {P : Set p} {Q : Dec P} → ¬ P → False Q
fromWitnessFalse {Q = yes p} = flip _$_ p
fromWitnessFalse {Q = no ¬p} = const _

map : ∀ {p q} {P : Set p} {Q : Set q} → P ⇔ Q → Dec P → Dec Q
map P⇔Q (yes p) = yes (Equivalence.to P⇔Q ⟨$⟩ p)
map P⇔Q (no ¬p) = no (¬p ∘ _⟨$⟩_ (Equivalence.from P⇔Q))

map′ : ∀ {p q} {P : Set p} {Q : Set q} →
       (P → Q) → (Q → P) → Dec P → Dec Q
map′ P→Q Q→P = map (equivalence P→Q Q→P)

module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} where

  open Injection
  open Setoid A using () renaming (_≈_ to _≈A_)
  open Setoid B using () renaming (_≈_ to _≈B_)

  -- If there is an injection from one setoid to another, and the
  -- latter's equivalence relation is decidable, then the former's
  -- equivalence relation is also decidable.

  via-injection : Injection A B → Decidable _≈B_ → Decidable _≈A_
  via-injection inj dec x y with dec (to inj ⟨$⟩ x) (to inj ⟨$⟩ y)
  ... | yes injx≈injy = yes (Injection.injective inj injx≈injy)
  ... | no  injx≉injy = no (λ x≈y → injx≉injy (Π.cong (to inj) x≈y))

-- If a decision procedure returns "yes", then we can extract the
-- proof using from-yes.

module _ {p} {P : Set p} where

  From-yes : Dec P → Set p
  From-yes (yes _) = P
  From-yes (no  _) = Lift p ⊤

  from-yes : (p : Dec P) → From-yes p
  from-yes (yes p) = p
  from-yes (no  _) = _

-- If a decision procedure returns "no", then we can extract the proof
-- using from-no.

  From-no : Dec P → Set p
  From-no (no  _) = ¬ P
  From-no (yes _) = Lift p ⊤

  from-no : (p : Dec P) → From-no p
  from-no (no ¬p) = ¬p
  from-no (yes _) = _


text:
module MLib.Prelude.Fin where

open import MLib.Prelude.FromStdlib

open import Data.Fin public
open import Data.Fin.Properties public

open FE using (cong)

import Relation.Binary.Indexed as I

--------------------------------------------------------------------------------
--  Types
--------------------------------------------------------------------------------

-- 'Fin∸ {n} i' is a finite set with "n - i" inhabitants.
Fin∸ : ∀ {n} → Fin n → Set
Fin∸ {n} i = Fin (n Nat.∸ toℕ i)

--------------------------------------------------------------------------------
--  Combinators
--------------------------------------------------------------------------------

foldUpto : ∀ {a} {A : Set a} n → A → (Fin n → A → A) → A
foldUpto Nat.zero z f = z
foldUpto (Nat.suc n) z f = f zero (foldUpto n z (f ∘ suc))

foldMap : ∀ {n ℓ} {A : Set ℓ} → A → (A → A → A) → (Fin n → A) → A
foldMap {n} z f g = foldUpto n z (f ∘ g)

inject∸ : ∀ {n} (i : Fin n) → Fin∸ i → Fin n
inject∸ zero j = j
inject∸ (suc i) j = inject₁ (inject∸ i j)

strengthen∸ : ∀ {n} (i : Fin n) → Fin∸ i → Fin n
strengthen∸ zero j = j
strengthen∸ (suc i) j = Fin.suc (strengthen∸ i j)

module _ where
  open import Data.List using (List; []; _∷_; _++_)
  open import Data.Maybe using (Is-just)

  -- Performs a comprehension over the finite set.
  collect : ∀ n {a} {A : Fin n → Set a} (f : ∀ i → Maybe (A i)) → List (∃ A)
  collect n {A = A} f = foldUpto n [] (λ i xs → maybe (λ x → (i , x) ∷ xs) xs (f i))

  collect′ : ∀ n {a} {A : Set a} (f : Fin n → Maybe A) → List A
  collect′ n {A = A} f = foldUpto n [] (λ i xs → maybe (λ x → x List.∷ xs) xs (f i))

--------------------------------------------------------------------------------
--  Theorems
--------------------------------------------------------------------------------

module _ {ℓ p} (setoid : Setoid ℓ p) where
  open Setoid setoid renaming (Carrier to A)

  module _ {x y : A} {_+_ : A → A → A} (z-cong : x ≈ y) (+-cong : ∀ {x y u v} → x ≈ y → u ≈ v → (x + u) ≈ (y + v)) where
    foldMap-cong :
      ∀ {n}
      → (f g : Fin n → A)
      → (∀ i → f i ≈ g i)
      → foldMap {n} x _+_ f ≈ foldMap y _+_ g
    foldMap-cong {Nat.zero} f g p = z-cong
    foldMap-cong {Nat.suc n} f g p = +-cong (p _) (foldMap-cong (f ∘ suc) (g ∘ suc) (p ∘ suc))

≠-inject : ∀ n (x : Fin n) → ¬ fromℕ n ≡ inject₁ x
≠-inject .(Nat.suc _) zero ()
≠-inject .(Nat.suc _) (suc x) = ≠-inject _ x ∘ suc-injective

suc≠inject : ∀ {n} (i : Fin n) → ¬ (suc i ≡ inject₁ i)
suc≠inject zero ()
suc≠inject (suc i) p = suc≠inject i (suc-injective p)

toℕ≤n : ∀ {n} (i : Fin n) → toℕ i Nat.≤ n
toℕ≤n zero = Nat.z≤n
toℕ≤n (suc i) = Nat.s≤s (toℕ≤n i)

inject-refute : ∀ n {i : Fin (Nat.suc n)} x → i ≡ fromℕ n → ¬ i ≡ inject₁ x
inject-refute _ {zero} zero ()
inject-refute _ {zero} (suc x) ()
inject-refute Nat.zero {suc i} _()
inject-refute (Nat.suc n) {suc i} (zero) p ()
inject-refute (Nat.suc n) {suc i} (suc x) p q = inject-refute _ _ (suc-injective p) (suc-injective q)

inject-< : ∀ {n} (i : Fin n) (j : Fin′ i) → inject j < i
inject-< zero ()
inject-< (suc i) zero = Nat.s≤s Nat.z≤n
inject-< (suc i) (suc j) = Nat.s≤s (inject-< i j)

data Compareℕ {m} : (i : Fin m) (n : ℕ) → Set where
  less : ∀ bound (least : Fin′ bound) {greatest} → Compareℕ (inject! least) greatest
  equal : ∀ i → Compareℕ i (toℕ i)
  greater : ∀ greatest (least : Fin′ greatest) → Compareℕ greatest (toℕ least)

compareℕ : ∀ {m} (i : Fin m) (n : ℕ) → Compareℕ i n
compareℕ zero Nat.zero = equal _
compareℕ zero (Nat.suc n) = less (suc zero) zero
compareℕ (suc i) Nat.zero = greater (suc i) zero
compareℕ (suc i) (Nat.suc n) with compareℕ i n
compareℕ (suc .(inject! least)) (Nat.suc n) | less bound least = less (suc bound) (suc least)
compareℕ (suc i) (Nat.suc .(toℕ i)) | equal .i = equal (suc i)
compareℕ (suc i) (Nat.suc .(toℕ least)) | greater .i least = greater (suc i) (suc least)

reduce+ : ∀ m {n} (i : Fin (m Nat.+ n)) → (∃ λ (j : Fin m) → inject+ n j ≡ i) ⊎ ∃ λ j → raise m j ≡ i
reduce+ Nat.zero i = inj₂ (i , ≡.refl)
reduce+ (Nat.suc m) zero = inj₁ (zero , ≡.refl)
reduce+ (Nat.suc m) (suc i) with reduce+ m i
reduce+ (Nat.suc m) (suc i) | inj₁ (j , p) = inj₁ (suc j , ≡.cong suc p)
reduce+ (Nat.suc m) (suc i) | inj₂ (j , p) = inj₂ (j , ≡.cong suc p)

inject+-injective : ∀ {n m} {i j : Fin m} → inject+ n i ≡ inject+ n j → i ≡ j
inject+-injective {i = zero} {zero} p = ≡.refl
inject+-injective {i = zero} {suc j} ()
inject+-injective {i = suc i} {zero} ()
inject+-injective {n} {i = suc i} {suc j} p = ≡.cong suc (inject+-injective {n} (suc-injective p))

raise≢ : ∀ m n {i : Fin m} {j : Fin n} → ¬ raise n i ≡ inject+ m j
raise≢ _ _ {j = zero} ()
raise≢ _ _ {j = suc _} p = ⊥-elim (raise≢ _ _ (suc-injective p))

raise-injective : ∀ {m} n {i j : Fin m} → raise n i ≡ raise n j → i ≡ j
raise-injective Nat.zero {i} {j} p = p
raise-injective (Nat.suc n) {i} {j} p = raise-injective n (suc-injective p)

toℕ-injective′ : ∀ {m n} {i : Fin m} {j : Fin n} → toℕ i ≡ toℕ j → m ≡ n → i ≅ j
toℕ-injective′ {i = i} {j} p ≡.refl = ≅.≡-to-≅ (toℕ-injective p)

toℕ-injective₂ : ∀ {m} {f : Fin m → ℕ} {i i′ : Fin m} {j : Fin (f i)} {j′ : Fin (f i′)} → (toℕ i , toℕ j) ≡ (toℕ i′ , toℕ j′) → _≡_ {A = Σ (Fin m) (Fin ∘ f)} (i , j) (i′ , j′)
toℕ-injective₂ {f = f} p =
  let q , r = Σ.≡⇒Pointwise-≡ p
      q′ = toℕ-injective q
  in Σ.Pointwise-≡⇒≡ (q′ , toℕ-injective′ (≅.≅-to-≡ r) (≡.cong f q′))