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

open import Tutorials.Monday-Complete
open import Tutorials.Tuesday
open List using (List; []; _∷_; _++_)
open Vec using (Vec; []; _∷_; _!_)
open Fin using (Fin; zero; suc)
module Tutorials.Wednesday where

-----------
-- Interfaces, isomorphisms
-----------

module Isomorphism where
  -- Why can we import _,_ from both modules without resulting in a nameclash?
  open Simple using (_⊎_; _×_; _,_; inl; inr)
  open Product using (Σ-syntax; Σ-⊎; Σ-×; Π-×; Π-→; _,_)

  infix 2 _≅_
  record _≅_ (A B : Set) : Set where
    constructor Mk≅
    field
      to      : A → B
      from    : B → A
      from∘to : ∀ a → from (to a) ≡ a
      to∘from : ∀ b → to (from b) ≡ b

  open _≅_

  -- We can use copattern matching to construct a record by defining how to construct each of its fields
  Σ-⊎-≅ : Σ-⊎ A B ≅ A ⊎ B
  Σ-⊎-≅ = {!!}

  Σ-×-≅ : Σ-× A B ≅ A × B
  Σ-×-≅ = {!!}

  Π-→-≅ : Π-→ A B ≅ (A → B)
  to Π-→-≅ = {!!}
  from Π-→-≅ = {!!}
  -- Needs η laws for functions (∀ x → f x) ≡ f
  from∘to Π-→-≅ = {!!}
  to∘from Π-→-≅ = {!!}

  -- The following isomorphism needs of function extensionality
  -- Function extensionality claims that if two functions give the same output on the same input, then they are equal
  -- This does not hold internally in Agda and we therefore need to postulate it as an axiom
  postulate
    extensionality : {P : A → Set} {f g : (a : A) → P a} → (∀ x → f x ≡ g x) → f ≡ g

  Π-×-≅ : Π-× A B ≅ A × B
  Π-×-≅ = {!!}

  curry : Π-→ A (Π-→ B C) → Π-→ (Σ-× A B) C
  curry f (a , b) = f a b

  uncurry : Π-→ (Σ-× A B) C → Π-→ A (Π-→ B C)
  uncurry f a b = f (a , b)

  curry-uncurry : Π-→ A (Π-→ B C) ≅ Π-→ (Σ-× A B) C
  curry-uncurry = {!!}

  Fin-≤-≅ : Fin m ≅ Σ[ n ∈ ℕ ] n < m
  Fin-≤-≅ = {!!}

  _iso-∘_ : B ≅ C → A ≅ B → A ≅ C
  x iso-∘ y = {!!}

-----------
-- Decidability
-----------

module Dec where
  open Product using (_×_; _,_; fst; snd)
  open Simple using (¬_)

  data Dec (A : Set) : Set where
    yes :   A → Dec A
    no  : ¬ A → Dec A

  DecEq : Set → Set
  DecEq A = (x y : A) → Dec (x ≡ y)

  map : (A → B) → (¬ A → B) → Dec A → B
  map f g (yes x) = f x
  map f g (no x) = g x

  infix 5 _×-dec_
  _×-dec_ : Dec A → Dec B → Dec (A × B)
  yes x ×-dec yes y = yes (x , y)
  yes x ×-dec no ¬y = no (¬y ∘ snd)
  no ¬x ×-dec B? = no (¬x ∘ fst)

  _ℕ-≟_ : (n m : ℕ) → Dec (n ≡ m)
  n ℕ-≟ m = {!!}

  suc-injective : {i j : Fin n} → _≡_ {A = Fin (suc n)} (suc i) (suc j) → i ≡ j
  suc-injective refl = refl

  _Fin-≟_ : (i j : Fin n) → Dec (i ≡ j)
  zero Fin-≟ zero = yes refl
  zero Fin-≟ suc j = no λ ()
  suc i Fin-≟ zero = no λ ()
  suc i Fin-≟ suc j = map
    (yes ∘ cong suc)
    (no ∘ (λ neq → neq ∘ suc-injective))
    (i Fin-≟ j)

  ∷-injective : {x y : A} {xs ys : List A} → _≡_ {A = List A} (x ∷ xs) (y ∷ ys) → x ≡ y × xs ≡ ys
  ∷-injective refl = refl , refl

  List-≟ : (_A-≟_ : (x y : A) → Dec (x ≡ y)) → (xs ys : List A) → Dec (xs ≡ ys)
  List-≟ _A-≟_ [] [] = yes refl
  List-≟ _A-≟_ [] (y ∷ ys) = no λ ()
  List-≟ _A-≟_ (x ∷ xs) [] = no λ ()
  List-≟ _A-≟_ (x ∷ xs) (y ∷ ys) = map
    (yes ∘ Isomorphism.curry (cong₂ _∷_))
    (no ∘ (λ neq → neq ∘ ∷-injective))
    (x A-≟ y ×-dec List-≟ _A-≟_ xs ys)

-----------
-- Interfaces
-----------

-- We define what it is to be a monoid on a carrier set C
record Monoid (C : Set) : Set where
  constructor MkMonoid
  field
    ε   : C
    _∙_ : C → C → C
    -- Including the algebraic laws
    idˡ : (x : C) → ε ∙ x ≡ x
    idʳ : (x : C) → x ∙ ε ≡ x
    assoc : (x y z : C) → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)

module MonoidSolver (Symbol : Set) (symbol-≟ : Dec.DecEq Symbol) where
  -- The syntax for an expression tree of symbolic monoidal operations
  infixl 20 _‵∙_
  infix 25 ‵_
  data Expr : Set where
    ‵ε   : Expr
    ‵_   : Symbol → Expr
    _‵∙_ : Expr → Expr → Expr

  -- And define equations on monoids
  infix 10 _‵≡_
  record Eqn : Set where
    constructor _‵≡_
    field
      lhs : Expr
      rhs : Expr

  -- The canonical normal form for expression trees
  NormalForm : Set
  NormalForm = List Symbol

  normalise : Expr → NormalForm
  normalise ‵ε = []
  normalise (‵ x) = x ∷ []
  normalise (xs ‵∙ ys) = normalise xs ++ normalise ys

  module Eval (M : Monoid C) where
    open Monoid M

    -- An environment maps symbols to values in the carrier set
    Env : Set
    Env = Symbol → C

    -- Evaluate the syntax in a given environment
    ⟦_⟧ : Expr → Env → C
    ⟦ ‵ε ⟧ Γ = ε
    ⟦ ‵ x ⟧ Γ = Γ x
    ⟦ x ‵∙ y ⟧ Γ = ⟦ x ⟧ Γ ∙ ⟦ y ⟧ Γ

    -- Evaluate the normal form in a given environment
    ⟦_⟧⇓ : NormalForm → Env → C
    ⟦ [] ⟧⇓ Γ = ε
    ⟦ x ∷ xs ⟧⇓ Γ = Γ x ∙ ⟦ xs ⟧⇓ Γ

    -- The evaluation of normal forms distributes over list concatenation
    ++-homo : ∀ Γ (xs ys : NormalForm) → ⟦ xs ++ ys ⟧⇓ Γ ≡ ⟦ xs ⟧⇓ Γ ∙ ⟦ ys ⟧⇓ Γ
    ++-homo Γ [] ys = sym (idˡ _)
    ++-homo Γ (x ∷ xs) ys = begin
      Γ x ∙ ⟦ xs ++ ys ⟧⇓ Γ
        ≡⟨ cong (_ ∙_) (++-homo Γ xs ys) ⟩
      Γ x ∙ (⟦ xs ⟧⇓ Γ ∙ ⟦ ys ⟧⇓ Γ)
        ≡⟨ sym (assoc _ _ _) ⟩
      (Γ x ∙ ⟦ xs ⟧⇓ Γ) ∙ ⟦ ys ⟧⇓ Γ
        ∎

    -- Normalising and then evaluating the normal form is equal to evaluating the original expression
    correct : ∀ Γ (expr : Expr) → ⟦ normalise expr ⟧⇓ Γ ≡ ⟦ expr ⟧ Γ
    correct Γ ‵ε = refl
    correct Γ (‵ x) = idʳ _
    correct Γ (le ‵∙ re) = begin
      ⟦ normalise le      ++  normalise re ⟧⇓ Γ ≡⟨ ++-homo Γ (normalise le) (normalise re) ⟩
      ⟦ normalise le ⟧⇓ Γ ∙ ⟦ normalise re ⟧⇓ Γ ≡⟨ cong₂ _∙_ (correct Γ le) (correct Γ re) ⟩
      ⟦ le ⟧            Γ ∙ ⟦ re ⟧            Γ ∎

    -- We describe what it is to be a solution to an equation
    -- If both sides normalise to the same symbols in the same order,
    -- we claim that the monoid laws make the equations hold in any environment
    Solution : Eqn → Set
    Solution (lhs ‵≡ rhs) =
      Dec.map
        -- Both sides normalise to a common list of symbols, we must now show that the equation holds under any environment
        (λ _ → ∀ (Γ : Env) → ⟦ lhs ⟧ Γ ≡ ⟦ rhs ⟧ Γ)
        -- Both sides do *not* normalise to a common list of symbols, we claim only the trivial
        (λ _ → ⊤)
        (Dec.List-≟ symbol-≟ (normalise lhs) (normalise rhs))

    -- Now that we have described what a solution is, we show that we can provide one
    solve : (eqn : Eqn) → Solution eqn
    -- Pattern matching using with makes the goal type compute
    solve (lhs ‵≡ rhs) with Dec.List-≟ symbol-≟ (normalise lhs) (normalise rhs)
    solve (lhs ‵≡ rhs) | Dec.no _ = tt
    solve (lhs ‵≡ rhs) | Dec.yes lhs⇓≡rhs⇓ = λ Γ → begin
      ⟦ lhs ⟧ Γ            ≡⟨ sym (correct Γ lhs) ⟩
      ⟦ normalise lhs ⟧⇓ Γ ≡⟨ cong (λ ● → ⟦ ● ⟧⇓ Γ) lhs⇓≡rhs⇓ ⟩
      ⟦ normalise rhs ⟧⇓ Γ ≡⟨ correct Γ rhs ⟩
      ⟦ rhs ⟧ Γ            ∎

open MonoidSolver

-- An example instance of a monoid: natural numbers with addition
NAT-MONOID : Monoid ℕ
Monoid.ε NAT-MONOID = zero
Monoid._∙_ NAT-MONOID = _+_
Monoid.idˡ NAT-MONOID = +-idˡ
Monoid.idʳ NAT-MONOID = +-idʳ
Monoid.assoc NAT-MONOID = +-assoc

-- An example usage of the monoid solver
-- We first need to "quote" the goal, i.e. describe it in terms of the expression language / syntax
-- NAT-MONOID describes how to interpret the syntax back and evaluate the expression into a value of the carrier set
eqn₁-auto : (x y z : ℕ) → (0 + x) + y + (y + z) ≡ x + (0 + y + 0) + (y + z + 0)
eqn₁-auto x y z =
  let
    ‵x = zero
    ‵y = suc zero
    ‵z = suc (suc zero)
    lhs = (‵ε ‵∙ ‵ ‵x) ‵∙ ‵ ‵y ‵∙ (‵ ‵y ‵∙ ‵ ‵z)
    rhs = ‵ ‵x ‵∙ (‵ε ‵∙ ‵ ‵y ‵∙ ‵ε) ‵∙ (‵ ‵y ‵∙ ‵ ‵z ‵∙ ‵ε)
  in
  Eval.solve (Fin 3) Dec._Fin-≟_ NAT-MONOID (lhs ‵≡ rhs) λ where
    zero → x
    (suc zero) → y
    (suc (suc zero)) → z

max_stars_repo_name: poncev/agda-bcam

max_issues_repo_name: poncev/agda-bcam

max_forks_repo_name: poncev/agda-bcam


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

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

module Data.List.Properties where

open import Algebra
import Algebra.Monoid-solver
open import Category.Monad
open import Data.Bool
open import Data.List as List
open import Data.List.All using (All; []; _∷_)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product as Prod hiding (map)
open import Function
import Algebra.FunctionProperties
import Relation.Binary.EqReasoning as EqR
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; _≗_; refl)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Unary using (Decidable)

private
  open module FP {a} {A : Set a} =
    Algebra.FunctionProperties (_≡_ {A = A})
  open module LMP {ℓ} = RawMonadPlus (List.monadPlus {ℓ = ℓ})
  module LM {a} {A : Set a} = Monoid (List.monoid A)

module List-solver {a} {A : Set a} =
  Algebra.Monoid-solver (monoid A) renaming (id to nil)

∷-injective : ∀ {a} {A : Set a} {x y : A} {xs ys} →
              x ∷ xs ≡ y List.∷ ys → x ≡ y × xs ≡ ys
∷-injective refl = (refl , refl)

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

∷ʳ-injective []          (_ ∷ [])    ()
∷ʳ-injective []          (_ ∷ _ ∷ _) ()
∷ʳ-injective (_ ∷ [])    []          ()
∷ʳ-injective (_ ∷ _ ∷ _) []          ()

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

left-identity-unique : ∀ {a} {A : Set a} {xs} (ys : List A) →
                       xs ≡ ys ++ xs → ys ≡ []
left-identity-unique               []       _  = refl
left-identity-unique {xs = []}     (y ∷ ys) ()
left-identity-unique {xs = x ∷ xs} (y ∷ ys) eq
  with left-identity-unique (ys ++ [ x ]) (begin
         xs                  ≡⟨ proj₂ (∷-injective eq) ⟩
         ys ++ x ∷ xs        ≡⟨ P.sym (LM.assoc ys [ x ] xs) ⟩
         (ys ++ [ x ]) ++ xs ∎)
  where open P.≡-Reasoning
left-identity-unique {xs = x ∷ xs} (y ∷ []   ) eq | ()
left-identity-unique {xs = x ∷ xs} (y ∷ _ ∷ _) eq | ()

-- Map, sum, and append.

map-++-commute : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) xs ys →
                 map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++-commute f []       ys = refl
map-++-commute f (x ∷ xs) ys =
  P.cong (_∷_ (f x)) (map-++-commute f xs ys)

