572 lines
18 KiB
Idris
572 lines
18 KiB
Idris
module Quox.OPE.Sub
|
|
|
|
import Quox.OPE.Basics
|
|
import Quox.OPE.Length
|
|
import Quox.NatExtra
|
|
import Data.DPair
|
|
import Data.SnocList.Elem
|
|
import Data.SnocList.Quantifiers
|
|
|
|
%default total
|
|
|
|
infix 0 `Sub'`, `Sub`
|
|
|
|
public export
|
|
data Sub' : Scope a -> Scope a -> Type where
|
|
End : [<] `Sub'` [<]
|
|
Keep : xs `Sub'` ys -> xs :< z `Sub'` ys :< z
|
|
Drop : xs `Sub'` ys -> xs `Sub'` ys :< z
|
|
%name Sub' p, q
|
|
|
|
export
|
|
keepInjective : Keep p = Keep q -> p = q
|
|
keepInjective Refl = Refl
|
|
|
|
export
|
|
dropInjective : Drop p = Drop q -> p = q
|
|
dropInjective Refl = Refl
|
|
|
|
-- these need to be `public export` so that
|
|
-- `id`, `zero`, and maybe others can reduce
|
|
public export %hint
|
|
lengthLeft : xs `Sub'` ys -> Length xs
|
|
lengthLeft End = Z
|
|
lengthLeft (Keep p) = S (lengthLeft p)
|
|
lengthLeft (Drop p) = lengthLeft p
|
|
|
|
public export %hint
|
|
lengthRight : xs `Sub'` ys -> Length ys
|
|
lengthRight End = Z
|
|
lengthRight (Keep p) = S (lengthRight p)
|
|
lengthRight (Drop p) = S (lengthRight p)
|
|
|
|
|
|
export %inline
|
|
dropLast' : (xs :< x) `Sub'` ys -> xs `Sub'` ys
|
|
dropLast' (Keep p) = Drop p
|
|
dropLast' (Drop p) = Drop $ dropLast' p
|
|
|
|
export
|
|
Uninhabited (xs :< x `Sub'` [<]) where uninhabited _ impossible
|
|
|
|
export
|
|
Uninhabited (xs :< x `Sub'` xs) where
|
|
uninhabited (Keep p) = uninhabited p
|
|
uninhabited (Drop p) = uninhabited $ dropLast' p
|
|
|
|
|
|
export
|
|
0 lteLen : xs `Sub'` ys -> length xs `LTE` length ys
|
|
lteLen End = LTEZero
|
|
lteLen (Keep p) = LTESucc $ lteLen p
|
|
lteLen (Drop p) = lteSuccRight $ lteLen p
|
|
|
|
export
|
|
0 lteNilRight : xs `Sub'` [<] -> xs = [<]
|
|
lteNilRight End = Refl
|
|
|
|
|
|
|
|
public export
|
|
refl' : Length xs => xs `Sub'` xs
|
|
refl' @{Z} = End
|
|
refl' @{S s} = Keep refl'
|
|
|
|
public export
|
|
zero' : Length xs => [<] `Sub'` xs
|
|
zero' @{Z} = End
|
|
zero' @{S s} = Drop zero'
|
|
|
|
public export
|
|
single' : Length xs => x `Elem` xs -> [< x] `Sub'` xs
|
|
single' @{S _} Here = Keep zero'
|
|
single' @{S _} (There p) = Drop $ single' p
|
|
|
|
|
|
namespace Sub
|
|
public export
|
|
(.) : ys `Sub'` zs -> xs `Sub'` ys -> xs `Sub'` zs
|
|
End . End = End
|
|
(Keep p) . (Keep q) = Keep $ p . q
|
|
(Keep p) . (Drop q) = Drop $ p . q
|
|
(Drop p) . q = Drop $ p . q
|
|
|
|
public export
|
|
comp' : ys `Sub'` zs -> xs `Sub'` ys -> xs `Sub'` zs
|
|
comp' = (.)
|
|
|
|
public export %inline
|
|
trans' : xs `Sub'` ys -> ys `Sub'` zs -> xs `Sub'` zs
|
|
trans' = flip (.)
|
|
|
|
public export
|
|
app' : xs1 `Sub'` ys1 -> xs2 `Sub'` ys2 -> (xs1 ++ xs2) `Sub'` (ys1 ++ ys2)
|
|
app' p End = p
|
|
app' p (Keep q) = Keep $ app' p q
|
|
app' p (Drop q) = Drop $ app' p q
|
|
|
|
|
|
||| if `p` holds for all elements of the main list,
|
|
||| it holds for all elements of the sublist
|
|
public export
|
|
subAll' : xs `Sub'` ys -> All p ys -> All p xs
|
|
subAll' End [<] = [<]
|
|
subAll' (Keep q) (ps :< x) = subAll' q ps :< x
|
|
subAll' (Drop q) (ps :< x) = subAll' q ps
|
|
|
|
||| if `p` holds for one element of the sublist,
|
|
||| it holds for one element of the main list
|
|
public export
|
|
subAny' : xs `Sub'` ys -> Any p xs -> Any p ys
|
|
subAny' (Keep q) (Here x) = Here x
|
|
subAny' (Keep q) (There x) = There (subAny' q x)
|
|
subAny' (Drop q) x = There (subAny' q x)
|
|
|
|
|
|
public export
|
|
data SubView : (lte : xs `Sub'` ys) -> (mask : Nat) -> Type where
|
|
[search lte]
|
|
END : (0 eq : n = 0) -> SubView End n
|
|
KEEP : {n : Nat} -> {0 p : xs `Sub'` ys} ->
|
|
(0 v : SubView p n) -> (0 eq : n' = S (2 * n)) ->
|
|
SubView (Keep {z} p) n'
|
|
DROP : {n : Nat} -> {0 p : xs `Sub'` ys} ->
|
|
(0 v : SubView p n) -> (0 eq : n' = 2 * n) ->
|
|
SubView (Drop {z} p) n'
|
|
%name SubView v
|
|
|
|
public export
|
|
record Sub {a : Type} (xs, ys : Scope a) where
|
|
constructor SubM
|
|
mask : Nat
|
|
0 lte : xs `Sub'` ys
|
|
0 view0 : SubView lte mask
|
|
%name Sub sub
|
|
|
|
public export %inline
|
|
sub : {mask : Nat} -> {0 lte : xs `Sub'` ys} -> (0 view0 : SubView lte mask) ->
|
|
xs `Sub` ys
|
|
sub v = SubM _ _ v
|
|
|
|
|
|
private
|
|
0 uip : (p, q : a = b) -> p = q
|
|
uip Refl Refl = Refl
|
|
|
|
export
|
|
0 viewIrrel : Length ys =>
|
|
{m : Nat} -> {lte : xs `Sub'` ys} ->
|
|
(v1, v2 : SubView lte m) -> v1 === v2
|
|
viewIrrel (END eq1) (END eq2) = rewrite uip eq1 eq2 in Refl
|
|
viewIrrel (KEEP v1 eq1) (KEEP v2 eq2) with (sDoubleInj $ trans (sym eq1) eq2)
|
|
_ | Refl = rewrite viewIrrel v1 v2 in rewrite uip eq1 eq2 in Refl
|
|
viewIrrel (DROP v1 eq1) (DROP v2 eq2) with (doubleInj $ trans (sym eq1) eq2)
|
|
_ | Refl = rewrite viewIrrel v1 v2 in rewrite uip eq1 eq2 in Refl
|
|
|
|
export
|
|
0 viewLteEq : {p, q : xs `Sub'` ys} -> SubView p m -> SubView q m -> p = q
|
|
viewLteEq (END _) (END _) = Refl
|
|
viewLteEq (KEEP {n = m} pv pe) (KEEP {n} qv qe) =
|
|
let eq = sDoubleInj {m, n} $ trans (sym pe) qe in
|
|
rewrite viewLteEq pv (rewrite eq in qv) in Refl
|
|
viewLteEq (KEEP pv pe) (DROP qv qe) = absurd $ lsbMutex qe pe
|
|
viewLteEq (DROP pv pe) (KEEP qv qe) = absurd $ lsbMutex pe qe
|
|
viewLteEq (DROP {n = m} pv pe) (DROP {n} qv qe) =
|
|
let eq = doubleInj {m, n} $ trans (sym pe) qe in
|
|
rewrite viewLteEq pv (rewrite eq in qv) in Refl
|
|
|
|
private
|
|
0 lteEq' : (p : xs `Sub'` ys) ->
|
|
(v1 : SubView p m1) -> (v2 : SubView p m2) ->
|
|
SubM m1 p v1 = SubM m2 p v2
|
|
lteEq' End (END Refl) (END Refl) = Refl
|
|
lteEq' {m1 = S (2 * n)} {m2 = S (2 * n)} (Keep p) (KEEP v1 Refl) (KEEP v2 Refl) =
|
|
cong (\v => SubM (S (2 * n)) (Keep p) (KEEP v Refl)) $
|
|
case lteEq' p v1 v2 of Refl => Refl
|
|
lteEq' {m1 = 2 * n} {m2 = 2 * n} (Drop p) (DROP v1 Refl) (DROP v2 Refl) =
|
|
cong (\v => SubM (2 * n) (Drop p) (DROP v Refl)) $
|
|
case lteEq' p v1 v2 of Refl => Refl
|
|
lteEq' {m1 = _} {m2 = S _} _ _ (END _) impossible
|
|
lteEq' {m1 = Z} {m2 = _} _ (KEEP _ _) _ impossible
|
|
lteEq' {m1 = _} {m2 = Z} _ _ (KEEP _ _) impossible
|
|
|
|
export
|
|
0 lteEq : {p, q : xs `Sub` ys} -> p.lte = q.lte -> p = q
|
|
lteEq {p = SubM pm pl pv} {q = SubM qm ql qv} eq =
|
|
rewrite eq in lteEq' ql (rewrite sym eq in pv) qv
|
|
|
|
|
|
public export %inline
|
|
end : [<] `Sub` [<]
|
|
end = SubM 0 End (END Refl)
|
|
|
|
public export %inline
|
|
keep : xs `Sub` ys -> xs :< z `Sub` ys :< z
|
|
keep (SubM mask lte view0) = SubM (S (2 * mask)) (Keep lte) (KEEP view0 Refl)
|
|
|
|
public export %inline
|
|
drop : xs `Sub` ys -> xs `Sub` ys :< z
|
|
drop (SubM mask lte view0) = SubM (2 * mask) (Drop lte) (DROP view0 Refl)
|
|
|
|
|
|
export
|
|
0 keepLte : (p : xs `Sub` ys) -> (keep p).lte = Keep p.lte
|
|
keepLte (SubM mask lte view0) = Refl
|
|
|
|
export
|
|
0 dropLte : (p : xs `Sub` ys) -> (drop p).lte = Drop p.lte
|
|
dropLte (SubM mask lte view0) = Refl
|
|
|
|
|
|
public export
|
|
data Eqv : {xs, ys : Scope a} -> (p, q : xs `Sub` ys) -> Type where
|
|
EQV : {0 p, q : xs `Sub` ys} -> p.mask = q.mask -> p `Eqv` q
|
|
%name Eqv eqv
|
|
|
|
export
|
|
Reflexive (xs `Sub` ys) Eqv where
|
|
reflexive = EQV Refl
|
|
|
|
export
|
|
Symmetric (xs `Sub` ys) Eqv where
|
|
symmetric (EQV eq) = EQV $ sym eq
|
|
|
|
export
|
|
Transitive (xs `Sub` ys) Eqv where
|
|
transitive (EQV eq1) (EQV eq2) = EQV $ trans eq1 eq2
|
|
|
|
export
|
|
0 eqvToEq : {p, q : xs `Sub` ys} -> p `Eqv` q -> p = q
|
|
eqvToEq {p = SubM _ _ pv} {q = SubM _ _ qv} (EQV Refl) with (viewLteEq pv qv)
|
|
_ | Refl = rewrite viewIrrel pv qv in Refl
|
|
|
|
export
|
|
0 eqToEqv : {p, q : xs `Sub` ys} -> p = q -> p `Eqv` q
|
|
eqToEqv Refl = reflexive
|
|
|
|
|
|
export
|
|
getMask : SubView lte mask -> Subset Nat (Equal mask)
|
|
getMask (END Refl) = Element 0 Refl
|
|
getMask (KEEP v eq) = Element _ eq
|
|
getMask (DROP v eq) = Element _ eq
|
|
|
|
|
|
private
|
|
splitExEq : {0 f, g : a -> b} ->
|
|
(0 p : (x : a ** f x = g x)) -> Exists (\x => f x = g x)
|
|
splitExEq p = Evidence p.fst (irr p.snd)
|
|
where irr : forall a, b. (0 eq : a = b) -> a = b
|
|
irr Refl = Refl
|
|
|
|
private
|
|
0 lteNil2End : (p : [<] `Sub'` [<]) -> p = End
|
|
lteNil2End End = Refl
|
|
|
|
private
|
|
0 ltemEnd : SubView p n -> p = End -> n = 0
|
|
ltemEnd (END eq) Refl = eq
|
|
|
|
private
|
|
0 ltemEvenDrop : {p : xs `Sub'` (ys :< y)} ->
|
|
n = 2 * n' -> SubView p n -> (q ** p = Drop q)
|
|
ltemEvenDrop eq (KEEP _ eq') = absurd $ lsbMutex eq eq'
|
|
ltemEvenDrop eq (DROP {}) = (_ ** Refl)
|
|
|
|
private
|
|
0 fromDROP : {lte : xs `Sub'` ys :< z} -> n = 2 * n' -> lte = Drop lte' ->
|
|
SubView lte n -> SubView lte' n'
|
|
fromDROP eq Refl (DROP {n} p Refl) =
|
|
let eq = doubleInj eq {m = n, n = n'} in
|
|
rewrite sym eq in p
|
|
|
|
private
|
|
0 ltemOddKeep : {p : (xs :< x) `Sub'` (ys :< x)} -> {n' : Nat} ->
|
|
n = S (2 * n') -> SubView p n -> (q ** p = Keep q)
|
|
ltemOddKeep eq (KEEP {}) = (_ ** Refl)
|
|
ltemOddKeep eq (DROP _ eq') = absurd $ lsbMutex eq' eq
|
|
ltemOddKeep eq (END _) impossible
|
|
|
|
private
|
|
0 ltemOddLeft : {0 n, n' : Nat} -> {lte : xs `Sub'` ys :< z} ->
|
|
n = S (2 * n') -> SubView lte n ->
|
|
(xs' ** xs = xs' :< z)
|
|
ltemOddLeft eq {lte = Keep p} _ = (_ ** Refl)
|
|
ltemOddLeft eq {lte = Drop p} (DROP n' eq') = void $ lsbMutex eq' eq
|
|
|
|
private
|
|
0 fromKEEP : {lte : xs :< z `Sub'` ys :< z} ->
|
|
n = S (2 * n') -> lte = Keep lte' ->
|
|
SubView lte n -> SubView lte' n'
|
|
fromKEEP eq Refl (KEEP {n} p Refl) =
|
|
let eq = sDoubleInj eq {m = n, n = n'} in
|
|
rewrite sym eq in p
|
|
|
|
|
|
export
|
|
view : Length ys => (m : Sub xs ys) -> SubView m.lte m.mask
|
|
view @{Z} (SubM mask lte view0) with 0 (lteNilRight lte)
|
|
_ | Refl =
|
|
rewrite lteNil2End lte in
|
|
rewrite ltemEnd view0 (lteNil2End lte) in
|
|
END Refl
|
|
view @{S sy} (SubM mask lte view0) {ys = ys :< z} with (viewLsb mask)
|
|
_ | Lsb0 n eqn with (splitExEq $ ltemEvenDrop eqn view0)
|
|
_ | Evidence lte' eql =
|
|
rewrite eqn in rewrite eql in
|
|
DROP (fromDROP eqn eql view0) Refl
|
|
_ | Lsb1 n eqn with (splitExEq $ ltemOddLeft eqn view0)
|
|
_ | Evidence xs' Refl =
|
|
let Evidence q eqq = splitExEq $ ltemOddKeep eqn view0 in
|
|
rewrite eqn in rewrite eqq in
|
|
KEEP (fromKEEP eqn eqq view0) Refl
|
|
|
|
public export %inline
|
|
(.view) : Length ys => (m : Sub xs ys) -> SubView m.lte m.mask
|
|
(.view) = view
|
|
|
|
public export %inline
|
|
review : Length ys => {m : Nat} -> {0 lte : xs `Sub'` ys} ->
|
|
(0 _ : SubView lte m) -> SubView lte m
|
|
review v = view $ sub v
|
|
|
|
|
|
|
|
export
|
|
ltemLen : (sy : Length ys) => xs `Sub` ys -> length xs `LTE` sy.nat
|
|
ltemLen (SubM mask lte view0) {sy} with (review view0)
|
|
ltemLen (SubM _ _ _) | END eq = LTEZero
|
|
ltemLen (SubM _ _ _) {sy = S _} | KEEP v eq = LTESucc $ ltemLen $ sub v
|
|
ltemLen (SubM _ _ _) {sy = S _} | DROP v eq = lteSuccRight $ ltemLen $ sub v
|
|
|
|
export
|
|
ltemNilRight : xs `Sub` [<] -> xs = [<]
|
|
ltemNilRight m = irrelevantEq $ lteNilRight m.lte
|
|
|
|
|
|
export %inline
|
|
dropLast : Length ys => (xs :< x) `Sub` ys -> xs `Sub` ys
|
|
dropLast (SubM _ _ view0) @{sy} with (review view0)
|
|
dropLast (SubM _ _ _) | KEEP v _ = drop $ sub v
|
|
dropLast (SubM _ _ _) @{S _} | DROP v _ = drop $ dropLast $ sub v
|
|
|
|
|
|
export
|
|
Uninhabited (xs :< x `Sub` [<]) where
|
|
uninhabited sub = void $ uninhabited sub.lte
|
|
|
|
export
|
|
Length xs => Uninhabited (xs :< x `Sub` xs) where
|
|
uninhabited (SubM _ _ view0) @{sx} with (review view0)
|
|
uninhabited (SubM _ _ _) @{S _} | KEEP v _ = uninhabited $ sub v
|
|
uninhabited (SubM _ _ _) @{S _} | DROP v _ = uninhabited $ dropLast $ sub v
|
|
|
|
|
|
export
|
|
refl : Length xs => xs `Sub` xs
|
|
refl @{Z} = end
|
|
refl @{S s} = keep refl
|
|
|
|
export
|
|
0 reflLte : {sx : Length xs} -> (refl @{sx}).lte = refl' @{sx}
|
|
reflLte {sx = Z} = Refl
|
|
reflLte {sx = S s} = trans (keepLte _) $ cong Keep reflLte
|
|
|
|
public export %inline
|
|
Reflexive (Scope a) Sub where reflexive = refl
|
|
|
|
mutual
|
|
private
|
|
antisym_ : Length xs => Length ys =>
|
|
{0 p : xs `Sub'` ys} -> {0 q : ys `Sub'` xs} ->
|
|
SubView p m1 -> SubView q m2 -> xs = ys
|
|
antisym_ (END _) (END _) = Refl
|
|
antisym_ (KEEP v1 _) (KEEP v2 _ {z}) @{S sx} @{S sy} =
|
|
cong (:< z) $ antisym (SubM _ _ v1) (SubM _ _ v2)
|
|
antisym_ (KEEP {}) (DROP {}) {p = Keep p} {q = Drop q} =
|
|
void $ succNotLTEpred $ lteLen q `transitive` lteLen p
|
|
antisym_ (DROP {}) (KEEP {}) {p = Drop p} {q = Keep q} =
|
|
void $ succNotLTEpred $ lteLen p `transitive` lteLen q
|
|
antisym_ (DROP {}) (DROP {}) {p = Drop p} {q = Drop q} =
|
|
void $ succNotLTEpred $ lteLen p `transitive` lteSuccLeft (lteLen q)
|
|
|
|
export
|
|
antisym : Length xs => Length ys => xs `Sub` ys -> ys `Sub` xs -> xs = ys
|
|
antisym v1 v2 = antisym_ v1.view v2.view
|
|
|
|
public export %inline
|
|
Antisymmetric (Scope a) Sub where
|
|
antisymmetric p q = antisym p q
|
|
|
|
|
|
mutual
|
|
private
|
|
trans_ : Length ys => Length zs =>
|
|
{0 p : xs `Sub'` ys} -> {0 q : ys `Sub'` zs} ->
|
|
SubView p m1 -> SubView q m2 -> xs `Sub` zs
|
|
trans_ (END _) (END _) = end
|
|
trans_ (KEEP v1 _) (KEEP v2 _) @{S sy} @{S sz} = keep $ sub v1 `trans` sub v2
|
|
trans_ (DROP v1 _) (KEEP v2 _) @{S sy} @{S sz} = drop $ sub v1 `trans` sub v2
|
|
trans_ v1 (DROP v2 _) @{sy} @{S sz} =
|
|
let Element m1' eq = getMask v1 in
|
|
drop $ SubM m1' _ (rewrite sym eq in v1) `trans` sub v2
|
|
|
|
export
|
|
trans : Length ys => Length zs => xs `Sub` ys -> ys `Sub` zs -> xs `Sub` zs
|
|
trans p q = trans_ p.view q.view
|
|
|
|
public export %inline
|
|
(.) : Length ys => Length zs => ys `Sub` zs -> xs `Sub` ys -> xs `Sub` zs
|
|
(.) = flip trans
|
|
|
|
public export %inline
|
|
comp : Length ys => Length zs => ys `Sub` zs -> xs `Sub` ys -> xs `Sub` zs
|
|
comp = (.)
|
|
|
|
public export %inline
|
|
Transitive (Scope a) Sub where
|
|
transitive p q = q . p
|
|
|
|
|
|
public export
|
|
zero : Length xs => [<] `Sub` xs
|
|
zero @{Z} = end
|
|
zero @{S s} = drop zero
|
|
|
|
export
|
|
0 zeroLte : {sx : Length xs} -> (zero @{sx}).lte = zero' @{sx}
|
|
zeroLte {sx = Z} = Refl
|
|
zeroLte {sx = S s} = trans (dropLte zero) $ cong Drop zeroLte
|
|
|
|
public export
|
|
single : Length xs => x `Elem` xs -> [< x] `Sub` xs
|
|
single @{S sx} Here = keep zero
|
|
single @{S sx} (There p) = drop $ single p
|
|
|
|
export
|
|
0 singleLte : {sx : Length xs} -> (p : x `Elem` xs) ->
|
|
(single p @{sx}).lte = single' p @{sx}
|
|
singleLte {sx = S s} Here = trans (keepLte zero) $ cong Keep zeroLte
|
|
singleLte {sx = S s} (There p) = trans (dropLte _) $ cong Drop $ singleLte p
|
|
|
|
|
|
mutual
|
|
private
|
|
app0 : Length ys2 =>
|
|
(l : xs1 `Sub` ys1) ->
|
|
{rm : Nat} -> {0 rl : xs2 `Sub'` ys2} -> (rv : SubView rl rm) ->
|
|
(xs1 ++ xs2) `Sub` (ys1 ++ ys2)
|
|
app0 l (END eq) = l
|
|
app0 l (KEEP v Refl) @{S sy} = keep $ l ++ sub v
|
|
app0 l (DROP v Refl) @{S sy} = drop $ l ++ sub v
|
|
|
|
export
|
|
app : Length ys2 =>
|
|
xs1 `Sub` ys1 -> xs2 `Sub` ys2 -> (xs1 ++ xs2) `Sub` (ys1 ++ ys2)
|
|
app l r = app0 l r.view
|
|
|
|
public export %inline
|
|
(++) : Length ys2 =>
|
|
xs1 `Sub` ys1 -> xs2 `Sub` ys2 -> (xs1 ++ xs2) `Sub` (ys1 ++ ys2)
|
|
(++) = app
|
|
|
|
export
|
|
0 appLte : {sy : Length ys2} ->
|
|
(l : xs1 `Sub` ys1) -> (r : xs2 `Sub` ys2) ->
|
|
(app l r @{sy}).lte = app' l.lte r.lte
|
|
appLte l r@(SubM 0 End (END Refl)) =
|
|
cong (\v => (app0 l v).lte) (viewIrrel (view end) (END Refl))
|
|
appLte l r@(SubM (S (2 * n)) (Keep p) (KEEP v Refl)) {sy = S sy} =
|
|
trans (cong (\v => (app0 l v @{S sy}).lte) (viewIrrel _ (KEEP v Refl))) $
|
|
trans (keepLte _) $
|
|
cong Keep $ appLte l (sub v)
|
|
appLte l r@(SubM 0 (Drop p) (DROP {n = 0} v Refl)) {sy = S sy} =
|
|
trans (cong (\v => (app0 l v @{S sy}).lte) (viewIrrel _ (DROP v Refl))) $
|
|
trans (dropLte _) $
|
|
cong Drop $ appLte l (sub v)
|
|
appLte l r@(SubM (2 * S n) (Drop p) (DROP {n = S n} v Refl)) {sy = S sy} =
|
|
trans (cong (\v => (app0 l v @{S sy}).lte) (viewIrrel _ (DROP v Refl))) $
|
|
trans (dropLte _) $
|
|
cong Drop $ appLte l (sub v)
|
|
appLte {xs2 = _ :< _, ys2 = [<]} _ (SubM _ _ _) impossible
|
|
|
|
export
|
|
0 keepAppRight : {sy : Length ys2} ->
|
|
(l : xs1 `Sub` ys1) -> (r : xs2 `Sub` ys2) ->
|
|
(l ++ keep r) @{S sy} = keep ((l ++ r) @{sy})
|
|
keepAppRight l (SubM mask _ _) = rewrite (lsbOdd mask).snd in Refl
|
|
|
|
export
|
|
0 dropAppRight : (l : xs1 `Sub` ys1) -> (r : xs2 `Sub` ys2) ->
|
|
(l ++ drop r) @{S sy} = drop ((l ++ r) @{sy})
|
|
dropAppRight l r = lteEq $
|
|
trans (appLte l (drop r)) $
|
|
trans (cong (app' l.lte) (dropLte r)) $
|
|
trans (cong Drop (sym (appLte l r))) $
|
|
sym $ dropLte (l ++ r)
|
|
|
|
|
|
export
|
|
0 endRight : {xs, ys : Scope a} -> (sub : xs `Sub` ys) -> sub = (sub ++ Sub.end)
|
|
endRight sub = Refl
|
|
|
|
|
|
private
|
|
0 transDrop_ : {p : xs `Sub'` ys} -> {q : ys `Sub'` zs} ->
|
|
(pv : SubView p m1) -> (qv : SubView q m2) ->
|
|
trans_ pv (DROP qv qe) @{sy} @{S sz} =
|
|
drop (trans_ pv qv @{sy} @{sz})
|
|
transDrop_ {sy = Z} {sz = sz} (END Refl) qv =
|
|
cong (\v => drop $ trans_ {m2, q} (END Refl) v) $ viewIrrel {}
|
|
transDrop_ {sy = S sy} {sz = sz} (KEEP pv Refl) qv {p = Keep p} =
|
|
cong2 (\x, y => drop (trans_ @{S sy} x y)) (viewIrrel {}) (viewIrrel {})
|
|
transDrop_ {sy = S sy} {sz = S sz} (DROP pv Refl) qv =
|
|
cong2 (\x, y => drop (trans_ @{S sy} @{S sz} x y))
|
|
(viewIrrel {}) (viewIrrel {})
|
|
transDrop_ {ys = _ :< _, zs = [<]} _ _ impossible
|
|
|
|
private
|
|
0 transLte_ : {p : xs `Sub'` ys} -> {q : ys `Sub'` zs} ->
|
|
(pv : SubView p m1) -> (qv : SubView q m2) ->
|
|
(trans_ pv qv @{sy} @{sz}).lte = trans' p q
|
|
transLte_ (END _) (END _) = Refl
|
|
transLte_ (KEEP pv pe) (KEEP qv qe) {sy = S _} {sz = S _} =
|
|
trans (keepLte _) $ cong Keep $ transLte_ {}
|
|
transLte_ (DROP pv pe) (KEEP qv qe) {sy = S _} {sz = S _} =
|
|
trans (dropLte _) $ cong Drop $ transLte_ {}
|
|
transLte_ pv (DROP qv qe) {sz = S _} =
|
|
trans (cong lte $ transDrop_ pv qv) $
|
|
trans (dropLte _) $ cong Drop $ transLte_ pv qv
|
|
transLte_ {ys = _ :< _, zs = [<]} _ _ impossible
|
|
|
|
export
|
|
0 transLte : {sy : Length ys} -> {sz : Length zs} ->
|
|
(p : xs `Sub` ys) -> (q : ys `Sub` zs) ->
|
|
(trans p q @{sy} @{sz}).lte = trans' p.lte q.lte
|
|
transLte p q = transLte_ p.view q.view
|
|
|
|
public export
|
|
0 compLte : {sy : Length ys} -> {sz : Length zs} ->
|
|
(q : ys `Sub` zs) -> (p : xs `Sub` ys) ->
|
|
((q . p) @{sy} @{sz}).lte = q.lte . p.lte
|
|
compLte q p = transLte p q
|
|
|
|
|
|
||| if `p` holds for all elements of the main list,
|
|
||| it holds for all elements of the sublist
|
|
export
|
|
subAll : Length ys => xs `Sub` ys -> All prop ys -> All prop xs
|
|
subAll (SubM _ _ v) ps @{sy} with (review v)
|
|
subAll (SubM _ _ _) [<] | END _ = [<]
|
|
subAll (SubM _ _ _) (ps :< p) @{S sy} | KEEP v _ = subAll (sub v) ps :< p
|
|
subAll (SubM _ _ _) (ps :< p) @{S sy} | DROP v _ = subAll (sub v) ps
|
|
|
|
|
|
||| if `p` holds for one element of the sublist,
|
|
||| it holds for one element of the main list
|
|
export
|
|
subAny : Length ys => xs `Sub` ys -> Any prop xs -> Any prop ys
|
|
subAny (SubM _ _ v) p @{sy} with (review v)
|
|
subAny (SubM _ _ _) (Here p) | KEEP v _ = Here p
|
|
subAny (SubM _ _ _) (There p) @{S sy} | KEEP v _ = There $ subAny (sub v) p
|
|
subAny (SubM _ _ _) p @{S sy} | DROP v _ = There $ subAny (sub v) p
|