open import Definition.Typed.Restrictions
open import Graded.Modality
module Definition.Typed.Decidable.Internal.Weakening
{a} {M : Set a}
{π : Modality M}
(R : Type-restrictions π)
where
open import Definition.Typed.Decidable.Internal.Term R
open import Definition.Untyped M as U using (Wk)
open import Definition.Untyped.Properties M
import Definition.Untyped.Sup R as S
open Wk
open import Tools.Fin
open import Tools.Function
open import Tools.Maybe
open import Tools.Nat as N
open import Tools.Product as Ξ£
import Tools.PropositionalEquality as PE
open import Tools.Reasoning.PropositionalEquality
private variable
n nβ nβ nβ : Nat
c : Constants
Ξ³ : Contexts _
Ο : Wk _ _
Ο : Subst _ _ _
mutual
infixl 30 _β’β_
_β’β_ : Wk nβ nβ β Subst c nβ nβ β Subst c nβ nβ
id β’β Ο = Ο
step Ο β’β Ο = wk1 (Ο β’β Ο)
lift Ο β’β id = toSubst Ο β
lift Ο β’β Ο β = (Ο β’β Ο) β
lift Ο β’β wk1 Ο = wk1 (Ο β’β Ο)
Ο β’β cons Ο t = cons (Ο β’β Ο) (weaken Ο t)
toSubst : Wk nβ nβ β Subst c nβ nβ
toSubst Ο = Ο β’β id
opaque mutual
ββ’ββΛ’ : β x β β Ο β’β Ο βΛ’ Ξ³ x PE.β‘ (Ο U.β’β β Ο βΛ’ Ξ³) x
ββ’ββΛ’ {Ο = id} {Ο} {Ξ³} x =
β Ο βΛ’ Ξ³ x β‘Λβ¨ wk-id _ β©
U.wk U.id (β Ο βΛ’ Ξ³ x) β
ββ’ββΛ’ {Ο = step Ο} {Ο} {Ξ³} x =
U.wk1 (β Ο β’β Ο βΛ’ Ξ³ x) β‘β¨ PE.cong U.wk1 (ββ’ββΛ’ _) β©
U.wk1 ((Ο U.β’β β Ο βΛ’ Ξ³) x) β‘β¨β©
U.wk1 (U.wk Ο (β Ο βΛ’ Ξ³ x)) β‘β¨ wk1-wk _ _ β©
U.wk (step Ο) (β Ο βΛ’ Ξ³ x) β
ββ’ββΛ’ {Ο = lift _} {Ο = id} x0 =
PE.refl
ββ’ββΛ’ {Ο = lift Ο} {Ο = id} {Ξ³} (x +1) =
U.wk1 (β toSubst Ο βΛ’ Ξ³ x) β‘β¨ PE.cong U.wk1 (βtoSubstβΛ’ x) β©
U.wk1 (U.toSubst Ο x) β
ββ’ββΛ’ {Ο = lift Ο} {Ο = wk1 Ο} {Ξ³} x =
U.wk1 (β Ο β’β Ο βΛ’ Ξ³ x) β‘β¨ PE.cong U.wk1 (ββ’ββΛ’ _) β©
U.wk1 (U.wk Ο (β Ο βΛ’ Ξ³ x)) β‘β¨ wk1-wkβ‘lift-wk1 _ _ β©
U.wk (lift Ο) (U.wk1 (β Ο βΛ’ Ξ³ x)) β
ββ’ββΛ’ {Ο = lift _} {Ο = _ β} x0 =
PE.refl
ββ’ββΛ’ {Ο = lift Ο} {Ο = Ο β} {Ξ³} (x +1) =
U.wk1 (β Ο β’β Ο βΛ’ Ξ³ x) β‘β¨ PE.cong U.wk1 (ββ’ββΛ’ _) β©
U.wk1 (U.wk Ο (β Ο βΛ’ Ξ³ x)) β‘β¨ wk1-wkβ‘lift-wk1 _ _ β©
U.wk (U.lift Ο) (U.wk1 (β Ο βΛ’ Ξ³ x)) β
ββ’ββΛ’ {Ο = lift _} {Ο = cons _ _} x0 =
PE.refl
ββ’ββΛ’ {Ο = Ο@(lift _)} {Ο = cons Ο _} {Ξ³} (x +1) =
β Ο β’β Ο βΛ’ Ξ³ x β‘β¨ ββ’ββΛ’ {Ο = Ο} x β©
U.wk Ο (β Ο βΛ’ Ξ³ x) β
βtoSubstβΛ’ : β x β β toSubst Ο βΛ’ Ξ³ x PE.β‘ U.toSubst Ο x
βtoSubstβΛ’ = ββ’ββΛ’ {Ο = id}
wk : Wk nβ nβ β Term c nβ β Term c nβ
wk Ο (meta-var x Ο) = meta-var x (Ο β’β Ο)
wk Ο (weaken Οβ² t) = weaken (Ο U.β’ Οβ²) t
wk Ο (subst t Ο) = subst t (Ο β’β Ο)
wk Ο (var x) = var (U.wkVar Ο x)
wk Ο (defn Ξ±) = defn Ξ±
wk Ο Empty = Empty
wk Ο (emptyrec p A t) = emptyrec p (weaken Ο A) (weaken Ο t)
wk _ Level = Level
wk _ zeroα΅ = zeroα΅
wk Ο (sucα΅ l) = sucα΅ (weaken Ο l)
wk Ο (lβ supα΅β lβ) = weaken Ο lβ supα΅β weaken Ο lβ
wk Ο (U l) = U (weaken Ο l)
wk Ο (Lift l A) = Lift (weaken Ο l) (weaken Ο A)
wk Ο (lift l t) = lift (weaken Ο <$> l) (weaken Ο t)
wk Ο (lower t) = lower (weaken Ο t)
wk Ο (Unit s) = Unit s
wk Ο (star s) = star s
wk Ο (unitrec p q A t u) = unitrec p q (weaken (lift Ο) A)
(weaken Ο t) (weaken Ο u)
wk Ο (Ξ Ξ£β¨ b β© p , q β· A βΉ B) = Ξ Ξ£β¨ b β© p , q β· weaken Ο A βΉ
weaken (lift Ο) B
wk Ο (lam p qA t) = lam p (Ξ£.map idαΆ (weaken Ο) <$> qA)
(weaken (lift Ο) t)
wk Ο (t ββ¨ p β© u) = weaken Ο t ββ¨ p β© weaken Ο u
wk Ο (prod s p qB t u) = prod s p
(Ξ£.map idαΆ (weaken (lift Ο)) <$> qB)
(weaken Ο t) (weaken Ο u)
wk Ο (fst p t) = fst p (weaken Ο t)
wk Ο (snd p t) = snd p (weaken Ο t)
wk Ο (prodrec r p q A t u) = prodrec r p q (weaken (lift Ο) A)
(weaken Ο t) (weaken (U.liftn Ο 2) u)
wk Ο β = β
wk Ο zero = zero
wk Ο (suc t) = suc (weaken Ο t)
wk Ο (natrec p q r A t u v) = natrec p q r (weaken (lift Ο) A)
(weaken Ο t) (weaken (U.liftn Ο 2) u)
(weaken Ο v)
wk Ο (Id A t u) = Id (weaken Ο A) (weaken Ο t) (weaken Ο u)
wk Ο (rfl t) = rfl (weaken Ο <$> t)
wk Ο (J p q A t B u v w) = J p q (weaken Ο A) (weaken Ο t)
(weaken (U.liftn Ο 2) B) (weaken Ο u)
(weaken Ο v) (weaken Ο w)
wk Ο (K p A t B u v) = K p (weaken Ο A) (weaken Ο t)
(weaken (lift Ο) B) (weaken Ο u)
(weaken Ο v)
wk Ο ([]-cong s l A t u v) = []-cong s (weaken Ο l) (weaken Ο A)
(weaken Ο t) (weaken Ο u) (weaken Ο v)
opaque
βwkβ : (t : Term c n) β β wk Ο t β Ξ³ PE.β‘ U.wk Ο (β t β Ξ³)
βwkβ {Ο} {Ξ³} (meta-var x Ο) =
β meta-var x (Ο β’β Ο) β Ξ³ β‘β¨ βmeta-varβ (Ο β’β _) β©
β x βα΅ Ξ³ U.[ β Ο β’β Ο βΛ’ Ξ³ ] β‘β¨ substVar-to-subst ββ’ββΛ’ (β x βα΅ Ξ³) β©
β x βα΅ Ξ³ U.[ Ο U.β’β β Ο βΛ’ Ξ³ ] β‘Λβ¨ wk-subst (β x βα΅ Ξ³) β©
U.wk Ο (β x βα΅ Ξ³ U.[ β Ο βΛ’ Ξ³ ]) β‘Λβ¨ PE.cong (U.wk _) (βmeta-varβ Ο) β©
U.wk Ο (β meta-var x Ο β Ξ³) β
βwkβ {Ο} {Ξ³} (weaken Οβ² t) =
β weaken (Ο U.β’ Οβ²) t β Ξ³ β‘β¨β©
U.wk (Ο U.β’ Οβ²) (β t β Ξ³) β‘Λβ¨ wk-comp _ _ _ β©
U.wk Ο (U.wk Οβ² (β t β Ξ³)) β
βwkβ {Ο} {Ξ³} (subst t Ο) =
β t β Ξ³ U.[ β Ο β’β Ο βΛ’ Ξ³ ] β‘β¨ substVar-to-subst ββ’ββΛ’ (β t β _) β©
β t β Ξ³ U.[ Ο U.β’β β Ο βΛ’ Ξ³ ] β‘Λβ¨ wk-subst (β t β _) β©
U.wk Ο (β t β Ξ³ U.[ β Ο βΛ’ Ξ³ ]) β
βwkβ (var _) =
PE.refl
βwkβ (defn _) =
PE.refl
βwkβ Level =
PE.refl
βwkβ zeroα΅ =
PE.refl
βwkβ (sucα΅ _) =
PE.refl
βwkβ {Ο} {Ξ³} (lβ supα΅β lβ) =
U.wk Ο (β lβ β Ξ³) S.supα΅β U.wk Ο (β lβ β Ξ³) β‘Λβ¨ S.wk-supα΅β β©
U.wk Ο (β lβ β Ξ³ S.supα΅β β lβ β Ξ³) β
βwkβ (U _) =
PE.refl
βwkβ (Lift _ _) =
PE.refl
βwkβ (lift _ _) =
PE.refl
βwkβ (lower _) =
PE.refl
βwkβ Empty =
PE.refl
βwkβ (emptyrec _ _ _) =
PE.refl
βwkβ (Unit _) =
PE.refl
βwkβ (star _) =
PE.refl
βwkβ (unitrec _ _ _ _ _) =
PE.refl
βwkβ (Ξ Ξ£β¨ _ β© _ , _ β· _ βΉ _) =
PE.refl
βwkβ (lam _ _ _) =
PE.refl
βwkβ (_ ββ¨ _ β© _) =
PE.refl
βwkβ (prod _ _ _ _ _) =
PE.refl
βwkβ (fst _ _) =
PE.refl
βwkβ (snd _ _) =
PE.refl
βwkβ (prodrec _ _ _ _ _ _) =
PE.refl
βwkβ β =
PE.refl
βwkβ zero =
PE.refl
βwkβ (suc _) =
PE.refl
βwkβ (natrec _ _ _ _ _ _ _) =
PE.refl
βwkβ (Id _ _ _) =
PE.refl
βwkβ (rfl _) =
PE.refl
βwkβ (J _ _ _ _ _ _ _ _) =
PE.refl
βwkβ (K _ _ _ _ _ _) =
PE.refl
βwkβ ([]-cong _ _ _ _ _ _) =
PE.refl
wk[_] : β k β Term c n β Term c (k N.+ n)
wk[ k ] t = weaken (U.stepn id k) t