diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Cfe/Context/Properties.agda | 46 | ||||
| -rw-r--r-- | src/Cfe/Derivation/Properties.agda | 87 | ||||
| -rw-r--r-- | src/Cfe/Expression/Base.agda | 2 | ||||
| -rw-r--r-- | src/Cfe/Expression/Properties.agda | 267 | ||||
| -rw-r--r-- | src/Cfe/Function/Power.agda | 37 | ||||
| -rw-r--r-- | src/Cfe/Language/Base.agda | 17 | ||||
| -rw-r--r-- | src/Cfe/Language/Properties.agda | 172 | ||||
| -rw-r--r-- | src/Cfe/Type/Properties.agda | 14 | ||||
| -rw-r--r-- | src/Cfe/Vec/Relation/Binary/Pointwise/Inductive.agda | 41 |
9 files changed, 497 insertions, 186 deletions
diff --git a/src/Cfe/Context/Properties.agda b/src/Cfe/Context/Properties.agda index 569b72e..933803c 100644 --- a/src/Cfe/Context/Properties.agda +++ b/src/Cfe/Context/Properties.agda @@ -20,6 +20,7 @@ open import Cfe.Type over using () ; ≤-trans to ≤ᵗ-trans ; ≤-antisym to ≤ᵗ-antisym ) +open import Cfe.Vec.Relation.Binary.Pointwise.Inductive open import Data.Fin hiding (pred; _≟_) renaming (_≤_ to _≤ᶠ_) open import Data.Fin.Properties using (toℕ<n; toℕ-injective; toℕ-inject₁) renaming @@ -47,33 +48,6 @@ private n : ℕ ------------------------------------------------------------------------ --- Properties for Pointwise ------------------------------------------------------------------------- - - pw-antisym : - ∀ {a b ℓ} {A : Set a} {B : Set b} {P : REL A B ℓ} {Q : REL B A ℓ} {R : REL A B ℓ} {m n} → - Antisym P Q R → Antisym (Pointwise P {m} {n}) (Pointwise Q) (Pointwise R) - pw-antisym antisym [] [] = [] - pw-antisym antisym (x ∷ xs) (y ∷ ys) = antisym x y ∷ pw-antisym antisym xs ys - - pw-insert : - ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} {m n} {xs : Vec A m} {ys : Vec B n} → - ∀ i j {i≡j : True (toℕ i ≟ toℕ j)} {x y} → - x ∼ y → Pointwise _∼_ xs ys → Pointwise _∼_ (insert xs i x) (insert ys j y) - pw-insert zero zero x xs = x ∷ xs - pw-insert (suc i) (suc j) {i≡j} x (y ∷ xs) = - y ∷ pw-insert i j {i≡j |> toWitness |> cong pred |> fromWitness} x xs - - pw-remove : - ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} → - ∀ {m n} {xs : Vec A (suc m)} {ys : Vec B (suc n)} → - ∀ i j {i≡j : True (toℕ i ≟ toℕ j)} → - Pointwise _∼_ xs ys → Pointwise _∼_ (remove xs i) (remove ys j) - pw-remove zero zero (_ ∷ xs) = xs - pw-remove (suc i) (suc j) {i≡j} (x ∷ y ∷ xs) = - x ∷ pw-remove i j {i≡j |> toWitness |> cong pred |> fromWitness} (y ∷ xs) - ------------------------------------------------------------------------- -- Properties of _≈_ ------------------------------------------------------------------------ -- Relational Properties @@ -126,7 +100,7 @@ setoid {n} = record { isEquivalence = ≈-isEquivalence {n} } ≤-trans = zip (flip ≤ᶠ-trans) (Pw.trans ≤ᵗ-trans) ≤-antisym : Antisymmetric (_≈_ {n}) _≤_ -≤-antisym = zip (sym ∘₂ ≤ᶠ-antisym) (pw-antisym ≤ᵗ-antisym) +≤-antisym = zip (sym ∘₂ ≤ᶠ-antisym) (antisym ≤ᵗ-antisym) ------------------------------------------------------------------------ -- Structures @@ -162,7 +136,7 @@ wkn₂-mono : τ₁ ≤ᵗ τ₂ → ctx₁ ≤ ctx₂ → wkn₂ {n} ctx₁ i τ₁ ≤ wkn₂ ctx₂ j τ₂ wkn₂-mono i j {i≡j} τ₁≤τ₂ (g₂≤g₁ , Γ,Δ₁≤Γ,Δ₂) = s≤s g₂≤g₁ , - pw-insert + Pointwise-insert (inject!< i) (inject!< j) {i≡j |> toWitness |> inject!<-cong |> fromWitness} τ₁≤τ₂ @@ -205,7 +179,7 @@ wkn₁-mono {_} {_ ⊐ g₁} {_ ⊐ g₂} i j {i≡j} τ₁≤τ₂ (g₂≤g₁ toℕ g₂ ≤⟨ g₂≤g₁ ⟩ toℕ g₁ ≡˘⟨ toℕ-inject₁ g₁ ⟩ toℕ (inject₁ g₁) ∎) , - pw-insert + Pointwise-insert (raise!> i) (raise!> j) {i≡j |> toWitness |> raise!>-cong |> fromWitness} τ₁≤τ₂ @@ -318,7 +292,11 @@ remove₂-mono : ctx₁ ≤ ctx₂ → remove₂ {n} ctx₁ i ≤ remove₂ ctx₂ j remove₂-mono i j {i≡j} (g₂≤g₁ , Γ,Δ₁≤Γ,Δ₂) = predⁱ<-mono j i g₂≤g₁ , - pw-remove (inject!< i) (inject!< j) {i≡j |> toWitness |> inject!<-cong |> fromWitness} Γ,Δ₁≤Γ,Δ₂ + Pointwise-remove + (inject!< i) + (inject!< j) + {i≡j |> toWitness |> inject!<-cong |> fromWitness} + Γ,Δ₁≤Γ,Δ₂ remove₂-cong : ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} → @@ -356,7 +334,11 @@ remove₁-mono : ctx₁ ≤ ctx₂ → remove₁ {n} ctx₁ i ≤ remove₁ ctx₂ j remove₁-mono i j {i≡j} (g₂≤g₁ , Γ,Δ₁≤Γ,Δ₂) = inject₁ⁱ>-mono j i g₂≤g₁ , - pw-remove (raise!> i) (raise!> j) {i≡j |> toWitness |> raise!>-cong |> fromWitness} Γ,Δ₁≤Γ,Δ₂ + Pointwise-remove + (raise!> i) + (raise!> j) + {i≡j |> toWitness |> raise!>-cong |> fromWitness} + Γ,Δ₁≤Γ,Δ₂ remove₁-cong : ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} → diff --git a/src/Cfe/Derivation/Properties.agda b/src/Cfe/Derivation/Properties.agda index d922f2a..99be370 100644 --- a/src/Cfe/Derivation/Properties.agda +++ b/src/Cfe/Derivation/Properties.agda @@ -1,6 +1,6 @@ {-# OPTIONS --without-K --safe #-} -open import Relation.Binary using (Setoid) +open import Relation.Binary using (Rel; Setoid) module Cfe.Derivation.Properties {c ℓ} (over : Setoid c ℓ) @@ -8,30 +8,39 @@ module Cfe.Derivation.Properties open Setoid over using () renaming (Carrier to C) -open import Cfe.Context over using (∙,∙) +open import Cfe.Context over using (_⊐_; Γ,Δ; ∙,∙; remove₁) renaming (wkn₂ to wkn₂ᶜ) open import Cfe.Derivation.Base over open import Cfe.Expression over -open import Cfe.Fin using (zero) +open import Cfe.Fin using (zero; inj; raise!>; cast>) open import Cfe.Judgement over open import Cfe.Language over hiding (_∙_) + renaming (_≈_ to _≈ˡ_; ≈-refl to ≈ˡ-refl; ≈-reflexive to ≈ˡ-reflexive; ≈-sym to ≈ˡ-sym) open import Cfe.Type over using (_⊛_; _⊨_) -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 Cfe.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise-insert) +open import Data.Empty using (⊥-elim) +open import Data.Fin using (Fin; zero; suc; _≟_; punchOut; punchIn) +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 using (ℕ; zero; suc; z≤n; s≤s; _+_) renaming (_≤_ to _≤ⁿ_) +open import Data.Nat.Properties using (n<1+n; m≤m+n; m≤n+m; m≤n⇒m<n∨m≡n; module ≤-Reasoning) +open import Data.Product using (_×_; _,_; -,_; ∃-syntax; map₂; proj₁; proj₂) +open import Data.Sum using (inj₁; inj₂; [_,_]′) +open import Data.Vec using ([]; _∷_; [_]; lookup; insert) +open import Data.Vec.Properties using (insert-lookup; insert-punchIn) +open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pw using ([]; _∷_) +open import Function using (_∘_; _|>_; _on_; flip) open import Induction.WellFounded -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 (¬_) +open import Level using (_⊔_; lift) +open import Relation.Binary.Construct.On using () renaming (wellFounded to on-wellFounded) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong) +open import Relation.Nullary +open import Relation.Nullary.Decidable using (fromWitness) -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⟧ +parse : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {w} → w ∈ ⟦ e ⟧ [] → e ⤇ w +parse {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 (w , e) = ∀ {τ} → ∙,∙ ⊢ e ∶ τ → w ∈ ⟦ e ⟧ [] → e ⤇ w @@ -55,14 +64,14 @@ w∈⟦e⟧⇒e⤇w {e = e} ctx⊢e∶τ {w} w∈⟦e⟧ = All.wfRec <ₗₑₓ- ⟦μe⟧⊆⟦e[μe/0]⟧ : ⟦ μ e ⟧ [] ⊆ ⟦ e [ μ e / zero ] ⟧ [] ⟦μe⟧⊆⟦e[μe/0]⟧ = begin - ⟦ μ e ⟧ [] ≤⟨ ⋃-unroll (⟦⟧-mono-env e ∘ (_∷ [])) ⟩ - ⟦ e ⟧ [ ⟦ μ e ⟧ [] ] ≈˘⟨ subst-cong e (μ e) zero [] ⟩ + ⟦ μ e ⟧ [] ⊆⟨ ⋃-unroll (⟦⟧-mono-env e ∘ (_∷ [])) ⟩ + ⟦ e ⟧ [ ⟦ μ e ⟧ [] ] ≈˘⟨ ⟦⟧-subst e (μ e) zero [] ⟩ ⟦ e [ μ e / zero ] ⟧ [] ∎ where open ⊆-Reasoning go (w , e₁ ∙ e₂) rec (Cat ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁⊛τ₂) (w₁ , w₂ , w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq) = Cat - (rec (w₁ , e₁) (lex-∙ˡ e₁ e₂ [] (-, -, w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq)) ctx⊢e₁∶τ₁ w₁∈⟦e₁⟧) - (rec (w₂ , e₂) (lex-∙ʳ e₁ e₂ [] ε∉⟦e₁⟧ (-, -, w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq)) ctx⊢e₂∶τ₂ w₂∈⟦e₂⟧) + (rec (w₁ , e₁) (lex-∙ˡ e₁ e₂ w₁ eq) ctx⊢e₁∶τ₁ w₁∈⟦e₁⟧) + (rec (w₂ , e₂) (lex-∙ʳ e₁ e₂ [] ε∉⟦e₁⟧ w₁∈⟦e₁⟧ eq) ctx⊢e₂∶τ₂ w₂∈⟦e₂⟧) eq where open _⊛_ τ₁⊛τ₂ using (¬n₁) @@ -72,3 +81,37 @@ w∈⟦e⟧⇒e⤇w {e = e} ctx⊢e∶τ {w} w∈⟦e⟧ = All.wfRec <ₗₑₓ- Veeˡ (rec (w , e₁) (inj₂ (refl , rank-∨ˡ e₁ e₂)) ctx⊢e₁∶τ₁ w∈⟦e₁⟧) go (w , e₁ ∨ e₂) rec (Vee ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁#τ₂) (inj₂ w∈⟦e₂⟧) = Veeʳ (rec (w , e₂) (inj₂ (refl , rank-∨ʳ e₁ e₂)) ctx⊢e₂∶τ₂ w∈⟦e₂⟧) + +generate : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {w} → e ⤇ w → w ∈ ⟦ e ⟧ [] +generate {e = e} ctx⊢e∶τ {w} e⤇w = All.wfRec <ₗₑₓ-wellFounded _ Pred go (w , e) ctx⊢e∶τ e⤇w + where + Pred : (List C × Expression 0) → Set _ + Pred (w , e) = ∀ {τ} → ∙,∙ ⊢ e ∶ τ → e ⤇ w → w ∈ ⟦ e ⟧ [] + + go : ∀ w,e → WfRec _<ₗₑₓ_ Pred w,e → Pred w,e + go (w , ε) rec Eps Eps = lift refl + go (w , Char c) rec (Char c) (Char c∼y) = c∼y ∷ [] + go (w , μ e) rec (Fix ctx⊢e∶τ) (Fix e[μe/0]⤇w) = ∈-resp-≈ (μ-roll e []) w∈⟦e[μe/0]⟧ + where + w,e[μe/0]<ₗₑₓw,μe : (w , e [ μ e / zero ]) <ₗₑₓ (w , μ e) + w,e[μe/0]<ₗₑₓw,μe = inj₂ (refl , (begin-strict + rank (e [ μ e / zero ]) ≡⟨ subst₂-pres-rank ctx⊢e∶τ zero (Fix ctx⊢e∶τ) ⟩ + rank e <⟨ rank-μ e ⟩ + rank (μ e) ∎)) + where open ≤-Reasoning + + w∈⟦e[μe/0]⟧ : w ∈ ⟦ e [ μ e / zero ] ⟧ [] + w∈⟦e[μe/0]⟧ = rec (w , e [ μ e / zero ]) w,e[μe/0]<ₗₑₓw,μe (subst₂ ctx⊢e∶τ zero (Fix ctx⊢e∶τ)) e[μe/0]⤇w + go (w , e₁ ∙ e₂) rec (Cat ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁⊛τ₂) (Cat {w₁ = w₁} {w₂} e₁⤇w₁ e₂⤇w₂ eq) = + w₁ , w₂ , w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq + where + open _⊛_ τ₁⊛τ₂ using (¬n₁) + ε∉⟦e₁⟧ : ¬ Null (⟦ e₁ ⟧ []) + ε∉⟦e₁⟧ = ¬n₁ ∘ _⊨_.n⇒n (soundness ctx⊢e₁∶τ₁ [] []) + + w₁∈⟦e₁⟧ = rec (w₁ , e₁) (lex-∙ˡ e₁ e₂ w₁ eq) ctx⊢e₁∶τ₁ e₁⤇w₁ + w₂∈⟦e₂⟧ = rec (w₂ , e₂) (lex-∙ʳ e₁ e₂ [] ε∉⟦e₁⟧ w₁∈⟦e₁⟧ eq) ctx⊢e₂∶τ₂ e₂⤇w₂ + go (w , e₁ ∨ e₂) rec (Vee ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁#τ₂) (Veeˡ e₁⤇w) = + inj₁ (rec (w , e₁) (inj₂ (refl , rank-∨ˡ e₁ e₂)) ctx⊢e₁∶τ₁ e₁⤇w) + go (w , e₁ ∨ e₂) rec (Vee ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁#τ₂) (Veeʳ e₂⤇w) = + inj₂ (rec (w , e₂) (inj₂ (refl , rank-∨ʳ e₁ e₂)) ctx⊢e₂∶τ₂ e₂⤇w) diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda index f37694b..933b3bb 100644 --- a/src/Cfe/Expression/Base.agda +++ b/src/Cfe/Expression/Base.agda @@ -46,7 +46,7 @@ infix 4 _≈_ ⟦ Char x ⟧ _ = ｛ x ｝ ⟦ e₁ ∨ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∪ ⟦ e₂ ⟧ γ ⟦ e₁ ∙ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∙ˡ ⟦ e₂ ⟧ γ -⟦ Var n ⟧ γ = lookup γ n +⟦ Var j ⟧ γ = lookup γ j ⟦ μ e ⟧ γ = ⋃ (λ X → ⟦ e ⟧ (X ∷ γ)) _≈_ : {n : ℕ} → Expression n → Expression n → Set _ 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⟧)) diff --git a/src/Cfe/Function/Power.agda b/src/Cfe/Function/Power.agda deleted file mode 100644 index da3b335..0000000 --- a/src/Cfe/Function/Power.agda +++ /dev/null @@ -1,37 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -module Cfe.Function.Power where - -open import Data.Nat using (ℕ) -open import Data.Product using (∃-syntax; _×_) -open import Function using (id; _∘_) -open import Level using (Level; _⊔_) -open import Relation.Binary using (Rel; REL) -open import Relation.Binary.PropositionalEquality using (cong; _≡_) - -private - variable - a : Level - A : Set a - -infix 10 _^_ - ------------------------------------------------------------------------- --- Definition - -_^_ : (A → A) → ℕ → A → A -f ^ ℕ.zero = id -f ^ ℕ.suc n = f ∘ f ^ n - ------------------------------------------------------------------------- --- Properties - -f∼g⇒fⁿ∼gⁿ : - ∀ {a b ℓ} {A : Set a} {B : Set b} (_∼_ : REL A B ℓ) {f g 0A 0B} → - 0A ∼ 0B → (∀ {x y} → x ∼ y → f x ∼ g y) → ∀ n → (f ^ n) 0A ∼ (g ^ n) 0B -f∼g⇒fⁿ∼gⁿ _ refl ext ℕ.zero = refl -f∼g⇒fⁿ∼gⁿ ∼ refl ext (ℕ.suc n) = ext (f∼g⇒fⁿ∼gⁿ ∼ refl ext n) - -fⁿf≡fⁿ⁺¹ : ∀ (f : A → A) n → (f ^ n) ∘ f ≡ f ^ (ℕ.suc n) -fⁿf≡fⁿ⁺¹ f ℕ.zero = _≡_.refl -fⁿf≡fⁿ⁺¹ f (ℕ.suc n) = cong (f ∘_) (fⁿf≡fⁿ⁺¹ f n) diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda index d9be456..d73fe19 100644 --- a/src/Cfe/Language/Base.agda +++ b/src/Cfe/Language/Base.agda @@ -8,14 +8,14 @@ module Cfe.Language.Base open Setoid over using () renaming (Carrier to C) -open import Cfe.Function.Power open import Data.Empty.Polymorphic using (⊥) open import Data.List open import Data.List.Relation.Binary.Equality.Setoid over +open import Data.Nat using (ℕ; zero; suc) open import Data.Product open import Data.Sum open import Function -open import Level +open import Level renaming (suc to ℓsuc) open import Relation.Binary.PropositionalEquality using (_≡_) open import Relation.Nullary using (Dec; ¬_) @@ -26,7 +26,7 @@ private ------------------------------------------------------------------------ -- Definition -record Language a : Set (c ⊔ ℓ ⊔ suc a) where +record Language a : Set (c ⊔ ℓ ⊔ ℓsuc a) where field 𝕃 : List C → Set a ∈-resp-≋ : 𝕃 ⟶ 𝕃 Respects _≋_ @@ -82,11 +82,16 @@ A ∪ B = record ; ∈-resp-≋ = uncurry Data.Sum.map ∘ < Language.∈-resp-≋ A , Language.∈-resp-≋ B > } +Iter : (Language a → Language a) → Language a → ℕ → Language _ +Iter F A zero = A +Iter F A (suc n) = F (Iter F A n) + Sup : (Language a → Language a) → Language a → Language _ Sup F A = record - { 𝕃 = λ w → ∃[ n ] w ∈ (F ^ n) A - ; ∈-resp-≋ = λ w≋w′ (n , w∈FⁿA) → n , Language.∈-resp-≋ ((F ^ n) A) w≋w′ w∈FⁿA + { 𝕃 = λ w → ∃[ n ] w ∈ Iter F A n + ; ∈-resp-≋ = λ w≋w′ (n , w∈FⁿA) → n , Iter.∈-resp-≋ F A n w≋w′ w∈FⁿA } + where module Iter F A n = Language (Iter F A n) ⋃_ : (Language a → Language a) → Language _ ⋃ F = Sup F ∅ @@ -96,7 +101,7 @@ Sup F A = record infix 4 _⊆_ _≈_ -data _⊆_ {a b} : REL (Language a) (Language b) (c ⊔ ℓ ⊔ suc (a ⊔ b)) where +data _⊆_ {a b} : REL (Language a) (Language b) (c ⊔ ℓ ⊔ ℓsuc (a ⊔ b)) where sub : ∀ {A : Language a} {B : Language b} → (∀ {w} → w ∈ A → w ∈ B) → A ⊆ B _⊇_ : REL (Language a) (Language b) _ diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda index fe153b1..ca288a8 100644 --- a/src/Cfe/Language/Properties.agda +++ b/src/Cfe/Language/Properties.agda @@ -16,7 +16,6 @@ open Setoid over using () ) open import Algebra -open import Cfe.Function.Power open import Cfe.Language.Base over open import Cfe.List.Compare over open import Data.Empty using (⊥-elim) @@ -25,11 +24,11 @@ open import Data.List as L open import Data.List.Properties open import Data.List.Relation.Binary.Equality.Setoid over import Data.List.Relation.Unary.Any as Any -import Data.Nat as ℕ +open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s) open import Data.Product as P open import Data.Sum as S open import Function hiding (_⟶_) -open import Level +open import Level renaming (suc to ℓsuc) import Relation.Binary.Construct.On as On open import Relation.Binary.PropositionalEquality hiding (setoid; [_]) open import Relation.Nullary hiding (Irrelevant) @@ -82,6 +81,12 @@ First-resp-∼ A c∼c′ (w , cw∈A) = w , ∈-resp-≋ (c∼c′ ∷ ≋-refl ⊆-min : Min (_⊆_ {a} {b}) ∅ ⊆-min _ = sub λ () +⊆-respʳ-≈ : Y ≈ Z → X ⊆ Y → X ⊆ Z +⊆-respʳ-≈ Y≈Z X⊆Y = ⊆-trans X⊆Y (⊆-reflexive Y≈Z) + +⊆-respˡ-≈ : Y ≈ Z → Y ⊆ X → Z ⊆ X +⊆-respˡ-≈ Y≈Z Y⊆X = ⊆-trans (⊇-reflexive Y≈Z) Y⊆X + ------------------------------------------------------------------------ -- Membership properties of _⊆_ @@ -108,6 +113,9 @@ Flast-resp-⊆ (sub A⊆B) = P.map₂ (P.map₂ (P.map A⊆B (P.map₂ A⊆B))) ≈-refl : Reflexive (_≈_ {a}) ≈-refl = ⊆-refl , ⊆-refl +≈-reflexive : _≡_ ⇒ (_≈_ {a}) +≈-reflexive refl = ≈-refl + ≈-sym : Sym (_≈_ {a} {b}) _≈_ ≈-sym = P.swap @@ -158,6 +166,93 @@ setoid {a} = record { isEquivalence = ≈-isEquivalence {a} } ⊆-poset : ∀ {a} → Poset _ _ _ ⊆-poset {a} = record { isPartialOrder = ⊆-isPartialOrder {a} } +-- Shamelessly adapted from Relation.Binary.Reasoning.Base.Double +module ⊆-Reasoning where + infix 4 _IsRelatedTo_ + + data _IsRelatedTo_ (A : Language a) (B : Language b) : Set (c ⊔ ℓ ⊔ ℓsuc (a ⊔ b)) where + nonstrict : (A⊆B : A ⊆ B) → A IsRelatedTo B + equals : (A≈B : A ≈ B) → A IsRelatedTo B + + ------------------------------------------------------------------------ + -- A record that is used to ensure that the final relation proved by the + -- chain of reasoning can be converted into the required relation. + + data IsEquality {A : Language a} {B : Language b} : A IsRelatedTo B → Set (c ⊔ ℓ ⊔ ℓsuc (a ⊔ b)) where + isEquality : ∀ A≈B → IsEquality (equals A≈B) + + IsEquality? : ∀ (A⊆B : A IsRelatedTo B) → Dec (IsEquality A⊆B) + IsEquality? (nonstrict _) = no λ() + IsEquality? (equals A≈B) = yes (isEquality A≈B) + + extractEquality : ∀ {A⊆B : A IsRelatedTo B} → IsEquality A⊆B → A ≈ B + extractEquality (isEquality A≈B) = A≈B + + ------------------------------------------------------------------------ + -- Reasoning combinators + + -- See `Relation.Binary.Reasoning.Base.Partial` for the design decisions + -- behind these combinators. + + infix 1 begin_ begin-equality_ + infixr 2 step-⊆ step-≈ step-≈˘ step-≡ step-≡˘ _≡⟨⟩_ + infix 3 _∎ + + -- Beginnings of various types of proofs + + begin_ : (r : A IsRelatedTo B) → A ⊆ B + begin (nonstrict A⊆B) = A⊆B + begin (equals A≈B) = ⊆-reflexive A≈B + + begin-equality_ : ∀ (r : A IsRelatedTo B) → {s : True (IsEquality? r)} → A ≈ B + begin-equality_ r {s} = extractEquality (toWitness s) + + -- Step with the main relation + + step-⊆ : ∀ (X : Language a) → Y IsRelatedTo Z → X ⊆ Y → X IsRelatedTo Z + step-⊆ X (nonstrict Y⊆Z) X⊆Y = nonstrict (⊆-trans X⊆Y Y⊆Z) + step-⊆ X (equals Y≈Z) X⊆Y = nonstrict (⊆-respʳ-≈ Y≈Z X⊆Y) + + -- Step with the setoid equality + + step-≈ : ∀ (X : Language a) → Y IsRelatedTo Z → X ≈ Y → X IsRelatedTo Z + step-≈ X (nonstrict Y⊆Z) X≈Y = nonstrict (⊆-respˡ-≈ (≈-sym X≈Y) Y⊆Z) + step-≈ X (equals Y≈Z) X≈Y = equals (≈-trans X≈Y Y≈Z) + + -- Flipped step with the setoid equality + + step-≈˘ : ∀ (X : Language a) → Y IsRelatedTo Z → Y ≈ X → X IsRelatedTo Z + step-≈˘ X Y⊆Z Y≈X = step-≈ X Y⊆Z (≈-sym Y≈X) + + -- Step with non-trivial propositional equality + + step-≡ : ∀ (X : Language a) → Y IsRelatedTo Z → X ≡ Y → X IsRelatedTo Z + step-≡ X (nonstrict Y⊆Z) X≡Y = nonstrict (case X≡Y of λ { refl → Y⊆Z }) + step-≡ X (equals Y≈Z) X≡Y = equals (case X≡Y of λ { refl → Y≈Z }) + + -- Flipped step with non-trivial propositional equality + + step-≡˘ : ∀ (X : Language a) → Y IsRelatedTo Z → Y ≡ X → X IsRelatedTo Z + step-≡˘ X Y⊆Z Y≡X = step-≡ X Y⊆Z (sym Y≡X) + + -- Step with trivial propositional equality + + _≡⟨⟩_ : ∀ (X : Language a) → X IsRelatedTo Y → X IsRelatedTo Y + X ≡⟨⟩ X⊆Y = X⊆Y + + -- Termination step + + _∎ : ∀ (X : Language a) → X IsRelatedTo X + X ∎ = equals ≈-refl + + -- Syntax declarations + + syntax step-⊆ X Y⊆Z X⊆Y = X ⊆⟨ X⊆Y ⟩ Y⊆Z + syntax step-≈ X Y⊆Z X≈Y = X ≈⟨ X≈Y ⟩ Y⊆Z + syntax step-≈˘ X Y⊆Z Y≈X = X ≈˘⟨ Y≈X ⟩ Y⊆Z + syntax step-≡ X Y⊆Z X≡Y = X ≡⟨ X≡Y ⟩ Y⊆Z + syntax step-≡˘ X Y⊆Z Y≡X = X ≡˘⟨ Y≡X ⟩ Y⊆Z + ------------------------------------------------------------------------ -- Membership properties of _≈_ @@ -797,26 +892,57 @@ _∪?_ : Decidable A → Decidable B → Decidable (A ∪ B) (A? ∪? B?) w = A? w ⊎-dec B? w ------------------------------------------------------------------------ +-- Properties of Iter +------------------------------------------------------------------------ +-- Membership properties of Iter + +FⁿFA≡Fⁿ⁺¹A : ∀ n → Iter {a} F (F A) n ≡ Iter F A (suc n) +FⁿFA≡Fⁿ⁺¹A zero = refl +FⁿFA≡Fⁿ⁺¹A {F = F} (suc n) = cong F (FⁿFA≡Fⁿ⁺¹A n) + +Iter-monoˡ : (∀ {A B} → A ⊆ B → F A ⊆ G B) → ∀ n → A ⊆ B → Iter F A n ⊆ Iter G B n +Iter-monoˡ mono zero A⊆B = A⊆B +Iter-monoˡ mono (suc n) A⊆B = mono (Iter-monoˡ mono n A⊆B) + +Iter-congˡ : (∀ {A B} → A ≈ B → F A ≈ G B) → ∀ n → A ≈ B → Iter F A n ≈ Iter G B n +Iter-congˡ cong zero A≈B = A≈B +Iter-congˡ cong (suc n) A≈B = cong (Iter-congˡ cong n A≈B) + +Iter-step : (∀ {A B} → A ⊆ B → F A ⊆ F B) → A ⊆ F A → ∀ n → Iter F A n ⊆ Iter F A (suc n) +Iter-step mono A⊆FA zero = A⊆FA +Iter-step mono A⊆FA (suc n) = mono (Iter-step mono A⊆FA n) + +Iter-monoʳ : (∀ {A B} → A ⊆ B → F A ⊆ F B) → A ⊆ F A → ∀ {m n} → m ≤ n → Iter F A m ⊆ Iter F A n +Iter-monoʳ mono A⊆FA {n = zero} z≤n = ⊆-refl +Iter-monoʳ {F = F} {A = A} mono A⊆FA {n = suc n} z≤n = begin + A ⊆⟨ A⊆FA ⟩ + F A ⊆⟨ mono (Iter-monoʳ mono A⊆FA {n = n} z≤n) ⟩ + F (Iter F A n) ∎ + where open ⊆-Reasoning +Iter-monoʳ mono A⊆FA (s≤s m≤n) = mono (Iter-monoʳ mono A⊆FA m≤n) + +------------------------------------------------------------------------ -- Properties of Sup ------------------------------------------------------------------------ -- Membership properties of Sup -FⁿA⊆SupFA : ∀ n → (F ^ n) A ⊆ Sup F A +FⁿA⊆SupFA : ∀ n → Iter F A n ⊆ Sup F A FⁿA⊆SupFA n = sub (n ,_) -FⁿFA⊆SupFA : ∀ n → (F ^ n) (F A) ⊆ Sup F A -FⁿFA⊆SupFA {F = F} {A = A} n = ⊆-trans (sub (go n)) (FⁿA⊆SupFA (ℕ.suc n)) - where - go : ∀ {w} n → w ∈ (F ^ n) (F A) → w ∈ (F ^ (ℕ.suc n)) A - go {w = w} n w∈Fⁿ̂FA = subst (λ x → w ∈ x A) (fⁿf≡fⁿ⁺¹ F n) w∈Fⁿ̂FA +FⁿFA⊆SupFA : ∀ n → Iter F (F A) n ⊆ Sup F A +FⁿFA⊆SupFA {F = F} {A = A} n = begin + Iter F (F A) n ≡⟨ FⁿFA≡Fⁿ⁺¹A n ⟩ + Iter F A (suc n) ⊆⟨ FⁿA⊆SupFA (suc n) ⟩ + Sup F A ∎ + where open ⊆-Reasoning -∀[FⁿA⊆B]⇒SupFA⊆B : (∀ n → (F ^ n) A ⊆ B) → Sup F A ⊆ B +∀[FⁿA⊆B]⇒SupFA⊆B : (∀ n → Iter F A n ⊆ B) → Sup F A ⊆ B ∀[FⁿA⊆B]⇒SupFA⊆B FⁿA⊆B = sub λ (n , w∈FⁿA) → ∈-resp-⊆ (FⁿA⊆B n) w∈FⁿA -∃[B⊆FⁿA]⇒B⊆SupFA : ∀ n → B ⊆ (F ^ n) A → B ⊆ Sup F A +∃[B⊆FⁿA]⇒B⊆SupFA : ∀ n → B ⊆ Iter F A n → B ⊆ Sup F A ∃[B⊆FⁿA]⇒B⊆SupFA n B⊆FⁿA = sub λ w∈B → n , ∈-resp-⊆ B⊆FⁿA w∈B -∀[FⁿA≈GⁿB]⇒SupFA≈SupGB : (∀ n → (F ^ n) A ≈ (G ^ n) B) → Sup F A ≈ Sup G B +∀[FⁿA≈GⁿB]⇒SupFA≈SupGB : (∀ n → Iter F A n ≈ Iter G B n) → Sup F A ≈ Sup G B ∀[FⁿA≈GⁿB]⇒SupFA≈SupGB FⁿA≈GⁿB = ⊆-antisym (sub λ (n , w∈FⁿA) → n , ∈-resp-≈ (FⁿA≈GⁿB n) w∈FⁿA) @@ -826,34 +952,38 @@ FⁿFA⊆SupFA {F = F} {A = A} n = ⊆-trans (sub (go n)) (FⁿA⊆SupFA (ℕ.su ------------------------------------------------------------------------ -- Membership properties of ⋃_ -Fⁿ⊆⋃F : ∀ n → (F ^ n) ∅ ⊆ ⋃ F +Fⁿ⊆⋃F : ∀ n → Iter F ∅ n ⊆ ⋃ F Fⁿ⊆⋃F = FⁿA⊆SupFA -∀[Fⁿ⊆B]⇒⋃F⊆B : (∀ n → (F ^ n) ∅ ⊆ B) → ⋃ F ⊆ B +∀[Fⁿ⊆B]⇒⋃F⊆B : (∀ n → Iter F ∅ n ⊆ B) → ⋃ F ⊆ B ∀[Fⁿ⊆B]⇒⋃F⊆B = ∀[FⁿA⊆B]⇒SupFA⊆B -∃[B⊆Fⁿ]⇒B⊆⋃F : ∀ n → B ⊆ (F ^ n) ∅ → B ⊆ ⋃ F +∃[B⊆Fⁿ]⇒B⊆⋃F : ∀ n → B ⊆ Iter F ∅ n → B ⊆ ⋃ F ∃[B⊆Fⁿ]⇒B⊆⋃F = ∃[B⊆FⁿA]⇒B⊆SupFA -∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G : (∀ n → (F ^ n) ∅ ≈ (G ^ n) ∅) → ⋃ F ≈ ⋃ G +∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G : (∀ n → Iter F ∅ n ≈ Iter G ∅ n) → ⋃ F ≈ ⋃ G ∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G = ∀[FⁿA≈GⁿB]⇒SupFA≈SupGB ------------------------------------------------------------------------ -- Functional properties of ⋃_ ⋃-mono : (∀ {A B} → A ⊆ B → F A ⊆ G B) → ⋃ F ⊆ ⋃ G -⋃-mono mono-ext = ∀[Fⁿ⊆B]⇒⋃F⊆B λ n → ⊆-trans (f∼g⇒fⁿ∼gⁿ _⊆_ (⊆-min ∅) mono-ext n) (Fⁿ⊆⋃F n) +⋃-mono {F = F} {G = G} mono-ext = ∀[Fⁿ⊆B]⇒⋃F⊆B λ n → (begin + Iter F ∅ n ⊆⟨ Iter-monoˡ mono-ext n (⊆-min ∅) ⟩ + Iter G ∅ n ⊆⟨ Fⁿ⊆⋃F n ⟩ + ⋃ G ∎) + where open ⊆-Reasoning ⋃-cong : (∀ {A B} → A ≈ B → F A ≈ G B) → ⋃ F ≈ ⋃ G -⋃-cong ext = ∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G (f∼g⇒fⁿ∼gⁿ _≈_ (⊆-antisym (⊆-min ∅) (⊆-min ∅)) ext) +⋃-cong ext = ∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G λ n → Iter-congˡ ext n (⊆-antisym (⊆-min ∅) (⊆-min ∅)) ⋃-inverseʳ : ∀ (A : Language a) → ⋃ (const A) ≈ A -⋃-inverseʳ _ = ⊆-antisym (sub λ {(ℕ.suc _ , w∈A) → w∈A}) (Fⁿ⊆⋃F 1) +⋃-inverseʳ _ = ⊆-antisym (sub λ {(suc _ , w∈A) → w∈A}) (Fⁿ⊆⋃F 1) ⋃-unroll : (∀ {A B} → A ⊆ B → F A ⊆ F B) → ⋃ F ⊆ F (⋃ F) ⋃-unroll {F = F} mono-ext = ∀[Fⁿ⊆B]⇒⋃F⊆B λ - { ℕ.zero → ⊆-min (F (⋃ F)) - ; (ℕ.suc n) → mono-ext (Fⁿ⊆⋃F n) + { zero → ⊆-min (F (⋃ F)) + ; (suc n) → mono-ext (Fⁿ⊆⋃F n) } ------------------------------------------------------------------------ diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda index 21051c0..4b38c1e 100644 --- a/src/Cfe/Type/Properties.agda +++ b/src/Cfe/Type/Properties.agda @@ -16,7 +16,6 @@ open Setoid over using () ) open import Algebra -open import Cfe.Function.Power open import Cfe.Language over hiding ( _≉_; ≈-refl; ≈-trans; ≈-isPartialEquivalence; ≈-isEquivalence; partialSetoid; setoid @@ -356,19 +355,20 @@ setoid {fℓ} {lℓ} = record { isEquivalence = ≈-isEquivalence {fℓ} {lℓ} ; l⇒l = λ (x , w , (m , xw∈Fᵐ) , w′ , n , xwcw′∈Fⁿ) → Fⁿ⊨τ.l⇒l (m + n) - (-, -, ∈-resp-⊆ (step (m≤m+n m n)) xw∈Fᵐ , -, ∈-resp-⊆ (step (m≤n+m n m)) xwcw′∈Fⁿ) + ( x + , w + , ∈-resp-⊆ (Iter-monoʳ mono (⊆-min (F ∅)) (m≤m+n m n)) xw∈Fᵐ + , w′ + , ∈-resp-⊆ (Iter-monoʳ mono (⊆-min (F ∅)) (m≤n+m n m)) xwcw′∈Fⁿ + ) } where - Fⁿ⊨τ : ∀ n → (F ^ n) ∅ ⊨ τ + Fⁿ⊨τ : ∀ n → Iter F ∅ n ⊨ τ Fⁿ⊨τ zero = ⊨-min τ Fⁿ⊨τ (suc n) = ⊨-step (Fⁿ⊨τ n) module Fⁿ⊨τ n = _⊨_ (Fⁿ⊨τ n) - step : ∀ {m n} → m ≤ⁿ n → (F ^ m) ∅ ⊆ (F ^ n) ∅ - step {n = n} z≤n = ⊆-min ((F ^ n) ∅) - step (s≤s m≤n) = mono (step m≤n) - ------------------------------------------------------------------------ -- Properties of _⊛_ ------------------------------------------------------------------------ diff --git a/src/Cfe/Vec/Relation/Binary/Pointwise/Inductive.agda b/src/Cfe/Vec/Relation/Binary/Pointwise/Inductive.agda new file mode 100644 index 0000000..ba75606 --- /dev/null +++ b/src/Cfe/Vec/Relation/Binary/Pointwise/Inductive.agda @@ -0,0 +1,41 @@ +{-# OPTIONS --without-K --safe #-} + +module Cfe.Vec.Relation.Binary.Pointwise.Inductive where + +open import Data.Fin using (toℕ; zero; suc) +open import Data.Nat using (ℕ; suc; _≟_; pred) +open import Data.Vec using (Vec; insert; remove) +open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_) +open import Function using (_|>_) +open import Level using (Level) +open import Relation.Binary using (REL; Antisym) +open import Relation.Binary.PropositionalEquality using (cong) +open import Relation.Nullary.Decidable using (True; toWitness; fromWitness) + +private + variable + a b ℓ : Level + A : Set a + B : Set b + _∼_ : REL A B ℓ + m n : ℕ + +antisym : + ∀ {P : REL A B ℓ} {Q : REL B A ℓ} {R : REL A B ℓ} → + Antisym P Q R → Antisym (Pointwise P {m} {n}) (Pointwise Q) (Pointwise R) +antisym anti [] [] = [] +antisym anti (x ∷ xs) (y ∷ ys) = anti x y ∷ antisym anti xs ys + +Pointwise-insert : + ∀ {xs : Vec A m} {ys : Vec B n} → ∀ i j {i≡j : True (toℕ i ≟ toℕ j)} {x y} → + x ∼ y → Pointwise _∼_ xs ys → Pointwise _∼_ (insert xs i x) (insert ys j y) +Pointwise-insert zero zero x xs = x ∷ xs +Pointwise-insert (suc i) (suc j) {i≡j} x (y ∷ xs) = + y ∷ Pointwise-insert i j {i≡j |> toWitness |> cong pred |> fromWitness} x xs + +Pointwise-remove : + ∀ {xs : Vec A (suc m)} {ys : Vec B (suc n)} → ∀ i j {i≡j : True (toℕ i ≟ toℕ j)} → + Pointwise _∼_ xs ys → Pointwise _∼_ (remove xs i) (remove ys j) +Pointwise-remove zero zero (_ ∷ xs) = xs +Pointwise-remove (suc i) (suc j) {i≡j} (x ∷ y ∷ xs) = + x ∷ Pointwise-remove i j {i≡j |> toWitness |> cong pred |> fromWitness} (y ∷ xs) |