77 lines
1.8 KiB
Idris
77 lines
1.8 KiB
Idris
|
||| "order preserving embeddings", for recording a correspondence between
|
||
|
|
||| a smaller scope and part of a larger one.
|
||
|
|
module Quox.OPE
|
||
|
|
|
||
|
|
import Quox.NatExtra
|
||
|
|
import Data.Nat
|
||
|
|
|
||
|
|
%default total
|
||
|
|
|
||
|
|
|
||
|
|
public export
|
||
|
|
data OPE : Nat -> Nat -> Type where
|
||
|
|
Id : OPE n n
|
||
|
|
Drop : OPE m n -> OPE m (S n)
|
||
|
|
Keep : OPE m n -> OPE (S m) (S n)
|
||
|
|
%name OPE p, q
|
||
|
|
|
||
|
|
public export %inline Injective Drop where injective Refl = Refl
|
||
|
|
public export %inline Injective Keep where injective Refl = Refl
|
||
|
|
|
||
|
|
public export
|
||
|
|
opeZero : {n : Nat} -> OPE 0 n
|
||
|
|
opeZero {n = 0} = Id
|
||
|
|
opeZero {n = S n} = Drop opeZero
|
||
|
|
|
||
|
|
public export
|
||
|
|
(.) : OPE m n -> OPE n p -> OPE m p
|
||
|
|
p . Id = p
|
||
|
|
Id . q = q
|
||
|
|
p . Drop q = Drop $ p . q
|
||
|
|
Drop p . Keep q = Drop $ p . q
|
||
|
|
Keep p . Keep q = Keep $ p . q
|
||
|
|
|
||
|
|
public export
|
||
|
|
toLTE : {m : Nat} -> OPE m n -> m `LTE` n
|
||
|
|
toLTE Id = reflexive
|
||
|
|
toLTE (Drop p) = lteSuccRight $ toLTE p
|
||
|
|
toLTE (Keep p) = LTESucc $ toLTE p
|
||
|
|
|
||
|
|
|
||
|
|
public export
|
||
|
|
keepN : (n : Nat) -> OPE a b -> OPE (n + a) (n + b)
|
||
|
|
keepN 0 p = p
|
||
|
|
keepN (S n) p = Keep $ keepN n p
|
||
|
|
|
||
|
|
public export
|
||
|
|
dropInner' : LTE' m n -> OPE m n
|
||
|
|
dropInner' LTERefl = Id
|
||
|
|
dropInner' (LTESuccR p) = Drop $ dropInner' $ force p
|
||
|
|
|
||
|
|
public export
|
||
|
|
dropInner : {n : Nat} -> LTE m n -> OPE m n
|
||
|
|
dropInner = dropInner' . fromLte
|
||
|
|
|
||
|
|
public export
|
||
|
|
dropInnerN : (m : Nat) -> OPE n (m + n)
|
||
|
|
dropInnerN 0 = Id
|
||
|
|
dropInnerN (S m) = Drop $ dropInnerN m
|
||
|
|
|
||
|
|
|
||
|
|
public export
|
||
|
|
interface Tighten t where
|
||
|
|
tighten : OPE m n -> t n -> Maybe (t m)
|
||
|
|
|
||
|
|
parameters {auto _ : Tighten t}
|
||
|
|
export %inline
|
||
|
|
tightenInner : {n : Nat} -> m `LTE` n -> t n -> Maybe (t m)
|
||
|
|
tightenInner = tighten . dropInner
|
||
|
|
|
||
|
|
export %inline
|
||
|
|
tightenN : (m : Nat) -> t (m + n) -> Maybe (t n)
|
||
|
|
tightenN m = tighten $ dropInnerN m
|
||
|
|
|
||
|
|
export %inline
|
||
|
|
tighten1 : t (S n) -> Maybe (t n)
|
||
|
|
tighten1 = tightenN 1
|