sum-++-commute : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys
sum-++-commute []       ys = refl
sum-++-commute (x ∷ xs) ys = begin
  x + sum (xs ++ ys)
                         ≡⟨ P.cong (_+_ x) (sum-++-commute xs ys) ⟩
  x + (sum xs + sum ys)
                         ≡⟨ P.sym $ +-assoc x _ _ ⟩
  (x + sum xs) + sum ys
                         ∎
  where
  open CommutativeSemiring commutativeSemiring hiding (_+_)
  open P.≡-Reasoning

-- Various properties about folds.

foldr-universal : ∀ {a b} {A : Set a} {B : Set b}
                  (h : List A → B) f e →
                  (h [] ≡ e) →
                  (∀ x xs → h (x ∷ xs) ≡ f x (h xs)) →
                  h ≗ foldr f e
foldr-universal h f e base step []       = base
foldr-universal h f e base step (x ∷ xs) = begin
  h (x ∷ xs)
    ≡⟨ step x xs ⟩
  f x (h xs)
    ≡⟨ P.cong (f x) (foldr-universal h f e base step xs) ⟩
  f x (foldr f e xs)
    ∎
  where open P.≡-Reasoning

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

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

++IsFold : ∀ {a} {A : Set a} (xs ys : List A) →
           xs ++ ys ≡ foldr _∷_ ys xs
++IsFold xs ys =
  begin
    xs ++ ys
  ≡⟨ P.cong (λ xs → xs ++ ys) (idIsFold xs) ⟩
    foldr _∷_ [] xs ++ ys
  ≡⟨ foldr-fusion (λ xs → xs ++ ys) [] (λ _ _ → refl) xs ⟩
    foldr _∷_ ([] ++ ys) xs
  ≡⟨ refl ⟩
    foldr _∷_ ys xs
  ∎
  where open P.≡-Reasoning

mapIsFold : ∀ {a b} {A : Set a} {B : Set b} {f : A → B} →
            map f ≗ foldr (λ x ys → f x ∷ ys) []
mapIsFold {f = f} =
  begin
    map f
  ≈⟨ P.cong (map f) ∘ idIsFold ⟩
    map f ∘ foldr _∷_ []
  ≈⟨ foldr-fusion (map f) [] (λ _ _ → refl) ⟩
    foldr (λ x ys → f x ∷ ys) []
  ∎
  where open EqR (P._→-setoid_ _ _)

concat-map : ∀ {a b} {A : Set a} {B : Set b} {f : A → B} →
             concat ∘ map (map f) ≗ map f ∘ concat
concat-map {b = b} {f = f} =
  begin
    concat ∘ map (map f)
  ≈⟨ P.cong concat ∘ mapIsFold {b = b} ⟩
    concat ∘ foldr (λ xs ys → map f xs ∷ ys) []
  ≈⟨ foldr-fusion {b = b} concat [] (λ _ _ → refl) ⟩
    foldr (λ ys zs → map f ys ++ zs) []
  ≈⟨ P.sym ∘
     foldr-fusion (map f) [] (λ ys zs → map-++-commute f ys zs) ⟩
    map f ∘ concat
  ∎
  where open EqR (P._→-setoid_ _ _)

map-id : ∀ {a} {A : Set a} → map id ≗ id {A = List A}
map-id {A = A} = begin
  map id        ≈⟨ mapIsFold ⟩
  foldr _∷_ []  ≈⟨ P.sym ∘ idIsFold {A = A} ⟩
  id            ∎
  where open EqR (P._→-setoid_ _ _)

map-compose : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
                {g : B → C} {f : A → B} →
              map (g ∘ f) ≗ map g ∘ map f
map-compose {A = A} {B} {g = g} {f} =
  begin
    map (g ∘ f)
  ≈⟨ P.cong (map (g ∘ f)) ∘ idIsFold ⟩
    map (g ∘ f) ∘ foldr _∷_ []
  ≈⟨ foldr-fusion (map (g ∘ f)) [] (λ _ _ → refl) ⟩
    foldr (λ a y → g (f a) ∷ y) []
  ≈⟨ P.sym ∘ foldr-fusion (map g) [] (λ _ _ → refl) ⟩
    map g ∘ foldr (λ a y → f a ∷ y) []
  ≈⟨ P.cong (map g) ∘ P.sym ∘ mapIsFold {A = A} {B = B} ⟩
    map g ∘ map f
  ∎
  where open EqR (P._→-setoid_ _ _)

foldr-cong : ∀ {a b} {A : Set a} {B : Set b}
               {f₁ f₂ : A → B → B} {e₁ e₂ : B} →
             (∀ x y → f₁ x y ≡ f₂ x y) → e₁ ≡ e₂ →
             foldr f₁ e₁ ≗ foldr f₂ e₂
foldr-cong {f₁ = f₁} {f₂} {e} f₁≗₂f₂ refl =
  begin
    foldr f₁ e
  ≈⟨ P.cong (foldr f₁ e) ∘ idIsFold ⟩
    foldr f₁ e ∘ foldr _∷_ []
  ≈⟨ foldr-fusion (foldr f₁ e) [] (λ x xs → f₁≗₂f₂ x (foldr f₁ e xs)) ⟩
    foldr f₂ e
  ∎
  where open EqR (P._→-setoid_ _ _)

map-cong : ∀ {a b} {A : Set a} {B : Set b} {f g : A → B} →
           f ≗ g → map f ≗ map g
map-cong {A = A} {B} {f} {g} f≗g =
  begin
    map f
  ≈⟨ mapIsFold ⟩
    foldr (λ x ys → f x ∷ ys) []
  ≈⟨ foldr-cong (λ x ys → P.cong₂ _∷_ (f≗g x) refl) refl ⟩
    foldr (λ x ys → g x ∷ ys) []
  ≈⟨ P.sym ∘ mapIsFold {A = A} {B = B} ⟩
    map g
  ∎
  where open EqR (P._→-setoid_ _ _)

-- Take, drop, and splitAt.

take++drop : ∀ {a} {A : Set a}
             n (xs : List A) → take n xs ++ drop n xs ≡ xs
take++drop zero    xs       = refl
take++drop (suc n) []       = refl
take++drop (suc n) (x ∷ xs) =
  P.cong (λ xs → x ∷ xs) (take++drop n xs)

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

-- TakeWhile, dropWhile, and span.

takeWhile++dropWhile : ∀ {a} {A : Set a} (p : A → Bool) (xs : List A) →
                       takeWhile p xs ++ dropWhile p xs ≡ xs
takeWhile++dropWhile p []       = refl
takeWhile++dropWhile p (x ∷ xs) with p x
... | true  = P.cong (_∷_ x) (takeWhile++dropWhile p xs)
... | false = refl

span-defn : ∀ {a} {A : Set a} (p : A → Bool) →
            span p ≗ < takeWhile p , dropWhile p >
span-defn p []       = refl
span-defn p (x ∷ xs) with p x
... | true  = P.cong (Prod.map (_∷_ x) id) (span-defn p xs)
... | false = refl

-- Partition, filter.

partition-defn : ∀ {a} {A : Set a} (p : A → Bool) →
                 partition p ≗ < filter p , filter (not ∘ p) >
partition-defn p []       = refl
partition-defn p (x ∷ xs)
 with p x | partition p xs | partition-defn p xs
...  | true  | (ys , zs) | eq = P.cong (Prod.map (_∷_ x) id) eq
...  | false | (ys , zs) | eq = P.cong (Prod.map id (_∷_ x)) eq

filter-filters : ∀ {a p} {A : Set a} →
                 (P : A → Set p) (dec : Decidable P) (xs : List A) →
                 All P (filter (⌊_⌋ ∘ dec) xs)
filter-filters P dec []       = []
filter-filters P dec (x ∷ xs) with dec x
filter-filters P dec (x ∷ xs) | yes px = px ∷ filter-filters P dec xs
filter-filters P dec (x ∷ xs) | no ¬px = filter-filters P dec xs

-- Inits, tails, and scanr.

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

scanl-defn : ∀ {a b} {A : Set a} {B : Set b}
             (f : A → B → A) (e : A) →
             scanl f e ≗ map (foldl f e) ∘ inits
scanl-defn f e []       = refl
scanl-defn f e (x ∷ xs) = P.cong (_∷_ e) (begin
     scanl f (f e x) xs
  ≡⟨ scanl-defn f (f e x) xs ⟩
     map (foldl f (f e x)) (inits xs)
  ≡⟨ refl ⟩
     map (foldl f e ∘ (_∷_ x)) (inits xs)
  ≡⟨ map-compose (inits xs) ⟩
     map (foldl f e) (map (_∷_ x) (inits xs))
  ∎)
  where open P.≡-Reasoning

-- Length.

length-map : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) xs →
             length (map f xs) ≡ length xs
length-map f []       = refl
length-map f (x ∷ xs) = P.cong suc (length-map f xs)

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

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

length-gfilter : ∀ {a b} {A : Set a} {B : Set b} (p : A → Maybe B) xs →
                 length (gfilter p xs) ≤ length xs
length-gfilter p []       = z≤n
length-gfilter p (x ∷ xs) with p x
length-gfilter p (x ∷ xs) | just y  = s≤s (length-gfilter p xs)
length-gfilter p (x ∷ xs) | nothing = ≤-step (length-gfilter p xs)

-- Reverse.

unfold-reverse : ∀ {a} {A : Set a} (x : A) (xs : List A) →
                 reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
unfold-reverse x xs = begin
  foldl (flip _∷_) [ x ] xs  ≡⟨ helper [ x ] xs ⟩
  reverse xs ∷ʳ x            ∎
  where
  open P.≡-Reasoning

  helper : ∀ {a} {A : Set a} (xs ys : List A) →
           foldl (flip _∷_) xs ys ≡ reverse ys ++ xs
  helper xs []       = P.refl
  helper xs (y ∷ ys) = begin
    foldl (flip _∷_) (y ∷ xs) ys  ≡⟨ helper (y ∷ xs) ys ⟩
    reverse ys ++ y ∷ xs          ≡⟨ P.sym $ LM.assoc (reverse ys) _ _ ⟩
    (reverse ys ∷ʳ y) ++ xs       ≡⟨ P.sym $ P.cong (λ zs → zs ++ xs) (unfold-reverse y ys) ⟩
    reverse (y ∷ ys) ++ xs        ∎

reverse-++-commute :
  ∀ {a} {A : Set a} (xs ys : List A) →
  reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++-commute {a} [] ys = begin
  reverse ys                ≡⟨ P.sym $ proj₂ {a = a} {b = a} LM.identity _ ⟩
  reverse ys ++ []          ≡⟨ P.refl ⟩
  reverse ys ++ reverse []  ∎
  where open P.≡-Reasoning
reverse-++-commute (x ∷ xs) ys = begin
  reverse (x ∷ xs ++ ys)               ≡⟨ unfold-reverse x (xs ++ ys) ⟩
  reverse (xs ++ ys) ++ [ x ]          ≡⟨ P.cong (λ zs → zs ++ [ x ]) (reverse-++-commute xs ys) ⟩
  (reverse ys ++ reverse xs) ++ [ x ]  ≡⟨ LM.assoc (reverse ys) _ _ ⟩
  reverse ys ++ (reverse xs ++ [ x ])  ≡⟨ P.sym $ P.cong (λ zs → reverse ys ++ zs) (unfold-reverse x xs) ⟩
  reverse ys ++ reverse (x ∷ xs)       ∎
  where open P.≡-Reasoning

reverse-map-commute :
  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → (xs : List A) →
  map f (reverse xs) ≡ reverse (map f xs)
reverse-map-commute f []       = refl
reverse-map-commute f (x ∷ xs) = begin
  map f (reverse (x ∷ xs))   ≡⟨ P.cong (map f) $ unfold-reverse x xs ⟩
  map f (reverse xs ∷ʳ x)    ≡⟨ map-++-commute f (reverse xs) ([ x ]) ⟩
  map f (reverse xs) ∷ʳ f x  ≡⟨ P.cong (λ y → y ∷ʳ f x) $ reverse-map-commute f xs ⟩
  reverse (map f xs) ∷ʳ f x  ≡⟨ P.sym $ unfold-reverse (f x) (map f xs) ⟩
  reverse (map f (x ∷ xs))   ∎
  where open P.≡-Reasoning

reverse-involutive : ∀ {a} {A : Set a} → Involutive (reverse {A = A})
reverse-involutive [] = refl
reverse-involutive (x ∷ xs) = begin
  reverse (reverse (x ∷ xs))   ≡⟨ P.cong reverse $ unfold-reverse x xs ⟩
  reverse (reverse xs ∷ʳ x)    ≡⟨ reverse-++-commute (reverse xs) ([ x ]) ⟩
  x ∷ reverse (reverse (xs))   ≡⟨ P.cong (λ y → x ∷ y) $ reverse-involutive xs ⟩
  x ∷ xs                       ∎
  where open P.≡-Reasoning

-- The list monad.

