From 4b3966d9cce2324bce132243ce167ed932fccfa7 Mon Sep 17 00:00:00 2001 From: effectfully Date: Mon, 15 Aug 2016 14:35:18 +0300 Subject: [PATCH] =?UTF-8?q?observe,=20fixed=20an=20error=20in=20=5F?= =?UTF-8?q?=E2=89=85e=5F?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Core.agda | 2 +- Data/Maybe.agda | 2 +- Main.agda | 2 +- Prelude.agda | 8 +++++-- Property/Eq.agda | 55 ++++++++++++++++++++++++++++++++++++++++++++++-- 5 files changed, 62 insertions(+), 7 deletions(-) diff --git a/Core.agda b/Core.agda index f38b8ba..a3fba68 100644 --- a/Core.agda +++ b/Core.agda @@ -207,7 +207,7 @@ var i₁ , x₁ ≅s var i₂ , x₂ = x₁ ≅ x₂ _ ≅s _ = bot var i₁ , q₁ ≅e var i₂ , q₂ = i₁ ≅ i₂ -π A₁ D₁ , x₁ , e₁ ≅e π A₂ D₂ , x₂ , e₂ = D₁ x₁ , e₁ ≅e D₂ x₂ , e₂ +π A₁ D₁ , x₁ , e₁ ≅e π A₂ D₂ , x₂ , e₂ = x₁ ≅ x₂ & D₁ x₁ , e₁ ≅e D₂ x₂ , e₂ (D₁ ⊛ E₁) , s₁ , e₁ ≅e (D₂ ⊛ E₂) , s₂ , e₂ = D₁ , s₁ ≅s D₂ , s₂ & E₁ , e₁ ≅e E₂ , e₂ _ ≅e _ = bot diff --git a/Data/Maybe.agda b/Data/Maybe.agda index ba67012..fd1b468 100644 --- a/Data/Maybe.agda +++ b/Data/Maybe.agda @@ -1,6 +1,6 @@ module OTT.Data.Maybe where -open import OTT.Main +open import OTT.Main hiding (Maybe; nothing; just) maybe : ∀ {a} {α : Level a} -> Univ α -> Type₋₁ α maybe {α = α} A = cmu₋₁ α diff --git a/Main.agda b/Main.agda index 02eed71..eee7f16 100644 --- a/Main.agda +++ b/Main.agda @@ -1,6 +1,6 @@ module OTT.Main where -open import OTT.Core hiding (Maybe; nothing; just) public +open import OTT.Core public open import OTT.Coerce public open import OTT.Data.List public open import OTT.Function.Pi public diff --git a/Prelude.agda b/Prelude.agda index b60c83d..60d5477 100644 --- a/Prelude.agda +++ b/Prelude.agda @@ -3,8 +3,8 @@ module OTT.Prelude where open import Level renaming (Level to MetaLevel; zero to lzeroₘ; suc to lsucₘ; _⊔_ to _⊔ₘ_) using () public open import Function public -open import Relation.Binary.PropositionalEquality - as P renaming (refl to prefl; trans to ptrans; cong to pcong; cong₂ to pcong₂) using (_≡_) public +open import Relation.Binary.PropositionalEquality as P using (_≡_) + renaming (refl to prefl; trans to ptrans; subst to psubst; cong to pcong; cong₂ to pcong₂) public open import Data.Empty public open import Data.Nat.Base hiding (_⊔_; _≟_; erase) public open import Data.Maybe.Base using (Maybe; nothing; just) public @@ -36,6 +36,10 @@ instance pright : ∀ {α} {A : Set α} {x y z : A} -> x ≡ y -> x ≡ z -> y ≡ z pright prefl prefl = prefl +hpcong₂ : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : Set γ} {x₁ x₂} {y₁ : B x₁} {y₂ : B x₂} + -> (f : ∀ x -> B x -> C) -> (q : x₁ ≡ x₂) -> psubst B q y₁ ≡ y₂ -> f x₁ y₁ ≡ f x₂ y₂ +hpcong₂ f prefl prefl = prefl + record Apply {α β} {A : Set α} (B : A -> Set β) x : Set β where constructor tag field detag : B x diff --git a/Property/Eq.agda b/Property/Eq.agda index 8ea3f07..eaec206 100644 --- a/Property/Eq.agda +++ b/Property/Eq.agda @@ -14,8 +14,6 @@ module _ where contr : {A : Prop} {x y : ⟦ A ⟧} -> x ≡ y contr = trustMe --- We could compare functions with a finite domain for equality, --- but then equality can't be `_≡_`. SemEq : ∀ {i a} {ι : Level i} {α : Level a} {I : Type ι} -> Desc I α -> Set SemEq (var i) = ⊤ SemEq (π A D) = ⊥ @@ -71,6 +69,59 @@ mutual _≟_ {A = desc I α} {{()}} _≟_ {A = imu D j } d₁ d₂ = decMu d₁ d₂ +coerceFamEnum : ∀ {n} {e f : Apply Enum n} -> (A : Apply Enum n -> Set) -> ⟦ e ≅ f ⟧ -> A e -> A f +coerceFamEnum {0} {tag () } {tag () } A q x +coerceFamEnum {1} {tag tt } {tag tt } A q x = x +coerceFamEnum {suc (suc n)} {tag nothing } {tag nothing } A q x = x +coerceFamEnum {suc (suc n)} {tag (just _)} {tag (just _)} A q x = + coerceFamEnum (A ∘ tag ∘ just ∘ detag) q x +coerceFamEnum {suc (suc n)} {tag nothing } {tag (just _)} A () x +coerceFamEnum {suc (suc n)} {tag (just _)} {tag nothing } A () x + +mutual + observeSem : ∀ {i a} {ι : Level i} {α : Level a} + {I : Type ι} {E : Desc I α} {{eqE : ExtendEq E}} + -> (D : Desc I α) {{edD : SemEq D}} + -> (d₁ d₂ : ⟦ D ⟧ᵈ (μ E)) -> ⟦ D , d₁ ≅s D , d₂ ⟧ -> d₁ ≡ d₂ + observeSem (var i) d₁ d₂ q = observe q + observeSem (π A D) {{()}} d₁ d₂ q + observeSem (D ⊛ E) {{eqD , eqE}} (d₁ , e₁) (d₂ , e₂) (qd , qe) = + pcong₂ _,_ (observeSem D {{eqD}} d₁ d₂ qd) (observeSem E {{eqE}} e₁ e₂ qe) + + observeExtend : ∀ {i a} {ι : Level i} {α : Level a} {I : Type ι} + {E : Desc I α} {j} {{edE : ExtendEq E}} + -> (D : Desc I α) {{edD : ExtendEq D}} + -> (e₁ e₂ : Extend D (μ E) j) -> ⟦ D , e₁ ≅e D , e₂ ⟧ -> e₁ ≡ e₂ + observeExtend (var i) q₁ q₂ q = contr + observeExtend (π A D) {{eqA , eqD}} (x₁ , e₁) (x₂ , e₂) (qx , qe) + rewrite observe {x = x₁} {x₂} {{eqA}} qx = + pcong (_,_ _) (observeExtend (D x₂) {{apply eqD x₂}} e₁ e₂ qe) + observeExtend (D ⊛ E) {{eqD , eqE}} (d₁ , e₁) (d₂ , e₂) (qd , qe) = + pcong₂ _,_ (observeSem D {{eqD}} d₁ d₂ qd) (observeExtend E {{eqE}} e₁ e₂ qe) + + observeMu : ∀ {i a} {ι : Level i} {α : Level a} {I : Type ι} {j} + {D : Desc I α} {d e : μ D j} {{eqD : ExtendEq D}} + -> ⟦ d ≅ e ⟧ -> d ≡ e + observeMu {D = D} {node e₁} {node e₂} q = pcong node (observeExtend D e₁ e₂ q) + + observe : ∀ {a} {α : Level a} {A : Univ α} {x y : ⟦ A ⟧} {{eqA : Eq A}} -> ⟦ x ≅ y ⟧ -> x ≡ y + observe {A = bot } {()} {()} + observe {A = top } q = prefl + observe {A = nat } q = coerceFamℕ (_ ≡_) q prefl + observe {A = enum n } {e₁} {e₂} q = coerceFamEnum (_ ≡_) q prefl + observe {A = univ α } {{()}} + observe {A = σ A B } {x₁ , y₁} {x₂ , y₂} {{eqA , eqB}} (qx , qy) + rewrite observe {x = x₁} {x₂} {{eqA}} qx = pcong (_,_ _) (observe {{apply eqB x₂}} qy) + observe {A = π A B } {{()}} + observe {A = desc I α} {{()}} + observe {A = imu D j } {node e₁} {node e₂} q = observeMu q + +module _ where + open import Relation.Binary.PropositionalEquality.TrustMe + + eobserve : ∀ {a} {α : Level a} {A : Univ α} {x y : ⟦ A ⟧} {{eqA : Eq A}} -> ⟦ x ≅ y ⟧ -> x ≡ y + eobserve = erase ∘ observe + private module Test where open import OTT.Data.Fin