diff options
Diffstat (limited to 'src/Core/Term/Substitution.idr')
| -rw-r--r-- | src/Core/Term/Substitution.idr | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/src/Core/Term/Substitution.idr b/src/Core/Term/Substitution.idr index 6846d80..abeb487 100644 --- a/src/Core/Term/Substitution.idr +++ b/src/Core/Term/Substitution.idr @@ -30,6 +30,16 @@ index (Wkn thin) i = Var i `Over` thin index (sub :< t) FZ = t index (sub :< t) (FS i) = index sub i +export +indexCong : + {0 sub1, sub2 : Subst m n} -> + sub1 =~= sub2 -> + (i : Fin m) -> + index sub1 i =~= index sub2 i +indexCong Refl i = Refl +indexCong (prf :< prf') FZ = prf' +indexCong (prf :< prf') (FS i) = indexCong prf i + -- Weakening ------------------------------------------------------------------- public export @@ -37,6 +47,15 @@ wkn : Subst k m -> m `Thins` n -> Subst k n wkn (Wkn thin') thin = Wkn (thin . thin') wkn (sub :< t) thin = wkn sub thin :< wkn t thin +export +wknCong : + {0 sub1, sub2 : Subst k m} -> + sub1 =~= sub2 -> + (thin : m `Thins` n) -> + wkn sub1 thin =~= wkn sub2 thin +wknCong Refl thin = Refl +wknCong (prf :< prf') thin = wknCong prf thin :< wknCong prf' thin + -- Constructors ---------------------------------------------------------------- public export @@ -52,3 +71,18 @@ subst Set sub = Set subst (Pi t u) sub = Pi (subst t sub) (subst u $ lift sub) subst (Abs t) sub = Abs (subst t $ lift sub) subst (App t u) sub = App (subst t sub) (subst u sub) + +export +substCong : + (t : Term m) -> + {0 sub1, sub2 : Subst m n} -> + sub1 =~= sub2 -> + subst t sub1 = subst t sub2 +substCong (Var i) prf = indexCong prf i +substCong Set prf = Refl +substCong (Pi t u) prf = + cong2 Pi + (substCong t prf) + (substCong u $ wknCong prf (drop $ id n) :< Refl) +substCong (Abs t) prf = cong Abs (substCong t $ wknCong prf (drop $ id n) :< Refl) +substCong (App t u) prf = cong2 App (substCong t prf) (substCong u prf) |