module Monad where

  left-zero : ∀ {ℓ} {A B : Set ℓ} (f : A → List B) → (∅ >>= f) ≡ ∅
  left-zero f = refl

  right-zero : ∀ {ℓ} {A B : Set ℓ} (xs : List A) →
               (xs >>= const ∅) ≡ ∅ {A = B}
  right-zero []       = refl
  right-zero (x ∷ xs) = right-zero xs

  private

    not-left-distributive :
      let xs = true ∷ false ∷ []; f = return; g = return in
      (xs >>= λ x → f x ∣ g x) ≢ ((xs >>= f) ∣ (xs >>= g))
    not-left-distributive ()

  right-distributive : ∀ {ℓ} {A B : Set ℓ}
                       (xs ys : List A) (f : A → List B) →
                       (xs ∣ ys >>= f) ≡ ((xs >>= f) ∣ (ys >>= f))
  right-distributive []       ys f = refl
  right-distributive (x ∷ xs) ys f = begin
    f x ∣ (xs ∣ ys >>= f)            ≡⟨ P.cong (_∣_ (f x)) $ right-distributive xs ys f ⟩
    f x ∣ ((xs >>= f) ∣ (ys >>= f))  ≡⟨ P.sym $ LM.assoc (f x) _ _ ⟩
    (f x ∣ (xs >>= f)) ∣ (ys >>= f)  ∎
    where open P.≡-Reasoning

  left-identity : ∀ {ℓ} {A B : Set ℓ} (x : A) (f : A → List B) →
                  (return x >>= f) ≡ f x
  left-identity {ℓ} x f = proj₂ (LM.identity {a = ℓ}) (f x)

  right-identity : ∀ {a} {A : Set a} (xs : List A) →
                   (xs >>= return) ≡ xs
  right-identity []       = refl
  right-identity (x ∷ xs) = P.cong (_∷_ x) (right-identity xs)

  associative : ∀ {ℓ} {A B C : Set ℓ}
                (xs : List A) (f : A → List B) (g : B → List C) →
                (xs >>= λ x → f x >>= g) ≡ (xs >>= f >>= g)
  associative []       f g = refl
  associative (x ∷ xs) f g = begin
    (f x >>= g) ∣ (xs >>= λ x → f x >>= g)  ≡⟨ P.cong (_∣_ (f x >>= g)) $ associative xs f g ⟩
    (f x >>= g) ∣ (xs >>= f >>= g)          ≡⟨ P.sym $ right-distributive (f x) (xs >>= f) g ⟩
    (f x ∣ (xs >>= f) >>= g)                ∎
    where open P.≡-Reasoning

  cong : ∀ {ℓ} {A B : Set ℓ} {xs₁ xs₂} {f₁ f₂ : A → List B} →
         xs₁ ≡ xs₂ → f₁ ≗ f₂ → (xs₁ >>= f₁) ≡ (xs₂ >>= f₂)
  cong {xs₁ = xs} refl f₁≗f₂ = P.cong concat (map-cong f₁≗f₂ xs)

-- The applicative functor derived from the list monad.

-- Note that these proofs (almost) show that RawIMonad.rawIApplicative
-- is correctly defined. The proofs can be reused if proof components
-- are ever added to RawIMonad and RawIApplicative.

module Applicative where

  open P.≡-Reasoning

  private

    -- A variant of flip map.

    pam : ∀ {ℓ} {A B : Set ℓ} → List A → (A → B) → List B
    pam xs f = xs >>= return ∘ f

  -- ∅ is a left zero for _⊛_.

  left-zero : ∀ {ℓ} {A B : Set ℓ} (xs : List A) → ∅ ⊛ xs ≡ ∅ {A = B}
  left-zero xs = begin
    ∅ ⊛ xs          ≡⟨ refl ⟩
    (∅ >>= pam xs)  ≡⟨ Monad.left-zero (pam xs) ⟩
    ∅               ∎

  -- ∅ is a right zero for _⊛_.

  right-zero : ∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) → fs ⊛ ∅ ≡ ∅
  right-zero {ℓ} fs = begin
    fs ⊛ ∅            ≡⟨ refl ⟩
    (fs >>= pam ∅)    ≡⟨ (Monad.cong (refl {x = fs}) λ f →
                          Monad.left-zero (return {ℓ = ℓ} ∘ f)) ⟩
    (fs >>= λ _ → ∅)  ≡⟨ Monad.right-zero fs ⟩
    ∅                 ∎

  -- _⊛_ distributes over _∣_ from the right.

  right-distributive :
    ∀ {ℓ} {A B : Set ℓ} (fs₁ fs₂ : List (A → B)) xs →
    (fs₁ ∣ fs₂) ⊛ xs ≡ (fs₁ ⊛ xs ∣ fs₂ ⊛ xs)
  right-distributive fs₁ fs₂ xs = begin
    (fs₁ ∣ fs₂) ⊛ xs                     ≡⟨ refl ⟩
    (fs₁ ∣ fs₂ >>= pam xs)               ≡⟨ Monad.right-distributive fs₁ fs₂ (pam xs) ⟩
    (fs₁ >>= pam xs) ∣ (fs₂ >>= pam xs)  ≡⟨ refl ⟩
    fs₁ ⊛ xs ∣ fs₂ ⊛ xs                  ∎

  -- _⊛_ does not distribute over _∣_ from the left.

  private

    not-left-distributive :
      let fs = id ∷ id ∷ []; xs₁ = true ∷ []; xs₂ = true ∷ false ∷ [] in
      fs ⊛ (xs₁ ∣ xs₂) ≢ (fs ⊛ xs₁ ∣ fs ⊛ xs₂)
    not-left-distributive ()

  -- Applicative functor laws.

  identity : ∀ {a} {A : Set a} (xs : List A) → return id ⊛ xs ≡ xs
  identity xs = begin
    return id ⊛ xs          ≡⟨ refl ⟩
    (return id >>= pam xs)  ≡⟨ Monad.left-identity id (pam xs) ⟩
    (xs >>= return)         ≡⟨ Monad.right-identity xs ⟩
    xs                      ∎

  private

    pam-lemma : ∀ {ℓ} {A B C : Set ℓ}
                (xs : List A) (f : A → B) (fs : B → List C) →
                (pam xs f >>= fs) ≡ (xs >>= λ x → fs (f x))
    pam-lemma xs f fs = begin
      (pam xs f >>= fs)                   ≡⟨ P.sym $ Monad.associative xs (return ∘ f) fs ⟩
      (xs >>= λ x → return (f x) >>= fs)  ≡⟨ Monad.cong (refl {x = xs}) (λ x → Monad.left-identity (f x) fs) ⟩
      (xs >>= λ x → fs (f x))             ∎

  composition :
    ∀ {ℓ} {A B C : Set ℓ}
    (fs : List (B → C)) (gs : List (A → B)) xs →
    return _∘′_ ⊛ fs ⊛ gs ⊛ xs ≡ fs ⊛ (gs ⊛ xs)
  composition {ℓ} fs gs xs = begin
    return _∘′_ ⊛ fs ⊛ gs ⊛ xs                      ≡⟨ refl ⟩
    (return _∘′_ >>= pam fs >>= pam gs >>= pam xs)  ≡⟨ Monad.cong (Monad.cong (Monad.left-identity _∘′_ (pam fs))
                                                                              (λ f → refl {x = pam gs f}))
                                                                  (λ fg → refl {x = pam xs fg}) ⟩
    (pam fs _∘′_ >>= pam gs >>= pam xs)             ≡⟨ Monad.cong (pam-lemma fs _∘′_ (pam gs)) (λ _ → refl) ⟩
    ((fs >>= λ f → pam gs (_∘′_ f)) >>= pam xs)     ≡⟨ P.sym $ Monad.associative fs (λ f → pam gs (_∘′_ f)) (pam xs) ⟩
    (fs >>= λ f → pam gs (_∘′_ f) >>= pam xs)       ≡⟨ (Monad.cong (refl {x = fs}) λ f →
                                                        pam-lemma gs (_∘′_ f) (pam xs)) ⟩
    (fs >>= λ f → gs >>= λ g → pam xs (f ∘′ g))     ≡⟨ (Monad.cong (refl {x = fs}) λ f →
                                                        Monad.cong (refl {x = gs}) λ g →
                                                        P.sym $ pam-lemma xs g (return ∘ f)) ⟩
    (fs >>= λ f → gs >>= λ g → pam (pam xs g) f)    ≡⟨ (Monad.cong (refl {x = fs}) λ f →
                                                        Monad.associative gs (pam xs) (return ∘ f)) ⟩
    (fs >>= pam (gs >>= pam xs))                    ≡⟨ refl ⟩
    fs ⊛ (gs ⊛ xs)                                  ∎

  homomorphism : ∀ {ℓ} {A B : Set ℓ} (f : A → B) x →
                 return f ⊛ return x ≡ return (f x)
  homomorphism f x = begin
    return f ⊛ return x            ≡⟨ refl ⟩
    (return f >>= pam (return x))  ≡⟨ Monad.left-identity f (pam (return x)) ⟩
    pam (return x) f               ≡⟨ Monad.left-identity x (return ∘ f) ⟩
    return (f x)                   ∎

  interchange : ∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) {x} →
                fs ⊛ return x ≡ return (λ f → f x) ⊛ fs
  interchange fs {x} = begin
    fs ⊛ return x                    ≡⟨ refl ⟩
    (fs >>= pam (return x))          ≡⟨ (Monad.cong (refl {x = fs}) λ f →
                                         Monad.left-identity x (return ∘ f)) ⟩
    (fs >>= λ f → return (f x))      ≡⟨ refl ⟩
    (pam fs (λ f → f x))             ≡⟨ P.sym $ Monad.left-identity (λ f → f x) (pam fs) ⟩
    (return (λ f → f x) >>= pam fs)  ≡⟨ refl ⟩
    return (λ f → f x) ⊛ fs          ∎

ext: agda


text:
module container.m.extensionality where

open import sum
open import equality
open import container.core
open import container.fixpoint
open import container.equality
open import container.m.core

module Extensionality {li la lb}(c : Container li la lb) where
  private
    module C where
      open Definition c public

      fp : Fixpoint c _
      fp = fix M fixpoint

      open Fixpoint fp public
        using (head; tail)

    module S where
      open Equality c C.fp
        using (equality)
      open Equality c C.fp public
        using (substX)
      open Definition equality public

      fp : Fixpoint equality _
      fp = fix M fixpoint

      open Fixpoint fp public
        using (head; tail)

    open C

  -- bisimilarity relation
  _≡M_ : ∀ {i}(u v : M i) → Set _
  u ≡M v = S.M (_ , u , v)

  reflM : ∀ {i}{u : M i} → u ≡M u
  reflM = S.inf refl (λ b → ♯ reflM)

  private
    -- total space of bisimilarity
    E : ∀ i → Set _
    E i = Σ (M i × M i) (uncurry _≡M_)

    f : E →ⁱ F E
    f i ((xs , ys) , bisim)
      = head xs
      , (λ b → (( tail xs b
                , S.substX (S.head bisim) b
                           (tail ys (subst B (S.head bisim) b)))
                , S.tail bisim b))

    π₁ : E →ⁱ M
    π₁ i ((xs , _), _) = xs

    π₁-mor : ∀ {i} (e : E i) → out i (π₁ i e) ≡ imap π₁ i (f i e)
    π₁-mor ((xs , ys) , p) = refl

    π₂ : E →ⁱ M
    π₂ _ ((_ , ys), _) = ys

    π₂-mor : ∀ {i} (e : E i) → out i (π₂ i e) ≡ imap π₂ i (f i e)
    π₂-mor {i} ((xs , ys) , bisim) = lem (S.head bisim) (tail ys)
      where
        lem : {a a' : A i}(p : a ≡ a')
            → (f : (b' : B a') → M (r b'))
            → _≡_ {A = F M i}
              (a' , f)
              (a , λ b → S.substX p b (f (subst B p b)))
        lem refl f = refl

    equal-π : ∀ {i}(e : E i) → π₁ i e ≡ π₂ i e
    equal-π e = unfold-η f π₁ π₁-mor e · sym (unfold-η f π₂ π₂-mor e)

    abstract
      mext₀ : ∀ {i} {xs ys : M i} → xs ≡M ys → xs ≡ ys
      mext₀ p = equal-π (_ , p)

  mext-inv : ∀ {i}{xs ys : M i} → xs ≡ ys → xs ≡M ys
  mext-inv refl = reflM

  mext : ∀ {i} {xs ys : M i} → xs ≡M ys → xs ≡ ys
  mext p = mext₀ p · sym (mext₀ reflM)

  mext-id : ∀ {i}{u : M i} → mext (reflM {u = u}) ≡ refl
  mext-id = left-inverse (mext₀ reflM)

  mext-retraction : ∀ {i}{xs ys : M i}(p : xs ≡ ys)
                  → mext (mext-inv p) ≡ p
  mext-retraction refl = left-inverse (mext₀ reflM)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


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

module fin where

open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ; _+_ )
open import Data.Fin.Properties hiding (≤-trans ;  <-trans ;  ≤-refl  ) renaming ( <-cmp to <-fcmp )
open import Data.Nat
open import Data.Nat.Properties
open import logic
open import nat
open import Relation.Binary.PropositionalEquality

-- toℕ<n
fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
fin<n {_} {zero} = s≤s z≤n
fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})

-- toℕ≤n
fin≤n : {n : ℕ} (f : Fin (suc n)) → toℕ f ≤ n
fin≤n {_} zero = z≤n
fin≤n {suc n} (suc f) = s≤s (fin≤n {n} f)

pred<n : {n : ℕ} {f : Fin (suc n)} → n > 0  → Data.Nat.pred (toℕ f) < n
pred<n {suc n} {zero} (s≤s z≤n) = s≤s z≤n
pred<n {suc n} {suc f} (s≤s z≤n) = fin<n

fin<asa : {n : ℕ} → toℕ (fromℕ< {n} a<sa) ≡ n
fin<asa = toℕ-fromℕ< nat.a<sa

-- fromℕ<-toℕ
toℕ→from : {n : ℕ} {x : Fin (suc n)} → toℕ x ≡ n → fromℕ n ≡ x
toℕ→from {0} {zero} refl = refl
toℕ→from {suc n} {suc x} eq = cong (λ k → suc k ) ( toℕ→from {n} {x} (cong (λ k → Data.Nat.pred k ) eq ))

0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa
0≤fmax  = subst (λ k → 0 ≤ k ) (sym (toℕ-fromℕ< a<sa)) z≤n

0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa
0<fmax = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< a<sa)) (s≤s z≤n)

-- toℕ-injective
i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j
i=j {suc n} zero zero refl = refl
i=j {suc n} (suc i) (suc j) eq = cong ( λ k → suc k ) ( i=j i j (cong ( λ k → Data.Nat.pred k ) eq) )

-- raise 1
fin+1 :  { n : ℕ } → Fin n → Fin (suc n)
fin+1  zero = zero
fin+1  (suc x) = suc (fin+1 x)

open import Data.Nat.Properties as NatP  hiding ( _≟_ )

fin+1≤ : { i n : ℕ } → (a : i < n)  → fin+1 (fromℕ< a) ≡ fromℕ< (<-trans a a<sa)
fin+1≤ {0} {suc i} (s≤s z≤n) = refl
fin+1≤ {suc n} {suc (suc i)} (s≤s (s≤s a)) = cong (λ k → suc k ) ( fin+1≤ {n} {suc i} (s≤s a) )

