text:
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Ordinals
module ODC {n : Level } (O : Ordinals {n} ) where

open import zf
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
open import  Relation.Binary.PropositionalEquality
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.Core

import OrdUtil
open import logic
open import nat
import OD
import ODUtil

open inOrdinal O
open OD O
open OD.OD
open OD._==_
open ODAxiom odAxiom
open ODUtil O

open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O

open HOD

open _∧_

postulate
  -- mimimul and x∋minimal is an Axiom of choice
  minimal : (x : HOD  ) → ¬ (x =h= od∅ )→ HOD
  -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
  x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
  -- minimality (may proved by ε-induction with LEM)
  minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (&  y) )

--
-- Axiom of choice in intutionistic logic implies the exclude middle
--     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
--

pred-od :  ( p : Set n )  → HOD
pred-od  p  = record { od = record { def = λ x → (x ≡ o∅) ∧ p } ;
   odmax = osuc o∅; <odmax = λ x → subst (λ k →  k o< osuc o∅) (sym (proj1 x)) <-osuc }

ppp :  { p : Set n } { a : HOD  } → pred-od p ∋ a → p
ppp  {p} {a} d = proj2 d

p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
p∨¬p  p with is-o∅ ( & (pred-od p ))
p∨¬p  p | yes eq = case2 (¬p eq) where
   ps = pred-od p
   eqo∅ : ps =h=  od∅  → & ps ≡  o∅
   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq))
   lemma : ps =h= od∅ → p → ⊥
   lemma eq p0 = ¬x<0  {& ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } )
   ¬p : (& ps ≡ o∅) → p → ⊥
   ¬p eq = lemma ( subst₂ (λ j k → j =h=  k ) *iso o∅≡od∅ ( o≡→== eq ))
p∨¬p  p | no ¬p = case1 (ppp  {p} {minimal ps (λ eq →  ¬p (eqo∅ eq))} lemma) where
   ps = pred-od p
   eqo∅ : ps =h=  od∅  → & ps ≡  o∅
   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq))
   lemma : ps ∋ minimal ps (λ eq →  ¬p (eqo∅ eq))
   lemma = x∋minimal ps (λ eq →  ¬p (eqo∅ eq))

decp : ( p : Set n ) → Dec p   -- assuming axiom of choice
decp  p with p∨¬p p
decp  p | case1 x = yes x
decp  p | case2 x = no x

∋-p : (A x : HOD ) → Dec ( A ∋ x )
∋-p A x with p∨¬p ( A ∋ x ) -- LEM
∋-p A x | case1 t  = yes t
∋-p A x | case2 t  = no (λ x → t x)

