diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-15 16:35:15 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-15 16:35:15 +0100 |
| commit | a38b0b5a6ee30e7dd22bc91765ba5361ed807dda (patch) | |
| tree | b2e4006c3d2feef19281aafb559f001bc3986693 /src/Core/Term/Thinned.idr | |
| parent | 5f83999f483e241158706522a35364ba32f7f203 (diff) | |
Prove substitution respects the quotient.
Diffstat (limited to 'src/Core/Term/Thinned.idr')
| -rw-r--r-- | src/Core/Term/Thinned.idr | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Core/Term/Thinned.idr b/src/Core/Term/Thinned.idr index 0bc6dcf..824439a 100644 --- a/src/Core/Term/Thinned.idr +++ b/src/Core/Term/Thinned.idr @@ -3,6 +3,8 @@ module Core.Term.Thinned import Core.Term import Core.Thinning +import Syntax.PreorderReasoning + %prefix_record_projections off infix 4 =~= @@ -32,3 +34,11 @@ t =~= u = expand t = expand u public export wkn : Thinned m -> m `Thins` n -> Thinned n wkn t thin = { thin $= (thin .) } t + +export +wknCong : t =~= u -> (thin : m `Thins` n) -> wkn t thin =~= wkn u thin +wknCong {t = t `Over` thin1, u = u `Over` thin2} prf thin = Calc $ + |~ wkn t (thin . thin1) + ~~ wkn (wkn t thin1) thin ...(sym $ wknHomo t thin1 thin) + ~~ wkn (wkn u thin2) thin ...(cong (flip wkn thin) prf) + ~~ wkn u (thin . thin2) ...(wknHomo u thin2 thin) |