fin+1-toℕ : { n : ℕ } → { x : Fin n} → toℕ (fin+1 x) ≡ toℕ x
fin+1-toℕ {suc n} {zero} = refl
fin+1-toℕ {suc n} {suc x} = cong (λ k → suc k ) (fin+1-toℕ {n} {x})

open import Relation.Nullary
open import Data.Empty

fin-1 :  { n : ℕ } → (x : Fin (suc n)) → ¬ (x ≡ zero )  → Fin n
fin-1 zero ne = ⊥-elim (ne refl )
fin-1 {n} (suc x) ne = x

fin-1-sx : { n : ℕ } → (x : Fin n) →  fin-1 (suc x) (λ ()) ≡ x
fin-1-sx zero = refl
fin-1-sx (suc x) = refl

fin-1-xs : { n : ℕ } → (x : Fin (suc n)) → (ne : ¬ (x ≡ zero ))  → suc (fin-1 x ne ) ≡ x
fin-1-xs zero ne = ⊥-elim ( ne refl )
fin-1-xs (suc x) ne = refl

-- suc-injective
-- suc-eq : {n : ℕ } {x y : Fin n} → Fin.suc x ≡ Fin.suc y  → x ≡ y
-- suc-eq {n} {x} {y} eq = subst₂ (λ j k → j ≡ k ) {!!} {!!} (cong (λ k → Data.Fin.pred k ) eq )

-- this is refl
lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt)
lemma3 (s≤s lt) = refl

-- fromℕ<-toℕ
lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m )  → toℕ f ≡ n → f ≡ fromℕ< n<m
lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl =  cong suc ( lemma12 {n} {m} n<m f refl  )

open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )

-- <-irrelevant
<-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n
<-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
<-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl  )

lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n
lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl  )

-- fromℕ<-irrelevant
lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
lemma10 {n} refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl  ))

lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl)

-- toℕ-fromℕ<
lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
lemma11 {n} {m} {x} n<m  = begin
              toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
           ≡⟨ toℕ-fromℕ< _ ⟩
              toℕ x
           ∎  where
               open ≡-Reasoning

x<y→fin-1 : {n : ℕ } → { x y : Fin (suc n)} →  toℕ x < toℕ y  → Fin n
x<y→fin-1 {n} {x} {y} lt = fromℕ< (≤-trans lt (fin≤n _ ))

x<y→fin-1-eq : {n : ℕ } → { x y : Fin (suc n)} → (lt : toℕ x < toℕ y ) → toℕ x ≡ toℕ (x<y→fin-1 lt )
x<y→fin-1-eq {n} {x} {y} lt = sym ( begin
           toℕ (fromℕ< (≤-trans lt (fin≤n y)) ) ≡⟨ toℕ-fromℕ< _ ⟩
           toℕ x  ∎  ) where open ≡-Reasoning

f<→< : {n : ℕ } → { x y : Fin n} → x Data.Fin.< y  →  toℕ x < toℕ y
f<→< {_} {zero} {suc y} (s≤s lt) = s≤s z≤n
f<→< {_} {suc x} {suc y} (s≤s lt) = s≤s (f<→< {_} {x} {y} lt)

f≡→≡ : {n : ℕ } → { x y : Fin n} → x ≡ y  →  toℕ x ≡ toℕ y
f≡→≡ refl = refl

open import Data.List
open import Relation.Binary.Definitions

-- fin-count : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → ℕ
-- fin-count q p[ = 0
-- fin-count q (q0 ∷ qs ) with <-fcmp q q0
-- ... | tri-e = suc (fin-count q qs)
-- ... | false = fin-count q qs

-- fin-not-dup-in-list : { n : ℕ}  (qs : List (Fin n) ) → Set
-- fin-not-dup-in-list {n} qs = (q : Fin n) → fin-count q ≤ 1

-- this is far easier
-- fin-not-dup-in-list→len<n : { n : ℕ}  (qs : List (Fin n) ) → ( (q : Fin n) → fin-not-dup-in-list qs q) → length qs ≤ n
-- fin-not-dup-in-list→len<n = ?

fin-phase2 : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → Bool
fin-phase2 q [] = false
fin-phase2 q (x ∷ qs) with <-fcmp q x
... | tri< a ¬b ¬c = fin-phase2 q qs
... | tri≈ ¬a b ¬c = true
... | tri> ¬a ¬b c = fin-phase2 q qs
fin-phase1 : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → Bool
fin-phase1 q [] = false
fin-phase1 q (x ∷ qs) with <-fcmp q x
... | tri< a ¬b ¬c = fin-phase1 q qs
... | tri≈ ¬a b ¬c = fin-phase2 q qs
... | tri> ¬a ¬b c = fin-phase1 q qs

fin-dup-in-list : { n : ℕ}  (q : Fin n) (qs : List (Fin n) ) → Bool
fin-dup-in-list {n} q qs = fin-phase1 q qs

record FDup-in-list (n : ℕ ) (qs : List (Fin n))  : Set where
   field
      dup : Fin n
      is-dup : fin-dup-in-list dup qs ≡ true

list-less : {n : ℕ } → List (Fin (suc n)) → List (Fin n)
list-less [] = []
list-less {n} (i ∷ ls) with <-fcmp (fromℕ< a<sa) i
... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ i < suc k ) (sym fin<asa) (fin≤n _ )))
... | tri≈ ¬a b ¬c = list-less ls
... | tri> ¬a ¬b c = x<y→fin-1 c ∷ list-less ls

fin010 : {n m : ℕ } {x : Fin n} (c : suc (toℕ x) ≤ toℕ (fromℕ< {m} a<sa) ) → toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) ≡ toℕ x
fin010 {_} {_} {x} c = begin
           toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa))))  ≡⟨ toℕ-fromℕ< _ ⟩
           toℕ x  ∎   where open ≡-Reasoning

