diff options
Diffstat (limited to 'src/Cfe/Expression/Properties.agda')
| -rw-r--r-- | src/Cfe/Expression/Properties.agda | 267 |
1 files changed, 207 insertions, 60 deletions
diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda index d994fe6..e520f7b 100644 --- a/src/Cfe/Expression/Properties.agda +++ b/src/Cfe/Expression/Properties.agda @@ -10,7 +10,6 @@ open Setoid over using () renaming (Carrier to C; _≈_ to _∼_) open import Algebra open import Cfe.Expression.Base over -open import Cfe.Function.Power open import Cfe.Language over hiding ( ≈-isPartialEquivalence; partialSetoid @@ -33,26 +32,31 @@ open import Cfe.Language over ; ∙-zeroʳ to ∙ˡ-zeroʳ ; ∙-zero to ∙ˡ-zero ) +open import Cfe.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise-insert) open import Data.Empty using (⊥-elim) open import Data.Fin hiding (_+_; _≤_; _<_) +open import Data.Fin.Properties using (punchIn-punchOut) open import Data.List using (List; length; _++_) open import Data.List.Properties using (length-++) +open import Data.List.Relation.Binary.Equality.Setoid over using (_≋_) open import Data.List.Relation.Binary.Pointwise using (Pointwise-length) open import Data.Nat hiding (_≟_; _⊔_; _^_) open import Data.Nat.Induction using (<-wellFounded) open import Data.Nat.Properties hiding (_≟_) open import Data.Product open import Data.Product.Relation.Binary.Lex.Strict using (×-wellFounded) -open import Data.Sum using (_⊎_; inj₁; inj₂) -open import Data.Vec hiding (length; _++_) +open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′) +open import Data.Vec hiding (length; map; _++_) open import Data.Vec.Properties -open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW - hiding (refl; sym; trans; setoid; lookup) +open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pw + hiding (refl; sym; trans; setoid; lookup; map) +open import Function using (_∘_; _|>_; id) open import Induction.WellFounded using (WellFounded) open import Level using (_⊔_) open import Relation.Binary.Construct.On using () renaming (wellFounded to on-wellFounded) open import Relation.Binary.PropositionalEquality hiding (setoid) open import Relation.Nullary +open import Relation.Nullary.Decidable using (fromWitness) private variable @@ -71,7 +75,7 @@ private ⟦⟧-mono-env (Char _) mono = ⊆-refl ⟦⟧-mono-env (e₁ ∨ e₂) mono = ∪-mono (⟦⟧-mono-env e₁ mono) (⟦⟧-mono-env e₂ mono) ⟦⟧-mono-env (e₁ ∙ e₂) mono = ∙-mono (⟦⟧-mono-env e₁ mono) (⟦⟧-mono-env e₂ mono) -⟦⟧-mono-env (Var j) mono = PW.lookup mono j +⟦⟧-mono-env (Var j) mono = Pw.lookup mono j ⟦⟧-mono-env (μ e) mono = ⋃-mono λ A⊆B → ⟦⟧-mono-env e (A⊆B ∷ mono) ⟦⟧-cong-env : ∀ (e : Expression n) {γ γ′} → Pointwise _≈ˡ_ γ γ′ → ⟦ e ⟧ γ ≈ˡ ⟦ e ⟧ γ′ @@ -80,7 +84,7 @@ private ⟦⟧-cong-env (Char _) cong = ≈ˡ-refl ⟦⟧-cong-env (e₁ ∨ e₂) cong = ∪-cong (⟦⟧-cong-env e₁ cong) (⟦⟧-cong-env e₂ cong) ⟦⟧-cong-env (e₁ ∙ e₂) cong = ∙ˡ-cong (⟦⟧-cong-env e₁ cong) (⟦⟧-cong-env e₂ cong) -⟦⟧-cong-env (Var j) cong = PW.lookup cong j +⟦⟧-cong-env (Var j) cong = Pw.lookup cong j ⟦⟧-cong-env (μ e) cong = ⋃-cong λ A≈B → ⟦⟧-cong-env e (A≈B ∷ cong) ------------------------------------------------------------------------ @@ -128,10 +132,14 @@ setoid {n} = record { isEquivalence = ≈-isEquivalence {n} } -- Definitions infix 4 _<ₗₑₓ_ +infix 4 _<ₕₑₜ_ _<ₗₑₓ_ : REL (List C × Expression m) (List C × Expression n) _ (w , e) <ₗₑₓ (w′ , e′) = length w < length w′ ⊎ length w ≡ length w′ × e <ᵣₐₙₖ e′ +_<ₕₑₜ_ : Rel (List C × ∃[ m ] Expression m) _ +(w , _ , e) <ₕₑₜ (w′ , _ , e′) = (w , e) <ₗₑₓ (w′ , e′) + ------------------------------------------------------------------------ -- Relational properties @@ -166,6 +174,9 @@ _<ₗₑₓ_ : REL (List C × Expression m) (List C × Expression n) _ <ₗₑₓ-wellFounded : WellFounded (_<ₗₑₓ_ {n}) <ₗₑₓ-wellFounded = on-wellFounded (map₁ length) (×-wellFounded <-wellFounded <ᵣₐₙₖ-wellFounded) +<ₕₑₜ-wellFounded : WellFounded _<ₕₑₜ_ +<ₕₑₜ-wellFounded = + on-wellFounded (map length (rank ∘ proj₂)) (×-wellFounded <-wellFounded <-wellFounded) ------------------------------------------------------------------------ -- Other properties @@ -175,26 +186,20 @@ rank-∨ˡ e₁ e₂ = begin-strict rank e₁ ≤⟨ m≤m+n (rank e₁) (rank e₂) ⟩ rank e₁ + rank e₂ <⟨ n<1+n (rank e₁ + rank e₂) ⟩ rank (e₁ ∨ e₂) ∎ - where - open ≤-Reasoning + where open ≤-Reasoning rank-∨ʳ : ∀ (e₁ e₂ : Expression n) → e₂ <ᵣₐₙₖ e₁ ∨ e₂ rank-∨ʳ e₁ e₂ = begin-strict rank e₂ ≤⟨ m≤n+m (rank e₂) (rank e₁) ⟩ rank e₁ + rank e₂ <⟨ n<1+n (rank e₁ + rank e₂) ⟩ rank (e₁ ∨ e₂) ∎ - where - open ≤-Reasoning + where open ≤-Reasoning rank-∙ˡ : ∀ (e₁ e₂ : Expression n) → e₁ <ᵣₐₙₖ e₁ ∙ e₂ rank-∙ˡ e₁ _ = n<1+n (rank e₁) -lex-∙ˡ : - ∀ (e₁ e₂ : Expression n) γ → - ∀ {w} → (w∈⟦e₁∙e₂⟧ : w ∈ ⟦ e₁ ∙ e₂ ⟧ γ) → - let w₁ = proj₁ w∈⟦e₁∙e₂⟧ in - (w₁ , e₁) <ₗₑₓ (w , e₁ ∙ e₂) -lex-∙ˡ e₁ e₂ γ {w} (w₁ , w₂ , w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq) with m≤n⇒m<n∨m≡n ∣w₁∣≤∣w∣ +lex-∙ˡ : ∀ (e₁ e₂ : Expression n) → ∀ w₁ {w₂ w} → w₁ ++ w₂ ≋ w → (w₁ , e₁) <ₗₑₓ (w , e₁ ∙ e₂) +lex-∙ˡ e₁ e₂ w₁ {w₂} {w} eq with m≤n⇒m<n∨m≡n ∣w₁∣≤∣w∣ where open ≤-Reasoning ∣w₁∣≤∣w∣ : length w₁ ≤ length w @@ -208,10 +213,9 @@ lex-∙ˡ e₁ e₂ γ {w} (w₁ , w₂ , w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ lex-∙ʳ : ∀ (e₁ e₂ : Expression n) γ → ¬ Null (⟦ e₁ ⟧ γ) → - ∀ {w} → (w∈⟦e₁∙e₂⟧ : w ∈ ⟦ e₁ ∙ e₂ ⟧ γ) → - let w₂ = proj₁ (proj₂ w∈⟦e₁∙e₂⟧) in + ∀ {w₁ w₂ w} → w₁ ∈ ⟦ e₁ ⟧ γ → w₁ ++ w₂ ≋ w → (w₂ , e₂) <ₗₑₓ (w , e₁ ∙ e₂) -lex-∙ʳ e₁ _ γ ε∉⟦e₁⟧ {w} (w₁ , w₂ , w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq) with m≤n⇒m<n∨m≡n ∣w₂∣≤∣w∣ +lex-∙ʳ e₁ _ γ ε∉⟦e₁⟧ {w₁} {w₂} {w} w₁∈⟦e₁⟧ eq with m≤n⇒m<n∨m≡n ∣w₂∣≤∣w∣ where open ≤-Reasoning ∣w₂∣≤∣w∣ : length w₂ ≤ length w @@ -223,14 +227,13 @@ lex-∙ʳ e₁ _ γ ε∉⟦e₁⟧ {w} (w₁ , w₂ , w₁∈⟦e₁⟧ , w₂ ... | inj₁ ∣w₂∣<∣w∣ = inj₁ ∣w₂∣<∣w∣ ... | inj₂ ∣w₂∣≡∣w∣ = ⊥-elim (ε∉⟦e₁⟧ (∣w∣≡0+w∈A⇒ε∈A {A = ⟦ e₁ ⟧ γ} ∣w₁∣≡0 w₁∈⟦e₁⟧)) where + open ≤-Reasoning ∣w₁∣≡0 : length w₁ ≡ 0 ∣w₁∣≡0 = +-cancelʳ-≡ (length w₁) 0 (begin-equality length w₁ + length w₂ ≡˘⟨ length-++ w₁ ⟩ length (w₁ ++ w₂) ≡⟨ Pointwise-length eq ⟩ length w ≡˘⟨ ∣w₂∣≡∣w∣ ⟩ length w₂ ∎) - where - open ≤-Reasoning rank-μ : ∀ (e : Expression (suc n)) → e <ᵣₐₙₖ μ e rank-μ e = n<1+n (rank e) @@ -258,15 +261,16 @@ Var-inj : ∀ {j k} → Var {n} j ≈ Var k → j ≡ k Var-inj {.(suc _)} {zero} {zero} j≈k = refl Var-inj {.(suc _)} {zero} {suc k} j≈k = ⊥-elim (ε∉∅ (Null-resp-≈ ｛ε｝≈∅ ε∈｛ε｝)) where - open import Relation.Binary.Reasoning.Setoid setoidˡ - ｛ε｝≈∅ = begin - ｛ε｝ {ℓ} ≈⟨ j≈k (｛ε｝ ∷ replicate ∅) ⟩ + open ⊆-Reasoning + ｛ε｝≈∅ : ｛ε｝ {ℓ} ≈ˡ ∅ {c ⊔ ℓ} + ｛ε｝≈∅ = begin-equality + ｛ε｝ ≈⟨ j≈k (｛ε｝ ∷ replicate ∅) ⟩ lookup (replicate ∅) k ≡⟨ lookup-replicate k ∅ ⟩ ∅ ∎ Var-inj {.(suc _)} {suc j} {zero} j≈k = ⊥-elim (ε∉∅ (Null-resp-≈ ｛ε｝≈∅ ε∈｛ε｝)) where - open import Relation.Binary.Reasoning.Setoid setoidˡ - ｛ε｝≈∅ = begin + open ⊆-Reasoning + ｛ε｝≈∅ = begin-equality ｛ε｝ {ℓ} ≡˘⟨ lookup-replicate j ｛ε｝ ⟩ lookup (replicate ｛ε｝) j ≈⟨ j≈k (∅ ∷ replicate ｛ε｝) ⟩ ∅ ∎ @@ -500,31 +504,40 @@ Var-inj {.(suc _)} {suc j} {suc k} j≈k = cong suc (Var-inj λ γ → j≈k ( -- Functional properties μ-cong : μ_ Preserves _≈_ ⟶ (_≈_ {n}) -μ-cong {x = e} {e′} e≈e′ γ = ⋃-cong λ {A} {B} A≈B → begin - ⟦ e ⟧ (A ∷ γ) ≈⟨ ⟦⟧-cong-env e (A≈B ∷ PW.refl ≈ˡ-refl) ⟩ +μ-cong {x = e} {e′} e≈e′ γ = ⋃-cong λ {A} {B} A≈B → begin-equality + ⟦ e ⟧ (A ∷ γ) ≈⟨ ⟦⟧-cong-env e (A≈B ∷ Pw.refl ≈ˡ-refl) ⟩ ⟦ e ⟧ (B ∷ γ) ≈⟨ e≈e′ (B ∷ γ) ⟩ ⟦ e′ ⟧ (B ∷ γ) ∎ - where - open import Relation.Binary.Reasoning.Setoid setoidˡ + where open ⊆-Reasoning ------------------------------------------------------------------------ -- Properties of wkn ------------------------------------------------------------------------ -- Algebraic properties -wkn-cong : ∀ (e : Expression n) i γ A → ⟦ wkn e i ⟧ (insert γ i A) ≈ˡ ⟦ e ⟧ γ -wkn-cong ⊥ i γ A = ≈ˡ-refl -wkn-cong ε i γ A = ≈ˡ-refl -wkn-cong (Char _) i γ A = ≈ˡ-refl -wkn-cong (e₁ ∨ e₂) i γ A = ∪-cong (wkn-cong e₁ i γ A) (wkn-cong e₂ i γ A) -wkn-cong (e₁ ∙ e₂) i γ A = ∙ˡ-cong (wkn-cong e₁ i γ A) (wkn-cong e₂ i γ A) -wkn-cong (Var j) i γ A = ≈ˡ-reflexive (insert-punchIn γ i A j) -wkn-cong (μ e) i γ A = ⋃-cong λ {B} {C} B≈C → begin - ⟦ wkn e (suc i) ⟧ (B ∷ insert γ i A) ≈⟨ ⟦⟧-cong-env (wkn e (suc i)) (B≈C ∷ PW.refl ≈ˡ-refl) ⟩ - ⟦ wkn e (suc i) ⟧ (C ∷ insert γ i A) ≈⟨ wkn-cong e (suc i) (C ∷ γ) A ⟩ +⟦⟧-wkn : ∀ (e : Expression n) i γ A → ⟦ wkn e i ⟧ (insert γ i A) ≈ˡ ⟦ e ⟧ γ +⟦⟧-wkn ⊥ i γ A = ≈ˡ-refl +⟦⟧-wkn ε i γ A = ≈ˡ-refl +⟦⟧-wkn (Char _) i γ A = ≈ˡ-refl +⟦⟧-wkn (e₁ ∨ e₂) i γ A = ∪-cong (⟦⟧-wkn e₁ i γ A) (⟦⟧-wkn e₂ i γ A) +⟦⟧-wkn (e₁ ∙ e₂) i γ A = ∙ˡ-cong (⟦⟧-wkn e₁ i γ A) (⟦⟧-wkn e₂ i γ A) +⟦⟧-wkn (Var j) i γ A = ≈ˡ-reflexive (insert-punchIn γ i A j) +⟦⟧-wkn (μ e) i γ A = ⋃-cong λ {B} {C} B≈C → begin-equality + ⟦ wkn e (suc i) ⟧ (B ∷ insert γ i A) ≈⟨ ⟦⟧-cong-env (wkn e (suc i)) (B≈C ∷ Pw.refl ≈ˡ-refl) ⟩ + ⟦ wkn e (suc i) ⟧ (C ∷ insert γ i A) ≈⟨ ⟦⟧-wkn e (suc i) (C ∷ γ) A ⟩ ⟦ e ⟧ (C ∷ γ) ∎ - where - open import Relation.Binary.Reasoning.Setoid setoidˡ + where open ⊆-Reasoning + +wkn-mono : + ∀ (e₁ e₂ : Expression n) i → (∀ γ → ⟦ e₁ ⟧ γ ⊆ ⟦ e₂ ⟧ γ) → ∀ γ → ⟦ wkn e₁ i ⟧ γ ⊆ ⟦ wkn e₂ i ⟧ γ +wkn-mono e₁ e₂ i mono γ = begin + ⟦ wkn e₁ i ⟧ γ ≡˘⟨ cong ⟦ wkn e₁ i ⟧ (insert-remove γ i) ⟩ + ⟦ wkn e₁ i ⟧ (insert (remove γ i) i (lookup γ i)) ≈⟨ ⟦⟧-wkn e₁ i (remove γ i) (lookup γ i) ⟩ + ⟦ e₁ ⟧ (remove γ i) ⊆⟨ mono (remove γ i) ⟩ + ⟦ e₂ ⟧ (remove γ i) ≈˘⟨ ⟦⟧-wkn e₂ i (remove γ i) (lookup γ i) ⟩ + ⟦ wkn e₂ i ⟧ (insert (remove γ i) i (lookup γ i)) ≡⟨ cong ⟦ wkn e₂ i ⟧ (insert-remove γ i) ⟩ + ⟦ wkn e₂ i ⟧ γ ∎ + where open ⊆-Reasoning -- Syntactic properties @@ -544,7 +557,7 @@ rank-wkn (μ e) i = cong suc (rank-wkn e (suc i)) μ-wkn e γ = ≈ˡ-trans (∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G λ { 0 → ≈ˡ-refl - ; (suc n) → wkn-cong e zero γ (((λ X → ⟦ wkn e zero ⟧ (X ∷ γ)) ^ n) ∅) + ; (suc n) → ⟦⟧-wkn e zero γ (Iter (λ X → ⟦ wkn e zero ⟧ (X ∷ γ)) ∅ n) }) (⋃-inverseʳ (⟦ e ⟧ γ)) @@ -553,33 +566,167 @@ rank-wkn (μ e) i = cong suc (rank-wkn e (suc i)) ------------------------------------------------------------------------ -- Algebraic properties -subst-cong : ∀ (e : Expression (suc n)) e′ i γ → ⟦ e [ e′ / i ] ⟧ γ ≈ˡ ⟦ e ⟧ (insert γ i (⟦ e′ ⟧ γ)) -subst-cong ⊥ e′ i γ = ≈ˡ-refl -subst-cong ε e′ i γ = ≈ˡ-refl -subst-cong (Char c) e′ i γ = ≈ˡ-refl -subst-cong (e₁ ∨ e₂) e′ i γ = ∪-cong (subst-cong e₁ e′ i γ) (subst-cong e₂ e′ i γ) -subst-cong (e₁ ∙ e₂) e′ i γ = ∙ˡ-cong (subst-cong e₁ e′ i γ) (subst-cong e₂ e′ i γ) -subst-cong (Var j) e′ i γ with i ≟ j +subst-monoʳ : + ∀ (e : Expression (suc n)) i {e₁ e₂} → (∀ γ → ⟦ e₁ ⟧ γ ⊆ ⟦ e₂ ⟧ γ) → + ∀ γ → ⟦ e [ e₁ / i ] ⟧ γ ⊆ ⟦ e [ e₂ / i ] ⟧ γ +subst-monoʳ ⊥ i mono γ = ⊆-refl +subst-monoʳ ε i mono γ = ⊆-refl +subst-monoʳ (Char c) i mono γ = ⊆-refl +subst-monoʳ (e₁ ∨ e₂) i mono γ = ∪-mono (subst-monoʳ e₁ i mono γ) (subst-monoʳ e₂ i mono γ) +subst-monoʳ (e₁ ∙ e₂) i mono γ = ∙-mono (subst-monoʳ e₁ i mono γ) (subst-monoʳ e₂ i mono γ) +subst-monoʳ (Var j) i mono γ with i ≟ j +... | yes refl = mono γ +... | no _ = ⊆-refl +subst-monoʳ (μ e) i {e₁} {e₂} mono γ = ⋃-mono (λ {A} {B} A⊆B → begin + ⟦ e [ wkn e₁ zero / suc i ] ⟧ (A ∷ γ) ⊆⟨ ⟦⟧-mono-env (e [ wkn e₁ zero / suc i ]) (A⊆B ∷ Pw.refl ⊆-refl) ⟩ + ⟦ e [ wkn e₁ zero / suc i ] ⟧ (B ∷ γ) ⊆⟨ subst-monoʳ e (suc i) (wkn-mono e₁ e₂ zero mono) (B ∷ γ) ⟩ + ⟦ e [ wkn e₂ zero / suc i ] ⟧ (B ∷ γ) ∎) + where open ⊆-Reasoning + +subst-congⁱ : ∀ (e : Expression (suc n)) e′ {i j} → i ≡ j → e [ e′ / i ] ≈ e [ e′ / j ] +subst-congⁱ e e′ {i} refl = ≈-refl {x = e [ e′ / i ]} + +⟦⟧-subst : ∀ (e : Expression (suc n)) e′ i γ → ⟦ e [ e′ / i ] ⟧ γ ≈ˡ ⟦ e ⟧ (insert γ i (⟦ e′ ⟧ γ)) +⟦⟧-subst ⊥ e′ i γ = ≈ˡ-refl +⟦⟧-subst ε e′ i γ = ≈ˡ-refl +⟦⟧-subst (Char c) e′ i γ = ≈ˡ-refl +⟦⟧-subst (e₁ ∨ e₂) e′ i γ = ∪-cong (⟦⟧-subst e₁ e′ i γ) (⟦⟧-subst e₂ e′ i γ) +⟦⟧-subst (e₁ ∙ e₂) e′ i γ = ∙ˡ-cong (⟦⟧-subst e₁ e′ i γ) (⟦⟧-subst e₂ e′ i γ) +⟦⟧-subst (Var j) e′ i γ with i ≟ j ... | yes refl = ≈ˡ-reflexive (sym (insert-lookup γ i (⟦ e′ ⟧ γ))) -... | no i≢j = ≈ˡ-reflexive (begin +... | no i≢j = begin-equality lookup γ po ≡˘⟨ cong (λ x → lookup x po) (remove-insert γ i (⟦ e′ ⟧ γ)) ⟩ lookup (remove γ′ i) po ≡⟨ remove-punchOut γ′ i≢j ⟩ - lookup γ′ j ∎) + lookup γ′ j ∎ where - open ≡-Reasoning + open ⊆-Reasoning po = punchOut i≢j γ′ = insert γ i (⟦ e′ ⟧ γ) -subst-cong (μ e) e′ i γ = ⋃-cong λ {A} {B} A≈B → begin - ⟦ e [ e′′ / suc i ] ⟧ (A ∷ γ) ≈⟨ ⟦⟧-cong-env (e [ e′′ / suc i ]) (A≈B ∷ PW.refl ≈ˡ-refl) ⟩ - ⟦ e [ e′′ / suc i ] ⟧ (B ∷ γ) ≈⟨ subst-cong e e′′ (suc i) (B ∷ γ) ⟩ - ⟦ e ⟧ (B ∷ insert γ i (⟦ e′′ ⟧ (B ∷ γ))) ≈⟨ ⟦⟧-cong-env e (insert′ (wkn-cong e′ zero γ B) (B ∷ γ) (suc i)) ⟩ +⟦⟧-subst (μ e) e′ i γ = ⋃-cong λ {A} {B} A≈B → begin-equality + ⟦ e [ e′′ / suc i ] ⟧ (A ∷ γ) ≈⟨ ⟦⟧-cong-env (e [ e′′ / suc i ]) (A≈B ∷ Pw.refl ≈ˡ-refl) ⟩ + ⟦ e [ e′′ / suc i ] ⟧ (B ∷ γ) ≈⟨ ⟦⟧-subst e e′′ (suc i) (B ∷ γ) ⟩ + ⟦ e ⟧ (B ∷ insert γ i (⟦ e′′ ⟧ (B ∷ γ))) ≈⟨ ⟦⟧-cong-env e (insert′ (⟦⟧-wkn e′ zero γ B) (B ∷ γ) (suc i)) ⟩ ⟦ e ⟧ (B ∷ insert γ i (⟦ e′ ⟧ γ)) ∎ where - open import Relation.Binary.Reasoning.Setoid setoidˡ + open ⊆-Reasoning e′′ = wkn e′ zero insert′ : ∀ {n} {x y : Language (c ⊔ ℓ)} (x≈y : x ≈ˡ y) xs i → Pointwise _≈ˡ_ {n = suc n} (insert xs i x) (insert xs i y) - insert′ x≈y xs zero = x≈y ∷ PW.refl ≈ˡ-refl + insert′ x≈y xs zero = x≈y ∷ Pw.refl ≈ˡ-refl insert′ x≈y (x ∷ xs) (suc i) = ≈ˡ-refl ∷ insert′ x≈y xs i + +------------------------------------------------------------------------ +-- Other properties + +μ-roll : ∀ (e : Expression (suc n)) → e [ μ e / zero ] ≈ μ e +μ-roll e γ = + ⊆-antisym + (begin + ⟦ e [ μ e / zero ] ⟧ γ ≈⟨ ⟦⟧-subst e (μ e) zero γ ⟩ + ⟦ e ⟧ (⟦ μ e ⟧ γ ∷ γ) ⊆⟨ big-bit ⟩ + ⟦ μ e ⟧ γ ∎) + (begin + ⟦ μ e ⟧ γ ⊆⟨ ⋃-unroll (⟦⟧-mono-env e ∘ (_∷ Pw.refl ⊆-refl)) ⟩ + ⟦ e ⟧ (⟦ μ e ⟧ γ ∷ γ) ≈˘⟨ ⟦⟧-subst e (μ e) zero γ ⟩ + ⟦ e [ μ e / zero ] ⟧ γ ∎) + where + open ⊆-Reasoning + + get-tag : + ∀ {m} e A (K : ℕ → Language _) → + (∀ {w} → w ∈ A → ∃[ n ] w ∈ K n) → (∀ {m n} → m ≤ n → K m ⊆ K n) → + ∀ i γ {w} → w ∈ ⟦ e ⟧ (insert {n = m} γ i A) → ∃[ n ] w ∈ ⟦ e ⟧ (insert γ i (K n)) + get-tag ε A K tag mono i γ w∈⟦e⟧ = 0 , w∈⟦e⟧ + get-tag (Char c) A K tag mono i γ w∈⟦e⟧ = 0 , w∈⟦e⟧ + get-tag (e₁ ∨ e₂) A K tag mono i γ w∈⟦e⟧ = + [ map₂ inj₁ ∘ get-tag e₁ A K tag mono i γ + , map₂ inj₂ ∘ get-tag e₂ A K tag mono i γ + ]′ w∈⟦e⟧ + get-tag (e₁ ∙ e₂) A K tag mono i γ (w₁ , w₂ , w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq) = + ( n₁ + n₂ + , w₁ + , w₂ + , ∈-resp-⊆ + (⟦⟧-mono-env + e₁ + (Pointwise-insert i i {fromWitness refl} (mono (m≤m+n n₁ n₂)) (Pw.refl ⊆-refl))) + w₁∈⟦e₁⟧′ + , ∈-resp-⊆ + (⟦⟧-mono-env + e₂ + (Pointwise-insert i i {fromWitness refl} (mono (m≤n+m n₂ n₁)) (Pw.refl ⊆-refl))) + w₂∈⟦e₂⟧′ + , eq + ) + where + n₁,w₁∈⟦e₁⟧′ = get-tag e₁ A K tag mono i γ w₁∈⟦e₁⟧ + n₂,w₂∈⟦e₂⟧′ = get-tag e₂ A K tag mono i γ w₂∈⟦e₂⟧ + + n₁ = proj₁ n₁,w₁∈⟦e₁⟧′ + n₂ = proj₁ n₂,w₂∈⟦e₂⟧′ + w₁∈⟦e₁⟧′ = proj₂ n₁,w₁∈⟦e₁⟧′ + w₂∈⟦e₂⟧′ = proj₂ n₂,w₂∈⟦e₂⟧′ + get-tag (Var j) A K tag mono i γ {w} w∈⟦e⟧ with i ≟ j + ... | yes refl = + map₂ + (λ {n} → K n |> insert-lookup γ j |> ≈ˡ-reflexive |> ≈ˡ-sym |> ∈-resp-≈) + (tag (∈-resp-≈ (≈ˡ-reflexive (insert-lookup γ j A)) w∈⟦e⟧)) + ... | no i≢j = + 0 , + ∈-resp-≈ + (begin-equality + lookup (insert γ i A) j ≡˘⟨ cong (lookup (insert γ i A)) (punchIn-punchOut i≢j) ⟩ + lookup (insert γ i A) (punchIn i (punchOut i≢j)) ≡⟨ insert-punchIn γ i A (punchOut i≢j) ⟩ + lookup γ (punchOut i≢j) ≡˘⟨ insert-punchIn γ i (K 0) (punchOut i≢j) ⟩ + lookup (insert γ i (K 0)) (punchIn i (punchOut i≢j)) ≡⟨ cong (lookup (insert γ i (K 0))) (punchIn-punchOut i≢j) ⟩ + lookup (insert γ i (K 0)) j ∎) + w∈⟦e⟧ + get-tag (μ e) A K tag mono i γ {w} (n , w∈⟦e⟧) = map₂ (n ,_) (⟦e⟧′-tag n w∈⟦e⟧) + where + ⟦e⟧′ : ℕ → Language _ → Language _ + ⟦e⟧′ n A = Iter (λ X → ⟦ e ⟧ (X ∷ insert γ i A)) ∅ n + + ⟦e⟧′-monoʳ : ∀ n {X Y} → X ⊆ Y → ⟦e⟧′ n X ⊆ ⟦e⟧′ n Y + ⟦e⟧′-monoʳ n X⊆Y = + Iter-monoˡ + (⟦⟧-mono-env e ∘ (_∷ (Pointwise-insert i i {fromWitness refl} X⊆Y (Pw.refl ⊆-refl)))) + n + ⊆-refl + + ⟦e⟧′-tag : ∀ m {w} → w ∈ ⟦e⟧′ m A → ∃[ n ] w ∈ ⟦e⟧′ m (K n) + ⟦e⟧′-tag (suc m) {w} w∈⟦e⟧′ = + n₁ + n₂ , + ∈-resp-⊆ + (⟦⟧-mono-env + e + ( ⟦e⟧′-monoʳ m (mono (m≤m+n n₁ n₂)) + ∷ Pointwise-insert i i {fromWitness refl} (mono (m≤n+m n₂ n₁)) (Pw.refl ⊆-refl)) + ) + w∈⟦e⟧′₂ + where + n₁,w∈⟦e⟧′₁ : ∃[ z ] w ∈ ⟦ e ⟧ (⟦e⟧′ m (K z) ∷ insert γ i A) + n₁,w∈⟦e⟧′₁ = get-tag e (⟦e⟧′ m A) (⟦e⟧′ m ∘ K) (⟦e⟧′-tag m) (⟦e⟧′-monoʳ m ∘ mono) zero (insert γ i A) w∈⟦e⟧′ + + n₁ = proj₁ n₁,w∈⟦e⟧′₁ + w∈⟦e⟧′₁ = proj₂ n₁,w∈⟦e⟧′₁ + + n₂,w∈⟦e⟧′₂ : ∃[ z ] w ∈ ⟦ e ⟧ (⟦e⟧′ m (K n₁) ∷ insert γ i (K z)) + n₂,w∈⟦e⟧′₂ = get-tag e A K tag mono (suc i) (⟦e⟧′ m (K n₁) ∷ γ) w∈⟦e⟧′₁ + + n₂ = proj₁ n₂,w∈⟦e⟧′₂ + w∈⟦e⟧′₂ = proj₂ n₂,w∈⟦e⟧′₂ + + big-bit : ⟦ e ⟧ (⟦ μ e ⟧ γ ∷ γ) ⊆ ⟦ μ e ⟧ γ + big-bit = sub (λ w∈⟦e⟧ → + map suc id + (get-tag + e + (⟦ μ e ⟧ γ) + (Iter (⟦ e ⟧ ∘ (_∷ γ)) ∅) + id + (Iter-monoʳ (⟦⟧-mono-env e ∘ (_∷ Pw.refl ⊆-refl)) (⊆-min (⟦ e ⟧ (∅ ∷ γ)))) + zero + γ + w∈⟦e⟧)) |