double-neg-eilm : {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
double-neg-eilm  {A} notnot with decp  A                         -- assuming axiom of choice
... | yes p = p
... | no ¬p = ⊥-elim ( notnot ¬p )

open _⊆_

power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where
   t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
   t1 = power→ A t PA∋t

OrdP : ( x : Ordinal  ) ( y : HOD  ) → Dec ( Ord x ∋ y )
OrdP  x y with trio< x (& y)
OrdP  x y | tri< a ¬b ¬c = no ¬c
OrdP  x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
OrdP  x y | tri> ¬a ¬b c = yes c

open import zfc

HOD→ZFC : ZFC
HOD→ZFC   = record {
    ZFSet = HOD
    ; _∋_ = _∋_
    ; _≈_ = _=h=_
    ; ∅  = od∅
    ; Select = Select
    ; isZFC = isZFC
 } where
    -- infixr  200 _∈_
    -- infixr  230 _∩_ _∪_
    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select
    isZFC = record {
       choice-func = choice-func ;
       choice = choice
     } where
         -- Axiom of choice ( is equivalent to the existence of minimal in our case )
         -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
         choice-func : (X : HOD  ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
         choice-func X {x} not X∋x = minimal x not
         choice : (X : HOD  ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A
         choice X {A} X∋A not = x∋minimal A not

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
-- Raw terms, weakening (renaming) and substitution.

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

module Definition.Untyped where

open import Tools.Nat
open import Tools.Product
open import Tools.List
import Tools.PropositionalEquality as PE

infixl 30 _∙_
infix 30 Π_▹_
infixr 22 _▹▹_
infixl 30 _ₛ•ₛ_ _•ₛ_ _ₛ•_
infix 25 _[_]
infix 25 _[_]↑

-- Typing contexts (snoc-lists, isomorphic to lists).

data Con (A : Set) : Set where
  ε   : Con A               -- Empty context.
  _∙_ : Con A → A → Con A  -- Context extension.

record GenT (A : Set) : Set where
  inductive
  constructor ⟦_,_⟧
  field
    l : Nat
    t : A

data Kind : Set where
  Ukind : Kind
  Pikind : Kind
  Natkind : Kind
  Lamkind : Kind
  Appkind : Kind
  Zerokind : Kind
  Suckind : Kind
  Natreckind : Kind

data Term : Set where
  var : (x : Nat) → Term
  gen : (k : Kind) (c : List (GenT Term)) → Term

-- The Grammar of our language.

-- We represent the expressions of our language as de Bruijn terms.
-- Variables are natural numbers interpreted as de Bruijn indices.
-- Π, lam, and natrec are binders.

-- Type constructors.
U      : Term                     -- Universe.
U = gen Ukind []

pattern Univ u = gen (Ukind u) []

Π_▹_   : (A B : Term)     → Term  -- Dependent function type (B is a binder).
Π A ▹ B = gen Pikind (⟦ 0 , A ⟧ ∷ ⟦ 1 , B ⟧ ∷ [])

ℕ      : Term                     -- Type of natural numbers.
ℕ = gen Natkind []

-- Lambda-calculus.
-- var    : (x : Nat)        → Term  -- Variable (de Bruijn index).
-- var = var

lam    : (t : Term)       → Term  -- Function abstraction (binder).
lam t = gen Lamkind (⟦ 1 , t ⟧ ∷ [])

_∘_    : (t u : Term)     → Term  -- Application.
t ∘ u = gen Appkind (⟦ 0 , t ⟧ ∷ ⟦ 0 , u ⟧ ∷ [])

-- Introduction and elimination of natural numbers.
zero   : Term                     -- Natural number zero.
zero = gen Zerokind []

suc    : (t : Term)       → Term  -- Successor.
suc t = gen Suckind (⟦ 0 , t ⟧ ∷ [])

natrec : (A t u v : Term) → Term  -- Recursor (A is a binder).
natrec A t u v = gen Natreckind (⟦ 1 , A ⟧ ∷ ⟦ 0 , t ⟧ ∷ ⟦ 0 , u ⟧ ∷ ⟦ 0 , v ⟧ ∷ [])

-- Injectivity of term constructors w.r.t. propositional equality.

-- If  Π F G = Π H E  then  F = H  and  G = E.

Π-PE-injectivity : ∀ {F G H E} → Π F ▹ G PE.≡ Π H ▹ E → F PE.≡ H × G PE.≡ E
Π-PE-injectivity PE.refl = PE.refl , PE.refl

-- If  suc n = suc m  then  n = m.

suc-PE-injectivity : ∀ {n m} → suc n PE.≡ suc m → n PE.≡ m
suc-PE-injectivity PE.refl = PE.refl

-- Neutral terms.

-- A term is neutral if it has a variable in head position.
-- The variable blocks reduction of such terms.

data Neutral : Term → Set where
  var     : ∀ n                     → Neutral (var n)
  ∘ₙ      : ∀ {k u}     → Neutral k → Neutral (k ∘ u)
  natrecₙ : ∀ {C c g k} → Neutral k → Neutral (natrec C c g k)

-- Weak head normal forms (whnfs).

-- These are the (lazy) values of our language.

data Whnf : Term → Set where

  -- Type constructors are whnfs.
  Uₙ    : Whnf U
  Πₙ    : ∀ {A B} → Whnf (Π A ▹ B)
  ℕₙ    : Whnf ℕ

  -- Introductions are whnfs.
  lamₙ  : ∀ {t} → Whnf (lam t)
  zeroₙ : Whnf zero
  sucₙ  : ∀ {t} → Whnf (suc t)

  -- Neutrals are whnfs.
  ne   : ∀ {n} → Neutral n → Whnf n

-- Whnf inequalities.

-- Different whnfs are trivially distinguished by propositional equality.
-- (The following statements are sometimes called "no-confusion theorems".)

U≢ℕ : U PE.≢ ℕ
U≢ℕ ()

U≢Π : ∀ {F G} → U PE.≢ Π F ▹ G
U≢Π ()

U≢ne : ∀ {K} → Neutral K → U PE.≢ K
U≢ne () PE.refl

ℕ≢Π : ∀ {F G} → ℕ PE.≢ Π F ▹ G
ℕ≢Π ()

ℕ≢ne : ∀ {K} → Neutral K → ℕ PE.≢ K
ℕ≢ne () PE.refl

Π≢ne : ∀ {F G K} → Neutral K → Π F ▹ G PE.≢ K
Π≢ne () PE.refl

zero≢suc : ∀ {n} → zero PE.≢ suc n
zero≢suc ()

zero≢ne : ∀ {k} → Neutral k → zero PE.≢ k
zero≢ne () PE.refl

suc≢ne : ∀ {n k} → Neutral k → suc n PE.≢ k
suc≢ne () PE.refl

-- Several views on whnfs (note: not recursive).

-- A whnf of type ℕ is either zero, suc t, or neutral.

data Natural : Term → Set where
  zeroₙ :                     Natural zero
  sucₙ  : ∀ {t}             → Natural (suc t)
  ne    : ∀ {n} → Neutral n → Natural n

-- A (small) type in whnf is either Π A B, ℕ, or neutral.
-- Large types could also be U.

data Type : Term → Set where
  Πₙ : ∀ {A B} → Type (Π A ▹ B)
  ℕₙ : Type ℕ
  ne : ∀{n} → Neutral n → Type n

-- A whnf of type Π A B is either lam t or neutral.

data Function : Term → Set where
  lamₙ : ∀{t} → Function (lam t)
  ne : ∀{n} → Neutral n → Function n

-- These views classify only whnfs.
-- Natural, Type, and Function are a subsets of Whnf.

naturalWhnf : ∀ {n} → Natural n → Whnf n
naturalWhnf sucₙ = sucₙ
naturalWhnf zeroₙ = zeroₙ
naturalWhnf (ne x) = ne x

typeWhnf : ∀ {A} → Type A → Whnf A
typeWhnf Πₙ = Πₙ
typeWhnf ℕₙ = ℕₙ
typeWhnf (ne x) = ne x

functionWhnf : ∀ {f} → Function f → Whnf f
functionWhnf lamₙ = lamₙ
functionWhnf (ne x) = ne x

------------------------------------------------------------------------
-- Weakening

-- In the following we define untyped weakenings η : Wk.
-- The typed form could be written η : Γ ≤ Δ with the intention
-- that η transport a term t living in context Δ to a context Γ
-- that can bind additional variables (which cannot appear in t).
-- Thus, if Δ ⊢ t : A and η : Γ ≤ Δ then Γ ⊢ wk η t : wk η A.
--
-- Even though Γ is "larger" than Δ we write Γ ≤ Δ to be conformant
-- with subtyping A ≤ B.  With subtyping, relation Γ ≤ Δ could be defined as
-- ``for all x ∈ dom(Δ) have Γ(x) ≤ Δ(x)'' (in the sense of subtyping)
-- and this would be the natural extension of weakenings.

data Wk : Set where
  id    : Wk        -- η : Γ ≤ Γ.
  step  : Wk  → Wk  -- If η : Γ ≤ Δ then step η : Γ∙A ≤ Δ.
  lift  : Wk  → Wk  -- If η : Γ ≤ Δ then lift η : Γ∙A ≤ Δ∙A.

-- Composition of weakening.
-- If η : Γ ≤ Δ and η′ : Δ ≤ Φ then η • η′ : Γ ≤ Φ.

infixl 30 _•_

_•_                :  Wk → Wk → Wk
id      • η′       =  η′
step η  • η′       =  step  (η • η′)
lift η  • id       =  lift  η
lift η  • step η′  =  step  (η • η′)
lift η  • lift η′  =  lift  (η • η′)

repeat : {A : Set} → (A → A) → A → Nat → A
repeat f a 0 = a
repeat f a (1+ n) = f (repeat f a n)

-- Weakening of variables.
-- If η : Γ ≤ Δ and x ∈ dom(Δ) then wkVar ρ x ∈ dom(Γ).

wkVar : (ρ : Wk) (n : Nat) → Nat
wkVar id       n        = n
wkVar (step ρ) n        = 1+ (wkVar ρ n)
wkVar (lift ρ) 0    = 0
wkVar (lift ρ) (1+ n) = 1+ (wkVar ρ n)

  -- Weakening of terms.
  -- If η : Γ ≤ Δ and Δ ⊢ t : A then Γ ⊢ wk η t : wk η A.

mutual
  wkGen : (ρ : Wk) (g : List (GenT Term)) → List (GenT Term)
  wkGen ρ [] = []
  wkGen ρ (⟦ l , t ⟧ ∷ g) = ⟦ l , (wk (repeat lift ρ l) t) ⟧ ∷ wkGen ρ g

  wk : (ρ : Wk) (t : Term) → Term
  wk ρ (var x) = var (wkVar ρ x)
  wk ρ (gen x c) = gen x (wkGen ρ c)

-- Adding one variable to the context requires wk1.
-- If Γ ⊢ t : B then Γ∙A ⊢ wk1 t : wk1 B.

wk1 : Term → Term
wk1 = wk (step id)

-- Weakening of a neutral term.

wkNeutral : ∀ {t} ρ → Neutral t → Neutral (wk ρ t)
wkNeutral ρ (var n)    = var (wkVar ρ n)
wkNeutral ρ (∘ₙ n)    = ∘ₙ (wkNeutral ρ n)
wkNeutral ρ (natrecₙ n) = natrecₙ (wkNeutral ρ n)

-- Weakening can be applied to our whnf views.

wkNatural : ∀ {t} ρ → Natural t → Natural (wk ρ t)
wkNatural ρ sucₙ    = sucₙ
wkNatural ρ zeroₙ   = zeroₙ
wkNatural ρ (ne x) = ne (wkNeutral ρ x)

wkType : ∀ {t} ρ → Type t → Type (wk ρ t)
wkType ρ Πₙ      = Πₙ
wkType ρ ℕₙ      = ℕₙ
wkType ρ (ne x) = ne (wkNeutral ρ x)

wkFunction : ∀ {t} ρ → Function t → Function (wk ρ t)
wkFunction ρ lamₙ    = lamₙ
wkFunction ρ (ne x) = ne (wkNeutral ρ x)

wkWhnf : ∀ {t} ρ → Whnf t → Whnf (wk ρ t)
wkWhnf ρ Uₙ      = Uₙ
wkWhnf ρ Πₙ      = Πₙ
wkWhnf ρ ℕₙ      = ℕₙ
wkWhnf ρ lamₙ    = lamₙ
wkWhnf ρ zeroₙ   = zeroₙ
wkWhnf ρ sucₙ    = sucₙ
wkWhnf ρ (ne x) = ne (wkNeutral ρ x)

-- Non-dependent version of Π.

_▹▹_ : Term → Term → Term
A ▹▹ B = Π A ▹ wk1 B

------------------------------------------------------------------------
-- Substitution

-- The substitution operation  subst σ t  replaces the free de Bruijn indices
-- of term t by chosen terms as specified by σ.

-- The substitution σ itself is a map from natural numbers to terms.

Subst : Set
Subst = Nat → Term

-- Given closed contexts ⊢ Γ and ⊢ Δ,
-- substitutions may be typed via Γ ⊢ σ : Δ meaning that
-- Γ ⊢ σ(x) : (subst σ Δ)(x) for all x ∈ dom(Δ).
--
-- The substitution operation is then typed as follows:
-- If Γ ⊢ σ : Δ and Δ ⊢ t : A, then Γ ⊢ subst σ t : subst σ A.
--
-- Although substitutions are untyped, typing helps us
-- to understand the operation on substitutions.

-- We may view σ as the infinite stream σ 0, σ 1, ...

-- Extract the substitution of the first variable.
--
-- If Γ ⊢ σ : Δ∙A  then Γ ⊢ head σ : subst σ A.

head : Subst → Term
head σ = σ 0

-- Remove the first variable instance of a substitution
-- and shift the rest to accommodate.
--
-- If Γ ⊢ σ : Δ∙A then Γ ⊢ tail σ : Δ.

tail : Subst → Subst
tail σ n = σ (1+ n)

-- Substitution of a variable.
--
-- If Γ ⊢ σ : Δ then Γ ⊢ substVar σ x : (subst σ Δ)(x).

substVar : (σ : Subst) (x : Nat) → Term
substVar σ x = σ x

-- Identity substitution.
-- Replaces each variable by itself.
--
-- Γ ⊢ idSubst : Γ.

idSubst : Subst
idSubst = var

-- Weaken a substitution by one.
--
-- If Γ ⊢ σ : Δ then Γ∙A ⊢ wk1Subst σ : Δ.

wk1Subst : Subst → Subst
wk1Subst σ x = wk1 (σ x)

-- Lift a substitution.
--
-- If Γ ⊢ σ : Δ then Γ∙A ⊢ liftSubst σ : Δ∙A.

liftSubst : (σ : Subst) → Subst
liftSubst σ 0    = var 0
liftSubst σ (1+ x) = wk1Subst σ x

-- Transform a weakening into a substitution.
--
-- If ρ : Γ ≤ Δ then Γ ⊢ toSubst ρ : Δ.

toSubst : Wk → Subst
toSubst pr x = var (wkVar pr x)

-- Apply a substitution to a term.
--
-- If Γ ⊢ σ : Δ and Δ ⊢ t : A then Γ ⊢ subst σ t : subst σ A.

mutual
  substGen : (σ : Subst) (g : List (GenT Term)) → List (GenT Term)
  substGen σ [] = []
  substGen σ (⟦ l , t ⟧ ∷ g) = ⟦ l , (subst (repeat liftSubst σ l) t) ⟧ ∷ substGen σ g

  subst : (σ : Subst) (t : Term) → Term
  subst σ (var x) = substVar σ x
  subst σ (gen x c) = gen x (substGen σ c)

-- Extend a substitution by adding a term as
-- the first variable substitution and shift the rest.
--
-- If Γ ⊢ σ : Δ and Γ ⊢ t : subst σ A then Γ ⊢ consSubst σ t : Δ∙A.

consSubst : Subst → Term → Subst
consSubst σ t 0    = t
consSubst σ t (1+ n) = σ n

-- Singleton substitution.
--
-- If Γ ⊢ t : A then Γ ⊢ sgSubst t : Γ∙A.

sgSubst : Term → Subst
sgSubst = consSubst idSubst

-- Compose two substitutions.
--
-- If Γ ⊢ σ : Δ and Δ ⊢ σ′ : Φ then Γ ⊢ σ ₛ•ₛ σ′ : Φ.

_ₛ•ₛ_ : Subst → Subst → Subst
_ₛ•ₛ_ σ σ′ x = subst σ (σ′ x)

-- Composition of weakening and substitution.
--
--  If ρ : Γ ≤ Δ and Δ ⊢ σ : Φ then Γ ⊢ ρ •ₛ σ : Φ.

_•ₛ_ : Wk → Subst → Subst
_•ₛ_ ρ σ x = wk ρ (σ x)

--  If Γ ⊢ σ : Δ and ρ : Δ ≤ Φ then Γ ⊢ σ ₛ• ρ : Φ.

_ₛ•_ : Subst → Wk → Subst
_ₛ•_ σ ρ x = σ (wkVar ρ x)

-- Substitute the first variable of a term with an other term.
--
-- If Γ∙A ⊢ t : B and Γ ⊢ s : A then Γ ⊢ t[s] : B[s].

_[_] : (t : Term) (s : Term) → Term
t [ s ] = subst (sgSubst s) t

-- Substitute the first variable of a term with an other term,
-- but let the two terms share the same context.
--
-- If Γ∙A ⊢ t : B and Γ∙A ⊢ s : A then Γ∙A ⊢ t[s]↑ : B[s]↑.

_[_]↑ : (t : Term) (s : Term) → Term
t [ s ]↑ = subst (consSubst (wk1Subst idSubst) s) t

ext: agda

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
module Productive where

open import Stream
open import Size
open import Data.Maybe
open import Data.Product
open import Relation.Binary.PropositionalEquality as P

PStream : Set → Set
PStream A = Stream (Maybe A)

mutual
  record Productive {A : Set} (s : PStream A) : Set where
    coinductive
    field
      step : EventualOutput s

  data EventualOutput {A : Set} (s : PStream A) : Set where
    here  : (a : A) → s .hd ≡ just a  → Productive (s .tl)     → EventualOutput s
    there :           s .hd ≡ nothing → EventualOutput (s .tl) → EventualOutput s

open Productive public

ProdStr : Set → Set
ProdStr A = Σ[ s ∈ PStream A ] (Productive s)

injS : {A : Set} → Stream A → ProdStr A
injS {A} s = (toPStream s , prod s)
  where
    toPStream : Stream {∞} A → PStream A
    toPStream s .hd = just (s .hd)
    toPStream s .tl = toPStream (s .tl)

    prod : (s : Stream A) → Productive (toPStream s)
    prod s .step = here (s .hd) refl (prod (s .tl))

extract  : {A : Set} → ProdStr A → Stream A
extract (s , p) = extr s p
  where
    extr  : {A : Set} → (s : PStream A) → Productive s → Stream A
    extrμ  : {A : Set} → (s : PStream A) → EventualOutput s → Stream A

    extr {A} s p = extrμ s (p .step)

    extrμ {A} s (here a q p') .hd = a
    extrμ {A} s (here a q p') .tl = extr (s .tl) p'
    extrμ {A} s (there x p')      = extrμ (s .tl) p'

zipS : ∀{A} → ProdStr A → ProdStr A → ProdStr A
zipS {A} (s , p) (t , q) = (z s t , pz p q)
  where
    z : PStream A → PStream A → PStream A
    cz : Maybe A → PStream A → PStream A → PStream A

    z s t = cz (s .hd) (s .tl) t

    cz (just a) s' t .hd = just a
    cz (just a) s' t .tl = z t s'
    cz nothing  s' t .hd = nothing
    cz nothing  s' t .tl = cz (s' .hd) (s' .tl) t

    pz : {s t : PStream A} → Productive s → Productive t → Productive (z s t)
    pcz : {s t : PStream A} → Productive s → Productive t →
          Productive (cz (s .hd) (s .tl) t)
    pczE : {s t : PStream A} → EventualOutput s → Productive t →
           EventualOutput (cz (s .hd) (s .tl) t)
    pz p q = pcz p q

    pcz p q .step = pczE (p .step) q

    pczE {s} (here a s₀≡a p')  q with s .hd
    pczE {s} (here .a refl p') q | just a = here a refl (pz q p')
    pczE {s} (here a () p')    q | nothing
    pczE {s} (there s₀≡∗ p')   q with s .hd
    pczE {s} (there () p')     q | just a
    pczE {s} (there refl p')   q | nothing = there refl (pczE p' q)

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


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

module Relation.Ternary.Separation.Construct.Product where

open import Level
open import Data.Product

open import Relation.Unary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Ternary.Separation
open import Data.Product.Relation.Binary.Pointwise.NonDependent

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

  _×-⊎_ : RawSep C₁ → RawSep C₂ → RawSep (C₁ × C₂)
  R₁ ×-⊎ R₂ =
    let
      module R₁ = RawSep R₁
      module R₂ = RawSep R₂
    in record
    { _⊎_≣_ = λ Φ₁ Φ₂ Φ →
        (proj₁ Φ₁) R₁.⊎ (proj₁ Φ₂) ≣ proj₁ Φ
      × (proj₂ Φ₁) R₂.⊎ (proj₂ Φ₂) ≣ proj₂ Φ }

  instance ×-rawsep : ⦃ _ : RawSep C₁ ⦄ ⦃ _ : RawSep C₂ ⦄ → RawSep (C₁ × C₂)
  ×-rawsep ⦃ R₁ ⦄ ⦃ R₂ ⦄ = R₁ ×-⊎ R₂

module _
  {ℓ₁ ℓ₂} {C₁ : Set ℓ₁} {C₂ : Set ℓ₂}
  {{R₁ : RawSep C₁}} {{R₂ : RawSep C₂}}
  ⦃ s₁ : IsSep R₁ ⦄ ⦃ s₂ : IsSep R₂ ⦄
  where

  instance ×-isSep : IsSep (R₁ ×-⊎ R₂)
  ×-isSep = record
    { ⊎-comm  = λ where (l , r) → ⊎-comm l , ⊎-comm r
    ; ⊎-assoc = λ where
      (l₁  , r₁) (l₂ , r₂) →
        let
          _ , l₃ , l₄ = ⊎-assoc l₁ l₂
          _ , r₃ , r₄ = ⊎-assoc r₁ r₂
        in -, (l₃ , r₃) , l₄ , r₄ }

module _
  {ℓ₁ ℓ₂} {C₁ : Set ℓ₁} {C₂ : Set ℓ₂}
  {{R₁ : RawSep C₁}} {{R₂ : RawSep C₂}} {u₁ u₂}
  ⦃ s₁ : IsUnitalSep R₁ u₁ ⦄ ⦃ s₂ : IsUnitalSep R₂ u₂ ⦄
  where

  instance ×-isUnitalSep : IsUnitalSep ×-rawsep (u₁ , u₂)
  ×-isUnitalSep = record
    { isSep = ×-isSep
    ; ⊎-idˡ = ⊎-idˡ , ⊎-idˡ
    ; ⊎-id⁻ˡ = λ where
      (fst , snd) → cong₂ _,_ (⊎-id⁻ˡ fst) (⊎-id⁻ˡ snd)
    }

  instance _×-ε-separation_ : UnitalSep _
  _×-ε-separation_ = record
    { isUnitalSep = ×-isUnitalSep }

module _
  {ℓ₁ ℓ₂}
  ⦃ s₁ : Separation ℓ₁ ⦄ ⦃ s₂ : Separation ℓ₂ ⦄
  where

  private
    module S₁ = Separation s₁
    module S₂ = Separation s₂

  ×-separation : Separation _
  ×-separation = record
    { isSep = ×-isSep {{ _ }} {{ _ }} ⦃ Separation.isSep s₁ ⦄ ⦃ Separation.isSep s₂ ⦄ }

module _
  {ℓ₁ ℓ₂}
  {C₁ : Set ℓ₁} {C₂ : Set ℓ₂}
  ⦃ sep₁ : RawSep C₁ ⦄ ⦃ sep₂ : RawSep C₂ ⦄
  ⦃ s₁ : IsConcattative sep₁ ⦄ ⦃ s₂ : IsConcattative sep₂ ⦄
  where

  private
    module S₁ = IsConcattative s₁
    module S₂ = IsConcattative s₂

  instance ×-concat : IsConcattative ×-rawsep
  ×-concat = record
    { _∙_ = (λ where (a , b) (c , d) → (a S₁.∙ c , b S₂.∙ d))
    ; ⊎-∙ₗ = λ where (p , q) → ⊎-∙ₗ p , ⊎-∙ₗ q }

{- Some useful type-formers for this instance -}
module _ {ℓ} {A : Set ℓ} {{ r : RawSep A }} {u} {{s : IsUnitalSep r u}} where

  data Π₁ {p} (P : Pred A p) : Pred (A × A) (ℓ ⊔ p) where
    fst : ∀ {a} → P a → Π₁ P (a , ε)

  data Π₂ {p} (P : Pred A p) : Pred (A × A) (ℓ ⊔ p) where
    snd : ∀ {a} → P a → Π₂ P (ε , a)


text:
module syntax-util where

open import cedille-types
open import general-util
open import constants
open import json

posinfo-gen : posinfo
posinfo-gen = "generated"

pi-gen = posinfo-gen

first-position : posinfo
first-position = "1"

dummy-var : var
dummy-var = "_dummy"

id-term : term
id-term = Lam ff "x" nothing (Var "x")

tt-term = Lam ff "t" nothing (Lam ff "f" nothing (Var "t"))
ff-term = Lam ff "t" nothing (Lam ff "f" nothing (Var "f"))

compileFailType : type
compileFailType = TpAbs tt "X" (Tkk KdStar) (TpVar "X")

qualif-info : Set
qualif-info = var × args

qualif : Set
qualif = trie qualif-info

tag : Set
tag = string × json

tagged-val : Set
tagged-val = string × rope × 𝕃 tag

tags-to-json : 𝕃 tag → 𝕃 json
tags-to-json [] = []
tags-to-json ts = [ json-object ts ]

tagged-val-to-json : tagged-val → string × json
tagged-val-to-json (t , v , tags) = t , json-array (json-rope v :: tags-to-json tags)

tagged-vals-to-json : 𝕃 tagged-val → json
tagged-vals-to-json = json-object ∘ map tagged-val-to-json

make-tag : (name : string) → (values : 𝕃 tag) → (start : ℕ) → (end : ℕ) → tag
make-tag name vs start end = name , json-object (("start" , json-nat start) :: ("end" , json-nat end) :: vs)

posinfo-to-ℕ : posinfo → ℕ
posinfo-to-ℕ pi with string-to-ℕ pi
posinfo-to-ℕ pi | just n = n
posinfo-to-ℕ pi | nothing = 0 -- should not happen

posinfo-plus : posinfo → ℕ → posinfo
posinfo-plus pi n = ℕ-to-string (posinfo-to-ℕ pi + n)

posinfo-plus-str : posinfo → string → posinfo
posinfo-plus-str pi s = posinfo-plus pi (string-length s)

-- qualify variable by module name
_#_ : string → string → string
fn # v = fn ^ qual-global-str ^  v

_%_ : posinfo → var → string
pi % v = pi ^ qual-local-str ^ v

compileFail : var
compileFail = "compileFail"
compileFail-qual = "" % compileFail

tk-is-type : tpkd → 𝔹
tk-is-type = either-else (const tt) (const ff)

tT-is-term : tmtp → 𝔹
tT-is-term = either-else (const tt) (const ff)

tk-start-pos : ex-tk → posinfo
term-start-pos : ex-tm → posinfo
type-start-pos : ex-tp → posinfo
kind-start-pos : ex-kd → posinfo

term-start-pos (ExApp t x t₁) = term-start-pos t
term-start-pos (ExAppTp t tp) = term-start-pos t
term-start-pos (ExHole pi) = pi
term-start-pos (ExLam pi x _ x₁ x₂ t) = pi
term-start-pos (ExLet pi _ _ _) = pi
term-start-pos (ExOpen pi _ _ _ _) = pi
term-start-pos (ExParens pi t pi') = pi
term-start-pos (ExVar pi x₁) = pi
term-start-pos (ExBeta pi _ _) = pi
term-start-pos (ExIotaPair pi _ _ _ _) = pi
term-start-pos (ExIotaProj t _ _) = term-start-pos t
term-start-pos (ExEpsilon pi _ _ _) = pi
term-start-pos (ExPhi pi _ _ _ _) = pi
term-start-pos (ExRho pi _ _ _ _ _) = pi
term-start-pos (ExChi pi _ _) = pi
term-start-pos (ExDelta pi _ _) = pi
term-start-pos (ExSigma pi _) = pi
term-start-pos (ExTheta pi _ _ _) = pi
term-start-pos (ExMu pi _ _ _ _ _ _) = pi

type-start-pos (ExTpAbs pi _ _ _ _ _) = pi
type-start-pos (ExTpLam pi _ _ _ _) = pi
type-start-pos (ExTpIota pi _ _ _ _) = pi
type-start-pos (ExTpApp t t₁) = type-start-pos t
type-start-pos (ExTpAppt t x) = type-start-pos t
type-start-pos (ExTpArrow t _ t₁) = type-start-pos t
type-start-pos (ExTpEq pi _ _ pi') = pi
type-start-pos (ExTpParens pi _ pi') = pi
type-start-pos (ExTpVar pi x₁) = pi
type-start-pos (ExTpNoSpans t _) = type-start-pos t -- we are not expecting this on input
type-start-pos (ExTpHole pi) = pi --ACG
type-start-pos (ExTpLet pi _ _) = pi

kind-start-pos (ExKdAbs pi _ x x₁ k) = pi
kind-start-pos (ExKdArrow atk k₁) = tk-start-pos atk
kind-start-pos (ExKdHole pi) = pi
kind-start-pos (ExKdParens pi k pi') = pi
kind-start-pos (ExKdVar pi x₁ _) = pi
kind-start-pos (ExKdStar pi) = pi

tk-start-pos (ExTkt t) = type-start-pos t
tk-start-pos (ExTkk k) = kind-start-pos k

term-end-pos : ex-tm → posinfo
type-end-pos : ex-tp → posinfo
kind-end-pos : ex-kd → posinfo
tk-end-pos : ex-tk → posinfo
lterms-end-pos : posinfo → 𝕃 lterm → posinfo
args-end-pos : posinfo → ex-args → posinfo
arg-end-pos : ex-arg → posinfo
kvar-end-pos : posinfo → var → ex-args → posinfo
params-end-pos : posinfo → ex-params → posinfo
param-end-pos : ex-param → posinfo

term-end-pos (ExApp t x t') = term-end-pos t'
term-end-pos (ExAppTp t tp) = type-end-pos tp
term-end-pos (ExHole pi) = posinfo-plus pi 1
term-end-pos (ExLam pi x _ x₁ x₂ t) = term-end-pos t
term-end-pos (ExLet _ _ _ t) = term-end-pos t
term-end-pos (ExOpen pi _ _ _ t) = term-end-pos t
term-end-pos (ExParens pi t pi') = pi'
term-end-pos (ExVar pi x) = posinfo-plus-str pi x
term-end-pos (ExBeta pi _ (just (PosTm t pi'))) = pi'
term-end-pos (ExBeta pi (just (PosTm t pi')) nothing) = pi'
term-end-pos (ExBeta pi nothing nothing) = posinfo-plus pi 1
term-end-pos (ExIotaPair _ _ _ _ pi) = pi
term-end-pos (ExIotaProj _ _ pi) = pi
term-end-pos (ExEpsilon pi _ _ t) = term-end-pos t
term-end-pos (ExPhi _ _ _ _ pi) = pi
term-end-pos (ExRho pi _ _ _ t t') = term-end-pos t'
term-end-pos (ExChi pi T t') = term-end-pos t'
term-end-pos (ExDelta pi oT t) = term-end-pos t
term-end-pos (ExSigma pi t) = term-end-pos t
term-end-pos (ExTheta _ _ t ls) = lterms-end-pos (term-end-pos t) ls
term-end-pos (ExMu _ _ _ _ _ _ pi) = pi

type-end-pos (ExTpAbs pi _ _ _ _ t) = type-end-pos t
type-end-pos (ExTpLam _ _ _ _ t) = type-end-pos t
type-end-pos (ExTpIota _ _ _ _ tp) = type-end-pos tp
type-end-pos (ExTpApp t t') = type-end-pos t'
type-end-pos (ExTpAppt t x) = term-end-pos x
type-end-pos (ExTpArrow t _ t') = type-end-pos t'
type-end-pos (ExTpEq pi _ _ pi') = pi'
type-end-pos (ExTpParens pi _ pi') = pi'
type-end-pos (ExTpVar pi x) = posinfo-plus-str pi x
type-end-pos (ExTpHole pi) = posinfo-plus pi 1
type-end-pos (ExTpNoSpans t pi) = pi
type-end-pos (ExTpLet _ _ t) = type-end-pos t

kind-end-pos (ExKdAbs pi _ x x₁ k) = kind-end-pos k
kind-end-pos (ExKdArrow atk k) = kind-end-pos k
kind-end-pos (ExKdHole pi) = posinfo-plus pi 1
kind-end-pos (ExKdParens pi k pi') = pi'
kind-end-pos (ExKdVar pi x ys) = args-end-pos (posinfo-plus-str pi x) ys
kind-end-pos (ExKdStar pi) = posinfo-plus pi 1

tk-end-pos (ExTkt T) = type-end-pos T
tk-end-pos (ExTkk k) = kind-end-pos k

args-end-pos pi (x :: ys) = args-end-pos (arg-end-pos x) ys
args-end-pos pi [] = pi

arg-end-pos (ExTmArg me t) = term-end-pos t
arg-end-pos (ExTpArg T) = type-end-pos T

kvar-end-pos pi v = args-end-pos (posinfo-plus-str pi v)

params-end-pos pi [] = pi
params-end-pos pi (p :: ps) = params-end-pos (param-end-pos p) ps

param-end-pos (ExParam pi me pi' x atk pi'') = pi''

lterms-end-pos pi [] = pi
lterms-end-pos pi (Lterm _ t :: ls) = lterms-end-pos (term-end-pos t) ls

{- return the end position of the given term if it is there, otherwise
   the given posinfo -}
optTerm-end-pos : posinfo → maybe pos-tm → posinfo
optTerm-end-pos pi nothing = pi
optTerm-end-pos pi (just (PosTm x x₁)) = x₁

optTerm-end-pos-beta : posinfo → maybe pos-tm → maybe pos-tm → posinfo
optTerm-end-pos-beta pi _ (just (PosTm x pi')) = pi'
optTerm-end-pos-beta pi (just (PosTm x pi')) nothing = pi'
optTerm-end-pos-beta pi nothing nothing = posinfo-plus pi 1

optAs-or : maybe import-as → posinfo → var → posinfo × var
optAs-or nothing pi x = pi , x
optAs-or (just (ImportAs pi x)) _ _ = pi , x

TpApp-tk : type → var → tpkd → type
TpApp-tk tp x (Tkk _) = TpAppTp tp (TpVar x)
TpApp-tk tp x (Tkt _) = TpAppTm tp (Var x)

-- checking-sythesizing enum
data checking-mode : Set where
  checking : checking-mode
  synthesizing : checking-mode
  untyped : checking-mode

maybe-to-checking : {A : Set} → maybe A → checking-mode
maybe-to-checking (just _) = checking
maybe-to-checking nothing = synthesizing

eq-checking-mode : (m₁ m₂ : checking-mode) → 𝔹
eq-checking-mode checking checking = tt
eq-checking-mode synthesizing synthesizing = tt
eq-checking-mode untyped untyped = tt
eq-checking-mode _ _ = ff

------------------------------------------------------
-- functions intended for building terms for testing
------------------------------------------------------

mlam : var → term → term
mlam x t = Lam ff x nothing t

mall : var → tpkd → type → type
mall = TpAbs tt

mpi : var → tpkd → type → type
mpi  = TpAbs ff

imps-to-cmds : imports → cmds
imps-to-cmds = map CmdImport

cmds-to-imps : cmds → imports
cmds-to-imps [] = []
cmds-to-imps (CmdImport i :: cs) = i :: cmds-to-imps cs
cmds-to-imps (_ :: cs) = cmds-to-imps cs

ex-cmds-to-imps : ex-cmds → ex-imports
ex-cmds-to-imps [] = []
ex-cmds-to-imps (ExCmdImport i :: cs) = i :: ex-cmds-to-imps cs
ex-cmds-to-imps (_ :: cs) = ex-cmds-to-imps cs

split-var-h : 𝕃 char → 𝕃 char × 𝕃 char
split-var-h [] = [] , []
split-var-h (qual-global-chr :: xs) = [] , xs
split-var-h (x :: xs) with split-var-h xs
... | xs' , ys = (x :: xs') , ys

split-var : var → var × var
split-var v with split-var-h (reverse (string-to-𝕃char v))
... | xs , ys = 𝕃char-to-string (reverse ys) , 𝕃char-to-string (reverse xs)

var-suffix : var → maybe var
var-suffix v with split-var v
... | "" , _ = nothing
... | _ , sfx = just sfx

-- unique qualif domain prefixes
qual-pfxs : qualif → 𝕃 var
qual-pfxs q = uniq (prefixes (trie-strings q))
  where
  uniq : 𝕃 var → 𝕃 var
  uniq vs = stringset-strings (stringset-insert* empty-stringset vs)
  prefixes : 𝕃 var → 𝕃 var
  prefixes [] = []
  prefixes (v :: vs) with split-var v
  ... | "" , sfx = vs
  ... | pfx , sfx = pfx :: prefixes vs

unqual-prefix : qualif → 𝕃 var → var → var → var
unqual-prefix q [] sfx v = v
unqual-prefix q (pfx :: pfxs) sfx v
  with trie-lookup q (pfx # sfx)
... | just (v' , _) = if v =string v' then pfx # sfx else v
... | nothing = v

unqual-bare : qualif → var → var → var
unqual-bare q sfx v with trie-lookup q sfx
... | just (v' , _) = if v =string v' then sfx else v
... | nothing = v

unqual-local : var → var
unqual-local v = f' (string-to-𝕃char v) where
  f : 𝕃 char → maybe (𝕃 char)
  f [] = nothing
  f ('@' :: t) = f t maybe-or just t
  f (h :: t) = f t
  f' : 𝕃 char → string
  f' (meta-var-pfx :: t) = maybe-else' (f t) v (𝕃char-to-string ∘ _::_ meta-var-pfx)
  f' t = maybe-else' (f t) v 𝕃char-to-string

unqual-all : qualif → var → string
unqual-all q v with var-suffix v
... | nothing = v
... | just sfx = unqual-bare q sfx (unqual-prefix q (qual-pfxs q) sfx v)

-- Given a qualified variable and a function that renames it,
-- we strip away the qualification prefix, call the function,
-- then prepend the prefix to the result
reprefix : (var → var) → var → var
reprefix f x =
  maybe-else' (pfx (string-to-𝕃char x) [])
    (f x) $ uncurry λ p s → p ^ f s where
  ret : 𝕃 char → 𝕃 char → maybe (var × var)
  ret pfx sfx = just (𝕃char-to-string (reverse pfx) , 𝕃char-to-string sfx)
  pfx : 𝕃 char → 𝕃 char → maybe (var × var)
  pfx (qual-global-chr :: xs) acc =
    pfx xs (qual-global-chr :: acc) maybe-or ret (qual-global-chr :: acc) xs
  pfx (qual-local-chr :: xs) acc =
    pfx xs (qual-local-chr :: acc) maybe-or ret (qual-local-chr :: acc) xs
  pfx (x :: xs) acc = pfx xs (x :: acc)
  pfx [] pfx = nothing

data-to/ = reprefix ("to/" ^_)
data-Is/ = reprefix ("Is/" ^_)
data-is/ = reprefix ("is/" ^_)
mu-Type/ = reprefix ("Type/" ^_)
mu-isType/ = reprefix ("isType/" ^_)
mu-isType/' = reprefix ("is" ^_)
-- Generated during elaboration
data-TypeF/ = reprefix ("F/" ^_)
data-IndF/ = reprefix ("IndF/" ^_)
data-fmap/ = reprefix ("fmap/" ^_)
--

num-gt : num → ℕ → 𝕃 string
num-gt n n' = maybe-else [] (λ n'' → if n'' > n' then [ n ] else []) (string-to-ℕ n)
nums-gt : 𝕃 num → ℕ → 𝕃 string
nums-gt [] n' = []
nums-gt (n :: ns) n' =
  maybe-else [] (λ n'' → if n'' > n' || iszero n'' then [ n ] else []) (string-to-ℕ n)
  ++ nums-gt ns n'

nums-to-stringset : 𝕃 num → stringset × 𝕃 string {- Repeated numbers -}
nums-to-stringset [] = empty-stringset , []
nums-to-stringset (n :: ns) with nums-to-stringset ns
...| ss , rs = if stringset-contains ss n
  then ss , n :: rs
  else stringset-insert ss n , rs

optNums-to-stringset : maybe (𝕃 num) → maybe stringset × (ℕ → maybe string)
optNums-to-stringset nothing = nothing , λ _ → nothing
optNums-to-stringset (just ns) with nums-to-stringset ns
...| ss , [] = just ss , λ n → case nums-gt ns n of λ where
  [] → nothing
  ns-g → just ("Occurrences not found: " ^ 𝕃-to-string id ", " ns-g ^ " (total occurrences: " ^ ℕ-to-string n ^ ")")
...| ss , rs = just ss , λ n →
  just ("The list of occurrences contains the following repeats: " ^ 𝕃-to-string id ", " rs)

def-var : ex-def → var
def-var (ExDefTerm _ x _ _) = x
def-var (ExDefType _ x _ _) = x

-- expression descriptor
data exprd : Set where
  TERM : exprd
  TYPE : exprd
  KIND : exprd
--  TPKD : exprd

⟦_⟧ : exprd → Set
⟦ TERM ⟧ = term
⟦ TYPE ⟧ = type
⟦ KIND ⟧ = kind
--⟦ TPKD ⟧ = tpkd

⟦_⟧' : exprd → Set
⟦ TERM ⟧' = ex-tm
⟦ TYPE ⟧' = ex-tp
⟦ KIND ⟧' = ex-kd
--⟦ TPKD ⟧' = ex-tk

exprd-name : exprd → string
exprd-name TERM = "term"
exprd-name TYPE = "type"
exprd-name KIND = "kind"

infixl 12 _-tk_ _-tk'_ _-tT_ _-tT'_ _-arg_ _-arg'_

_-tk_ : (∀ {ed} → ⟦ ed ⟧ → ⟦ ed ⟧) → tpkd → tpkd
f -tk Tkt T = Tkt (f T)
f -tk Tkk k = Tkk (f k)

_-tk'_ : ∀ {X : Set} → (∀ {ed : exprd} → ⟦ ed ⟧ → X) → tpkd → X
f -tk' Tkt T = f T
f -tk' Tkk k = f k

_-tT_ : (∀ {ed} → ⟦ ed ⟧ → ⟦ ed ⟧) → tmtp → tmtp
f -tT Ttm t = Ttm (f t)
f -tT Ttp T = Ttp (f T)

_-tT'_ : ∀ {X : Set} → (∀ {ed : exprd} → ⟦ ed ⟧ → X) → tmtp → X
f -tT' Ttm t = f t
f -tT' Ttp T = f T

_-arg_ : (∀ {ed} → ⟦ ed ⟧ → ⟦ ed ⟧) → arg → arg
f -arg Arg t = Arg (f t)
f -arg ArgE tT = ArgE (f -tT tT)

_-arg'_ : ∀ {X : Set} → (∀ {ed : exprd} → ⟦ ed ⟧ → X) → arg → X
f -arg' Arg t = f t
f -arg' ArgE tT = f -tT' tT

pos-tm-to-tm : pos-tm → ex-tm
pos-tm-to-tm (PosTm t pi) = t

ex-case-arg-erased : ex-case-arg-sym → erased?
ex-case-arg-erased ExCaseArgTm = ff
ex-case-arg-erased _ = tt

ex-case-ctr : ex-case → var
ex-case-ctr (ExCase pi x cas t) = x

start-modname : ex-file → string
start-modname (ExModule _ _ _ mn _ _ _) = mn

{-
traverse-internal : ∀ {ed} {X} → (∀ {ed} → X → ⟦ ed ⟧ → X × ⟦ ed ⟧) → X → ⟦ ed ⟧ → ⟦ ed ⟧
traverse-internal {_} {X} f = h (fr ff) where
  fr : ∀ {ed} → 𝔹 → (X → ⟦ ed ⟧ → ⟦ ed ⟧)
  fr tt = f
  fr ff = λ x t → t

  h : ∀ {ed} → (∀ {ed} → X → ⟦ ed ⟧ → X × ⟦ ed ⟧) → X → ⟦ ed ⟧ → ⟦ ed ⟧
  h {TERM} f (App t t') = ?
  h {TERM} f (AppE t tT) = ?
  h {TERM} f (Beta t t') = ?
  h {TERM} f (Delta T t) = ?
  h {TERM} f (Hole pi) = ?
  h {TERM} f (Internal r t) = ?
  h {TERM} f (IotaPair t t' x T) =?
  h {TERM} f (IotaProj t n) = ?
  h {TERM} f (Lam me x tk t) = ?
  h {TERM} f (LetTm me x T? t t') = ?
  h {TERM} f (LetTp x k T t) = ?
  h {TERM} f (Phi tₑ t₁ t₂) = ?
  h {TERM} f (Rho t x T t') = ?
  h {TERM} f (Sigma t) = ?
  h {TERM} f (Mu μ t T t~ cs) = ?
  h {TERM} f (Var x) = ?
  h {TYPE} f (TpAbs me x tk T) = ?
  h {TYPE} f (TpIota x T₁ T₂) = ?
  h {TYPE} f (TpApp T tT) = ?
  h {TYPE} f (TpEq t₁ t₂) = ?
  h {TYPE} f (TpHole pi) = ?
  h {TYPE} f (TpLam x tk T) = ?
  h {TYPE} f (TpVar x) = ?
  h {KIND} f KdStar = ?
  h {KIND} f (KdHole pi) = ?
  h {KIND} f (KdAbs x tk k) = ?
-}

max_stars_repo_name: zmthy/cedille

max_issues_repo_name: zmthy/cedille

max_forks_repo_name: zmthy/cedille


text:
module Data.Interval where

data Interval (A : Set) : Set where
  [_▻_] : A -> A -> Interval A

lowerBound : {A : Set} -> Interval A -> A
lowerBound [ l ▻ u ] = l

upperBound : {A : Set} -> Interval A -> A
upperBound [ l ▻ u ] = u

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Pointed.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.Foundations.Structure
open import Cubical.Foundations.Structure using (typ) public
open import Cubical.Foundations.GroupoidLaws

Pointed : (ℓ : Level) → Type (ℓ-suc ℓ)
Pointed ℓ = TypeWithStr ℓ (λ x → x)

pt : ∀ {ℓ} (A∙ : Pointed ℓ) → typ A∙
pt = str

Pointed₀ = Pointed ℓ-zero

{- Pointed functions -}
_→∙_ : ∀{ℓ ℓ'} → (A : Pointed ℓ) (B : Pointed ℓ') → Type (ℓ-max ℓ ℓ')
_→∙_ A B = Σ[ f ∈ (typ A → typ B) ] f (pt A) ≡ pt B

_→∙_∙ : ∀{ℓ ℓ'} → (A : Pointed ℓ) (B : Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
A →∙ B ∙  = (A →∙ B) , (λ x → pt B) , refl

idfun∙ : ∀ {ℓ} (A : Pointed ℓ) → A →∙ A
idfun∙ A = (λ x → x) , refl

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
-- Andreas, 2020-01-28, issue #4399, reported by G. Brunerie

postulate
  A : Set

data T : Set where
  tt : T

f : {x : A} {{_ : T}} → A
f {{ p }} = {!p!}

-- Problem was:
-- Splitting on p produced pattern {{_ = tt}}
-- which was interpreted as cubical partial split.

-- Expected:
-- Splitting on p should produce an unnamed pattern.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K #-}
module container.m.from-nat.cone where

open import level
open import sum
open import equality
open import function
open import sets.nat.core
open import sets.nat.struct
open import sets.unit
open import container.core
open import container.m.from-nat.core
open import hott.level

module _ {li la lb} (c : Container li la lb) where
  open Container c
  open import container.m.coalgebra c hiding (_≅_; module _≅_)

  -- X and π play the role of the "chain" as in
  -- Definition 8 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
  module _ (Xⁱ : ℕ → I → Set (la ⊔ lb))
           (πⁱ : ∀ n → Xⁱ (suc n) →ⁱ Xⁱ n) where

    private
      X : (i : I) → ℕ → Set (la ⊔ lb)
      X i n = Xⁱ n i

      π : (i : I) (n : ℕ) → X i (suc n) → X i n
      π i n = πⁱ n i

    module cones {ℓ} (𝓩 : Coalg ℓ) where
      private
        Z = proj₁ 𝓩; θ = proj₂ 𝓩

      Cone₀ : Set _
      Cone₀ = (n : ℕ) → Z →ⁱ Xⁱ n

      Cone₁ : Cone₀ → Set _
      Cone₁ u = (n : ℕ) → πⁱ n ∘ⁱ u (suc n) ≡ u n

      Cone : Set _
      Cone = Σ Cone₀ Cone₁

      Cone₀-eq-iso : {u₁ u₂ : Cone₀}
                   → ((n : ℕ)(i : I)(z : Z i) → u₁ n i z ≡ u₂ n i z)
                   ≅ (u₁ ≡ u₂)
      Cone₀-eq-iso = Π-ap-iso refl≅ (λ _ → funext-isoⁱ) ·≅ strong-funext-iso

      Cone₁-eq-iso : {u : Cone₀}{q₁ q₂ : Cone₁ u}
                   → ( (n : ℕ)(i : I)(z : Z i)
                     → funext-invⁱ (q₁ n) i z
                     ≡ funext-invⁱ (q₂ n) i z )
                   ≅ (q₁ ≡ q₂)
      Cone₁-eq-iso {u}{q₁}{q₂} = begin
          ( (n : ℕ)(i : I)(z : Z i)
          → funext-invⁱ (q₁ n) i z
          ≡ funext-invⁱ (q₂ n) i z )
        ≅⟨ (Π-ap-iso refl≅ λ n → funext-isoⁱ) ⟩
          ( (n : ℕ) → funext-invⁱ (q₁ n) ≡ funext-invⁱ (q₂ n) )
        ≅⟨ ( Π-ap-iso refl≅ λ n → sym≅ (iso≡ (sym≅ funext-isoⁱ)) ) ⟩
          ( (n : ℕ) → q₁ n ≡ q₂ n )
        ≅⟨ strong-funext-iso ⟩
          (q₁ ≡ q₂)
        ∎
        where
          open ≅-Reasoning

      Cone-eq : {c₁ c₂ : Cone}
              → (p : (n : ℕ)(i : I)(z : Z i)
                   → proj₁ c₁ n i z ≡ proj₁ c₂ n i z)
              → ( (n : ℕ)(i : I)(z : Z i)
                → funext-invⁱ (proj₂ c₁ n) i z
                ≡ ap (π i n) (p (suc n) i z)
                · funext-invⁱ (proj₂ c₂ n) i z
                · sym (p n i z) )
              → c₁ ≡ c₂
      Cone-eq {c₁}{c₂} p α = unapΣ' (p' , α')
        where
          subst-lem : {u₁ u₂ : Cone₀}(p : u₁ ≡ u₂)(q : Cone₁ u₂)
                    → (n : ℕ)(i : I)(z : Z i)
                    → funext-invⁱ (subst Cone₁ (sym p) q n) i z
                    ≡ ap (π i n) (funext-invⁱ (funext-inv p (suc n)) i z)
                    · funext-invⁱ (q n) i z
                    · sym (funext-invⁱ (funext-inv p n) i z)
          subst-lem refl q n i z = sym (left-unit _)

          subst-lem' : {u₁ u₂ : Cone₀}(p : (n : ℕ)(i : I)(z : Z i) → u₁ n i z ≡ u₂ n i z)
                     → (q : Cone₁ u₂)(n : ℕ)(i : I)(z : Z i)
                     → funext-invⁱ (subst Cone₁ (sym (apply Cone₀-eq-iso p)) q n) i z
                     ≡ ap (π i n) (p (suc n) i z)
                     · funext-invⁱ (q n) i z
                     · sym (p n i z)
          subst-lem' {u₁}{u₂} p q n i z = subst ( λ p₁
            → funext-invⁱ (subst Cone₁ (sym (apply Cone₀-eq-iso p)) q n) i z
            ≡ ap (π i n) (p₁ (suc n) i z) · funext-invⁱ (q n) i z · sym (p₁ n i z) )
              (_≅_.iso₁ Cone₀-eq-iso p) (subst-lem (apply Cone₀-eq-iso p) q n i z)

          p' : proj₁ c₁ ≡ proj₁ c₂
          p' = apply Cone₀-eq-iso p

          α' : proj₂ c₁ ≡ subst Cone₁ (sym p') (proj₂ c₂)
          α' = apply Cone₁-eq-iso λ n i z
             → α n i z
             · sym (subst-lem' p (proj₂ c₂) n i z)

          unapΣ' : ∀ {i j}{A : Set i}{B : A → Set j}
                 → {a a' : A}{b : B a}{b' : B a'}
                 → (Σ (a ≡ a') λ q → b ≡ subst B (sym q) b')
                 → (a , b) ≡ (a' , b')
          unapΣ' (refl , refl) = refl

      private
        module limit where
          module _ (i : I) where
            open Limit (X i) (π i) public

          isom : Cone ≅ (Z →ⁱ L)
          isom = Limit-univⁱ.univ-iso I Xⁱ πⁱ

      open limit public using (isom)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
module LineEndings.Dos where

postulate ThisWorks : Set


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

module Bf.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

TmRepr : Set1
TmRepr = Cx -> Ty -> Set

module ArrMp where
  record Tm (tr : TmRepr) : Set1 where
    infixl 1 _$_
    infixr 0 lam=>_
    field
      var    : forall {tc a}   -> isTrue a tc               -> tr tc a
      lam=>_ : forall {tc a b} -> tr (tc , a) b             -> tr tc (a => b)
      _$_    : forall {tc a b} -> tr tc (a => b) -> tr tc a -> tr tc b

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

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

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

module Mp where
  record Tm (tr : TmRepr) : Set1 where
    field
      pair' : forall {tc a b}   -> tr tc a        -> tr tc b -> tr tc (a && b)
      fst   : forall {tc a b}   -> tr tc (a && b)            -> tr tc a
      snd   : forall {tc a b}   -> tr tc (a && b)            -> tr tc b
      left  : forall {tc a b}   -> tr tc a                   -> tr tc (a || b)
      right : forall {tc a b}   -> tr tc b                   -> tr tc (a || b)
      case' : forall {tc a b c} -> tr tc (a || b) -> tr (tc , a) c -> tr (tc , b) c -> tr tc c

      isArrMp : ArrMp.Tm tr
    open ArrMp.Tm isArrMp public

    syntax pair' x y    = [ x , y ]
    syntax case' xy x y = case xy => x => y
  open Tm {{...}} public

module Cp where
  record Tm (tr : TmRepr) : Set1 where
    infixr 0 abort=>_
    field
      abort=>_ : forall {tc a} -> tr (tc , NOT a) FALSE -> tr tc a

      isMp : Mp.Tm tr
    open Mp.Tm isMp public
  open Tm {{...}} public

  Thm : Ty -> Set1
  Thm a = forall {tr tc} {{_ : Tm tr}} -> tr 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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An explanation about how data types are laid out in the standard
-- library.
------------------------------------------------------------------------

module README.Data where

-- The top-level folder `Data` contains all the definitions of datatypes
-- and their associated properties.

-- Datatypes can broadly split into two categories
--   i) "Basic" datatypes which do not take other datatypes as generic
--      arguments (Nat, String, Fin, Bool, Char etc.)
--   ii) "Container" datatypes which take other generic datatypes as
--   arguments, (List, Vec, Sum, Product, Maybe, AVL trees etc.)

------------------------------------------------------------------------
-- Basic datatypes
------------------------------------------------------------------------

-- Basic datatypes are usually organised as follows:

-- 1. A `Base` module which either contains the definition of the
-- datatype or reimports it from the builtin modules, along with common
-- functions, operations and relations over elements of the datatype.

import Data.Nat.Base
import Data.Integer.Base
import Data.Char.Base
import Data.String.Base
import Data.Bool.Base

-- Commonly these modules don't need to be imported directly as their
-- contents is re-exported by the top level module (see below).

-- 2. A `Properties` module which contains the basic properties of the
-- functions, operations and relations contained in the base module.

import Data.Nat.Properties
import Data.Integer.Properties
import Data.Char.Properties
import Data.String.Properties
import Data.Bool.Properties

-- 3. A top-level module which re-exports the contents of the base
-- module as well as various queries (i.e. decidability proofs) from the
-- properties file.

import Data.Nat
import Data.Integer
import Data.Char
import Data.String
import Data.Bool

-- 4. A `Solver` module (for those datatypes that have an algebraic solver)
-- which can be used to automatically solve equalities over the basic datatype.

import Data.Nat.Solver
import Data.Integer.Solver
import Data.Bool.Solver

-- 5. More complex operations and relations are commonly found in their
-- own module beneath the top-level directory. For example:

import Data.Nat.DivMod
import Data.Integer.Coprimality

-- Note that eventually there is a plan to re-organise the library to
-- have the top-level module export a far wider range of properties and
-- additional operations in order to minimise the number of imports
-- needed. Currently it is necessary to import each of these separately
-- however.

------------------------------------------------------------------------
-- Container datatypes
------------------------------------------------------------------------

-- 1. As with basic datatypes, a `Base` module which contains the
-- definition of the datatype, along with common functions and
-- operations over that data. Unlike basic datatypes, the `Base` module
-- for container datatypes does not export any relations or predicates
-- over the datatype (see the `Relation` section below).

import Data.List.Base
import Data.Maybe.Base
import Data.Sum.Base

-- Commonly these modules don't need to be imported directly as their
-- contents is re-exported by the top level module (see below).

-- 2. As with basic datatypes, a `Properties` module which contains the
-- basic properties of the functions, operations and contained in the
-- base module.

import Data.List.Properties
import Data.Maybe.Properties
import Data.Sum.Properties

-- 3. As with basic datatypes, a top-level module which re-exports the
-- contents of the base module. In some cases this may also contain
-- additional functions which could not be placed into the corresponding
-- Base module because of cyclic dependencies.

import Data.List
import Data.Maybe
import Data.Sum

-- 4. A `Relation.Binary` folder where binary relations over the datatypes
-- are stored. Because relations over container datatypes often depend on
-- relations over the parameter datatype, this differs from basic datatypes
-- where the binary relations are usually defined in the `Base` module, e.g.
-- equality over the type `List A` depends on equality over type `A`.

-- For example the `Pointwise` relation that takes a relation over the
-- underlying type A and lifts it to the container parameterised can be found
-- as follows:

import Data.List.Relation.Binary.Pointwise
import Data.Maybe.Relation.Binary.Pointwise
import Data.Sum.Relation.Binary.Pointwise

-- Another useful subfolder in the `Data.X.Relation.Binary` folders is the
-- `Data.X.Relation.Binary.Equality` folder which contains various forms of
-- equality over the datatype.

-- 5. A `Relation.Unary` folder where unary relations, or predicates,
-- over the datatypes are stored. These can be viewed as properties
-- over a single list.

-- For example a common, useful example is `Data.X.Relation.Unary.Any`
-- that contains the types of proofs that at least one element in the
-- container satisfies some predicate/property.

import Data.List.Relation.Unary.Any
import Data.Vec.Relation.Unary.Any
import Data.Maybe.Relation.Unary.Any

-- Alternatively the `Data.X.Relation.Unary.All` module contains the
-- type of proofs that all elements in the container satisfy some
-- property.

import Data.List.Relation.Unary.All
import Data.Vec.Relation.Unary.All
import Data.Maybe.Relation.Unary.All

-- 6. A `Categorical` module/folder that contains categorical
-- interpretations of the datatype.

import Data.List.Categorical
import Data.Maybe.Categorical
import Data.Sum.Categorical.Left
import Data.Sum.Categorical.Right

-- 7. A `Function` folder that contains lifting of various types of
-- functions (e.g. injections, surjections, bijections, inverses) to
-- the datatype.

import Data.Sum.Function.Propositional
import Data.Sum.Function.Setoid
import Data.Product.Function.Dependent.Propositional
import Data.Product.Function.Dependent.Setoid

------------------------------------------------------------------------
-- Full list of documentation for the Data folder
------------------------------------------------------------------------

-- Some examples showing where the natural numbers/integers and some
-- related operations and properties are defined, and how they can be
-- used:

import README.Data.Nat
import README.Data.Nat.Induction

import README.Data.Integer

-- Some examples showing how the AVL tree module can be used.

import README.Data.AVL

-- Some examples showing how List module can be used.

import README.Data.List

-- Some examples showing how the Fresh list can be used.

import README.Data.List.Fresh

-- Using List's Interleaving to define a fully certified filter function.

import README.Data.Interleaving

-- Example of an encoding of record types with manifest fields and "with".

import README.Data.Record

-- Example use case for a trie: a wee generic lexer

import README.Data.Trie.NonDependent

-- Examples how (indexed) containers and constructions over them (free
-- monad, least fixed point, etc.) can be used

import README.Data.Container.FreeMonad
import README.Data.Container.Indexed


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Finite sets defined in terms of Data.Star
------------------------------------------------------------------------

module Data.Star.Fin where

open import Data.Star
open import Data.Star.Nat as ℕ using (ℕ)
open import Data.Star.Pointer
open import Data.Unit

-- Finite sets are undecorated pointers into natural numbers.

Fin : ℕ → Set
Fin = Any (λ _ → ⊤) (λ _ → ⊤)

-- "Constructors".

zero : ∀ {n} → Fin (ℕ.suc n)
zero = this tt

suc : ∀ {n} → Fin n → Fin (ℕ.suc n)
suc = that tt


text:
------------------------------------------------------------------------
-- Closure properties for Compatible and Size-preserving
------------------------------------------------------------------------

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

module Up-to.Closure where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude as P
open import Prelude.Size

open import Bijection equality-with-J using (_↔_)
open import Function-universe equality-with-J hiding (id; _∘_)

import Bisimilarity
open import Indexed-container hiding (Bisimilarity)
open import Indexed-container.Combinators hiding (id; _∘_)
open import Labelled-transition-system
import Labelled-transition-system.CCS
open import Relation
import Similarity
import Similarity.CCS as SC
open import Up-to

private
  module CCS {ℓ} (Name : Type ℓ) where
    open Labelled-transition-system.CCS Name public
    open module B = Bisimilarity CCS public
    open module S = Similarity CCS public using (Similarity)

------------------------------------------------------------------------
-- Closure properties for Compatible

-- The results in this section are closely related to
-- Proposition 6.3.21 in Pous and Sangiorgi's "Enhancements of the
-- bisimulation proof method".

-- The function flip Compatible F is closed under _⊗_, assuming that F
-- is monotone.

Compatible-⊗ :
  ∀ {ℓ} {I : Type ℓ} {C₁ C₂ : Container I I} {F : Trans ℓ I} →
  Monotone F →
  Compatible C₁ F → Compatible C₂ F → Compatible (C₁ ⊗ C₂) F
Compatible-⊗ {C₁ = C₁} {C₂} {F} mono comp₁ comp₂ {R = R} =
  F (⟦ C₁ ⊗ C₂ ⟧ R)            ⊆⟨ mono (⟦⊗⟧↔ _ C₁ C₂) ⟩
  F (⟦ C₁ ⟧ R ∩ ⟦ C₂ ⟧ R)      ⊆⟨ (λ x → mono proj₁ x , mono proj₂ x) ⟩
  F (⟦ C₁ ⟧ R) ∩ F (⟦ C₂ ⟧ R)  ⊆⟨ Σ-map comp₁ comp₂ ⟩
  ⟦ C₁ ⟧ (F R) ∩ ⟦ C₂ ⟧ (F R)  ⊆⟨ _⇔_.from (⟦⊗⟧↔ _ C₁ C₂) ⟩∎
  ⟦ C₁ ⊗ C₂ ⟧ (F R)            ∎

-- The function flip Compatible F is closed under reindex₁ f, assuming
-- that F is monotone and f-symmetric.

Compatible-reindex₁ :
  ∀ {ℓ} {I : Type ℓ} {C : Container I I} {F : Trans ℓ I} {f : I → I} →
  Monotone F → Symmetric f F →
  Compatible C F → Compatible (reindex₁ f C) F
Compatible-reindex₁ {C = C} {F} {f} mono hyp comp {R = R} =
  F (⟦ reindex₁ f C ⟧ R)  ⊆⟨ mono (⟦reindex₁⟧↔ _ C) ⟩
  F (⟦ C ⟧ (R ∘ f))       ⊆⟨ comp ⟩
  ⟦ C ⟧ (F (R ∘ f))       ⊆⟨ map C (hyp _) ⟩
  ⟦ C ⟧ (F R ∘ f)         ⊆⟨ _⇔_.from (⟦reindex₁⟧↔ _ C) ⟩∎
  ⟦ reindex₁ f C ⟧ (F R)  ∎

-- The function flip Compatible F is closed under reindex₂ f, assuming
-- that F is f-symmetric.

Compatible-reindex₂ :
  ∀ {ℓ} {I : Type ℓ} {C : Container I I} {F : Trans ℓ I} {f : I → I} →
  Symmetric f F →
  Compatible C F → Compatible (reindex₂ f C) F
Compatible-reindex₂ {C = C} {F} {f} hyp comp {R = R} =
  F (⟦ reindex₂ f C ⟧ R)  ⊆⟨⟩
  F (⟦ C ⟧ R ∘ f)         ⊆⟨ hyp _ ⟩
  F (⟦ C ⟧ R) ∘ f         ⊆⟨ comp ⟩
  ⟦ C ⟧ (F R) ∘ f         ⊆⟨ id ⟩∎
  ⟦ reindex₂ f C ⟧ (F R)  ∎

-- The function flip Compatible F is closed under reindex f, assuming
-- that F is monotone and f-symmetric.

Compatible-reindex :
  ∀ {ℓ} {I : Type ℓ} {C : Container I I} {F : Trans ℓ I} {f : I → I} →
  Monotone F → Symmetric f F →
  Compatible C F → Compatible (reindex f C) F
Compatible-reindex {C = C} {F} {f} mono hyp =
  Compatible C F                            ↝⟨ Compatible-reindex₁ mono hyp ⟩
  Compatible (reindex₁ f C) F               ↝⟨ Compatible-reindex₂ hyp ⟩
  Compatible (reindex₂ f (reindex₁ f C)) F  ↔⟨⟩
  Compatible (reindex f C) F                □

-- The function flip Compatible F is closed under _⟷_, assuming that F
-- is monotone and symmetric.

Compatible-⟷ :
  ∀ {ℓ} {I : Type ℓ}
    {C₁ C₂ : Container (I × I) (I × I)} {F : Trans₂ ℓ I} →
  Monotone F → Symmetric swap F →
  Compatible C₁ F → Compatible C₂ F → Compatible (C₁ ⟷ C₂) F
Compatible-⟷ {C₁ = C₁} {C₂} {F} mono sym = curry (
  Compatible C₁ F × Compatible C₂ F                 ↝⟨ Σ-map id (Compatible-reindex mono sym) ⟩
  Compatible C₁ F × Compatible (reindex swap C₂) F  ↝⟨ uncurry (Compatible-⊗ mono) ⟩
  Compatible (C₁ ⊗ reindex swap C₂) F               ↔⟨⟩
  Compatible (C₁ ⟷ C₂) F                            □)

-- An instance of the result above: If F is monotone and symmetric,
-- and compatible for strong similarity for some LTS, then F is
-- compatible for strong bisimilarity for this LTS.

compatible-for-similarity→compatible-for-bisimilarity :
  ∀ {ℓ} {lts : LTS ℓ} {F} →
  Monotone F → Symmetric swap F →
  Compatible (Similarity.StepC lts) F →
  Compatible (Bisimilarity.StepC lts) F
compatible-for-similarity→compatible-for-bisimilarity mono sym comp =
  Compatible-⟷ mono sym comp comp

------------------------------------------------------------------------
-- Closure properties for Size-preserving

-- The function flip Size-preserving F is closed under reindex,
-- assuming that F is f-symmetric for an involutory function f.
--
-- Note that the assumptions are different from the ones asked for in
-- Compatible-reindex: monotonicity of F has been replaced by the
-- assumption that f is an involution.

Size-preserving-reindex :
  ∀ {ℓ} {I : Type ℓ} {C : Container I I} {F : Trans ℓ I} {f : I → I} →
  f ∘ f ≡ id → Symmetric f F →
  Size-preserving C F → Size-preserving (reindex f C) F
Size-preserving-reindex {C = C} {F} {f}
                        inv hyp pres {R = R} {i = i} R⊆ =

  F R                        ⊆⟨ (λ {x} → subst (λ g → F (R ∘ g) x) (sym inv)) ⟩
  F (R ∘ f ∘ f)              ⊆⟨ hyp _ ⟩
  F (R ∘ f) ∘ f              ⊆⟨ pres (

      R ∘ f                       ⊆⟨ R⊆ ⟩
      ν (reindex f C) i ∘ f       ⊆⟨ _⇔_.to (ν-reindex⇔ inv) ⟩
      ν C i ∘ f ∘ f               ⊆⟨ (λ {x} → subst (λ g → ν C i (g x)) inv) ⟩∎
      ν C i                       ∎) ⟩

  ν C i ∘ f                  ⊆⟨ _⇔_.from (ν-reindex⇔ inv) ⟩∎
  ν (reindex f C) i          ∎

-- Some negative results:
--
-- * For inhabited name types it is not in general the case that a
--   monotone and symmetric function F that is size-preserving for
--   similarity for CCS is also size-preserving for bisimilarity for
--   CCS.
--
-- * It is not in general the case that if F is monotone and
--   symmetric, and size-preserving for strong similarity for some
--   LTS, then F is size-preserving for strong bisimilarity for this
--   LTS.
--
-- * The function flip Size-preserving F is not closed under _⟷_ for
--   all F, not even those that are monotone and symmetric.
--
-- * Furthermore flip Size-preserving F is not closed under _⊗_ for
--   all F, not even those that are monotone.

¬-Size-preserving-⟷/⊗ :
  ∀ {ℓ} →
  ({Name : Type ℓ} →
   let open CCS Name in
   Name →
   ¬ ({F : Trans₂ ℓ (Proc ∞)} →
      Monotone F → Symmetric swap F →
      Size-preserving S.StepC F →
      Size-preserving B.StepC F))
    ×
  ¬ (∀ {lts : LTS ℓ} {F} →
     Monotone F → Symmetric swap F →
     Size-preserving (Similarity.StepC lts) F →
     Size-preserving (Bisimilarity.StepC lts) F)
    ×
  ¬ ({I : Type ℓ} {C₁ C₂ : Container (I × I) (I × I)}
     {F : Trans₂ ℓ I} →
     Monotone F → Symmetric swap F →
     Size-preserving C₁ F → Size-preserving C₂ F →
     Size-preserving (C₁ ⟷ C₂) F)
    ×
  ¬ ({I : Type ℓ} {C₁ C₂ : Container I I} {F : Trans ℓ I} →
     Monotone F →
     Size-preserving C₁ F → Size-preserving C₂ F →
     Size-preserving (C₁ ⊗ C₂) F)
¬-Size-preserving-⟷/⊗ {ℓ} =
    Lemmas.contradiction₂
  , Lemmas.contradiction₃ (lift tt)
  , Lemmas.contradiction₄ (lift tt)
  , Lemmas.contradiction₅ (lift tt)
  where
  module Lemmas {Name : Type ℓ} (a : Name) where
    open CCS Name public

    ≤≥≁ = SC.≤≥≁ a

    m₁ = proj₁ ≤≥≁
    m₂ = proj₁ (proj₂ ≤≥≁)

    F : Trans₂ ℓ (Proc ∞)
    F R = R ∪ (_≡ (m₁ , m₂)) ∪ (_≡ (m₂ , m₁))

    mono : Monotone F
    mono R⊆S = ⊎-map R⊆S id

    symm : Symmetric swap F
    symm R =
      F (R ⁻¹)                                      ⊆⟨⟩
      R ⁻¹ ∪ (_≡ (m₁ , m₂))    ∪ (_≡ (m₂ , m₁))     ⊆⟨ ⊎-map id P.[ inj₂ ∘ lemma , inj₁ ∘ lemma ] ⟩
      R ⁻¹ ∪ (_≡ (m₁ , m₂)) ⁻¹ ∪ (_≡ (m₂ , m₁)) ⁻¹  ⊆⟨ id ⟩∎
      F R ⁻¹                                        ∎
      where
      lemma : {p₁ p₂ : Proc ∞ × Proc ∞} → p₁ ≡ swap p₂ → swap p₁ ≡ p₂
      lemma refl = refl

    pres : Size-preserving S.StepC F
    pres {R = R} {i = i} R⊆ =
      F R                                  ⊆⟨⟩
      R ∪ (_≡ (m₁ , m₂)) ∪ (_≡ (m₂ , m₁))  ⊆⟨ [ R⊆ , helper ] ⟩∎
      Similarity i                         ∎
      where
      helper : ∀ {p} → p ≡ (m₁ , m₂) ⊎ p ≡ (m₂ , m₁) → Similarity i p
      helper (inj₁ refl) = proj₁ (proj₂ (proj₂ ≤≥≁))
      helper (inj₂ refl) = proj₁ (proj₂ (proj₂ (proj₂ ≤≥≁)))

    contradiction =
      Size-preserving B.StepC F            ↝⟨ (λ hyp → _⇔_.to (monotone→⇔ _ mono) hyp) ⟩
      F (Bisimilarity ∞) ⊆ Bisimilarity ∞  ↝⟨ _$ inj₂ (inj₁ refl) ⟩
      m₁ ∼ m₂                              ↝⟨ proj₂ (proj₂ (proj₂ (proj₂ ≤≥≁))) ⟩□
      ⊥                                    □

    contradiction₂ =
      ({F : Trans₂ ℓ (Proc ∞)} →
       Monotone F → Symmetric swap F →
       Size-preserving S.StepC F →
       Size-preserving B.StepC F)       ↝⟨ (λ closed → closed mono symm pres) ⟩

      Size-preserving B.StepC F         ↝⟨ contradiction ⟩□

      ⊥                                 □

    contradiction₃ =
      (∀ {lts : LTS ℓ} {F} →
       Monotone F → Symmetric swap F →
       Size-preserving (Similarity.StepC lts) F →
       Size-preserving (Bisimilarity.StepC lts) F)        ↝⟨ (λ closed mono sym pres → closed mono sym pres) ⟩

      ({F : Trans₂ ℓ (Proc ∞)} →
       Monotone F → Symmetric swap F →
       Size-preserving S.StepC F →
       Size-preserving B.StepC F)                         ↝⟨ contradiction₂ ⟩□

      ⊥                                                   □

    contradiction₄ =
      ({I : Type ℓ} {C₁ C₂ : Container (I × I) (I × I)}
       {F : Trans₂ ℓ I} →
       Monotone F → Symmetric swap F →
       Size-preserving C₁ F → Size-preserving C₂ F →
       Size-preserving (C₁ ⟷ C₂) F)                       ↝⟨ (λ closed mono symm pres → closed mono symm pres pres) ⟩

      (∀ {lts : LTS ℓ} {F} →
       Monotone F → Symmetric swap F →
       Size-preserving (Similarity.StepC lts) F →
       Size-preserving (Bisimilarity.StepC lts) F)        ↝⟨ contradiction₃ ⟩□

      ⊥                                                   □

    contradiction₅ =
      ({I : Type ℓ} {C₁ C₂ : Container I I}
       {F : Trans ℓ I} →
       Monotone F →
       Size-preserving C₁ F → Size-preserving C₂ F →
       Size-preserving (C₁ ⊗ C₂) F)                   ↝⟨ (λ closed → closed mono pres) ⟩

      (Size-preserving (reindex swap S.StepC) F →
       Size-preserving B.StepC F)                     ↝⟨ _$ Size-preserving-reindex refl symm pres ⟩

      Size-preserving B.StepC F                       ↝⟨ contradiction ⟩□

      ⊥                                               □

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
module CTL.Modalities.AG where

open import FStream.Core
open import Library

-- Certainly forever : s₀ ⊧ φ ⇔ ∀ s₀ R s₁ R ... ∀ i . sᵢ ⊧ φ
{-# NO_POSITIVITY_CHECK #-} -- Not necessary from Agda 2.6 upwards
record AG' {i : Size} {ℓ₁ ℓ₂} {C : Container ℓ₁}
  (props : FStream' C (Set ℓ₂)) : Set (ℓ₁ ⊔ ℓ₂) where
  coinductive
  field
    nowA   : head props
    laterA : {j : Size< i} → A (fmap AG' (inF (tail props)))
open AG' public

AG : ∀ {i : Size} {ℓ₁ ℓ₂} {C : Container ℓ₁}
   → FStream C (Set ℓ₂) → Set (ℓ₁ ⊔ ℓ₂)
AG props = APred AG' (inF props)

mutual
  AGₛ' : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁}
       → FStream' C (Set ℓ₂) → FStream' {i} C (Set (ℓ₁ ⊔ ℓ₂))
  head (AGₛ' props) = AG' props
  tail (AGₛ' props) = AGₛ (tail props)

  AGₛ : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁}
      → FStream C (Set ℓ₂) → FStream {i} C (Set (ℓ₁ ⊔ ℓ₂))
  inF (AGₛ props) = fmap AGₛ' (inF props)

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
module Symmetric where

open import Level hiding ( suc ; zero )
open import Algebra
open import Algebra.Structures
open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ )
open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ) renaming ( <-cmp to <-fcmp )
open import Data.Product
open import Data.Fin.Permutation
open import Function hiding (id ; flip)
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function.LeftInverse  using ( _LeftInverseOf_ )
open import Function.Equality using (Π)
open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
open import Data.Nat.Properties -- using (<-trans)
open import Relation.Binary.PropositionalEquality
open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ) renaming (reverse to rev )
open import nat

fid : {p : ℕ } → Fin p → Fin p
fid x = x

-- Data.Fin.Permutation.id
pid : {p : ℕ } → Permutation p p
pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }

-- Data.Fin.Permutation.flip
pinv : {p : ℕ } → Permutation p p → Permutation p p
pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }

record _=p=_ {p : ℕ } ( x y : Permutation p p )  : Set where
    field
       peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q

open _=p=_

prefl : {p : ℕ } { x  : Permutation p p } → x =p= x
peq (prefl {p} {x}) q = refl

psym : {p : ℕ } { x y : Permutation p p } → x =p= y →  y =p= x
peq (psym {p} {x} {y}  eq ) q = sym (peq eq q)

ptrans : {p : ℕ } { x y z : Permutation p p } → x =p= y  → y =p= z →  x =p= z
peq (ptrans {p} {x} {y} x=y y=z ) q = trans (peq x=y q) (peq y=z q)

peqˡ :  {p : ℕ }{ x y : Permutation p p } → x =p= y → (q : Fin p)  →  x ⟨$⟩ˡ q ≡ y ⟨$⟩ˡ q
peqˡ {p} {x} {y} eq q = begin
       x ⟨$⟩ˡ q
   ≡⟨ sym ( inverseˡ y ) ⟩
       y ⟨$⟩ˡ (y ⟨$⟩ʳ ( x ⟨$⟩ˡ  q ))
   ≡⟨ cong (λ k → y ⟨$⟩ˡ k ) (sym (peq eq _ )) ⟩
       y ⟨$⟩ˡ (x ⟨$⟩ʳ ( x ⟨$⟩ˡ  q ))
   ≡⟨ cong (λ k → y ⟨$⟩ˡ k ) ( inverseʳ x ) ⟩
       y ⟨$⟩ˡ q
   ∎ where open ≡-Reasoning

presp : { p : ℕ } {x y u v : Permutation p p } → x =p= y → u =p= v → (x ∘ₚ u) =p= (y ∘ₚ v)
presp {p} {x} {y} {u} {v} x=y u=v = record { peq = λ q → lemma4 q } where
   lemma4 : (q : Fin p) → ((x ∘ₚ u) ⟨$⟩ʳ q) ≡ ((y ∘ₚ v) ⟨$⟩ʳ q)
   lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ )
passoc : { p : ℕ } (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) =p=  (x ∘ₚ (y ∘ₚ z))
passoc x y z = record { peq = λ q → refl }
p-inv : { p : ℕ } {i j : Permutation p p} →  i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q
p-inv {p} {i} {j} i=j q = begin
   i ⟨$⟩ˡ q                      ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (inverseʳ j)  )  ⟩
   i ⟨$⟩ˡ ( j ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ cong (λ k  →  i ⟨$⟩ˡ k) (sym (peq i=j _ ))  ⟩
   i ⟨$⟩ˡ ( i ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ inverseˡ i  ⟩
   j ⟨$⟩ˡ q
   ∎ where open ≡-Reasoning

Symmetric : ℕ → Group  Level.zero Level.zero
Symmetric p = record {
      Carrier        = Permutation p p
    ; _≈_            = _=p=_
    ; _∙_            = _∘ₚ_
    ; ε              = pid
    ; _⁻¹            = pinv
    ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
       isEquivalence = record {refl = prefl ; trans = ptrans ; sym = psym }
       ; ∙-cong = presp }
       ; assoc = passoc }
       ; identity = ( (λ q → record { peq = λ q → refl } ) , (λ q → record { peq = λ q → refl } ))  }
       ; inverse   = ( (λ x → record { peq = λ q → inverseʳ x} ) , (λ x → record { peq = λ q → inverseˡ x} ))
       ; ⁻¹-cong   = λ i=j → record { peq = λ q → p-inv i=j q }
      }
   }

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois


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

open import LogicalFormulae
open import Setoids.Setoids
open import Rings.Definition
open import Rings.IntegralDomains.Definition
open import Vectors
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Definition
open import Sets.EquivalenceRelations

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Rings.UniqueFactorisationDomains.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where

open import Rings.Units.Definition R
open import Rings.Irreducibles.Definition intDom
open import Rings.Associates.Definition intDom
open import Rings.Primes.Definition intDom
open import Rings.Divisible.Definition R
open import Rings.Divisible.Lemmas R
open import Rings.UniqueFactorisationDomains.Definition intDom
open Ring R
open Setoid S
open Equivalence eq

ufdImpliesUfd' : UFD → UFD'
UFD'.factorisation (ufdImpliesUfd' x) = UFD.factorisation x
Prime.isPrime (UFD'.irreduciblesArePrime (ufdImpliesUfd' ufd) {r} irreducible) a b (s , ab=rs) rNotDivA = {!!}
  where
  -- we can't factorise a, it might be a unit :(
    factA : Factorisation {a} (λ p → rNotDivA (divisibleWellDefined reflexive (symmetric p) (everythingDividesZero r))) {!!}
    factA = UFD.factorisation ufd {a} {!!} {!!}
    fact1 : Factorisation {r} {!!} {!!}
    fact1 = {!!}
    fact2 : Factorisation {r} {!!} {!!}
    fact2 = {!!}
Prime.nonzero (UFD'.irreduciblesArePrime (ufdImpliesUfd' x) irreducible) = Irreducible.nonzero irreducible
Prime.nonunit (UFD'.irreduciblesArePrime (ufdImpliesUfd' x) irreducible) = Irreducible.nonunit irreducible

private
  lemma2 : UFD' → {r : A} → .(nonzero : (r ∼ 0R) → False) .(nonunit : (Unit r) → False) → (f1 f2 : Factorisation {r} nonzero nonunit) → factorisationEquality f1 f2
  lemma2 x nonzero nonunit record { len = lenA ; factorise = factoriseA ; factoriseIsFactorisation = factoriseIsFactorisationA ; factoriseIsIrreducibles = factoriseIsIrreduciblesA ; distinct = distinctA } record { len = lenB ; factorise = factoriseB ; factoriseIsFactorisation = factoriseIsFactorisationB ; factoriseIsIrreducibles = factoriseIsIrreduciblesB ; distinct = distinctB } with ℕDecideEquality lenA lenB
  lemma2 x nonzero nonunit record { len = zero ; factorise = [] ; factoriseIsFactorisation = factoriseIsFactorisationA ; factoriseIsIrreducibles = factoriseIsIrreduciblesA ; distinct = distinctA } record { len = .0 ; factorise = [] ; factoriseIsFactorisation = factoriseIsFactorisationB ; factoriseIsIrreducibles = factoriseIsIrreduciblesB ; distinct = distinctB } | inl refl = record {}
  lemma2 ufd' {r} nonzero nonunit record { len = (succ len) ; factorise = (a1 ,, n1) ,- factoriseA ; factoriseIsFactorisation = factoriseIsFactorisationA ; factoriseIsIrreducibles = factoriseIsIrreduciblesA ; distinct = distinctA } record { len = .(succ len) ; factorise = factoriseB ; factoriseIsFactorisation = factoriseIsFactorisationB ; factoriseIsIrreducibles = factoriseIsIrreduciblesB ; distinct = distinctB } | inl refl = {!!}
    where
      a1Prime : Prime a1
      a1Prime = UFD'.irreduciblesArePrime ufd' (_&&_.fst factoriseIsIrreduciblesA)
      a1DivR : a1 ∣ r
      a1DivR = {!!}

  ... | inr neq = {!!}

ufd'ImpliesUfd : UFD' → UFD
UFD.factorisation (ufd'ImpliesUfd x) = UFD'.factorisation x
UFD.uniqueFactorisation (ufd'ImpliesUfd x) {r} nonzero nonunit f1 f2 = lemma2 x nonzero nonunit f1 f2


text:
module Numeral.Matrix.Proofs where

import      Lvl
open import Syntax.Number
open import Data
open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.Boolean.Stmt.Proofs
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
import      Functional as Fn
open import Function.Equals
open import Lang.Inspect
open import Logic.Predicate
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Numeral.Finite
open import Numeral.Finite.Bound
open import Numeral.Finite.Oper
open import Numeral.Finite.Oper.Comparisons
open import Numeral.Finite.Oper.Comparisons.Proofs
open import Numeral.Finite.Proofs
open import Numeral.Matrix as Matrix using (Matrix ; SquareMatrix)
open import Numeral.Natural
open import Numeral.CoordinateVector as Vector using (Vector)
import      Numeral.CoordinateVector.Proofs as Vector
open import Relator.Equals using ([≡]-intro) renaming (_≡_ to _≡ₑ_ ; _≢_ to _≢ₑ_)
open import Relator.Equals.Proofs.Equivalence
open import Structure.Function
open import Structure.Operator.Group
open import Structure.Operator.Monoid
open import Structure.Operator.Properties
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Function
open import Syntax.Implication
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₑ : Lvl.Level
private variable T A B : Type{ℓ}

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  private variable s : ℕ ⨯ ℕ
  private variable w h n : ℕ
  private variable x y z : 𝕟(n)
  private variable id id₁ id₂ zero elem 𝟎ₛ 𝟏ₛ : T
  private variable f g inv : T → T
  private variable _▫_ _▫₁_ _▫₂_ _+ₛ_ _⋅ₛ_ : T → T → T
  private variable v v₁ v₂ : Vector(n)(T)
  private variable M : Matrix(s)(T)

  instance
    matrix-equiv : Equiv(Matrix(s)(T))
    Equiv._≡_ matrix-equiv (Matrix.mat proj₁) (Matrix.mat proj₂) = proj₁ ⊜ proj₂
    Reflexivity.proof  (Equivalence.reflexivity  (Equiv.equivalence matrix-equiv)) = reflexivity(_⊜_)
    Symmetry.proof     (Equivalence.symmetry     (Equiv.equivalence matrix-equiv)) = symmetry(_⊜_)
    Transitivity.proof (Equivalence.transitivity (Equiv.equivalence matrix-equiv)) = transitivity(_⊜_)

  instance
    matrix-map₂-binaryOperator : ⦃ oper : BinaryOperator(_▫_) ⦄ → BinaryOperator(Matrix.map₂{s = s}(_▫_))
    BinaryOperator.congruence (matrix-map₂-binaryOperator {_▫_ = _▫_} ⦃ oper ⦄) (intro p) (intro q) = intro (congruence₂(_▫_) ⦃ oper ⦄ p q)

  instance
    matrix-map₂-identityₗ : ⦃ ident : Identityₗ(_▫_)(id) ⦄ → Identityₗ(Matrix.map₂{s = s}(_▫_)) (Matrix.fill(id))
    Identityₗ.proof (matrix-map₂-identityₗ {_▫_ = _▫_} {id = id}) = intro(identityₗ(_▫_)(id))

  instance
    matrix-map₂-identityᵣ : ⦃ ident : Identityᵣ(_▫_)(id) ⦄ → Identityᵣ(Matrix.map₂{s = s}(_▫_)) (Matrix.fill(id))
    Identityᵣ.proof (matrix-map₂-identityᵣ {_▫_ = _▫_} {id = id}) = intro(identityᵣ(_▫_)(id))

  instance
    matrix-map₂-identity : ⦃ ident : Identity(_▫_)(id) ⦄ → Identity(Matrix.map₂{s = s}(_▫_)) (Matrix.fill(id))
    matrix-map₂-identity = intro

  instance
    matrix-map₂-absorberₗ : ⦃ absorb : Absorberₗ(_▫_)(id) ⦄ → Absorberₗ(Matrix.map₂{s = s}(_▫_)) (Matrix.fill(id))
    Absorberₗ.proof (matrix-map₂-absorberₗ {_▫_ = _▫_} {id = id}) = intro(absorberₗ(_▫_)(id))

  instance
    matrix-map₂-absorberᵣ : ⦃ absorb : Absorberᵣ(_▫_)(id) ⦄ → Absorberᵣ(Matrix.map₂{s = s}(_▫_)) (Matrix.fill(id))
    Absorberᵣ.proof (matrix-map₂-absorberᵣ {_▫_ = _▫_} {id = id}) = intro(absorberᵣ(_▫_)(id))

  instance
    matrix-map₂-absorber : ⦃ absorb : Absorber(_▫_)(id) ⦄ → Absorber(Matrix.map₂{s = s}(_▫_)) (Matrix.fill(id))
    matrix-map₂-absorber = intro

  instance
    matrix-map₂-commutativity : ⦃ comm : Commutativity(_▫_) ⦄ → Commutativity(Matrix.map₂{s = s}(_▫_))
    Commutativity.proof (matrix-map₂-commutativity {_▫_ = _▫_}) = intro(commutativity(_▫_))

  instance
    matrix-map₂-associativity : ⦃ assoc : Associativity(_▫_) ⦄ → Associativity(Matrix.map₂{s = s}(_▫_))
    Associativity.proof (matrix-map₂-associativity {_▫_ = _▫_}) = intro(associativity(_▫_))

  instance
    matrix-map₂-map-inverseFunctionₗ : ⦃ ident : Identityₗ(_▫_)(id) ⦄ ⦃ inver : InverseFunctionₗ(_▫_) ⦃ [∃]-intro _ ⦄ (inv) ⦄ → InverseFunctionₗ(Matrix.map₂{s = s}(_▫_)) ⦃ [∃]-intro _ ⦄ (Matrix.map inv)
    InverseFunctionₗ.proof (matrix-map₂-map-inverseFunctionₗ {_▫_ = _▫_} {inv = inv}) = intro (inverseFunctionₗ(_▫_) ⦃ [∃]-intro _ ⦄ (inv))

  instance
    matrix-map₂-map-inverseFunctionᵣ : ⦃ ident : Identityᵣ(_▫_)(id) ⦄ ⦃ inver : InverseFunctionᵣ(_▫_) ⦃ [∃]-intro _ ⦄ (inv) ⦄ → InverseFunctionᵣ(Matrix.map₂{s = s}(_▫_)) ⦃ [∃]-intro _ ⦄ (Matrix.map inv)
    InverseFunctionᵣ.proof (matrix-map₂-map-inverseFunctionᵣ {_▫_ = _▫_} {inv = inv}) = intro (inverseFunctionᵣ(_▫_) ⦃ [∃]-intro _ ⦄ (inv))

  instance
    matrix-map₂-map-inverseFunction : ⦃ ident : Identity(_▫_)(id) ⦄ ⦃ inver : InverseFunction(_▫_) ⦃ [∃]-intro _ ⦄ (inv) ⦄ → InverseFunction(Matrix.map₂{s = s}(_▫_)) ⦃ [∃]-intro _ ⦄ (Matrix.map inv)
    matrix-map₂-map-inverseFunction = intro

  instance
    matrix-map-function : ⦃ func : Function(f) ⦄ → Function(Matrix.map{s = s} (f))
    Function.congruence matrix-map-function (intro p) = intro(congruence₁ _ p)

  instance
    matrix-map₂-monoid : ⦃ monoid : Monoid(_▫_) ⦄ → Monoid(Matrix.map₂{s = s}(_▫_))
    Monoid.identity-existence matrix-map₂-monoid = [∃]-intro(Matrix.fill(_))

  instance
    matrix-map₂-group : ⦃ group : Group(_▫_) ⦄ → Group(Matrix.map₂{s = s}(_▫_))
    Group.monoid matrix-map₂-group = matrix-map₂-monoid
    Group.inverse-existence matrix-map₂-group = [∃]-intro _

  diagMat-element-zero : (Matrix.proj (SquareMatrix.diagMat zero v) (x , y) ≡ zero) ↔ ((x ≢ₑ y) ∨ (Vector.proj v(x) ≡ zero))
  diagMat-element-zero {zero = zero}{𝐒 n}{v = v}{x = x}{y = y} =
    [↔]-intro ([↔]-to-[←] [→ₗ][∨][∧]-preserving ([∧]-intro l₁ l₂)) r ⦗ [↔]-transitivity ⦘ᵣ
    [∨]-mapₗ-[↔] ([↔]-transitivity false-true-opposites ([↔]-symmetry([¬]-unaryOperator [≡][≡?]-equivalence)))
    where
      l₁ : (Matrix.proj (SquareMatrix.diagMat zero v) (x , y) ≡ zero) ← IsFalse(x ≡? y)
      l₁ p with 𝐹 ← (x ≡? y) = reflexivity(_≡_)
      l₂ : (Matrix.proj (SquareMatrix.diagMat zero v) (x , y) ≡ zero) ← (Vector.proj v(x) ≡ zero)
      l₂ p with (x ≡? y)
      ... | 𝑇 = p
      ... | 𝐹 = reflexivity(_≡_)
      r : (Matrix.proj (SquareMatrix.diagMat zero v) (x , y) ≡ zero) → (IsFalse(x ≡? y) ∨ (Vector.proj v(x) ≡ zero))
      r p with (x ≡? y)
      ... | 𝑇 = [∨]-introᵣ p
      ... | 𝐹 = [∨]-introₗ [⊤]-intro

  diagMat-element-vector : (Matrix.proj (SquareMatrix.diagMat zero v) (x , y) ≡ Vector.proj v(x)) ↔ ((x ≡ₑ y) ∨ (Vector.proj v(x) ≡ zero))
  diagMat-element-vector {zero = zero}{𝐒 n}{v = v}{x = x}{y = y} =
    [↔]-intro ([↔]-to-[←] [→ₗ][∨][∧]-preserving ([∧]-intro l₁ l₂)) r ⦗ [↔]-transitivity ⦘ᵣ
    [∨]-mapₗ-[↔] ([↔]-symmetry [≡][≡?]-equivalence)
    where
      l₁ : (Matrix.proj (SquareMatrix.diagMat zero v) (x , y) ≡ Vector.proj v(x)) ← IsTrue(x ≡? y)
      l₁ p with 𝑇 ← (x ≡? y) = reflexivity(_≡_)
      l₂ : (Matrix.proj (SquareMatrix.diagMat zero v) (x , y) ≡ Vector.proj v(x)) ← (Vector.proj v(x) ≡ zero)
      l₂ p with (x ≡? y)
      ... | 𝑇 = reflexivity(_≡_)
      ... | 𝐹 = symmetry(_≡_) p
      r : (Matrix.proj (SquareMatrix.diagMat zero v) (x , y) ≡ Vector.proj v(x)) → (IsTrue(x ≡? y) ∨ (Vector.proj v(x) ≡ zero))
      r p with (x ≡? y)
      ... | 𝑇 = [∨]-introₗ [⊤]-intro
      ... | 𝐹 = [∨]-introᵣ (symmetry(_≡_) p)

  scalarMat-element-zero : (Matrix.proj (SquareMatrix.scalarMat zero elem) (x , y) ≡ zero) ↔ ((x ≢ₑ y) ∨ (elem ≡ zero))
  scalarMat-element-zero {zero = zero}{elem = elem}{x = x}{y = y} =
    Matrix.proj (SquareMatrix.scalarMat zero elem) (x , y) ≡ zero             ⇔-[]
    Matrix.proj (SquareMatrix.diagMat zero (Vector.fill elem)) (x , y) ≡ zero ⇔-[ diagMat-element-zero ]
    (x ≢ₑ y) ∨ (Vector.proj (Vector.fill elem)(x) ≡ zero)                     ⇔-[]
    (x ≢ₑ y) ∨ (elem ≡ zero)                                                  ⇔-end

  scalarMat-element-scalar : (Matrix.proj (SquareMatrix.scalarMat zero elem) (x , y) ≡ elem) ↔ ((x ≡ₑ y) ∨ (elem ≡ zero))
  scalarMat-element-scalar {zero = zero}{elem = elem}{x = x}{y = y} =
    Matrix.proj (SquareMatrix.scalarMat zero elem) (x , y) ≡ elem                            ⇔-[]
    Matrix.proj (SquareMatrix.diagMat zero (Vector.fill elem)) (x , y) ≡ Vector.fill elem(x) ⇔-[ diagMat-element-vector ]
    (x ≡ₑ y) ∨ (Vector.proj (Vector.fill elem)(x) ≡ zero)                                    ⇔-[]
    (x ≡ₑ y) ∨ (elem ≡ zero)                                                                 ⇔-end

  map₂-tail : Vector.tail(Vector.map₂(_▫_) v₁ v₂) ≡ Vector.map₂(_▫_) (Vector.tail v₁) (Vector.tail v₂)
  _⊜_.proof (map₂-tail {d = 𝐒(d)}) = reflexivity(_≡_)

  -- TODO: Probably not neccessary : row-tail : ∀{M : Matrix(𝐒(w) , 𝐒(h))(T)}{i} → Vector.tail(Matrix.row {s = (𝐒(w) , 𝐒(h))} M (𝐒(i))) ≡ Matrix.row {s = (w , h)}(Matrix.minor M(𝟎 , 𝟎))(i)

  col-scalarMat-is-indexProject : ∀{false true : T}{i : 𝕟(n)} → (Matrix.col(SquareMatrix.scalarMat {d = n} false true)(i) ≡ Vector.indexProject i true false)
  _⊜_.proof (col-scalarMat-is-indexProject {i = i}) {x} with (i ≡? x)
  ... | 𝑇 = reflexivity(_≡_)
  ... | 𝐹 = reflexivity(_≡_)

  row-scalarMat-is-indexProject : ∀{false true : T}{i : 𝕟(n)} → (Matrix.row(SquareMatrix.scalarMat {d = n} false true)(i) ≡ Vector.indexProject i true false)
  _⊜_.proof (row-scalarMat-is-indexProject {i = i}) {x} with (i ≡? x) | (x ≡? i) | commutativity ⦃ [≡]-equiv ⦄ (_≡?_) {i}{x}
  ... | 𝑇 | 𝑇 | [≡]-intro = reflexivity(_≡_)
  ... | 𝑇 | 𝐹 | ()
  ... | 𝐹 | 𝑇 | ()
  ... | 𝐹 | 𝐹 | [≡]-intro = reflexivity(_≡_)

  module _
    ⦃ oper₁ : BinaryOperator(_+ₛ_) ⦄
    ⦃ oper₂ : BinaryOperator(_⋅ₛ_) ⦄
    ⦃ ident₁ : Identityᵣ(_+ₛ_)(𝟎ₛ) ⦄
    ⦃ ident₂ : Identityᵣ(_⋅ₛ_)(𝟏ₛ) ⦄
    ⦃ absor₂ : Absorberᵣ(_⋅ₛ_)(𝟎ₛ) ⦄
    where
    instance
      postulate matrix-multPattern-identityᵣ : Identityᵣ{T₁ = Matrix(s) T}(Matrix.multPattern(_+ₛ_)(_⋅ₛ_) 𝟎ₛ) (SquareMatrix.scalarMat 𝟎ₛ 𝟏ₛ)
      {-_⊜_.proof (Identityᵣ.proof (matrix-multPattern-identityᵣ ) {M}) {x , y} =
        Matrix.proj (Matrix.multPattern(_+ₛ_)(_⋅ₛ_) 𝟎ₛ M (SquareMatrix.scalarMat 𝟎ₛ 𝟏ₛ)) (x , y)                   🝖[ _≡_ ]-[]
        Vector.foldᵣ(_+ₛ_) 𝟎ₛ (Vector.map₂(_⋅ₛ_) (Matrix.row(M)(y)) (Matrix.col(SquareMatrix.scalarMat 𝟎ₛ 𝟏ₛ)(x))) 🝖[ _≡_ ]-[ congruence₁(Vector.foldᵣ(_+ₛ_) 𝟎ₛ) (congruence₂ᵣ(Vector.map₂(_⋅ₛ_))(Matrix.row M(y)) (col-scalarMat-is-indexProject {false = 𝟎ₛ}{true = 𝟏ₛ}{i = x})) ]
        Vector.foldᵣ(_+ₛ_) 𝟎ₛ (Vector.map₂(_⋅ₛ_) (Matrix.row(M)(y)) (Vector.indexProject x 𝟏ₛ 𝟎ₛ))                 🝖[ _≡_ ]-[ congruence₁(Vector.foldᵣ(_+ₛ_) 𝟎ₛ) (Vector.map₂-indexProject-identityᵣ {v = Matrix.row(M)(y)}{i = x}) ]
        Vector.foldᵣ(_+ₛ_) 𝟎ₛ (Vector.indexProject x (Vector.proj(Matrix.row(M)(y))(x)) 𝟎ₛ)                        🝖[ _≡_ ]-[]
        Vector.foldᵣ(_+ₛ_) 𝟎ₛ (Vector.indexProject x (Matrix.proj M(x , y)) 𝟎ₛ)                                    🝖[ _≡_ ]-[ {!!} ]
        Matrix.proj M(x , y) ⋅ₛ (Vector.foldᵣ(_+ₛ_) 𝟎ₛ (Vector.indexProject x 𝟏ₛ 𝟎ₛ))                              🝖[ _≡_ ]-[ congruence₂ᵣ(_⋅ₛ_)(_) {!!} ]
        Matrix.proj M(x , y) ⋅ₛ 𝟏ₛ                                                                                🝖[ _≡_ ]-[ identityᵣ(_⋅ₛ_)(𝟏ₛ) ]
        Matrix.proj M(x , y)                                                                                🝖-end
      -}

  module _
    ⦃ oper₁ : BinaryOperator(_+ₛ_) ⦄
    ⦃ oper₂ : BinaryOperator(_⋅ₛ_) ⦄
    ⦃ ident₁ : Identityₗ(_▫₁_)(id₁) ⦄
    ⦃ ident₂ : Identityₗ(_▫₂_)(id₂) ⦄
    ⦃ absor₂ : Absorberₗ(_⋅ₛ_)(𝟎ₛ) ⦄
    where
    instance
      postulate matrix-multPattern-identityₗ : Identityₗ{T₂ = Matrix(n , n) T}(Matrix.multPattern(_▫₂_)(_▫₁_) id₁) (SquareMatrix.scalarMat id₂ id₁)

  module _
    ⦃ oper₁ : BinaryOperator(_+ₛ_) ⦄
    ⦃ oper₂ : BinaryOperator(_⋅ₛ_) ⦄
    ⦃ ident₁ : Identity(_▫₁_)(id₁) ⦄
    ⦃ ident₂ : Identity(_▫₂_)(id₂) ⦄
    ⦃ absor₂ : Absorber(_⋅ₛ_)(𝟎ₛ) ⦄
    where
    instance
      postulate matrix-multPattern-identity : Identity{T = Matrix(n , n) T}(Matrix.multPattern(_▫₂_)(_▫₁_) id₁) (SquareMatrix.scalarMat id₂ id₁)

{-
  instance
    matrix-map₂-distributivityᵣ : ⦃ dist : Distributivityᵣ(_▫₁_)(_▫₂_) ⦄ → Distributivityᵣ(Matrix.multPattern(_▫₂_)(_▫₁_) id) (Matrix.map₂{s = s}(_▫₂_))
    _⊜_.proof (Distributivityᵣ.proof (matrix-map₂-distributivityᵣ {_▫₁_} {_▫₂_} {id = id}) {a} {b} {c}) {x , y} =
      Matrix.proj(Matrix.multPattern(_▫₂_) (_▫₁_) id (Matrix.map₂(_▫₂_) a b) c) (x , y) 🝖[ _≡_ ]-[]
      Vector.foldᵣ(_▫₂_) id (Vector.map₂ (_▫₁_) (Matrix.row(Matrix.map₂(_▫₂_) a b)(y)) (Matrix.col(c)(x))) 🝖[ _≡_ ]-[]

      Vector.foldᵣ(_▫₂_) id (Vector.map₂(_▫₁_) (λ x₁ → (Matrix.proj a (x₁ , y)) ▫₂ (Matrix.proj b (x₁ , y))) (λ y₁ → Matrix.proj c (x , y₁))) 🝖[ _≡_ ]-[ {!!} ]
      (Vector.foldᵣ(_▫₂_) id (Vector.map₂ _▫₁_ (λ x₁ → Matrix.proj a (x₁ , y)) (λ y₁ → Matrix.proj c (x , y₁)))) ▫₂ (Vector.foldᵣ(_▫₂_) id (Vector.map₂(_▫₁_) (λ x₁ → Matrix.proj b (x₁ , y)) (λ y₁ → Matrix.proj c (x , y₁)))) 🝖[ _≡_ ]-[]

      (Vector.foldᵣ(_▫₂_) id (Vector.map₂ (_▫₁_) (Matrix.row(a)(y)) (Matrix.col(c)(x)))) ▫₂ (Vector.foldᵣ(_▫₂_) id (Vector.map₂ (_▫₁_) (Matrix.row(b)(y)) (Matrix.col(c)(x)))) 🝖[ _≡_ ]-[]
      Matrix.proj(Matrix.map₂(_▫₂_) (Matrix.multPattern(_▫₂_)(_▫₁_) id a c) (Matrix.multPattern(_▫₂_)(_▫₁_) id b c)) (x , y) 🝖-end
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Logic.Linear.Properties where

open import Logic.Linear using
  (LinearProp; _⊢_; Proof
  ; _^⊥; _⊗_; _⊕_; _&_; _⅋_; _⊸_; _≡_; e!_; e?_
  ; ^⊥-i; ⊗-i; ⊕-i₁; ⊕-i₂; &-i; ⅋-i; e?-i₁; e?-i₂; e!-i; e?-e; swap
  )
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin; zero; suc)
open import Data.Vec using (Vec; []; _∷_; _++_; map)

one : {n : ℕ} → Fin (suc (suc n))
one = suc zero
two : {n : ℕ} → Fin (suc (suc (suc n)))
two = suc one
three : {n : ℕ} → Fin (suc (suc (suc (suc n))))
three = suc two

-- Proof of distributivity of _⊗_ over _⊕_: p ⊗ (q ⊕ r) ≡ (p ⊗ q) ⊕ (p ⊗ r).
⊕⊗-distrib : ∀ {a}
             {A : Set a}
             (S : LinearProp A → Set a)
             {p q r : LinearProp A} →
             Proof S (p ⊗ (q ⊕ r) ≡ (p ⊗ q) ⊕ (p ⊗ r))
⊕⊗-distrib {_} {_} S {p} {q} {r} = &-i left⊸right right⊸left where
  left⊸right : S ⊢ (p ⊗ (q ⊕ r) ⊸ p ⊗ q ⊕ p ⊗ r ∷ [])
  left⊸right = ⅋-i (⅋-i (swap zero one q&r)) where
    q&r : S ⊢ (q ^⊥ & r ^⊥ ∷ p ^⊥ ∷ p ⊗ q ⊕ p ⊗ r ∷ [])
    q&r = &-i q-side r-side where
      q-side : S ⊢ (q ^⊥ ∷ p ^⊥ ∷ p ⊗ q ⊕ p ⊗ r ∷ [])
      q-side = swap one two (swap zero one disj)
        where
          conj : S ⊢ (p ⊗ q ∷ p ^⊥ ∷ q ^⊥ ∷ [])
          conj = ⊗-i (^⊥-i p) (^⊥-i q)
          disj : S ⊢ (p ⊗ q ⊕ p ⊗ r ∷ q ^⊥ ∷ p ^⊥ ∷ [])
          disj = ⊕-i₁ (swap one two conj)
      r-side : S ⊢ (r ^⊥ ∷ p ^⊥ ∷ p ⊗ q ⊕ p ⊗ r ∷ [])
      r-side = swap one two (swap zero one disj)
        where
          conj : S ⊢ (p ⊗ r ∷ p ^⊥ ∷ r ^⊥ ∷ [])
          conj = ⊗-i (^⊥-i p) (^⊥-i r)
          disj : S ⊢ (p ⊗ q ⊕ p ⊗ r ∷ r ^⊥ ∷ p ^⊥ ∷ [])
          disj = ⊕-i₂ (swap one two conj)
  right⊸left : S ⊢ (p ⊗ q ⊕ p ⊗ r ⊸ p ⊗ (q ⊕ r) ∷ [])
  right⊸left = ⅋-i (&-i q-side r-side) where
    q-side : S ⊢ (p ^⊥ ⅋ q ^⊥ ∷ p ⊗ (q ⊕ r) ∷ [])
    q-side = ⅋-i (swap one two (swap zero one conj)) where
      disj : S ⊢ (q ⊕ r ∷ q ^⊥ ∷ [])
      disj = ⊕-i₁ (^⊥-i q)
      conj : S ⊢ (p ⊗ (q ⊕ r) ∷ p ^⊥ ∷ q ^⊥ ∷ [])
      conj = ⊗-i (^⊥-i p) disj
    r-side : S ⊢ (p ^⊥ ⅋ r ^⊥ ∷ p ⊗ (q ⊕ r) ∷ [])
    r-side = ⅋-i (swap one two (swap zero one conj)) where
      disj : S ⊢ (q ⊕ r ∷ r ^⊥ ∷ [])
      disj = ⊕-i₂ (^⊥-i r)
      conj : S ⊢ (p ⊗ (q ⊕ r) ∷ p ^⊥ ∷ r ^⊥ ∷ [])
      conj = ⊗-i (^⊥-i p) disj

-- Proof of isomorphism of e!_ through _&_ and _⊗_: e! (p & q) ≡ (e! p) ⊗ (e! q).
e!-iso : ∀ {a}
         {A : Set a}
         (S : LinearProp A → Set a)
         {p q : LinearProp A} →
         Proof S (e! (p & q) ≡ (e! p) ⊗ (e! q))
e!-iso {_} {_} S {p} {q} = &-i left⊸right right⊸left where
  left⊸right : S ⊢ (e! (p & q) ⊸ e! p ⊗ e! q ∷ [])
  left⊸right = ⅋-i (e?-e (swap zero two conj)) where
    p-side : S ⊢ (p ∷ e? (p ^⊥ ⊕ q ^⊥) ∷ [])
    p-side = swap zero one (e?-i₂ disj) where
      disj : S ⊢ (p ^⊥ ⊕ q ^⊥ ∷ p ∷ [])
      disj = ⊕-i₁ (swap zero one (^⊥-i p))
    q-side : S ⊢ (q ∷ e? (p ^⊥ ⊕ q ^⊥) ∷ [])
    q-side = swap zero one (e?-i₂ disj) where
      disj : S ⊢ (p ^⊥ ⊕ q ^⊥ ∷ q ∷ [])
      disj = ⊕-i₂ (swap zero one (^⊥-i q))
    conj : S ⊢ (e! p ⊗ e! q ∷ e? (p ^⊥ ⊕ q ^⊥) ∷ e? (p ^⊥ ⊕ q ^⊥) ∷ [])
    conj = ⊗-i (e!-i p-side) (e!-i q-side)
  right⊸left : S ⊢ (e! p ⊗ e! q ⊸ e! (p & q) ∷ [])
  right⊸left = ⅋-i (⅋-i swapped) where
    p-side : S ⊢ (p ∷ e? (p ^⊥) ∷ e? (q ^⊥) ∷ [])
    p-side = swap zero two (e?-i₁ init) where
      init : S ⊢ (e? (p ^⊥) ∷ p ∷ [])
      init = e?-i₂ (swap zero one (^⊥-i p))
    q-side : S ⊢ (q ∷ e? (p ^⊥) ∷ e? (q ^⊥) ∷ [])
    q-side = swap zero one (swap one two (e?-i₁ init)) where
      init : S ⊢ (e? (q ^⊥) ∷ q ∷ [])
      init = e?-i₂ (swap zero one (^⊥-i q))
    conj : S ⊢ (p & q ∷ e? (p ^⊥) ∷ e? (q ^⊥) ∷ [])
    conj = &-i p-side q-side
    swapped : S ⊢ (e? (p ^⊥) ∷ e? (q ^⊥) ∷ e! (p & q) ∷ [])
    swapped = swap one two (swap zero one (e!-i conj))

-- Proof of mapping of _⊗_ and _⅋_: p ⊗ (q ⅋ r) ⊸ (p ⊗ q) ⅋ r.
⊗⅋-map : ∀ {a}
         {A : Set a}
         (S : LinearProp A → Set a)
         {p q r : LinearProp A} →
         Proof S (p ⊗ (q ⅋ r) ⊸ (p ⊗ q) ⅋ r)
⊗⅋-map {_} {_} S {p} {q} {r} = ⅋-i (⅋-i (swap zero two disj)) where
  pq-side : S ⊢ (q ^⊥ ∷ p ⊗ q ∷ p ^⊥ ∷ [])
  pq-side = swap zero one (swap one two (⊗-i (^⊥-i p) (^⊥-i q)))
  r-side : S ⊢ (r ^⊥ ∷ r ∷ [])
  r-side = swap zero one (^⊥-i r)
  conj : S ⊢ (q ^⊥ ⊗ r ^⊥ ∷ p ⊗ q ∷ p ^⊥ ∷ r ∷ [])
  conj = ⊗-i pq-side r-side
  disj : S ⊢ (p ⊗ q ⅋ r ∷ (q ^⊥ ⊗ r ^⊥) ∷ p ^⊥ ∷ [])
  disj = ⅋-i (swap one two (swap zero one (swap two three conj)))

max_stars_repo_name: brunoczim/linear-logic

max_issues_repo_name: brunoczim/linear-logic

max_forks_repo_name: brunoczim/linear-logic


text:
------------------------------------------------------------------------------
-- In the Agda standard library, gcd 0 0 = 0.
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.GCD.GCD00-SL where

open import Data.Nat.GCD
open import Data.Product
open import Relation.Binary.PropositionalEquality

open GCD hiding ( refl )

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

gcd00 : proj₁ (gcd 0 0) ≡ 0
gcd00 = refl

-- A different proof.
gcd00' : GCD 0 0 0
gcd00' = base

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module SystemF where

open import Data.Nat using (ℕ; zero; suc; _+_)

open import Data.Fin as Fin using (Fin; zero; suc)

open import Function as Fun using (_∘_)

open import Relation.Binary.PropositionalEquality as Eq
  using (_≡_; refl; cong; cong₂; cong-app; sym)
open Eq.≡-Reasoning

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

infixr 7 _⇒_
infix 9 `_

data Type (n : ℕ) : Set where
  `_ : Fin n → Type n
  _⇒_ : Type n → Type n → Type n
  `∀ : Type (1 + n) → Type n

⇒-cong : ∀ { n } { τ₁¹ τ₁² τ₂¹ τ₂² : Type n }
  → τ₁¹ ≡ τ₂¹
  → τ₁² ≡ τ₂²
  -- ----------------------
  → τ₁¹ ⇒ τ₁² ≡ τ₂¹ ⇒ τ₂²
⇒-cong ≡τ¹ ≡τ² = cong₂ _⇒_ ≡τ¹ ≡τ²

`∀-cong : ∀ { n } { τ₁ τ₂ : Type (1 + n) }
  → τ₁ ≡ τ₂
  -- -------------
  → `∀ τ₁ ≡ `∀ τ₂
`∀-cong ≡τ = cong `∀ ≡τ

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

open import Sigma.Subst.Core
open import Sigma.Renaming.Base

ren-τ : ∀ { m n } → Ren m n → Type m → Type n
ren-τ ρ (` α) = ` ρ α
ren-τ ρ (τ₁ ⇒ τ₂) = ren-τ ρ τ₁  ⇒ ren-τ ρ τ₂
ren-τ ρ (`∀ τ) = `∀ (ren-τ (ρ ⇑) τ)

_⇑τ : ∀ { m n } → Sub (Type n) m → Sub (Type (1 + n)) (1 + m)
σ ⇑τ = ` zero ∷ (ren-τ ↑ ∘ σ)

sub-τ : ∀ { m n } → Sub (Type n) m → Type m → Type n
sub-τ σ (` α) = σ α
sub-τ σ (τ₁ ⇒ τ₂) = sub-τ σ τ₁ ⇒ sub-τ σ τ₂
sub-τ σ (`∀ τ) = `∀ (sub-τ (σ ⇑τ) τ)

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

open import Sigma.Subst.Properties using (extensionality)
open import Sigma.Renaming.Properties using (∘-⇑-distrib; ⇑-id)

-- ------------------------------------------------------------------------
-- Congruences
-- ------------------------------------------------------------------------

ren-τ-cong : ∀  { m n } { ρ₁ ρ₂ : Ren m n }
  → ρ₁ ≡ ρ₂
  -- -------
  → ren-τ ρ₁ ≡ ren-τ ρ₂
ren-τ-cong ρ₁≡ρ₂ = cong ren-τ ρ₁≡ρ₂

⇑τ-cong : ∀ { m n } { σ₁ σ₂ : Sub (Type n) m }
  → σ₁ ≡ σ₂
  -- ------------
  → σ₁ ⇑τ ≡ σ₂ ⇑τ
⇑τ-cong σ₁≡σ₂ = cong _⇑τ  σ₁≡σ₂

-- ⇑τ✶-cong

sub-τ-cong : ∀ { m n } { σ₁ σ₂ : Sub (Type n) m }
  → σ₁ ≡ σ₂
  -- --------
  → sub-τ σ₁ ≡ sub-τ σ₂
sub-τ-cong σ₁≡σ₂ = cong sub-τ σ₁≡σ₂

-- ------------------------------------------------------------------------
-- Coincidence Laws
-- ------------------------------------------------------------------------
-- Every renaming can form a subsitution

⇑τ-coincidence : ∀ { m n } (ρ : Ren m n)
  → `_ ∘ (ρ ⇑) ≡ (`_ ∘ ρ) ⇑τ
⇑τ-coincidence ρ = extensionality lemma
  where
    lemma : ∀ x → ` ((ρ ⇑) x) ≡ ((`_ ∘ ρ) ⇑τ) x
    lemma zero = refl
    lemma (suc x) = refl

ren-τ-coincidence : ∀ { m n } (ρ : Ren m n)
  → ren-τ ρ ≡ sub-τ (`_ ∘ ρ)
ren-τ-coincidence ρ = extensionality (lemma ρ)
  where
    lemma : ∀ { m n } (ρ : Ren m n)
      → ∀ τ → ren-τ ρ τ ≡ sub-τ (`_ ∘ ρ) τ
    lemma ρ (` α) = refl
    lemma ρ (τ₁ ⇒ τ₂) = ⇒-cong (lemma ρ τ₁) (lemma ρ τ₂)
    lemma ρ (`∀ τ) = `∀-cong (
      begin
        ren-τ (ρ ⇑) τ
      ≡⟨ lemma (ρ ⇑) τ ⟩
        sub-τ (`_ ∘ (ρ ⇑)) τ
      ≡⟨ cong-app (sub-τ-cong (⇑τ-coincidence ρ)) τ ⟩
        sub-τ ((`_ ∘ ρ) ⇑τ) τ
      ∎)

-- ------------------------------------------------------------------------
-- Identity laws
-- ------------------------------------------------------------------------

⇑τ-id : ∀ { n : ℕ } →  ((`_ { n }) ⇑τ)  ≡ `_ { n = 1 + n }
⇑τ-id = extensionality (lemma)
  where
    lemma : ∀ { n : ℕ } x →  ((`_ { n }) ⇑τ) x  ≡ ` x
    lemma zero = refl
    lemma (suc x) = refl

ren-τ-idᵣ : ∀ { n } → ren-τ (id { n }) ≡ Fun.id
ren-τ-idᵣ = extensionality lemma
  where
    lemma : ∀ { n } τ →  ren-τ (id { n }) τ ≡ τ
    lemma (` α) = refl
    lemma (τ₁ ⇒ τ₂) = ⇒-cong (lemma τ₁) (lemma τ₂)
    lemma (`∀ τ) = `∀-cong (
      begin
        ren-τ (id ⇑) τ
      ≡⟨ cong-app (ren-τ-cong ⇑-id) τ ⟩
        ren-τ id τ
      ≡⟨ lemma τ ⟩
        τ
      ∎)

sub-τ-idₗ : ∀ { m n } (σ : Sub (Type n) m)
  → sub-τ σ ∘ `_  ≡ σ
sub-τ-idₗ σ = extensionality lemma
  where
    lemma : ∀ x → sub-τ σ (` x) ≡ σ x
    lemma zero = refl
    lemma (suc x) = refl

-- The functional form of the Monad Law: Right Identity
sub-τ-idᵣ : ∀ { n } → sub-τ (`_ {n}) ≡ Fun.id
sub-τ-idᵣ = extensionality lemma
  where
    lemma : ∀ { n } τ → sub-τ (`_ {n}) τ ≡ τ
    lemma (` α) = refl
    lemma (τ₁ ⇒ τ₂) = ⇒-cong (lemma τ₁) (lemma τ₂)
    lemma (`∀ τ) = `∀-cong (
      begin
        sub-τ ((`_) ⇑τ) τ
      ≡⟨ cong-app (sub-τ-cong ⇑τ-id) τ ⟩
        sub-τ (`_) τ
      ≡⟨ lemma τ ⟩
        τ
      ∎)

-- ------------------------------------------------------------------------
-- Monad Law : Compositionality
-- ------------------------------------------------------------------------
-- Lemmas required to prove the law:
-- sub-τ σ₂ ∘ sub-τ σ₁ ≡ sub-τ (sub-τ σ₂ ∘ σ₁)

∘-ren-τ-distrib : ∀ { m n k } ( ρ₁ : Ren m n ) ( ρ₂ : Ren n k )
  → ren-τ ρ₂ ∘ ren-τ ρ₁ ≡ ren-τ (ρ₂ ∘ ρ₁)
∘-ren-τ-distrib ρ₁ ρ₂ = extensionality (lemma ρ₁ ρ₂)
  where
    lemma : ∀ { m n k } ( ρ₁ : Ren m n ) ( ρ₂ : Ren n k )
      → ∀ τ → ren-τ ρ₂ (ren-τ ρ₁ τ) ≡ ren-τ (ρ₂ ∘ ρ₁) τ
    lemma ρ₁ ρ₂ (` α) = refl
    lemma ρ₁ ρ₂ (τ₁ ⇒ τ₂) = ⇒-cong (lemma ρ₁ ρ₂ τ₁) (lemma ρ₁ ρ₂ τ₂)
    lemma ρ₁ ρ₂ (`∀ τ) = `∀-cong (
      begin
        ren-τ (ρ₂ ⇑) (ren-τ (ρ₁ ⇑) τ)
      ≡⟨ lemma (ρ₁ ⇑) (ρ₂ ⇑) τ ⟩
        ren-τ (ρ₂ ⇑ ∘ ρ₁ ⇑) τ
      ≡⟨ cong-app (ren-τ-cong (∘-⇑-distrib ρ₁ ρ₂)) τ ⟩
        ren-τ ((ρ₂ ∘ ρ₁) ⇑) τ
      ∎)

∘-⇑-ren-τ-distrib : ∀ { m n k } (σ : Sub (Type n) m) (ρ : Ren n k)
  → ren-τ (ρ ⇑) ∘ (σ ⇑τ) ≡ (ren-τ ρ ∘ σ) ⇑τ
∘-⇑-ren-τ-distrib σ ρ = extensionality lemma
  where
    lemma : ∀ x → ren-τ (ρ ⇑) ((σ ⇑τ) x) ≡ ((ren-τ ρ ∘ σ) ⇑τ) x
    lemma zero = refl
    lemma (suc x) =
      begin
        ren-τ (ρ ⇑) ((σ ⇑τ) (suc x))
      ≡⟨⟩
        ren-τ (ρ ⇑) (ren-τ ↑ (σ x))
      ≡⟨ cong-app (∘-ren-τ-distrib ↑ (ρ ⇑)) (σ x) ⟩
        ren-τ (ρ ⇑ ∘ ↑) (σ x)
      ≡⟨ cong-app (sym (∘-ren-τ-distrib ρ ↑)) (σ x) ⟩
        ren-τ ↑ (ren-τ ρ (σ x))
      ≡⟨⟩
        ((ren-τ ρ ∘ σ) ⇑τ) (suc x)
      ∎

-- ∘-⇑✶-ren-τ-distrib

∘-⇑-τ-distrib : ∀  { m n k } (σ : Sub (Type k) n) (ρ : Ren m n)
  → (σ ⇑τ) ∘ (ρ ⇑) ≡ (σ ∘ ρ) ⇑τ
∘-⇑-τ-distrib σ ρ = extensionality lemma
  where
    lemma : ∀ x → (σ ⇑τ) ((ρ ⇑) x) ≡ ((σ ∘ ρ) ⇑τ) x
    lemma zero = refl
    lemma (suc x) = refl

∘-sub-ren-τ-distrib : ∀ { m n k } (σ : Sub (Type k) n) (ρ : Ren m n)
  → sub-τ σ ∘ ren-τ ρ ≡ sub-τ (σ ∘ ρ)
∘-sub-ren-τ-distrib σ ρ = extensionality (lemma σ ρ)
  where
    lemma : ∀ { m n k } (σ : Sub (Type k) n) (ρ : Ren m n)
      → ∀ τ → sub-τ σ (ren-τ ρ τ) ≡ sub-τ (σ ∘ ρ) τ
    lemma σ ρ (` α) = refl
    lemma σ ρ (τ₁ ⇒ τ₂) = ⇒-cong (lemma σ ρ τ₁) (lemma σ ρ τ₂)
    lemma σ ρ (`∀ τ) = `∀-cong (
      begin
        sub-τ (σ ⇑τ) (ren-τ (ρ ⇑) τ)
      ≡⟨ lemma (σ ⇑τ) (ρ ⇑) τ ⟩
        sub-τ ((σ ⇑τ) ∘ (ρ ⇑)) τ
      ≡⟨ cong-app (sub-τ-cong (∘-⇑-τ-distrib σ ρ)) τ ⟩
        sub-τ ((σ ∘ ρ) ⇑τ) τ
      ∎)

∘-ren-sub-τ-distrib : ∀ { m n k } (σ : Sub (Type n) m) (ρ : Ren n k)
  → ren-τ ρ ∘ sub-τ σ ≡ sub-τ (ren-τ ρ ∘ σ)
∘-ren-sub-τ-distrib σ ρ = extensionality (lemma σ ρ)
  where
    lemma : ∀ { m n k } (σ : Sub (Type n) m) (ρ : Ren n k)
      → ∀ τ → ren-τ ρ (sub-τ σ τ) ≡ sub-τ (ren-τ ρ ∘ σ) τ
    lemma σ ρ (` α) = refl
    lemma σ ρ (τ₁ ⇒ τ₂) = ⇒-cong (lemma σ ρ τ₁) (lemma σ ρ τ₂)
    lemma σ ρ (`∀ τ) = `∀-cong (
      begin
        ren-τ (ρ ⇑) (sub-τ (σ ⇑τ) τ)
      ≡⟨ lemma (σ ⇑τ) (ρ ⇑) τ ⟩
        sub-τ (ren-τ (ρ ⇑) ∘ (σ ⇑τ)) τ
      ≡⟨ cong-app (sub-τ-cong (∘-⇑-ren-τ-distrib σ ρ)) τ ⟩
        sub-τ ((ren-τ ρ ∘ σ) ⇑τ) τ
      ∎)

∘-⇑-sub-τ-distrib : ∀ { m n k } (σ₁ : Sub (Type n) m) (σ₂ : Sub (Type k) n)
  → sub-τ (σ₂ ⇑τ) ∘ σ₁ ⇑τ ≡ (sub-τ σ₂ ∘ σ₁) ⇑τ
∘-⇑-sub-τ-distrib σ₁ σ₂ = extensionality lemma
  where
    lemma : ∀ x → sub-τ (σ₂ ⇑τ) ((σ₁ ⇑τ) x) ≡ ((sub-τ σ₂ ∘ σ₁) ⇑τ) x
    lemma zero = refl
    lemma (suc x) =
      begin
        sub-τ (σ₂ ⇑τ) ((σ₁ ⇑τ) (suc x))
      ≡⟨⟩
        sub-τ (σ₂ ⇑τ) (ren-τ ↑ (σ₁ x))
      ≡⟨ cong-app (∘-sub-ren-τ-distrib (σ₂ ⇑τ) ↑) (σ₁ x) ⟩
        sub-τ ((σ₂ ⇑τ) ∘ ↑) (σ₁ x)
      ≡⟨⟩
        sub-τ (ren-τ ↑ ∘ σ₂) (σ₁ x)
      ≡⟨ cong-app (sym (∘-ren-sub-τ-distrib σ₂ ↑)) (σ₁ x) ⟩
        ren-τ ↑ (sub-τ σ₂ (σ₁ x))
      ≡⟨⟩
        ((sub-τ σ₂ ∘ σ₁) ⇑τ) (suc x)
      ∎

∘-sub-τ-distrib : ∀ { m n k } ( σ₁ : Sub (Type n) m ) ( σ₂ : Sub (Type k) n )
  → sub-τ σ₂ ∘ sub-τ σ₁ ≡ sub-τ (sub-τ σ₂ ∘ σ₁)
∘-sub-τ-distrib σ₁ σ₂ = extensionality (lemma σ₁ σ₂)
  where
    lemma : ∀ { m n k } ( σ₁ : Sub (Type n) m ) ( σ₂ : Sub (Type k) n )
      → ∀ τ → sub-τ σ₂ (sub-τ σ₁ τ) ≡ sub-τ (sub-τ σ₂ ∘ σ₁) τ
    lemma σ₁ σ₂ (` α) = refl
    lemma σ₁ σ₂ (τ₁ ⇒ τ₂) = ⇒-cong (lemma σ₁ σ₂ τ₁) (lemma σ₁ σ₂ τ₂)
    lemma σ₁ σ₂ (`∀ τ) = `∀-cong (
      begin
        sub-τ (σ₂ ⇑τ) (sub-τ (σ₁ ⇑τ) τ)
      ≡⟨ lemma (σ₁ ⇑τ) (σ₂ ⇑τ) τ ⟩
        sub-τ (sub-τ (σ₂ ⇑τ) ∘ (σ₁ ⇑τ)) τ
      ≡⟨ cong-app (sub-τ-cong (∘-⇑-sub-τ-distrib σ₁ σ₂)) τ ⟩
        sub-τ ((sub-τ σ₂ ∘ σ₁) ⇑τ) τ
      ∎)

-- ------------------------------------------------------------------------
-- Supplementary Laws
-- ------------------------------------------------------------------------

∘-sub-τ : ∀ { m n k l } ( σ₁ : Sub (Type n) m ) ( σ₂ : Sub (Type k) n ) (σ₃ : Sub (Type l) k)
  → sub-τ σ₃ ∘ (sub-τ σ₂ ∘ σ₁) ≡ sub-τ (sub-τ σ₃ ∘ σ₂) ∘ σ₁
∘-sub-τ σ₁ σ₂ σ₃ =
  begin
    sub-τ σ₃ ∘ (sub-τ σ₂ ∘ σ₁)
  ≡⟨⟩
    (sub-τ σ₃ ∘ sub-τ σ₂) ∘ σ₁
  ≡⟨ cong (_∘ σ₁) (∘-sub-τ-distrib σ₂ σ₃) ⟩
    sub-τ (sub-τ σ₃ ∘ σ₂) ∘ σ₁
  ∎

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

-- infixl 7 _·_ _[_]
-- infix 9 #_

-- data Term (n : ℕ) (m : ℕ) : Set where
--   #_ : Fin n → Term n m
--   ƛ : Term (1 + n) m → Term n m
--   _·_ : Term n m → Term n m → Term n m
--   _[_] : Term n m → Type m → Term n m
--   Λ : Term n (1 + m) → Term n m

max_stars_repo_name: johnyob/agda-sigma

max_issues_repo_name: johnyob/agda-sigma

max_forks_repo_name: johnyob/agda-sigma