diff --git a/code/cubical/Examples/Dyck.agda b/code/cubical/Examples/Dyck.agda index 5778030..9971ce1 100644 --- a/code/cubical/Examples/Dyck.agda +++ b/code/cubical/Examples/Dyck.agda @@ -24,18 +24,22 @@ private data Bracket : Type where [ ] : Bracket -BracketRep : Bracket ≃ Bool -BracketRep = isoToEquiv (iso - (λ { [ → true ; ] → false }) - (λ { false → ] ; true → [ }) - (λ { false → refl ; true → refl }) - λ { [ → refl ; ] → refl }) +opaque + BracketRep : Bracket ≃ Bool + BracketRep = isoToEquiv (iso + (λ { [ → true ; ] → false }) + (λ { false → ] ; true → [ }) + (λ { false → refl ; true → refl }) + λ { [ → refl ; ] → refl }) + + isFinBracket : isFinSet Bracket + isFinBracket = EquivPresIsFinSet (invEquiv BracketRep) isFinSetBool -isFinBracket : isFinSet Bracket -isFinBracket = EquivPresIsFinSet (invEquiv BracketRep) isFinSetBool + isSetBracket : isSet Bracket + isSetBracket = isFinSet→isSet isFinBracket Alphabet : hSet _ -Alphabet = (Bracket , isFinSet→isSet isFinBracket) +Alphabet = (Bracket , isSetBracket) open import Grammar Alphabet open import Grammar.Maybe Alphabet diff --git a/code/cubical/Examples/Indexed/Dyck.agda b/code/cubical/Examples/Indexed/Dyck.agda index fd8fbd3..924a3f6 100644 --- a/code/cubical/Examples/Indexed/Dyck.agda +++ b/code/cubical/Examples/Indexed/Dyck.agda @@ -11,9 +11,9 @@ open import Cubical.Foundations.Structure open import Cubical.Data.Bool as Bool hiding (_⊕_ ;_or_) import Cubical.Data.Equality as Eq open import Cubical.Data.Nat as Nat -open import Cubical.Data.List hiding (init; rec) +open import Cubical.Data.List hiding (init; rec; map) open import Cubical.Data.Sigma -open import Cubical.Data.Sum as Sum hiding (rec) +open import Cubical.Data.Sum as Sum hiding (rec; map) open import Cubical.Data.FinSet private @@ -22,11 +22,14 @@ private open import Examples.Dyck open import Grammar Alphabet -open import Grammar.Maybe Alphabet hiding (μ) +open import Grammar.String.Properties Alphabet open import Grammar.Equivalence Alphabet open import Grammar.Inductive.Indexed Alphabet +open import Grammar.Lift Alphabet open import Term Alphabet +open StrongEquivalence + data DyckTag : Type ℓ-zero where nil' balanced' : DyckTag DyckTy : Unit → Functor Unit @@ -36,75 +39,457 @@ DyckTy _ = ⊕e DyckTag (λ IndDyck : Grammar ℓ-zero IndDyck = μ DyckTy _ -data TraceTag : Type where - eof' open' close' leftovers' unexpected' : TraceTag -TraceTys : ℕ × Bool → Functor (ℕ × Bool) -TraceTys (n , b) = ⊕e TraceTag (λ - { eof' → ⊕e (n Eq.≡ zero) (λ _ → ⊕e (b Eq.≡ true) λ _ → k ε) - ; open' → ⊗e (k (literal [)) (Var (suc n , b)) - ; close' → ⊕e (Eq.fiber suc n) λ (n-1 , _) → ⊗e (k (literal ])) (Var (n-1 , b)) - ; leftovers' → ⊕e (Eq.fiber suc n) λ (n-1 , _) → ⊕e (b Eq.≡ false) λ _ → k ε - ; unexpected' → ⊕e ((n , b) Eq.≡ (0 , false)) λ _ → ⊗e (k (literal ])) (k ⊤) - }) +NIL : ε ⊢ IndDyck +NIL = roll ∘g ⊕ᴰ-in nil' ∘g liftG -Trace : ℕ → Bool → Grammar ℓ-zero -Trace n b = μ TraceTys (n , b) - -opaque - unfolding _⊗_ ⊗-intro - parse : string ⊢ &[ n ∈ ℕ ] ⊕[ b ∈ _ ] Trace n b - parse = foldKL*r _ (record { the-ℓ = ℓ-zero ; G = _ - ; nil-case = LinΠ-intro (Nat.elim - (LinΣ-intro true ∘g roll ∘g LinΣ-intro eof' ∘g LinΣ-intro Eq.refl ∘g LinΣ-intro Eq.refl ∘g id) - (λ n-1 _ → LinΣ-intro false ∘g roll ∘g LinΣ-intro leftovers' ∘g LinΣ-intro (_ , Eq.refl) ∘g LinΣ-intro Eq.refl ∘g id)) - ; cons-case = LinΠ-intro λ n → ⟜-intro⁻ (LinΣ-elim (λ - { [ → ⟜-intro {k = Goal n} (⊸-intro⁻ ( - (LinΣ-elim λ b → ⊸-intro {k = Goal n} - (LinΣ-intro b ∘g roll ∘g LinΣ-intro open')) - ∘g LinΠ-app (suc n))) - ; ] → ⟜-intro {k = Goal n} (Nat.elim {A = λ n → _ ⊢ Goal n} - (LinΣ-intro false ∘g roll ∘g LinΣ-intro unexpected' ∘g LinΣ-intro Eq.refl ∘g id ,⊗ ⊤-intro) - (λ n-1 _ → - ⊸-intro⁻ ((LinΣ-elim λ b → ⊸-intro {k = Goal (suc n-1)} (LinΣ-intro b ∘g roll ∘g LinΣ-intro close' ∘g LinΣ-intro (_ , Eq.refl))) - ∘g LinΠ-app n-1)) - n) })) }) - where - Goal : ℕ → Grammar ℓ-zero - Goal n = ⊕[ b ∈ Bool ] Trace n b - - mkTree : Trace zero true ⊢ IndDyck - mkTree = ⊗-unit-r ∘g rec TraceTys alg (0 , true) where - Stk : ℕ → Grammar ℓ-zero - Stk = Nat.elim ε λ _ Stk⟨n⟩ → literal ] ⊗ IndDyck ⊗ Stk⟨n⟩ - GenIndDyck : ℕ × Bool → Grammar ℓ-zero - GenIndDyck (n , false) = ⊤ - GenIndDyck (n , true) = IndDyck ⊗ Stk n - alg : Algebra TraceTys GenIndDyck - alg (n , b) = LinΣ-elim (λ - { eof' → LinΣ-elim (λ { Eq.refl → LinΣ-elim λ { Eq.refl → (roll ∘g LinΣ-intro nil') ,⊗ id ∘g ⊗-unit-r⁻ } }) - ; open' → Bool.elim {A = λ b → literal [ ⊗ GenIndDyck (suc n , b) ⊢ GenIndDyck (n , b)} - (⟜4⊗ (⟜4-intro-ε (roll ∘g LinΣ-intro balanced'))) - ⊤-intro b - ; close' → LinΣ-elim (λ { (n-1 , Eq.refl) → Bool.elim - {A = - λ b → - Term (literal ] ⊗ GenIndDyck (n-1 , b)) (GenIndDyck (suc n-1 , b))} - (⟜0⊗ (roll ∘g LinΣ-intro nil')) - ⊤-intro - b } ) - ; leftovers' → LinΣ-elim λ { (n-1 , Eq.refl) → LinΣ-elim λ { Eq.refl → ⊤-intro } } - ; unexpected' → LinΣ-elim λ { Eq.refl → ⊤-intro } - }) +BALANCED : literal [ ⊗ IndDyck ⊗ literal ] ⊗ IndDyck ⊢ IndDyck +BALANCED = roll ∘g ⊕ᴰ-in balanced' ∘g liftG ,⊗ liftG ,⊗ liftG ,⊗ liftG + +appendAlg : Algebra DyckTy λ _ → IndDyck ⟜ IndDyck +appendAlg tt = ⊕ᴰ-elim λ + { nil' → ⟜-intro-ε id ∘g lowerG + ; balanced' → ⟜-intro (BALANCED + ∘g lowerG ,⊗ (⟜-app ∘g lowerG ,⊗ NIL ∘g ⊗-unit-r⁻) + ,⊗ lowerG ,⊗ (⟜-app ∘g lowerG ,⊗ id) + ∘g id ,⊗ id ,⊗ ⊗-assoc⁻ ∘g id ,⊗ ⊗-assoc⁻ ∘g ⊗-assoc⁻) + } + +append : IndDyck ⊗ IndDyck ⊢ IndDyck +append = ⟜-intro⁻ (rec _ appendAlg _) + +-- Need this lemma for the retract property below +append-nil-r : append ∘g id ,⊗ NIL ∘g ⊗-unit-r⁻ ≡ id +append-nil-r = {!!} + +data TraceTag (b : Bool) (n : ℕ) : Type where + eof' : b Eq.≡ true → n Eq.≡ zero → TraceTag b n + close' : ∀ n-1 → (suc n-1 Eq.≡ n) → TraceTag b n + open' : TraceTag b n + leftovers' : (b Eq.≡ false) → ∀ n-1 → (suc n-1 Eq.≡ n) → TraceTag b n + unexpected' : b Eq.≡ false → n Eq.≡ zero → TraceTag b n + +LP = [ +RP = ] + +-- Trace is *parameterized* by a Bool and *indexed* by a ℕ +TraceTys : Bool → ℕ → Functor ℕ +TraceTys b n = ⊕e (TraceTag b n) (λ + { (eof' x x₁) → k ε + ; (leftovers' x n-1 x₁) → k ε + ; open' → ⊗e (k (literal LP)) (Var (suc n)) + ; (close' n-1 _) → ⊗e (k (literal RP)) (Var n-1) + ; (unexpected' x x₁) → ⊗e (k (literal RP)) (k ⊤) }) + +Trace : Bool → ℕ → Grammar _ +Trace b = μ (TraceTys b) + +EOF : ε ⊢ Trace true 0 +EOF = roll ∘g ⊕ᴰ-in (eof' Eq.refl Eq.refl) ∘g liftG + +OPEN : ∀ {n b} → literal [ ⊗ Trace b (suc n) ⊢ Trace b n +OPEN = roll ∘g ⊕ᴰ-in open' ∘g liftG ,⊗ liftG + +CLOSE : ∀ {n b} → literal ] ⊗ Trace b n ⊢ Trace b (suc n) +CLOSE = roll ∘g ⊕ᴰ-in (close' _ Eq.refl) ∘g liftG ,⊗ liftG + +LEFTOVERS : ∀ {n} → ε ⊢ Trace false (suc n) +LEFTOVERS = roll ∘g ⊕ᴰ-in (leftovers' Eq.refl _ Eq.refl) ∘g liftG + +UNEXPECTED : literal ] ⊗ ⊤ ⊢ Trace false 0 +UNEXPECTED = roll ∘g ⊕ᴰ-in (unexpected' Eq.refl Eq.refl) ∘g liftG ,⊗ liftG - exhibitTrace' : IndDyck ⊢ Trace zero true - exhibitTrace' = ((⟜-app ∘g ⊸0⊗ (roll ∘g LinΣ-intro eof' ∘g LinΣ-intro Eq.refl ∘g LinΣ-intro Eq.refl)) ∘g LinΠ-app 0) ∘g rec DyckTy alg _ where - Goal : Unit → Grammar ℓ-zero - Goal _ = &[ n ∈ ℕ ] (Trace n true ⟜ Trace n true) - alg : Algebra DyckTy Goal - alg _ = LinΣ-elim (λ - { nil' → LinΠ-intro (λ n → ⟜-intro-ε id) - ; balanced' → LinΠ-intro λ n → ⟜-intro {k = Trace n true} - (roll ∘g LinΣ-intro open' - ∘g id ,⊗ ((⟜-app ∘g LinΠ-app (suc n) ,⊗ ((roll ∘g LinΣ-intro close' ∘g LinΣ-intro (_ , Eq.refl) ∘g id ,⊗ (⟜-app ∘g LinΠ-app n ,⊗ id)) ∘g ⊗-assoc⁻)) ∘g ⊗-assoc⁻) - ∘g ⊗-assoc⁻) +parseTy = &[ n ∈ ℕ ] ⊕[ b ∈ _ ] Trace b n +parse : string ⊢ parseTy +parse = foldKL*r _ (record { the-ℓ = _ ; G = _ + ; nil-case = + &ᴰ-in (Nat.elim (⊕ᴰ-in true ∘g EOF) (λ _ _ → ⊕ᴰ-in false ∘g LEFTOVERS)) + ; cons-case = &ᴰ-in λ n → + ⊕ᴰ-elim (λ + { [ → ⊕ᴰ-elim (λ b → ⊕ᴰ-in b ∘g OPEN) ∘g ⊕ᴰ-distR .fun ∘g id ,⊗ &ᴰ-π (suc n) + ; ] → Nat.elim {A = λ n → literal RP ⊗ parseTy ⊢ ⊕[ b ∈ _ ] Trace b n} + (⊕ᴰ-in false ∘g UNEXPECTED ∘g id ,⊗ ⊤-intro) + (λ n-1 _ → ⊕ᴰ-elim (λ b → ⊕ᴰ-in b ∘g CLOSE) ∘g ⊕ᴰ-distR .fun ∘g id ,⊗ &ᴰ-π n-1) + n }) + ∘g ⊕ᴰ-distL .fun + }) + +printAlg : ∀ b → Algebra (TraceTys b) (λ _ → string) +printAlg b n = ⊕ᴰ-elim λ + { (eof' _ _) → KL*.nil ∘g lowerG + ; (leftovers' _ _ _) → KL*.nil ∘g lowerG + ; open' → CONS ∘g (⊕ᴰ-in LP ∘g lowerG) ,⊗ lowerG + ; (close' _ _) → CONS ∘g (⊕ᴰ-in RP ∘g lowerG) ,⊗ lowerG + ; (unexpected' _ _) → CONS ∘g (⊕ᴰ-in RP ∘g lowerG) ,⊗ (⊤→string ∘g lowerG) + } + +print : ∀ {n b} → Trace b n ⊢ string +print = rec (TraceTys _) (printAlg _) _ + +⊕ᴰAlg : ∀ b → Algebra (TraceTys b) (λ n → ⊕[ b' ∈ _ ] Trace b' n) +⊕ᴰAlg b n = ⊕ᴰ-elim (λ + { (eof' Eq.refl Eq.refl) → ⊕ᴰ-in true ∘g EOF ∘g lowerG + ; (leftovers' Eq.refl n-1 Eq.refl) → ⊕ᴰ-in false ∘g LEFTOVERS ∘g lowerG + ; (close' n-1 Eq.refl) → + (⊕ᴰ-elim λ b' → ⊕ᴰ-in b' ∘g CLOSE) + ∘g ⊕ᴰ-distR .fun ∘g lowerG ,⊗ lowerG + ; open' → + ((⊕ᴰ-elim λ b' → ⊕ᴰ-in b' ∘g OPEN) ∘g ⊕ᴰ-distR .fun) + ∘g lowerG ,⊗ lowerG + ; (unexpected' Eq.refl Eq.refl) → + ⊕ᴰ-in false ∘g UNEXPECTED ∘g lowerG ,⊗ lowerG + }) + +⊕ᴰ-in-homo : ∀ b → + Homomorphism (TraceTys b) (initialAlgebra (TraceTys b)) (⊕ᴰAlg b) +⊕ᴰ-in-homo b .fst n = ⊕ᴰ-in b +⊕ᴰ-in-homo b .snd n = pf where + opaque + unfolding ⊕ᴰ-distR ⊗-intro + pf : ⊕ᴰ-in b ∘g initialAlgebra (TraceTys b) n + ≡ ⊕ᴰAlg b n ∘g map (TraceTys b n) λ _ → ⊕ᴰ-in b + pf = ⊕ᴰ≡ _ _ (λ + { (eof' Eq.refl Eq.refl) → refl + ; (leftovers' Eq.refl n-1 Eq.refl) → refl + ; open' → refl + ; (close' n-1 Eq.refl) → refl + ; (unexpected' Eq.refl Eq.refl) → refl }) + +parseHomo : ∀ b → Homomorphism (TraceTys b) (printAlg b) (⊕ᴰAlg b) +parseHomo b .fst n = &ᴰ-π n ∘g parse +parseHomo b .snd n = pf where + opaque + unfolding KL*r-elim ⊕ᴰ-distR CONS ⊤ + pf : &ᴰ-π n ∘g parse ∘g printAlg b n + ≡ ⊕ᴰAlg b n ∘g map (TraceTys b n) (λ n → &ᴰ-π n ∘g parse) + pf = ⊕ᴰ≡ _ _ λ + { (eof' Eq.refl Eq.refl) → refl + ; (close' n-1 Eq.refl) → refl + ; open' → refl + ; (leftovers' Eq.refl n-1 Eq.refl) → refl + ; (unexpected' Eq.refl Eq.refl) → refl + } + +Trace≅String : ∀ {n} → StrongEquivalence (⊕[ b ∈ _ ] Trace b n) string +Trace≅String {n} = mkStrEq + (⊕ᴰ-elim (λ _ → print)) + (&ᴰ-π _ ∘g parse) + (unambiguous-string _ _) + isRetr + where + isRetr : (&ᴰ-π n ∘g parse) ∘g ⊕ᴰ-elim (λ _ → print) ≡ id + isRetr = ⊕ᴰ≡ _ _ (λ b → + ind' (TraceTys b) + (⊕ᴰAlg b) + (compHomo (TraceTys b) (initialAlgebra (TraceTys b)) (printAlg b) (⊕ᴰAlg b) + (parseHomo b) + (recHomo (TraceTys b) (printAlg b))) + (⊕ᴰ-in-homo b) + n) + +{- + Next, we establish that IndDyck and Trace true zero are strongly equivalent. + + To prove this inductively, we more generally prove that Trace true n + is strongly equivalent to a "GenDyck n" that is an analogously + "unbalanced" Dyck tree. + +-} +GenDyck : ℕ → Grammar _ +GenDyck 0 = IndDyck +GenDyck (suc n-1) = IndDyck ⊗ literal RP ⊗ GenDyck n-1 + +{- First, we construct a GenDyck from a Trace -} +genBALANCED : ∀ n → literal LP ⊗ IndDyck ⊗ literal RP ⊗ GenDyck n ⊢ GenDyck n +genBALANCED zero = BALANCED +genBALANCED (suc n) = ⟜4⊗ (⟜4-intro-ε BALANCED) + +genMkTreeAlg : Algebra (TraceTys true) GenDyck +genMkTreeAlg n = ⊕ᴰ-elim (λ + { (eof' Eq.refl Eq.refl) → NIL ∘g lowerG + ; open' → genBALANCED n ∘g lowerG ,⊗ lowerG + ; (close' n-1 Eq.refl) → ⟜0⊗ NIL ∘g lowerG ,⊗ lowerG + }) + +genMkTree : ∀ {n} → Trace true n ⊢ GenDyck n +genMkTree = rec (TraceTys _) genMkTreeAlg _ + +mkTree : Trace true zero ⊢ IndDyck +mkTree = genMkTree + +{- + + Next, we extract the trace from an IndDyck and then iterate this to + extract one from a GenDyck. + + The trick to defining this by structural recursion is to map each + IndDyck recursively to a "TraceBuilder" + +-} + +genAppend : ∀ n → IndDyck ⊗ GenDyck n ⊢ GenDyck n +genAppend zero = append +genAppend (suc _) = ⟜2⊗ (⟜2-intro-ε append) + +TraceBuilder : Unit → Grammar ℓ-zero +TraceBuilder _ = &[ n ∈ _ ] (Trace true n ⟜ Trace true n) + +buildTraceAlg : Algebra DyckTy TraceBuilder +buildTraceAlg _ = ⊕ᴰ-elim (λ + { nil' → &ᴰ-intro (λ n → ⟜-intro-ε id ∘g lowerG) + ; balanced' → &ᴰ-intro λ n → ⟜-intro + -- OPEN, making a Trace n + (OPEN + -- build a Trace (suc n) with the left subtree + ∘g id ,⊗ (⟜-app ∘g &ᴰ-π (suc n) ,⊗ id) + -- CLOSE, making a Trace (suc n) + ∘g id ,⊗ id ,⊗ CLOSE + -- build a Trace n with the right subtree + ∘g id ,⊗ id ,⊗ id ,⊗ (⟜-app ∘g &ᴰ-π n ,⊗ id) + -- reassoc the builder arg to the right, and lower everything else + ∘g lowerG ,⊗ (lowerG ,⊗ (lowerG ,⊗ lowerG ,⊗ id ∘g ⊗-assoc⁻) ∘g ⊗-assoc⁻) + ∘g ⊗-assoc⁻ + ) + }) + +buildTrace : IndDyck ⊢ TraceBuilder _ +buildTrace = rec DyckTy buildTraceAlg _ + +genBuildTrace : ∀ m → GenDyck m ⊢ &[ n ∈ _ ] (Trace true (m + n) ⟜ Trace true n) +genBuildTrace zero = buildTrace +genBuildTrace (suc m) = &ᴰ-intro λ n → ⟜-intro + -- build using the left subtree + ((⟜-app ∘g (&ᴰ-π (suc (m + n)) ∘g buildTrace) ,⊗ id) + -- CLOSE the trace, to make is (suc (m + n)) + ∘g id ,⊗ CLOSE + -- recursively build using the right subtree + ∘g id ,⊗ id ,⊗ (⟜-app ∘g (&ᴰ-π n ∘g genBuildTrace m) ,⊗ id) + -- reassoc everything + ∘g id ,⊗ ⊗-assoc⁻ ∘g ⊗-assoc⁻) + +-- -- appEOF : TraceAction _ ⊢ Trace zero true +-- -- appEOF = (⟜-app ∘g ⊸0⊗ EOF ∘g &ᴰ-π 0) + +-- -- -- prove this by induction and this should imply the retract property +-- -- genRetract : +-- -- ∀ {n} → +-- -- Path (IndDyck ⊗ Trace n true ⊢ GenIndDyck (n , true)) +-- -- (genMkTree ∘g ⟜-app ∘g (&ᴰ-π n ∘g traceBuilder) ,⊗ id) +-- -- (genAppend {n = n} ∘g id ,⊗ genMkTree) +-- -- genRetract = {!!} + +-- -- genSection : +-- -- ∀ {n} → +-- -- Path (Trace n true ⊢ Trace n true) +-- -- -- seems unavoidable unfortunately +-- -- (subst (λ m → Trace n true ⊢ Trace m true) (+-zero n) +-- -- (⟜-app ∘g ⊸0⊗ EOF ∘g &ᴰ-π 0 ∘g genTraceBuilder {m = n} ∘g genMkTree)) +-- -- id +-- -- genSection = {!!} + +-- -- -- mkTree ∘g ((⟜-app ∘g ⊸0⊗ (roll ∘g ⊕ᴰ-in eof' ∘g ⊕ᴰ-in Eq.refl ∘g ⊕ᴰ-in Eq.refl)) ∘g &ᴰ-π 0) + +-- -- -- is a homomorphism from eTAlg to (initialAlgebra DyckTy) + +-- -- Dyck≅Trace : StrongEquivalence IndDyck (Trace zero true) +-- -- Dyck≅Trace = mkStrEq exhibitTrace' mkTree +-- -- {!!} -- use mkTreeAlg +-- -- (ind-id' DyckTy (compHomo DyckTy (initialAlgebra DyckTy) eTAlg (initialAlgebra DyckTy) +-- -- ((λ _ → mkTree ∘g appEOF) +-- -- , λ _ → ⊕ᴰ≡ _ _ (λ +-- -- { nil' → +-- -- cong +-- -- (rec TraceTys mkTreeAlg (0 , true) ∘g_) +-- -- (p (roll ∘g ⊕ᴰ-in eof' ∘g ⊕ᴰ-in Eq.refl ∘g ⊕ᴰ-in Eq.refl)) +-- -- ; balanced' → +-- -- mkTree ∘g appEOF ∘g eTAlg _ ∘g ⊕ᴰ-in balanced' +-- -- ≡⟨ refl ⟩ +-- -- mkTree ∘g ⟜-app ∘g ⊸0⊗ EOF ∘g ⟜-intro {k = Trace 0 true} +-- -- (OPEN +-- -- ∘g id ,⊗ (⟜-app ∘g &ᴰ-π (suc 0) ,⊗ id) +-- -- ∘g id ,⊗ id ,⊗ CLOSE +-- -- ∘g id ,⊗ id ,⊗ id ,⊗ (⟜-app ∘g &ᴰ-π 0 ,⊗ id) +-- -- ∘g id ,⊗ id ,⊗ ⊗-assoc⁻ ∘g id ,⊗ ⊗-assoc⁻ ∘g ⊗-assoc⁻) +-- -- ≡⟨ {!!} ⟩ +-- -- mkTree ∘g OPEN +-- -- ∘g id ,⊗ (⟜-app ∘g &ᴰ-π (suc 0) ,⊗ id) +-- -- ∘g id ,⊗ id ,⊗ CLOSE +-- -- ∘g id ,⊗ id ,⊗ id ,⊗ (⟜-app ∘g &ᴰ-π 0 ,⊗ id) +-- -- ∘g id ,⊗ id ,⊗ ⊗-assoc⁻ ∘g id ,⊗ ⊗-assoc⁻ ∘g ⊗-assoc⁻ +-- -- ∘g ⊸0⊗ EOF +-- -- ≡⟨ refl ⟩ +-- -- BALANCED +-- -- ∘g id ,⊗ rec TraceTys mkTreeAlg (1 , true) +-- -- ∘g id ,⊗ (⟜-app ∘g &ᴰ-π (suc 0) ,⊗ id) +-- -- ∘g id ,⊗ id ,⊗ CLOSE +-- -- ∘g id ,⊗ id ,⊗ id ,⊗ (⟜-app ∘g &ᴰ-π 0 ,⊗ id) +-- -- ∘g id ,⊗ id ,⊗ ⊗-assoc⁻ ∘g id ,⊗ ⊗-assoc⁻ ∘g ⊗-assoc⁻ +-- -- ∘g ⊸0⊗ EOF +-- -- ≡⟨ {!!} ⟩ -- TODO: tedious but just βη +-- -- BALANCED +-- -- ∘g id ,⊗ (rec TraceTys mkTreeAlg (1 , true) ∘g (⟜-app ∘g &ᴰ-π (suc 0) ,⊗ id ∘g id ,⊗ (CLOSE ∘g id ,⊗ appEOF))) +-- -- ≡⟨ (λ i → BALANCED ∘g id ,⊗ the-lemma i) ⟩ +-- -- BALANCED +-- -- ∘g id ,⊗ (mkTree ∘g appEOF) ,⊗ id ,⊗ (mkTree ∘g appEOF) +-- -- ∎ +-- -- -- ⊸0⊗ : ε ⊢ k → l ⊢ l ⊗ k +-- -- -- ⊸0⊗ f = id ,⊗ f ∘g ⊗-unit-r⁻ + +-- -- -- rec TraceTys mkTreeAlg (0 , true) ∘g +-- -- -- ⟜-app ∘g +-- -- -- id ,⊗ (roll ∘g +-- -- -- ⊕ᴰ-in eof' ∘g ⊕ᴰ-in Eq.refl ∘g ⊕ᴰ-in Eq.refl) ∘g +-- -- -- ⊗-unit-r⁻ ∘g +-- -- -- ⟜-intro {k = Trace 0 true} +-- -- -- (roll ∘g ⊕ᴰ-in open' +-- -- -- ∘g id ,⊗ ((⟜-app ∘g &ᴰ-π (suc 0) ,⊗ ((roll ∘g ⊕ᴰ-in close' ∘g ⊕ᴰ-in (_ , Eq.refl) ∘g id ,⊗ (⟜-app ∘g &ᴰ-π 0 ,⊗ id)) ∘g ⊗-assoc⁻)) ∘g ⊗-assoc⁻) +-- -- -- ∘g ⊗-assoc⁻) +-- -- -- ≡⟨ cong ((rec TraceTys mkTreeAlg (0 , true)) ∘g_) (q' _ _) ⟩ +-- -- -- rec TraceTys mkTreeAlg (0 , true) ∘g +-- -- -- roll ∘g +-- -- -- ⊕ᴰ-in open' ∘g +-- -- -- -- Bool.elim {A = λ b → literal [ ⊗ GenIndDyck (suc 0 , b) ⊢ GenIndDyck (0 , b)} +-- -- -- -- (roll ∘g ⊕ᴰ-in balanced') +-- -- -- -- ⊤-intro true ∘g +-- -- -- id ,⊗ +-- -- -- (⟜-app ∘g +-- -- -- &ᴰ-π (suc 0) ,⊗ +-- -- -- (roll ∘g +-- -- -- ⊕ᴰ-in close' ∘g +-- -- -- ⊕ᴰ-in (0 , Eq.refl) ∘g id ,⊗ (⟜-app ∘g &ᴰ-π 0 ,⊗ id) ∘g +-- -- -- ⊗-assoc⁻) ∘g +-- -- -- ⊗-assoc⁻) ∘g +-- -- -- ⊗-assoc⁻ ∘g +-- -- -- id ,⊗ (roll ∘g ⊕ᴰ-in eof' ∘g ⊕ᴰ-in Eq.refl ∘g ⊕ᴰ-in Eq.refl) ∘g +-- -- -- ⊗-unit-r⁻ +-- -- -- ≡⟨ (λ i → roll ∘g ⊕ᴰ-in balanced' ∘g id ,⊗ rec TraceTys mkTreeAlg (1 , true) ∘g ((id ,⊗ (⟜-app ∘g ⊗-intro (&ᴰ-π 1) +-- -- -- (roll ∘g +-- -- -- ⊕ᴰ-in close' ∘g +-- -- -- ⊕ᴰ-in (0 , Eq.refl) ∘g +-- -- -- id ,⊗ (⟜-app ∘g &ᴰ-π 0 ,⊗ id) ∘g ⊗-assoc⁻) ∘g ⊗-assoc⁻) +-- -- -- ∘g ⊗-assoc⁻ ∘g id ,⊗ (roll ∘g ⊕ᴰ-in eof' ∘g ⊕ᴰ-in Eq.refl ∘g ⊕ᴰ-in Eq.refl) ∘g (id ,⊗ rec TraceTys mkTreeAlg (1 , true)) ∘g {!!}) ∘g id ,⊗ id ,⊗ {!!}) ∘g (⊗-assoc⁻ ∘g +-- -- -- id ,⊗ (roll ∘g ⊕ᴰ-in eof' ∘g ⊕ᴰ-in Eq.refl ∘g ⊕ᴰ-in Eq.refl) ∘g +-- -- -- ⊗-unit-r⁻)) ⟩ + + +-- -- -- roll ∘g ⊕ᴰ-in balanced' ∘g id ,⊗ recHomo TraceTys mkTreeAlg .fst (1 , true) ∘g {!!} ∘g (⊗-assoc⁻ ∘g +-- -- -- id ,⊗ (roll ∘g ⊕ᴰ-in eof' ∘g ⊕ᴰ-in Eq.refl ∘g ⊕ᴰ-in Eq.refl) ∘g +-- -- -- ⊗-unit-r⁻) +-- -- -- -- roll ∘g +-- -- -- -- ⊕ᴰ-in balanced' ∘g +-- -- -- -- id ,⊗ ({!id!} ∘g map (DyckTy _) {!!} ∘g {!id!}) ∘g +-- -- -- -- id ,⊗ +-- -- -- -- (⟜-app ∘g +-- -- -- -- &ᴰ-π (suc 0) ,⊗ +-- -- -- -- (roll ∘g +-- -- -- -- ⊕ᴰ-in close' ∘g +-- -- -- -- ⊕ᴰ-in (0 , Eq.refl) ∘g id ,⊗ (⟜-app ∘g &ᴰ-π 0 ,⊗ id) ∘g +-- -- -- -- ⊗-assoc⁻) ∘g +-- -- -- -- ⊗-assoc⁻) ∘g +-- -- -- -- ⊗-assoc⁻ ∘g +-- -- -- -- id ,⊗ (roll ∘g ⊕ᴰ-in eof' ∘g ⊕ᴰ-in Eq.refl ∘g ⊕ᴰ-in Eq.refl) ∘g +-- -- -- -- ⊗-unit-r⁻ +-- -- -- ≡⟨ (λ i → roll ∘g ⊕ᴰ-in balanced' ∘g {!!} ) ⟩ +-- -- -- roll ∘g +-- -- -- map (DyckTy _) +-- -- -- (λ z → +-- -- -- mkTree ∘g +-- -- -- (⟜-app ∘g +-- -- -- ⊸0⊗ +-- -- -- (roll ∘g +-- -- -- ⊕ᴰ-in eof' ∘g ⊕ᴰ-in Eq.refl ∘g ⊕ᴰ-in Eq.refl)) +-- -- -- ∘g &ᴰ-π 0) +-- -- -- ∘g ⊕ᴰ-in balanced' +-- -- -- ∎ +-- -- })) +-- -- (recHomo DyckTy eTAlg)) +-- -- tt) +-- -- where +-- -- -- maybe generalize from 0 to n and prove ∀ n by induction? +-- -- the-lemma : +-- -- Path (TraceAction _ ⊗ literal ] ⊗ TraceAction _ ⊢ IndDyck ⊗ literal ] ⊗ IndDyck) +-- -- (rec TraceTys mkTreeAlg ((suc 0) , true) ∘g (⟜-app ∘g &ᴰ-π (suc 0) ,⊗ id ∘g id ,⊗ (CLOSE ∘g id ,⊗ appEOF))) +-- -- ((rec TraceTys mkTreeAlg (0 , true) ∘g appEOF) ,⊗ id ,⊗ (rec TraceTys mkTreeAlg (0 , true) ∘g appEOF)) +-- -- the-lemma = {!!} + +-- -- the-lemma' : +-- -- Path (TraceAction _ ⊗ literal ] ⊗ Trace 0 true ⊢ IndDyck ⊗ literal ] ⊗ IndDyck) +-- -- (rec TraceTys mkTreeAlg ((suc 0) , true) ∘g (⟜-app ∘g &ᴰ-π (suc 0) ,⊗ id ∘g id ,⊗ (CLOSE ∘g id ,⊗ id))) +-- -- ((rec TraceTys mkTreeAlg (0 , true) ∘g appEOF) ,⊗ id ,⊗ (rec TraceTys mkTreeAlg (0 , true))) +-- -- the-lemma' = {!!} +-- -- -- TODO rename all of these lemmas and put them in the relevant external +-- -- -- files +-- -- opaque +-- -- unfolding ε +-- -- -- Epsilon.Properties +-- -- u : unambiguous ε +-- -- u = EXTERNAL.propParses→unambiguous isFinBracket λ w → isSetString _ _ + +-- -- -- Epsilon.Properties +-- -- s : ⊗-unit-l {g = ε} ≡ ⊗-unit-r {g = ε} +-- -- s = u _ _ + +-- -- -- Epsilon.Properties +-- -- t : ⊗-unit-l⁻ {g = ε} ≡ ⊗-unit-r⁻ {g = ε} +-- -- t = +-- -- ⊗-unit-l⁻ +-- -- ≡⟨ cong (⊗-unit-l⁻ ∘g_) (sym ⊗-unit-r⁻r) ⟩ +-- -- ⊗-unit-l⁻ ∘g ⊗-unit-r ∘g ⊗-unit-r⁻ +-- -- ≡⟨ cong (λ z → ⊗-unit-l⁻ ∘g z ∘g ⊗-unit-r⁻) (sym s) ⟩ +-- -- ⊗-unit-l⁻ ∘g ⊗-unit-l ∘g ⊗-unit-r⁻ +-- -- ≡⟨ cong (_∘g ⊗-unit-r⁻) ⊗-unit-ll⁻ ⟩ +-- -- ⊗-unit-r⁻ +-- -- ∎ + +-- -- opaque +-- -- -- opaque so that ⊗-unit-r⁻ commutes for free +-- -- unfolding ⊗-unit-r⁻ ⊗-unit-l⁻ +-- -- q' : ∀ {ℓg ℓh ℓk : Level} +-- -- {g : Grammar ℓg}{h : Grammar ℓh}{k : Grammar ℓk} +-- -- (e : ε ⊢ g)(e' : k ⊗ g ⊢ h) → +-- -- ⟜-app ∘g (id ,⊗ e) ∘g ⊗-unit-r⁻ ∘g ⟜-intro e' ≡ +-- -- e' ∘g id ,⊗ e ∘g ⊗-unit-r⁻ +-- -- q' e e' = cong (_∘g (id ,⊗ e ∘g ⊗-unit-r⁻)) (⟜-β e') + +-- -- q : ∀ {ℓg ℓh : Level} +-- -- {g : Grammar ℓg}{h : Grammar ℓh} +-- -- (e : ε ⊢ g)(e' : g ⊢ h) → +-- -- ⟜-app ∘g (id ,⊗ e) ∘g ⊗-unit-r⁻ ∘g ⟜-intro-ε e' ≡ e' ∘g e +-- -- q e e' = +-- -- q' e (e' ∘g ⊗-unit-l) ∙ +-- -- cong ((e' ∘g ⊗-unit-l ∘g id ,⊗ e) ∘g_) (sym t) ∙ +-- -- cong (λ z → e' ∘g z ∘g e) ⊗-unit-l⁻l + +-- -- p : ∀ e → +-- -- ⟜-app ∘g +-- -- (id ,⊗ e) ∘g +-- -- ⊗-unit-r⁻ ∘g +-- -- ⟜-intro-ε id ≡ e +-- -- p e = q e id + +-- -- weirdAlg : ∀ b → Algebra (TraceBTys b) (λ n → ⊕[ b' ∈ _ ] Trace' b' n) +-- -- weirdAlg b n = ⊕ᴰ-elim (λ +-- -- { eof' → +-- -- ⊕ᴰ-in b +-- -- ∘g ⊕ᴰ-elim (λ { n≡0 → ⊕ᴰ-elim (λ { b≡true → +-- -- roll ∘g ⊕ᴰ-in eof' ∘g ⊕ᴰ-in n≡0 ∘g ⊕ᴰ-in b≡true }) }) +-- -- ; open' → +-- -- ⊸-intro⁻ (⊕ᴰ-elim λ b' → ⊸-intro (⊕ᴰ-in b' ∘g roll ∘g ⊕ᴰ-in open')) +-- -- ; close' → ⊕ᴰ-elim λ { n-1 → ⊸-intro⁻ (⊕ᴰ-elim λ b' → ⊸-intro (⊕ᴰ-in b' ∘g roll ∘g ⊕ᴰ-in close' ∘g ⊕ᴰ-in n-1)) } +-- -- ; leftovers' → +-- -- ⊕ᴰ-in b ∘g +-- -- ⊕ᴰ-elim (λ n-1 → ⊕ᴰ-elim (λ { b≡false → roll ∘g ⊕ᴰ-in leftovers' ∘g ⊕ᴰ-in n-1 ∘g ⊕ᴰ-in b≡false })) +-- -- ; unexpected' → ⊕ᴰ-in b ∘g ⊕ᴰ-elim λ n,b≡0,false → roll ∘g ⊕ᴰ-in unexpected' ∘g ⊕ᴰ-in n,b≡0,false +-- -- }) + +-- -- EOF' : ε ⊢ Trace' true 0 +-- -- EOF' = roll ∘g ⊕ᴰ-in eof' ∘g ⊕ᴰ-in Eq.refl ∘g ⊕ᴰ-in Eq.refl + +-- -- OPEN' : ∀ {n b} → literal [ ⊗ Trace' b (suc n) ⊢ Trace' b n +-- -- OPEN' = roll ∘g ⊕ᴰ-in open' + +-- -- CLOSE' : ∀ {n b} → literal ] ⊗ Trace' b n ⊢ Trace' b (suc n) +-- -- CLOSE' = roll ∘g ⊕ᴰ-in close' ∘g ⊕ᴰ-in (_ , Eq.refl) + + + diff --git a/code/cubical/Grammar/Dependent/Base.agda b/code/cubical/Grammar/Dependent/Base.agda index 1d303d5..5ab56be 100644 --- a/code/cubical/Grammar/Dependent/Base.agda +++ b/code/cubical/Grammar/Dependent/Base.agda @@ -20,38 +20,52 @@ private LinearΠ : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG) LinearΠ {A = A} f w = ∀ (a : A) → f a w +&ᴰ : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG) +&ᴰ = LinearΠ LinearΣ : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG) LinearΣ {A = A} f w = Σ[ a ∈ A ] f a w +-- TODO: full rename? +⊕ᴰ : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG) +⊕ᴰ = LinearΣ -Dep⊕-syntax : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG) -Dep⊕-syntax = LinearΣ +⊕ᴰ-syntax : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG) +⊕ᴰ-syntax = LinearΣ LinearΣ-syntax : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG) LinearΣ-syntax = LinearΣ -Dep&-syntax : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG) -Dep&-syntax = LinearΠ +&ᴰ-syntax : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG) +&ᴰ-syntax = LinearΠ LinearΠ-syntax : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG) LinearΠ-syntax = LinearΠ -- TODO: this precedence isn't really right syntax LinearΣ-syntax {A = A} (λ x → B) = LinΣ[ x ∈ A ] B -syntax Dep⊕-syntax {A = A} (λ x → B) = ⊕[ x ∈ A ] B +syntax ⊕ᴰ-syntax {A = A} (λ x → B) = ⊕[ x ∈ A ] B syntax LinearΠ-syntax {A = A} (λ x → B) = LinΠ[ x ∈ A ] B -syntax Dep&-syntax {A = A} (λ x → B) = &[ x ∈ A ] B +syntax &ᴰ-syntax {A = A} (λ x → B) = &[ x ∈ A ] B -module _ {A : Type ℓS} {g : Grammar ℓG}{h : A → Grammar ℓH} where - LinΠ-intro : (∀ a → g ⊢ h a) → g ⊢ LinΠ[ a ∈ A ] h a - LinΠ-intro = λ f w z a → f a w z - - LinΣ-elim : (∀ a → h a ⊢ g) → (LinΣ[ a ∈ A ] h a) ⊢ g - LinΣ-elim f w x = f (fst x) w (snd x) module _ {A : Type ℓS} {h : A → Grammar ℓH} where LinΠ-app : ∀ a → LinΠ[ a ∈ A ] h a ⊢ h a LinΠ-app = λ a w z → z a + &ᴰ-π = LinΠ-app LinΣ-intro : ∀ a → h a ⊢ LinΣ[ a ∈ A ] h a LinΣ-intro = λ a w → _,_ a + ⊕ᴰ-in = LinΣ-intro +module _ {A : Type ℓS} {g : Grammar ℓG}{h : A → Grammar ℓH} where + LinΠ-intro : (∀ a → g ⊢ h a) → g ⊢ LinΠ[ a ∈ A ] h a + LinΠ-intro = λ f w z a → f a w z + &ᴰ-intro = LinΠ-intro + &ᴰ-in = LinΠ-intro + + LinΣ-elim : (∀ a → h a ⊢ g) → (LinΣ[ a ∈ A ] h a) ⊢ g + LinΣ-elim f w x = f (fst x) w (snd x) + ⊕ᴰ-elim = LinΣ-elim + ⊕ᴰ≡ : (f f' : (⊕[ a ∈ A ] h a) ⊢ g) + → (∀ a → f ∘g ⊕ᴰ-in a ≡ f' ∘g ⊕ᴰ-in a) + → f ≡ f' + ⊕ᴰ≡ f f' fa≡fa' i w x = fa≡fa' (x .fst) i w (x .snd) diff --git a/code/cubical/Grammar/Dependent/Properties.agda b/code/cubical/Grammar/Dependent/Properties.agda index cf40a7b..e1057fc 100644 --- a/code/cubical/Grammar/Dependent/Properties.agda +++ b/code/cubical/Grammar/Dependent/Properties.agda @@ -9,6 +9,9 @@ open import Cubical.Data.FinSet open import Cubical.Foundations.Structure open import Grammar.Base Alphabet +open import Grammar.LinearProduct Alphabet +open import Grammar.LinearFunction Alphabet +open import Grammar.Equivalence.Base Alphabet open import Grammar.Properties Alphabet open import Grammar.Dependent.Base Alphabet open import Grammar.Top Alphabet @@ -19,25 +22,60 @@ private variable ℓg ℓh ℓS : Level +module _ {A : Type ℓS} {g : Grammar ℓg}{h : A → Grammar ℓh} where + open StrongEquivalence + opaque + unfolding _⊗_ + ⊕ᴰ-distL : + StrongEquivalence + ((⊕[ a ∈ A ] h a) ⊗ g) + (⊕[ a ∈ A ] (h a ⊗ g)) + ⊕ᴰ-distL .fun w (s , (a , x) , y) = a , ((s , (x , y))) + ⊕ᴰ-distL .inv w (a , (s , (x , y))) = s , ((a , x) , y) + ⊕ᴰ-distL .sec = refl + ⊕ᴰ-distL .ret = refl + + ⊕ᴰ-distR : + StrongEquivalence + (g ⊗ (⊕[ a ∈ A ] h a)) + (⊕[ a ∈ A ] (g ⊗ h a)) + ⊕ᴰ-distR .fun w (s , x , (a , y)) = a , ((s , (x , y))) + ⊕ᴰ-distR .inv w (a , (s , (x , y))) = s , (x , (a , y)) + ⊕ᴰ-distR .sec = refl + ⊕ᴰ-distR .ret = refl + + &ᴰ-strengthL : + (&[ a ∈ A ] h a) ⊗ g ⊢ &[ a ∈ A ] (h a ⊗ g) + &ᴰ-strengthL w (s , f , pg) a = s , (f a , pg) + + &ᴰ-strengthR : + g ⊗ (&[ a ∈ A ] h a) ⊢ &[ a ∈ A ] (g ⊗ h a) + &ᴰ-strengthR w (s , pg , f) a = s , (pg , f a) + module _ {A : Type ℓS} {h : A → Grammar ℓh} - {isSetA : isSet A} - (isFinSetAlphabet : isFinSet ⟨ Alphabet ⟩) + (isSetA : isSet A) where - isMono-LinΣ-intro : (a : A) → isMono (LinΣ-intro {h = h} a) - isMono-LinΣ-intro a e e' !∘e=!∘e' = + isMono-⊕ᴰ-in : (a : A) → isMono (⊕ᴰ-in {h = h} a) + isMono-⊕ᴰ-in a e e' !∘e=!∘e' = funExt λ w → funExt λ p → sym (transportRefl (e w p)) ∙ Σ-contractFst (refl , (isSetA _ _ _)) .fst (PathΣ→ΣPathTransport _ _ (funExt⁻ (funExt⁻ !∘e=!∘e' w) p)) - unambiguous'Σ : - unambiguous' (LinΣ[ a ∈ A ] h a) → + unambiguous'⊕ᴰ : + unambiguous' (⊕[ a ∈ A ] h a) → (a : A) → unambiguous' (h a) - unambiguous'Σ unambigΣ a f f' !≡ = - isMono-LinΣ-intro a f f' - (unambigΣ (LinΣ-intro a ∘g f) (LinΣ-intro a ∘g f') + unambiguous'⊕ᴰ unambig⊕ a f f' !≡ = + isMono-⊕ᴰ-in a f f' + (unambig⊕ (LinΣ-intro a ∘g f) (LinΣ-intro a ∘g f') -- Need to change the endpoints of !≡ to line up with the -- ⊤-intro at the proper domain (unambiguous⊤ _ _ ∙ !≡ ∙ sym (unambiguous⊤ _ _))) + + unambiguous⊕ᴰ : unambiguous (⊕[ a ∈ A ] h a) → (a : A) → + unambiguous (h a) + unambiguous⊕ᴰ unambig⊕ a = + unambiguous'→unambiguous + (unambiguous'⊕ᴰ (unambiguous→unambiguous' unambig⊕) a) diff --git a/code/cubical/Grammar/Inductive/Indexed.agda b/code/cubical/Grammar/Inductive/Indexed.agda index 3eaf55e..50b3b8b 100644 --- a/code/cubical/Grammar/Inductive/Indexed.agda +++ b/code/cubical/Grammar/Inductive/Indexed.agda @@ -8,10 +8,11 @@ open import Cubical.Foundations.Structure open import Helper open import Grammar Alphabet +open import Grammar.Lift Alphabet open import Term Alphabet private - variable ℓG ℓG' ℓ ℓ' : Level + variable ℓG ℓG' ℓ ℓ' ℓ'' ℓ''' : Level module _ where data Functor (A : Type ℓ) : Type (ℓ-suc ℓ) where @@ -20,60 +21,69 @@ module _ where &e ⊕e : ∀ (B : Type ℓ) → (F : B → Functor A) → Functor A ⊗e : (F : Functor A) → (F' : Functor A) → Functor A - ⟦_⟧ : {A : Type ℓ} → Functor A → (A → Grammar ℓ) → Grammar ℓ - ⟦ k h ⟧ g = h - ⟦ Var a ⟧ g = g a - ⟦ &e B F ⟧ g = &[ b ∈ B ] ⟦ F b ⟧ g - ⟦ ⊕e B F ⟧ g = ⊕[ b ∈ B ] ⟦ F b ⟧ g - ⟦ ⊗e F F' ⟧ g = ⟦ F ⟧ g ⊗' ⟦ F' ⟧ g + module _ {A : Type ℓ}{ℓ'} where + ⟦_⟧ : Functor A → (A → Grammar ℓ') → Grammar (ℓ-max ℓ ℓ') + ⟦ k h ⟧ g = LiftG ℓ' h + ⟦ Var a ⟧ g = LiftG ℓ (g a) + ⟦ &e B F ⟧ g = &[ b ∈ B ] ⟦ F b ⟧ g + ⟦ ⊕e B F ⟧ g = ⊕[ b ∈ B ] ⟦ F b ⟧ g + ⟦ ⊗e F F' ⟧ g = ⟦ F ⟧ g ⊗ ⟦ F' ⟧ g + + map : ∀ {A : Type ℓ}(F : Functor A) {g : A → Grammar ℓ'}{h : A → Grammar ℓ''} + → (∀ a → g a ⊢ h a) + → ⟦ F ⟧ g ⊢ ⟦ F ⟧ h + map (k g) f = liftG ∘g lowerG + map (Var a) f = liftG ∘g f a ∘g lowerG + map (&e B F) f = &ᴰ-intro λ a → map (F a) f ∘g &ᴰ-π a + map (⊕e B F) f = ⊕ᴰ-elim λ a → ⊕ᴰ-in a ∘g map (F a) f + map (⊗e F F') f = map F f ,⊗ map F' f module _ {A : Type ℓ} where opaque unfolding _⊗_ ⊗-intro - map : ∀ (F : Functor A) {g h : A → Grammar ℓ} - → (∀ a → g a ⊢ h a) - → ⟦ F ⟧ g ⊢ ⟦ F ⟧ h - map (k g) f = id - map (Var a) f = f a - map (&e B F) f = LinΠ-intro λ a → map (F a) f ∘g LinΠ-app a - map (⊕e B F) f = LinΣ-elim λ a → LinΣ-intro a ∘g map (F a) f - map (⊗e F F') f = map F f ,⊗ map F' f - map-id : ∀ (F : Functor A) {g : A → Grammar _} → + map-id : ∀ (F : Functor A) {g : A → Grammar ℓ'} → map F (λ a → id {g = g a}) ≡ id map-id (k g) i = id map-id (Var a) i = id - map-id (&e B F) i = LinΠ-intro (λ a → map-id (F a) i ∘g LinΠ-app a) - map-id (⊕e B F) i = LinΣ-elim (λ a → LinΣ-intro a ∘g map-id (F a) i) + map-id (&e B F) i = &ᴰ-intro (λ a → map-id (F a) i ∘g &ᴰ-π a) + map-id (⊕e B F) i = ⊕ᴰ-elim (λ a → ⊕ᴰ-in a ∘g map-id (F a) i) map-id (⊗e F F') i = map-id F i ,⊗ map-id F' i - map-∘ : ∀ (F : Functor A) {g h k : A → Grammar _} (f : ∀ a → h a ⊢ k a)(f' : ∀ a → g a ⊢ h a) + map-∘ : ∀ {g : A → Grammar ℓ'}{h : A → Grammar ℓ''}{k : A → Grammar ℓ'''} + (F : Functor A) + (f : ∀ a → h a ⊢ k a)(f' : ∀ a → g a ⊢ h a) → map F (λ a → f a ∘g f' a) ≡ map F f ∘g map F f' - map-∘ (k g) f f' i = id - map-∘ (Var a) f f' i = f a ∘g f' a - map-∘ (&e B F) f f' i = LinΠ-intro (λ a → map-∘ (F a) f f' i ∘g LinΠ-app a) - map-∘ (⊕e B F) f f' i = LinΣ-elim (λ a → LinΣ-intro a ∘g map-∘ (F a) f f' i) + map-∘ (k g) f f' i = liftG ∘g lowerG + map-∘ (Var a) f f' i = liftG ∘g f a ∘g f' a ∘g lowerG + map-∘ (&e B F) f f' i = &ᴰ-intro (λ a → map-∘ (F a) f f' i ∘g &ᴰ-π a) + map-∘ (⊕e B F) f f' i = ⊕ᴰ-elim (λ a → ⊕ᴰ-in a ∘g map-∘ (F a) f f' i) map-∘ (⊗e F F') f f' i = map-∘ F f f' i ,⊗ map-∘ F' f f' i + -- NOTE: this is only needed because ⊗ is opaque. If it's not + -- opaque this passes the positivity check. + -- https://github.com/agda/agda/issues/6970 + {-# NO_POSITIVITY_CHECK #-} data μ (F : A → Functor A) a : Grammar ℓ where roll : ⟦ F a ⟧ (μ F) ⊢ μ F a module _ {A : Type ℓ} (F : A → Functor A) where - Algebra : (A → Grammar ℓ) → Type _ + Algebra : (A → Grammar ℓ') → Type (ℓ-max ℓ ℓ') Algebra g = ∀ a → ⟦ F a ⟧ g ⊢ g a initialAlgebra : Algebra (μ F) initialAlgebra = λ a → roll - Homomorphism : ∀ {g h} → Algebra g → Algebra h → Type _ + Homomorphism : ∀ {g : A → Grammar ℓ'}{h : A → Grammar ℓ''} → Algebra g → Algebra h → Type _ Homomorphism {g = g}{h} α β = Σ[ ϕ ∈ (∀ a → g a ⊢ h a) ] (∀ a → ϕ a ∘g α a ≡ β a ∘g map (F a) ϕ) - idHomo : ∀ {g} → (α : Algebra g) → Homomorphism α α + idHomo : ∀ {g : A → Grammar ℓ'} → (α : Algebra g) → Homomorphism α α idHomo α = (λ a → id) , λ a → cong (α a ∘g_) (sym (map-id (F a))) - compHomo : ∀ {g h k} (α : Algebra g)(β : Algebra h)(η : Algebra k) + compHomo : ∀ {g : A → Grammar ℓ'}{h : A → Grammar ℓ''}{k : A → Grammar ℓ'''} + (α : Algebra g)(β : Algebra h)(η : Algebra k) → Homomorphism β η → Homomorphism α β → Homomorphism α η compHomo α β η ϕ ψ .fst a = ϕ .fst a ∘g ψ .fst a compHomo α β η ϕ ψ .snd a = @@ -81,31 +91,37 @@ module _ where ∙ cong (_∘g map (F a) (ψ .fst)) (ϕ .snd a) ∙ cong (η a ∘g_) (sym (map-∘ (F a) (ϕ .fst) (ψ .fst))) - {-# TERMINATING #-} - recHomo : ∀ {g} → (α : Algebra g) → Homomorphism initialAlgebra α - recHomo α .fst a w (roll ._ x) = - α a w (map (F a) (recHomo α .fst) w x) - recHomo α .snd a = refl + module _ {g : A → Grammar ℓ'} (α : Algebra g) where + {-# TERMINATING #-} + recHomo : Homomorphism initialAlgebra α + recHomo .fst a w (roll ._ x) = + α a w (map (F a) (recHomo .fst) w x) + recHomo .snd a = refl + + rec : ∀ a → (μ F a) ⊢ g a + rec = recHomo .fst - rec : ∀ {g} → (α : Algebra g) → ∀ a → (μ F a) ⊢ g a - rec α = recHomo α .fst + module _ (ϕ : Homomorphism initialAlgebra α) where + private + {-# TERMINATING #-} + μ-η' : ∀ a w x → ϕ .fst a w x ≡ rec a w x + μ-η' a w (roll _ x) = + (λ i → ϕ .snd a i w x) + ∙ λ i → α a w (map (F a) (λ a w x → μ-η' a w x i) w x) + μ-η : ϕ .fst ≡ rec + μ-η = funExt (λ a → funExt λ w → funExt λ x → μ-η' a w x) - module _ {g} (α : Algebra g) (ϕ : Homomorphism initialAlgebra α) where - private - {-# TERMINATING #-} - μ-η' : ∀ a w x → ϕ .fst a w x ≡ rec α a w x - μ-η' a w (roll _ x) = - (λ i → ϕ .snd a i w x) - ∙ λ i → α a w (map (F a) (λ a w x → μ-η' a w x i) w x) - μ-η : ϕ .fst ≡ rec α - μ-η = funExt (λ a → funExt λ w → funExt λ x → μ-η' a w x) + ind : (ϕ ϕ' : Homomorphism initialAlgebra α) → ϕ .fst ≡ ϕ' .fst + ind ϕ ϕ' = μ-η ϕ ∙ sym (μ-η ϕ') - ind : ∀ {g} (α : Algebra g) (ϕ ϕ' : Homomorphism initialAlgebra α) → ϕ .fst ≡ ϕ' .fst - ind α ϕ ϕ' = μ-η α ϕ ∙ sym (μ-η α ϕ') + ind' : ∀ (ϕ ϕ' : Homomorphism initialAlgebra α) → ∀ a → ϕ .fst a ≡ ϕ' .fst a + ind' ϕ ϕ' = funExt⁻ (ind ϕ ϕ') ind-id : ∀ (ϕ : Homomorphism initialAlgebra initialAlgebra) → ϕ .fst ≡ idHomo initialAlgebra .fst ind-id ϕ = ind initialAlgebra ϕ (idHomo initialAlgebra) + ind-id' : ∀ (ϕ : Homomorphism initialAlgebra initialAlgebra) a → ϕ .fst a ≡ id + ind-id' ϕ a = funExt⁻ (ind-id ϕ) a unroll : ∀ a → μ F a ⊢ ⟦ F a ⟧ (μ F) unroll a w (roll .w x) = x diff --git a/code/cubical/Grammar/KleeneStar.agda b/code/cubical/Grammar/KleeneStar.agda index 5a9ca53..1f9ae68 100644 --- a/code/cubical/Grammar/KleeneStar.agda +++ b/code/cubical/Grammar/KleeneStar.agda @@ -169,3 +169,6 @@ opaque unfolding _⊗_ cons' : ε ⊢ KL* g ⟜ KL* g ⟜ g cons' = ⟜2-intro-ε cons + + CONS : g ⊗ KL* g ⊢ KL* g + CONS = cons diff --git a/code/cubical/Grammar/Lift.agda b/code/cubical/Grammar/Lift.agda new file mode 100644 index 0000000..3cdce55 --- /dev/null +++ b/code/cubical/Grammar/Lift.agda @@ -0,0 +1,33 @@ +{-# OPTIONS --allow-unsolved-metas #-} +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Isomorphism + +module Grammar.Lift (Alphabet : hSet ℓ-zero) where + +open import Cubical.Data.List +open import Cubical.Data.Sigma +open import Cubical.Data.Nat + +open import Grammar.Base Alphabet +open import Grammar.LinearProduct Alphabet +open import Grammar.Epsilon Alphabet +open import Term.Base Alphabet +open import Term.Bilinear Alphabet + +private + variable + ℓg ℓh ℓk ℓl ℓ ℓ' : Level + g g' g'' g1 g2 g3 g4 g5 : Grammar ℓg + h h' h'' : Grammar ℓh + k : Grammar ℓk + l : Grammar ℓl + +LiftG : ∀ ℓ' → Grammar ℓ → Grammar (ℓ-max ℓ ℓ') +LiftG ℓ' g w = Lift {j = ℓ'} (g w) + +liftG : g ⊢ LiftG ℓ' g +liftG = λ w z → lift z + +lowerG : LiftG ℓ' g ⊢ g +lowerG = λ w z → z .lower diff --git a/code/cubical/Grammar/LinearFunction.agda b/code/cubical/Grammar/LinearFunction.agda index 18e03db..a67d9a8 100644 --- a/code/cubical/Grammar/LinearFunction.agda +++ b/code/cubical/Grammar/LinearFunction.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --allow-unsolved-metas #-} open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism @@ -226,3 +227,8 @@ opaque ⊸0⊗ : ε ⊢ k → l ⊢ l ⊗ k ⊸0⊗ f = id ,⊗ f ∘g ⊗-unit-r⁻ + +⟜-app⊸0⊗ : + ∀ (f : g ⊗ h ⊢ k) (x : ε ⊢ h) → + ⟜-app ∘g ⊸0⊗ x ∘g ⟜-intro f ≡ f ∘g ⊸0⊗ x +⟜-app⊸0⊗ = {!!} diff --git a/code/cubical/Grammar/LinearProduct.agda b/code/cubical/Grammar/LinearProduct.agda index a690f37..ed9e811 100644 --- a/code/cubical/Grammar/LinearProduct.agda +++ b/code/cubical/Grammar/LinearProduct.agda @@ -314,5 +314,8 @@ opaque ≡ (⊗-intro f id) ∘g ⊗-unit-r⁻ ⊗-unit-r⁻⊗-intro = refl + id,⊗id≡id : ⊗-intro id id ≡ id {g = g ⊗ h} + id,⊗id≡id = refl + _,⊗_ = ⊗-intro infixr 20 _,⊗_ diff --git a/code/cubical/Grammar/Properties.agda b/code/cubical/Grammar/Properties.agda index 7e39ac8..921f053 100644 --- a/code/cubical/Grammar/Properties.agda +++ b/code/cubical/Grammar/Properties.agda @@ -131,11 +131,32 @@ decidable→totallyParseable : decidable g → totallyParseable g decidable→totallyParseable dec-g = _ , dec-g -open isStrongEquivalence -opaque - unfolding ⊤-intro - unambiguous≅ : StrongEquivalence g h → unambiguous g → unambiguous h - unambiguous≅ {g = g}{h = h} eq unambig-g e e' = - sym (cong (_∘g e) (eq .sec)) ∙ - cong (eq .fun ∘g_) (unambig-g (eq .inv ∘g e) (eq .inv ∘g e')) ∙ - cong (_∘g e') (eq .sec) +isUnambiguousRetract : + ∀ (f : g ⊢ h) (f' : h ⊢ g) + → (f' ∘g f ≡ id) + → unambiguous h → unambiguous g +isUnambiguousRetract f f' ret unambH e e' = + cong (_∘g e) (sym ret) + ∙ cong (f' ∘g_) (unambH _ _) + ∙ cong (_∘g e') ret + +unambiguous≅ : StrongEquivalence g h → unambiguous g → unambiguous h +unambiguous≅ g≅h unambG = isUnambiguousRetract (g≅h .inv) (g≅h .fun) (g≅h .sec) unambG + where open isStrongEquivalence + +unambiguous→StrongEquivalence + : unambiguous g + → unambiguous h + → (g ⊢ h) + → (h ⊢ g) + → StrongEquivalence g h +unambiguous→StrongEquivalence unambG unambH f f' = + mkStrEq f f' (unambH (f ∘g f') id) (unambG (f' ∘g f) id) + +unambiguousRetract→StrongEquivalence + : ∀ (f : g ⊢ h) (f' : h ⊢ g) + → (f' ∘g f ≡ id) + → unambiguous h + → StrongEquivalence g h +unambiguousRetract→StrongEquivalence f f' ret unambH + = unambiguous→StrongEquivalence (isUnambiguousRetract f f' ret unambH) unambH f f'