From 0708355c7988345c98961cad087dc56eeb16ea7f Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sat, 24 Apr 2021 15:30:30 +0100 Subject: Cleanup Derivation. --- src/Cfe/Derivation/Base.agda | 54 +++++++------ src/Cfe/Derivation/Properties.agda | 152 ++++++++++++++----------------------- src/Cfe/Expression/Properties.agda | 34 ++++++++- src/Cfe/Language/Properties.agda | 6 ++ 4 files changed, 122 insertions(+), 124 deletions(-) (limited to 'src/Cfe') diff --git a/src/Cfe/Derivation/Base.agda b/src/Cfe/Derivation/Base.agda index ce368d0..0432c3d 100644 --- a/src/Cfe/Derivation/Base.agda +++ b/src/Cfe/Derivation/Base.agda @@ -8,37 +8,41 @@ module Cfe.Derivation.Base open Setoid over renaming (Carrier to C; _≈_ to _∼_) -open import Cfe.Expression over hiding (_≋_) -open import Data.Fin -open import Data.List -open import Data.List.Relation.Binary.Equality.Setoid over +open import Cfe.Expression over hiding (_≈_) +open import Data.Fin using (zero) +open import Data.List using (List; []; [_]; _++_) +open import Data.List.Relation.Binary.Equality.Setoid over using (_≋_) open import Level using (_⊔_) infix 5 _⤇_ infix 4 _≈_ data _⤇_ : Expression 0 → List C → Set (c ⊔ ℓ) where - Eps : ε ⤇ [] + Eps : ε ⤇ [] Char : ∀ {c y} → (c∼y : c ∼ y) → Char c ⤇ [ y ] - Cat : ∀ {e₁ e₂ l₁ l₂ l} → e₁ ⤇ l₁ → e₂ ⤇ l₂ → l₁ ++ l₂ ≋ l → e₁ ∙ e₂ ⤇ l - Veeˡ : ∀ {e₁ e₂ l} → e₁ ⤇ l → e₁ ∨ e₂ ⤇ l - Veeʳ : ∀ {e₁ e₂ l} → e₂ ⤇ l → e₁ ∨ e₂ ⤇ l - Fix : ∀ {e l} → e [ μ e / zero ] ⤇ l → μ e ⤇ l + Cat : ∀ {e₁ e₂ w₁ w₂ w} → e₁ ⤇ w₁ → e₂ ⤇ w₂ → w₁ ++ w₂ ≋ w → e₁ ∙ e₂ ⤇ w + Veeˡ : ∀ {e₁ e₂ w} → e₁ ⤇ w → e₁ ∨ e₂ ⤇ w + Veeʳ : ∀ {e₁ e₂ w} → e₂ ⤇ w → e₁ ∨ e₂ ⤇ w + Fix : ∀ {e w} → e [ μ e / zero ] ⤇ w → μ e ⤇ w -data _≈_ : ∀ {e l l′} → REL (e ⤇ l) (e ⤇ l′) (c ⊔ ℓ) where - Eps : Eps ≈ Eps +data _≈_ : ∀ {e w w′} → REL (e ⤇ w) (e ⤇ w′) (c ⊔ ℓ) where + Eps : Eps ≈ Eps Char : ∀ {c y y′} → (c∼y : c ∼ y) → (c∼y′ : c ∼ y′) → Char c∼y ≈ Char c∼y′ - Cat : ∀ {e₁ e₂ l l₁ l₂ l₁′ l₂′ e₁⤇l₁ e₁⤇l₁′ e₂⤇l₂ e₂⤇l₂′} → - (e₁⤇l₁≈e₁⤇l′ : _≈_ {e₁} {l₁} {l₁′} e₁⤇l₁ e₁⤇l₁′) → - (e₂⤇l₂≈e₂⤇l′ : _≈_ {e₂} {l₂} {l₂′} e₂⤇l₂ e₂⤇l₂′) → - (eq : l₁ ++ l₂ ≋ l) → (eq′ : l₁′ ++ l₂′ ≋ l) → - Cat e₁⤇l₁ e₂⤇l₂ eq ≈ Cat e₁⤇l₁′ e₂⤇l₂′ eq′ - Veeˡ : ∀ {e₁ e₂ l l′ e₁⤇l e₁⤇l′} → - (e₁⤇l≈e₁⤇l′ : _≈_ {e₁} {l} {l′} e₁⤇l e₁⤇l′) → - Veeˡ {e₂ = e₂} e₁⤇l ≈ Veeˡ e₁⤇l′ - Veeʳ : ∀ {e₁ e₂ l l′ e₂⤇l e₂⤇l′} → - (e₂⤇l≈e₂⤇l′ : _≈_ {e₂} {l} {l′} e₂⤇l e₂⤇l′) → - Veeʳ {e₁} e₂⤇l ≈ Veeʳ e₂⤇l′ - Fix : ∀ {e l l′ e[μe/0]⤇l e[μe/0]⤇l′} → - (e[μe/0]⤇l≈e[μe/0]⤇l′ : _≈_ {e [ μ e / zero ]} {l} {l′} e[μe/0]⤇l e[μe/0]⤇l′) → - Fix {e} e[μe/0]⤇l ≈ Fix e[μe/0]⤇l′ + Cat : + ∀ {e₁ e₂ w w₁ w₂ w₁′ w₂′ e₁⤇w₁ e₁⤇w₁′ e₂⤇w₂ e₂⤇w₂′} → + (e₁⤇w₁≈e₁⤇w′ : _≈_ {e₁} {w₁} {w₁′} e₁⤇w₁ e₁⤇w₁′) → + (e₂⤇w₂≈e₂⤇w′ : _≈_ {e₂} {w₂} {w₂′} e₂⤇w₂ e₂⤇w₂′) → + (eq : w₁ ++ w₂ ≋ w) → (eq′ : w₁′ ++ w₂′ ≋ w) → + Cat e₁⤇w₁ e₂⤇w₂ eq ≈ Cat e₁⤇w₁′ e₂⤇w₂′ eq′ + Veeˡ : + ∀ {e₁ e₂ w w′ e₁⤇w e₁⤇w′} → + (e₁⤇w≈e₁⤇w′ : _≈_ {e₁} {w} {w′} e₁⤇w e₁⤇w′) → + Veeˡ {e₂ = e₂} e₁⤇w ≈ Veeˡ e₁⤇w′ + Veeʳ : + ∀ {e₁ e₂ w w′ e₂⤇w e₂⤇w′} → + (e₂⤇w≈e₂⤇w′ : _≈_ {e₂} {w} {w′} e₂⤇w e₂⤇w′) → + Veeʳ {e₁} e₂⤇w ≈ Veeʳ e₂⤇w′ + Fix : + ∀ {e w w′ e[μe/0]⤇w e[μe/0]⤇w′} → + (e[μe/0]⤇w≈e[μe/0]⤇w′ : _≈_ {e [ μ e / zero ]} {w} {w′} e[μe/0]⤇w e[μe/0]⤇w′) → + Fix {e} e[μe/0]⤇w ≈ Fix e[μe/0]⤇w′ diff --git a/src/Cfe/Derivation/Properties.agda b/src/Cfe/Derivation/Properties.agda index e89d9f1..d922f2a 100644 --- a/src/Cfe/Derivation/Properties.agda +++ b/src/Cfe/Derivation/Properties.agda @@ -6,111 +6,69 @@ module Cfe.Derivation.Properties {c ℓ} (over : Setoid c ℓ) where -open Setoid over renaming (Carrier to C; _≈_ to _∼_) +open Setoid over using () renaming (Carrier to C) -open import Cfe.Context over hiding (_≋_) -open import Cfe.Expression over hiding (_≋_) -open import Cfe.Language over hiding (≤-refl; _≈_; _<_) -open import Cfe.Language.Construct.Concatenate over using (Concat) -open import Cfe.Language.Indexed.Construct.Iterate over -open import Cfe.Judgement over +open import Cfe.Context over using (∙,∙) open import Cfe.Derivation.Base over +open import Cfe.Expression over +open import Cfe.Fin using (zero) +open import Cfe.Judgement over +open import Cfe.Language over hiding (_∙_) open import Cfe.Type over using (_⊛_; _⊨_) -open import Data.Bool using (T; not; true; false) -open import Data.Empty using (⊥-elim) -open import Data.Fin as F hiding (_<_) -open import Data.List hiding (null) -open import Data.List.Relation.Binary.Equality.Setoid over -open import Data.Nat as ℕ hiding (_⊔_; _^_; _<_) -open import Data.Nat.Properties using (≤-step; m≤m+n; m≤n+m; ≤-refl; n<1+n; module ≤-Reasoning) -open import Data.Nat.Induction using () renaming (<-wellFounded to <ⁿ-wellFounded) -open import Data.Product as Product -open import Data.Product.Relation.Binary.Lex.Strict -open import Data.Sum as Sum -open import Data.Vec hiding (length; _++_) -open import Data.Vec.Relation.Binary.Pointwise.Inductive -open import Data.Vec.Relation.Binary.Pointwise.Extensional -open import Function +open import Data.Fin using (zero) +open import Data.List using (List; []; length) +open import Data.List.Relation.Binary.Pointwise using ([]; _∷_) +open import Data.Nat.Properties using (n<1+n; module ≤-Reasoning) +open import Data.Product using (_×_; _,_; -,_) +open import Data.Sum using (inj₁; inj₂) +open import Data.Vec using ([]; [_]) +open import Data.Vec.Relation.Binary.Pointwise.Inductive using ([]; _∷_) +open import Function using (_∘_) open import Induction.WellFounded -open import Level -open import Relation.Binary -import Relation.Binary.Construct.On as On -open import Relation.Binary.PropositionalEquality as ≡ hiding (subst₂; setoid) - -private - infix 4 _<_ - _<_ : Rel (List C × Expression 0) _ - _<_ = ×-Lex _≡_ ℕ._<_ _<ᵣₐₙₖ_ on (Product.map₁ length) +open import Level using (_⊔_) +open import Relation.Binary.PropositionalEquality using (refl) +import Relation.Binary.Reasoning.PartialOrder (⊆-poset {c ⊔ ℓ}) as ⊆-Reasoning +open import Relation.Nullary using (¬_) - <-wellFounded : WellFounded _<_ - <-wellFounded = On.wellFounded (Product.map₁ length) (×-wellFounded <ⁿ-wellFounded <ᵣₐₙₖ-wellFounded) - -l∈⟦e⟧⇒e⤇l : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {l} → l ∈ ⟦ e ⟧ [] → e ⤇ l -l∈⟦e⟧⇒e⤇l {e} {τ} ∙,∙⊢e∶τ {l} l∈⟦e⟧ = All.wfRec <-wellFounded _ Pred go (l , e) ∙,∙⊢e∶τ l∈⟦e⟧ +w∈⟦e⟧⇒e⤇w : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {w} → w ∈ ⟦ e ⟧ [] → e ⤇ w +w∈⟦e⟧⇒e⤇w {e = e} ctx⊢e∶τ {w} w∈⟦e⟧ = All.wfRec <ₗₑₓ-wellFounded _ Pred go (w , e) ctx⊢e∶τ w∈⟦e⟧ where - Pred : List C × Expression 0 → Set _ - Pred (l , e) = ∀ {τ} → ∙,∙ ⊢ e ∶ τ → l ∈ ⟦ e ⟧ [] → e ⤇ l - - e[μe/0]<μe : ∀ {e τ} l → ∙,∙ ⊢ μ e ∶ τ → (l , e [ μ e / F.zero ]) < (l , μ e) - e[μe/0]<μe {e} l (Fix ∙,τ⊢e∶τ)= inj₂ (≡.refl , (begin-strict - rank (e [ μ e / F.zero ]) ≡⟨ subst-preserves-rank z≤n ∙,τ⊢e∶τ (Fix ∙,τ⊢e∶τ) ⟩ - rank e <⟨ n<1+n (rank e) ⟩ - ℕ.suc (rank e) ≡⟨⟩ - rank (μ e) ∎)) - where - open ≤-Reasoning + Pred : (List C × Expression 0) → Set _ + Pred (w , e) = ∀ {τ} → ∙,∙ ⊢ e ∶ τ → w ∈ ⟦ e ⟧ [] → e ⤇ w - l₁++l₂≋l⇒∣l₁∣≤∣l∣ : ∀ {l₂ l} l₁ → l₁ ++ l₂ ≋ l → (length l₁ ℕ.< length l) ⊎ (length l₁ ≡ length l) - l₁++l₂≋l⇒∣l₁∣≤∣l∣ [] [] = inj₂ ≡.refl - l₁++l₂≋l⇒∣l₁∣≤∣l∣ [] (_ ∷ _) = inj₁ (s≤s z≤n) - l₁++l₂≋l⇒∣l₁∣≤∣l∣ (_ ∷ l₁) (_ ∷ eq) = Sum.map s≤s (cong ℕ.suc) (l₁++l₂≋l⇒∣l₁∣≤∣l∣ l₁ eq) - - l₁++l₂≋l⇒∣l₂∣≤∣l∣ : ∀ {l₂ l} l₁ → l₁ ++ l₂ ≋ l → (length l₂ ℕ.< length l) ⊎ (length l₁ ≡ 0) - l₁++l₂≋l⇒∣l₂∣≤∣l∣ [] _ = inj₂ ≡.refl - l₁++l₂≋l⇒∣l₂∣≤∣l∣ (_ ∷ []) (_ ∷ []) = inj₁ (s≤s z≤n) - l₁++l₂≋l⇒∣l₂∣≤∣l∣ (x ∷ []) (x∼y ∷ _ ∷ eq) = inj₁ ([ s≤s , (λ ()) ]′ (l₁++l₂≋l⇒∣l₂∣≤∣l∣ (x ∷ []) (x∼y ∷ eq))) - l₁++l₂≋l⇒∣l₂∣≤∣l∣ (_ ∷ x ∷ l₁) (_ ∷ eq) = inj₁ ([ ≤-step , (λ ()) ]′ (l₁++l₂≋l⇒∣l₂∣≤∣l∣ (x ∷ l₁) eq)) - - e₁