---
---  if List (Fin n) is longer than n, there is at most one duplication
---
fin-dup-in-list>n : {n : ℕ } → (qs : List (Fin n))  → (len> : length qs > n ) → FDup-in-list n qs
fin-dup-in-list>n {zero} [] ()
fin-dup-in-list>n {zero} (() ∷ qs) lt
fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where
     open import Level using ( Level )
     --  make a dup from one level below
     fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) →  fin-dup-in-list  (fromℕ< a<sa ) qs ≡ false
          → fin-dup-in-list i (list-less qs) ≡ true → FDup-in-list (suc n) qs
     fdup+1 qs i ne p = record { dup = fin+1 i ; is-dup = f1-phase1 qs p (case1 ne) } where
          -- we have two loops on the max element and the current level. The disjuction means the phases may differ.
          f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true
              → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false)
              → fin-phase2 (fin+1 i) qs ≡ true
          f1-phase2 (x ∷ qs) p (case1 q1) with  <-fcmp (fromℕ< a<sa) x
          ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
          f1-phase2 (x ∷ qs) p (case1 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x
          ... | tri< a ¬b ¬c₁ = f1-phase2 qs p (case2 q1)
          ... | tri≈ ¬a₁ b₁ ¬c₁ = refl
          ... | tri> ¬a₁ ¬b c = f1-phase2 qs p (case2 q1)
          -- two fcmp is only different in the size of Fin, but to develop both f1-phase and list-less both fcmps are required
          f1-phase2 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
          ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase2 qs p (case1 q1)
          ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
          ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
          ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
          ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = refl
          ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ ))
          ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
          ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
          ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase2 qs p (case1 q1)
          f1-phase2 (x ∷ qs) p (case2 q1) with  <-fcmp (fromℕ< a<sa) x
          ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
          f1-phase2 (x ∷ qs) p (case2 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x
          ... | tri< a ¬b ¬c₁ = ⊥-elim ( ¬-bool q1 refl )
          ... | tri≈ ¬a₁ b₁ ¬c₁ = refl
          ... | tri> ¬a₁ ¬b c = ⊥-elim ( ¬-bool q1 refl )
          f1-phase2 (x ∷ qs) p (case2 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
          ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase2 qs p (case2 q1)
          ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
          ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
          ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
          ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = refl
          ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ ))
          ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
          ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
          ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ =  f1-phase2 qs p (case2 q1 )
          f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true
              → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false)
              → fin-phase1 (fin+1 i) qs ≡ true
          f1-phase1 (x ∷ qs) p (case1 q1) with  <-fcmp (fromℕ< a<sa) x
          ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
          f1-phase1 (x ∷ qs) p (case1 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x
          ... | tri< a ¬b ¬c₁ = f1-phase1 qs p (case2 q1)
          ... | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (fdup-10 b b₁) where
               fdup-10 : fromℕ< a<sa ≡ x → fin+1 i ≡ x → ⊥
               fdup-10 eq eq1 = nat-≡< (cong toℕ (trans eq1 (sym eq))) (subst₂ (λ j k → j < k ) (sym fin+1-toℕ) (sym fin<asa) fin<n )
          ... | tri> ¬a₁ ¬b c = f1-phase1 qs p (case2 q1)
          f1-phase1 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
          ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case1 q1)
          ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
          ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
          ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
          ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = f1-phase2 qs p (case1 q1)
          ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ ))
          ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
          ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
          ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case1 q1)
          f1-phase1 (x ∷ qs) p (case2 q1) with  <-fcmp (fromℕ< a<sa) x
          ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
          f1-phase1 (x ∷ qs) p (case2 q1) | tri≈ ¬a b ¬c = ⊥-elim ( ¬-bool q1 refl )
          f1-phase1 (x ∷ qs) p (case2 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
          ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case2 q1)
          ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
          ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
          ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
          ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = f1-phase2 qs p (case2 q1)
          ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ ))
          ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
          ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
          ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case2 q1)
     fdup-phase0 : FDup-in-list (suc n) qs
     fdup-phase0 with fin-dup-in-list (fromℕ< a<sa) qs | inspect (fin-dup-in-list (fromℕ< a<sa)) qs
     ... | true  | record { eq = eq } = record { dup = fromℕ< a<sa ; is-dup = eq }
     ... | false | record { eq = ne } = fdup+1 qs (FDup-in-list.dup fdup) ne (FDup-in-list.is-dup fdup)  where
           -- if no dup in the max element, the list without the element is only one length shorter
           fless : (qs : List (Fin (suc n))) → length qs > suc n  → fin-dup-in-list (fromℕ< a<sa) qs ≡ false → n < length (list-less qs)
           fless qs lt p = fl-phase1 n qs lt p where
               fl-phase2 : (n1 : ℕ) (qs : List (Fin (suc n))) → length qs > n1  → fin-phase2 (fromℕ< a<sa) qs ≡ false → n1 < length (list-less qs)
               fl-phase2 zero (x ∷ qs) (s≤s lt) p with  <-fcmp (fromℕ< a<sa) x
               ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
               ... | tri> ¬a ¬b c =  s≤s z≤n
               fl-phase2 (suc n1) (x ∷ qs) (s≤s lt) p with  <-fcmp (fromℕ< a<sa) x
               ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
               ... | tri> ¬a ¬b c = s≤s ( fl-phase2 n1 qs lt p )
               fl-phase1 : (n1 : ℕ) (qs : List (Fin (suc n))) → length qs > suc n1  → fin-phase1 (fromℕ< a<sa) qs ≡ false → n1 < length (list-less qs)
               fl-phase1 zero (x ∷ qs) (s≤s lt) p  with <-fcmp (fromℕ< a<sa) x
               ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
               ... | tri≈ ¬a b ¬c = fl-phase2 0 qs lt p
               ... | tri> ¬a ¬b c = s≤s z≤n
               fl-phase1 (suc n1) (x ∷ qs) (s≤s lt) p with <-fcmp (fromℕ< a<sa) x
               ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
               ... | tri≈ ¬a b ¬c = fl-phase2 (suc n1) qs lt p
               ... | tri> ¬a ¬b c = s≤s ( fl-phase1 n1 qs lt p )
           -- if the list without the max element is only one length shorter, we can recurse
           fdup : FDup-in-list n (list-less qs)
           fdup = fin-dup-in-list>n (list-less qs) (fless qs lt ne)

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
open import Level using (Level; suc; zero; _⊔_)
open import Function using (const)
open import Algebra
open import Algebra.Structures
open import Algebra.OrderedMonoid
open import Algebra.FunctionProperties as FunctionProperties using (Op₁; Op₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Binary
open import Relation.Binary.PartialOrderReasoning as ≤-Reasoning using ()

module Algebra.Pregroup where

-- Definition of the properties of left and right contraction and
-- expansion for usage in the below definition of pregroups.
module AdjointProperties {a ℓ} {A : Set a} (_≤_ : Rel A ℓ) (_∙_ : Op₂ A) (ε : A) where

  LeftContract : Op₁ A → Set _
  LeftContract _ˡ = ∀ x → (x ˡ ∙ x) ≤ ε

  LeftExpand : Op₁ A → Set _
  LeftExpand _ˡ = ∀ x → ε ≤ (x ∙ x ˡ)

  RightContract : Op₁ A → Set _
  RightContract _ʳ = ∀ x → (x ∙ x ʳ) ≤ ε

  RightExpand : Op₁ A → Set _
  RightExpand _ʳ = ∀ x → ε ≤ (x ʳ ∙ x)

  -- define shorthand notation for a term being the left/right adjoint
  -- of another term, which can be proven to be unique.
  _LeftAdjointOf_ : ∀ y x → Set _
  _LeftAdjointOf_ y x = (y ∙ x) ≤ ε × ε ≤ (x ∙ y)

  _RightAdjointOf_ : ∀ y x → Set _
  _RightAdjointOf_ y x = (x ∙ y) ≤ ε × ε ≤ (y ∙ x)

-- Definition of a pregroup, which adds a left and a right adjoint to
-- an ordered monoid.
record IsPregroup {a ℓ₁ ℓ₂} {A : Set a} (≈ : Rel A ℓ₁) (≤ : Rel A ℓ₂)
                  (∙ : Op₂ A) (ε : A) (ˡ : Op₁ A) (ʳ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where

  open AdjointProperties ≤ ∙ ε
  field
    isOrderedMonoid : IsOrderedMonoid ≈ ≤ ∙ ε
    ˡ-cong          : ˡ Preserves ≈ ⟶ ≈
    ʳ-cong          : ʳ Preserves ≈ ⟶ ≈
    ˡ-contract      : LeftContract ˡ
    ˡ-expand        : LeftExpand ˡ
    ʳ-contract      : RightContract ʳ
    ʳ-expand        : RightExpand ʳ

  open IsOrderedMonoid isOrderedMonoid public
  open AdjointProperties ≤ ∙ ε public

record Pregroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infixl 7 _∙_
  infix  4 _≈_
  infix  4 _≤_
  field
    Carrier    : Set c
    _≈_        : Rel Carrier ℓ₁
    _≤_        : Rel Carrier ℓ₂
    _∙_        : Op₂ Carrier
    _ˡ         : Op₁ Carrier
    _ʳ         : Op₁ Carrier
    ε          : Carrier
    isPregroup : IsPregroup _≈_ _≤_ _∙_ ε _ˡ _ʳ

  open IsPregroup isPregroup public

  private
    -- for usage with ≤-Reasoning
    poset : Poset c ℓ₁ ℓ₂
    poset = record { isPartialOrder = isPartialOrder }
    open ≤-Reasoning poset

    -- for usage of substitutivity (which is not defined in IsPregroup)
    orderedMonoid : OrderedMonoid _ _ _
    orderedMonoid = record { isOrderedMonoid = isOrderedMonoid }
    open OrderedMonoid orderedMonoid public using (substitutivity)

  ˡ-unique : ∀ {x y} → y LeftAdjointOf x → y ≈ x ˡ
  ˡ-unique {x} {y} (y-contract , y-expand) = antisym y≤xˡ xˡ≤y
    where
      y≤xˡ : y ≤ x ˡ
      y≤xˡ =
        begin
          y             ≈⟨ sym (proj₂ identity y) ⟩
          y ∙ ε         ≤⟨ compatibility ≤-refl (ˡ-expand x) ⟩
          y ∙ (x ∙ x ˡ) ≈⟨ sym (assoc y x (x ˡ)) ⟩
          (y ∙ x) ∙ x ˡ ≤⟨ compatibility y-contract ≤-refl ⟩
          ε ∙ x ˡ       ≈⟨ proj₁ identity (x ˡ) ⟩
          x ˡ
        ∎
      xˡ≤y : x ˡ ≤ y
      xˡ≤y =
        begin
          x ˡ             ≈⟨ sym (proj₂ identity (x ˡ)) ⟩
          x ˡ ∙ ε         ≤⟨ compatibility ≤-refl y-expand ⟩
          x ˡ ∙ (x ∙ y)   ≈⟨ sym (assoc (x ˡ) x y) ⟩
          (x ˡ  ∙ x) ∙ y  ≤⟨ compatibility (ˡ-contract x) ≤-refl ⟩
          ε ∙ y           ≈⟨ proj₁ identity y ⟩
          y
        ∎

  ʳ-unique : ∀ {x y} → y RightAdjointOf x → y ≈ x ʳ
  ʳ-unique {x} {y} (y-contract , y-expand) = antisym y≤xʳ xʳ≤y
    where
      xʳ≤y : x ʳ ≤ y
      xʳ≤y =
        begin
          x ʳ             ≈⟨ sym (proj₁ identity (x ʳ)) ⟩
          ε ∙ x ʳ         ≤⟨ compatibility y-expand ≤-refl ⟩
          (y ∙ x) ∙ x ʳ ≈⟨ assoc  y x (x ʳ) ⟩
          y ∙ (x ∙ x ʳ) ≤⟨ compatibility ≤-refl (ʳ-contract x) ⟩
          y ∙ ε         ≈⟨ proj₂ identity y ⟩
          y
        ∎
      y≤xʳ : y ≤ x ʳ
      y≤xʳ =
        begin
          y             ≈⟨ sym (proj₁ identity y) ⟩
          ε ∙ y         ≤⟨ compatibility (ʳ-expand x) ≤-refl ⟩
          (x ʳ ∙ x) ∙ y ≈⟨ assoc (x ʳ) x y ⟩
          x ʳ ∙ (x ∙ y) ≤⟨ compatibility ≤-refl y-contract ⟩
          x ʳ ∙ ε       ≈⟨ proj₂ identity (x ʳ) ⟩
          x ʳ
        ∎

  ˡ-identity : ε ˡ ≈ ε
  ˡ-identity = antisym εˡ≤ε ε≤εˡ
    where
      εˡ≤ε : ε ˡ ≤ ε
      εˡ≤ε =
        begin
          ε ˡ     ≈⟨ sym (proj₂ identity (ε ˡ)) ⟩
          ε ˡ ∙ ε ≤⟨ ˡ-contract ε ⟩
          ε
        ∎
      ε≤εˡ : ε ≤ ε ˡ
      ε≤εˡ =
        begin
          ε       ≤⟨ ˡ-expand ε ⟩
          ε ∙ ε ˡ ≈⟨ proj₁ identity (ε ˡ) ⟩
          ε ˡ
        ∎

  ʳ-identity : ε ʳ ≈ ε
  ʳ-identity = antisym εʳ≤ε ε≤εʳ
    where
      εʳ≤ε : ε ʳ ≤ ε
      εʳ≤ε =
        begin
          ε ʳ     ≈⟨ sym (proj₁ identity (ε ʳ)) ⟩
          ε ∙ ε ʳ ≤⟨ ʳ-contract ε ⟩
          ε
        ∎
      ε≤εʳ : ε ≤ ε ʳ
      ε≤εʳ =
        begin
          ε       ≤⟨ ʳ-expand ε ⟩
          ε ʳ ∙ ε ≈⟨ proj₂ identity (ε ʳ) ⟩
          ε ʳ
        ∎

  ˡ-distrib : ∀ x y → y ˡ ∙ x ˡ ≈ (x ∙ y) ˡ
  ˡ-distrib x y = ˡ-unique ([yˡxˡ][xy]≤ε , ε≤[xy][yˡxˡ])
    where
      [yˡxˡ][xy]≤ε : (y ˡ ∙ x ˡ) ∙ (x ∙ y) ≤ ε
      [yˡxˡ][xy]≤ε =
        begin
          (y ˡ ∙ x ˡ) ∙ (x ∙ y) ≈⟨ sym (assoc (y ˡ ∙ x ˡ) x y) ⟩
          ((y ˡ ∙ x ˡ) ∙ x) ∙ y ≈⟨ ∙-cong (assoc (y ˡ) (x ˡ) x) refl ⟩
          (y ˡ ∙ (x ˡ ∙ x)) ∙ y ≤⟨ compatibility (compatibility ≤-refl (ˡ-contract x)) ≤-refl ⟩
          y ˡ ∙ ε ∙ y           ≈⟨ ∙-cong (proj₂ identity (y ˡ)) refl ⟩
          y ˡ ∙ y               ≤⟨ ˡ-contract y ⟩
          ε
        ∎
      ε≤[xy][yˡxˡ] : ε ≤ (x ∙ y) ∙ (y ˡ ∙ x ˡ)
      ε≤[xy][yˡxˡ] =
        begin
          ε                     ≤⟨ ˡ-expand x ⟩
          x ∙ x ˡ               ≈⟨ ∙-cong (sym (proj₂ identity x)) refl ⟩
          x ∙ ε ∙ x ˡ           ≤⟨ compatibility (compatibility ≤-refl (ˡ-expand y)) ≤-refl ⟩
          (x ∙ (y ∙ y ˡ) ∙ x ˡ) ≈⟨ ∙-cong (sym (assoc x y (y ˡ))) refl ⟩
          ((x ∙ y) ∙ y ˡ) ∙ x ˡ ≈⟨ assoc (x ∙ y) (y ˡ) (x ˡ) ⟩
          (x ∙ y) ∙ (y ˡ ∙ x ˡ)
        ∎

  ʳ-distrib : ∀ x y → y ʳ ∙ x ʳ ≈ (x ∙ y) ʳ
  ʳ-distrib x y = ʳ-unique ([xy][yʳxʳ]≤ε , ε≤[xy][yʳxʳ])
    where
      [xy][yʳxʳ]≤ε : (x ∙ y) ∙ (y ʳ ∙ x ʳ) ≤ ε
      [xy][yʳxʳ]≤ε =
        begin
          (x ∙ y) ∙ (y ʳ ∙ x ʳ) ≈⟨ sym (assoc (x ∙ y) (y ʳ) (x ʳ)) ⟩
          ((x ∙ y) ∙ y ʳ) ∙ x ʳ ≈⟨ ∙-cong (assoc x y (y ʳ)) refl ⟩
          (x ∙ (y ∙ y ʳ) ∙ x ʳ) ≤⟨ compatibility (compatibility ≤-refl (ʳ-contract y)) ≤-refl ⟩
          x ∙ ε ∙ x ʳ           ≈⟨ ∙-cong (proj₂ identity x) refl ⟩
          x ∙ x ʳ               ≤⟨ ʳ-contract x ⟩
          ε
        ∎
      ε≤[xy][yʳxʳ] : ε ≤ (y ʳ ∙ x ʳ) ∙ (x ∙ y)
      ε≤[xy][yʳxʳ] =
        begin
          ε                     ≤⟨ ʳ-expand y ⟩
          y ʳ ∙ y               ≈⟨ ∙-cong refl (sym (proj₁ identity y)) ⟩
          y ʳ ∙ (ε ∙ y)         ≤⟨ compatibility ≤-refl (compatibility (ʳ-expand x) ≤-refl) ⟩
          y ʳ ∙ ((x ʳ ∙ x) ∙ y) ≈⟨ ∙-cong refl (assoc (x ʳ) x y) ⟩
          y ʳ ∙ (x ʳ ∙ (x ∙ y)) ≈⟨ sym (assoc (y ʳ) (x ʳ) (x ∙ y)) ⟩
          (y ʳ ∙ x ʳ) ∙ (x ∙ y)
        ∎

  ˡ-contra : ∀ {x y} → x ≤ y → y ˡ ≤ x ˡ
  ˡ-contra {x} {y} x≤y =
    begin
      y ˡ             ≈⟨ sym (proj₂ identity (y ˡ)) ⟩
      y ˡ ∙ ε         ≤⟨ compatibility ≤-refl (ˡ-expand x) ⟩
      y ˡ ∙ (x ∙ x ˡ) ≈⟨ sym (assoc (y ˡ) x (x ˡ)) ⟩
      (y ˡ ∙ x) ∙ x ˡ ≤⟨ substitutivity x≤y ⟩
      (y ˡ ∙ y) ∙ x ˡ ≤⟨ compatibility (ˡ-contract y) ≤-refl ⟩
      ε ∙ x ˡ         ≈⟨ proj₁ identity (x ˡ) ⟩
      x ˡ
    ∎

  ʳ-contra : ∀ {x y} → x ≤ y → y ʳ ≤ x ʳ
  ʳ-contra {x} {y} x≤y =
    begin
      y ʳ             ≈⟨ sym (proj₁ identity (y ʳ)) ⟩
      ε ∙ y ʳ         ≤⟨ compatibility (ʳ-expand x) ≤-refl ⟩
      (x ʳ ∙ x) ∙ y ʳ ≤⟨ substitutivity x≤y ⟩
      (x ʳ ∙ y) ∙ y ʳ ≈⟨ assoc (x ʳ) y (y ʳ) ⟩
      x ʳ ∙ (y ∙ y ʳ) ≤⟨ compatibility ≤-refl (ʳ-contract y) ⟩
      x ʳ ∙ ε         ≈⟨ proj₂ identity (x ʳ) ⟩
      x ʳ
    ∎

  ʳˡ-cancel : ∀ x → x ʳ ˡ ≈ x
  ʳˡ-cancel x = sym (ˡ-unique (ʳ-contract x , ʳ-expand x))

  ˡʳ-cancel : ∀ x → x ˡ ʳ ≈ x
  ˡʳ-cancel x = sym (ʳ-unique (ˡ-contract x , ˡ-expand x))

max_stars_repo_name: wenkokke/agda-pregroup

max_issues_repo_name: wenkokke/agda-pregroup

max_forks_repo_name: wenkokke/agda-pregroup


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

{-# OPTIONS --sized-types --guardedness #-}

open import Data.Nat
open import Data.Vec
open import Data.Product
open import Data.Sum
open import Data.Fin
open import Relation.Binary.PropositionalEquality
open import Data.Unit
open import Data.Bool
open import Data.Empty
open import Codata.Colist
open import Codata.Thunk
open import Size
open import Examples.Colists.Auxiliary.Colist_member
open import Examples.Colists.Auxiliary.MaxOf

open import is-lib.InfSys

module Examples.Colists.Max where

  U = ℕ × Colist ℕ ∞

  data maxElemRN : Set where
    max-h max-t : maxElemRN

  data maxElemCoRN : Set where
    co-max-h : maxElemCoRN

  max-h-r : FinMetaRule U
  max-h-r .Ctx = Σ[ (_ , xs) ∈ ℕ × Thunk (Colist ℕ) ∞ ] xs .force ≡ []
  max-h-r .comp ((x , xs) , _) =
    [] ,
    --------------
    (x , x ∷ xs)

  max-t-r : FinMetaRule U
  max-t-r .Ctx = Σ[ (x , y , z , _) ∈ ℕ × ℕ × ℕ × Thunk (Colist ℕ) ∞ ] z ≡ max x y
  max-t-r .comp ((x , y , z , xs) , _) =
    (x , xs .force) ∷ [] ,
    --------------
    (z , y ∷ xs)

  co-max-h-r : FinMetaRule U
  co-max-h-r .Ctx = ℕ × Thunk (Colist ℕ) ∞
  co-max-h-r .comp (x , xs) =
    [] ,
    --------------
    (x , x ∷ xs)

  maxElemIS : IS U
  maxElemIS .Names = maxElemRN
  maxElemIS .rules max-h = from max-h-r
  maxElemIS .rules max-t = from max-t-r

  maxElemCoIS : IS U
  maxElemCoIS .Names = maxElemCoRN
  maxElemCoIS .rules co-max-h = from co-max-h-r

  _maxElem_ : ℕ → Colist ℕ ∞ → Set
  x maxElem xs = FCoInd⟦ maxElemIS , maxElemCoIS ⟧ (x , xs)

  _maxElemᵢ_ : ℕ → Colist ℕ ∞ → Set
  x maxElemᵢ xs = Ind⟦ maxElemIS ∪ maxElemCoIS ⟧ (x , xs)

  maxSpec inSpec geqSpec : U → Set
  inSpec (x , xs) = x ∈ xs
  geqSpec (x , xs) = ∀{n} → n ∈ xs → x ≡ max x n
  maxSpec u = inSpec u × geqSpec u

  maxElemSound-in-ind : ∀{x xs} → x maxElemᵢ xs → inSpec (x , xs)
  maxElemSound-in-ind (fold (inj₁ max-h , _ , refl , _)) = here
  maxElemSound-in-ind (fold (inj₁ max-t , (_ , eq) , refl , prem)) with max-refl-eq eq
  maxElemSound-in-ind (fold (inj₁ max-t , (_ , eq) , refl , prem)) | inj₁ refl = there (maxElemSound-in-ind (prem zero))
  maxElemSound-in-ind (fold (inj₁ max-t , (_ , eq) , refl , prem)) | inj₂ refl = here
  maxElemSound-in-ind (fold (inj₂ co-max-h , _ , refl , _)) = here

  maxElemSound-in : ∀{x xs} → x maxElem xs → inSpec (x , xs)
  maxElemSound-in max = maxElemSound-in-ind (fcoind-to-ind max)

  maxElemSound-gr : ∀{x xs} → x maxElem xs → geqSpec (x , xs)
  maxElemSound-gr max here with max .CoInd⟦_⟧.unfold
  maxElemSound-gr max here | max-h , _ , refl , _ = max-self
  maxElemSound-gr max here | max-t , ((_ , eq) , _) , refl , _ with max-refl-eq eq
  ... | inj₁ refl = eq
  ... | inj₂ refl = max-self
  maxElemSound-gr max (there mem) with max .CoInd⟦_⟧.unfold
  maxElemSound-gr max (there mem) | max-h , ((_ , eq) , _) , refl , _ = ⊥-elim (mem-abs mem eq)
  maxElemSound-gr max (there mem) | max-t , ((_ , eq) , _) , refl , pr with max-refl-eq eq
  ... | inj₁ refl = maxElemSound-gr (pr zero) mem
  ... | inj₂ refl =
    let rec = maxElemSound-gr (pr zero) mem in
    max-trans rec (max-comm eq)

  maxElemSound : ∀{x xs} → x maxElem xs → maxSpec (x , xs)
  maxElemSound max = maxElemSound-in max , maxElemSound-gr max

  maxSpecBounded : ∀{x xs} → inSpec (x , xs) → geqSpec (x , xs) → x maxElemᵢ xs
  maxSpecBounded here _ = apply-ind (inj₂ co-max-h) _ λ ()
  maxSpecBounded (there mem) gr = apply-ind (inj₁ max-t) (_ , gr here) λ{zero → maxSpecBounded mem λ m → gr (there m)}

  postulate
    old-max : ∀{n x y xs ys} → Thunk.force xs ≡ (y ∷ ys) →
                    maxSpec (n , (x ∷ xs)) → Σ[ m ∈ ℕ ] maxSpec (m , (y ∷ ys))

  maxSpecCons : ∀{x xs} → inSpec (x , xs) → geqSpec (x , xs) → ISF[ maxElemIS ] maxSpec (x , xs)
  maxSpecCons {x} {x ∷ xs} here gr with xs .force | inspect (λ t → t .force) xs
  maxSpecCons {x} {x ∷ xs} here gr | [] | [ eq ] = max-h , (_ , eq) , refl , λ ()
  maxSpecCons {x} {x ∷ xs} here gr | _ ∷ _ | [ eq ] =
    let old , mem , gr' = old-max eq (here , gr) in
    let mem-xs = subst (λ xs → old ∈ xs) (sym eq) mem in
    max-t , (_ , max-comm (gr (there mem-xs))) , refl , λ{zero → mem-xs , λ m → gr' (subst (λ xs → _ ∈ xs) eq m)}
  maxSpecCons {x} {.(_ ∷ _)} (there mem) gr = max-t , (_ , gr here) , refl , λ{zero → mem , λ m → gr (there m)}

  maxElemComplete : ∀{x xs} → maxSpec (x , xs) → x maxElem xs
  maxElemComplete =
    bounded-coind[ maxElemIS , maxElemCoIS ] maxSpec (λ{(x , xs) → maxSpecBounded x xs}) λ{(x , xs) → maxSpecCons x xs}

max_stars_repo_name: LcicC/inference-systems-agda

max_issues_repo_name: LcicC/inference-systems-agda

max_forks_repo_name: LcicC/inference-systems-agda


text:
------------------------------------------------------------------------
-- A stream equality universe
------------------------------------------------------------------------

module Stream.Equality where

open import Codata.Musical.Notation
open import Stream hiding (_⋎_)
open import Stream.Programs
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Vec using (Vec; []; _∷_)

infixr 5 _≺_
infix  3 _≃_ _≅_ _≊_ _∎
infixr 2 _≊⟨_⟩_ _≡⟨_⟩_

mutual

  _≊_ : ∀ {A} (xs ys : Prog A) → Set1
  xs ≊ ys = ⟦ xs ⟧ ≅ ⟦ ys ⟧

  data _≅_ {A} : (xs ys : Stream A) → Set1 where
    _≺_          : ∀ {x y xs ys}
                   (x≡ : x ≡ y) (xs≈ : ∞ (♭ xs ≅ ♭ ys)) →
                   x ≺ xs ≅ y ≺ ys
    _≊⟨_⟩_       : ∀ xs {ys zs}
                   (xs≈ys : ⟦ xs ⟧ ≅ ys) (ys≈zs : ys ≅ zs) → ⟦ xs ⟧ ≅ zs
    _≡⟨_⟩_       : ∀ xs {ys zs}
                   (xs≡ys : ⟦ xs ⟧ ≡ ys) (ys≈zs : ys ≅ zs) → ⟦ xs ⟧ ≅ zs
    ≅-sym        : ∀ {xs ys} (xs≈ys : xs ≅ ys) → ys ≅ xs
    ·-cong       : ∀ {B}
                   (f : B → A) xs ys (xs≈ys : xs ≊ ys) →
                   f · xs ≊ f · ys
    ⟨_⟩-cong     : ∀ {B C} (_∙_ : B → C → A)
                   xs xs′ (xs≈xs′ : xs ≊ xs′)
                   ys ys′ (ys≈ys′ : ys ≊ ys′) →
                   xs ⟨ _∙_ ⟩ ys ≊ xs′ ⟨ _∙_ ⟩ ys′
    ⋎-cong       : ∀ xs xs′ (xs≈xs′ : xs ≊ xs′)
                          ys ys′ (ys≈ys′ : ys ≊ ys′) →
                   xs ⋎ ys ≊ xs′ ⋎ ys′
    ≺≺-cong      : ∀ {n}
                   (xs xs′ : Vec A n) (xs≡xs′ : xs ≡ xs′)
                   ys ys′ (ys≈ys′ : ys ≊ ys′) →
                   xs ≺≺ ys ≊ xs′ ≺≺ ys′

data _≃_ {A} : (xs ys : Stream A) → Set1 where
  _≺_ : ∀ {x y xs ys}
        (x≡ : x ≡ y) (xs≈ : ♭ xs ≅ ♭ ys) → x ≺ xs ≃ y ≺ ys

≅⇒≃ : ∀ {A} {xs ys : Stream A} → xs ≅ ys → xs ≃ ys
≅⇒≃ (x≡ ≺ xs≈)                 = x≡ ≺ ♭ xs≈
≅⇒≃ (xs ≊⟨ xs≈ys ⟩ ys≈zs)      with whnf xs | ≅⇒≃ xs≈ys | ≅⇒≃ ys≈zs
≅⇒≃ (xs ≊⟨ xs≈ys ⟩ ys≈zs)      | x ≺ xs′ | x≡y ≺ xs≈ys′ | y≡z ≺ ys≈zs′ =
                                 trans x≡y y≡z ≺ (xs′ ≊⟨ xs≈ys′ ⟩ ys≈zs′)
≅⇒≃ (xs ≡⟨ refl ⟩ ys≈zs)       = ≅⇒≃ ys≈zs
≅⇒≃ (≅-sym xs≈ys)              with ≅⇒≃ xs≈ys
≅⇒≃ (≅-sym xs≈ys)              | x≡y ≺ xs≈ys′ = sym x≡y ≺ ≅-sym xs≈ys′
≅⇒≃ (·-cong f xs ys xs≈ys)     with whnf xs | whnf ys | ≅⇒≃ xs≈ys
≅⇒≃ (·-cong f xs ys xs≈ys)     | x ≺ xs′ | y ≺ ys′ | x≡y ≺ xs≈ys′ =
                                 cong f x≡y ≺ ·-cong f xs′ ys′ xs≈ys′
≅⇒≃ (⟨ ∙ ⟩-cong xs xs′ xs≈xs′
                ys ys′ ys≈ys′) with whnf xs | whnf xs′ | ≅⇒≃ xs≈xs′
                                  | whnf ys | whnf ys′ | ≅⇒≃ ys≈ys′
≅⇒≃ (⟨ ∙ ⟩-cong xs xs′ xs≈xs′
                ys ys′ ys≈ys′) | _ ≺ txs | _ ≺ txs′ | x≡y  ≺ txs≈txs′
                               | _ ≺ tys | _ ≺ tys′ | x≡y′ ≺ tys≈tys′ =
                                 cong₂ ∙ x≡y x≡y′ ≺
                                 ⟨ ∙ ⟩-cong txs txs′ txs≈txs′
                                            tys tys′ tys≈tys′
≅⇒≃ (⋎-cong xs xs′ xs≈xs′
            ys ys′ ys≈ys′)     with whnf xs | whnf xs′ | ≅⇒≃ xs≈xs′
≅⇒≃ (⋎-cong xs xs′ xs≈xs′
            ys ys′ ys≈ys′)     | _ ≺ txs | _ ≺ txs′ | x≡y ≺ txs≈txs′ =
                                 x≡y ≺ ⋎-cong ys  ys′  ys≈ys′
                                              txs txs′ txs≈txs′
≅⇒≃ (≺≺-cong [] [] refl
             ys ys′ ys≈ys′)    = ≅⇒≃ ys≈ys′
≅⇒≃ (≺≺-cong
      (x ∷ xs) .(_ ∷ _) refl
      ys ys′ ys≈ys′)           = refl ≺ ≺≺-cong xs xs refl ys ys′ ys≈ys′

mutual

  ≃⇒≈ : ∀ {A} {xs ys : Stream A} → xs ≃ ys → xs ≈ ys
  ≃⇒≈ (refl ≺ xs≈) = refl ≺ ♯ ≅⇒≈ xs≈

  ≅⇒≈ : ∀ {A} {xs ys : Stream A} → xs ≅ ys → xs ≈ ys
  ≅⇒≈ xs≈ = ≃⇒≈ (≅⇒≃ xs≈)

≊⇒≈ : ∀ {A} {xs ys : Prog A} → xs ≊ ys → ⟦ xs ⟧ ≈ ⟦ ys ⟧
≊⇒≈ = ≅⇒≈

≈⇒≅ : ∀ {A} {xs ys : Stream A} → xs ≈ ys → xs ≅ ys
≈⇒≅ (refl ≺ xs≈) = refl ≺ ♯ ≈⇒≅ (♭ xs≈)

_∎ : ∀ {A} (xs : Prog A) → xs ≊ xs
xs ∎ = ≈⇒≅ (Setoid.refl (Stream.setoid _))

≊-η : ∀ {A} (xs : Prog A) → xs ≊ headP xs ≺ ♯ tailP xs
≊-η xs with whnf xs
≊-η xs | x ≺ xs′ = refl ≺ ♯ (xs′ ∎)

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
module sbconst2 where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat
open import Data.Fin
open import Data.List

open import automaton
open import nfa
open import logic
open NAutomaton
open Automaton
open import  Relation.Binary.PropositionalEquality hiding ( [_] )

open Bool

δconv : { Q : Set } { Σ : Set  } → ( ( Q → Bool ) → Bool ) →  ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool)
δconv {Q} { Σ} exists nδ f i q =  exists ( λ r → f r /\ nδ r i q )

subset-construction : { Q : Set } { Σ : Set  } →
    ( ( Q → Bool ) → Bool ) →
    (NAutomaton Q  Σ ) → (Automaton (Q → Bool)  Σ )
subset-construction {Q} { Σ}  exists NFA = record {
        δ = λ q x → δconv exists ( Nδ NFA ) q x
     ;  aend = λ f → exists ( λ q → f q /\ Nend NFA q )
   }

test4 = subset-construction existsS1 am2

test51 = accept test4 start1 ( i0  ∷ i1  ∷ i0  ∷ [] )
test61 = accept test4 start1 ( i1  ∷ i1  ∷ i1  ∷ [] )

subset-construction-lemma→ : { Q : Set } { Σ : Set  } → (exists : ( Q → Bool ) → Bool ) →
    (NFA : NAutomaton Q  Σ ) → (astart : Q → Bool )
    → (x : List Σ)
    → Naccept NFA exists astart  x ≡ true
    → accept (  subset-construction exists NFA ) astart  x ≡ true
subset-construction-lemma→ {Q} {Σ}  exists NFA astart x naccept = lemma1 x astart naccept where
    lemma1 :  (x : List Σ) → ( states : Q → Bool )
       → Naccept NFA exists states x ≡ true
       → accept (  subset-construction exists NFA ) states x ≡ true
    lemma1 [] states naccept = naccept
    lemma1 (h ∷ t ) states naccept = lemma1 t (δconv exists (Nδ NFA) states h) naccept

subset-construction-lemma← : { Q : Set } { Σ : Set  }   → (exists : ( Q → Bool ) → Bool ) →
    (NFA : NAutomaton Q  Σ ) → (astart : Q → Bool )
    → (x : List Σ)
    → accept (  subset-construction exists NFA ) astart x ≡ true
    → Naccept NFA exists astart x ≡ true
subset-construction-lemma← {Q} {Σ}  exists NFA astart x saccept = lemma2 x astart saccept where
    lemma2 :  (x : List Σ) → ( states : Q → Bool )
       → accept (  subset-construction exists NFA ) states x ≡ true
       → Naccept NFA exists states x ≡ true
    lemma2 [] states saccept = saccept
    lemma2 (h ∷ t ) states saccept = lemma2 t (δconv exists (Nδ NFA) states h) saccept


text:
{-# OPTIONS --without-K #-}
module function where

open import function.core public
open import function.overloading public
open import function.isomorphism public
open import function.extensionality public
open import function.fibration public

max_issues_repo_name: HoTT/M-types


text:
{-# OPTIONS --copatterns #-}
{-# IMPORT Ex4Haskell #-}
{-# IMPORT System.IO #-}

module Ex4 where -- Conor: 8/20

{- I'm sorry I haven't quite finished setting this exercise yet, but by
   the joy of version control, the rest of it can be merged in later
   (quite soon). At least you can get cracking: I promise not to break
   anything, just to add a bit more on the end.

   The deadline for this is Friday of Week 12 (11 Dec).
   It'd be good to get the marks in before Christmas, but if the end of
   term is looking deadlinetastic, please open negotiations.

   UPDATE: I had to work around a bug in Agda to get this finished, so
   it took longer than I had hoped. I apologise, and will be flexible
   with deadlines, consequently. Also, I had to tweak the setup for
   cp a little, asking you to abstract out your definition of the
   FinalState of cp. I need to refer to it in the later code. That may
   cause a wee merge conflict, easily rectified with cut and paste.
-}

open import CS410-Prelude
open import CS410-Indexed

{-
data List (X : Set) : Set where  -- X scopes over the whole declaration...
  []    : List X                 -- ...so you can use it here...
  _::_  : X -> List X -> List X  -- ...and here.
infixr 3 _::_

{-# BUILTIN BOOL Two #-}
{-# BUILTIN TRUE tt #-}
{-# BUILTIN FALSE ff #-}
{-# BUILTIN LIST List #-}
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _::_ #-}
{-# COMPILED_DATA List [] [] (:) #-}

postulate -- this means that we just suppose the following things exist...
  Char : Set
  String : Set

{-# BUILTIN CHAR Char #-}
{-# COMPILED_TYPE Char Char #-}
{-# BUILTIN STRING String #-}
{-# COMPILED_TYPE String String #-}

primitive -- these are baked in; they even work!
  primCharEquality : Char -> Char -> Two
  primStringAppend : String -> String -> String
  primStringToList : String -> List Char
  primStringFromList : List Char -> String
-}

---------------------------------------------------------------------------
-- WRITING FILES, AN INTERFACE
---------------------------------------------------------------------------

{- If you possess the ability to open a file for writing, you might
   have the following interface. -}

-- States
data WriteState : Set where
  opened closed : WriteState  -- do you currently have a file open or not?

-- Commands
data WriteC : WriteState -> Set where
  openWrite   : (fileName : String)  -> WriteC closed
  writeChar   : Char                 -> WriteC opened
  closeWrite  :                         WriteC opened

-- Responses
WriteR : (j : WriteState)(c : WriteC j) -> Set
WriteR .closed (openWrite fileName)  = WriteState  -- we get told whether it worked
WriteR .opened (writeChar x)         = One  -- always works
WriteR .opened closeWrite            = One  -- always works

{- 4.1 Implement the following operation which determines the next
   state. You should ensure that you can write characters only to
   a successfully opened file, and that you can write as many as
   you want. It should also be possible to insist that a process
   closes its file. -} -- Conor: 1/1

writeNext : (j : WriteState)(c : WriteC j) -> WriteR j c -> WriteState
writeNext .closed (openWrite fileName) r = r
writeNext .opened (writeChar x) r = opened
writeNext .opened closeWrite r = closed
-- the file writing interface, assembled as an indexed container
WRITE : WriteState => WriteState
WRITE = WriteC <! WriteR / writeNext

---------------------------------------------------------------------------
-- READING FILES, AN INTERFACE
---------------------------------------------------------------------------

{- To read from a file, it should be open, and you shouldn't be at the
   end of it. -}

-- States
data ReadState : Set where
  opened : (eof : Two) -> ReadState -- eof is tt if we're at end of file
  closed : ReadState

{- 4.2 Finish the READ implementation, in accordance with the description. -}
-- Conor: 2.5/3

-- Commands
data ReadC : ReadState -> Set where
  openRead    : (fileName : String) -> ReadC closed
 -- needs a filename; might not open successfully;
 -- might open an empty file
  readChar : ReadC (opened ff)
 -- makes sense only if we're not at end of file
 -- and might take us to end of file
  closeRead   : (eof : Two) -> ReadC (opened eof)
 -- makes sense only if the file is open

-- Responses
ReadR : (j : ReadState)(c : ReadC j) -> Set
ReadR .closed (openRead fileName) = ReadState
ReadR .(opened ff) readChar = Two  -- Conor: the character read should also be given
ReadR .(opened eof) (closeRead eof) = One

-- next State; you need to make sure the response gives enough info
readNext : (j : ReadState)(c : ReadC j) -> ReadR j c -> ReadState
readNext .closed (openRead fileName) r = r
readNext .(opened ff) readChar r =  opened r
readNext .(opened eof) (closeRead eof) r = closed

READ : ReadState => ReadState
READ = ReadC <! ReadR / readNext

---------------------------------------------------------------------------
-- COMBINING TWO INTERFACES WITH SHARED STATE
---------------------------------------------------------------------------

{- 4.3 Let's suppose we have two command-response interfaces which offer
       different functionality for the same system. Correspondingly, we'll
       have two indexed containers for the same index set. Show that you
       can combine them into one indexed container which lets you choose a
       command from either menu and evolves the state as specified by
       whichever interface offered the chosen command.
-} -- Conor: 1/1

_=+=_ : {I : Set} -> I => I -> I => I -> I => I
(Shape <! Position / index) =+= (Shape1 <! Position1 / index1) =
 (Shape +: Shape1) <!
 (λ j → λ {(inl x) → Position j x; (inr x) -> Position1 j x }) /
 (λ j → \{(inl x) → index j x ; (inr x) -> index1 j x})

--  {!λ {(inl x) Position → index j x Position ;(inl x) Position → index1 j x Position1 }!})

--_=+=_ : {I : Set} -> I => I -> I => I -> I => I
--(Shape <! Position / index) =+= (Shape1 <! Position1 / index1)
--  = (Shape +: Shape1) <!
-- (λ j → λ {(inl x) → Position j x; (inr x) -> Position1 j x }) /
-- (λ j x y → {! λ {?}!})
--
--(λ j x y → {!λ {(inl x) y → index j x y ;(inl x) y → index1 j x y }!})

--record _=>_ (I J : Set) : Set1 where
--  constructor _<!_/_
--  field
--    Shape     : J -> Set
--    Position  : (j : J) -> Shape j -> Set
--    index     : (j : J)(s : Shape j) -> Position j s -> I

---------------------------------------------------------------------------
-- WHEN IGNORANCE IS BLISS, BIS
---------------------------------------------------------------------------

{- 4.4 If we have a command-response interface with index I representing
       states of the system, show that we can index basically the same
       commands and responses over a state, I * J, where the J is just
       useless information which never changes. (This operation isn't
       super-useful on its own, but it's handy in combination with other
       things. -} -- Conor: 2/2

GrowR : {I J : Set} -> I => I -> (I * J) => (I * J)
GrowR (Shape <! Position / index)
  = (λ z → Shape (fst z))
  <! (λ j z → Position (fst j) z )
  / (λ j s x → index (fst j) s x , snd j)

-- do the same for "growing the index on the left"

GrowL : {I J : Set} -> I => I -> (J * I) => (J * I)
GrowL (Shape <! Position / index)
  = (λ z → Shape (snd z))
  <! (λ j z → Position (snd j) z)
  / (λ j s x → fst j , index (snd j) s x)

---------------------------------------------------------------------------
-- COMBINING TWO INTERFACES WITH SEPARATE STATE
---------------------------------------------------------------------------

{- 4.5 Making use of 4.3 and 4.4, show how to combine two interfaces which
       operate independently on separate state: commands from one should
       not affect the state of the other.
-} -- Conor: 1/1

_<+>_ : {I0 I1 : Set} -> I0 => I0 -> I1 => I1 -> (I0 * I1) => (I0 * I1)
CRn0 <+> CRn1 = GrowR CRn0 =+= GrowL CRn1

---------------------------------------------------------------------------
-- ERROR REPORTING, AN INTERFACE
---------------------------------------------------------------------------

{- I'm building the next bit for you.

   When things go wrong, we need to trigger an error condition and abort
   mission. However, if we have other stuff going on (open files, etc),
   it may not always be ok to drop everything and run away. There will
   be some states in which it is safe to escape (and deliver a suitable
   error message, perhaps) and other states in which escape should be
   impossible.

   If it is safe to issue an error message, we should be able to do so
   without fear of any response from the environment that would oblige
   us to carry on.
-}

data ErrorC {I : Set}(SafeMessage : I -> Set)(i : I) : Set where
  error : SafeMessage i -> ErrorC SafeMessage i
    -- the SafeMessage parameter tells us what is an acceptable
    -- error message in any given state; in states where this gives
    -- Zero, it will be impossible to trigger an error!

ErrorR : {I : Set}{SafeMessage : I -> Set}(i : I)(c : ErrorC SafeMessage i) -> Set
ErrorR _ _ = Zero  -- there's no comeback

errorNext : {I : Set}{SafeMessage : I -> Set}
            (i : I)(c : ErrorC SafeMessage i) -> ErrorR i c -> I
errorNext i c ()  -- so we don't have to say how the state will evolve

ERROR : {I : Set}(SafeMessage : I -> Set) -> I => I
ERROR SafeMessage = ErrorC SafeMessage <! ErrorR / errorNext

---------------------------------------------------------------------------
-- COPY A FILE
---------------------------------------------------------------------------

{- 4.6 Implement a process which, given access to suitable interfaces, will
       give the process for copying a named source file to a named target
       file. This goes in two phases.
-}

{- 4.6.1 Firstly, you should identify the command-reponse interface within
   which you need to work. You will need to be able to read and write files,
   but also to signal errors (in case a file fails to open for some reason).
   You must ensure that it is impossible for any process using your interface
   to escape with an error leaving a file open. You must also make it
   possible to guarantee that your copying process will, error or not, leave
   all files closed.
-} -- Conor: 0.5/1

CPState : Set
CPState =  ReadState * WriteState

CPInterface : CPState => CPState
CPInterface = (READ <+> WRITE) -- Conor: good start but, yes
--ERROR -- Conor: is the question

{-
 ReadState  WriteState
-}

{- 4.6.2 Secondly, you should implement your copying process, working to your
   interface.
-} -- Conor: 0/3

FinalState : CPState -> Set
FinalState c = {!!}

cp : (sourceFile targetFile : String) -> IterIx CPInterface FinalState {!!}
cp sourceFile targetFile = {!!}

{- HINTS
  You will certainly need to build some extra bits and pieces.

  You have the components for reading, writing and error handling, and
  suitable kit with which to combine them. Reading and writing don't
  interfere with each other, but it's important to make sure that you
  can't bomb out with an error, so some shared state seems important.

  There are really two phases to the process:
    (1) getting the files open  -- this may go wrong
    (2) copying from one to the other  -- this will work if we reach it
  You might want to split these phases apart.
-}

---------------------------------------------------------------
-- TO BE CONTINUED...
---------------------------------------------------------------

-- The rest of the exercise is to fill selected gaps in code that
-- gets your cp process to the stage where it actually compiles.

-- Agda version 2.4.2.4 is needed t compile the "copatterns" involved
-- in the code, but you should be able to complete the exercise
-- without upgrading, if you are currently using an earlier version.
-- It is only the business of generating a standalone executable that
-- needs the upgrade. Still, it'd be nice to see it go, wouldn't it?

-- The key is to build a device driver between your carefully
-- designed command-response system and "scripts" built from
-- low-level Haskell commands, maintaining the file handles
-- involved as you go.

-- Then you'll need to explain how to run the low-level script.

---------------------------------------------------------------
-- What's a Device Driver? (My bit. Do read.)
---------------------------------------------------------------

open _=>_ public

Driver :
  {I J : Set}              -- I is "high-level state" ; J, "low"
  (Sync : I -> J -> Set)   -- when are states "in sync"?
  (Hi : I => I)            -- high-level command-response system
  (Lo : J => J)            -- low-level command-response system
  -> Set

Driver {I}{J} Sync Hi Lo =
  forall i j -> Sync i j ->     -- whenever we're in sync,
  (c : Shape Hi i) ->           -- we can take a high-level command
  Sg (Shape Lo j) \ c' ->       -- and give the low-level version,
  (r' : Position Lo j c') ->    -- then take the low-level response
  Sg (Position Hi i c) \ r ->   -- and give the high-level version,
  Sync (index Hi i c r) (index Lo j c' r')  -- and stay in sync!

drive : forall  {I J}{Sync : I -> J -> Set}
                {Hi : I => I}{Lo : J => J}
                (D : Driver Sync Hi Lo)
                {X : I -> Set}
                (i : I)(j : J)
                (ij : Sync i j) ->  -- if we're in sync and have
                IC Hi X i ->        -- a high-level way to get an X
                IC Lo (\ j -> Sg I \ i -> Sync i j * X i) j
                  -- then we have a low-level plan to
                  -- stay in sync and get an X
drive D i j ij (c , k) =
  let x = D i j ij c ; c' = fst x ; D' = snd x
  in  c' , \ r' ->  -- issue low-level command c', get response r'
      let y = D' r' ; r = fst y ; s = snd y
      in  _ , s , k r  -- choose sync state from driver, call continuation

---------------------------------------------------------------
-- SCRIPTING COMMANDS (your bit)
---------------------------------------------------------------

{- 4.7 Complete the definition of the command response system
   for scripting commands built from another command response system,
   C. A scripted command is a whole strategy for interacting with C,
   the way you can write shell scripts which give strategies for
   issuing commands at a terminal. Your job is to give the type
   for responses (which should pack up all the responses to the
   commands) and compute the next state (which should be the state
   the system reaches when the script stops).

   Then you should construct the function which translates
   one SCRIPT C interaction to many C interactions. That's to say,
   implement the "script interpreter".
-} -- Conor: 0/2

SCRIPT : forall {I} -> (I => I) -> (I => I)
SCRIPT {I} C = FreeIx C (\ _ -> One) <! ScriptR / ScriptN where
  ScriptR : (i : I) -> FreeIx C (\ _ -> One) i -> Set
  ScriptR i cs = {!!}
  ScriptN : (i : I)(c : FreeIx C (\ _ -> One) i) -> ScriptR i c -> I
  ScriptN i cs rs = {!!}

unscript : forall {I}{X : I -> Set}(C : I => I) ->
           [ IC (SCRIPT C) X -:> FreeIx C X ]
unscript {I}{X} C (c , k) = help c k where
  help : {i : I}(c : FreeIx C (\ _ -> One) i)
         (k : (p : Position (SCRIPT C) i c) ->
                X (index (SCRIPT C) i c p)) ->
         FreeIx C X i
  help cs k = {!!}

---------------------------------------------------------------
-- An Interface to Haskell IO (also my bit)
---------------------------------------------------------------

-- an Agda Maybe-type which connects to Haskell's
data Maybe (X : Set) : Set where
  yes : X -> Maybe X
  no  : Maybe X
{-# COMPILED_DATA Maybe Maybe Just Nothing #-}

-- an Agda Either-type which connects to Haskell's
data Either (S T : Set) : Set where
  left  : S -> Either S T
  right : T -> Either S T
{-# COMPILED_DATA Either Either Left Right #-}

-- a copy of Haskell's file access more datatype
data IOMode : Set where
  readMode writeMode appendMode readWriteMode : IOMode
{-# COMPILED_DATA IOMode System.IO.IOMode System.IO.ReadMode System.IO.WriteMode System.IO.AppendMode System.IO.ReadWriteMode #-}

-- Haskell's file handles imported abstractly
postulate Handle : Set
{-# COMPILED_TYPE Handle System.IO.Handle #-}

-- The Low-Level Haskell Command-Response System. Please use wisely.

data HaskellIOCommand : Set where
  hOpen                   : String  -> IOMode  -> HaskellIOCommand
  hClose hIsEOF hGetChar  : Handle             -> HaskellIOCommand
  hPutChar                : Handle  -> Char    -> HaskellIOCommand
  hError                  : String             -> HaskellIOCommand

HaskellIOResponse : HaskellIOCommand -> Set
HaskellIOResponse (hOpen f m)     = Maybe Handle
HaskellIOResponse (hClose h)      = One
HaskellIOResponse (hIsEOF h)      = Two
HaskellIOResponse (hGetChar h)    = Char
HaskellIOResponse (hPutChar h c)  = One
HaskellIOResponse (hError e)      = Zero

HASKELLIO : One => One
HASKELLIO = (\ _ -> HaskellIOCommand) <! (\ _ -> HaskellIOResponse) / _

postulate       -- Haskell has a monad for doing IO, which we use at the top level
  IO      : Set -> Set
  return  : {A : Set} -> A -> IO A
  _>>=_   : {A B : Set} -> IO A -> (A -> IO B) -> IO B
  hOpenIO : String -> IOMode -> IO (Maybe Handle)
  hCloseIO : Handle -> IO One
  hIsEOFIO : Handle -> IO Two
  hGetCharIO : Handle -> IO Char
  hPutCharIO : Handle -> Char -> IO One
  hErrorIO : {X : Set} -> String -> IO X
  mainLoop : {S : Set} -> (S -> Either String (IO S)) -> (String -> String -> S) -> IO One
infixl 1 _>>=_
{-# BUILTIN IO IO #-}
{-# COMPILED_TYPE IO IO #-}
{-# COMPILED return (\ _ -> return)    #-}
{-# COMPILED _>>=_  (\ _ _ -> (>>=)) #-}
{-# COMPILED hOpenIO Ex4Haskell.hOpenIO #-}
{-# COMPILED hCloseIO Ex4Haskell.hCloseIO #-}
{-# COMPILED hIsEOFIO Ex4Haskell.hIsEOFIO #-}
{-# COMPILED hGetCharIO Ex4Haskell.hGetCharIO #-}
{-# COMPILED hPutCharIO Ex4Haskell.hPutCharIO #-}
{-# COMPILED hErrorIO (\ _ -> Ex4Haskell.hErrorIO) #-}
{-# COMPILED mainLoop (\ _ -> Ex4Haskell.mainLoop) #-}

-- We explain how to do one command.

doHaskellCommand : (c : HaskellIOCommand) -> IO (HaskellIOResponse c)
doHaskellCommand (hOpen n m) = hOpenIO n m
doHaskellCommand (hClose h)       = hCloseIO h
doHaskellCommand (hIsEOF h)       = hIsEOFIO h
doHaskellCommand (hGetChar h)     = hGetCharIO h
doHaskellCommand (hPutChar h c)   = hPutCharIO h c
doHaskellCommand (hError e)       = hErrorIO e

-- We need a MONAD MORPHISM to translate our HASKELLIO monad to
-- Haskell's IO Monad. A monad morphism is a function between monads
-- which respects return and >>=. Every monad morphism from a FREE
-- monad is given by explaining how to do one command.

haskellIO : forall {X} -> FreeIx HASKELLIO (\ _ -> X) <> -> IO X
haskellIO (ret x)        = return x
haskellIO (do (c , k))   = doHaskellCommand c >>= \ v -> haskellIO (k v)

---------------------------------------------------------------
-- The Driver (your bit)
---------------------------------------------------------------

-- Due to an annoying bug in Agda (which I reported and which has
-- been fixed in the head version), I had to resort to making
-- a rubbish version of One, called Dull.

postulate
  Dull : Set       -- it's a unit type
  dull : Dull      -- see? it has one thing in it?
                   -- you can't pattern match on it

-- For read and write states, we can say which handles we need to
-- know. We should know handles only when files are open.

RH : ReadState -> Set
RH (opened eof)  = Handle
RH closed        = Dull

WH : WriteState -> Set
WH opened        = Handle
WH closed        = Dull

{- 4.8 Define the appropriate notion of Sync for your notion of
   CPState. It should be a collection of the handles appropriate
   for the files currently open, built using RH and WH.

   Then build the driver, carefully. Remember, when reading, to
   check the end-of-file status as required.
-} -- Conor: 0/4

HANDLES : CPState -> One -> Set
HANDLES cps = {!!}

haskellDriver : Driver HANDLES CPInterface (SCRIPT HASKELLIO)
haskellDriver i j s c = {!!}

---------------------------------------------------------------
-- Putting it all together
---------------------------------------------------------------

-- A concrete STATE is some CPState for which we have
--   (i)   the right handles, and
--   (ii)  a plan for how to make progress with copying.

STATE : Set
STATE = Sg CPState \ i ->
        HANDLES i <> * IterIx CPInterface FinalState i

{- 4.9 For your chosen final state, you need to explain how to
   issue a message signalling successful completion. The empty
   string will do, but perhaps you want more. -} -- Conor: 0/1

finalMessage : (i : CPState) -> FinalState i -> String
finalMessage i x = {!!}

-- Now, in each state, we will either discover we're done, or
-- we'll learn the next bunch of Haskell commands to do.

runCP : STATE -> Either String (IO STATE)
runCP (i , h , cp) with force cp
runCP (i , h , cp)  | ret x  = left (finalMessage i x)
runCP (i , h , cp)  | do c   = right
  (haskellIO (unscript HASKELLIO
    (drive haskellDriver {IterIx CPInterface FinalState} i <> h c)))

{- 4.10 To complete the main program, fill in the starting
   CPState and its associated handle information. -} -- Conor: 0/1

main : IO One
main = mainLoop runCP \ src trg ->
         {!!} , {!!} , cp src trg

-- Now, to compile this (using Agda 2.4.2.4), grab a terminal and
-- issue the command
--
--   agda --compile Ex4.agda
--
-- and if you're very lucky, you should be able to issue commands
--
--   ./Ex4 <sourceFile> <targetFile>
--
-- Be careful not to overwrite your homework.
--
-- PS if in doubt about Agda versions, try
--
--   agda -V


text:
------------------------------------------------------------------------------
-- The gcd program is correct
------------------------------------------------------------------------------

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

-- This module proves the correctness of the gcd program using
-- the Euclid's algorithm.

module LTC-PCF.Program.GCD.Total.CorrectnessProof where

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat.Type
open import LTC-PCF.Program.GCD.Total.CommonDivisor using ( gcdCD )
open import LTC-PCF.Program.GCD.Total.Definitions using ( gcdSpec )
open import LTC-PCF.Program.GCD.Total.Divisible using ( gcdDivisible )
open import LTC-PCF.Program.GCD.Total.GCD using ( gcd )

------------------------------------------------------------------------------
-- The gcd is correct.
gcdCorrect : ∀ {m n} → N m → N n → gcdSpec m n (gcd m n)
gcdCorrect Nm Nn = gcdCD Nm Nn , gcdDivisible Nm Nn

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- When checking pattern coverage we might end up having to split
-- on a dot pattern (if the individual clauses split differently).
-- This is fine as long as the dot pattern is on constructor form.
module SplitOnDotPattern where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data Vec (A : Set) : Nat -> Set where
  []   : Vec A zero
  _::_ : forall {n} -> A -> Vec A n -> Vec A (suc n)

rev : forall {A n m} -> Vec A n -> Vec A m -> Vec A m
rev             []        ys = ys
rev {n = suc n} (x :: xs) ys = ys

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe #-}
module Issue2487-3 where

import Issue2487.B


text:
{-# OPTIONS --without-K #-}
module Common.Unit where

open import Agda.Builtin.Unit public renaming (⊤ to Unit; tt to unit)


text:
-- Andreas, 2017-03-01 issue #2480, reported by nad, discovered by simonhu
-- Exploit by Jesper Cockx

-- {-# OPTIONS -v tc.lhs.split:60 #-}

open import Agda.Builtin.Equality

data Bool : Set where
  tt ff : Bool

const : Bool → (Bool → Bool)
const = λ x _ → x

ap : {A : Set} {B : Set} (f : A → B) {a b : A} (p : a ≡ b) → f a ≡ f b
ap f refl = refl

mutual
  -- Type of constant boolean functions, using @UnusedArg@
  Bool→cBool : Set
  Bool→cBool = _

  accepted : (p : const tt ≡ const ff) → ap (λ f → f tt) p ≡ ap (λ f → f ff) p
  accepted p = refl {x = ap {A = Bool→cBool} (λ f → f tt) p}

constant : (f : Bool→cBool) (x y : Bool) → f x ≡ f y
constant f x y = refl

swap : Bool→cBool
swap tt = ff
swap ff = tt
-- swap is definitely not constant, should be rejected

BOOM : tt ≡ ff
BOOM = constant swap ff tt

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2014-05-02
-- Epic issue by Nisse and Andrea Vezzosi

record R : Set₁ where
  field
    A : Set

postulate
  X : R
  x : R.A X

Y : R
Y = X

record S : Set where
  field
    G : R.A Y  -- Works if Y is replaced by X.

s : S
s = record { G = x }

-- This crashed epic with an internal error.

-- Expected behavior now: crash because main is missing.

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Abelian.Instances.Terminal where

open import Cubical.Foundations.Prelude

open import Cubical.Categories.Abelian.Base
open import Cubical.Categories.Additive.Instances.Terminal

open import Cubical.Data.Unit

private
  variable
    ℓ : Level

private
  open PreAbCategory
  open PreAbCategoryStr

  terminalPreAbCategory : PreAbCategory ℓ ℓ
  PreAbCategory.additive terminalPreAbCategory = terminalAdditiveCategory

  Kernel.k (hasKernels (preAbStr terminalPreAbCategory) f) = tt*
  Kernel.ker (hasKernels (preAbStr terminalPreAbCategory) f) = refl
  IsKernel.ker⋆f (Kernel.isKer (hasKernels (preAbStr terminalPreAbCategory) f)) = refl
  IsKernel.univ (Kernel.isKer (hasKernels (preAbStr terminalPreAbCategory) f)) = λ _ _ _ → (refl , refl) , λ _ → refl

  Cokernel.c (hasCokernels (preAbStr terminalPreAbCategory) f) = tt*
  Cokernel.coker (hasCokernels (preAbStr terminalPreAbCategory) f) = refl
  IsCokernel.f⋆coker (Cokernel.isCoker (hasCokernels (preAbStr terminalPreAbCategory) f)) = refl
  IsCokernel.univ (Cokernel.isCoker (hasCokernels (preAbStr terminalPreAbCategory) f)) = λ _ _ _ → (refl , refl) , λ _ → refl

open AbelianCategory
open AbelianCategoryStr

terminalAbelianCategory : AbelianCategory ℓ ℓ
preAb terminalAbelianCategory = terminalPreAbCategory

fst (monNormal (abelianStr terminalAbelianCategory) m _) = tt*
fst (snd (monNormal (abelianStr terminalAbelianCategory) m _)) = m
IsKernel.ker⋆f (snd (snd (monNormal (abelianStr terminalAbelianCategory) m _))) = refl
IsKernel.univ (snd (snd (monNormal (abelianStr terminalAbelianCategory) m _))) = λ _ _ _ → (refl , refl) , (λ _ → refl)

fst (epiNormal (abelianStr terminalAbelianCategory) e _) = tt*
fst (snd (epiNormal (abelianStr terminalAbelianCategory) e _)) = e
IsCokernel.f⋆coker (snd (snd (epiNormal (abelianStr terminalAbelianCategory) e _))) = refl
IsCokernel.univ (snd (snd (epiNormal (abelianStr terminalAbelianCategory) e _))) = λ _ _ _ → (refl , refl) , (λ _ → refl)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical