Skip to content

Some lemmas related to renamings and substitutions #1750

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Sep 27, 2023
Merged
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 32 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -1142,6 +1142,38 @@ Other minor changes
cantor-schröder-bernstein : ∀ {f : Fin m → Fin n} {g : Fin n → Fin m} → Injective f → Injective g → m ≡ n
```

* Changed the fixity of `Data.Fin.Substitution.TermSubst._/Var_`.

* Added new lemmas in `Data.Fin.Substitution.Lemmas.TermLemmas`:
```
map-var≡ :
∀ {m n} {ρ₁ : 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 :
∀ {n} → map T.var VarSubst.wk ≡ T.wk {n = n}
id≡id :
∀ {n} → map T.var VarSubst.id ≡ T.id {n = n}
sub≡sub :
∀ {n} {x : Fin n} →
map T.var (VarSubst.sub x) ≡ T.sub (T.var x)
↑≡↑ :
∀ {m n} {ρ : Sub Fin m n} →
map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑
/Var≡/ :
∀ {m n} {ρ : Sub Fin m n} {t} →
t /Var ρ ≡ t T./ map T.var ρ
sub-renaming-commutes :
∀ {m n t x} {ρ : Sub T m n} →
t /Var VarSubst.sub x T./ ρ ≡
t T./ ρ T.↑ T./ T.sub (lookup ρ x)
sub-commutes-with-renaming :
∀ {m n} {t t′} {ρ : 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`:
```
_^_ : ℤ → ℕ → ℤ
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Fin/Substitution.agda
Original file line number Diff line number Diff line change
Expand Up @@ -160,7 +160,7 @@ 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_ = app varLift
Expand Down
66 changes: 66 additions & 0 deletions src/Data/Fin/Substitution/Lemmas.agda
Original file line number Diff line number Diff line change
Expand Up @@ -543,3 +543,69 @@ record TermLemmas (T : ℕ → Set) : Set₁ where
T.weaken t₁ T./ (T.sub t₂) ≡⟨ weaken-∷ t₁ ⟩
t₁ T./ T.id ≡⟨ id-vanishes t₁ ⟩
t₁ ∎

-- Lemmas relating renamings to substitutions.

map-var≡ :
∀ {m n} {ρ₁ : 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 : ∀ {n} → map T.var VarSubst.wk ≡ T.wk {n = n}
wk≡wk = map-var≡ VarLemmas.lookup-wk lookup-wk

id≡id : ∀ {n} → map T.var VarSubst.id ≡ T.id {n = n}
id≡id = map-var≡ VarLemmas.lookup-id lookup-id

sub≡sub :
∀ {n} {x : Fin n} →
map T.var (VarSubst.sub x) ≡ T.sub (T.var x)
sub≡sub = cong (_ ∷_) id≡id

↑≡↑ :
∀ {m n} {ρ : 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≡/ :
∀ {m n} {ρ : 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 :
∀ {m n 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 :
∀ {m n} {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 ρ) ∎