diff options
Diffstat (limited to 'src/Data/Term/Property.idr')
| -rw-r--r-- | src/Data/Term/Property.idr | 174 |
1 files changed, 136 insertions, 38 deletions
diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr index 2de450f..62f4caa 100644 --- a/src/Data/Term/Property.idr +++ b/src/Data/Term/Property.idr @@ -16,7 +16,7 @@ public export record Property (sig : Signature) (k : Nat) where constructor MkProp 0 Prop : forall n. (Fin k -> Term sig n) -> Type - cong : forall n. {f, g : Fin k -> Term sig n} -> f .=. g -> Prop f -> Prop g + cong : forall n. (f, g : Fin k -> Term sig n) -> f .=. g -> Prop f -> Prop g %name Property p, q @@ -26,7 +26,7 @@ public export Unifies : Term sig k -> Term sig k -> Property sig k Unifies t u = MkProp { Prop = \f => f <$> t = f <$> u - , cong = \cong, prf => Calc $ + , cong = \_, _, cong, prf => Calc $ |~ _ <$> t ~~ _ <$> t ..<(subExtensional cong t) ~~ _ <$> u ...(prf) @@ -35,7 +35,7 @@ Unifies t u = MkProp public export All : Vect n (Property sig k) -> Property sig k -All ps = MkProp (\f => All (\p => p.Prop f) ps) (\cong => mapRel (\p => p.cong cong)) +All ps = MkProp (\f => All (\p => p.Prop f) ps) (\f, g, cong => mapRel (\p => p.cong f g cong)) public export UnifiesAll : Vect n (Term sig k) -> Vect n (Term sig k) -> Property sig k @@ -111,7 +111,7 @@ public export Extension : Property sig k -> (Fin k -> Term sig n) -> Property sig n Extension p f = MkProp { Prop = \g => p.Prop (g . f) - , cong = \prf => p.cong (\i => subExtensional prf (f i)) + , cong = \g, h, prf => p.cong (g . f) (h . f) (\i => subExtensional prf (f i)) } -- Properties @@ -128,8 +128,8 @@ extendCong2 : p <=> q -> Extension p f <=> Extension q g extendCong2 prf1 prf2 = MkEquivalence - (\h, x => prf2.leftToRight (h . g) $ p.cong (\i => cong (h <$>) $ prf1 i) x) - (\h, x => prf2.rightToLeft (h . f) $ q.cong (\i => sym $ cong (h <$>) $ prf1 i) x) + (\h, x => prf2.leftToRight (h . g) $ p.cong _ _ (\i => cong (h <$>) $ prf1 i) x) + (\h, x => prf2.rightToLeft (h . f) $ q.cong _ _ (\i => sym $ cong (h <$>) $ prf1 i) x) export extendCong : @@ -152,8 +152,8 @@ extendAssoc : Extension (Extension p f) g <=> Extension p (g . f) extendAssoc p f g = MkEquivalence - (\h => p.cong (\i => subAssoc h g (f i))) - (\h => p.cong (\i => sym $ subAssoc h g (f i))) + (\h => p.cong _ _ (\i => subAssoc h g (f i))) + (\h => p.cong _ _ (\i => sym $ subAssoc h g (f i))) export extendUnify : @@ -253,25 +253,78 @@ lteExtend : (prf : f <= g) -> p.Prop f -> (Extension p g).Prop prf.sub -lteExtend prf x = p.cong prf.prf x +lteExtend prf x = p.cong _ _ prf.prf x -- Most General ---------------------------------------------------------------- --- public export --- record MostGeneral (p : Property sig k) where +public export +record MostGeneral (p : Property sig k) (f : Fin k -> Term sig n) where + constructor MkMostGeneral + valid : p.Prop f + universal : forall j. (g : Fin k -> Term sig j) -> p.Prop g -> Fin n -> Term sig j + factors : + forall j. + (g : Fin k -> Term sig j) -> + (v : p.Prop g) -> + g .=. universal g v . f + unique : + forall j. + (g : Fin k -> Term sig j) -> + (v : p.Prop g) -> + (h : Fin n -> Term sig j) -> + g .=. h . f -> + h .=. universal g v + +%name MostGeneral mg + +export +varMostGeneral : p.Prop Var -> MostGeneral p Var +varMostGeneral v = + MkMostGeneral + { valid = v + , universal = \g, _ => g + , factors = \g, _, x => Refl + , unique = \g, _, h, prf', x => sym $ prf' x + } public export Max : Property sig k -> Property sig k Max p = MkProp - { Prop = \f => (p.Prop f, forall n. (g : Fin k -> Term sig n) -> p.Prop g -> g <= f) - , cong = \cong, (x, max) => (p.cong cong x, \g, y => lteCong (\_ => Refl) cong (max g y)) + { Prop = MostGeneral p + , cong = \f, g, prf, mg => + MkMostGeneral + { valid = p.cong f g prf mg.valid + , universal = mg.universal + , factors = \h, v, x => Calc $ + |~ h x + ~~ mg.universal h v <$> f x ...(mg.factors h v x) + ~~ mg.universal h v <$> g x ...(compCongR (mg.universal h v) prf x) + , unique = \h, v, i, prf' => + mg.unique h v i $ + \x => Calc $ + |~ h x + ~~ i <$> g x ...(prf' x) + ~~ i <$> f x ...(compCongR i (\x => sym $ prf x) x) + } } export maxCong : p <=> q -> Max p <=> Max q maxCong prf = MkEquivalence - { leftToRight = \f, (x, max) => (prf.leftToRight f x, \g, y => max g (prf.rightToLeft g y)) - , rightToLeft = \f, (x, max) => (prf.rightToLeft f x, \g, y => max g (prf.leftToRight g y)) + { leftToRight = \f, mg => + MkMostGeneral + { valid = prf.leftToRight f mg.valid + , universal = \g, v => mg.universal g (prf.rightToLeft g v) + , factors = \g, v => mg.factors g (prf.rightToLeft g v) + , unique = \g, v => mg.unique g (prf.rightToLeft g v) + } + , rightToLeft = \f, mg => + MkMostGeneral + { valid = prf.rightToLeft f mg.valid + , universal = \g, v => mg.universal g (prf.leftToRight g v) + , factors = \g, v => mg.factors g (prf.leftToRight g v) + , unique = \g, v => mg.unique g (prf.leftToRight g v) + } } -- Downward Closed ------------------------------------------------------------- @@ -306,26 +359,66 @@ optimistLemma : {f : Fin k -> Term sig m} -> {g : Fin m -> Term sig n} -> DClosed p -> - (Max (Extension p a)).Prop f -> - (Max (Extension (All ps) (f . a))).Prop g -> - (Max (Extension (All (p :: ps)) a)).Prop (g . f) -optimistLemma prf (x, max1) (y, max2) = - ( ( prf.closed ((g . f) . a) (f . a) (compLte (MkLte g (\i => Refl)) a) x - :: (All ps).cong (\i => sym $ subAssoc g f (a i)) y - ) - , \h, (x' :: y') => - let prf1 = max1 h x' in - let y'' = (All ps).cong (\i => trans (subExtensional prf1.prf (a i)) (subAssoc prf1.sub f (a i))) y' in - let prf2 = max2 prf1.sub y'' in - MkLte - { sub = prf2.sub - , prf = \i => Calc $ - |~ h i - ~~ prf1.sub <$> f i ...(prf1.prf i) - ~~ (prf2.sub . g) <$> f i ...(subExtensional (prf2.prf) (f i)) - ~~ prf2.sub <$> (g <$> f i) ...(subAssoc prf2.sub g (f i)) - } - ) + (MostGeneral (Extension p a)) f -> + (MostGeneral (Extension (All ps) (f . a))) g -> + (MostGeneral (Extension (All (p :: ps)) a)) (g . f) +optimistLemma closed mg mg' = + MkMostGeneral + { valid = + closed.closed ((g . f) . a) (f . a) (compLte (MkLte g (\i => Refl)) a) mg.valid :: + (All ps).cong _ _ (\i => sym $ subAssoc g f (a i)) mg'.valid + , universal = universal + , factors = factors + , unique = unique + } + where + coerce : + forall i. + (h : Fin k -> Term sig i) -> + (v : (Extension p a).Prop h) -> + (Extension (All ps) a).Prop h -> + (Extension (All ps) (f . a)).Prop (mg.universal h v) + coerce h v = + (All ps).cong _ _ + (\x => Calc $ + |~ h <$> a x + ~~ mg.universal h v . f <$> a x ...(subExtensional (mg.factors h v) (a x)) + ~~ mg.universal h v <$> f <$> a x ...(subAssoc (mg.universal h v) f (a x))) + universal : + forall i. + (h : Fin k -> Term sig i) -> + (vs : (Extension (All (p :: ps)) a).Prop h) -> + Fin n -> Term sig i + universal h (v :: vs) = + mg'.universal (mg.universal h v) (coerce h v vs) + + factors : + forall i. + (h : Fin k -> Term sig i) -> + (vs : (Extension (All (p :: ps)) a).Prop h) -> + h .=. universal h vs . (g . f) + factors h (v :: vs) x = Calc $ + |~ h x + ~~ mg.universal h v <$> f x ...(mg.factors h v x) + ~~ mg'.universal (mg.universal h v) (coerce h v vs) . g <$> f x ...(subExtensional (mg'.factors (mg.universal h v) (coerce h v vs)) (f x)) + ~~ mg'.universal (mg.universal h v) (coerce h v vs) <$> g <$> f x ...(subAssoc (mg'.universal (mg.universal h v) (coerce h v vs)) g (f x)) + + unique : + forall i. + (h : Fin k -> Term sig i) -> + (vs : (Extension (All (p :: ps)) a).Prop h) -> + (r : Fin n -> Term sig i) -> + h .=. r . (g . f) -> + r .=. universal h vs + unique h (v :: vs) r prf = + mg'.unique (mg.universal h v) (coerce h v vs) r $ + \x => sym $ + mg.unique h v (r . g) + (\x => Calc $ + |~ h x + ~~ r <$> g <$> f x ...(prf x) + ~~ r . g <$> f x ..<(subAssoc r g (f x))) + x export failHead : Nothing (Extension p a) -> Nothing (Extension (All (p :: ps)) a) @@ -339,6 +432,11 @@ failTail : (Max (Extension p a)).Prop f -> Nothing (Extension (All ps) (f . a)) -> Nothing (Extension (All (p :: ps)) a) -failTail (x, max) absurd g (y :: ys) = - let prf = max g y in - absurd prf.sub $ (All ps).cong (compLte prf a).prf ys +failTail mg absurd g (v :: vs) = + absurd (mg.universal g v) $ + (All ps).cong _ _ + (\x => Calc $ + |~ g <$> a x + ~~ mg.universal g v . f <$> a x ...(subExtensional (mg.factors g v) (a x)) + ~~ mg.universal g v <$> f <$> a x ...(subAssoc (mg.universal g v) f (a x))) + vs |