diff options
author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-22 16:43:49 +0000 |
---|---|---|
committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-22 16:43:49 +0000 |
commit | 9e89f36e3fc6210b270d673c30691530015278fb (patch) | |
tree | b99e51012d555043032c632a42bc6d4b3636c718 /src/Cfe/Judgement/Properties.agda | |
parent | 9c72c8ed0c3e10b5dafb41e438285b08f244ba68 (diff) |
Prove transfer.
Diffstat (limited to 'src/Cfe/Judgement/Properties.agda')
-rw-r--r-- | src/Cfe/Judgement/Properties.agda | 98 |
1 files changed, 96 insertions, 2 deletions
diff --git a/src/Cfe/Judgement/Properties.agda b/src/Cfe/Judgement/Properties.agda index 7f357f0..053ab73 100644 --- a/src/Cfe/Judgement/Properties.agda +++ b/src/Cfe/Judgement/Properties.agda @@ -6,15 +6,28 @@ module Cfe.Judgement.Properties {c ℓ} (over : Setoid c ℓ) where -open import Cfe.Context over renaming (wkn₁ to cwkn₁; wkn₂ to cwkn₂; _≋_ to _≋ᶜ_) +open import Cfe.Context over + renaming + ( wkn₁ to cwkn₁ + ; wkn₂ to cwkn₂ + ; rotate to crotate + ; rotate₁ to crotate₁ + ; transfer to ctransfer + ; _≋_ to _≋ᶜ_ + ) open import Cfe.Expression over open import Cfe.Judgement.Base over -open import Data.Fin +open import Data.Empty +open import Data.Fin as F +open import Data.Fin.Properties hiding (≤-refl; ≤-trans; ≤-irrelevant) open import Data.Nat as ℕ open import Data.Nat.Properties open import Data.Product open import Data.Vec +open import Data.Vec.Properties +open import Function open import Relation.Binary.PropositionalEquality +open import Relation.Nullary toℕ-punchIn : ∀ {n} i j → toℕ j ℕ.≤ toℕ (punchIn {n} i j) toℕ-punchIn zero j = n≤1+n (toℕ j) @@ -65,3 +78,84 @@ wkn₂ {Γ,Δ = Γ,Δ} (Var {i = j} j≥m) i τ′ i≤m = wkn₂ (Fix Γ,Δ⊢e∶τ) i τ′ i≤m = Fix (wkn₂ Γ,Δ⊢e∶τ (suc i) τ′ (s≤s i≤m)) wkn₂ {Γ,Δ = Γ,Δ} (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) i τ′ i≤m = Cat (wkn₂ Γ,Δ⊢e₁∶τ₁ i τ′ i≤m) (congᶜ (≋-sym (wkn₂-shift Γ,Δ i i≤m τ′)) (wkn₁ Δ++Γ,∙⊢e₂∶τ₂ i τ′ z≤n)) τ₁⊛τ₂ wkn₂ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) i τ′ i≤m = Vee (wkn₂ Γ,Δ⊢e₁∶τ₁ i τ′ i≤m) (wkn₂ Γ,Δ⊢e₂∶τ₂ i τ′ i≤m) τ₁#τ₂ + +rotate₁ : ∀ {n} {Γ,Δ : Context n} {e τ} → Γ,Δ ⊢ e ∶ τ → ∀ i j i≥m i≤j → crotate₁ Γ,Δ i j i≥m i≤j ⊢ rotate e i j i≤j ∶ τ +rotate₁ Eps i j i≥m i≤j = Eps +rotate₁ (Char c) i j i≥m i≤j = Char c +rotate₁ Bot i j i≥m i≤j = Bot +rotate₁ {suc n} {Γ,Δ = record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ }} (Var {i = k} k≥m) i j i≥m i≤j with i F.≟ k +... | yes refl = congᵗ (τ≡τ′ Γ m≤n i j i≥m i≤j) (Var (≤-trans i≥m i≤j)) + where + τ≡τ′ : ∀ {a A m n} xs m≤n i j i≥m i≤j → lookup {a} {A} (crotate (reduce≥′ {m} {n} m≤n i i≥m) (reduce≥′ m≤n j (≤-trans i≥m i≤j)) (reduce≥′-mono m≤n i j i≥m i≤j) xs) (reduce≥′ m≤n j (≤-trans i≥m i≤j)) ≡ lookup xs (reduce≥′ m≤n i i≥m) + τ≡τ′ {m = zero} (x ∷ xs) m≤n zero j i≥m i≤j = insert-lookup xs j x + τ≡τ′ {m = zero} (x ∷ xs) m≤n (suc i) (suc j) i≥m i≤j = τ≡τ′ xs z≤n i j z≤n (pred-mono i≤j) + τ≡τ′ {m = suc m} {suc n} xs m≤n (suc i) (suc j) (s≤s i≥m) (s≤s i≤j) = τ≡τ′ xs (pred-mono m≤n) i j i≥m i≤j +... | no i≢k = congᵗ (τ≡τ′ Γ m≤n i j k i≢k i≥m i≤j k≥m) (Var (punchIn-punchOut≥m i j k i≢k i≥m i≤j k≥m)) + where + punchIn-punchOut≥m : ∀ {m n} (i j k : Fin (suc n)) (i≢k : i ≢ k) → toℕ i ≥ m → i F.≤ j → toℕ k ≥ m → toℕ (punchIn j (punchOut i≢k)) ≥ m + punchIn-punchOut≥m {zero} _ _ _ _ _ _ _ = z≤n + punchIn-punchOut≥m {suc _} zero _ zero i≢k _ _ _ = ⊥-elim (i≢k refl) + punchIn-punchOut≥m {suc _} zero zero (suc _) _ _ _ k≥m = k≥m + punchIn-punchOut≥m {suc _} {suc _} (suc i) (suc j) (suc k) i≢k (s≤s i≥m) (s≤s i≤j) (s≤s k≥m) = s≤s (punchIn-punchOut≥m i j k (i≢k ∘ cong suc) i≥m i≤j k≥m) + + τ≡τ′ : ∀ {a A m n} xs m≤n i j k i≢k i≥m i≤j k≥m → + lookup {a} {A} + (crotate + (reduce≥′ {m} {suc n} m≤n i i≥m) + (reduce≥′ m≤n j (≤-trans i≥m i≤j)) + (reduce≥′-mono m≤n i j i≥m i≤j) xs) + (reduce≥′ + m≤n + (punchIn j (punchOut i≢k)) + (punchIn-punchOut≥m i j k i≢k i≥m i≤j k≥m)) ≡ + lookup xs (reduce≥′ m≤n k k≥m) + τ≡τ′ {m = zero} _ _ zero _ zero i≢k _ _ _ = ⊥-elim (i≢k refl) + τ≡τ′ {m = zero} (_ ∷ _) _ zero zero (suc _) _ _ _ _ = refl + τ≡τ′ {m = zero} (_ ∷ _ ∷ _) _ zero (suc _) (suc zero) _ _ _ _ = refl + τ≡τ′ {m = zero} (x ∷ _ ∷ xs) _ zero (suc j) (suc (suc k)) _ _ _ _ = τ≡τ′ (x ∷ xs) z≤n zero j (suc k) (λ ()) z≤n z≤n z≤n + τ≡τ′ {m = zero} (_ ∷ _ ∷ _) _ (suc _) (suc _) zero _ _ _ _ = refl + τ≡τ′ {m = zero} (_ ∷ x ∷ xs) _ (suc i) (suc j) (suc k) i≢k _ i≤j _ = τ≡τ′ (x ∷ xs) z≤n i j k (i≢k ∘ cong suc) z≤n (pred-mono i≤j) z≤n + τ≡τ′ {m = suc m} {suc _} xs m≤n (suc i) (suc j) (suc k) i≢k i≥m i≤j k≥m = τ≡τ′ xs (pred-mono m≤n) i j k (i≢k ∘ cong suc) (pred-mono i≥m) (pred-mono i≤j) (pred-mono k≥m) +rotate₁ (Fix Γ,Δ⊢e∶τ) i j i≥m i≤j = Fix (rotate₁ Γ,Δ⊢e∶τ (suc i) (suc j) (s≤s i≥m) (s≤s i≤j)) +rotate₁ {Γ,Δ = Γ,Δ} (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) i j i≥m i≤j = Cat (rotate₁ Γ,Δ⊢e₁∶τ₁ i j i≥m i≤j) (congᶜ (rotate₁-shift Γ,Δ i j i≥m i≤j) (rotate₁ Δ++Γ,∙⊢e₂∶τ₂ i j z≤n i≤j)) τ₁⊛τ₂ +rotate₁ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) i j i≥m i≤j = Vee (rotate₁ Γ,Δ⊢e₁∶τ₁ i j i≥m i≤j) (rotate₁ Γ,Δ⊢e₂∶τ₂ i j i≥m i≤j) τ₁#τ₂ + +transfer : ∀ {n} {Γ,Δ : Context n} {e τ} → Γ,Δ ⊢ e ∶ τ → ∀ i j i<m 1+j≥m → ctransfer Γ,Δ i j i<m 1+j≥m ⊢ rotate e i j (pred-mono (≤-trans i<m 1+j≥m)) ∶ τ +transfer Eps i j i<m 1+j≥m = Eps +transfer (Char c) i j i<m 1+j≥m = Char c +transfer Bot i j i<m 1+j≥m = Bot +transfer {suc n} {Γ,Δ = record { m = suc m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ }} (Var {i = k} k≥m) i j i<m 1+j≥m with suc m ℕ.≟ 0 | i F.≟ k +... | no m≢0 | yes refl = ⊥-elim (<⇒≱ i<m k≥m) +... | no m≢0 | no i≢k = congᵗ (τ≡τ′ Γ (lookup Δ (fromℕ< i<m)) m≢0 m≤n i j k i<m 1+j≥m k≥m i≢k) (Var (punchIn≥m i j k i≢k i<m 1+j≥m k≥m)) + where + punchIn≥m : ∀ {m n} (i j k : Fin (suc n)) (i≢k : i ≢ k) → toℕ i ℕ.< m → .(suc (toℕ j) ≥ m) → toℕ k ≥ m → toℕ (punchIn j (punchOut i≢k)) ≥ ℕ.pred m + punchIn≥m {suc zero} _ _ _ _ _ _ _ = z≤n + punchIn≥m {suc (suc _)} zero _ zero i≢k _ _ _ = ⊥-elim (i≢k refl) + punchIn≥m {suc (suc _)} zero zero (suc _) _ _ _ (s≤s k≥m) = ≤-step k≥m + punchIn≥m {suc (suc _)} {suc _} (suc i) zero (suc k) i≢k (s≤s i<m) 1+j≥m (s≤s k≥m) = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m)) + punchIn≥m {suc (suc _)} zero (suc _) (suc zero) _ _ _ (s≤s k≥m) = k≥m + punchIn≥m {suc (suc _)} zero (suc j) (suc (suc k)) _ _ 1+j≥m (s≤s k≥m) = s≤s (punchIn≥m zero j (suc k) (λ ()) (s≤s z≤n) (pred-mono 1+j≥m) k≥m) + punchIn≥m {suc (suc _)} {suc _} (suc i) (suc j) (suc k) i≢k (s≤s i<m) 1+j≥m (s≤s k≥m) = s≤s (punchIn≥m i j k (i≢k ∘ cong suc) i<m (pred-mono 1+j≥m) k≥m) + + τ≡τ′ : ∀ {a A m n} xs y m≢0 .(m≤n : _) i j k i<m .(1+j≥m : _) k≥m i≢k → + lookup + (insert′ {a} {A} {m} {suc n} xs m≤n m≢0 + (reduce≥′ (pred-mono (≤-step m≤n)) j (pred-mono 1+j≥m)) + y) + (reduce≥′ + (pred-mono (≤-step m≤n)) + (punchIn j (punchOut i≢k)) + (punchIn≥m i j k i≢k i<m 1+j≥m k≥m)) ≡ + lookup xs (reduce≥′ m≤n k k≥m) + τ≡τ′ {m = suc zero} _ _ _ _ zero zero (suc _) _ _ (s≤s z≤n) _ = refl + τ≡τ′ {m = suc zero} _ _ _ _ (suc _) zero (suc _) (s≤s ()) _ _ _ + τ≡τ′ {m = suc zero} (_ ∷ _) _ _ _ zero (suc _) (suc zero) _ _ (s≤s z≤n) _ = refl + τ≡τ′ {m = suc zero} (_ ∷ xs) y _ _ zero (suc j) (suc (suc k)) _ _ (s≤s z≤n) _ = τ≡τ′ xs y (λ ()) (s≤s (z≤n)) zero j (suc k) (s≤s z≤n) (s≤s z≤n) (s≤s z≤n) (λ ()) + τ≡τ′ {m = suc (suc _)} _ _ _ _ _ zero _ _ 1+j≥m _ _ = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m)) + τ≡τ′ {m = suc (suc _)} _ _ _ _ zero _ (suc zero) _ _ (s≤s ()) _ + τ≡τ′ {m = suc (suc _)} {suc (suc _)} xs y _ m≤n zero (suc j) (suc (suc k)) _ 1+j≥m (s≤s k≥m) _ = τ≡τ′ xs y (λ ()) (pred-mono m≤n) zero j (suc k) (s≤s z≤n) (pred-mono 1+j≥m) k≥m (λ ()) + τ≡τ′ {m = suc (suc m)} xs y m≢0 m≤n (suc i) (suc j) (suc zero) (s≤s i<m) 1+j≥m (s≤s k≥m) i≢k = τ≡τ′ xs y (λ ()) (pred-mono m≤n) i j zero i<m (pred-mono 1+j≥m) k≥m (i≢k ∘ cong suc) + τ≡τ′ {m = suc (suc m)} xs y m≢0 m≤n (suc i) (suc j) (suc (suc k)) (s≤s i<m) 1+j≥m (s≤s k≥m) i≢k = τ≡τ′ xs y (λ ()) (pred-mono m≤n) i j (suc k) i<m (pred-mono 1+j≥m) k≥m (i≢k ∘ cong suc) +transfer {Γ,Δ = Γ,Δ} {τ = τ} (Fix Γ,Δ⊢e∶τ) i j i<m 1+j≥m = Fix (congᶜ (transfer-cons Γ,Δ i j i<m 1+j≥m τ) (transfer Γ,Δ⊢e∶τ (suc i) (suc j) (s≤s i<m) (s≤s 1+j≥m))) +transfer {Γ,Δ = Γ,Δ} (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) i j i<m 1+j≥m = Cat (transfer Γ,Δ⊢e₁∶τ₁ i j i<m 1+j≥m) (congᶜ (transfer-shift Γ,Δ i j i<m 1+j≥m) (rotate₁ Δ++Γ,∙⊢e₂∶τ₂ i j z≤n (pred-mono (≤-trans i<m 1+j≥m)))) τ₁⊛τ₂ +transfer (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) i j i<m 1+j≥m = Vee (transfer Γ,Δ⊢e₁∶τ₁ i j i<m 1+j≥m) (transfer Γ,Δ⊢e₂∶τ₂ i j i<m 1+j≥m) τ₁#τ₂ |