text:
{-
  Verified Red-Black Trees
        Toon Nolten

  Based on Chris Okasaki's "Red-Black Trees in a Functional Setting"
  where he uses red-black trees to implement sets.

  Invariants
  ----------

  1. No red node has a red parent
  2. Every Path from the root to an empty node contains the same number of
     black nodes.
    (Empty nodes are considered black)
-}
module RedBlackTree where

open import Data.Bool using (Bool; true; false) renaming (T to So; not to ¬)
_⇒_ : ∀{ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set _
P ⇒ T = {{p : P}} → T
infixr 3 _⇒_

if_then_else_ : ∀{ℓ}{A : Set ℓ} b → (So b ⇒ A) → (So (¬ b) ⇒ A) → A
if true  then t else f = t
if false then t else f = f

open import Data.Nat hiding (_<_; _≤_; _≟_; compare)
  renaming (decTotalOrder to ℕ-DTO)
open import Level hiding (suc)
open import Relation.Binary hiding (_⇒_)

open import Data.Sum using (_⊎_) renaming (inj₁ to h+0; inj₂ to h+1)
open import Data.Product using (Σ; Σ-syntax; _,_; proj₁; proj₂)

module RBTree {a ℓ}(order : StrictTotalOrder a ℓ ℓ) where

  open module sto = StrictTotalOrder order
  A = Carrier

  pattern LT = tri< _ _ _
  pattern EQ = tri≈ _ _ _
  pattern GT = tri> _ _ _
  _≤_ = compare

  data Color : Set where
    R B : Color

  _=ᶜ_ : Color → Color → Bool
  R =ᶜ R = true
  B =ᶜ B = true
  _ =ᶜ _ = false

  Height = ℕ

  data Tree : Color → Height → Set a where
    E : Tree B 0
    R : ∀{h} → Tree B h → A → Tree B h → Tree R h
    B : ∀{cl cr h} → Tree cl h → A → Tree cr h → Tree B (suc h)

  data IRTree : Height → Set a where
    IRl : ∀{h} → Tree R h → A → Tree B h → IRTree h
    IRr : ∀{h} → Tree B h → A → Tree R h → IRTree h

  data OutOfBalance : Height → Set a where
    _◂_◂_ : ∀{c h} → IRTree h → A → Tree c h → OutOfBalance h
    _▸_▸_ : ∀{c h} → Tree c h → A → IRTree h → OutOfBalance h

  data Treeish : Color → Height → Set a where
    RB : ∀{c h} → Tree c h → Treeish c h
    IR : ∀{h} → IRTree h → Treeish R h

  -- Insertion

  balance : ∀{h} → OutOfBalance h → Tree R (suc h)
  balance (IRl (R a x b) y c ◂ z ◂ d) = R (B a x b) y (B c z d)
  balance (IRr a x (R b y c) ◂ z ◂ d) = R (B a x b) y (B c z d)
  balance (a ▸ x ▸ IRl (R b y c) z d) = R (B a x b) y (B c z d)
  balance (a ▸ x ▸ IRr b y (R c z d)) = R (B a x b) y (B c z d)

  blacken : ∀{c h} → (Treeish c h)
            → (if c =ᶜ B then Tree B h else Tree B (suc h))
  blacken (RB E) = E
  blacken (RB (R l b r)) = (B l b r)
  blacken (RB (B l b r)) = (B l b r)
  blacken (IR (IRl l b r)) = (B l b r)
  blacken (IR (IRr l b r)) = (B l b r)

  ins : ∀{c h} → (a : A) → (t : Tree c h)
        → Σ[ c' ∈ Color ] (if c =ᶜ B then (Tree c' h) else (Treeish c' h))
  ins a E = R , R E a E
  --
  ins a (R _ b _) with a ≤ b
  ins a (R l _ _) | LT with ins a l
  ins _ (R _ b r) | LT | R , t = R , IR (IRl t b r)
  ins _ (R _ b r) | LT | B , t = R , (RB (R t b r))
  ins _ (R l b r) | EQ = R , RB (R l b r)
  ins a (R _ _ r) | GT with ins a r
  ins _ (R l b _) | GT | R , t = R , (IR (IRr l b t))
  ins _ (R l b _) | GT | B , t = R , (RB (R l b t))
  --
  ins a (B _ b _) with a ≤ b
  ins a (B l _ _) | LT with ins a l
  ins _ (B {R} _ b r) | LT | c , RB t = B , B t b r
  ins _ (B {R} _ b r) | LT | .R , IR t = R , balance (t ◂ b ◂ r)
  ins _ (B {B} _ b r) | LT | c , t = B , B t b r
  ins _ (B l b r) | EQ = B , B l b r
  ins a (B _ _ r) | GT with ins a r
  ins _ (B {cr = R} l b _) | GT | c , RB t = B , B l b t
  ins _ (B {cr = R} l b _) | GT | .R , IR t = R , balance (l ▸ b ▸ t)
  ins _ (B {cr = B} l b _) | GT | c , t = B , B l b t

  insert : ∀{c h} → (a : A) → (t : Tree c h)
           → Tree B h ⊎ Tree B (suc h)
  insert {R} a t with ins a t
  ... | R , t' = h+1 (blacken t')
  ... | B , t' = h+0 (blacken t')
  insert {B} a t with ins a t
  ... | R , t' = h+1 (blacken (RB t'))
  ... | B , t' = h+0 (blacken (RB t'))

  -- Simple Set Operations
  set : ∀{c h} → Set _
  set {c}{h} = Tree c h

  empty : set
  empty = E

  member : ∀{c h} → (a : A) → set {c}{h} → Bool
  member a E = false
  member a (R l b r) with a ≤ b
  ... | LT = member a l
  ... | EQ = true
  ... | GT = member a r
  member a (B l b r) with a ≤ b
  ... | LT = member a l
  ... | EQ = true
  ... | GT = member a r

-- Usage example

open import Relation.Binary.Properties.DecTotalOrder ℕ-DTO
ℕ-STO : StrictTotalOrder _ _ _
ℕ-STO = strictTotalOrder

open module rbtree = RBTree ℕ-STO

t0 : Tree B 2
t0 = B (R (B E 1 E) 2 (B (R E 3 E) 5 (R E 7 E)))
       8
       (B E 9 (R E 10 E))

t1 : Tree B 3
t1 = B (B (B E 1 E) 2 (B E 3 E))
       4
       (B (B E 5 (R E 7 E)) 8 (B E 9 (R E 10 E)))

t2 : Tree B 3
t2 = B (B (B E 1 E) 2 (B E 3 E))
       4
       (B (R (B E 5 E) 6 (B E 7 E)) 8 (B E 9 (R E 10 E)))

open import Relation.Binary.PropositionalEquality
t1≡t0+4 : h+1 t1 ≡ insert 4 t0
t1≡t0+4 = refl

t2≡t1+6 : h+0 t2 ≡ insert 6 t1
t2≡t1+6 = refl

max_stars_repo_name: toonn/sciartt

max_issues_repo_name: toonn/sciartt

max_forks_repo_name: toonn/sciartt


text:
-- Andreas, 2015-03-26

-- Andrea discovered that unfold for Lists is typable with sized types
-- (and termination checks).
-- Dually, fold for Streams should work.  Therefore, the restriction
-- of coinductive records to recursive records should be lifted.

