From 0dc59b43f78654a746ef5baaeabcc767c64ee0df Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 13 Mar 2021 20:06:22 +0000
Subject: Add weakening proofs for type judgements.

---
 src/Cfe/Expression/Base.agda       | 12 +++++++++++-
 src/Cfe/Expression/Properties.agda | 38 ++++++++++++++++++++++++++++++++++----
 2 files changed, 45 insertions(+), 5 deletions(-)

(limited to 'src/Cfe/Expression')

diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index c4940b6..f4a8dc0 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -15,11 +15,12 @@ open import Cfe.Language.Construct.Concatenate over renaming (_∙_ to _∙ₗ_)
 open import Cfe.Language.Construct.Single over
 open import Cfe.Language.Construct.Union over
 open import Cfe.Language.Indexed.Construct.Iterate over
-open import Data.Fin as F hiding (_≤_)
+open import Data.Fin as F hiding (_≤_; cast)
 open import Data.Nat as ℕ hiding (_≤_; _⊔_)
 open import Data.Product
 open import Data.Vec
 open import Level renaming (suc to lsuc) hiding (Lift)
+open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary
 
 infix 10 _[_/_]
@@ -36,6 +37,15 @@ data Expression : ℕ → Set c where
   Var : ∀ {n} → Fin n → Expression n
   μ : ∀ {n} → Expression (suc n) → Expression n
 
+cast : ∀ {m n} → .(_ : m ≡ n) → Expression m → Expression n
+cast eq ⊥ = ⊥
+cast eq ε = ε
+cast eq (Char x) = Char x
+cast eq (e₁ ∨ e₂) = cast eq e₁ ∨ cast eq e₂
+cast eq (e₁ ∙ e₂) = cast eq e₁ ∙ cast eq e₂
+cast eq (Var i) = Var (F.cast eq i)
+cast eq (μ e) = μ (cast (cong suc eq) e)
+
 wkn : ∀ {n} → Expression n → Fin (suc n) → Expression (suc n)
 wkn ⊥ i = ⊥
 wkn ε i = ε
diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
index e810ce4..1e41f42 100644
--- a/src/Cfe/Expression/Properties.agda
+++ b/src/Cfe/Expression/Properties.agda
@@ -9,12 +9,13 @@ module Cfe.Expression.Properties
 open Setoid over using () renaming (Carrier to C)
 
 open import Algebra
-open import Cfe.Expression.Base over
+open import Cfe.Expression.Base over as E
 open import Cfe.Language over as L
 import Cfe.Language.Construct.Concatenate over as ∙
 import Cfe.Language.Construct.Union over as ∪
 import Cfe.Language.Indexed.Construct.Iterate over as ⋃
 open import Data.Fin as F
+open import Data.Fin.Properties
 open import Data.Nat as ℕ hiding (_⊔_)
 open import Data.Product
 open import Data.Sum
@@ -190,10 +191,39 @@ subst-fun (μ e) e′ i γ = ⋃.⋃-cong λ {x} {y} x≈y → begin
   insert′ x≈y (z≈w ∷ xs≋ys) (suc i) = z≈w ∷ insert′ x≈y xs≋ys i
 
 monotone : ∀ {n} (e : Expression n) → ⟦ e ⟧ Preserves PW.Pointwise L._≤_ ⟶ L._≤_
-monotone ⊥ γ≤γ′ = ≤-refl
-monotone ε γ≤γ′ = ≤-refl
-monotone (Char x) γ≤γ′ = ≤-refl
+monotone ⊥ γ≤γ′ = L.≤-refl
+monotone ε γ≤γ′ = L.≤-refl
+monotone (Char x) γ≤γ′ = L.≤-refl
 monotone (e₁ ∨ e₂) γ≤γ′ = ∪.∪-monotone (monotone e₁ γ≤γ′) (monotone e₂ γ≤γ′)
 monotone (e₁ ∙ e₂) γ≤γ′ = ∙.∙-monotone (monotone e₁ γ≤γ′) (monotone e₂ γ≤γ′)
 monotone (Var i) γ≤γ′ = PW.lookup γ≤γ′ i
 monotone (μ e) γ≤γ′ = ⋃.⋃-monotone (λ x≤y → monotone e (x≤y PW.∷ γ≤γ′))
+
+cast-inverse : ∀ {m n} e → .(m≡n : m ≡ n) → .(n≡m : n ≡ m) → E.cast m≡n (E.cast n≡m e) ≡ e
+cast-inverse ⊥ m≡n n≡m = ≡.refl
+cast-inverse ε m≡n n≡m = ≡.refl
+cast-inverse (Char x) m≡n n≡m = ≡.refl
+cast-inverse (e₁ ∨ e₂) m≡n n≡m = ≡.cong₂ _∨_ (cast-inverse e₁ m≡n n≡m) (cast-inverse e₂ m≡n n≡m)
+cast-inverse (e₁ ∙ e₂) m≡n n≡m = ≡.cong₂ _∙_ (cast-inverse e₁ m≡n n≡m) (cast-inverse e₂ m≡n n≡m)
+cast-inverse (Var x) m≡n n≡m = ≡.cong Var (toℕ-injective (begin
+  toℕ (F.cast m≡n (F.cast n≡m x)) ≡⟨ toℕ-cast m≡n (F.cast n≡m x) ⟩
+  toℕ (F.cast n≡m x)              ≡⟨ toℕ-cast n≡m x ⟩
+  toℕ x                           ∎))
+  where
+  open ≡.≡-Reasoning
+cast-inverse (μ e) m≡n n≡m = ≡.cong μ (cast-inverse e (≡.cong suc m≡n) (≡.cong suc n≡m))
+
+cast-involutive : ∀ {k m n} e → .(k≡m : k ≡ m) → .(m≡n : m ≡ n) → .(k≡n : k ≡ n) → E.cast m≡n (E.cast k≡m e) ≡ E.cast k≡n e
+cast-involutive ⊥ k≡m m≡n k≡n = ≡.refl
+cast-involutive ε k≡m m≡n k≡n = ≡.refl
+cast-involutive (Char x) k≡m m≡n k≡n = ≡.refl
+cast-involutive (e₁ ∨ e₂) k≡m m≡n k≡n = ≡.cong₂ _∨_ (cast-involutive e₁ k≡m m≡n k≡n) (cast-involutive e₂ k≡m m≡n k≡n)
+cast-involutive (e₁ ∙ e₂) k≡m m≡n k≡n = ≡.cong₂ _∙_ (cast-involutive e₁ k≡m m≡n k≡n) (cast-involutive e₂ k≡m m≡n k≡n)
+cast-involutive (Var x) k≡m m≡n k≡n = ≡.cong Var (toℕ-injective (begin
+  toℕ (F.cast m≡n (F.cast k≡m x)) ≡⟨ toℕ-cast m≡n (F.cast k≡m x) ⟩
+  toℕ (F.cast k≡m x)              ≡⟨ toℕ-cast k≡m x ⟩
+  toℕ x                           ≡˘⟨ toℕ-cast k≡n x ⟩
+  toℕ (F.cast k≡n x)              ∎))
+  where
+  open ≡.≡-Reasoning
+cast-involutive (μ e) k≡m m≡n k≡n = ≡.cong μ (cast-involutive e (≡.cong suc k≡m) (≡.cong suc m≡n) (≡.cong suc k≡n))
-- 
cgit v1.2.3