From 2d471201ce5adf2754a9d812ddd47b2f506fd05c Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 11 Jun 2019 23:20:48 +0200 Subject: [PATCH] [ src-cbpv ] start to prove comonad coalgebra laws --- src-cbpv/Everything.agda | 4 +++ src-cbpv/NfCBPV.agda | 27 --------------- src-cbpv/NfCBPVLaws.agda | 75 ++++++++++++++++++++++++++++++++++++++++ src/Library.agda | 5 ++- 4 files changed, 83 insertions(+), 28 deletions(-) create mode 100644 src-cbpv/Everything.agda create mode 100644 src-cbpv/NfCBPVLaws.agda diff --git a/src-cbpv/Everything.agda b/src-cbpv/Everything.agda new file mode 100644 index 0000000..cb947b5 --- /dev/null +++ b/src-cbpv/Everything.agda @@ -0,0 +1,4 @@ +module Everything where + +import Library +import NfCBPV diff --git a/src-cbpv/NfCBPV.agda b/src-cbpv/NfCBPV.agda index 8c6b02c..b019746 100644 --- a/src-cbpv/NfCBPV.agda +++ b/src-cbpv/NfCBPV.agda @@ -284,12 +284,6 @@ join (split x c) = split x (join c) ◇-fun : Mon A → ◇ (A ⇒̂ B) →̇ (A ⇒̂ ◇ B) ◇-fun mA c a = ◇-map! (λ τ f → f (mA a τ)) c -◇-mon : Mon A → Mon (◇ A) -◇-mon mA (return a) τ = return (mA a τ) -◇-mon mA (bind u c) τ = bind {!!} (◇-mon mA c (refl ∷ τ)) -- need monotonicity of Ne -◇-mon mA (case x t) τ = case (monVar x τ) (λ i → ◇-mon mA (t i) (refl ∷ τ)) -◇-mon mA (split x c) τ = split (monVar x τ) (◇-mon mA c (refl ∷ refl ∷ τ)) - -- Monoidal functoriality -- ◇-pair : ⟨ ◇ A ⊙ ◇ B ⟩→̇ ◇ (A ×̂ B) -- does not hold! @@ -328,11 +322,6 @@ Run A = ◇ A →̇ A ⇒-run : Mon A → Run B → Run (A ⇒̂ B) ⇒-run mA rB f = rB ∘ ◇-fun mA f --- From ◇-mon we get □-run - -□-run : Run B → Run (□ B) -□-run rB c = rB ∘ ◇-map extract ∘ ◇-mon □-mon c - -- Bind for the ◇ monad ◇-elim : Run B → (A →̇ B) → ◇ A →̇ B @@ -501,22 +490,6 @@ ext (γ , a) = a ∷ γ ◇-ext : ◇ (⟦ Γ ⟧ᶜ ×̂ ⟦ P ⟧⁺) →̇ ◇ ⟦ P ∷ Γ ⟧ᶜ ◇-ext = ◇-map ext -freshᶜ₀ : (Γ : Cxt) → ◇ ⟦ Γ ⟧ᶜ Γ -freshᶜ₀ [] = return [] -freshᶜ₀ (P ∷ Γ) = ◇-ext $ - □-weak (◇-mon (monᶜ Γ) (freshᶜ₀ Γ)) -- BAD, use of ◇-mon - ⋉ fresh◇ --- freshᶜ (P ∷ Γ) = ◇-ext $ --- (λ τ → ◇-mon (monᶜ Γ) (freshᶜ Γ) (⊆-trans (_ ∷ʳ ⊆-refl) τ)) -- BAD, use of ◇-mon --- ⋉ fresh◇ - - -freshG₀ : □ (◇ ⟦ Γ ⟧ᶜ) Γ --- freshG₀ : (τ : Γ ⊆ Δ) → ◇ ⟦ Γ ⟧ᶜ Δ -freshG₀ [] = return [] -freshG₀ (P ∷ʳ τ) = ◇-mon (monᶜ _) (freshG₀ τ) (P ∷ʳ ⊆-refl) -- BAD, use of ◇-mon -freshG₀ (refl ∷ τ) = ◇-ext $ (λ τ₁ → freshG₀ (⊆-trans τ (⊆-trans (_ ∷ʳ ⊆-refl) τ₁))) ⋉ fresh◇ - -- Without the use of ◇-mon! freshᶜ : (Γ : Cxt) → □ (◇ ⟦ Γ ⟧ᶜ) Γ diff --git a/src-cbpv/NfCBPVLaws.agda b/src-cbpv/NfCBPVLaws.agda new file mode 100644 index 0000000..b6443b8 --- /dev/null +++ b/src-cbpv/NfCBPVLaws.agda @@ -0,0 +1,75 @@ +{-# OPTIONS --rewriting #-} + +module NfCBPVLaws where + +open import Library hiding (_×̇_) + +open import NfCBPV + +-- NB: mon⁺ is a comonad coalgebra + +module MonIsComonadCoalgebra where + + mon-id : ∀ (P : Ty⁺) {Γ} (a : ⟦ P ⟧⁺ Γ) → mon⁺ P a ⊆-refl ≡ a + mon-id (base o) x = {!monVar-id!} + mon-id (P₁ ×̇ P₂) (a₁ , a₂) = cong₂ _,_ (mon-id P₁ a₁) (mon-id P₂ a₂) + mon-id (Σ̇ I Ps) (i , a) = cong (i ,_) (mon-id (Ps i) a) + mon-id (□̇ N) f = funExtH (funExt (λ τ → cong f {!!})) -- ⊆-trans ⊆-refl τ ≡ τ + + -- Identity: extract ∘ mon⁺ ≡ id + + extract∘mon : ∀ (P : Ty⁺) {Γ} → extract ∘ mon⁺ P ≗ id {A = ⟦ P ⟧⁺ Γ} + extract∘mon = mon-id + + -- Associativity: □-map (mon⁺ P) ∘ mon⁺ P ≡ duplicate ∘ mon⁺ P + + mon∘mon : ∀ (P : Ty⁺) {Γ} (a : ⟦ P ⟧⁺ Γ) {Δ} {τ : Γ ⊆ Δ} {Φ} {τ' : Δ ⊆ Φ} → + mon⁺ P (mon⁺ P a τ) τ' ≡ mon⁺ P a (⊆-trans τ τ') + mon∘mon (base o) x = {!!} -- monVar∘monVar + mon∘mon (P₁ ×̇ P₂) (a₁ , a₂) = cong₂ _,_ (mon∘mon P₁ a₁) (mon∘mon P₂ a₂) + mon∘mon (Σ̇ I Ps) (i , a) = cong (i ,_) (mon∘mon (Ps i) a) + mon∘mon (□̇ N) f = {!!} -- □-mon∘□-mon + + map-mon∘mon : ∀ (P : Ty⁺) {Γ} → □-map (mon⁺ P) ∘ mon⁺ P ≗ duplicate ∘ mon⁺ P {Γ} + map-mon∘mon P a = funExtH $ funExt λ τ → funExtH $ funExt λ τ' → mon∘mon P a + + +module RunIsMonadAlgebra where + + -- Identity: run⁻ N ∘ return ≡ id + + -- Associativity: run⁻ N ∘ ◇-map (run⁻ N) ≡ run⁻ N ∘ join + + +-- ◇ preserves monotonicity +------------------------------------------------------------------------ + +-- This needs weakening of neutrals + +◇-mon : Mon A → Mon (◇ A) +◇-mon mA (return a) τ = return (mA a τ) +◇-mon mA (bind u c) τ = bind {!!} (◇-mon mA c (refl ∷ τ)) -- need monotonicity of Ne +◇-mon mA (case x t) τ = case (monVar x τ) (λ i → ◇-mon mA (t i) (refl ∷ τ)) +◇-mon mA (split x c) τ = split (monVar x τ) (◇-mon mA c (refl ∷ refl ∷ τ)) + +-- From ◇-mon we get □-run + +□-run : Run B → Run (□ B) +□-run rB c = rB ∘ ◇-map extract ∘ ◇-mon □-mon c + + +freshᶜ₀ : (Γ : Cxt) → ◇ ⟦ Γ ⟧ᶜ Γ +freshᶜ₀ [] = return [] +freshᶜ₀ (P ∷ Γ) = ◇-ext $ + □-weak (◇-mon (monᶜ Γ) (freshᶜ₀ Γ)) -- BAD, use of ◇-mon + ⋉ fresh◇ +-- freshᶜ (P ∷ Γ) = ◇-ext $ +-- (λ τ → ◇-mon (monᶜ Γ) (freshᶜ Γ) (⊆-trans (_ ∷ʳ ⊆-refl) τ)) -- BAD, use of ◇-mon +-- ⋉ fresh◇ + + +freshG₀ : □ (◇ ⟦ Γ ⟧ᶜ) Γ +-- freshG₀ : (τ : Γ ⊆ Δ) → ◇ ⟦ Γ ⟧ᶜ Δ +freshG₀ [] = return [] +freshG₀ (P ∷ʳ τ) = ◇-mon (monᶜ _) (freshG₀ τ) (P ∷ʳ ⊆-refl) -- BAD, use of ◇-mon +freshG₀ (refl ∷ τ) = ◇-ext $ (λ τ₁ → freshG₀ (⊆-trans τ (⊆-trans (_ ∷ʳ ⊆-refl) τ₁))) ⋉ fresh◇ diff --git a/src/Library.agda b/src/Library.agda index 1f6eaca..9434d89 100644 --- a/src/Library.agda +++ b/src/Library.agda @@ -20,7 +20,7 @@ open import Data.List.Relation.Sublist.Propositional public using (_⊆_; []; open import Function public using (_∘_; _∘′_; id; _$_; _ˢ_; case_of_; const; flip) -open import Relation.Binary.PropositionalEquality public using (_≡_; refl; sym; trans; cong; cong₂; subst) +open import Relation.Binary.PropositionalEquality public using (_≡_; refl; sym; trans; cong; cong₂; subst; _≗_) {-# BUILTIN REWRITE _≡_ #-} @@ -38,6 +38,9 @@ postulate funExt : ∀{a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g + funExtH : ∀{a b} {A : Set a} {B : A → Set b} {f g : {x : A} → B x} + → (∀ {x} → f {x} ≡ g {x}) + → (λ {x} → f {x}) ≡ g ⊥-elim-ext : ∀{a b} {A : Set a} {B : Set b} {f : A → ⊥} {g : A → B} → ⊥-elim {b} {B} ∘ f ≡ g ⊥-elim-ext {f = f} = funExt λ a → ⊥-elim (f a)