{-# OPTIONS --copatterns #-}

open import Common.Size

-- StreamF A X i = ∀j<i. A × X j
record StreamF (A : Set) (X : Size → Set) (i : Size) : Set where
  coinductive
  field
    head : A
    tail : ∀{j : Size< i} → X j
module F = StreamF

record Stream (A : Set) (i : Size) : Set where
  coinductive
  field
    head : A
    tail : ∀{j : Size< i} → Stream A j
module S = Stream

module Inlined {A T} (f : ∀ i → StreamF A T i → T i) where

  fix : ∀ i → Stream A i → StreamF A T i
  F.head (fix i s)         = S.head s
  F.tail (fix i s) {j = j} = f j (fix j (S.tail s {j = j}))

module Mutual {A T} (f : ∀ i → StreamF A T i → T i) where

 mutual

  fold : ∀ i → Stream A i → T i
  fold i s = f i (h i s)

  h : ∀ i → Stream A i → StreamF A T i
  F.head (h i s) = S.head s
  F.tail (h i s) {j = j} = fold j (S.tail s {j = j})

module Local where

  fold : ∀{A T}
    → (f : ∀ i → StreamF A T i → T i)
    → ∀ i → Stream A i → T i
  fold {A} {T} f i s = f i (h i s)
    where
      h : ∀ i → Stream A i → StreamF A T i
      F.head (h i s) = S.head s
      F.tail (h i s) {j = j} = fold f j (S.tail s {j = j})

-- Unfold for lists

-- ListF A X i = ⊤ + ∃j<i. A × X j
data ListF (A : Set) (X : Size → Set) (i : Size) : Set where
  []  : ListF A X i
  _∷_ : ∀{j : Size< i} (a : A) (xs : X j) → ListF A X i

data List (A : Set) (i : Size) : Set where
  []  : List A i
  _∷_ : ∀{j : Size< i} (a : A) (xs : List A j) → List A i

module With where

  unfold : ∀{A}{S : Size → Set}
    → (f : ∀ i → S i → ListF A S i)
    → ∀ i → S i → List A i
  unfold f i s with f i s
  ... | [] = []
  ... | _∷_ {j = j} a s' = a ∷ unfold f j s'

unfold : ∀{A}{S : Size → Set}
  → (f : ∀ i → S i → ListF A S i)
  → ∀ i → S i → List A i
unfold {A}{S} f i s = aux (f i s)
  where
    aux : ListF A S i → List A i
    aux [] = []
    aux (_∷_ {j = j} a s') = a ∷ unfold f j s'

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Empty {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Introductions.Universe

open import Tools.Unit
open import Tools.Product

-- Validity of the Empty type.
Emptyᵛ : ∀ {Γ l} ([Γ] : ⊩ᵛ Γ) → Γ ⊩ᵛ⟨ l ⟩ Empty / [Γ]
Emptyᵛ [Γ] ⊢Δ [σ] = Emptyᵣ (idRed:*: (Emptyⱼ ⊢Δ)) , λ _ x₂ → id (Emptyⱼ ⊢Δ)

-- Validity of the Empty type as a term.
Emptyᵗᵛ : ∀ {Γ} ([Γ] : ⊩ᵛ Γ)
    → Γ ⊩ᵛ⟨ ¹ ⟩ Empty ∷ U / [Γ] / Uᵛ [Γ]
Emptyᵗᵛ [Γ] ⊢Δ [σ] = let ⊢Empty  = Emptyⱼ ⊢Δ
                         [Empty] = Emptyᵣ (idRed:*: (Emptyⱼ ⊢Δ))
                 in  Uₜ Empty (idRedTerm:*: ⊢Empty) Emptyₙ (≅ₜ-Emptyrefl ⊢Δ) [Empty]
                 ,   (λ x x₁ → Uₜ₌ Empty Empty (idRedTerm:*: ⊢Empty) (idRedTerm:*: ⊢Empty) Emptyₙ Emptyₙ
                                   (≅ₜ-Emptyrefl ⊢Δ) [Empty] [Empty] (id (Emptyⱼ ⊢Δ)))


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommMonoid.Instances.FreeComMonoid where

open import Cubical.Foundations.Prelude
open import Cubical.HITs.FreeComMonoids

open import Cubical.Algebra.CommMonoid.Base

private variable
  ℓ : Level

FCMCommMonoid : {A : Type ℓ} → CommMonoid ℓ
FCMCommMonoid {A = A} = makeCommMonoid {M = FreeComMonoid A} ε _·_ trunc assoc identityᵣ comm

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Reduction where

import Level
open import Data.Empty
open import Data.Unit as Unit
open import Data.Nat
open import Data.List as List renaming ([] to Ø; [_] to [_]L)
open import NonEmptyList as NList
open import Data.Fin hiding (_+_)
open import Data.Vec as Vec renaming ([_] to [_]V; _++_ to _++V_)
open import Data.Product as Prod
open import Function

open import Relation.Binary.PropositionalEquality as PE hiding ([_])
open import Relation.Binary
open ≡-Reasoning

Rel₀ : Set → Set₁
Rel₀ X = Rel X Level.zero

open import Common.Context as Context

open import Algebra
open Monoid {{ ... }} hiding (refl)

open import SyntaxRaw
open import Syntax

-----------------------------------------------------
---- Action of types on terms
-----------------------------------------------------

PreArrow : RawCtx → Set
PreArrow Γ = PreType Ø Γ Ø × PreTerm (∗ ∷ Γ) Ø × PreType Ø Γ Ø

Args : TyCtx → Set
Args Ø = ⊤
Args (Γ ∷ Θ) = PreArrow Γ × (Args Θ)

getArg : ∀ {Θ Γ₁} → TyVar Θ Γ₁ → Args Θ → PreTerm (∗ ∷ Γ₁) Ø
getArg zero        ((_ , t , _) , ts) = t
getArg (succ Γ₁ X) (_           , ts) = getArg X ts

projArgDom : ∀ {Θ} → Args Θ → TyCtxMorP Ø Θ
projArgDom {Ø} a = tt
projArgDom {Γ ∷ Θ} ((A , _) , a) = (Λ A , projArgDom a)

projArgCodom : ∀ {Θ} → Args Θ → TyCtxMorP Ø Θ
projArgCodom {Ø} a = tt
projArgCodom {Γ ∷ Θ} ((_ , _ , B) , a) = (Λ B , projArgDom a)

-- | Extend arguments by the identity on a given type.
extArgs : ∀ {Θ Γ} → Args Θ → PreType Ø Γ Ø → Args (Γ ∷ Θ)
extArgs a A = ((A , varPO zero , A) , a)

-- | Domain of ⟪ A ⟫(φ) for arguments φ : Args Θ.
⟪_⟫₀ : ∀ {Θ Γ₁ Γ₂} →
       PreType Θ Γ₁ Γ₂ → Args Θ → PreType Ø (Γ₂ ++ Γ₁) Ø
⟪_⟫₀ {Γ₁ = Γ₁} {Γ₂} C φ =
  substTy (weakenPT' Γ₂ C) (projArgDom φ) §ₜ ctxProjP' Ø Γ₂ Γ₁

-- | Functorial action of a type A on terms.
-- We are given one term with its types for domain and codomain for each
-- variable in Θ. This is ensured by Args Θ. The result is then a term, which
-- can be thought of as ⟪A⟫(φ) : ⟪A⟫₀(φ) → ⟪A⟫₁(φ).
-- Otherwise, ⟪A⟫ is just defined by induction in A, as in the paper.
-- Note: For now, we have to declare this as non-terminating, as the induction
-- is not obviously terminating for Agda. This should be fixable through sized
-- types.
tyAction : ∀ {Θ Γ₁ Γ₂} →
           (A : Raw Θ Γ₁ Γ₂) → DecentType A → Args Θ → PreTerm (∗ ∷ Γ₂ ++ Γ₁) Ø
tyAction ._ (DT-⊤ Θ Γ)                    ts = varPO zero
tyAction ._ (DT-tyVar Γ₁ X)               ts = weakenPO'' Γ₁ Ø (getArg X ts)
tyAction ._ (DT-inst {Θ} {Γ₁} {Γ₂} {B} A t p q) ts
  = substP (tyAction A p ts) f
  where
    -- | Substitute t for the second variable, i.e., f = (id, t, x).
    f : CtxMorP (∗ ∷ Γ₂ ++ Γ₁) (∗ ∷ Γ₂ ↑ B ++ Γ₁)
    f = subst
        (Vec (PreTerm (∗ ∷ Γ₂ ++ Γ₁) Ø)) -- (CtxMorP (∗ ∷ Γ₂ ++ Γ₁))
        (cong suc r)
        (varPO zero
          ∷ (ctxProjP' [ ∗ ]L Γ₂ Γ₁)
          ++V [ weakenPO' (∗ ∷ Γ₂) (t , q) ]V
          ++V ctxProjP Γ₁ (∗ ∷ Γ₂)
        )
      where
        r : length' Γ₂ + suc (length' Γ₁) ≡ length' (Γ₂ ↑ B ++ Γ₁)
        r =
          begin
            length' Γ₂ + suc (length' Γ₁)
          ≡⟨ refl ⟩
            length' Γ₂ + length' (B ∷ Γ₁)
          ≡⟨ PE.sym (length'-hom Γ₂ (B ∷ Γ₁)) ⟩
            length' (Γ₂ ++ B ∷ Γ₁)
          ≡⟨ mvVar-length Γ₁ Γ₂ B ⟩
            length' (Γ₂ ↑ B ++ Γ₁)
          ∎

tyAction ._ (DT-paramAbstr {Θ} {Γ₂} {B} Γ₁ {A} p) ts =
  subst (λ u → PreTerm u Ø)
        (cong (_∷_ ∗) (mvVar Γ₁ Γ₂ B))
        (tyAction A p ts)

tyAction ._ (DT-fp {Θ} {Γ₂} Γ₁ μ D D-dec) ts
  = weakenPO'' Γ₁ Ø (rec Γ₂ (∗ ∷ Γ₂) (gs D D-dec 0) §ₘ ctxidP (∗ ∷ Γ₂))
  where
    RB : PreType Ø Γ₂ Ø
    RB = subst (λ u → PreType Ø u Ø) (proj₂ identity Γ₂)
               (⟪ fpPT {Θ} {Γ₂} Ø μ (mkFpDataP {D = D} D-dec) ⟫₀ ts)

    -- Construction of gₖ = αₖ id (⟪ Bₖ ⟫ (ts, id))
    mkBase : ∀{Γ'}
             (f : CtxMor Raw Γ' Γ₂) (A : Raw (Γ₂ ∷ Θ) Γ' Ø) →
             DecentCtxMor f →
             DecentType A →
             ℕ →
             Σ RawCtx (λ Γ' →
               PreType [ Γ₂ ]L Γ' Ø
               × CtxMorP Γ' Γ₂
               × PreTerm (∗ ∷ Γ') Ø)
    mkBase {Γ'} g M g-dec M-dec k
      = (Γ' , C , mkCtxMorP g-dec , αₖ §ₘ r)
      where
        A : PreType (Γ₂ ∷ Θ) Γ' Ø
        A = mkPreType M-dec

        αₖ : PreTerm (∗ ∷ Γ') (∗ ∷ Γ')
        αₖ = α _ Γ' ∗ k

        r : CtxMorP (∗ ∷ Γ') (∗ ∷ Γ')
        r = tyAction M M-dec (extArgs ts RB) ∷ ctxProjP Γ' [ ∗ ]L

        C : PreType [ Γ₂ ]L Γ' Ø
        C = substTy A (tyVarPT Ø zero , weakenTyCtxMor₁ Γ₂ (projArgDom ts))

    -- Construct the g₁, ..., gₙ used in the recursion
    gs : (D : FpData Raw Θ Γ₂) → DecentFpData D → ℕ → FpMapDataP Γ₂
    gs [ Γ' , f , M ] (f-dec , M-dec) k
      = [ mkBase f M f-dec M-dec k ]
    gs ((Γ' , f , M) ∷ D) ((f-dec , M-dec) , D-dec) k
      = mkBase f M f-dec M-dec k ∷ gs D D-dec (suc k)

tyAction ._ (DT-fp {Θ} {Γ₂} Γ₁ ν D D-dec) ts
  = weakenPO'' Γ₁ Ø (corec Γ₂ (∗ ∷ Γ₂) (gs D D-dec 0) §ₘ ctxidP (∗ ∷ Γ₂))
  where
    -- Construction of gₖ = αₖ id (⟪ Bₖ ⟫ (ts, id))
    mkBase : ∀{Γ'} (x : CtxMor Raw Γ' Γ₂ × Raw (Γ₂ ∷ Θ) Γ' Ø) →
             (f : DecentCtxMor (proj₁ x)) →
             (q : DecentType (proj₂ x)) →
             ℕ →
             Σ RawCtx (λ Γ' →
               PreType [ Γ₂ ]L Γ' Ø
               × CtxMorP Γ' Γ₂
               × PreTerm (∗ ∷ Γ') Ø)
    mkBase {Γ'} (g , M) g-dec M-dec k = (Γ' , C , mkCtxMorP g-dec , f)
      where
        A : PreType (Γ₂ ∷ Θ) Γ' Ø
        A = mkPreType M-dec

        ξₖ : PreTerm (∗ ∷ Γ') (∗ ∷ Γ')
        ξₖ = ξ _ Γ' ∗ k

        RA : PreType Ø Γ₂ Ø
        RA = subst (λ u → PreType Ø u Ø) (proj₂ identity Γ₂)
             (⟪ fpPT {Θ} {Γ₂} Ø μ (mkFpDataP {D = D} D-dec) ⟫₀ ts)

        f : PreTerm (∗ ∷ Γ') Ø
        f = substPO (tyAction M M-dec (extArgs ts RA))
                    ((ξₖ §ₘ ctxidP (∗ ∷ Γ')) ∷ weakenCtxMorP (ctxidP Γ'))

        C : PreType [ Γ₂ ]L Γ' Ø
        C = substTy A (tyVarPT Ø zero , weakenTyCtxMor₁ Γ₂ (projArgDom ts))

    -- Construct the g₁, ..., gₙ used in the recursion
    gs : (D : FpData Raw Θ Γ₂) → DecentFpData D → ℕ → FpMapDataP Γ₂
    gs [ Γ' , x ] (f , p) k = [ mkBase x f p k ]
    gs ((Γ' , x) ∷ D₁) ((f , q) , p₁) k = mkBase x f q k ∷ gs D₁ p₁ (suc k)

⟪_⟫ : ∀ {Θ Γ₁ Γ₂} →
      PreType Θ Γ₁ Γ₂ → Args Θ → PreTerm (∗ ∷ Γ₂ ++ Γ₁) Ø
⟪ A , A-dec ⟫ = tyAction A A-dec

-----------------------------------------------------
---- Reduction relation on pre-types and pre-terms
-----------------------------------------------------

getRecCtx : ∀{Γ} → (D : FpMapDataP Γ) → Pos D → RawCtx
getRecCtx [ x ]   _       = proj₁ x
getRecCtx (x ∷ D) zero    = proj₁ x
getRecCtx (x ∷ D) (suc p) = getRecCtx D p

getRecMor : ∀{Γ} (D : FpMapDataP Γ) (p : Pos D) →
            PreTerm (∗ ∷ getRecCtx D p) Ø
getRecMor [ Γ' , A , f , t ]      _       = t
getRecMor ((Γ' , A , f , t) ∷ D) zero    = t
getRecMor (x ∷ D)                (suc p) = getRecMor D p

getRecTy : ∀{Γ} (D : FpMapDataP Γ) (p : Pos D) →
           PreType [ Γ ]L (getRecCtx D p) Ø
getRecTy [ x ]   _       = proj₁ (proj₂ x)
getRecTy (x ∷ D) zero    = proj₁ (proj₂ x)
getRecTy (x ∷ D) (suc p) = getRecTy D p

getRecSubst : ∀{Γ} (D : FpMapDataP Γ) (p : Pos D) →
              CtxMorP (getRecCtx D p) Γ
getRecSubst [ Γ' , A , f , t ]     _       = f
getRecSubst ((Γ' , A , f , t) ∷ D) zero    = f
getRecSubst (x ∷ D)                (suc p) = getRecSubst D p

infix 0 _≻_

-- | Contraction for terms
data _≻_  : {Γ₁ Γ₂ : RawCtx} → PreTerm Γ₁ Γ₂ → PreTerm Γ₁ Γ₂ → Set where
  contract-iter : (Γ Δ : RawCtx) (D : FpMapDataP Γ) (C : PreType Ø Ø Γ)
                  (p : Pos D)
                  (τ : CtxMorP Δ (getRecCtx D p))
                  (u : PreTerm Δ Ø) →
                rec Γ Δ D §ₘ
                  (α Δ (getRecCtx D p) ∗ (toℕ p) §ₘ' τ §ₒ u)
                  ∷ getRecSubst D p • τ
                ≻ (getRecMor D p)
                  ↓[ (⟪ getRecTy D p ⟫ (
                        ( fpPT Γ μ (getFpData D) §ₜ ctxidP Γ
                        , rec Γ (∗ ∷ Γ) D §ₘ ctxidP _
                        , (weakenPT'' Γ C) §ₜ ctxidP Γ)
                        , tt))
                     ∷ ctxProjP (getRecCtx D p) [ ∗ ]L ]
                  ↓[ u ∷ τ ]
  contract-coiter : (Γ Δ : RawCtx) (D : FpMapDataP Γ) (C : PreType Ø Ø Γ)
                    (p : Pos D)
                    (τ : CtxMorP Δ (getRecCtx D p))
                    (u : PreTerm Δ Ø) →
                    ξ Δ (getRecCtx D p) ∗ (toℕ p)
                      §ₘ' τ
                      §ₒ corec Γ Δ D §ₘ u ∷ (getRecSubst D p • τ)
                    ≻ (⟪ getRecTy D p ⟫ (
                         (weakenPT'' Γ C §ₜ ctxidP Γ
                         , corec Γ (∗ ∷ Γ) D §ₘ ctxidP _
                         , fpPT Γ ν (getFpData D) §ₜ ctxidP Γ)
                      , tt)
                      ↓[ (getRecMor D p) ∷ ctxProjP (getRecCtx D p) [ ∗ ]L ])
                      ↓[ u ∷ τ ]

-- | Lift term reduction to fixed point data
data _∼>_ : {Γ : RawCtx} → Rel₀ (FpMapDataP Γ)

-- | Compatible closure of contraction
data _⟶_ : {Γ₁ Γ₂ : RawCtx} → Rel₀ (PreTerm Γ₁ Γ₂) where
  contract : {Γ₁ Γ₂ : RawCtx} (t₁ t₂ : PreTerm Γ₁ Γ₂) → t₁ ≻ t₂ → t₁ ⟶ t₂

  inst-clos₁ : ∀ {Γ₁ Γ₂ A} (s₁ s₂ : PreTerm Γ₁ (Γ₂ ↑ A)) (t : PreTerm Γ₁ Ø) →
               s₁ ⟶ s₂ → instPO {Γ₁} {Γ₂} s₁ t ⟶ instPO s₂ t

  inst-clos₂ : ∀ {Γ₁ Γ₂ A} (s : PreTerm Γ₁ (Γ₂ ↑ A)) (t₁ t₂ : PreTerm Γ₁ Ø) →
               t₁ ⟶ t₂ → instPO {Γ₁} {Γ₂} s t₂ ⟶ instPO s t₂

  grec-clos : (Γ : RawCtx) (Δ : RawCtx) (D D' : FpMapDataP Γ) (ρ : FP) →
              D ∼> D' → grec Γ Δ D ρ ⟶ grec Γ Δ D' ρ

data _∼>_ where
  single-clos : {Γ : RawCtx} (Γ' : RawCtx) (A : PreType [ Γ ]L Γ' Ø)
                (f : CtxMorP Γ' Γ) (M₁ M₂ : PreTerm (∗ ∷ Γ') Ø) →
                M₁ ⟶ M₂ → [ Γ' , A , f , M₁ ] ∼> [ Γ' , A , f , M₂ ]

  step-clos₁ : {Γ : RawCtx} (Γ' : RawCtx) (A : PreType [ Γ ]L Γ' Ø)
               (f : CtxMorP Γ' Γ) (M₁ M₂ : PreTerm (∗ ∷ Γ') Ø)
               (D : FpMapDataP Γ) →
               M₁ ⟶ M₂ → ((Γ' , A , f , M₁) ∷ D) ∼> ((Γ' , A , f , M₂) ∷ D)

  step-clos₂ : {Γ : RawCtx} (Γ' : RawCtx) (A : PreType [ Γ ]L Γ' Ø)
               (f : CtxMorP Γ' Γ) (M : PreTerm (∗ ∷ Γ') Ø)
               (D₁ D₂ : FpMapDataP Γ) →
               D₁ ∼> D₂ → ((Γ' , A , f , M) ∷ D₁) ∼> ((Γ' , A , f , M) ∷ D₂)

-- | β-reduction for parameter abstraction/instantiation
data _⟶ₚ_ : {Θ : TyCtx} {Γ₁ Γ₂ : RawCtx} → Rel₀ (PreType Θ Γ₁ Γ₂) where
     β-red : {Θ : TyCtx} {Γ₂ : RawCtx} (Γ₁ : RawCtx) {A : U}
             (B : PreType Θ (A ∷ Γ₁) Γ₂) (t : PreTerm Γ₁ Ø) →
             instPT (paramAbstrPT Γ₁ B) t ⟶ₚ substPT B (t ∷ (ctxidP Γ₁))

-- | Lift type reductions to fixed point data
data _∼>ₜ_ : {Θ : TyCtx} {Γ : RawCtx} → Rel₀ (FpDataP Θ Γ)

-- | Reduction on types. This is either a β-reduction for parameters,
-- a reduction of a term in parameter position, or it happens through
-- the compatible closure.
data _⟶ₜ_ : {Θ : TyCtx} {Γ₁ Γ₂ : RawCtx} → Rel₀ (PreType Θ Γ₁ Γ₂) where
     param-conv : ∀ {Θ Γ₁ Γ₂ A}
                  (B : PreType Θ Γ₁ (Γ₂ ↑ A)) (t₁ t₂ : PreTerm Γ₁ Ø) →
                  t₁ ⟶ t₂ → instPT {Γ₂ = Γ₂} B t₁ ⟶ₜ instPT B t₂

     inst-conv : {Θ : TyCtx} {Γ₁ Γ₂ : RawCtx} → (A₁ A₂ : PreType Θ Γ₁ Γ₂) →
                 A₁ ⟶ₚ A₂ → A₁ ⟶ₜ A₂

     instPT-clos : ∀ {Θ Γ₁ Γ₂ A}
                  (B₁ B₂ : PreType Θ Γ₁ (Γ₂ ↑ A)) (t : PreTerm Γ₁ Ø) →
                  B₁ ⟶ₜ B₂ → instPT {Γ₂ = Γ₂} B₁ t ⟶ₜ instPT B₂ t

     paramAbstr-clos : {Θ : TyCtx} {Γ₂ : RawCtx} (Γ₁ : RawCtx) {A : U} →
                       (B₁ B₂ : PreType Θ (A ∷ Γ₁) Γ₂) →
                       B₁ ⟶ₜ B₂ → paramAbstrPT Γ₁ B₁ ⟶ₜ paramAbstrPT Γ₁ B₂

     fp-clos : {Θ : TyCtx} {Γ₂ : RawCtx} (Γ₁ : RawCtx) →
               (ρ : FP) (D₁ D₂ : FpDataP Θ Γ₂) →
               D₁ ∼>ₜ D₂ → fpPT Γ₁ ρ D₁ ⟶ₜ fpPT Γ₁ ρ D₂

data _∼>ₜ_ where
  singlePT-clos : {Θ : TyCtx} {Γ : RawCtx}
    (Γ' : RawCtx) (f : CtxMorP Γ' Γ) (A₁ A₂ : PreType (Γ ∷ Θ) Γ' Ø) →
    A₁ ⟶ₜ A₂ → [ Γ' , f , A₁ ] ∼>ₜ [ Γ' , f , A₂ ]

  stepPT-clos₁ : {Θ : TyCtx} {Γ : RawCtx}
    (Γ' : RawCtx) (f : CtxMorP Γ' Γ) (A₁ A₂ : PreType (Γ ∷ Θ) Γ' Ø)
    (D : FpDataP Θ Γ) →
    A₁ ⟶ₜ A₂ -> ((Γ' , f , A₁) ∷ D) ∼>ₜ ((Γ' , f , A₂) ∷ D)

  stepPT-clos₂ : {Θ : TyCtx} {Γ : RawCtx}
    (Γ' : RawCtx) (f : CtxMorP Γ' Γ) (A : PreType (Γ ∷ Θ) Γ' Ø)
    (D₁ D₂ : FpDataP Θ Γ) →
    D₁ ∼>ₜ D₂ -> ((Γ' , f , A) ∷ D₁) ∼>ₜ ((Γ' , f , A) ∷ D₂)

max_stars_repo_name: StillerHarpo/CoindDepTypes

max_issues_repo_name: StillerHarpo/CoindDepTypes

max_forks_repo_name: StillerHarpo/CoindDepTypes


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Nat.GCD where

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

open import Cubical.Induction.WellFounded

open import Cubical.Data.Fin
open import Cubical.Data.Sigma as Σ
open import Cubical.Data.NatPlusOne

open import Cubical.HITs.PropositionalTruncation as PropTrunc

open import Cubical.Data.Nat.Base
open import Cubical.Data.Nat.Properties
open import Cubical.Data.Nat.Order
open import Cubical.Data.Nat.Divisibility

private
  variable
    m n d : ℕ

-- common divisors

isCD : ℕ → ℕ → ℕ → Type₀
isCD m n d = (d ∣ m) × (d ∣ n)

isPropIsCD : isProp (isCD m n d)
isPropIsCD = isProp× isProp∣ isProp∣

symCD : isCD m n d → isCD n m d
symCD (d∣m , d∣n) = (d∣n , d∣m)

-- greatest common divisors

isGCD : ℕ → ℕ → ℕ → Type₀
isGCD m n d = (isCD m n d) × (∀ d' → isCD m n d' → d' ∣ d)

GCD : ℕ → ℕ → Type₀
GCD m n = Σ ℕ (isGCD m n)

isPropIsGCD : isProp (isGCD m n d)
isPropIsGCD = isProp× isPropIsCD (isPropΠ2 (λ _ _ → isProp∣))

isPropGCD : isProp (GCD m n)
isPropGCD (d , dCD , gr) (d' , d'CD , gr') =
  ΣProp≡ (λ _ → isPropIsGCD) (antisym∣ (gr' d dCD) (gr d' d'CD))

symGCD : isGCD m n d → isGCD n m d
symGCD (dCD , gr) = symCD dCD , λ { d' d'CD → gr d' (symCD d'CD) }

divsGCD : m ∣ n → isGCD m n m
divsGCD p = (∣-refl refl , p) , λ { d (d∣m , _) → d∣m }

-- The base case of the Euclidean algorithm
zeroGCD : ∀ m → isGCD m 0 m
zeroGCD m = divsGCD (∣-zeroʳ m)

private
  lem₁ : prediv d (suc n) → prediv d (m % suc n) → prediv d m
  lem₁ {d} {n} {m} (c₁ , p₁) (c₂ , p₂) = (q * c₁ + c₂) , p
    where r = m % suc n; q = n%k≡n[modk] m (suc n) .fst
          p = (q * c₁ + c₂) * d     ≡⟨ sym (*-distribʳ (q * c₁) c₂ d) ⟩
              (q * c₁) * d + c₂ * d ≡⟨ cong (_+ c₂ * d) (sym (*-assoc q c₁ d))  ⟩
              q * (c₁ * d) + c₂ * d ≡[ i ]⟨ q * (p₁ i) + (p₂ i) ⟩
              q * (suc n)  + r      ≡⟨ n%k≡n[modk] m (suc n) .snd ⟩
              m                     ∎

  lem₂ : prediv d (suc n) → prediv d m → prediv d (m % suc n)
  lem₂ {d} {n} {m} (c₁ , p₁) (c₂ , p₂) = c₂ ∸ q * c₁ , p
    where r = m % suc n; q = n%k≡n[modk] m (suc n) .fst
          p = (c₂ ∸ q * c₁) * d               ≡⟨ ∸-distribʳ c₂ (q * c₁) d ⟩
              c₂ * d ∸ (q * c₁) * d           ≡⟨ cong (c₂ * d ∸_) (sym (*-assoc q c₁ d)) ⟩
              c₂ * d ∸ q * (c₁ * d)           ≡[ i ]⟨ p₂ i ∸ q * (p₁ i) ⟩
              m      ∸ q * (suc n)            ≡⟨ cong (_∸ q * (suc n)) (sym (n%k≡n[modk] m (suc n) .snd)) ⟩
              (q * (suc n) + r) ∸ q * (suc n) ≡⟨ cong (_∸ q * (suc n)) (+-comm (q * (suc n)) r) ⟩
              (r + q * (suc n)) ∸ q * (suc n) ≡⟨ ∸-cancelʳ r zero (q * (suc n)) ⟩
              r ∎

-- The inductive step of the Euclidean algorithm
stepGCD : isGCD (suc n) (m % suc n) d
        → isGCD m       (suc n)     d
fst (stepGCD ((d∣n , d∣m%n) , gr)) = PropTrunc.map2 lem₁ d∣n d∣m%n , d∣n
snd (stepGCD ((d∣n , d∣m%n) , gr)) d' (d'∣m , d'∣n) = gr d' (d'∣n , PropTrunc.map2 lem₂ d'∣n d'∣m)

-- putting it all together using well-founded induction

euclid< : ∀ m n → n < m → GCD m n
euclid< = WFI.induction <-wellfounded λ {
  m rec zero    p → m , zeroGCD m ;
  m rec (suc n) p → let d , dGCD = rec (suc n) p (m % suc n) (n%sk<sk m n)
                     in d , stepGCD dGCD }

euclid : ∀ m n → GCD m n
euclid m n with n ≟ m
... | lt p = euclid< m n p
... | gt p = Σ.mapʳ symGCD (euclid< n m p)
... | eq p = m , divsGCD (∣-refl (sym p))

isContrGCD : ∀ m n → isContr (GCD m n)
isContrGCD m n = euclid m n , isPropGCD _

-- the gcd operator on ℕ

gcd : ℕ → ℕ → ℕ
gcd m n = euclid m n .fst

gcdIsGCD : ∀ m n → isGCD m n (gcd m n)
gcdIsGCD m n = euclid m n .snd


text:
open import Oscar.Prelude
open import Oscar.Class.HasEquivalence
import Oscar.Data.Constraint

module Oscar.Data.ProductIndexEquivalence where

module _ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} {ℓ} ⦃ _ : HasEquivalence 𝔒 ℓ ⦄  where

  record _≈₀_ (P Q : Σ 𝔒 𝔓) : Ø ℓ where
    constructor ∁
    field
      π₀ : π₀ P ≈ π₀ Q

  open _≈₀_ public

module _ {𝔬} (𝔒 : Ø 𝔬) {𝔭} (𝔓 : 𝔒 → Ø 𝔭) {ℓ} ⦃ _ : HasEquivalence 𝔒 ℓ ⦄  where

  ProductIndexEquivalence⟦_/_⟧ : (P Q : Σ 𝔒 𝔓) → Ø ℓ
  ProductIndexEquivalence⟦_/_⟧ = _≈₀_


text:
-- https://www.codewars.com/kata/50654ddff44f800200000004

{-# OPTIONS --safe #-}
module Solution where

open import Data.Nat

multiply : ℕ → ℕ → ℕ
multiply a b = a * b

max_stars_repo_name: hiljusti/codewars-solutions

max_issues_repo_name: hiljusti/codewars-solutions

max_forks_repo_name: hiljusti/codewars-solutions


text:
module Channel where

open import Data.Bool hiding (_≤_)
open import Data.Fin hiding (_≤_)
open import Data.List hiding (map)
open import Data.Maybe
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product hiding (map)
open import Relation.Binary.PropositionalEquality

open import Typing
open import Syntax hiding (send ; recv)
open import Global

data ChannelEnd : Set where
  POS NEG : ChannelEnd

otherEnd : ChannelEnd → ChannelEnd
otherEnd POS = NEG
otherEnd NEG = POS

-- the main part of a channel endpoint value is a valid channel reference
-- the channel end determines whether it's the front end or the back end of the channel
-- enforces that the session context has only one channel
data ChannelRef : (G : SCtx) (ce : ChannelEnd) (s : STypeF SType) → Set where
  here-pos : ∀ {s s'} {G : SCtx}
    → (ina-G : Inactive G)
    → s ≲' s'
    → ChannelRef (just (s , POS) ∷ G) POS s'
  here-neg : ∀ {s s'} {G : SCtx}
    → (ina-G : Inactive G)
    → dualF s ≲' s'
    → ChannelRef (just (s , NEG) ∷ G) NEG s'
  there : ∀ {b s} {G : SCtx}
    → (vcr : ChannelRef G b s)
    → ChannelRef (nothing ∷ G) b s

-- coerce channel ref to a supertype
vcr-coerce : ∀ {G b s s'} → ChannelRef G b s → s ≲' s' → ChannelRef G b s'
vcr-coerce (here-pos ina-G x) s≤s' = here-pos ina-G (subF-trans x s≤s')
vcr-coerce (here-neg ina-G x) s≤s' = here-neg ina-G (subF-trans x s≤s')
vcr-coerce (there vcr) s≤s' = there (vcr-coerce vcr s≤s')

-- find matching wait instruction in thread pool
vcr-match : ∀ {G G₁ G₂ b₁ b₂ s₁ s₂}
  → SSplit G G₁ G₂
  → ChannelRef G₁ b₁ s₁
  → ChannelRef G₂ b₂ s₂
  → Maybe (b₁ ≡ otherEnd b₂ × dualF s₂ ≲' s₁)
vcr-match () (here-pos _ _) (here-pos _ _)
vcr-match (ss-posneg ss) (here-pos{s} ina-G s<=s') (here-neg ina-G₁ ds<=s'') = just (refl , subF-trans (dual-subF ds<=s'') (subF-trans (eqF-implies-subF (eqF-sym (dual-involutionF s))) s<=s'))
vcr-match (ss-left ss) (here-pos _ _) (there vcr2) = nothing
vcr-match (ss-negpos ss) (here-neg ina-G ds<=s') (here-pos ina-G₁ s<=s'') = just (refl , subF-trans (dual-subF s<=s'') ds<=s')
vcr-match (ss-left ss) (here-neg _ _) (there vcr2) = nothing
vcr-match (ss-right ss) (there vcr1) (here-pos _ ina-G) = nothing
vcr-match (ss-right ss) (there vcr1) (here-neg _ ina-G) = nothing
vcr-match (ss-both ss) (there vcr1) (there vcr2) = vcr-match ss vcr1 vcr2

-- ok. brute force for a fixed tree with three levels
data SSplit2 (G G₁ G₂ G₁₁ G₁₂ : SCtx) : Set where
  ssplit2 :
    (ss1 : SSplit G G₁ G₂)
    → (ss2 : SSplit G₁ G₁₁ G₁₂)
    → SSplit2 G G₁ G₂ G₁₁ G₁₂

vcr-match-2-sr : ∀ {G G₁ G₂ G₁₁ G₁₂ b₁ b₂ s₁ s₂ t₁ t₂}
  → SSplit2 G G₁ G₂ G₁₁ G₁₂
  → ChannelRef G₁₁ b₁ (recv t₁ s₁)
  → ChannelRef G₁₂ b₂ (send t₂ s₂)
  → Maybe (SubT t₂ t₁ × dual s₂ ≲ s₁ ×
          ∃ λ G' → ∃ λ G₁' → ∃ λ G₁₁' → ∃ λ G₁₂' →
          SSplit2 G' G₁' G₂ G₁₁' G₁₂' ×
          ChannelRef G₁₁' b₁ (SType.force s₁) ×
          ChannelRef G₁₂' b₂ (SType.force s₂))
vcr-match-2-sr (ssplit2 ss-[] ()) (here-pos ina-G x) (here-pos ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-both ss1) ()) (here-pos ina-G x) (here-pos ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-left ss1) ()) (here-pos ina-G x) (here-pos ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-right ss1) ()) (here-pos ina-G x) (here-pos ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-posneg ss1) ()) (here-pos ina-G x) (here-pos ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-negpos ss1) ()) (here-pos ina-G x) (here-pos ina-G₁ x₁)
vcr-match-2-sr (ssplit2 ss-[] ()) (here-pos ina-G x) (here-neg ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-both ss1) ()) (here-pos ina-G x) (here-neg ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-left ss1) (ss-posneg ss2)) (here-pos ina-G (sub-recv{s1} t t' t<=t' s1<=s1')) (here-neg ina-G₁ (sub-send .t t'' t'<=t s1<=s1'')) = just ((subt-trans t'<=t t<=t') , (sub-trans (dual-sub s1<=s1'') (sub-trans (eq-implies-sub (eq-sym (dual-involution s1))) s1<=s1')) , _ , _ , _ , _ , ssplit2 (ss-left ss1) (ss-posneg ss2) , here-pos ina-G (Sub.force s1<=s1') , here-neg ina-G₁ (Sub.force s1<=s1''))
vcr-match-2-sr (ssplit2 (ss-right ss1) ()) (here-pos ina-G x) (here-neg ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-posneg ss1) ()) (here-pos ina-G x) (here-neg ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-negpos ss1) ()) (here-pos ina-G x) (here-neg ina-G₁ x₁)
vcr-match-2-sr (ssplit2 ss-[] ()) (here-pos ina-G x) (there vcr2)
vcr-match-2-sr (ssplit2 (ss-both ss1) ()) (here-pos ina-G x) (there vcr2)
vcr-match-2-sr (ssplit2 (ss-left ss1) (ss-left ss2)) (here-pos ina-G x) (there vcr2) = nothing
vcr-match-2-sr (ssplit2 (ss-right ss1) ()) (here-pos ina-G x) (there vcr2)
vcr-match-2-sr (ssplit2 (ss-posneg ss1) (ss-left ss2)) (here-pos ina-G x) (there vcr2) = nothing
vcr-match-2-sr (ssplit2 (ss-negpos ss1) ()) (here-pos ina-G x) (there vcr2)
vcr-match-2-sr (ssplit2 ss-[] ()) (here-neg ina-G x) (here-pos ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-both ss1) ()) (here-neg ina-G x) (here-pos ina-G₁ x₁)
vcr-match-2-sr {s₁ = s₁} {s₂} (ssplit2 (ss-left ss1) (ss-negpos ss2)) (here-neg ina-G (sub-recv .t t'' t<=t' s1<=s1'')) (here-pos ina-G₁ (sub-send t t' t'<=t s1<=s1')) = just ((subt-trans t'<=t t<=t') , ((sub-trans (dual-sub s1<=s1') s1<=s1'') , (_ , (_ , (_ , (_ , ((ssplit2 (ss-left ss1) (ss-negpos ss2)) , ((here-neg ina-G (Sub.force s1<=s1'')) , (here-pos ina-G₁ (Sub.force s1<=s1'))))))))))
vcr-match-2-sr (ssplit2 (ss-right ss1) ()) (here-neg ina-G x) (here-pos ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-posneg ss1) ()) (here-neg ina-G x) (here-pos ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-negpos ss1) ()) (here-neg ina-G x) (here-pos ina-G₁ x₁)
vcr-match-2-sr (ssplit2 ss-[] ()) (here-neg ina-G x) (here-neg ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-both ss1) ()) (here-neg ina-G x) (here-neg ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-right ss1) ()) (here-neg ina-G x) (here-neg ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-posneg ss1) ()) (here-neg ina-G x) (here-neg ina-G₁ x₁)
vcr-match-2-sr (ssplit2 (ss-negpos ss1) ()) (here-neg ina-G x) (here-neg ina-G₁ x₁)
vcr-match-2-sr (ssplit2 ss-[] ()) (here-neg ina-G x) (there vcr2)
vcr-match-2-sr (ssplit2 (ss-both ss1) ()) (here-neg ina-G x) (there vcr2)
vcr-match-2-sr (ssplit2 (ss-left ss1) (ss-left ss2)) (here-neg ina-G x) (there vcr2) = nothing
vcr-match-2-sr (ssplit2 (ss-right ss1) ()) (here-neg ina-G x) (there vcr2)
vcr-match-2-sr (ssplit2 (ss-posneg ss1) ()) (here-neg ina-G x) (there vcr2)
vcr-match-2-sr (ssplit2 (ss-negpos ss1) (ss-left ss2)) (here-neg ina-G x) (there vcr2) = nothing
vcr-match-2-sr (ssplit2 ss-[] ()) (there vcr1) (here-pos ina-G x)
vcr-match-2-sr (ssplit2 (ss-both ss1) ()) (there vcr1) (here-pos ina-G x)
vcr-match-2-sr (ssplit2 (ss-left ss1) (ss-right ss2)) (there vcr1) (here-pos ina-G x) = nothing
vcr-match-2-sr (ssplit2 (ss-right ss1) ()) (there vcr1) (here-pos ina-G x)
vcr-match-2-sr (ssplit2 (ss-posneg ss1) (ss-right ss2)) (there vcr1) (here-pos ina-G x) = nothing
vcr-match-2-sr (ssplit2 (ss-negpos ss1) ()) (there vcr1) (here-pos ina-G x)
vcr-match-2-sr (ssplit2 ss-[] ()) (there vcr1) (here-neg ina-G x)
vcr-match-2-sr (ssplit2 (ss-both ss1) ()) (there vcr1) (here-neg ina-G x)
vcr-match-2-sr (ssplit2 (ss-left ss1) (ss-right ss2)) (there vcr1) (here-neg ina-G x) = nothing
vcr-match-2-sr (ssplit2 (ss-right ss1) ()) (there vcr1) (here-neg ina-G x)
vcr-match-2-sr (ssplit2 (ss-negpos ss1) (ss-right ss2)) (there vcr1) (here-neg ina-G x) = nothing
vcr-match-2-sr (ssplit2 ss-[] ()) (there vcr1) (there vcr2)
vcr-match-2-sr (ssplit2 (ss-both ss1) (ss-both ss2)) (there vcr1) (there vcr2) with vcr-match-2-sr (ssplit2 ss1 ss2) vcr1 vcr2
... | nothing = nothing
... | just (t2<=t1 , ds2<=s1 , _ , _ , _ , _ , ssplit2 ss1' ss2' , vcr1' , vcr2') = just (t2<=t1 , ds2<=s1 , _ , _ , _ , _ , (ssplit2 (ss-both ss1') (ss-both ss2')) , ((there vcr1') , (there vcr2')))
vcr-match-2-sr (ssplit2 (ss-right ss1) (ss-both ss2)) (there vcr1) (there vcr2) = map (λ { (t2<=t1 , ds2<=s1 , _ , _ , _ , _ , ssplit2 ss1' ss2' , vcr1' , vcr2') → t2<=t1 , ds2<=s1 , _ , _ , _ , _ , (ssplit2 (ss-right ss1') (ss-both ss2')) , (there vcr1') , (there vcr2') }) (vcr-match-2-sr (ssplit2 ss1 ss2) vcr1 vcr2)
vcr-match-2-sr (ssplit2 (ss-negpos ss1) ()) (there vcr1) (there vcr2)

vcr-match-2-sb : ∀ {G G₁ G₂ G₁₁ G₁₂ b₁ b₂ s₁₁ s₁₂ s₂₁ s₂₂}
  → SSplit2 G G₁ G₂ G₁₁ G₁₂
  → ChannelRef G₁₁ b₁ (sintern s₁₁ s₁₂)
  → ChannelRef G₁₂ b₂ (sextern s₂₁ s₂₂)
  → (lab : Selector)
  → Maybe (dual s₂₁ ≲ s₁₁ × dual s₂₂ ≲ s₁₂ ×
          ∃ λ G' → ∃ λ G₁' → ∃ λ G₁₁' → ∃ λ G₁₂' →
          SSplit2 G' G₁' G₂ G₁₁' G₁₂' ×
          ChannelRef G₁₁' b₁ (selection lab (SType.force s₁₁) (SType.force s₁₂)) ×
          ChannelRef G₁₂' b₂ (selection lab (SType.force s₂₁) (SType.force s₂₂)))
vcr-match-2-sb (ssplit2 ss1 ss2) (here-pos ina-G (sub-sintern s1<=s1' s2<=s2')) (here-pos ina-G₁ (sub-sextern s1<=s1'' s2<=s2'')) lab = nothing
vcr-match-2-sb (ssplit2 ss-[] ()) (here-pos ina-G (sub-sintern s1<=s1' s2<=s2')) (here-neg ina-G₁ x₁) lab
vcr-match-2-sb (ssplit2 (ss-both ss1) ()) (here-pos ina-G (sub-sintern s1<=s1' s2<=s2')) (here-neg ina-G₁ x₁) lab
vcr-match-2-sb (ssplit2 (ss-left ss1) (ss-posneg ss2)) (here-pos ina-G (sub-sintern s1<=s1' s2<=s2')) (here-neg ina-G₁ (sub-sextern s1<=s1'' s2<=s2'')) Left = just ((sub-trans (dual-sub s1<=s1'') (sub-trans (eq-implies-sub (eq-sym (dual-involution _))) s1<=s1')) , (sub-trans (dual-sub s2<=s2'') (sub-trans (eq-implies-sub (eq-sym (dual-involution _))) s2<=s2')) , _ , _ , _ , _ , (ssplit2 (ss-left ss1) (ss-posneg ss2)) , (here-pos ina-G (Sub.force s1<=s1')) , (here-neg ina-G₁ (Sub.force s1<=s1'')))
vcr-match-2-sb (ssplit2 (ss-left ss1) (ss-posneg ss2)) (here-pos ina-G (sub-sintern s1<=s1' s2<=s2')) (here-neg ina-G₁ (sub-sextern s1<=s1'' s2<=s2'')) Right = just ((sub-trans (dual-sub s1<=s1'') (sub-trans (eq-implies-sub (eq-sym (dual-involution _))) s1<=s1')) , (sub-trans (dual-sub s2<=s2'') (sub-trans (eq-implies-sub (eq-sym (dual-involution _))) s2<=s2')) , _ , _ , _ , _ , (ssplit2 (ss-left ss1) (ss-posneg ss2)) , (here-pos ina-G (Sub.force s2<=s2')) , (here-neg ina-G₁ (Sub.force s2<=s2'')))
vcr-match-2-sb (ssplit2 (ss-right ss1) ()) (here-pos ina-G (sub-sintern s1<=s1' s2<=s2')) (here-neg ina-G₁ x₁) lab
vcr-match-2-sb (ssplit2 (ss-posneg ss1) ()) (here-pos ina-G (sub-sintern s1<=s1' s2<=s2')) (here-neg ina-G₁ x₁) lab
vcr-match-2-sb (ssplit2 (ss-negpos ss1) ()) (here-pos ina-G (sub-sintern s1<=s1' s2<=s2')) (here-neg ina-G₁ x₁) lab
vcr-match-2-sb (ssplit2 ss1 ss2) (here-pos ina-G x) (there vcr2) lab = nothing
vcr-match-2-sb (ssplit2 ss-[] ()) (here-neg ina-G x) (here-pos ina-G₁ (sub-sextern s1<=s1' s2<=s2')) lab
vcr-match-2-sb (ssplit2 (ss-both ss1) ()) (here-neg ina-G x) (here-pos ina-G₁ (sub-sextern s1<=s1' s2<=s2')) lab
vcr-match-2-sb (ssplit2 (ss-left ss1) (ss-negpos ss2)) (here-neg ina-G (sub-sintern s1<=s1'' s2<=s2'')) (here-pos ina-G₁ (sub-sextern s1<=s1' s2<=s2')) Left = just ((sub-trans (dual-sub s1<=s1') s1<=s1'') , ((sub-trans (dual-sub s2<=s2') s2<=s2'') , (_ , (_ , (_ , (_ , ((ssplit2 (ss-left ss1) (ss-negpos ss2)) , ((here-neg ina-G (Sub.force s1<=s1'')) , (here-pos ina-G₁ (Sub.force s1<=s1'))))))))))
vcr-match-2-sb (ssplit2 (ss-left ss1) (ss-negpos ss2)) (here-neg ina-G (sub-sintern s1<=s1'' s2<=s2'')) (here-pos ina-G₁ (sub-sextern s1<=s1' s2<=s2')) Right = just ((sub-trans (dual-sub s1<=s1') s1<=s1'') , ((sub-trans (dual-sub s2<=s2') s2<=s2'') , (_ , (_ , (_ , (_ , ((ssplit2 (ss-left ss1) (ss-negpos ss2)) , ((here-neg ina-G (Sub.force s2<=s2'')) , (here-pos ina-G₁ (Sub.force s2<=s2'))))))))))
vcr-match-2-sb (ssplit2 (ss-right ss1) ()) (here-neg ina-G x) (here-pos ina-G₁ (sub-sextern s1<=s1' s2<=s2')) lab
vcr-match-2-sb (ssplit2 (ss-posneg ss1) ()) (here-neg ina-G x) (here-pos ina-G₁ (sub-sextern s1<=s1' s2<=s2')) lab
vcr-match-2-sb (ssplit2 (ss-negpos ss1) ()) (here-neg ina-G x) (here-pos ina-G₁ (sub-sextern s1<=s1' s2<=s2')) lab
vcr-match-2-sb (ssplit2 ss1 ss2) (here-neg ina-G x) (here-neg ina-G₁ x₁) lab = nothing
vcr-match-2-sb (ssplit2 ss1 ss2) (here-neg ina-G x) (there vcr2) lab = nothing
vcr-match-2-sb (ssplit2 ss1 ss2) (there vcr1) (here-pos ina-G x) lab = nothing
vcr-match-2-sb (ssplit2 ss1 ss2) (there vcr1) (here-neg ina-G x) lab = nothing
vcr-match-2-sb (ssplit2 ss-[] ()) (there vcr1) (there vcr2) lab
vcr-match-2-sb (ssplit2 (ss-both ss1) (ss-both ss2)) (there vcr1) (there vcr2) lab = map (λ { (ds21<=s11 , ds22<=s12 , _ , _ , _ , _ , ssplit2 ss1' ss2' , vcr1' , vcr2') → ds21<=s11 , ds22<=s12 , _ , _ , _ , _ , (ssplit2 (ss-both ss1') (ss-both ss2')) , ((there vcr1') , (there vcr2')) }) (vcr-match-2-sb (ssplit2 ss1 ss2) vcr1 vcr2 lab)
vcr-match-2-sb (ssplit2 (ss-left ss1) ()) (there vcr1) (there vcr2) lab
vcr-match-2-sb (ssplit2 (ss-right ss1) (ss-both ss2)) (there vcr1) (there vcr2) lab = map  (λ { (ds21<=s11 , ds22<=s12 , _ , _ , _ , _ , ssplit2 ss1' ss2' , vcr1' , vcr2') → ds21<=s11 , ds22<=s12 , _ , _ , _ , _ , (ssplit2 (ss-right ss1') (ss-both ss2')) , ((there vcr1') , (there vcr2')) }) (vcr-match-2-sb (ssplit2 ss1 ss2) vcr1 vcr2 lab)
vcr-match-2-sb (ssplit2 (ss-posneg ss1) ()) (there vcr1) (there vcr2) lab
vcr-match-2-sb (ssplit2 (ss-negpos ss1) ()) (there vcr1) (there vcr2) lab

vcr-match-2-nsb : ∀ {G G₁ G₂ G₁₁ G₁₂ b₁ b₂ m₁ m₂ alti alte}
  → SSplit2 G G₁ G₂ G₁₁ G₁₂
  → ChannelRef G₁₁ b₁ (sintN m₁ alti)
  → ChannelRef G₁₂ b₂ (sextN m₂ alte)
  → (lab : Fin m₁)
  → Maybe (Σ (m₁ ≤ m₂) λ { p →
          ((i : Fin m₁) → dual (alti i) ≲ alte (inject≤ i p)) ×
          ∃ λ G' → ∃ λ G₁' → ∃ λ G₁₁' → ∃ λ G₁₂' →
          SSplit2 G' G₁' G₂ G₁₁' G₁₂' ×
          ChannelRef G₁₁' b₁ (SType.force (alti lab)) ×
          ChannelRef G₁₂' b₂ (SType.force (alte (inject≤ lab p)))})
vcr-match-2-nsb (ssplit2 ss1 ss2) (here-pos ina-G _) (here-pos ina-G₁ _) lab = nothing
vcr-match-2-nsb (ssplit2 ss-[] ()) (here-pos ina-G (sub-sintN m'≤m x)) (here-neg ina-G₁ x₁) lab
vcr-match-2-nsb (ssplit2 (ss-both ss1) ()) (here-pos ina-G (sub-sintN m'≤m x)) (here-neg ina-G₁ x₁) lab
vcr-match-2-nsb {m₁ = m₁} {alti = alti} {alte = alte} (ssplit2 (ss-left ss1) (ss-posneg ss2)) (here-pos ina-G (sub-sintN {alt = alt} m'≤m subint)) (here-neg ina-G₁ (sub-sextN m≤m' subext)) lab = just (≤-trans m'≤m m≤m' , auxSub , _ , _ , _ , _ , (ssplit2 (ss-left ss1) (ss-posneg ss2)) , (here-pos ina-G (Sub.force (subint lab))) , (here-neg ina-G₁ auxExt))
  where
    auxSub : (i : Fin m₁) → dual (alti i) ≲ alte (inject≤ i (≤-trans m'≤m m≤m'))
    auxSub i with subext (inject≤ i m'≤m)
    ... | r  rewrite (inject-trans m≤m' m'≤m i) = sub-trans (dual-sub (subint i)) r
    auxExt : dualF (SType.force (alt (inject≤ lab m'≤m))) ≲' SType.force (alte (inject≤ lab (≤-trans m'≤m m≤m')))
    auxExt with Sub.force (subext (inject≤ lab m'≤m))
    ... | se rewrite inject-trans  m≤m' m'≤m lab = se
vcr-match-2-nsb (ssplit2 (ss-right ss1) ()) (here-pos ina-G (sub-sintN m'≤m x)) (here-neg ina-G₁ x₁) lab
vcr-match-2-nsb (ssplit2 (ss-posneg ss1) ()) (here-pos ina-G (sub-sintN m'≤m x)) (here-neg ina-G₁ x₁) lab
vcr-match-2-nsb (ssplit2 (ss-negpos ss1) ()) (here-pos ina-G (sub-sintN m'≤m x)) (here-neg ina-G₁ x₁) lab
vcr-match-2-nsb (ssplit2 ss1 ss2) (here-pos ina-G x) (there vcr2) lab = nothing
vcr-match-2-nsb (ssplit2 ss-[] ()) (here-neg ina-G x) (here-pos ina-G₁ (sub-sextN m≤m' x₁)) lab
vcr-match-2-nsb (ssplit2 (ss-both ss1) ()) (here-neg ina-G x) (here-pos ina-G₁ (sub-sextN m≤m' x₁)) lab
vcr-match-2-nsb {m₁ = m₁} {alti = alti} {alte = alte} (ssplit2 (ss-left ss1) (ss-negpos ss2)) (here-neg ina-G (sub-sintN m'≤m subint)) (here-pos ina-G₁ (sub-sextN {alt = alt} m≤m' subext)) lab = just ((≤-trans m'≤m m≤m') , auxSub , _ , _ , _ , _ , ssplit2 (ss-left ss1) (ss-negpos ss2) , here-neg ina-G (Sub.force (subint lab)) , here-pos ina-G₁ auxExt)
  where
    auxSub : (i : Fin m₁) → dual (alti i) ≲ alte (inject≤ i (≤-trans m'≤m m≤m'))
    auxSub i with subext (inject≤ i m'≤m)
    ... | sub2 rewrite (inject-trans m≤m' m'≤m i) =
      sub-trans (sub-trans (dual-sub (subint i)) (eq-implies-sub (eq-sym (dual-involution _)))) sub2
    auxExt : SType.force (alt (inject≤ lab m'≤m)) ≲' SType.force (alte (inject≤ lab (≤-trans m'≤m m≤m')))
    auxExt with Sub.force (subext (inject≤ lab m'≤m))
    ... | se rewrite (inject-trans m≤m' m'≤m lab) = se
vcr-match-2-nsb (ssplit2 (ss-right ss1) ()) (here-neg ina-G x) (here-pos ina-G₁ (sub-sextN m≤m' x₁)) lab
vcr-match-2-nsb (ssplit2 (ss-posneg ss1) ()) (here-neg ina-G x) (here-pos ina-G₁ (sub-sextN m≤m' x₁)) lab
vcr-match-2-nsb (ssplit2 (ss-negpos ss1) ()) (here-neg ina-G x) (here-pos ina-G₁ (sub-sextN m≤m' x₁)) lab
vcr-match-2-nsb (ssplit2 ss1 ss2) (here-neg ina-G x) (here-neg ina-G₁ x₁) lab = nothing
vcr-match-2-nsb (ssplit2 ss1 ss2) (here-neg ina-G x) (there vcr2) lab = nothing
vcr-match-2-nsb (ssplit2 ss1 ss2) (there vcr1) (here-pos ina-G x) lab = nothing
vcr-match-2-nsb (ssplit2 ss1 ss2) (there vcr1) (here-neg ina-G x) lab = nothing
vcr-match-2-nsb (ssplit2 ss-[] ()) (there vcr1) (there vcr2) lab
vcr-match-2-nsb (ssplit2 (ss-both ss1) (ss-both ss2)) (there vcr1) (there vcr2) lab =
  map (λ { (m1≤m2 , fdi≤e , _ , _ , _ , _ , ssplit2 ss1' ss2' , vcr1' , vcr2') → m1≤m2 , fdi≤e , _ , _ , _ , _ , (ssplit2 (ss-both ss1') (ss-both ss2')) , there vcr1' , there vcr2' })
      (vcr-match-2-nsb (ssplit2 ss1 ss2) vcr1 vcr2 lab)
vcr-match-2-nsb (ssplit2 (ss-left ss1) ()) (there vcr1) (there vcr2) lab
vcr-match-2-nsb (ssplit2 (ss-right ss1) (ss-both ss2)) (there vcr1) (there vcr2) lab =
  map (λ { (m1≤m2 , fdi≤e , _ , _ , _ , _ , ssplit2 ss1' ss2' , vcr1' , vcr2') → m1≤m2 , fdi≤e , _ , _ , _ , _ , (ssplit2 (ss-right ss1') (ss-both ss2')) , there vcr1' , there vcr2' })
      (vcr-match-2-nsb (ssplit2 ss1 ss2) vcr1 vcr2 lab)
vcr-match-2-nsb (ssplit2 (ss-posneg ss1) ()) (there vcr1) (there vcr2) lab
vcr-match-2-nsb (ssplit2 (ss-negpos ss1) ()) (there vcr1) (there vcr2) lab

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
module Structure.Categorical.Names where

import      Lvl
open import Functional using (const ; swap)
open import Logic
open import Structure.Setoid
import      Structure.Operator.Names as Names
import      Structure.Relator.Names as Names
open import Type

private variable ℓₒ ℓₘ ℓₑ : Lvl.Level
private variable Obj : Type{ℓₒ}
private variable x y z w : Obj

-- Obj is the collection of objects.
-- _⟶_ is the collection of morphisms.
module _ (Morphism : Obj → Obj → Type{ℓₘ}) where
  -- A morphism is an endomorphism when the domain and the codomain are equal.
  -- Something which morphs itself (referring to the object).
  Endomorphism : Obj → Stmt{ℓₘ}
  Endomorphism a = Morphism a a

  module ArrowNotation where
    _⟶_ : Obj → Obj → Type{ℓₘ}
    _⟶_ = Morphism

    -- Reversed arrow
    _⟵_ : Obj → Obj → Type{ℓₘ}
    _⟵_ = swap(_⟶_)

    -- Self-pointing arrow
    ⟲_ : Obj → Type{ℓₘ}
    ⟲_ = Endomorphism

module Morphism where
  module _ (Morphism : Obj → Obj → Type{ℓₘ}) where
    open ArrowNotation(Morphism)

    -- The domain of a morphism
    dom : ∀{x y : Obj} → Morphism(x)(y) → Obj
    dom{x}{_} (_) = x

    -- The codomain of a morphism
    codom : ∀{x y : Obj} → Morphism(x)(y) → Obj
    codom{_}{y} (_) = y

  module _ {Morphism : Obj → Obj → Type{ℓₘ}} ⦃ equiv-morphism : ∀{x y} → Equiv{ℓₑ}(Morphism x y) ⦄ where
    open ArrowNotation(Morphism)

    module _ (_▫_ : Names.SwappedTransitivity(_⟶_)) where
      Associativity : Stmt
      Associativity = ∀{x y z w : Obj} → Names.AssociativityPattern {T₁ = z ⟶ w} {T₂ = y ⟶ z} {T₃ = x ⟶ y} (_▫_)(_▫_)(_▫_)(_▫_)

      Idempotent : (x ⟶ x) → Stmt
      Idempotent(f) = (f ▫ f ≡ f)

      module _ (id : Names.Reflexivity(_⟶_)) where
        Identityₗ : Stmt
        Identityₗ = ∀{x y}{f : x ⟶ y} → (id ▫ f ≡ f)

        Identityᵣ : Stmt
        Identityᵣ = ∀{x y}{f : x ⟶ y} → (f ▫ id ≡ f)

        Inverseₗ : (x ⟶ y) → (y ⟶ x) → Stmt
        Inverseₗ(f)(f⁻¹) = (f⁻¹ ▫ f ≡ id)

        Inverseᵣ : (x ⟶ y) → (y ⟶ x) → Stmt
        Inverseᵣ(f)(f⁻¹) = (f ▫ f⁻¹ ≡ id)

        Involution : (x ⟶ x) → Stmt
        Involution(f) = Inverseᵣ f f

module Polymorphism where
  module _ {Morphism : Obj → Obj → Type{ℓₘ}} ⦃ equiv-morphism : ∀{x y} → Equiv{ℓₑ}(Morphism x y) ⦄ where
    open ArrowNotation(Morphism)

    module _ (_▫_ : Names.SwappedTransitivity(_⟶_)) where
      IdempotentOn : Obj → Obj → (∀{x y} → (x ⟶ y)) → Stmt
      IdempotentOn(x)(z) (f) = ∀{y} → (f{y}{z} ▫ f{x}{y} ≡ f{x}{z})

      module _ (id : Names.Reflexivity(_⟶_)) where
        InvolutionOn : Obj → Obj → (∀{x y} → (x ⟶ y)) → Stmt
        InvolutionOn(x)(y) (f) = (f{x}{y} ▫ f{y}{x} ≡ id{y})

        Involution : (∀{x y} → (x ⟶ y)) → Stmt
        Involution(f) = ∀{x y} → InvolutionOn(x)(y)(f)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

variable
  @0 A : Set

record D : Set₁ where
  field
    f : A


text:
module QuoteContext where

open import Common.Level
open import Common.Prelude
open import Common.Product
open import Common.Equality
open import Common.Reflection

Vec : Set → Nat → Set
Vec A zero = ⊤
Vec A (suc x) = A × Vec A x

test : (n : Nat) (v : Vec Nat n) (m : Nat) → List (Arg Type)
test zero v n = quoteContext
test (suc m) v n = quoteContext

test-zero : test 0 _ 0 ≡
  vArg (def (quote Nat) []) ∷
  vArg (def (quote ⊤) []) ∷ []
test-zero = refl

test-suc : test 1 (zero , _) 0 ≡
  vArg (def (quote Nat) []) ∷
  vArg
    (def (quote Σ)
      (hArg (def (quote lzero) []) ∷
       hArg (def (quote lzero) []) ∷
       vArg (def (quote Nat) []) ∷
       vArg (lam visible (abs "x" (def (quote Vec)
         (vArg (def (quote Nat) []) ∷
          vArg (var 1 []) ∷ [])))) ∷ [])) ∷
  vArg (def (quote Nat) []) ∷ []
test-suc = refl


text:
data D (A : Set) : Set where
  c : A → D A

postulate
  f : (A : Set) → D A → D A
  P : (A : Set) → D A → Set
  _ : (A : Set) (B : _) (g : A → B) → P _ (f _ (c g))

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cumulativity #-}

open import Agda.Primitive
open import Agda.Builtin.Equality

lone ltwo lthree : Level
lone = lsuc lzero
ltwo = lsuc lone
lthree = lsuc ltwo

fails : _≡_ {a = lthree} {A = Set₂} Set₀ Set₁
fails = refl


text:
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Equality

variable
  A B : Set

data Eqn (A : Set) : Set where
  eqn : (x y : A) → x ≡ y → Eqn A

infix 3 _==_
pattern _==_ x y = eqn x y refl

infixl 0 such-that
syntax such-that a (λ x → P) p = a is x such-that p proves P
such-that : (x : A) (P : A → Set) → P x → A
such-that x _ _ = x

infix -1 check_
check_ : A → ⊤
check _ = _

infixl -2 _and_
_and_ : ⊤ → A → ⊤
_ and _ = _

-- Record fields can be marked with @tactic

data ShouldRun : Set where
  run norun : ShouldRun

defaultTo : {A : Set} (x : A) → ShouldRun → Term → TC ⊤
defaultTo _ norun _    = typeError (strErr "Should not run!" ∷ [])
defaultTo x run   hole = bindTC (quoteTC x) (unify hole)

record Class (r : ShouldRun) : Set where
  constructor con
  field
    x : Bool
    @(tactic defaultTo x r) {y} : Bool
open Class

-- # Cases where the tactic should run

test₁ test₂ test₃ : Class run
test₁    = con true             -- Constructor application
test₂    = record { x = true }  -- Record construction
test₃ .x = true                 -- Missing copattern clause

_ = check test₁ == con true {true}
      and test₂ == con true {true}
      and test₃ == con true {true}

-- More elaborate missing copatterns
test₃′ : List Bool → Class run
test₃′ []      .x = false
test₃′ []      .y = true
test₃′ (b ∷ _) .x = b

_ =
  check test₃′ []             == con false {true}
    and λ b → test₃′ (b ∷ []) == con b {b}

-- # Cases where the tactic should not run

-- ## Giving the field explicitly

test₄ test₅ : Class norun
test₄ = con true {_}              is c such-that refl proves c .y ≡ false
test₅ = record{ x = true; y = _ } is c such-that refl proves c .y ≡ false

_ = check test₄ == con true {false}
      and test₅ == con true {false}

-- ## Eta-expansion

-- Eta-expansion of record metas should *not* trigger the tactic, since that
-- would make eta-expansion potentially lose solutions. For instance,
-- `con true {false} == _1`. Here solving `_1 := con true {false}` is valid, but
-- eta-expanding to `con _2 {_3}` and running `defaultTo _2 _3` leads to an error.

test₆ : Class norun
test₆ =
  _ is c such-that refl proves c .x ≡ true
    is c such-that refl proves c .y ≡ false

check₆ : test₆ ≡ con true {false}
check₆ = refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A module used for creating function pipelines, see
-- README.Function.Reasoning for examples
------------------------------------------------------------------------

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

module Function.Reasoning where

open import Function using (_∋_)

-- Need to give _∋_ a new name as syntax cannot contain underscores
infixl 0 ∋-syntax
∋-syntax = _∋_

-- Create ∶ syntax
syntax ∋-syntax A a = a ∶ A

-- Export pipeline functions
open import Function public using (_|>_; _|>′_)


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

module Function.Surjective.Properties where

open import Path
open import Function.Fiber
open import Level
open import HITs.PropositionalTruncation
open import Data.Sigma
open import Function.Surjective.Base
open import Function.Injective.Base
open import Function.Injective.Properties
open import Path.Reasoning
open import Relation.Nullary.Discrete
open import Function

surj-to-inj : (A ↠! B) → (B ↣ A)
surj-to-inj (f , surj) .fst x = surj x .fst
surj-to-inj (f , surj) .snd x y f⁻¹⟨x⟩≡f⁻¹⟨y⟩ =
  x                ≡˘⟨ surj x .snd ⟩
  f (surj x .fst)  ≡⟨ cong f f⁻¹⟨x⟩≡f⁻¹⟨y⟩ ⟩
  f (surj y .fst)  ≡⟨ surj y .snd ⟩
  y ∎

Discrete-distrib-surj : (A ↠! B) → Discrete A → Discrete B
Discrete-distrib-surj = Discrete-pull-inj ∘ surj-to-inj

SplitSurjective⟨id⟩ : SplitSurjective (id {A = A})
SplitSurjective⟨id⟩ x .fst = x
SplitSurjective⟨id⟩ x .snd _ = x

↠!-ident : A ↠! A
↠!-ident .fst = id
↠!-ident .snd y .fst = y
↠!-ident .snd y .snd _ = y
↠!-comp : A ↠! B → B ↠! C → A ↠! C
↠!-comp a→b b→c .fst = b→c .fst ∘ a→b .fst
↠!-comp a→b b→c .snd y .fst = a→b .snd (b→c .snd y .fst) .fst
↠!-comp a→b b→c .snd y .snd = cong (fst b→c) (snd (snd a→b (fst (snd b→c y)))) ; snd (snd b→c y)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Data.Collection.Properties where

open import Data.Collection.Core
open import Data.Collection.Equivalence
open import Data.Collection.Inclusion
open import Data.Collection

open import Data.Sum renaming (map to mapSum)
open import Data.Product
open import Function.Equivalence using (_⇔_; equivalence)

-- open import Data.List public using (List; []; _∷_)
-- open import Data.String public using (String; _≟_)
-- open import Level using (zero)
--
open import Function using (id; _∘_)
open import Relation.Nullary
open import Relation.Nullary.Negation
-- open import Relation.Nullary.Decidable renaming (map to mapDec; map′ to mapDec′)
open import Relation.Unary
-- open import Relation.Binary
open import Relation.Binary.PropositionalEquality

--------------------------------------------------------------------------------
--  Singleton
--------------------------------------------------------------------------------

singleton-≡ : ∀ {x y} → x ∈ c[ singleton y ] ⇔ x ≡ y
singleton-≡ = equivalence to from
    where   to : ∀ {x y} → x ∈ c[ singleton y ] → x ≡ y
            to here = refl
            to (there ())
            from : ∀ {x y} → x ≡ y → x ∈ c[ singleton y ]
            from refl = here

--------------------------------------------------------------------------------
--  Delete
--------------------------------------------------------------------------------

-- still-∈-after-deleted : ∀ {x} y A → x ≢ y → x ∈ c[ A ] → x ∈ c[ delete y A ]
still-∈-after-deleted : ∀ y A → c[ A ] ⊆[ _≢_ y ] c[ delete y A ]
still-∈-after-deleted y []          ≢y ()
still-∈-after-deleted y (a ∷ A) {x} ≢y ∈A with y ≟ a
still-∈-after-deleted y (a ∷ A) ≢y here       | yes p = contradiction p ≢y
still-∈-after-deleted y (a ∷ A) ≢y (there ∈A) | yes p = still-∈-after-deleted y A ≢y ∈A
still-∈-after-deleted y (x ∷ A) ≢y here       | no ¬p = here
still-∈-after-deleted y (a ∷ A) ≢y (there ∈A) | no ¬p = there (still-∈-after-deleted y A ≢y ∈A)

-- still-∉-after-recovered : ∀ {x} y A → x ≢ y → x ∉c delete y A → x ∉ c[ A ]
still-∉-after-recovered : ∀ y A → c[ delete y A ] ⊈[ _≢_ y ] c[ A ]
still-∉-after-recovered y []      ≢y ∉A-y ()
still-∉-after-recovered y (a ∷ A) ≢y ∉A-y ∈a∷A with y ≟ a
still-∉-after-recovered y (a ∷ A) ≢y ∉A-y here       | yes p = contradiction p ≢y
still-∉-after-recovered y (a ∷ A) ≢y ∉A-y (there ∈A) | yes p = contradiction (still-∈-after-deleted y A ≢y ∈A) ∉A-y
still-∉-after-recovered y (a ∷ A) ≢y ∉A-y here       | no ¬p = contradiction here ∉A-y
still-∉-after-recovered y (a ∷ A) ≢y ∉A-y (there ∈A) | no ¬p = contradiction (there (still-∈-after-deleted y A ≢y ∈A)) ∉A-y

--------------------------------------------------------------------------------
--  Union
--------------------------------------------------------------------------------

in-right-union : ∀ A B → c[ B ] ⊆ c[ union A B ]
in-right-union []      B x∈B = x∈B
in-right-union (a ∷ A) B x∈B with a ∈? B
in-right-union (a ∷ A) B x∈B | yes p = in-right-union A B x∈B
in-right-union (a ∷ A) B x∈B | no ¬p = there (in-right-union A B x∈B)

in-left-union : ∀ A B → c[ A ] ⊆ c[ union A B ]
in-left-union []      B ()
in-left-union (a ∷ A) B x∈A         with a ∈? B
in-left-union (a ∷ A) B here        | yes p = in-right-union A B p
in-left-union (a ∷ A) B (there x∈A) | yes p = in-left-union A B x∈A
in-left-union (a ∷ A) B here        | no ¬p = here
in-left-union (a ∷ A) B (there x∈A) | no ¬p = there (in-left-union A B x∈A)

∪-left-identity : ∀ A → c[ [] ] ∪ c[ A ] ≋ c[ A ]
∪-left-identity A = equivalence to inj₂
    where
            to : c[ [] ] ∪ c[ A ] ⊆ c[ A ]
            to (inj₁ ())
            to (inj₂ ∈A) = ∈A

∪-right-identity : ∀ A → c[ A ] ∪ c[ [] ] ≋ c[ A ]
∪-right-identity A = equivalence to inj₁
    where
            to : c[ A ] ∪ c[ [] ] ⊆ c[ A ]
            to (inj₁ ∈A) = ∈A
            to (inj₂ ())

in-either : ∀ A B → c[ union A B ] ⊆ c[ A ] ∪ c[ B ]
in-either []      B x∈A∪B         = inj₂ x∈A∪B
in-either (a ∷ A) B x∈A∪B         with a ∈? B
in-either (a ∷ A) B x∈A∪B         | yes p = mapSum there id (in-either A B x∈A∪B)
in-either (a ∷ A) B here          | no ¬p = inj₁ here
in-either (a ∷ A) B (there x∈A∪B) | no ¬p = mapSum there id (in-either A B x∈A∪B)

not-in-left-union : ∀ A B → c[ union A B ] ⊈ c[ A ]
not-in-left-union A B ∉union ∈A = contradiction (in-left-union A B ∈A) ∉union

not-in-right-union : ∀ A B → c[ union A B ] ⊈ c[ B ]
not-in-right-union A B ∉union ∈A = contradiction (in-right-union A B ∈A) ∉union

in-neither : ∀ A B → c[ union A B ] ⊈ c[ A ] ∪ c[ B ]
in-neither A B ∉union (inj₁ ∈A) = contradiction (in-left-union A B ∈A) ∉union
in-neither A B ∉union (inj₂ ∈B) = contradiction (in-right-union A B ∈B) ∉union

∪-union : ∀ A B → c[ A ] ∪ c[ B ] ≋ c[ union A B ]
∪-union A B = equivalence to (in-either A B)
    where   to : ∀ {x} → x ∈ c[ A ] ∪ c[ B ] → x ∈ c[ union A B ]
            to (inj₁ ∈A) = in-left-union A B ∈A
            to (inj₂ ∈B) = in-right-union A B ∈B

head-∈ : ∀ a A B → c[ a ∷ A ] ⊆ c[ B ] → a ∈ c[ B ]
head-∈ a A B ⊆B = ⊆B here

tail-⊆ : ∀ a A B → c[ a ∷ A ] ⊆ c[ B ] → c[ A ] ⊆ c[ B ]
tail-⊆ a A B ⊆B ∈A = ⊆B (there ∈A)

union-monotone : ∀ {A B C D a} (P : String → Set a) → c[ A ] ⊆[ P ] c[ C ] → c[ B ] ⊆[ P ] c[ D ] → c[ union A B ] ⊆[ P ] c[ union C D ]
union-monotone {[]}    {B} {C} {D} P A⊆C B⊆D ∈P ∈A∪B = in-right-union C D (B⊆D ∈P ∈A∪B)
union-monotone {a ∷ A} {B} {C} {D} P A⊆C B⊆D ∈P ∈A∪B with a ∈? B
union-monotone {a ∷ A}             P A⊆C B⊆D ∈P ∈A∪B         | yes p = union-monotone P (λ P A → A⊆C P (there A)) B⊆D ∈P ∈A∪B
union-monotone {a ∷ A} {B} {C} {D} P A⊆C B⊆D ∈P here         | no ¬p = in-left-union C D (A⊆C ∈P here)
union-monotone {a ∷ A}             P A⊆C B⊆D ∈P (there ∈A∪B) | no ¬p = union-monotone P (λ P₁ A₁ → A⊆C P₁ (there A₁)) B⊆D ∈P ∈A∪B
-- union-monotone {A} P A⊆C B⊆D ∈P ∈A∪B = {!   !}
-- union-monotone : ∀ A B C D → c[ A ] ⊆ c[ C ] → c[ B ] ⊆ c[ D ] → c[ union A B ] ⊆ c[ union C D ]
-- union-monotone [] ._ C D A⊆C B⊆D here = in-right-union C D (B⊆D here)
-- union-monotone [] ._ C D A⊆C B⊆D (there ∈A∪B) = in-right-union C D (B⊆D (there ∈A∪B))
-- union-monotone (a ∷ A) B C D A⊆C B⊆D ∈A∪B with a ∈? B
-- union-monotone (a ∷ A) B C D A⊆C B⊆D ∈A∪B         | yes p = union-monotone A B C D (A⊆C ∘ there) B⊆D ∈A∪B
-- union-monotone (a ∷ A) B C D A⊆C B⊆D here         | no ¬p = in-left-union C D (A⊆C here)
-- union-monotone (a ∷ A) B C D A⊆C B⊆D (there ∈A∪B) | no ¬p = union-monotone A B C D (A⊆C ∘ there) B⊆D ∈A∪B

max_stars_repo_name: banacorn/lambda-calculus

max_issues_repo_name: banacorn/lambda-calculus

max_forks_repo_name: banacorn/lambda-calculus


text:
-- Classical propositional logic, de Bruijn approach, initial encoding

module Bi.Cp where

open import Lib using (List; _,_; LMem; lzero; lsuc)

-- Types

infixl 2 _&&_
infixl 1 _||_
infixr 0 _=>_
data Ty : Set where
  UNIT  :             Ty
  _=>_  : Ty -> Ty -> Ty
  _&&_  : Ty -> Ty -> Ty
  _||_  : Ty -> Ty -> Ty
  FALSE :             Ty

infixr 0 _<=>_
_<=>_ : Ty -> Ty -> Ty
a <=> b = (a => b) && (b => a)

NOT : Ty -> Ty
NOT a = a => FALSE

TRUE : Ty
TRUE = FALSE => FALSE

-- Context and truth judgement

Cx : Set
Cx = List Ty

isTrue : Ty -> Cx -> Set
isTrue a tc = LMem a tc

-- Terms

module Cp where
  infixl 1 _$_
  infixr 0 lam=>_
  infixr 0 abort=>_
  data Tm (tc : Cx) : Ty -> Set where
    var      : forall {a}     -> isTrue a tc               -> Tm tc a
    lam=>_   : forall {a b}   -> Tm (tc , a) b             -> Tm tc (a => b)
    _$_      : forall {a b}   -> Tm tc (a => b) -> Tm tc a -> Tm tc b
    pair'    : forall {a b}   -> Tm tc a        -> Tm tc b -> Tm tc (a && b)
    fst      : forall {a b}   -> Tm tc (a && b)            -> Tm tc a
    snd      : forall {a b}   -> Tm tc (a && b)            -> Tm tc b
    left     : forall {a b}   -> Tm tc a                   -> Tm tc (a || b)
    right    : forall {a b}   -> Tm tc b                   -> Tm tc (a || b)
    case'    : forall {a b c} -> Tm tc (a || b) -> Tm (tc , a) c -> Tm (tc , b) c -> Tm tc c
    abort=>_ : forall {a}     -> Tm (tc , NOT a) FALSE     -> Tm tc a

  syntax pair' x y    = [ x , y ]
  syntax case' xy x y = case xy => x => y

  v0 : forall {tc a} -> Tm (tc , a) a
  v0 = var lzero

  v1 : forall {tc a b} -> Tm (tc , a , b) a
  v1 = var (lsuc lzero)

  v2 : forall {tc a b c} -> Tm (tc , a , b , c) a
  v2 = var (lsuc (lsuc lzero))

  Thm : Ty -> Set
  Thm a = forall {tc} -> Tm tc a
open Cp public

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
module _ where

open import Function.Iteration using (repeatᵣ ; repeatₗ)

[+]-repeatᵣ-𝐒 : ∀{x y z : ℕ} → (x + y ≡ repeatᵣ y (const 𝐒) z x)
[+]-repeatᵣ-𝐒 {x} {𝟎}       = [≡]-intro
[+]-repeatᵣ-𝐒 {x} {𝐒 y} {z} = congruence₁(𝐒) ([+]-repeatᵣ-𝐒 {x} {y} {z})

[+]-repeatₗ-𝐒 : ∀{x y z : ℕ} → (x + y ≡ repeatₗ y (const ∘ 𝐒) x z)
[+]-repeatₗ-𝐒 {x} {𝟎}       = [≡]-intro
[+]-repeatₗ-𝐒 {x} {𝐒 y} {z} = congruence₁(𝐒) ([+]-repeatₗ-𝐒 {x} {y} {z})

[⋅]-repeatᵣ-[+] : ∀{x y} → (x ⋅ y ≡ repeatᵣ y (_+_) x 0)
[⋅]-repeatᵣ-[+] {x} {𝟎}   = [≡]-intro
[⋅]-repeatᵣ-[+] {x} {𝐒 y} = congruence₁(x +_) ([⋅]-repeatᵣ-[+] {x} {y})

[^]-repeatᵣ-[⋅] : ∀{x y} → (x ^ y ≡ repeatᵣ y (_⋅_) x 1)
[^]-repeatᵣ-[⋅] {x} {𝟎}   = [≡]-intro
[^]-repeatᵣ-[⋅] {x} {𝐒 y} = congruence₁(x ⋅_) ([^]-repeatᵣ-[⋅] {x} {y})


text:
-- Andreas, 2015-11-10, issue reported by Wolfram Kahl
-- {-# OPTIONS -v scope.mod.inst:30 #-}
-- {-# OPTIONS -v tc.mod.check:10 -v tc.mod.apply:80 -v impossible:10 #-}

postulate
  A : Set
  a : A

module Id (A : Set) (a : A) where
  x = a

module ModParamsToLoose (A : Set) where
  private module M (a : A) where module I = Id A a
  open M public

open ModParamsToLoose A
open I a

y : A
y = x


text:
open import FRP.JS.String using ( String )
open import FRP.JS.Time using ( Time ; _+_ )
open import FRP.JS.Behaviour using ( Beh ; map ; [_] ; join )
open import FRP.JS.DOM using ( DOM ; text )
open import FRP.JS.RSet using ( ⟦_⟧; ⟨_⟩ )
open import FRP.JS.Time using ( toUTCString ; every )
open import FRP.JS.Delay using ( _sec ; _min )

module FRP.JS.Demo.FastClock where

model : ⟦ Beh ⟨ Time ⟩ ⟧
model = map (λ t → t + 5 min) (every (1 sec))

view : ∀ {w} → ⟦ Beh (DOM w) ⟧
view = join (map (λ t → text [ toUTCString t ]) model)

main : ∀ {w} → ⟦ Beh (DOM w) ⟧
main = view

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

postulate
  A : Set
  B : A → Set
  a : A

Pi : (A → Set) → Set
Pi B = {x : A} → B x

foo : Pi \ y →  Σ (B y) \ _ → Pi \ z → Σ (y ≡ a → B z) \ _ → B y → B z → A
foo = {!!} , (\ { refl → {!!} }) , {!!}

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


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

open import Prelude
import GSeTT.Syntax
import GSeTT.Rules
import GSeTT.Typed-Syntax
open import MCaTT.Desuspension
open import CaTT.Ps-contexts
import CaTT.CaTT

module MCaTT.MCaTT where

  J = CaTT.CaTT.J
  eqdecJ = CaTT.CaTT.eqdecJ

  open import Globular-TT.Syntax J

  ↓C : Pre-Ctx → Pre-Ctx
  ↓T : Pre-Ctx → Pre-Ty → Pre-Ty
  ↓t : Pre-Ctx → Pre-Tm → Pre-Tm
  ↓S : Pre-Ctx → Pre-Sub → Pre-Sub

  ↓C ⊘ = ⊘
  ↓C (Γ ∙ x # ∗) = ↓C Γ
  ↓C (Γ ∙ x # A@(_ ⇒[ _ ] _)) = (↓C Γ) ∙ x # (↓T Γ A)

  ↓T Γ ∗ = ∗
  ↓T Γ (t ⇒[ ∗ ] u) = ∗
  ↓T Γ (t ⇒[ A@(_ ⇒[ _ ] _) ] u) = (↓t Γ t) ⇒[ ↓T Γ A ] (↓t Γ u)

  count-objects-in_until_ : Pre-Ctx → ℕ → ℕ
  count-objects-in ⊘ until x = 0
  count-objects-in Γ ∙ y # ∗ until x with dec-≤ y x
  ... | inl y≤x = S (count-objects-in Γ until x)
  ... | inr x<y = count-objects-in Γ until x
  count-objects-in Γ ∙ y # (_ ⇒[ _ ] _) until x = count-objects-in Γ until x

  ↓t Γ (Var x) = Var (x - (count-objects-in Γ until x))
  ↓t Δ (Tm-constructor i@(((Γ , _) , _) , _) γ) = Tm-constructor i (↓S (GPre-Ctx Γ) γ)

  ↓S Γ <> = <>
  ↓S Γ < γ , x ↦ t > = < ↓S Γ γ , x ↦ ↓t Γ t >

  rule : J → GSeTT.Typed-Syntax.Ctx × Pre-Ty
  rule (((Γ , Γ⊢ps) , A) , _) =
    let Γ⊢ = Γ⊢ps→Γ⊢ Γ⊢ps in
    (↓GC Γ Γ⊢ , ↓⊢C Γ Γ⊢) , ↓T (GPre-Ctx Γ) (CaTT.CaTT.Ty→Pre-Ty A)

  open import Globular-TT.Rules J rule
  open import Globular-TT.CwF-Structure J rule
  open import Globular-TT.Uniqueness-Derivations J rule eqdecJ
  open import Globular-TT.Disks J rule eqdecJ

max_stars_repo_name: ThiBen/catt-formalization

max_issues_repo_name: ThiBen/catt-formalization

max_forks_repo_name: ThiBen/catt-formalization


text:
-- Andreas, 2015-12-05 issue reported by Conor

-- {-# OPTIONS -v tc.cover.splittree:10 -v tc.cc:20 #-}

module Issue1734 where

infix 4 _≡_

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

record One : Set where constructor <>

data Two : Set where tt ff : Two

-- two : ∀{α}{A : Set α} → A → A → Two → A
two : (S T : Set) → Two → Set
two a b tt = a
two a b ff = b

record Sg (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst
open Sg public

_+_ : Set -> Set -> Set
S + T = Sg Two (two S T)

data Twoey : Two -> Set where
  ffey  : Twoey ff
  ttey  : Twoey tt

postulate Thingy : Set

ThingyIf : Two -> Set
ThingyIf tt = Thingy
ThingyIf ff = One

thingy? : (b : Two) -> ThingyIf b -> Twoey b + One -> Thingy + One
thingy? .ff <> (tt , ffey) = ff , <>
thingy? .tt x  (tt , ttey) = tt , x
thingy? _   _  _           = ff , <>

-- WORKS: thingy? _   _  (ff , _   ) = ff , <>

{- Correct split tree

split at 2
|
`- Issue1734.Sg._,_ -> split at 2
   |
   +- Issue1734.Two.tt -> split at 2
   |  |
   |  +- Issue1734.Twoey.ffey -> split at 1
   |  |  |
   |  |  `- Issue1734.One.<> -> done, 0 bindings
   |  |
   |  `- Issue1734.Twoey.ttey -> done, 1 bindings
   |
   `- Issue1734.Two.ff -> done, 3 bindings

but clause compiler deviated from it:

thingy? b x p =
  case p of (y , z) ->
    case y of
      tt -> case x of
              <> -> case z of
                      ffey -> ff , <>
                      ttey -> tt , <>
              _  -> case z of
                      ttey -> tt , x
      _  -> ff , <>

compiled clauses (still containing record splits)
  case 2 of
  Issue1734.Sg._,_ ->
    case 2 of
      Issue1734.Two.tt ->
        case 1 of
          Issue1734.One.<> ->
            case 1 of
              Issue1734.Twoey.ffey -> ff , <>
              Issue1734.Twoey.ttey -> tt , <>
          _ -> case 2 of
                 Issue1734.Twoey.ttey -> tt , x
      _ -> ff , <>

-}

test1 : ∀ x → thingy? tt x (tt , ttey) ≡ tt , x
test1 = λ x → refl  -- should pass!

first-eq-works : ∀ x → thingy? ff x (tt , ffey) ≡ ff , x
first-eq-works = λ x → refl

-- It's weird. I couldn't make it happen with Twoey b alone: I needed Twoey b + One.

-- I also checked that reordering the arguments made it go away. This...

thygni? : (b : Two) -> Twoey b + One -> ThingyIf b -> Thingy + One
thygni? .ff (tt , ffey) <> = ff , <>
thygni? .tt (tt , ttey) x  = tt , x
thygni? _ _ _ = ff , <>

works : ∀ x → thygni? tt (tt , ttey) x ≡ tt , x
works = λ x → refl

-- Moreover, replacing the gratuitous <> pattern by a variable...

hingy? : (b : Two) -> ThingyIf b -> Twoey b + One -> Thingy + One
hingy? .ff x  (tt , ffey) = ff , <>
hingy? .tt x  (tt , ttey) = tt , x
hingy? _ _ _ = ff , <>

-- ...gives...

works2 : ∀ x → hingy? tt x (tt , ttey) ≡ tt , x
works2 = λ x -> refl

-- ...and it has to be a variable: an _ gives the same outcome as <>.


text:
-- Andreas, 2018-10-16, wrong quantity in lambda-abstraction

applyErased : {@0 A B : Set} → (@0 A → B) → @0 A → B
applyErased f x = f x

test : {A : Set} → A → A
test x = applyErased (λ (@ω y) → y) x

-- Expected error:
--
-- Wrong quantity annotation in lambda abstraction.
--
-- Current error (because @ω as default quantity is ignored):
--
-- Variable y is declared erased, so it cannot be used here
-- when checking that the expression y has type _B_7


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

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

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

inequalityShrinkRight : {a b c : ℕ} → a +N b <N c → b <N c
inequalityShrinkRight {a} {b} {c} (le x proof) = le (x +N a) (transitivity (applyEquality succ (equalityCommutative (Semiring.+Associative ℕSemiring x a b))) proof)

inequalityShrinkLeft : {a b c : ℕ} → a +N b <N c → a <N c
inequalityShrinkLeft {a} {b} {c} (le x proof) = le (x +N b) (transitivity (applyEquality succ (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring x b a)) (applyEquality (x +N_) (Semiring.commutative ℕSemiring b a)))) proof)

productCancelsRight : (a b c : ℕ) → (zero <N a) → (b *N a ≡ c *N a) → (b ≡ c)
productCancelsRight a zero zero aPos eq = refl
productCancelsRight zero zero (succ c) (le x ()) eq
productCancelsRight (succ a) zero (succ c) aPos eq = contr
  where
    h : zero ≡ succ c *N succ a
    h = eq
    contr : zero ≡ succ c
    contr = exFalso (naughtE h)
productCancelsRight zero (succ b) zero (le x ()) eq
productCancelsRight (succ a) (succ b) zero aPos eq = contr
  where
    h : succ b *N succ a ≡ zero
    h = eq
    contr : succ b ≡ zero
    contr = exFalso (naughtE (equalityCommutative h))
productCancelsRight zero (succ b) (succ c) (le x ()) eq
productCancelsRight (succ a) (succ b) (succ c) aPos eq = applyEquality succ (productCancelsRight (succ a) b c aPos l)
    where
      i : succ a +N b *N succ a ≡ succ c *N succ a
      i = eq
      j : succ c *N succ a ≡ succ a +N c *N succ a
      j = refl
      k : succ a +N b *N succ a ≡ succ a +N c *N succ a
      k = transitivity i j
      l : b *N succ a ≡ c *N succ a
      l = canSubtractFromEqualityLeft {succ a} {b *N succ a} {c *N succ a} k

productCancelsLeft : (a b c : ℕ) → (zero <N a) → (a *N b ≡ a *N c) → (b ≡ c)
productCancelsLeft a b c aPos pr = productCancelsRight a b c aPos j
  where
    i : b *N a ≡ a *N c
    i = identityOfIndiscernablesLeft _≡_ pr (multiplicationNIsCommutative a b)
    j : b *N a ≡ c *N a
    j = identityOfIndiscernablesRight _≡_ i (multiplicationNIsCommutative a c)

productCancelsRight' : (a b c : ℕ) → (b *N a ≡ c *N a) → (a ≡ zero) || (b ≡ c)
productCancelsRight' zero b c pr = inl refl
productCancelsRight' (succ a) b c pr = inr (productCancelsRight (succ a) b c (succIsPositive a) pr)

productCancelsLeft' : (a b c : ℕ) → (a *N b ≡ a *N c) → (a ≡ zero) || (b ≡ c)
productCancelsLeft' zero b c pr = inl refl
productCancelsLeft' (succ a) b c pr = inr (productCancelsLeft (succ a) b c (succIsPositive a) pr)

subtractionPreservesInequality : {a b : ℕ} → (c : ℕ) → a +N c <N b +N c → a <N b
subtractionPreservesInequality {a} {b} zero prABC rewrite commutative a 0 | commutative b 0 = prABC
subtractionPreservesInequality {a} {b} (succ c) (le x proof) = le x (canSubtractFromEqualityRight {b = succ c} (transitivity (equalityCommutative (+Associative (succ x) a (succ c))) proof))

cancelInequalityLeft : {a b c : ℕ} → a *N b <N a *N c → b <N c
cancelInequalityLeft {a} {zero} {zero} (le x proof) rewrite (productZeroRight a) = exFalso (naughtE (equalityCommutative proof))
cancelInequalityLeft {a} {zero} {succ c} pr = succIsPositive c
cancelInequalityLeft {a} {succ b} {zero} (le x proof) rewrite (productZeroRight a) = exFalso (naughtE (equalityCommutative proof))
cancelInequalityLeft {a} {succ b} {succ c} pr = succPreservesInequality q'
  where
    p' : succ b *N a <N succ c *N a
    p' = canFlipMultiplicationsInIneq {a} {succ b} {a} {succ c} pr
    p'' : b *N a +N a <N succ c *N a
    p'' = identityOfIndiscernablesLeft _<N_ p' (commutative a (b *N a))
    p''' : b *N a +N a <N c *N a +N a
    p''' = identityOfIndiscernablesRight _<N_ p'' (commutative a (c *N a))
    p : b *N a <N c *N a
    p = subtractionPreservesInequality a p'''
    q : a *N b <N a *N c
    q = canFlipMultiplicationsInIneq {b} {a} {c} {a} p
    q' : b <N c
    q' = cancelInequalityLeft {a} {b} {c} q

<NProp : {a b : ℕ} → .(a <N b) → a <N b
<NProp {zero} {succ b} a<b = succIsPositive _
<NProp {succ a} {succ b} a<b = succPreservesInequality (<NProp (canRemoveSuccFrom<N a<b))

zeroLeast : {m n : ℕ} → m <N n → 0 <N n
zeroLeast {zero} m<n = m<n
zeroLeast {succ m} {succ n} m<n = le n (applyEquality succ (Semiring.sumZeroRight ℕSemiring n))


text:
{-# OPTIONS --without-K #-}
module Explore.Explorable.Isos where

open import Function
open import Data.Product
open import Data.Nat
open import Data.Vec renaming (sum to vsum)
open import Function.Related.TypeIsomorphisms.NP
import Relation.Binary.PropositionalEquality.NP as ≡
open ≡ using (_≡_; _≗_)

open import Explore.Type
open import Explore.Explorable
open import Explore.Product

swap-μ : ∀ {A B} → Explorable (A × B) → Explorable (B × A)
swap-μ = μ-iso swap-iso

swapS-preserve : ∀ {A B} f (μA×B : Explorable (A × B)) → sum μA×B f ≡ sum (swap-μ μA×B) (f ∘ swap)
swapS-preserve = μ-iso-preserve swap-iso

μ^ : ∀ {A} (μA : Explorable A) n → Explorable (A ^ n)
μ^ μA zero    = μLift μ𝟙
μ^ μA (suc n) = μA ×-μ μ^ μA n

μVec : ∀ {A} (μA : Explorable A) n  → Explorable (Vec A n)
μVec μA n = μ-iso (^↔Vec n) (μ^ μA n)

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
open import Preliminaries

module Lab3-LRSol where

  {- de Bruijn indices are representd as proofs that
     an element is in a list -}
  data _∈_ {A : Set} : (x : A) (l : List A) → Set where -- type \in
    i0 : {x : A} {xs : List A} → x ∈ x :: xs
    iS : {x y : A} {xs : List A} → x ∈ xs → x ∈ y :: xs

  {- types of the STLC -}
  data Tp : Set where
    b : Tp             -- uninterpreted base type
    _⇒_ : Tp → Tp → Tp -- type \=>

  {- contexts are lists of Tp's -}
  Ctx = List Tp
  _,,_ : Ctx → Tp → Ctx
  Γ ,, τ = τ :: Γ

  infixr 10 _⇒_
  infixr 9 _,,_
  infixr 8 _|-_ -- type \entails

  {- Γ ⊢ τ represents a term of type τ in context Γ -}
  data _|-_ (Γ : Ctx) : Tp → Set where
    c   : Γ |- b -- some constant of the base type
    v   : {τ : Tp}
        → τ ∈ Γ
        → Γ |- τ
    lam : {τ1 τ2 : Tp}
        → Γ ,, τ1 |- τ2
        → Γ |- τ1 ⇒ τ2
    app : {τ1 τ2 : Tp}
        → Γ |- τ1 ⇒ τ2
        → Γ |- τ1
        → Γ |- τ2

  module Examples where
    i : [] |- b ⇒ b
    i = lam (v i0) -- \ x -> x

    k : [] |- b ⇒ b ⇒ b
    k = lam (lam (v (iS i0))) -- \ x -> \ y -> x

    {- TASK 1: Define a term representing  \ x -> \ y -> y -}
    k' : [] |- b ⇒ b ⇒ b
    k' = lam (lam (v i0))

  {- The following proof is like a "0-ary" logical relation.
     It gives a semantics of the STLC in Agda.
     This shows that the STLC is sound, relative to Agda.
  -}
  module Semantics (B : Set) (elB : B) where
    -- works for any interpretation of the base type b

    -- function mapping STLC types to Agda types
    [_]t : Tp → Set  -- type \(0 and \)0
    [ b ]t = B
    [ τ1 ⇒ τ2 ]t = [ τ1 ]t → [ τ2 ]t

    -- function mapping STLC contexts to Agda types
    [_]c : Ctx → Set
    [ [] ]c = Unit
    [ τ :: Γ ]c = [ Γ ]c × [ τ ]t

    {- TASK 2 : Define the interpretation of terms -}
    [_] : {Γ : Ctx} {τ : Tp} → Γ |- τ → [ Γ ]c → [ τ ]t
    [ c ] γ = elB
    [ v i0 ] γ = snd γ
    [ v (iS x) ] γ = [ v x ] (fst γ)
    [ lam e ] γ = \ x → [ e ] (γ , x)
    [ app e1 e2 ] γ = [ e1 ] γ ([ e2 ] γ)

    {- the following test should pass
    test : ⟦ Examples.k ⟧ == \ γ x y → x
    test = Refl
    -}

  {- you can ignore the implementation of this module.
     the interface for the components you need is listed below
  -}
  module RenamingAndSubstitution where

    -- renamings = variable for variable substitutions.
    -- For simplicity, these are defined as tuples, by recursion on the context.
    -- It might clean up some of the proofs to use a functional view,
    --   {τ : Tp} → τ ∈ Γ → τ ∈ Γ'
    -- because then we could avoid some of the inductions here,
    -- and some of the associativity/unit properties would be free.
    module Renamings where

      infix 9 _⊇_

      _⊇_ : Ctx → Ctx → Set -- type \sup=
      Γ' ⊇ [] = Unit
      Γ' ⊇ (τ :: Γ) = (Γ' ⊇ Γ) × (τ ∈ Γ')

      -- variables are functorial in the context
      rename-var : {Γ Γ' : Ctx} {τ : Tp} → Γ' ⊇ Γ → τ ∈ Γ → τ ∈ Γ'
      rename-var (ρ , x') i0 = x'
      rename-var (ρ , _) (iS x) = rename-var ρ x

      {- conceptually, we could define p and ⊇-compose and ⊇-id as primitive
         and derive this.
         but this works better inductively than ⊇-single does.
      -}
      p· : {Γ : Ctx} {Γ' : Ctx} → Γ ⊇ Γ' → {τ : Tp} → (Γ ,, τ) ⊇ Γ'
      p· {Γ' = []} ren = <>
      p· {Γ' = (τ :: Γ')} (ρ , x) = p· ρ , iS x

      idr : {Γ : Ctx} → Γ ⊇ Γ
      idr {[]} = <>
      idr {τ :: Γ} = p· idr , i0

      _·rr_ : {Γ1 Γ2 Γ3 : Ctx} → Γ1 ⊇ Γ2 → Γ2 ⊇ Γ3 → Γ1 ⊇ Γ3
      _·rr_ {Γ1} {Γ2} {[]} ρ2 ρ3 = <>
      _·rr_ {Γ1} {Γ2} {x :: Γ3} ρ2 (ρ3 , x3) = (ρ2 ·rr ρ3) , rename-var ρ2 x3

      -- category with families notation
      p : {Γ : Ctx} {τ : Tp} → (Γ ,, τ ⊇ Γ)
      p = p· idr

      -- next, we should show associativity and unit laws for ∘rr.
      -- However:
      -- (1) because renamings are defined using variables, this depends on (some of) functoriality of τ ∈ -,
      --     so we define that here, too.
      -- (2) we only need one of the unit laws

      rename-var-· : {Γ1 Γ2 Γ3 : Ctx} → (ρ2 : Γ1 ⊇ Γ2) (ρ3 : Γ2 ⊇ Γ3) {τ : Tp} (x : τ ∈ Γ3)
                         → rename-var ρ2 (rename-var ρ3 x) == rename-var (_·rr_ ρ2 ρ3) x
      rename-var-· ρ2 ρ3 i0 = Refl
      rename-var-· ρ2 ρ3 (iS x) = rename-var-· ρ2 (fst ρ3) x

      ·rr-assoc : {Γ1 Γ2 Γ3 Γ4 : Ctx} → (ρ2 : Γ1 ⊇ Γ2) (ρ3 : Γ2 ⊇ Γ3) (ρ4 : Γ3 ⊇ Γ4) → _·rr_ ρ2 (_·rr_ ρ3 ρ4) == _·rr_ (_·rr_ ρ2 ρ3) ρ4
      ·rr-assoc {Γ4 = []} ρ2 ρ3 ρ4 = Refl
      ·rr-assoc {Γ4 = τ4 :: Γ4} ρ2 ρ3 (ρ4 , x4) = ap2 _,_ (·rr-assoc ρ2 ρ3 ρ4) (rename-var-· ρ2 ρ3 x4)

      -- rest of functoriality of rename-var
      mutual
        -- generalization to get the induction to go through
        rename-var-p' : {Γ Γ' : Ctx} {τ τ' : Tp} (ρ : Γ' ⊇ Γ) (x : τ ∈ Γ) → rename-var (p· ρ {τ'}) x == (iS (rename-var ρ x))
        rename-var-p' ρ i0 = Refl
        rename-var-p' (ρ , _) (iS x) = rename-var-p' ρ x

        -- this would be definitional if renamings were functions.
        -- this instances is often needed below
        rename-var-p : {Γ : Ctx} {τ τ' : Tp} (x : τ ∈ Γ) → rename-var (p· idr {τ'}) x == (iS x)
        rename-var-p x = ap iS (rename-var-ident _ x) ∘ rename-var-p' idr x

        rename-var-ident : {τ : Tp} (Γ : Ctx) (x : τ ∈ Γ) → rename-var idr x == x
        rename-var-ident .(τ :: Γ) (i0 {τ} {Γ}) = Refl
        rename-var-ident .(τ' :: Γ) (iS {τ} {τ'} {Γ} x) = rename-var-p x

      -- beta reduction for p
      pβ1' : {Γ1 Γ2 Γ3 : Ctx} → (ρ2 : Γ1 ⊇ Γ2) (ρ3 : Γ2 ⊇ Γ3) {τ : Tp} (x : τ ∈ Γ1)
            → (ρ2 , x) ·rr (p· ρ3) == (ρ2 ·rr ρ3)
      pβ1' {Γ1} {_} {[]} ρ2 ρ3 x = Refl
      pβ1' {Γ1} {_} {τ3 :: Γ3} ρ2 (ρ3 , x3) x₁ = ap (λ x → x , rename-var ρ2 x3) (pβ1' ρ2 ρ3 _)

      mutual
        ·rr-unitr : {Γ1 Γ2 : Ctx} → (ρ2 : Γ1 ⊇ Γ2)
              → ρ2 ·rr idr == ρ2
        ·rr-unitr {Γ1} {[]} ρ2 = Refl
        ·rr-unitr {Γ1} {τ2 :: Γ2} (ρ2 , x2) = ap (λ x → x , x2) (pβ1 ρ2 x2)

        pβ1 : {Γ1 Γ2 : Ctx} → (ρ2 : Γ1 ⊇ Γ2) {τ : Tp} (x : τ ∈ Γ1)
              → (ρ2 , x) ·rr p == ρ2
        pβ1 ρ2 x = ·rr-unitr ρ2 ∘ pβ1' ρ2 idr x

      -- p· is equivalent to the alternate definition.
      p·-def : {Γ1 Γ2 : Ctx} {τ : Tp} (ρ : Γ1 ⊇ Γ2) → p· ρ {τ} == p ·rr ρ
      p·-def {_}{[]} ρ = Refl
      p·-def {_}{τ1 :: Γ1} (ρ , x) = ap2 _,_ (p·-def ρ) (! (rename-var-p x))

      -- terms are functorial in renamings

      addvar-ren : {Γ Γ' : Ctx} {τ : Tp} → Γ' ⊇ Γ → Γ' ,, τ ⊇ Γ ,, τ
      addvar-ren ρ = (p· ρ , i0)

      rename : {Γ Γ' : Ctx} {τ : Tp} → Γ' ⊇ Γ → Γ |- τ → Γ' |- τ
      rename ρ c = c
      rename ρ (v x) = v (rename-var ρ x)
      rename ρ (lam e) = lam (rename (addvar-ren ρ) e)
      rename ρ (app e e') = app (rename ρ e) (rename ρ e')

      rename-· : {Γ1 Γ2 Γ3 : Ctx} → (ρ2 : Γ1 ⊇ Γ2) (ρ3 : Γ2 ⊇ Γ3) {τ : Tp} (e : Γ3 |- τ)
                     → rename ρ2 (rename ρ3 e) == rename (ρ2 ·rr ρ3) e
      rename-· ρ2 ρ3 c = Refl
      rename-· ρ2 ρ3 (v x) = ap v (rename-var-· ρ2 ρ3 x)
      rename-·{Γ1}{Γ2}{Γ3} ρ2 ρ3 (lam e) = ap lam (ap (λ x → rename (x , i0) e) lemma1 ∘ rename-· (addvar-ren ρ2) (addvar-ren ρ3) e) where
        lemma1 : (p· ρ2 , i0) ·rr (p· ρ3) == p· (ρ2 ·rr ρ3)
        lemma1 = (p· ρ2 , i0) ·rr (p· ρ3)  =⟨ pβ1' (p· ρ2) ρ3 i0 ⟩
                 (p· ρ2) ·rr ρ3            =⟨ ap (λ x → _·rr_ x ρ3) (p·-def ρ2) ⟩
                 (p ·rr ρ2) ·rr ρ3         =⟨ ! (·rr-assoc p ρ2 ρ3) ⟩
                 p ·rr (ρ2 ·rr ρ3)         =⟨ ! (p·-def (ρ2 ·rr ρ3))⟩
                 p· (ρ2 ·rr ρ3) ∎
      rename-· ρ2 ρ3 (app e e₁) = ap2 app (rename-· ρ2 ρ3 e) (rename-· ρ2 ρ3 e₁)

      -- not necessary for the proof, but an easy corollary of the above
      rename-id : {Γ : Ctx}{τ : Tp} (e : Γ |- τ) → rename idr e == e
      rename-id c = Refl
      rename-id (v x) = ap v (rename-var-ident _ x)
      rename-id (lam e) = ap lam (rename-id e)
      rename-id (app e e₁) = ap2 app (rename-id e) (rename-id e₁)
    open Renamings

    -- expression-for-variable substitutions

    module Subst where

      _|-c_ : Ctx → Ctx → Set
      Γ' |-c [] = Unit
      Γ' |-c (τ :: Γ) = (Γ' |-c Γ) × (Γ' |- τ)

      _·rs_ : {Γ1 Γ2 Γ3 : Ctx} →  Γ1 ⊇ Γ2 → Γ2 |-c Γ3 → Γ1 |-c Γ3
      _·rs_ {Γ1} {Γ2} {[]} ρ θ = <>
      _·rs_ {Γ1} {Γ2} {τ3 :: Γ3} ρ (θ , e) = ρ ·rs θ , rename ρ e

      addvar : {Γ Γ' : Ctx} {τ : Tp} → Γ |-c Γ' → (Γ ,, τ) |-c (Γ' ,, τ)
      addvar θ = p ·rs θ , v i0

      ids : {Γ : Ctx} → Γ |-c Γ
      ids {[]} = <>
      ids {τ :: Γ} = p ·rs ids , v i0

      subst-var : {Γ Γ' : Ctx}{τ : Tp} → Γ |-c Γ' → τ ∈ Γ' → Γ |- τ
      subst-var (θ , e) i0 = e
      subst-var (θ , _) (iS x) = subst-var θ x

      subst : {Γ Γ' : Ctx}{τ : Tp} → Γ |-c Γ' → Γ' |- τ  → Γ |- τ
      subst θ c = c
      subst θ (v x) = subst-var θ x
      subst θ (lam e) = lam (subst (addvar θ) e)
      subst θ (app e e') = app (subst θ e) (subst θ e')

      subst1 : {τ τ0 : Tp} → [] |- τ0 → ([] ,, τ0) |- τ → [] |- τ
      subst1 e0 e = subst (<> , e0) e

      -- composition of renamings and substitutions

      _·sr_ : {Γ1 Γ2 Γ3 : Ctx} →  Γ1 |-c Γ2 → Γ2 ⊇ Γ3 → Γ1 |-c Γ3
      _·sr_ {Γ1} {Γ2} {[]} θ ρ = <>
      _·sr_ {Γ1} {Γ2} {τ3 :: Γ3} θ (ρ , x) = _·sr_ θ ρ , subst-var θ x

      _·ss_ : {Γ1 Γ2 Γ3 : Ctx} → Γ1 |-c Γ2 → Γ2 |-c Γ3 → Γ1 |-c Γ3
      _·ss_ {Γ3 = []} θ1 θ2 = <>
      _·ss_ {Γ1} {Γ2} {τ :: Γ3} θ1 (θ2 , e2) = θ1 ·ss θ2 , subst θ1 e2

      -- subst var functoriality

      subst-var-·rs : {Γ1 Γ2 Γ3 : Ctx} (ρ : Γ1 ⊇ Γ2) (θ : Γ2 |-c Γ3) {τ : Tp} (x : τ ∈ Γ3)
                           → subst-var (ρ ·rs θ) x == rename ρ (subst-var θ x)
      subst-var-·rs ρ θ i0 = Refl
      subst-var-·rs ρ (θ , _) (iS x) = subst-var-·rs ρ θ x

      subst-var-∘ss : {Γ1 Γ2 Γ3 : Ctx} → (θ2 : Γ1 |-c Γ2) (θ3 : Γ2 |-c Γ3) {τ : Tp} (x : τ ∈ Γ3)
                        → subst-var (_·ss_ θ2 θ3) x == subst θ2 (subst-var θ3 x)
      subst-var-∘ss θ2 θ3 i0 = Refl
      subst-var-∘ss θ2 (θ3 , _) (iS x) = subst-var-∘ss θ2 θ3 x

      subst-var-·sr : {Γ1 Γ2 Γ3 : Ctx} {τ : Tp} → (θ2 : Γ1 |-c Γ2) (ρ : Γ2 ⊇ Γ3) (x : τ ∈ Γ3)
                           → (subst-var θ2 (rename-var ρ x)) == subst-var (_·sr_ θ2 ρ) x
      subst-var-·sr θ2 ρ i0 = Refl
      subst-var-·sr θ2 ρ (iS x) = subst-var-·sr θ2 (fst ρ) x

      subst-var-id : {Γ : Ctx} {τ : Tp} → (x : τ ∈ Γ) → v x == subst-var ids x
      subst-var-id i0 = Refl
      subst-var-id {τ :: Γ} (iS x) = !
        (_ =〈 subst-var-·rs (p· idr) ids x 〉
         rename (p· idr) _ =〈 ! (ap (rename (p· idr)) (subst-var-id x)) 〉
         rename (p· idr) (v x) =〈 ap v (rename-var-p x) 〉
         v (iS x) ∎)

      -- associativity and unit laws for composition.
      -- also includes some β rules for composing with p.
      -- and functoriality of subst in the various compositions, since substitutions involve terms.

      ∘rsr-assoc : {Γ1 Γ2 Γ3 Γ4 : Ctx} → (ρ2 : Γ1 ⊇ Γ2) (θ3 : Γ2 ⊢c Γ3) (ρ4 : Γ3 ⊇ Γ4)
                 → (ρ2 ·rs θ3) ·sr ρ4 == ρ2 ·rs (θ3 ·sr ρ4)
      ∘rsr-assoc {Γ1} {Γ2} {Γ3} {[]} ρ2 θ3 ρ4 = Refl
      ∘rsr-assoc {Γ1} {Γ2} {Γ3} {τ4 :: Γ4} ρ2 θ3 (ρ4 , x4) = ap2 _,_ (∘rsr-assoc ρ2 θ3 ρ4) (subst-var-·rs ρ2 θ3 x4)

      ·sr-pβ'  : {Γ1 Γ2 Γ3 : Ctx} {τ : Tp} → (θ2 : Γ1 ⊢c Γ2) (ρ : Γ2 ⊇ Γ3) {e : _ ⊢ τ}
                → (θ2 , e) ·sr (p· ρ) == θ2 ·sr ρ
      ·sr-pβ' {Γ1} {Γ2} {[]} θ2 ρ = Refl
      ·sr-pβ' {Γ1} {Γ2} {τ :: Γ3} θ2 (ρ , x) = ap2 _,_ (·sr-pβ' θ2 ρ) Refl

      mutual
        ·sr-unitr : {Γ1 Γ2 : Ctx} → (θ : Γ1 ⊢c Γ2) → θ ·sr idr == θ
        ·sr-unitr {Γ1} {[]} θ = Refl
        ·sr-unitr {Γ1} {τ2 :: Γ2} (θ , e) = ap (λ x → x , e) (·sr-pβ θ)

        ·sr-pβ  : {Γ1 Γ2 : Ctx} {τ : Tp} → (θ2 : Γ1 ⊢c Γ2) {e : _ ⊢ τ}
                         → (θ2 , e) ·sr p == θ2
        ·sr-pβ θ2 = ·sr-unitr θ2 ∘ ·sr-pβ' θ2 idr

      subst-id : {Γ : Ctx} {τ : Tp} {e : Γ ⊢ τ} → e == subst (ids) e
      subst-id {e = c} = Refl
      subst-id {e = v x} = subst-var-id x
      subst-id {e = lam e} = ap lam (subst-id)
      subst-id {e = app e e₁} = ap2 app subst-id subst-id

      subst-·rs : {Γ1 Γ2 Γ4 : Ctx} {τ : Tp} → (ρ : Γ4 ⊇ Γ1) (θ2 : Γ1 ⊢c Γ2) (e : Γ2 ⊢ τ)
                → rename ρ (subst θ2 e) == subst (ρ ·rs θ2) e
      subst-·rs ρ θ2 c = Refl
      subst-·rs ρ θ2 (v x) = ! (subst-var-·rs ρ θ2 x)
      subst-·rs ρ θ2 (lam e) = ap lam (ap (λ x → subst x e) (ap (λ x → x , v i0) (lemma2 ρ θ2)) ∘ subst-·rs (addvar-ren ρ) (addvar θ2) e) where
              lemma1 : {Γ3 Γ5 : Ctx} (ρ₁ : Γ5 ⊇ Γ3) {τ3 : Tp}
                     →  (addvar-ren {_}{_}{τ3} ρ₁) ·rr (p· idr) == (p· idr) ·rr ρ₁
              lemma1 {Γ3} {Γ5} ρ₁ = (p· ρ₁ , i0) ·rr (p· idr) =〈 Refl 〉
                                   (p· ρ₁ , i0) ·rr  p       =〈 ap (λ x → (x , i0) ·rr p) (p·-def ρ₁)〉
                                   (p ·rr ρ₁ , i0) ·rr  p    =〈 pβ1 (p ·rr ρ₁) i0 〉
                                   p ·rr ρ₁                  =〈 Refl 〉
                                   (p· idr) ·rr ρ₁ ∎

              lemma2 : {Γ1 Γ2 Γ4 : Ctx} {τ : Tp} → (ρ : Γ4 ⊇ Γ1) (θ2 : Γ1 ⊢c Γ2)
                     → (addvar-ren{_}{_}{τ} ρ) ·rs (fst (addvar θ2)) == p ·rs (ρ ·rs θ2)
              lemma2 {Γ2 = []} ρ₁ θ3 = Refl
              lemma2 {Γ2 = τ2 :: Γ2} ρ₁ (θ3 , e3) = ap2 _,_ (lemma2 ρ₁ θ3)
                         (! (rename-· (p·  idr) ρ₁ e3) ∘
                          (ap (λ x → rename x e3) (lemma1 ρ₁) ∘
                           rename-· (addvar-ren ρ₁) (p·  idr) e3))
      subst-·rs ρ θ2 (app e e₁) = ap2 app (subst-·rs ρ θ2 e) (subst-·rs ρ θ2 e₁)

      ·rss-assoc : {Γ1 Γ2 Γ3 Γ4 : Ctx} → (ρ : Γ4 ⊇ Γ1) (θ2 : Γ1 ⊢c Γ2) (θ3 : Γ2 ⊢c Γ3)
                           → ρ ·rs (θ2 ·ss θ3) == (ρ ·rs θ2) ·ss θ3
      ·rss-assoc {Γ1} {Γ2} {[]} ρ θ2 θ3 = Refl
      ·rss-assoc {Γ1} {Γ2} {x :: Γ3} ρ θ2 (θ3 , e3) = ap2 _,_ (·rss-assoc ρ θ2 θ3) (subst-·rs ρ θ2 e3)

      subst-·sr : {Γ1 Γ2 Γ3 : Ctx} {τ : Tp} → (θ2 : Γ1 ⊢c Γ2) (ρ : Γ2 ⊇ Γ3) (e : Γ3 ⊢ τ)
                           → (subst θ2 (rename ρ e)) == subst (θ2 ·sr ρ) e
      subst-·sr θ2 ρ c = Refl
      subst-·sr θ2 ρ (v x) = subst-var-·sr θ2 ρ x
      subst-·sr θ2 ρ (lam e) = ap lam (ap (λ x → subst x e) (ap (λ x → x , v i0) (lemma θ2 ρ)) ∘ subst-·sr (addvar θ2) (addvar-ren ρ) e) where
         lemma :  {Γ1 Γ2 Γ3 : Ctx} {τ : Tp} → (θ2 : Γ1 ⊢c Γ2) (ρ : Γ2 ⊇ Γ3) → (addvar{_}{_}{τ} θ2) ·sr (p· ρ) == p ·rs (θ2 ·sr ρ)
         lemma θ2 ρ = ∘rsr-assoc (p·  idr) θ2 ρ ∘ ·sr-pβ' (_·rs_ (p·  idr) θ2) ρ {v i0}
      subst-·sr θ2 ρ (app e e₁) = ap2 app (subst-·sr θ2 ρ e) (subst-·sr θ2 ρ e₁)

      ·srs-assoc : {Γ1 Γ2 Γ3 Γ4 : Ctx} (θ : Γ1 ⊢c Γ2) (ρ : Γ2 ⊇ Γ3) (θ' : Γ3 ⊢c Γ4)
                 → θ ·ss (ρ ·rs θ') == (θ ·sr ρ) ·ss θ'
      ·srs-assoc {Γ1} {Γ2} {Γ3} {[]} θ ρ θ' = Refl
      ·srs-assoc {Γ1} {Γ2} {Γ3} {x :: Γ4} θ ρ (θ' , e') = ap2 _,_ (·srs-assoc θ ρ θ') (subst-·sr θ ρ e')

      subst-·ss : {Γ1 Γ2 Γ3 : Ctx} → (θ2 : Γ1 ⊢c Γ2) (θ3 : Γ2 ⊢c Γ3) {τ : Tp} (e : Γ3 ⊢ τ)
                    → subst (θ2 ·ss θ3) e == subst θ2 (subst θ3 e)
      subst-·ss θ2 θ3 c = Refl
      subst-·ss θ2 θ3 (v x) = subst-var-∘ss θ2 θ3 x
      subst-·ss θ2 θ3 (lam e) = ap lam (subst-·ss (addvar θ2) (addvar θ3) e ∘
                                            ap (λ x → subst x e) (ap (λ x → x , v i0)
                                               (lemma1 ∘ ·rss-assoc p θ2 θ3))) where
                    lemma1 : (p ·rs θ2) ·ss θ3 ==
                             (addvar θ2) ·ss (fst (addvar θ3))
                    lemma1 = (p ·rs θ2) ·ss θ3 =〈 ! (ap (λ x → x ·ss θ3) (·sr-pβ (p ·rs θ2) {v i0})) 〉
                             ((p ·rs θ2 , v i0) ·sr p) ·ss θ3 =〈 ! (·srs-assoc (p ·rs θ2 , v i0) p θ3) 〉
                             (p ·rs θ2 , v i0) ·ss (p ·rs θ3) ∎
      subst-·ss θ2 θ3 (app e e₁) = ap2 app (subst-·ss θ2 θ3 e) (subst-·ss θ2 θ3 e₁)

      ·ss-unitl : {Γ1 Γ2 : Ctx} → (θ : Γ1 ⊢c Γ2) → ids ·ss θ == θ
      ·ss-unitl {Γ2 = []} θ = Refl
      ·ss-unitl {Γ2 = τ :: Γ2} (θ , e) = ap2 _,_ (·ss-unitl θ) (! subst-id)

      compose1 : {τ1 τ2 : Tp} {Γ : Ctx} (θ : [] ⊢c Γ) (e' : [] ⊢ τ1)
               → (θ , e') == (<> , e') ·ss (addvar θ)
      compose1 {τ1}{τ2} θ e' = ap (λ x → x , e') (! (·srs-assoc (<> , e') (p{_}{τ1}) θ) ∘ ! (·ss-unitl θ))

      subst-compose1 : {τ1 τ2 : Tp} {Γ : Ctx} (θ : [] ⊢c Γ) (e' : [] ⊢ τ1) (e : Γ ,, τ1 ⊢ τ2)
              → subst (θ , e') e == subst1 e' (subst (addvar θ) e)
      subst-compose1{τ1}{τ2}{Γ} θ e' e = subst-·ss (<> , e') (addvar θ) e ∘ ap (λ x → subst x e) (compose1{τ1}{τ2}{Γ} θ e')

    open Subst public

  open RenamingAndSubstitution using (subst1 ; _⊢c_ ; subst ; subst-id ; subst-compose1)
  {- θ : Γ ⊢c Γ' means θ is a substitution for Γ' in terms of Γ.  It is defined as follows:

    _⊢c_ : Ctx → Ctx → Set
    Γ' ⊢c [] = Unit
    Γ' ⊢c (τ :: Γ) = (Γ' ⊢c Γ) × (Γ' ⊢ τ)

    -- apply a substitution to a term
    subst : {Γ Γ' : Ctx}{τ : Tp} → Γ ⊢c Γ' → Γ' ⊢ τ  → Γ ⊢ τ

    -- substitution for a single variable
    subst1 : {τ τ0 : Tp} → [] ⊢ τ0 → ([] ,, τ0) ⊢ τ → [] ⊢ τ

    -- you will need these two properties:
    subst-compose1 : {τ1 τ2 : Tp} {Γ : Ctx} (θ : [] ⊢c Γ) (e' : [] ⊢ τ1) (e : Γ ,, τ1 ⊢ τ2)
                   → subst (θ , e') e == subst1 e' (subst (addvar θ) e)

    subst-id : {Γ : Ctx} {τ : Tp} {e : Γ ⊢ τ} → e == subst (ids) e
  -}

  module OpSem where
    -- step relation
    data _↦_ : {τ : Tp} → [] |- τ → [] |- τ → Set where
      Step/app  :{τ1 τ2 : Tp} {e e' : [] |- τ1 ⇒ τ2} {e1 : [] |- τ1}
             → e ↦ e'
             → (app e e1) ↦ (app e' e1)
      Step/β : {τ1 τ2 : Tp} {e : [] ,, τ1 |- τ2} {e1 : [] |- τ1}
             → (app (lam e) e1) ↦ subst1 e1 e

    -- reflexive/transitive closure
    data _↦*_ : {τ : Tp} → [] |- τ → [] |- τ → Set where
      Done : {τ : Tp} {e : [] |- τ} → e ↦* e
      Step : {τ : Tp} {e1 e2 e3 : [] |- τ}
           → e1 ↦ e2  →  e2 ↦* e3
           → e1 ↦* e3

  {- Next, you will prove "very weak normalization".  The theorem is
     that any closed term *of base type b* evaluates to the constant c.
     No claims are made about terms of function type.
  -}
  module VeryWeakNormalization where

    open OpSem

    WN : (τ : Tp) → [] ⊢ τ → Set
    -- WN_τ(e) iff e ↦* c
    WN b e = e ↦* c
    -- WN_τ(e) iff for all e1 : τ1, if WN_τ1(e1) then WN_τ2(e e1)
    WN (τ1 ⇒ τ2) e = (e1 : [] ⊢ τ1) → WN τ1 e1 → WN τ2 (app e e1)

    -- extend WN to contexts and substitutions
    WNc : (Γ : Ctx) → [] ⊢c Γ → Set
    WNc [] θ = Unit
    WNc (τ :: Γ) (θ , e) = WNc Γ θ × WN τ e

    {- TASK 3 : show that the relation is closed under head expansion: -}
    head-expand : (τ : Tp) {e e' : [] ⊢ τ} → e ↦ e' → WN τ e' → WN τ e
    head-expand b e↦e' w = Step e↦e' w
    head-expand (τ1 ⇒ τ2) e↦e' w = λ e1 we1 → head-expand τ2 (Step/app e↦e') (w e1 we1)

    {- TASK 4 : prove the fundamental theorem -}
    fund : {Γ : Ctx} {τ : Tp} {θ : [] ⊢c Γ}
         → (e : Γ ⊢ τ)
         → WNc Γ θ
         → WN τ (subst θ e)
    fund c wθ = Done
    fund (v i0) (_ , we) = we
    fund (v (iS x)) (wθ , _) = fund (v x) wθ
    fund {_}{._}{θ} (lam{τ1}{τ2} e) wθ =
      λ e1 we1 → head-expand τ2 Step/β
        (transport (λ x → WN τ2 x) (subst-compose1 θ e1 e) (fund e (wθ , we1)))
    fund (app e e₁) wθ = fund e wθ _ (fund e₁ wθ)

    {- TASK 5 : conclude weak normalization at base type -}
    corollary : (e : [] ⊢ b) → e ↦* c
    corollary e = transport (\ x -> x ↦* _) (! subst-id) (fund e <>)

  {- TASK 6 : change the definition of the logical relation so that you also can conclude normalization
              at function type
  -}
  module WeakNormalization where

    open OpSem

    WN : (τ : Tp) → [] ⊢ τ → Set
    WN b e = e ↦* c
    WN (τ1 ⇒ τ2) e =
      Σ \ (e' : [] ,, τ1 ⊢ τ2) →
      (e ↦* lam e') × ((e1 : [] ⊢ τ1) → WN τ1 e1 → WN τ2 (subst1 e1 e'))

    -- extend WN to contexts and substitutions
    WNc : (Γ : Ctx) → [] ⊢c Γ → Set
    WNc [] θ = Unit
    WNc (τ :: Γ) (θ , e) = WNc Γ θ × WN τ e

    open RenamingAndSubstitution using (addvar)
    --- you will want to use
    --    addvar : {Γ Γ' : Ctx} {τ : Tp} → Γ ⊢c Γ' → (Γ ,, τ) ⊢c (Γ' ,, τ)

    head-expand : (τ : Tp) {e e' : [] ⊢ τ} → e ↦ e' → WN τ e' → WN τ e
    head-expand b e↦e' w = Step e↦e' w
    head-expand (τ1 ⇒ τ2) e↦e' (body , steps , wn) = body , Step e↦e' steps , wn

    -- Hint: you will need a couple of lemmas about ↦* that we didn't need above
    -- (I used three of them)

    head-expand* : {τ : Tp} {e e' : [] ⊢ τ} → e ↦* e' → WN τ e' → WN τ e
    head-expand* Done w = w
    head-expand* (Step s ss) w = head-expand _ s (head-expand* ss w)

    Step/app*  :{τ1 τ2 : Tp} {e e' : [] ⊢ τ1 ⇒ τ2} {e1 : [] ⊢ τ1}
             → e ↦* e'
             → (app e e1) ↦* (app e' e1)
    Step/app* Done = Done
    Step/app* (Step s ss) = (Step (Step/app s) (Step/app* ss))

    Step' : {τ : Tp} {e1 e2 e3 : [] ⊢ τ}
           → e1 ↦* e2  →  e2 ↦ e3
           → e1 ↦* e3
    Step' Done s = Step s Done
    Step' (Step s ss) s' = Step s (Step' ss s')

    fund : {Γ : Ctx} {τ : Tp} {θ : [] ⊢c Γ}
         → (e : Γ ⊢ τ)
         → WNc Γ θ
         → WN τ (subst θ e)
    fund c wθ = Done
    fund (v i0) (_ , we) = we
    fund (v (iS x)) (wθ , _) = fund (v x) wθ
    fund {_}{._}{θ} (lam{τ1}{τ2} e) wθ =
      subst (addvar θ) e , Done , (λ e1 we1 → transport (WN τ2) (subst-compose1 θ e1 e) (fund e (wθ , we1)))
    fund (app e e₁) wθ with fund e wθ
    ... | (body , reduction , wn) = head-expand* (Step' (Step/app* reduction) Step/β) (wn _ (fund e₁ wθ))

    {- TASK 6a -}
    corollary1 : (e : [] ⊢ b) → e ↦* c
    corollary1 e = transport (λ x → x ↦* _) (! subst-id) (fund e <>)

    {- TASK 6b -}
    corollary2 : {τ1 τ2 : Tp} (e : [] ⊢ τ1 ⇒ τ2) → Σ \(e' : _) → e ↦* (lam e')
    corollary2 e with (fund e <>)
    ... | (e' , steps , _) = e' , transport (λ x → x ↦* _) (! subst-id) steps

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda