From 53f421168e9e0ea79dce915bb0fcd25494b7938a Mon Sep 17 00:00:00 2001 From: Nils Anders Danielsson Date: Thu, 28 Sep 2023 01:00:57 +0200 Subject: [PATCH] Add some lemmas related to renamings and substitutions (#1750) --- CHANGELOG.md | 25 +++ .../Data/Fin/Substitution/UntypedLambda.agda | 103 +++++++++++ src/Data/Fin/Substitution.agda | 56 +++--- src/Data/Fin/Substitution/Example.agda | 10 +- src/Data/Fin/Substitution/Lemmas.agda | 170 ++++++++++++------ src/Data/Fin/Substitution/List.agda | 16 +- 6 files changed, 294 insertions(+), 86 deletions(-) create mode 100644 README/Data/Fin/Substitution/UntypedLambda.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index f88667b87b..35a0991cac 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1117,6 +1117,10 @@ Deprecated modules * The module `Data.Nat.Properties.Core` has been deprecated, and its one entry moved to `Data.Nat.Properties` +### Deprecation of `Data.Fin.Substitution.Example` + +* The module `Data.Fin.Substitution.Example` has been deprecated, and moved to `README.Data.Fin.Substitution.UntypedLambda` + ### Deprecation of `Data.Product.Function.Dependent.Setoid.WithK` * This module has been deprecated, as none of its contents actually depended on axiom K. The contents has been moved to `Data.Product.Function.Dependent.Setoid`. @@ -2201,6 +2205,27 @@ Additions to existing modules inject≤-irrelevant : inject≤ i m≤n ≡ inject≤ i m≤n′ ``` +* Changed the fixity of `Data.Fin.Substitution.TermSubst._/Var_`. + ```agda + infix 8 ↦ infixl 8 + ``` + +* Added new lemmas in `Data.Fin.Substitution.Lemmas.TermLemmas`: + ``` + map-var≡ : {ρ₁ : Sub Fin m n} {ρ₂ : Sub T m n} {f : Fin m → Fin n} → + (∀ x → lookup ρ₁ x ≡ f x) → + (∀ x → lookup ρ₂ x ≡ T.var (f x)) → + map T.var ρ₁ ≡ ρ₂ + wk≡wk : map T.var VarSubst.wk ≡ T.wk {n = n} + id≡id : map T.var VarSubst.id ≡ T.id {n = n} + sub≡sub : {x : Fin n} → map T.var (VarSubst.sub x) ≡ T.sub (T.var x) + ↑≡↑ : {ρ : Sub Fin m n} → map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑ + /Var≡/ : {ρ : Sub Fin m n} {t} → t /Var ρ ≡ t T./ map T.var ρ + sub-renaming-commutes : {ρ : Sub T m n} → + t /Var VarSubst.sub x T./ ρ ≡ t T./ ρ T.↑ T./ T.sub (lookup ρ x) + sub-commutes-with-renaming : {ρ : Sub Fin m n} → + t T./ T.sub t′ /Var ρ ≡ t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) + * Added new functions in `Data.Integer.Base`: ``` _^_ : ℤ → ℕ → ℤ diff --git a/README/Data/Fin/Substitution/UntypedLambda.agda b/README/Data/Fin/Substitution/UntypedLambda.agda new file mode 100644 index 0000000000..126959958f --- /dev/null +++ b/README/Data/Fin/Substitution/UntypedLambda.agda @@ -0,0 +1,103 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- An example of how Data.Fin.Substitution can be used: a definition +-- of substitution for the untyped λ-calculus, along with some lemmas +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module README.Data.Fin.Substitution.UntypedLambda where + +open import Data.Fin.Substitution +open import Data.Fin.Substitution.Lemmas +open import Data.Nat.Base hiding (_/_) +open import Data.Fin.Base using (Fin) +open import Data.Vec.Base +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; sym; cong; cong₂; module ≡-Reasoning) +open import Relation.Binary.Construct.Closure.ReflexiveTransitive + using (Star; ε; _◅_) + +open ≡-Reasoning + +private + variable + m n : ℕ + +------------------------------------------------------------------------ +-- A representation of the untyped λ-calculus. Uses de Bruijn indices. + +infixl 9 _·_ + +data Lam (n : ℕ) : Set where + var : (x : Fin n) → Lam n + ƛ : (t : Lam (suc n)) → Lam n + _·_ : (t₁ t₂ : Lam n) → Lam n + +------------------------------------------------------------------------ +-- Code for applying substitutions. + +module LamApp {ℓ} {T : ℕ → Set ℓ} (l : Lift T Lam) where + open Lift l hiding (var) + + -- Applies a substitution to a term. + + infixl 8 _/_ + + _/_ : Lam m → Sub T m n → Lam n + var x / ρ = lift (lookup ρ x) + ƛ t / ρ = ƛ (t / ρ ↑) + t₁ · t₂ / ρ = (t₁ / ρ) · (t₂ / ρ) + + open Application (record { _/_ = _/_ }) using (_/✶_) + + -- Some lemmas about _/_. + + ƛ-/✶-↑✶ : ∀ k {t} (ρs : Subs T m n) → + ƛ t /✶ ρs ↑✶ k ≡ ƛ (t /✶ ρs ↑✶ suc k) + ƛ-/✶-↑✶ k ε = refl + ƛ-/✶-↑✶ k (ρ ◅ ρs) = cong (_/ _) (ƛ-/✶-↑✶ k ρs) + + ·-/✶-↑✶ : ∀ k {t₁ t₂} (ρs : Subs T m n) → + t₁ · t₂ /✶ ρs ↑✶ k ≡ (t₁ /✶ ρs ↑✶ k) · (t₂ /✶ ρs ↑✶ k) + ·-/✶-↑✶ k ε = refl + ·-/✶-↑✶ k (ρ ◅ ρs) = cong (_/ _) (·-/✶-↑✶ k ρs) + +lamSubst : TermSubst Lam +lamSubst = record { var = var; app = LamApp._/_ } + +open TermSubst lamSubst hiding (var) + +------------------------------------------------------------------------ +-- Substitution lemmas. + +lamLemmas : TermLemmas Lam +lamLemmas = record + { termSubst = lamSubst + ; app-var = refl + ; /✶-↑✶ = Lemma./✶-↑✶ + } + where + module Lemma {T₁ T₂} {lift₁ : Lift T₁ Lam} {lift₂ : Lift T₂ Lam} where + + open Lifted lift₁ using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_) + open Lifted lift₂ using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_) + + /✶-↑✶ : (ρs₁ : Subs T₁ m n) (ρs₂ : Subs T₂ m n) → + (∀ k x → var x /✶₁ ρs₁ ↑✶₁ k ≡ var x /✶₂ ρs₂ ↑✶₂ k) → + ∀ k t → t /✶₁ ρs₁ ↑✶₁ k ≡ t /✶₂ ρs₂ ↑✶₂ k + /✶-↑✶ ρs₁ ρs₂ hyp k (var x) = hyp k x + /✶-↑✶ ρs₁ ρs₂ hyp k (ƛ t) = begin + ƛ t /✶₁ ρs₁ ↑✶₁ k ≡⟨ LamApp.ƛ-/✶-↑✶ _ k ρs₁ ⟩ + ƛ (t /✶₁ ρs₁ ↑✶₁ suc k) ≡⟨ cong ƛ (/✶-↑✶ ρs₁ ρs₂ hyp (suc k) t) ⟩ + ƛ (t /✶₂ ρs₂ ↑✶₂ suc k) ≡⟨ sym (LamApp.ƛ-/✶-↑✶ _ k ρs₂) ⟩ + ƛ t /✶₂ ρs₂ ↑✶₂ k ∎ + /✶-↑✶ ρs₁ ρs₂ hyp k (t₁ · t₂) = begin + t₁ · t₂ /✶₁ ρs₁ ↑✶₁ k ≡⟨ LamApp.·-/✶-↑✶ _ k ρs₁ ⟩ + (t₁ /✶₁ ρs₁ ↑✶₁ k) · (t₂ /✶₁ ρs₁ ↑✶₁ k) ≡⟨ cong₂ _·_ (/✶-↑✶ ρs₁ ρs₂ hyp k t₁) + (/✶-↑✶ ρs₁ ρs₂ hyp k t₂) ⟩ + (t₁ /✶₂ ρs₂ ↑✶₂ k) · (t₂ /✶₂ ρs₂ ↑✶₂ k) ≡⟨ sym (LamApp.·-/✶-↑✶ _ k ρs₂) ⟩ + t₁ · t₂ /✶₂ ρs₂ ↑✶₂ k ∎ + +open TermLemmas lamLemmas public hiding (var) diff --git a/src/Data/Fin/Substitution.agda b/src/Data/Fin/Substitution.agda index 18769dde37..84a4484715 100644 --- a/src/Data/Fin/Substitution.agda +++ b/src/Data/Fin/Substitution.agda @@ -4,12 +4,12 @@ -- Substitutions ------------------------------------------------------------------------ --- Uses a variant of Conor McBride's technique from "Type-Preserving --- Renaming and Substitution". +-- Uses a variant of Conor McBride's technique from his paper +-- "Type-Preserving Renaming and Substitution". --- See Data.Fin.Substitution.Example for an example of how this module --- can be used: a definition of substitution for the untyped --- λ-calculus. +-- See README.Data.Fin.Substitution.UntypedLambda for an example +-- of how this module can be used: a definition of substitution for +-- the untyped λ-calculus. {-# OPTIONS --cubical-compatible --safe #-} @@ -24,23 +24,29 @@ open import Relation.Binary.Construct.Closure.ReflexiveTransitive open import Level using (Level; _⊔_; 0ℓ) open import Relation.Unary using (Pred) +private + variable + ℓ ℓ₁ ℓ₂ : Level + k m n o : ℕ + + ------------------------------------------------------------------------ -- General functionality -- A Sub T m n is a substitution which, when applied to something with -- at most m variables, yields something with at most n variables. -Sub : ∀ {ℓ} → Pred ℕ ℓ → ℕ → ℕ → Set ℓ +Sub : Pred ℕ ℓ → ℕ → ℕ → Set ℓ Sub T m n = Vec (T n) m -- A /reversed/ sequence of matching substitutions. -Subs : ∀ {ℓ} → Pred ℕ ℓ → ℕ → ℕ → Set ℓ +Subs : Pred ℕ ℓ → ℕ → ℕ → Set ℓ Subs T = flip (Star (flip (Sub T))) -- Some simple substitutions. -record Simple {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where +record Simple (T : Pred ℕ ℓ) : Set ℓ where infix 10 _↑ infixl 10 _↑⋆_ _↑✶_ @@ -50,40 +56,39 @@ record Simple {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where -- Lifting. - _↑ : ∀ {m n} → Sub T m n → Sub T (suc m) (suc n) + _↑ : Sub T m n → Sub T (suc m) (suc n) ρ ↑ = var zero ∷ map weaken ρ - _↑⋆_ : ∀ {m n} → Sub T m n → ∀ k → Sub T (k + m) (k + n) + _↑⋆_ : Sub T m n → ∀ k → Sub T (k + m) (k + n) ρ ↑⋆ zero = ρ ρ ↑⋆ suc k = (ρ ↑⋆ k) ↑ - _↑✶_ : ∀ {m n} → Subs T m n → ∀ k → Subs T (k + m) (k + n) + _↑✶_ : Subs T m n → ∀ k → Subs T (k + m) (k + n) ρs ↑✶ k = Star.gmap (_+_ k) (λ ρ → ρ ↑⋆ k) ρs -- The identity substitution. - id : ∀ {n} → Sub T n n + id : Sub T n n id {zero} = [] id {suc n} = id ↑ -- Weakening. - wk⋆ : ∀ k {n} → Sub T n (k + n) + wk⋆ : ∀ k → Sub T n (k + n) wk⋆ zero = id wk⋆ (suc k) = map weaken (wk⋆ k) - wk : ∀ {n} → Sub T n (suc n) + wk : Sub T n (suc n) wk = wk⋆ 1 -- A substitution which only replaces the first variable. - sub : ∀ {n} → T n → Sub T (suc n) n + sub : T n → Sub T (suc n) n sub t = t ∷ id -- Application of substitutions. -record Application {ℓ₁ ℓ₂ : Level} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : - Set (ℓ₁ ⊔ ℓ₂) where +record Application (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where infixl 8 _/_ _/✶_ infixl 9 _⊙_ @@ -93,17 +98,17 @@ record Application {ℓ₁ ℓ₂ : Level} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred -- Reverse composition. (Fits well with post-application.) - _⊙_ : ∀ {m n k} → Sub T₁ m n → Sub T₂ n k → Sub T₁ m k - ρ₁ ⊙ ρ₂ = map (λ t → t / ρ₂) ρ₁ + _⊙_ : Sub T₁ m n → Sub T₂ n o → Sub T₁ m o + ρ₁ ⊙ ρ₂ = map (_/ ρ₂) ρ₁ -- Application of multiple substitutions. - _/✶_ : ∀ {m n} → T₁ m → Subs T₂ m n → T₁ n + _/✶_ : T₁ m → Subs T₂ m n → T₁ n _/✶_ = Star.gfold Fun.id _ (flip _/_) {k = zero} -- A combination of the two records above. -record Subst {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where +record Subst (T : Pred ℕ ℓ) : Set ℓ where field simple : Simple T application : Application T T @@ -113,7 +118,7 @@ record Subst {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where -- Composition of multiple substitutions. - ⨀ : ∀ {m n} → Subs T m n → Sub T m n + ⨀ : Subs T m n → Sub T m n ⨀ ε = id ⨀ (ρ ◅ ε) = ρ -- Convenient optimisation; simplifies some proofs. ⨀ (ρ ◅ ρs) = ⨀ ρs ⊙ ρ @@ -123,8 +128,7 @@ record Subst {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where -- Liftings from T₁ to T₂. -record Lift {ℓ₁ ℓ₂ : Level} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : - Set (ℓ₁ ⊔ ℓ₂) where +record Lift (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where field simple : Simple T₁ lift : ∀ {n} → T₁ n → T₂ n @@ -160,9 +164,9 @@ record TermSubst (T : Pred ℕ 0ℓ) : Set₁ where varLift : Lift Fin T varLift = record { simple = VarSubst.simple; lift = var } - infix 8 _/Var_ + infixl 8 _/Var_ - _/Var_ : ∀ {m n} → T m → Sub Fin m n → T n + _/Var_ : T m → Sub Fin m n → T n _/Var_ = app varLift simple : Simple T diff --git a/src/Data/Fin/Substitution/Example.agda b/src/Data/Fin/Substitution/Example.agda index 8b3c903a7c..02c98c539f 100644 --- a/src/Data/Fin/Substitution/Example.agda +++ b/src/Data/Fin/Substitution/Example.agda @@ -1,14 +1,20 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- An example of how Data.Fin.Substitution can be used: a definition --- of substitution for the untyped λ-calculus, along with some lemmas +-- This module is DEPRECATED. Please see +-- `README.Data.Nat.Fin.Substitution.UntypedLambda` instead. +-- ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Fin.Substitution.Example where +{-# WARNING_ON_IMPORT +"Data.Fin.Substitution.Example was deprecated in v2.0. +Please see README.Data.Nat.Fin.Substitution.UntypedLambda instead." +#-} + open import Data.Fin.Substitution open import Data.Fin.Substitution.Lemmas open import Data.Nat.Base hiding (_/_) diff --git a/src/Data/Fin/Substitution/Lemmas.agda b/src/Data/Fin/Substitution/Lemmas.agda index 6109f28726..ffa26e64fb 100644 --- a/src/Data/Fin/Substitution/Lemmas.agda +++ b/src/Data/Fin/Substitution/Lemmas.agda @@ -8,7 +8,6 @@ module Data.Fin.Substitution.Lemmas where -import Effect.Applicative.Indexed as Applicative open import Data.Fin.Substitution open import Data.Nat hiding (_⊔_; _/_) open import Data.Fin.Base using (Fin; zero; suc; lift) @@ -23,25 +22,32 @@ open PropEq.≡-Reasoning open import Level using (Level; _⊔_) open import Relation.Unary using (Pred) +private + variable + ℓ ℓ₁ ℓ₂ : Level + m n o p : ℕ + +------------------------------------------------------------------------ -- A lemma which does not refer to any substitutions. -lift-commutes : ∀ {n} k j (x : Fin (j + (k + n))) → +lift-commutes : ∀ k j (x : Fin (j + (k + n))) → lift j suc (lift j (lift k suc) x) ≡ lift j (lift (suc k) suc) (lift j suc x) lift-commutes k zero x = refl lift-commutes k (suc j) zero = refl lift-commutes k (suc j) (suc x) = cong suc (lift-commutes k j x) +------------------------------------------------------------------------ -- The modules below prove a number of substitution lemmas, on the -- assumption that the underlying substitution machinery satisfies -- certain properties. -record Lemmas₀ {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where +record Lemmas₀ (T : Pred ℕ ℓ) : Set ℓ where field simple : Simple T open Simple simple - extensionality : ∀ {m n} {ρ₁ ρ₂ : Sub T m n} → + extensionality : {ρ₁ ρ₂ : Sub T m n} → (∀ x → lookup ρ₁ x ≡ lookup ρ₂ x) → ρ₁ ≡ ρ₂ extensionality {ρ₁ = []} {[]} hyp = refl extensionality {ρ₁ = t₁ ∷ ρ₁} { t₂ ∷ ρ₂} hyp with hyp zero @@ -54,7 +60,7 @@ record Lemmas₀ {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where (id ↑⋆ k) ↑ ≡⟨ cong _↑ (id-↑⋆ k) ⟩ id ↑ ∎ - lookup-map-weaken-↑⋆ : ∀ {m n} k x {ρ : Sub T m n} → + lookup-map-weaken-↑⋆ : ∀ k x {ρ : Sub T m n} → lookup (map weaken ρ ↑⋆ k) x ≡ lookup ((ρ ↑) ↑⋆ k) (lift k suc x) lookup-map-weaken-↑⋆ zero x = refl @@ -65,7 +71,7 @@ record Lemmas₀ {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where weaken (lookup ((ρ ↑) ↑⋆ k) (lift k suc x)) ≡⟨ sym $ VecProp.lookup-map (lift k suc x) weaken ((ρ ↑) ↑⋆ k) ⟩ lookup (map weaken ((ρ ↑) ↑⋆ k)) (lift k suc x) ∎ -record Lemmas₁ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where +record Lemmas₁ (T : Pred ℕ ℓ) : Set ℓ where field lemmas₀ : Lemmas₀ T open Lemmas₀ lemmas₀ @@ -73,7 +79,7 @@ record Lemmas₁ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where field weaken-var : ∀ {n} {x : Fin n} → weaken (var x) ≡ var (suc x) - lookup-map-weaken : ∀ {m n} x {y} {ρ : Sub T m n} → + lookup-map-weaken : ∀ x {y} {ρ : Sub T m n} → lookup ρ x ≡ var y → lookup (map weaken ρ) x ≡ var (suc y) lookup-map-weaken x {y} {ρ} hyp = begin @@ -84,14 +90,14 @@ record Lemmas₁ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where mutual - lookup-id : ∀ {n} (x : Fin n) → lookup id x ≡ var x + lookup-id : (x : Fin n) → lookup id x ≡ var x lookup-id zero = refl lookup-id (suc x) = lookup-wk x - lookup-wk : ∀ {n} (x : Fin n) → lookup wk x ≡ var (suc x) + lookup-wk : (x : Fin n) → lookup wk x ≡ var (suc x) lookup-wk x = lookup-map-weaken x {ρ = id} (lookup-id x) - lookup-↑⋆ : ∀ {m n} (f : Fin m → Fin n) {ρ : Sub T m n} → + lookup-↑⋆ : (f : Fin m → Fin n) {ρ : Sub T m n} → (∀ x → lookup ρ x ≡ var (f x)) → ∀ k x → lookup (ρ ↑⋆ k) x ≡ var (lift k f x) lookup-↑⋆ f hyp zero x = hyp x @@ -99,7 +105,7 @@ record Lemmas₁ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where lookup-↑⋆ f {ρ = ρ} hyp (suc k) (suc x) = lookup-map-weaken x {ρ = ρ ↑⋆ k} (lookup-↑⋆ f hyp k x) - lookup-lift-↑⋆ : ∀ {m n} (f : Fin n → Fin m) {ρ : Sub T m n} → + lookup-lift-↑⋆ : (f : Fin n → Fin m) {ρ : Sub T m n} → (∀ x → lookup ρ (f x) ≡ var x) → ∀ k x → lookup (ρ ↑⋆ k) (lift k f x) ≡ var x lookup-lift-↑⋆ f hyp zero x = hyp x @@ -107,22 +113,22 @@ record Lemmas₁ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where lookup-lift-↑⋆ f {ρ = ρ} hyp (suc k) (suc x) = lookup-map-weaken (lift k f x) {ρ = ρ ↑⋆ k} (lookup-lift-↑⋆ f hyp k x) - lookup-wk-↑⋆ : ∀ {n} k (x : Fin (k + n)) → + lookup-wk-↑⋆ : ∀ k (x : Fin (k + n)) → lookup (wk ↑⋆ k) x ≡ var (lift k suc x) lookup-wk-↑⋆ = lookup-↑⋆ suc lookup-wk - lookup-wk-↑⋆-↑⋆ : ∀ {n} k j (x : Fin (j + (k + n))) → + lookup-wk-↑⋆-↑⋆ : ∀ k j (x : Fin (j + (k + n))) → lookup (wk ↑⋆ k ↑⋆ j) x ≡ var (lift j (lift k suc) x) lookup-wk-↑⋆-↑⋆ k = lookup-↑⋆ (lift k suc) (lookup-wk-↑⋆ k) - lookup-sub-↑⋆ : ∀ {n t} k (x : Fin (k + n)) → + lookup-sub-↑⋆ : ∀ {t} k (x : Fin (k + n)) → lookup (sub t ↑⋆ k) (lift k suc x) ≡ var x lookup-sub-↑⋆ = lookup-lift-↑⋆ suc lookup-id open Lemmas₀ lemmas₀ public -record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where +record Lemmas₂ (T : Pred ℕ ℓ) : Set ℓ where field lemmas₁ : Lemmas₁ T application : Application T T @@ -136,18 +142,18 @@ record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where field var-/ : ∀ {m n x} {ρ : Sub T m n} → var x / ρ ≡ lookup ρ x - suc-/-sub : ∀ {n x} {t : T n} → var (suc x) / sub t ≡ var x + suc-/-sub : ∀ {x} {t : T n} → var (suc x) / sub t ≡ var x suc-/-sub {x = x} {t} = begin var (suc x) / sub t ≡⟨ var-/ ⟩ lookup (sub t) (suc x) ≡⟨ refl ⟩ lookup id x ≡⟨ lookup-id x ⟩ var x ∎ - lookup-⊙ : ∀ {m n k} x {ρ₁ : Sub T m n} {ρ₂ : Sub T n k} → + lookup-⊙ : ∀ x {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} → lookup (ρ₁ ⊙ ρ₂) x ≡ lookup ρ₁ x / ρ₂ lookup-⊙ x {ρ₁} {ρ₂} = VecProp.lookup-map x (λ t → t / ρ₂) ρ₁ - lookup-⨀ : ∀ {m n} x (ρs : Subs T m n) → + lookup-⨀ : ∀ x (ρs : Subs T m n) → lookup (⨀ ρs) x ≡ var x /✶ ρs lookup-⨀ x ε = lookup-id x lookup-⨀ x (ρ ◅ ε) = sym var-/ @@ -158,14 +164,14 @@ record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where var x /✶ ρs / ρ ∎ where ρs = ρ′ ◅ ρs′ - id-⊙ : ∀ {m n} {ρ : Sub T m n} → id ⊙ ρ ≡ ρ + id-⊙ : {ρ : Sub T m n} → id ⊙ ρ ≡ ρ id-⊙ {ρ = ρ} = extensionality λ x → begin lookup (id ⊙ ρ) x ≡⟨ lookup-⊙ x {ρ₁ = id} ⟩ lookup id x / ρ ≡⟨ cong₂ _/_ (lookup-id x) refl ⟩ var x / ρ ≡⟨ var-/ ⟩ lookup ρ x ∎ - lookup-wk-↑⋆-⊙ : ∀ {m n} k {x} {ρ : Sub T (k + suc m) n} → + lookup-wk-↑⋆-⊙ : ∀ k {x} {ρ : Sub T (k + suc m) n} → lookup (wk ↑⋆ k ⊙ ρ) x ≡ lookup ρ (lift k suc x) lookup-wk-↑⋆-⊙ k {x} {ρ} = begin lookup (wk ↑⋆ k ⊙ ρ) x ≡⟨ lookup-⊙ x {ρ₁ = wk ↑⋆ k} ⟩ @@ -173,14 +179,14 @@ record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where var (lift k suc x) / ρ ≡⟨ var-/ ⟩ lookup ρ (lift k suc x) ∎ - wk-⊙-sub′ : ∀ {n} {t : T n} k → wk ↑⋆ k ⊙ sub t ↑⋆ k ≡ id + wk-⊙-sub′ : ∀ {t : T n} k → wk ↑⋆ k ⊙ sub t ↑⋆ k ≡ id wk-⊙-sub′ {t = t} k = extensionality λ x → begin lookup (wk ↑⋆ k ⊙ sub t ↑⋆ k) x ≡⟨ lookup-wk-↑⋆-⊙ k ⟩ lookup (sub t ↑⋆ k) (lift k suc x) ≡⟨ lookup-sub-↑⋆ k x ⟩ var x ≡⟨ sym (lookup-id x) ⟩ lookup id x ∎ - wk-⊙-sub : ∀ {n} {t : T n} → wk ⊙ sub t ≡ id + wk-⊙-sub : {t : T n} → wk ⊙ sub t ≡ id wk-⊙-sub = wk-⊙-sub′ zero var-/-wk-↑⋆ : ∀ {n} k (x : Fin (k + n)) → @@ -190,7 +196,7 @@ record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where lookup (wk ↑⋆ k) x ≡⟨ lookup-wk-↑⋆ k x ⟩ var (lift k suc x) ∎ - wk-↑⋆-⊙-wk : ∀ {n} k j → + wk-↑⋆-⊙-wk : ∀ k j → wk {n} ↑⋆ k ↑⋆ j ⊙ wk ↑⋆ j ≡ wk ↑⋆ j ⊙ wk ↑⋆ suc k ↑⋆ j wk-↑⋆-⊙-wk k j = extensionality λ x → begin @@ -207,7 +213,7 @@ record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where open Subst subst public hiding (simple; application) open Lemmas₁ lemmas₁ public -record Lemmas₃ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where +record Lemmas₃ (T : Pred ℕ ℓ) : Set ℓ where field lemmas₂ : Lemmas₂ T open Lemmas₂ lemmas₂ @@ -217,7 +223,7 @@ record Lemmas₃ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where (∀ k x → var x /✶ ρs₁ ↑✶ k ≡ var x /✶ ρs₂ ↑✶ k) → ∀ k t → t /✶ ρs₁ ↑✶ k ≡ t /✶ ρs₂ ↑✶ k - /✶-↑✶′ : ∀ {m n} (ρs₁ ρs₂ : Subs T m n) → + /✶-↑✶′ : (ρs₁ ρs₂ : Subs T m n) → (∀ k → ⨀ (ρs₁ ↑✶ k) ≡ ⨀ (ρs₂ ↑✶ k)) → ∀ k t → t /✶ ρs₁ ↑✶ k ≡ t /✶ ρs₂ ↑✶ k /✶-↑✶′ ρs₁ ρs₂ hyp = /✶-↑✶ ρs₁ ρs₂ (λ k x → begin @@ -226,10 +232,10 @@ record Lemmas₃ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where lookup (⨀ (ρs₂ ↑✶ k)) x ≡⟨ lookup-⨀ x (ρs₂ ↑✶ k) ⟩ var x /✶ ρs₂ ↑✶ k ∎) - id-vanishes : ∀ {n} (t : T n) → t / id ≡ t + id-vanishes : (t : T n) → t / id ≡ t id-vanishes = /✶-↑✶′ (ε ▻ id) ε id-↑⋆ zero - ⊙-id : ∀ {m n} {ρ : Sub T m n} → ρ ⊙ id ≡ ρ + ⊙-id : {ρ : Sub T m n} → ρ ⊙ id ≡ ρ ⊙-id {ρ = ρ} = begin map (λ t → t / id) ρ ≡⟨ VecProp.map-cong id-vanishes ρ ⟩ map Fun.id ρ ≡⟨ VecProp.map-id ρ ⟩ @@ -237,7 +243,7 @@ record Lemmas₃ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where open Lemmas₂ lemmas₂ public hiding (wk-⊙-sub′) -record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where +record Lemmas₄ (T : Pred ℕ ℓ) : Set ℓ where field lemmas₃ : Lemmas₃ T open Lemmas₃ lemmas₃ @@ -246,7 +252,7 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where private - ↑-distrib′ : ∀ {m n k} {ρ₁ : Sub T m n} {ρ₂ : Sub T n k} → + ↑-distrib′ : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} → (∀ t → t / ρ₂ / wk ≡ t / wk / ρ₂ ↑) → (ρ₁ ⊙ ρ₂) ↑ ≡ ρ₁ ↑ ⊙ ρ₂ ↑ ↑-distrib′ {ρ₁ = ρ₁} {ρ₂} hyp = begin @@ -265,7 +271,7 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where map (λ t → weaken t / ρ₂ ↑) ρ₁ ≡⟨ VecProp.map-∘ _ _ _ ⟩ map (λ t → t / ρ₂ ↑) (map weaken ρ₁) ∎ - ↑⋆-distrib′ : ∀ {m n o} {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} → + ↑⋆-distrib′ : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} → (∀ k t → t / ρ₂ ↑⋆ k / wk ≡ t / wk / ρ₂ ↑⋆ suc k) → ∀ k → (ρ₁ ⊙ ρ₂) ↑⋆ k ≡ ρ₁ ↑⋆ k ⊙ ρ₂ ↑⋆ k ↑⋆-distrib′ hyp zero = refl @@ -274,7 +280,7 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where (ρ₁ ↑⋆ k ⊙ ρ₂ ↑⋆ k) ↑ ≡⟨ ↑-distrib′ (hyp k) ⟩ ρ₁ ↑⋆ suc k ⊙ ρ₂ ↑⋆ suc k ∎ - map-weaken : ∀ {m n} {ρ : Sub T m n} → map weaken ρ ≡ ρ ⊙ wk + map-weaken : {ρ : Sub T m n} → map weaken ρ ≡ ρ ⊙ wk map-weaken {ρ = ρ} = begin map weaken ρ ≡⟨ VecProp.map-cong (λ _ → sym /-wk) ρ ⟩ map (λ t → t / wk) ρ ≡⟨ refl ⟩ @@ -282,7 +288,7 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where private - ⊙-wk′ : ∀ {m n} {ρ : Sub T m n} k → + ⊙-wk′ : ∀ {ρ : Sub T m n} k → ρ ↑⋆ k ⊙ wk ↑⋆ k ≡ wk ↑⋆ k ⊙ ρ ↑ ↑⋆ k ⊙-wk′ {ρ = ρ} k = sym (begin wk ↑⋆ k ⊙ ρ ↑ ↑⋆ k ≡⟨ lemma ⟩ @@ -297,31 +303,30 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where lookup (ρ ↑ ↑⋆ k) (lift k suc x) ≡⟨ sym (lookup-map-weaken-↑⋆ k x) ⟩ lookup (map weaken ρ ↑⋆ k) x ∎ - ⊙-wk : ∀ {m n} {ρ : Sub T m n} → ρ ⊙ wk ≡ wk ⊙ ρ ↑ + ⊙-wk : {ρ : Sub T m n} → ρ ⊙ wk ≡ wk ⊙ ρ ↑ ⊙-wk = ⊙-wk′ zero - wk-commutes : ∀ {m n} {ρ : Sub T m n} t → + wk-commutes : ∀ {ρ : Sub T m n} t → t / ρ / wk ≡ t / wk / ρ ↑ wk-commutes {ρ = ρ} = /✶-↑✶′ (ε ▻ ρ ▻ wk) (ε ▻ wk ▻ ρ ↑) ⊙-wk′ zero - ↑⋆-distrib : ∀ {m n o} {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} → + ↑⋆-distrib : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} → ∀ k → (ρ₁ ⊙ ρ₂) ↑⋆ k ≡ ρ₁ ↑⋆ k ⊙ ρ₂ ↑⋆ k ↑⋆-distrib = ↑⋆-distrib′ (λ _ → wk-commutes) - /-⊙ : ∀ {m n k} {ρ₁ : Sub T m n} {ρ₂ : Sub T n k} t → + /-⊙ : ∀ {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} t → t / ρ₁ ⊙ ρ₂ ≡ t / ρ₁ / ρ₂ /-⊙ {ρ₁ = ρ₁} {ρ₂} t = /✶-↑✶′ (ε ▻ ρ₁ ⊙ ρ₂) (ε ▻ ρ₁ ▻ ρ₂) ↑⋆-distrib zero t - ⊙-assoc : ∀ {m n k o} - {ρ₁ : Sub T m n} {ρ₂ : Sub T n k} {ρ₃ : Sub T k o} → + ⊙-assoc : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} {ρ₃ : Sub T o p} → ρ₁ ⊙ (ρ₂ ⊙ ρ₃) ≡ (ρ₁ ⊙ ρ₂) ⊙ ρ₃ ⊙-assoc {ρ₁ = ρ₁} {ρ₂} {ρ₃} = begin map (λ t → t / ρ₂ ⊙ ρ₃) ρ₁ ≡⟨ VecProp.map-cong /-⊙ ρ₁ ⟩ map (λ t → t / ρ₂ / ρ₃) ρ₁ ≡⟨ VecProp.map-∘ _ _ _ ⟩ map (λ t → t / ρ₃) (map (λ t → t / ρ₂) ρ₁) ∎ - map-weaken-⊙-sub : ∀ {m n} {ρ : Sub T m n} {t} → map weaken ρ ⊙ sub t ≡ ρ + map-weaken-⊙-sub : ∀ {ρ : Sub T m n} {t} → map weaken ρ ⊙ sub t ≡ ρ map-weaken-⊙-sub {ρ = ρ} {t} = begin map weaken ρ ⊙ sub t ≡⟨ cong₂ _⊙_ map-weaken refl ⟩ ρ ⊙ wk ⊙ sub t ≡⟨ sym ⊙-assoc ⟩ @@ -329,7 +334,7 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where ρ ⊙ id ≡⟨ ⊙-id ⟩ ρ ∎ - sub-⊙ : ∀ {m n} {ρ : Sub T m n} t → sub t ⊙ ρ ≡ ρ ↑ ⊙ sub (t / ρ) + sub-⊙ : ∀ {ρ : Sub T m n} t → sub t ⊙ ρ ≡ ρ ↑ ⊙ sub (t / ρ) sub-⊙ {ρ = ρ} t = begin sub t ⊙ ρ ≡⟨ refl ⟩ t / ρ ∷ id ⊙ ρ ≡⟨ cong (_∷_ (t / ρ)) id-⊙ ⟩ @@ -337,7 +342,7 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where t / ρ ∷ map weaken ρ ⊙ sub (t / ρ) ≡⟨ cong₂ _∷_ (sym var-/) refl ⟩ ρ ↑ ⊙ sub (t / ρ) ∎ - suc-/-↑ : ∀ {m n} {ρ : Sub T m n} x → + suc-/-↑ : ∀ {ρ : Sub T m n} x → var (suc x) / ρ ↑ ≡ var x / ρ / wk suc-/-↑ {ρ = ρ} x = begin var (suc x) / ρ ↑ ≡⟨ var-/ ⟩ @@ -346,7 +351,7 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where lookup ρ x / wk ≡⟨ cong₂ _/_ (sym var-/) refl ⟩ var x / ρ / wk ∎ - weaken-↑ : ∀ {k n} t {ρ : Sub T k n} → weaken t / (ρ ↑) ≡ weaken (t / ρ) + weaken-↑ : ∀ t {ρ : Sub T m n} → weaken t / (ρ ↑) ≡ weaken (t / ρ) weaken-↑ t {ρ} = begin weaken t / (ρ ↑) ≡⟨ cong (_/ ρ ↑) (sym /-wk) ⟩ t / wk / ρ ↑ ≡⟨ sym (wk-commutes t) ⟩ @@ -357,10 +362,11 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where hiding (/✶-↑✶; /✶-↑✶′; wk-↑⋆-⊙-wk; lookup-wk-↑⋆-⊙; lookup-map-weaken-↑⋆) +------------------------------------------------------------------------ -- For an example of how AppLemmas can be used, see -- Data.Fin.Substitution.List. -record AppLemmas {ℓ₁ ℓ₂} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where +record AppLemmas (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where field application : Application T₁ T₂ lemmas₄ : Lemmas₄ T₂ @@ -376,7 +382,7 @@ record AppLemmas {ℓ₁ ℓ₂} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ private module L₄ = Lemmas₄ lemmas₄ - /-⨀ : ∀ {m n} t (ρs : Subs T₂ m n) → t / ⨀ ρs ≡ t /✶ ρs + /-⨀ : ∀ t (ρs : Subs T₂ m n) → t / ⨀ ρs ≡ t /✶ ρs /-⨀ t ε = id-vanishes t /-⨀ t (ρ ◅ ε) = refl /-⨀ t (ρ ◅ (ρ′ ◅ ρs′)) = begin @@ -385,7 +391,7 @@ record AppLemmas {ℓ₁ ℓ₂} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ t /✶ ρs / ρ ∎ where ρs = ρ′ ◅ ρs′ - ⨀→/✶ : ∀ {m n} (ρs₁ ρs₂ : Subs T₂ m n) → + ⨀→/✶ : (ρs₁ ρs₂ : Subs T₂ m n) → ⨀ ρs₁ ≡ ⨀ ρs₂ → ∀ t → t /✶ ρs₁ ≡ t /✶ ρs₂ ⨀→/✶ ρs₁ ρs₂ hyp t = begin t /✶ ρs₁ ≡⟨ sym (/-⨀ t ρs₁) ⟩ @@ -393,19 +399,19 @@ record AppLemmas {ℓ₁ ℓ₂} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ t / ⨀ ρs₂ ≡⟨ /-⨀ t ρs₂ ⟩ t /✶ ρs₂ ∎ - wk-commutes : ∀ {m n} {ρ : Sub T₂ m n} t → + wk-commutes : ∀ {ρ : Sub T₂ m n} t → t / ρ / wk ≡ t / wk / ρ ↑ wk-commutes {ρ = ρ} = ⨀→/✶ (ε ▻ ρ ▻ wk) (ε ▻ wk ▻ ρ ↑) L₄.⊙-wk - sub-commutes : ∀ {m n} {t′} {ρ : Sub T₂ m n} t → + sub-commutes : ∀ {t′} {ρ : Sub T₂ m n} t → t / sub t′ / ρ ≡ t / ρ ↑ / sub (t′ ⊘ ρ) sub-commutes {t′ = t′} {ρ} = ⨀→/✶ (ε ▻ sub t′ ▻ ρ) (ε ▻ ρ ↑ ▻ sub (t′ ⊘ ρ)) (L₄.sub-⊙ t′) - wk-sub-vanishes : ∀ {n t′} (t : T₁ n) → t / wk / sub t′ ≡ t + wk-sub-vanishes : ∀ {t′} (t : T₁ n) → t / wk / sub t′ ≡ t wk-sub-vanishes {t′ = t′} = ⨀→/✶ (ε ▻ wk ▻ sub t′) ε L₄.wk-⊙-sub - /-weaken : ∀ {m n} {ρ : Sub T₂ m n} t → t / map weaken ρ ≡ t / ρ / wk + /-weaken : ∀ {ρ : Sub T₂ m n} t → t / map weaken ρ ≡ t / ρ / wk /-weaken {ρ = ρ} = ⨀→/✶ (ε ▻ map weaken ρ) (ε ▻ ρ ▻ wk) L₄.map-weaken open Application application public @@ -527,19 +533,75 @@ record TermLemmas (T : ℕ → Set) : Set₁ where open Lemmas₅ lemmas₅ public hiding (lemmas₃) - wk-⊙-∷ : ∀ {m n} (t : T n) (ρ : Sub T m n) → (T.wk T.⊙ (t ∷ ρ)) ≡ ρ - wk-⊙-∷ t ρ = extensionality (λ x → begin + wk-⊙-∷ : (t : T n) (ρ : Sub T m n) → (T.wk T.⊙ (t ∷ ρ)) ≡ ρ + wk-⊙-∷ t ρ = extensionality λ x → begin lookup (T.wk T.⊙ (t ∷ ρ)) x ≡⟨ L₃.lookup-wk-↑⋆-⊙ 0 {ρ = t ∷ ρ} ⟩ - lookup ρ x ∎) + lookup ρ x ∎ - weaken-∷ : ∀ {k n} (t₁ : T k) {t₂ : T n} {ρ : Sub T k n} → T.weaken t₁ T./ (t₂ ∷ ρ) ≡ t₁ T./ ρ + weaken-∷ : (t₁ : T m) {t₂ : T n} {ρ : Sub T m n} → + T.weaken t₁ T./ (t₂ ∷ ρ) ≡ t₁ T./ ρ weaken-∷ t₁ {t₂} {ρ} = begin T.weaken t₁ T./ (t₂ ∷ ρ) ≡⟨ cong (T._/ (t₂ ∷ ρ)) (sym /-wk) ⟩ (t₁ T./ T.wk) T./ (t₂ ∷ ρ) ≡⟨ ⨀→/✶ ((t₂ ∷ ρ) ◅ T.wk ◅ ε) (ρ ◅ ε) (wk-⊙-∷ t₂ ρ) t₁ ⟩ t₁ T./ ρ ∎ - weaken-sub : ∀ {n} (t₁ : T n) {t₂ : T n} → T.weaken t₁ T./ (T.sub t₂) ≡ t₁ + weaken-sub : (t₁ : T n) {t₂ : T n} → T.weaken t₁ T./ (T.sub t₂) ≡ t₁ weaken-sub t₁ {t₂} = begin T.weaken t₁ T./ (T.sub t₂) ≡⟨ weaken-∷ t₁ ⟩ t₁ T./ T.id ≡⟨ id-vanishes t₁ ⟩ t₁ ∎ + + -- Lemmas relating renamings to substitutions. + + map-var≡ : {ρ₁ : Sub Fin m n} {ρ₂ : Sub T m n} {f : Fin m → Fin n} → + (∀ x → lookup ρ₁ x ≡ f x) → + (∀ x → lookup ρ₂ x ≡ T.var (f x)) → + map T.var ρ₁ ≡ ρ₂ + map-var≡ {ρ₁ = ρ₁} {ρ₂ = ρ₂} {f = f} hyp₁ hyp₂ = extensionality λ x → + lookup (map T.var ρ₁) x ≡⟨ VecProp.lookup-map x _ ρ₁ ⟩ + T.var (lookup ρ₁ x) ≡⟨ cong T.var $ hyp₁ x ⟩ + T.var (f x) ≡⟨ sym $ hyp₂ x ⟩ + lookup ρ₂ x ∎ + + wk≡wk : map T.var VarSubst.wk ≡ T.wk {n = n} + wk≡wk = map-var≡ VarLemmas.lookup-wk lookup-wk + + id≡id : map T.var VarSubst.id ≡ T.id {n = n} + id≡id = map-var≡ VarLemmas.lookup-id lookup-id + + sub≡sub : {x : Fin n} → map T.var (VarSubst.sub x) ≡ T.sub (T.var x) + sub≡sub = cong (_ ∷_) id≡id + + ↑≡↑ : {ρ : Sub Fin m n} → map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑ + ↑≡↑ {ρ = ρ} = map-var≡ + (VarLemmas.lookup-↑⋆ (lookup ρ) (λ _ → refl) 1) + (lookup-↑⋆ (lookup ρ) (λ _ → VecProp.lookup-map _ _ ρ) 1) + + /Var≡/ : ∀ {ρ : Sub Fin m n} {t} → t /Var ρ ≡ t T./ map T.var ρ + /Var≡/ {ρ = ρ} {t = t} = + /✶-↑✶ (ε ▻ ρ) (ε ▻ map T.var ρ) + (λ k x → + T.var x /Var ρ VarSubst.↑⋆ k ≡⟨ app-var ⟩ + T.var (lookup (ρ VarSubst.↑⋆ k) x) ≡⟨ cong T.var $ VarLemmas.lookup-↑⋆ _ (λ _ → refl) k _ ⟩ + T.var (lift k (VarSubst._/ ρ) x) ≡⟨ sym $ lookup-↑⋆ _ (λ _ → VecProp.lookup-map _ _ ρ) k _ ⟩ + lookup (map T.var ρ T.↑⋆ k) x ≡⟨ sym app-var ⟩ + T.var x T./ map T.var ρ T.↑⋆ k ∎) + zero t + + sub-renaming-commutes : ∀ {t x} {ρ : Sub T m n} → + t /Var VarSubst.sub x T./ ρ ≡ t T./ ρ T.↑ T./ T.sub (lookup ρ x) + sub-renaming-commutes {t = t} {x = x} {ρ = ρ} = + t /Var VarSubst.sub x T./ ρ ≡⟨ cong (T._/ ρ) /Var≡/ ⟩ + t T./ map T.var (VarSubst.sub x) T./ ρ ≡⟨ cong (λ ρ′ → t T./ ρ′ T./ ρ) sub≡sub ⟩ + t T./ T.sub (T.var x) T./ ρ ≡⟨ sub-commutes _ ⟩ + t T./ ρ T.↑ T./ T.sub (T.var x T./ ρ) ≡⟨ cong (λ t′ → t T./ ρ T.↑ T./ T.sub t′) app-var ⟩ + t T./ ρ T.↑ T./ T.sub (lookup ρ x) ∎ + + sub-commutes-with-renaming : ∀ {t t′} {ρ : Sub Fin m n} → + t T./ T.sub t′ /Var ρ ≡ t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) + sub-commutes-with-renaming {t = t} {t′ = t′} {ρ = ρ} = + t T./ T.sub t′ /Var ρ ≡⟨ /Var≡/ ⟩ + t T./ T.sub t′ T./ map T.var ρ ≡⟨ sub-commutes _ ⟩ + t T./ map T.var ρ T.↑ T./ T.sub (t′ T./ map T.var ρ) ≡⟨ sym $ cong (λ ρ′ → t T./ ρ′ T./ T.sub (t′ T./ map T.var ρ)) ↑≡↑ ⟩ + t T./ map T.var (ρ VarSubst.↑) T./ T.sub (t′ T./ map T.var ρ) ≡⟨ sym $ cong₂ (λ t ρ → t T./ T.sub ρ) /Var≡/ /Var≡/ ⟩ + t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) ∎ diff --git a/src/Data/Fin/Substitution/List.agda b/src/Data/Fin/Substitution/List.agda index 63a7e39279..ce5ff3e27c 100644 --- a/src/Data/Fin/Substitution/List.agda +++ b/src/Data/Fin/Substitution/List.agda @@ -19,17 +19,25 @@ open import Data.List.Properties open import Data.Fin.Substitution import Function.Base as Fun open import Relation.Binary.PropositionalEquality -open ≡-Reasoning private + variable + m n : ℕ + + ListT : ℕ → Set ℓ + ListT = List Fun.∘ T + open module L = Lemmas₄ lemmas₄ using (_/_; id; _⊙_) +------------------------------------------------------------------------ +-- Listwise application of a substitution, plus lemmas about it + infixl 8 _//_ -_//_ : ∀ {m n} → List (T m) → Sub T m n → List (T n) +_//_ : ListT m → Sub T m n → ListT n ts // ρ = map (λ σ → σ / ρ) ts -appLemmas : AppLemmas (λ n → List (T n)) T +appLemmas : AppLemmas ListT T appLemmas = record { application = record { _/_ = _//_ } ; lemmas₄ = lemmas₄ @@ -41,7 +49,7 @@ appLemmas = record ts // ρ₁ ⊙ ρ₂ ≡⟨ map-cong L./-⊙ ts ⟩ map (λ σ → σ / ρ₁ / ρ₂) ts ≡⟨ map-∘ ts ⟩ ts // ρ₁ // ρ₂ ∎ - } + } where open ≡-Reasoning open AppLemmas appLemmas public hiding (_/_) renaming (_/✶_ to _//✶_)