Add some lemmas related to renamings and substitutions (#1750)

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`:
   ```
   _^_ : ℤ → ℕ → ℤ

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)

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

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 (_/_)