129 lines
4.7 KiB
Idris
129 lines
4.7 KiB
Idris
|
module Quox.Thin.Eqv
|
||
|
|
|
||
|
|
import public Quox.Thin.Base
|
||
|
|
import public Quox.Thin.View
|
||
|
|
import Quox.NatExtra
|
||
|
|
import Syntax.PreorderReasoning
|
||
|
|
|
||
|
|
%default total
|
||
|
|
|
||
|
|
infix 6 `Eqv`
|
||
|
|
|
||
|
|
private
|
||
|
|
uip : (p, q : a = b) -> p = q
|
||
|
|
uip Refl Refl = Refl
|
||
|
|
|
||
|
|
|
||
|
|
public export
|
||
|
|
data Eqv : OPE m1 n1 mask1 -> OPE m2 n2 mask2 -> Type where
|
||
|
|
EqvStop : Eqv Stop Stop
|
||
|
|
EqvDrop : {0 p : OPE m1 n1 mask1} ->
|
||
|
|
{0 q : OPE m2 n2 mask2} ->
|
||
|
|
Eqv p q -> Eqv (Drop p eq1) (Drop q eq2)
|
||
|
|
EqvKeep : {0 p : OPE m1 n1 mask1} ->
|
||
|
|
{0 q : OPE m2 n2 mask2} ->
|
||
|
|
Eqv p q -> Eqv (Keep p eq1) (Keep q eq2)
|
||
|
|
%name Eqv eqv
|
||
|
|
|
||
|
|
export Uninhabited (Stop `Eqv` Drop p e) where uninhabited _ impossible
|
||
|
|
export Uninhabited (Stop `Eqv` Keep p e) where uninhabited _ impossible
|
||
|
|
export Uninhabited (Drop p e `Eqv` Stop) where uninhabited _ impossible
|
||
|
|
export Uninhabited (Drop p e `Eqv` Keep q f) where uninhabited _ impossible
|
||
|
|
export Uninhabited (Keep p e `Eqv` Stop) where uninhabited _ impossible
|
||
|
|
export Uninhabited (Keep p e `Eqv` Drop q f) where uninhabited _ impossible
|
||
|
|
|
||
|
|
export
|
||
|
|
Reflexive (OPE m n mask) Eqv where
|
||
|
|
reflexive {x = Stop} = EqvStop
|
||
|
|
reflexive {x = Drop {}} = EqvDrop reflexive
|
||
|
|
reflexive {x = Keep {}} = EqvKeep reflexive
|
||
|
|
|
||
|
|
export
|
||
|
|
symmetric : p `Eqv` q -> q `Eqv` p
|
||
|
|
symmetric EqvStop = EqvStop
|
||
|
|
symmetric (EqvDrop eqv) = EqvDrop $ symmetric eqv
|
||
|
|
symmetric (EqvKeep eqv) = EqvKeep $ symmetric eqv
|
||
|
|
|
||
|
|
export
|
||
|
|
transitive : p `Eqv` q -> q `Eqv` r -> p `Eqv` r
|
||
|
|
transitive EqvStop EqvStop = EqvStop
|
||
|
|
transitive (EqvDrop eqv1) (EqvDrop eqv2) = EqvDrop (transitive eqv1 eqv2)
|
||
|
|
transitive (EqvKeep eqv1) (EqvKeep eqv2) = EqvKeep (transitive eqv1 eqv2)
|
||
|
|
|
||
|
|
|
||
|
|
private
|
||
|
|
recompute' : {mask1, mask2, n1, n2 : Nat} ->
|
||
|
|
(0 p : OPE m1 n1 mask1) -> (0 q : OPE m2 n2 mask2) ->
|
||
|
|
(0 eqv : p `Eqv` q) -> p `Eqv` q
|
||
|
|
recompute' p q eqv with %syntactic (view p) | (view q)
|
||
|
|
recompute' Stop Stop _ | StopV | StopV = EqvStop
|
||
|
|
recompute' (Drop p _) (Drop q _) eqv | DropV _ p | DropV _ q =
|
||
|
|
EqvDrop $ recompute' {eqv = let EqvDrop e = eqv in e, _}
|
||
|
|
recompute' (Keep p _) (Keep q _) eqv | KeepV _ p | KeepV _ q =
|
||
|
|
EqvKeep $ recompute' {eqv = let EqvKeep e = eqv in e, _}
|
||
|
|
recompute' (Drop p _) (Keep q _) eqv | DropV _ p | KeepV _ q =
|
||
|
|
void $ absurd eqv
|
||
|
|
recompute' (Keep p _) (Drop q _) eqv | KeepV _ p | DropV _ q =
|
||
|
|
void $ absurd eqv
|
||
|
|
|
||
|
|
private
|
||
|
|
recompute : {mask1, mask2, n1, n2 : Nat} ->
|
||
|
|
{0 p : OPE m1 n1 mask1} -> {0 q : OPE m2 n2 mask2} ->
|
||
|
|
(0 _ : p `Eqv` q) -> p `Eqv` q
|
||
|
|
recompute eqv = recompute' {eqv, _}
|
||
|
|
|
||
|
|
|
||
|
|
export
|
||
|
|
eqvIndices : {0 p : OPE m1 n1 mask1} -> {0 q : OPE m2 n2 mask2} ->
|
||
|
|
p `Eqv` q -> (m1 = m2, n1 = n2, mask1 = mask2)
|
||
|
|
eqvIndices EqvStop = (Refl, Refl, Refl)
|
||
|
|
eqvIndices (EqvDrop eqv {eq1 = Refl, eq2 = Refl}) =
|
||
|
|
let (Refl, Refl, Refl) = eqvIndices eqv in (Refl, Refl, Refl)
|
||
|
|
eqvIndices (EqvKeep eqv {eq1 = Refl, eq2 = Refl}) =
|
||
|
|
let (Refl, Refl, Refl) = eqvIndices eqv in (Refl, Refl, Refl)
|
||
|
|
|
||
|
|
export
|
||
|
|
0 eqvMask : (p : OPE m1 n mask1) -> (q : OPE m2 n mask2) ->
|
||
|
|
mask1 = mask2 -> p `Eqv` q
|
||
|
|
eqvMask Stop Stop _ = EqvStop
|
||
|
|
eqvMask (Drop ope1 Refl) (Drop {mask = mm2} ope2 eq2) Refl =
|
||
|
|
EqvDrop $ eqvMask ope1 ope2 (doubleInj _ _ eq2)
|
||
|
|
eqvMask (Drop ope1 Refl) (Keep ope2 eq2) Refl =
|
||
|
|
void $ notEvenOdd _ _ eq2
|
||
|
|
eqvMask (Keep ope1 eq1) (Keep ope2 eq2) Refl =
|
||
|
|
EqvKeep $ eqvMask ope1 ope2 (doubleInj _ _ $ inj S $ trans (sym eq1) eq2)
|
||
|
|
eqvMask (Keep ope1 eq1) (Drop ope2 eq2) Refl =
|
||
|
|
void $ notEvenOdd _ _ $ trans (sym eq2) eq1
|
||
|
|
|
||
|
|
export
|
||
|
|
0 eqvEq : (p, q : OPE m n mask) -> p `Eqv` q -> p === q
|
||
|
|
eqvEq Stop Stop EqvStop = Refl
|
||
|
|
eqvEq (Drop p eq1) (Drop q eq2) (EqvDrop eqv)
|
||
|
|
with %syntactic (doubleInj _ _ $ trans (sym eq1) eq2)
|
||
|
|
_ | Refl = cong2 Drop (eqvEq p q eqv) (uip eq1 eq2)
|
||
|
|
eqvEq (Keep p eq1) (Keep q eq2) (EqvKeep eqv)
|
||
|
|
with %syntactic (doubleInj _ _ $ inj S $ trans (sym eq1) eq2)
|
||
|
|
_ | Refl = cong2 Keep (eqvEq p q eqv) (uip eq1 eq2)
|
||
|
|
|
||
|
|
export
|
||
|
|
0 eqvEq' : (p : OPE m1 n1 mask1) -> (q : OPE m2 n2 mask2) ->
|
||
|
|
p `Eqv` q -> p ~=~ q
|
||
|
|
eqvEq' p q eqv = let (Refl, Refl, Refl) = eqvIndices eqv in eqvEq p q eqv
|
||
|
|
|
||
|
|
export
|
||
|
|
0 maskEqInner : (0 ope1 : OPE m1 n mask1) -> (0 ope2 : OPE m2 n mask2) ->
|
||
|
|
mask1 = mask2 -> m1 = m2
|
||
|
|
maskEqInner Stop Stop _ = Refl
|
||
|
|
maskEqInner (Drop ope1 Refl) (Drop ope2 Refl) eq =
|
||
|
|
maskEqInner ope1 ope2 (doubleInj _ _ eq)
|
||
|
|
maskEqInner (Keep ope1 Refl) (Keep ope2 Refl) eq =
|
||
|
|
cong S $ maskEqInner ope1 ope2 $ doubleInj _ _ $ inj S eq
|
||
|
|
maskEqInner (Drop ope1 Refl) (Keep ope2 Refl) eq = void $ notEvenOdd _ _ eq
|
||
|
|
maskEqInner (Keep {mask = mask1'} ope1 eq1) (Drop {mask = mask2'} ope2 eq2) eq =
|
||
|
|
-- matching on eq1, eq2, or eq here triggers that weird coverage bug ☹
|
||
|
|
void $ notEvenOdd _ _ $ Calc $
|
||
|
|
|~ mask2' + mask2'
|
||
|
|
~~ mask2 ..<(eq2)
|
||
|
|
~~ mask1 ..<(eq)
|
||
|
|
~~ S (mask1' + mask1') ...(eq1)
|