diff options
| -rw-r--r-- | soat.ipkg | 1 | ||||
| -rw-r--r-- | src/Data/Morphism/Indexed.idr | 8 | ||||
| -rw-r--r-- | src/Data/Setoid/Indexed.idr | 7 | ||||
| -rw-r--r-- | src/Soat/FirstOrder/Algebra.idr | 8 | ||||
| -rw-r--r-- | src/Soat/FirstOrder/Algebra/Coproduct.idr | 118 | ||||
| -rw-r--r-- | src/Soat/FirstOrder/Algebra/FreeExtension.idr | 58 | ||||
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 118 | ||||
| -rw-r--r-- | src/Soat/SecondOrder/Algebra.idr | 26 | ||||
| -rw-r--r-- | src/Soat/SecondOrder/Algebra/Lift.idr | 553 |
9 files changed, 583 insertions, 314 deletions
@@ -10,6 +10,7 @@ modules = Data.Morphism.Indexed , Soat.Data.Sublist , Soat.FirstOrder.Algebra , Soat.FirstOrder.Algebra.Coproduct + , Soat.FirstOrder.Algebra.FreeExtension , Soat.FirstOrder.Signature , Soat.FirstOrder.Term , Soat.SecondOrder.Algebra diff --git a/src/Data/Morphism/Indexed.idr b/src/Data/Morphism/Indexed.idr index c271c90..6737275 100644 --- a/src/Data/Morphism/Indexed.idr +++ b/src/Data/Morphism/Indexed.idr @@ -11,3 +11,11 @@ record IFunction {a : Type} (x, y : ISetoid a) where constructor MkIFunction func : IFunc x.U y.U cong : (i : a) -> {u, v : x.U i} -> x.relation i u v -> y.relation i (func i u) (func i v) + +public export +ifunc : IFunc x y -> IFunction (isetoid x) (isetoid y) +ifunc f = MkIFunction f (\i => cong (f i)) + +public export +compFunc : IFunction b c -> IFunction a b -> IFunction a c +compFunc f g = MkIFunction (\i => f.func i . g.func i) (\i => f.cong i . g.cong i) diff --git a/src/Data/Setoid/Indexed.idr b/src/Data/Setoid/Indexed.idr index 7277932..db5fb07 100644 --- a/src/Data/Setoid/Indexed.idr +++ b/src/Data/Setoid/Indexed.idr @@ -40,5 +40,12 @@ public export (.index) x i = MkSetoid (x.U i) (x.relation i) (x.equivalence i) public export +(.reindex) : ISetoid b -> (f : a -> b) -> ISetoid a +(.reindex) x f = MkISetoid + (\i => x.U $ f i) + (\i => x.relation $ f i) + (\i => x.equivalence $ f i) + +public export isetoid : (a -> Type) -> ISetoid a isetoid u = MkISetoid u (\_ => Equal) (\_ => equiv) diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr index 245af6d..26370cc 100644 --- a/src/Soat/FirstOrder/Algebra.idr +++ b/src/Soat/FirstOrder/Algebra.idr @@ -104,3 +104,11 @@ compIsHomo fHomo gHomo = MkIsHomomorphism public export compHomo : {a, b, c : Algebra sig} -> Homomorphism b c -> Homomorphism a b -> Homomorphism a c compHomo f g = MkHomomorphism _ $ compIsHomo f.homo g.homo + +public export +record Isomorphism {0 sig : Signature} (a, b : Algebra sig) where + constructor MkIsomorphism + to : Homomorphism a b + from : Homomorphism b a + fromTo : {t : sig.T} -> (x : a.raw.U t) -> a.relation t (from.func t $ to.func t x) x + toFrom : {t : sig.T} -> (x : b.raw.U t) -> b.relation t (to.func t $ from.func t x) x diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr index d0b1b14..a29080f 100644 --- a/src/Soat/FirstOrder/Algebra/Coproduct.idr +++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr @@ -73,14 +73,13 @@ Coproduct x y = MakeRawAlgebra } public export -CoproductIsAlgebra : IsAlgebra sig x rel -> IsAlgebra sig y rel' - -> IsAlgebra sig (Coproduct x y) - ((~=~) (MkRawAlgebraWithRelation x rel) (MkRawAlgebraWithRelation y rel')) -CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra +CoproductIsAlgebra : (x, y : Algebra sig) + -> IsAlgebra sig (Coproduct x.raw y.raw) ((~=~) x.rawWithRelation y.rawWithRelation) +CoproductIsAlgebra x y = MkIsAlgebra { equivalence = \t => MkEquivalence { refl = MkReflexive $ coprodRelRefl - (\t => (xIsAlgebra.equivalence t).refl) - (\t => (yIsAlgebra.equivalence t).refl) + (\t => (x.algebra.equivalence t).refl) + (\t => (y.algebra.equivalence t).refl) _ , sym = MkSymmetric $ Sym , trans = MkTransitive $ Trans @@ -90,44 +89,88 @@ CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra public export CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig -CoproductAlgebra x y = MkAlgebra _ _ $ CoproductIsAlgebra x.algebra y.algebra - -public export -injectLIsHomo : IsHomomorphism x (CoproductAlgebra x y) (\_ => Done . Left) -injectLIsHomo = MkIsHomomorphism - { cong = \_ => DoneL - , semHomo = InjectL - } - -public export -injectRIsHomo : IsHomomorphism y (CoproductAlgebra x y) (\_ => Done . Right) -injectRIsHomo = MkIsHomomorphism - { cong = \_ => DoneR - , semHomo = InjectR - } +CoproductAlgebra x y = MkAlgebra _ _ $ CoproductIsAlgebra x y public export injectLHomo : Homomorphism x (CoproductAlgebra x y) -injectLHomo = MkHomomorphism _ $ injectLIsHomo +injectLHomo = MkHomomorphism _ $ MkIsHomomorphism { cong = \_ => DoneL , semHomo = InjectL } public export injectRHomo : Homomorphism y (CoproductAlgebra x y) -injectRHomo = MkHomomorphism _ $ injectRIsHomo +injectRHomo = MkHomomorphism _ $ MkIsHomomorphism { cong = \_ => DoneR , semHomo = InjectR } public export coproduct : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> IFunc (CoproductSet sig x y) z.U -coproduct f g _ = bindTerm (\i => either (f i) (g i)) +coproduct f g = bindTerm (\i => either (f i) (g i)) public export coproducts : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> (ts : _) -> CoproductSet sig x y ^ ts -> z.U ^ ts -coproducts f g _ = bindTerms (\i => either (f i) (g i)) +coproducts f g = bindTerms (\i => either (f i) (g i)) + +public export +coproductCong' : {x, y, z : Algebra sig} + -> (f, f' : Homomorphism x z) -> (g, g' : Homomorphism y z) + -> (congL : (t : _) -> {i, j : x.raw.U t} -> x.relation t i j + -> z.relation t (f.func t i) (f'.func t j)) + -> (congR : (t : _) -> {i, j : y.raw.U t} -> y.relation t i j + -> z.relation t (g.func t i) (g'.func t j)) + -> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawWithRelation y.rawWithRelation t tm tm' + -> z.relation t + (coproduct {z = z.raw} f.func g.func t tm) + (coproduct {z = z.raw} f'.func g'.func t tm') + +public export +coproductsCong' : {x, y, z : Algebra sig} + -> (f, f' : Homomorphism x z) -> (g, g' : Homomorphism y z) + -> (congL : (t : _) -> {i, j : x.raw.U t} -> x.relation t i j + -> z.relation t (f.func t i) (f'.func t j)) + -> (congR : (t : _) -> {i, j : y.raw.U t} -> y.relation t i j + -> z.relation t (g.func t i) (g'.func t j)) + -> (ts : List sig.T) -> {tms, tms' : _ ^ ts} + -> Pointwise ((~=~) x.rawWithRelation y.rawWithRelation) tms tms' + -> Pointwise z.relation + (coproducts {z = z.raw} f.func g.func ts tms) + (coproducts {z = z.raw} f'.func g'.func ts tms') + +coproductCong' f f' g g' congL congR _ (DoneL eq) = congL _ eq +coproductCong' f f' g g' congL congR _ (DoneR eq) = congR _ eq +coproductCong' f f' g g' congL congR _ (Call op eqs) = + z.algebra.semCong op $ + coproductsCong' f f' g g' congL congR _ eqs +coproductCong' f f' g g' congL congR _ (InjectL op ts) = CalcWith (z.setoid.index _) $ + |~ f.func _ (x.raw.sem op ts) + ~~ f'.func _ (x.raw.sem op ts) ...(congL _ $ (x.algebra.equivalence _).reflexive {x = x.raw.sem op ts}) + ~~ z.raw.sem op (map f'.func ts) ...(f'.homo.semHomo op ts) + ~~ z.raw.sem op (map (coproduct f'.func g'.func) (map (\_ => Done . Left) ts)) .=.(cong (z.raw.sem op) $ mapComp ts) + ~~ z.raw.sem op (coproducts f'.func g'.func _ (map (\_ => Done . Left) ts)) .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _) +coproductCong' f f' g g' congL congR _ (InjectR op ts) = CalcWith (z.setoid.index _) $ + |~ g.func _ (y.raw.sem op ts) + ~~ g'.func _ (y.raw.sem op ts) ...(congR _ $ (y.algebra.equivalence _).reflexive {x = y.raw.sem op ts}) + ~~ z.raw.sem op (map g'.func ts) ...(g'.homo.semHomo op ts) + ~~ z.raw.sem op (map (coproduct f'.func g'.func) (map (\_ => Done . Right) ts)) .=.(cong (z.raw.sem op) $ mapComp ts) + ~~ z.raw.sem op (coproducts f'.func g'.func _ (map (\_ => Done . Right) ts)) .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _) +coproductCong' f f' g g' congL congR _ (Sym eq) = + (z.algebra.equivalence _).symmetric $ + coproductCong' f' f g' g + (\t => (z.algebra.equivalence t).symmetric . congL t . (x.algebra.equivalence t).symmetric) + (\t => (z.algebra.equivalence t).symmetric . congR t . (y.algebra.equivalence t).symmetric) + _ + eq +coproductCong' f f' g g' congL congR _ (Trans eq eq') = (z.algebra.equivalence _).transitive + (coproductCong' f f g g f.homo.cong g.homo.cong _ eq) + (coproductCong' f f' g g' congL congR _ eq') + +coproductsCong' f f' g g' congL congR _ [] = [] +coproductsCong' f f' g g' congL congR _ (eq :: eqs) = + coproductCong' f f' g g' congL congR _ eq :: coproductsCong' f f' g g' congL congR _ eqs public export coproductCong : {x, y, z : Algebra sig} -> (f : Homomorphism x z) -> (g : Homomorphism y z) -> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawWithRelation y.rawWithRelation t tm tm' -> (z.relation t `on` coproduct {z = z.raw} f.func g.func t) tm tm' +coproductCong f g = coproductCong' f f g g f.homo.cong g.homo.cong public export coproductsCong : {x, y, z : Algebra sig} @@ -135,30 +178,7 @@ coproductsCong : {x, y, z : Algebra sig} -> (ts : List sig.T) -> {tms, tms' : _ ^ ts} -> Pointwise ((~=~) x.rawWithRelation y.rawWithRelation) tms tms' -> (Pointwise z.relation `on` (coproducts {z = z.raw} f.func g.func ts)) tms tms' - -coproductCong f g _ (DoneL eq) = f.homo.cong _ eq -coproductCong f g _ (DoneR eq) = g.homo.cong _ eq -coproductCong f g _ (Call op eqs) = - z.algebra.semCong op $ - coproductsCong f g _ eqs -coproductCong f g _ (InjectL op ts) = CalcWith (z.setoid.index _) $ - |~ f.func _ (x.raw.sem op ts) - ~~ z.raw.sem op (map f.func ts) ...(f.homo.semHomo op ts) - ~~ z.raw.sem op (map (coproduct f.func g.func) (map (\_ => Done . Left) ts)) .=.(cong (z.raw.sem op) $ mapComp ts) - ~~ z.raw.sem op (coproducts f.func g.func _ (map (\_ => Done . Left) ts)) .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _) -coproductCong f g _ (InjectR op ts) = CalcWith (z.setoid.index _) $ - |~ g.func _ (y.raw.sem op ts) - ~~ z.raw.sem op (map g.func ts) ...(g.homo.semHomo op ts) - ~~ z.raw.sem op (map (coproduct f.func g.func) (map (\_ => Done . Right) ts)) .=.(cong (z.raw.sem op) $ mapComp ts) - ~~ z.raw.sem op (coproducts f.func g.func _ (map (\_ => Done . Right) ts)) .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _) -coproductCong f g _ (Sym eq) = (z.algebra.equivalence _).symmetric $ coproductCong f g _ eq -coproductCong f g _ (Trans eq eq') = (z.algebra.equivalence _).transitive - (coproductCong f g _ eq) - (coproductCong f g _ eq') - -coproductsCong f g _ [] = [] -coproductsCong f g _ (eq :: eqs) = - coproductCong f g _ eq :: coproductsCong f g _ eqs +coproductsCong f g = coproductsCong' f f g g f.homo.cong g.homo.cong public export coproductIsHomo : {x, y, z : Algebra sig} -> (f : Homomorphism x z) -> (g : Homomorphism y z) diff --git a/src/Soat/FirstOrder/Algebra/FreeExtension.idr b/src/Soat/FirstOrder/Algebra/FreeExtension.idr new file mode 100644 index 0000000..675c65b --- /dev/null +++ b/src/Soat/FirstOrder/Algebra/FreeExtension.idr @@ -0,0 +1,58 @@ +module Soat.FirstOrder.Algebra.FreeExtension + +import Data.Morphism.Indexed +import Data.Setoid.Indexed + +import Soat.FirstOrder.Algebra +import Soat.FirstOrder.Algebra.Coproduct +import Soat.FirstOrder.Signature +import Soat.FirstOrder.Term + +%default total + +public export +FreeExtension : (a : RawAlgebra sig) -> (v : sig.T -> Type) -> RawAlgebra sig +FreeExtension a v = Coproduct a (Free v) + +public export +FreeExtensionAlgebra : (a : Algebra sig) -> (v : ISetoid sig.T) -> Algebra sig +FreeExtensionAlgebra a v = CoproductAlgebra a (FreeAlgebra v) + +public export +extend : {a : RawAlgebra sig} -> {u : sig.T -> Type} -> (f : IFunc v u) + -> IFunc (FreeExtension a v).U (FreeExtension a u).U +extend f = coproduct {z = FreeExtension a u} + (\_ => Done . Left) + (\t => Done . Right . free f t) + +public export +extendHomo : {a : Algebra sig} -> {v, u : ISetoid sig.T} -> (f : IFunction v u) + -> Homomorphism (FreeExtensionAlgebra a v) (FreeExtensionAlgebra a u) +extendHomo f = coproductHomo {z = FreeExtensionAlgebra a u} + (injectLHomo {y = FreeAlgebra u}) + (compHomo injectRHomo (freeHomo f)) + +public export +extendCong : {a : Algebra sig} -> {v, u : ISetoid sig.T} -> (f : IFunction v u) + -> (t : sig.T) -> {tm, tm' : (FreeExtension a.raw v.U).U t} + -> (FreeExtensionAlgebra a v).relation t tm tm' + -> ((FreeExtensionAlgebra a u).relation t `on` extend {a = a.raw} f.func t) tm tm' +extendCong f = coproductCong {z = FreeExtensionAlgebra a u} + (injectLHomo {y = FreeAlgebra u}) + (compHomo injectRHomo (freeHomo f)) + +public export +extendUnique : {a : Algebra sig} -> {v, u : ISetoid sig.T} + -> (f : IFunction v u) + -> (g : Homomorphism (FreeExtensionAlgebra a v) (FreeExtensionAlgebra a u)) + -> (congL : {t : sig.T} -> (i : a.raw.U t) + -> (FreeExtensionAlgebra a u).relation t (g.func t (Done (Left i))) (Done (Left i))) + -> (congR : {t : sig.T} -> (i : Term sig v.U t) + -> (FreeExtensionAlgebra a u).relation t + (g.func t (Done (Right i))) + (Done (Right (free f.func t i)))) + -> {t : sig.T} -> (tm : _) + -> (FreeExtensionAlgebra a u).relation t (g.func t tm) (extend {a = a.raw} f.func t tm) +extendUnique f = coproductUnique {z = FreeExtensionAlgebra a u} + (injectLHomo {y = FreeAlgebra u}) + (compHomo injectRHomo (freeHomo f)) diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index 4a51f94..dc0c182 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -15,25 +15,6 @@ data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where Done : (i : v t) -> Term sig v t Call : (op : Op sig t) -> (ts : Term sig v ^ op.arity) -> Term sig v t -public export -bindTerm : {auto a : RawAlgebra sig} -> IFunc v a.U -> {t : _} -> Term sig v t -> a.U t - -public export -bindTerms : {auto a : RawAlgebra sig} -> IFunc v a.U -> {ts : _} -> Term sig v ^ ts -> a.U ^ ts - -bindTerm env (Done i) = env _ i -bindTerm {a = a} env (Call op ts) = a.sem op (bindTerms env ts) - -bindTerms env [] = [] -bindTerms env (t :: ts) = bindTerm env t :: bindTerms env ts - -public export -bindTermsIsMap : {auto a : RawAlgebra sig} - -> (env : IFunc v a.U) -> {ts : _} -> (tms : Term sig v ^ ts) - -> bindTerms (\tm => env tm) tms = map (\t => bindTerm (\tm => env tm)) tms -bindTermsIsMap env [] = Refl -bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env t)) (bindTermsIsMap env ts) - -- FIXME: these names shouldn't be public. Indication of bad API design namespace Rel public export @@ -138,42 +119,85 @@ FreeAlgebra : ISetoid sig.T -> Algebra sig FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v) public export +inject : IFunc v (Term sig v) +inject _ = Done + +public export +injectFunc : IFunction v (FreeAlgebra v).setoid +injectFunc = MkIFunction (\_ => Done) (\_ => Done') + +public export +bindTerm : {auto a : RawAlgebra sig} -> IFunc v a.U -> IFunc (Term sig v) a.U + +public export +bindTerms : {auto a : RawAlgebra sig} -> IFunc v a.U -> IFunc ((^) (Term sig v)) ((^) a.U) + +bindTerm env _ (Done i) = env _ i +bindTerm env _ (Call op ts) = a.sem op (bindTerms env _ ts) + +bindTerms env _ [] = [] +bindTerms env _ (t :: ts) = bindTerm env _ t :: bindTerms env _ ts + +public export +free : IFunc v u -> IFunc (Term sig v) (Term sig u) +free f = bindTerm {a = Free u} (\i => inject i . f i) + +public export +bindTermsIsMap : {a : RawAlgebra sig} + -> (env : IFunc v a.U) -> {ts : _} -> (tms : Term sig v ^ ts) + -> bindTerms (\tm => env tm) _ tms = map (bindTerm (\tm => env tm)) tms +bindTermsIsMap env [] = Refl +bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env _ t)) (bindTermsIsMap env ts) + +public export bindTermCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v} -> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.relation t (env t x) (env' t y)) - -> {t : sig.T} -> {tm, tm' : Term sig v t} -> (~=~) rel t tm tm' - -> a.relation t (bindTerm {a = a.raw} env tm) (bindTerm {a = a.raw} env' tm') + -> (t : sig.T) -> {tm, tm' : Term sig v t} -> (~=~) rel t tm tm' + -> a.relation t (bindTerm {a = a.raw} env t tm) (bindTerm {a = a.raw} env' t tm') public export bindTermsCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v} -> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.relation t (env t x) (env' t y)) - -> {ts : List sig.T} -> {tms, tms' : Term sig v ^ ts} -> Pointwise ((~=~) rel) tms tms' - -> Pointwise a.relation (bindTerms {a = a.raw} env tms) (bindTerms {a = a.raw} env' tms') + -> (ts : List sig.T) -> {tms, tms' : Term sig v ^ ts} -> Pointwise ((~=~) rel) tms tms' + -> Pointwise a.relation (bindTerms {a = a.raw} env _ tms) (bindTerms {a = a.raw} env' _ tms') -bindTermCong' cong (Done' i) = cong _ i -bindTermCong' {a = a} cong (Call' op ts) = a.algebra.semCong op (bindTermsCong' cong ts) +bindTermCong' cong _ (Done' i) = cong _ i +bindTermCong' cong _ (Call' op ts) = a.algebra.semCong op (bindTermsCong' cong _ ts) -bindTermsCong' cong [] = [] -bindTermsCong' cong (t :: ts) = bindTermCong' cong t :: bindTermsCong' cong ts +bindTermsCong' cong _ [] = [] +bindTermsCong' cong _ (t :: ts) = bindTermCong' cong _ t :: bindTermsCong' cong _ ts + +public export +freeCong' : {u : ISetoid sig.T} -> {f, g : IFunc v u.U} -> {0 rel : IRel v} + -> (cong : (t : sig.T) -> {i, j : v t} -> rel t i j -> u.relation t (f t i) (g t j)) + -> (t : sig.T) -> {tm, tm' : Term sig v t} + -> (~=~) rel t tm tm' -> (~=~) u.relation t (free f t tm) (free g t tm') +freeCong' cong = bindTermCong' {a = FreeAlgebra u} (\i => Done' . cong i) public export bindTermCong : {a : Algebra sig} -> (env : IFunction v a.setoid) - -> {t : sig.T} -> {tm, tm' : Term sig v.U t} -> (~=~) v.relation t tm tm' - -> a.relation t (bindTerm {a = a.raw} env.func tm) (bindTerm {a = a.raw} env.func tm') + -> (t : sig.T) -> {tm, tm' : Term sig v.U t} -> (~=~) v.relation t tm tm' + -> a.relation t (bindTerm {a = a.raw} env.func t tm) (bindTerm {a = a.raw} env.func t tm') bindTermCong env = bindTermCong' env.cong public export bindTermsCong : {a : Algebra sig} -> (env : IFunction v a.setoid) - -> {ts : List sig.T} -> {tms, tms' : Term sig v.U ^ ts} -> Pointwise ((~=~) v.relation) tms tms' + -> (ts : List sig.T) -> {tms, tms' : Term sig v.U ^ ts} -> Pointwise ((~=~) v.relation) tms tms' -> Pointwise a.relation - (bindTerms {a = a.raw} env.func tms) - (bindTerms {a = a.raw} env.func tms') + (bindTerms {a = a.raw} env.func ts tms) + (bindTerms {a = a.raw} env.func ts tms') bindTermsCong env = bindTermsCong' env.cong public export +freeCong : {u : ISetoid sig.T} -> (f : IFunction v u) -> (t : sig.T) -> {tm, tm' : Term sig v.U t} + -> (~=~) v.relation t tm tm' -> (~=~) u.relation t (free f.func t tm) (free f.func t tm') +freeCong f = freeCong' f.cong + +public export bindIsHomo : (a : Algebra sig) -> (env : IFunction v a.setoid) - -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.func) + -> IsHomomorphism (FreeAlgebra v) a (bindTerm {a = a.raw} env.func) bindIsHomo a env = MkIsHomomorphism - (\t, eq => bindTermCong env eq) + (bindTermCong env) (\op, tms => a.algebra.semCong op $ map (\t => (a.algebra.equivalence t).equalImpliesEq) $ @@ -185,14 +209,19 @@ bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> Homomorphism (Fr bindHomo env = MkHomomorphism _ (bindIsHomo _ env) public export -bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig} +freeHomo : {u : ISetoid sig.T} -> IFunction v u + -> Homomorphism {sig = sig} (FreeAlgebra v) (FreeAlgebra u) +freeHomo f = bindHomo $ compFunc injectFunc f + +public export +bindUnique' : {0 v : ISetoid sig.T} -> {a : Algebra sig} -> (f, g : Homomorphism (FreeAlgebra v) a) -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i))) -> {t : sig.T} -> (tm : Term sig v.U t) -> a.relation t (f.func t tm) (g.func t tm) public export -bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig} +bindsUnique' : {0 v : ISetoid sig.T} -> {a : Algebra sig} -> (f, g : Homomorphism (FreeAlgebra v) a) -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i))) -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts) @@ -213,7 +242,7 @@ bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.se -> (f : Homomorphism (FreeAlgebra v) a) -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i)) -> {t : sig.T} -> (tm : Term sig v.U t) - -> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func tm) + -> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func t tm) bindUnique env f = bindUnique' f (bindHomo env) public export @@ -221,8 +250,17 @@ bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.s -> (f : Homomorphism (FreeAlgebra v) a) -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i)) -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts) - -> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func tms) + -> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func ts tms) bindsUnique env f cong ts = CalcWith (pwSetoid a.setoid _) $ |~ map f.func ts - ~~ map (\_ => bindTerm {a = a.raw} env.func) ts ...( bindsUnique' f (bindHomo env) cong ts ) - ~~ bindTerms {a = a.raw} env.func ts .=<( bindTermsIsMap {a = a.raw} env.func ts ) + ~~ map (bindTerm {a = a.raw} env.func) ts ...( bindsUnique' f (bindHomo env) cong ts ) + ~~ bindTerms {a = a.raw} env.func _ ts .=<( bindTermsIsMap {a = a.raw} env.func ts ) + +public export +freeUnique : {v, u : ISetoid sig.T} -> (f : IFunction v u) + -> (g : Homomorphism (FreeAlgebra v) (FreeAlgebra u)) + -> (cong : {t : sig.T} -> (i : v.U t) + -> (FreeAlgebra u).relation t (g.func t (Done i)) (Done (f.func t i))) + -> {t : sig.T} -> (tm : Term sig v.U t) + -> (FreeAlgebra u).relation t (g.func t tm) (free f.func t tm) +freeUnique f = bindUnique $ compFunc injectFunc f diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr index c506c85..f28d4bc 100644 --- a/src/Soat/SecondOrder/Algebra.idr +++ b/src/Soat/SecondOrder/Algebra.idr @@ -18,6 +18,11 @@ extendRel : {U : a -> List a -> Type} -> (rel : IRel (uncurry U)) extendRel rel ctx ty = rel (snd ty, fst ty ++ ctx) public export +extendFunc : {0 U, V : a -> List a -> Type} -> (f : (t : a) -> IFunc (U t) (V t)) -> (ctx : List a) + -> IFunc (extend U ctx) (extend V ctx) +extendFunc f ctx ty = f (snd ty) (fst ty ++ ctx) + +public export algebraOver : (sig : Signature) -> (U : sig.T -> List sig.T -> Type) -> Type algebraOver sig x = (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t) -> extend x ctx ^ op.arity -> x t ctx @@ -26,13 +31,23 @@ public export record RawAlgebra (0 sig : Signature) where constructor MakeRawAlgebra 0 U : (t : sig.T) -> (ctx : List sig.T) -> Type - rename : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx') -> U t ctx -> U t ctx' + rename : (t : sig.T) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx') -> U t ctx -> U t ctx' sem : sig `algebraOver` U var : forall t, ctx . (i : Elem t ctx) -> U t ctx subst : (t : sig.T) -> (ctx : List sig.T) -> forall ctx' . U t ctx' -> (\t => U t ctx) ^ ctx' -> U t ctx public export +(.extendSubst) : (a : RawAlgebra sig) -> (ctx : _) -> {ctx' : _} + -> (tms : (\t => a.U t ctx) ^ ctx') -> IFunc (extend a.U ctx') (extend a.U ctx) +(.extendSubst) a ctx tms ty tm = a.subst + (snd ty) + (fst ty ++ ctx) + tm + (tabulate {is = fst ty} (a.var . Sublist.elemJoinL {ys = ctx}) ++ + map (\t => a.rename t ([] {ys = fst ty} ++ Relation.reflexive {x = ctx})) tms) + +public export record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncurry a.U)) where constructor MkIsAlgebra equivalence : IEquivalence (uncurry a.U) rel @@ -94,12 +109,7 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncur -> {ctx' : _} -> (tms : extend a.U ctx' ^ op.arity) -> (tms' : (\t => a.U t ctx) ^ ctx') -> rel (t, ctx) (a.subst t ctx (a.sem ctx' op tms) tms') - (a.sem ctx op $ - map (\ty, tm => - a.subst (snd ty) (fst ty ++ ctx) tm - (tabulate {is = fst ty} (a.var . Sublist.elemJoinL {ys = ctx}) ++ - map (\t => a.rename t ([] {ys = fst ty} ++ Relation.reflexive {x = ctx})) tms')) $ - tms) + (a.sem ctx op $ map (a.extendSubst ctx tms') $ tms) public export record Algebra (0 sig : Signature) where @@ -139,7 +149,7 @@ record IsHomomorphism -> (tms : extend a.raw.U ctx ^ op.arity) -> b.relation (t, ctx) (f t ctx $ a.raw.sem ctx op tms) - (b.raw.sem ctx op $ map (\ty => f (snd ty) (fst ty ++ ctx)) tms) + (b.raw.sem ctx op $ map (extendFunc f ctx) tms) varHomo : {t : _} -> {ctx : _} -> (i : Elem t ctx) -> b.relation (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i) substHomo : (t : sig.T) -> (ctx : List sig.T) -> {ctx' : _} -> (tm : a.raw.U t ctx') diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr index b08eb0e..61852f2 100644 --- a/src/Soat/SecondOrder/Algebra/Lift.idr +++ b/src/Soat/SecondOrder/Algebra/Lift.idr @@ -6,11 +6,17 @@ import Data.Setoid.Indexed import Soat.Data.Product import Soat.Data.Sublist + import Soat.FirstOrder.Algebra +import Soat.FirstOrder.Algebra.Coproduct +import Soat.FirstOrder.Algebra.FreeExtension import Soat.FirstOrder.Term + import Soat.SecondOrder.Algebra import Soat.SecondOrder.Signature.Lift +import Syntax.PreorderReasoning.Setoid + %default total public export @@ -35,17 +41,17 @@ projectAlgebra a ctx = MkAlgebra _ _ (projectIsAlgebra a.algebra ctx) public export projectIsHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> {f : _} -> IsHomomorphism a b f - -> (ctx : _) + -> (ctx : List sig.T) -> IsHomomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra b ctx) (\t => f t ctx) -projectIsHomo {b = b} f ctx = MkIsHomomorphism - (\t => f.cong t ctx) - (\op, tms => - (b.algebra.equivalence _).transitive - (f.semHomo ctx (MkOp (Op op.op)) (wrap (MkPair []) tms)) $ - b.algebra.semCong ctx (MkOp (Op op.op)) $ - map (\(_,_) => (b.algebra.equivalence _).equalImpliesEq) $ - equalImpliesPwEq $ - mapWrap (MkPair []) tms) +projectIsHomo {b = b} homo ctx = MkIsHomomorphism + { cong = \t => homo.cong t ctx + , semHomo = \op, tms => CalcWith (b.setoid.index _) $ + |~ f _ ctx (a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) tms)) + ~~ b.raw.sem ctx (MkOp (Op op.op)) (map (extendFunc f ctx) (wrap (MkPair []) tms)) + ...(homo.semHomo ctx (MkOp (Op op.op)) (wrap (MkPair []) tms)) + ~~ b.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => f t ctx) tms)) + .=.(cong (b.raw.sem ctx (MkOp (Op op.op))) $ mapWrap (MkPair []) {f = extendFunc f ctx} tms) + } public export projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> Homomorphism a b @@ -57,88 +63,77 @@ public export -> (f : ctx `Sublist` ctx') -> FirstOrder.Algebra.Homomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra a ctx') (.renameHomo) a f = MkHomomorphism - (\t => a.raw.rename t f) - (MkIsHomomorphism - (\t => a.algebra.renameCong t f) - (\op, tms => (a.algebra.equivalence _).transitive - (a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms)) - (a.algebra.semCong _ (MkOp (Op op.op)) $ - map (\(_,_) => (a.algebra.equivalence _).equalImpliesEq) $ - pwSym (\_ => MkSymmetric symmetric) $ - pwTrans (\_ => MkTransitive transitive) - (wrapIntro $ - mapIntro'' (\t, tm, _, Refl => - cong (\f => a.raw.rename t f tm) $ - sym $ - uncurryCurry f) $ - equalImpliesPwEq Refl) $ - equalImpliesPwEq $ - sym $ - mapWrap (MkPair []) tms))) + { func = \t => a.raw.rename t f + , homo = MkIsHomomorphism + { cong = \t => a.algebra.renameCong t f + , semHomo = \op, tms => CalcWith (a.setoid.index _) $ + |~ a.raw.rename _ f (a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) tms)) + ~~ a.raw.sem _ (MkOp (Op op.op)) (map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms)) + ...(a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms)) + ~~ a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => a.raw.rename t f) tms)) + ...(a.algebra.semCong _ (MkOp (Op op.op)) $ + CalcWith (pwSetoid (a.setoid.reindex (\ty => (snd ty, fst ty ++ _))) _) $ + |~ map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms) + ~~ wrap (MkPair []) (map (\t => a.raw.rename t (reflexive {x = []} ++ f)) tms) + .=.(mapWrap (MkPair []) tms) + ~~ wrap (MkPair []) (map (\t => a.raw.rename t f) tms) + .=.(cong (wrap (MkPair [])) $ + pwEqImpliesEqual $ + mapIntro'' (\t, tm, _, Refl => cong (\f => a.raw.rename t f tm) $ uncurryCurry f) $ + equalImpliesPwEq Refl)) + } + } public export (.substHomo1) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> (ctx : List sig.T) -> {ctx' : List sig.T} -> (tms : (\t => a.raw.U t ctx) ^ ctx') -> FirstOrder.Algebra.Homomorphism {sig = sig} (projectAlgebra a ctx') (projectAlgebra a ctx) (.substHomo1) a ctx tms = MkHomomorphism - (\t, tm => a.raw.subst t ctx tm tms) - (MkIsHomomorphism - (\t, eq => a.algebra.substCong t ctx eq $ pwRefl (\_ => (a.algebra.equivalence _).refl)) - (\op, tms' => (a.algebra.equivalence _).transitive - (a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms) - (a.algebra.semCong ctx (MkOp (Op op.op)) $ - pwSym (\(_,_) => (a.algebra.equivalence _).sym) $ - pwTrans (\(_,_) => (a.algebra.equivalence _).trans) - (pwSym (\(_,_) => (a.algebra.equivalence _).sym) $ - wrapIntro $ - mapIntro'' (\t, tm, _, Refl => - a.algebra.substCong t ctx (a.algebra.equivalence _).reflexive $ - pwTrans (\_ => (a.algebra.equivalence _).trans) - (mapIntro'' (\t, tm, _, Refl => (a.algebra.equivalence _).transitive - ((a.algebra.equivalence _).equalImpliesEq $ - cong (\f => a.raw.rename t f tm) $ - uncurryCurry reflexive) - (a.algebra.renameId _ _ tm)) $ - equalImpliesPwEq Refl) $ - map (\_ => (a.algebra.equivalence _).equalImpliesEq) $ - equalImpliesPwEq $ - mapId tms) $ - equalImpliesPwEq Refl) $ - map (\(_,_) => (a.algebra.equivalence _).equalImpliesEq) $ - equalImpliesPwEq $ - sym $ - mapWrap (MkPair []) tms'))) - -renameBodyFunc : (f : ctx `Sublist` ctx') - -> IFunction - (isetoid (flip Elem ctx)) - (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx'))).setoid -renameBodyFunc f = MkIFunction (\_ => Done . curry f) (\_ => Done' . cong (curry f)) + { func = \t, tm => a.raw.subst t ctx tm tms + , homo = MkIsHomomorphism + { cong = \t, eq => a.algebra.substCong t ctx eq $ pwRefl (\_ => (a.algebra.equivalence _).refl) + , semHomo = \op, tms' => CalcWith (a.setoid.index _) $ + |~ a.raw.subst _ ctx (a.raw.sem ctx' (MkOp (Op op.op)) (wrap (MkPair []) tms')) tms + ~~ a.raw.sem ctx (MkOp (Op op.op)) (map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms')) + ...(a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms) + ~~ a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms')) + ...(a.algebra.semCong ctx (MkOp (Op op.op)) $ + CalcWith (pwSetoid (a.setoid.reindex (\ty => (snd ty, fst ty ++ ctx))) _) $ + |~ map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms') + ~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm (map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms)) tms') + .=.(mapWrap (MkPair []) tms') + ~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms') + ...(wrapIntro $ + mapIntro' (\t, eq => + a.algebra.substCong t ctx eq $ + CalcWith (pwSetoid (a.setoidAt _) _) $ + |~ map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms + ~~ map (\t => a.raw.rename t reflexive) tms + .=.(pwEqImpliesEqual $ + mapIntro' (\t => cong2 (a.raw.rename t) $ uncurryCurry reflexive) $ + equalImpliesPwEq Refl) + ~~ map (\t => id) tms + ...(mapIntro' (\t, Refl => a.algebra.renameId t ctx _) $ + equalImpliesPwEq Refl) + ~~ tms + .=.(mapId tms)) $ + pwRefl (\t => (a.algebra.equivalence _).refl))) + } + } -indexFunc : {ctx : List sig.T} -> (tms : Term sig (flip Elem ctx) ^ ts) - -> IFunction - (isetoid (flip Elem ts)) - (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx))).setoid +indexFunc : {x : ISetoid a} -> (tms : x.U ^ ts) -> IFunction (isetoid (flip Elem ts)) x indexFunc tms = MkIFunction (\_ => index tms) - (\_ => ((FreeIsAlgebra (isetoid (flip Elem _))).equivalence _).equalImpliesEq . cong (index tms)) - --- renameFunc : (f : ctx `Sublist` ctx') --- -> IFunction --- (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx))).setoid --- (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx'))).setoid --- renameFunc f = MkIFunction --- (\_ => bindTerm {a = Free _} (renameBodyFunc f).func) --- (\t => bindTermCong {a = FreeAlgebra (isetoid (flip Elem _))} (renameBodyFunc f)) + (\_ => (x.equivalence _).equalImpliesEq . cong (index tms)) public export Initial : (0 sig : _) -> SecondOrder.Algebra.RawAlgebra (lift sig) Initial sig = MakeRawAlgebra (\t, ctx => Term sig (flip Elem ctx) t) - (\t, f => bindTerm {a = Free _} (renameBodyFunc f).func) + (\t, f => free (\_ => curry f) t) (\_, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair [])) Done - (\_, _, t, ts => bindTerm {a = Free _} (\_ => index ts) t) + (\t, _, tm, tms => bindTerm {a = Free _} (\_ => index tms) t tm) public export InitialIsAlgebra : (0 sig : _) @@ -147,91 +142,80 @@ InitialIsAlgebra : (0 sig : _) (Initial sig) (\(t, ctx) => (~=~) {sig = sig} {v = flip Elem ctx} (\_ => Equal) t) InitialIsAlgebra sig = MkIsAlgebra - (\(t, ctx) => tmRelEq (\_ => equiv) t) - (\t, f => bindTermCong {a = FreeAlgebra (isetoid (flip Elem _))} (renameBodyFunc f)) - (\_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro) - (\_, _, eq, eqs => bindTermCong' + { equivalence = \(t, ctx) => tmRelEq (\_ => equiv) t + , renameCong = \t, f => freeCong (ifunc (\_ => curry f)) t + , semCong = \_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro + , substCong = \_, _, eq, eqs => bindTermCong' {a = FreeAlgebra (isetoid (flip Elem _))} (\t, Refl => index eqs _) - eq) - (\t, ctx, tm => + _ + eq + , renameId = \t, ctx, tm => tmRelSym (\_ => MkSymmetric symmetric) $ - bindUnique (renameBodyFunc reflexive) idHomo (\i => Done' $ sym $ curryUncurry id i) $ - tm) - (\t, f, g, tm => + freeUnique (ifunc (\_ => curry reflexive)) idHomo (\i => Done' $ sym $ curryUncurry id i) $ + tm + , renameComp = \t, f, g, tm => tmRelSym (\_ => MkSymmetric symmetric) $ - bindUnique - {a = FreeAlgebra (isetoid (flip Elem _))} - (renameBodyFunc (transitive g f)) - (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (renameBodyFunc g))) + freeUnique + (ifunc (\_ => curry (transitive g f))) + (compHomo (freeHomo (ifunc (\_ => curry f))) (freeHomo (ifunc (\_ => curry g)))) (\i => Done' $ sym $ curryUncurry (curry f . curry g) i) $ - tm) - (\f, (MkOp (Op op)), tms => + tm + , semNat = \f, (MkOp (Op op)), tms => Call' (MkOp op) $ - Pointwise.map (\_ => tmRelReflexive (\_ => MkReflexive reflexive)) $ - pwTrans (\_ => MkTransitive transitive) (equalImpliesPwEq $ bindTermsIsMap {a = Free _} _ _) $ - pwTrans (\_ => MkTransitive transitive) - (mapIntro' (\t, eq => - tmRelEqualIsEqual $ - bindTermCong' - {rel = \_ => Equal} - {a = FreeAlgebra (isetoid (flip Elem _))} - (\_, Refl => Done' $ sym $ curryUncurry (curry f) _) $ - tmRelReflexive (\_ => MkReflexive reflexive) $ - eq) $ - equalImpliesPwEq Refl) $ - equalImpliesPwEq $ - mapUnwrap _ _) - -- Pointwise.map (\_ => tmRelReflexive (\_ => MkReflexive reflexive)) $ - -- transitive (equalImpliesPwEq $ bindTermsIsMap {a = Free _} _ (unwrap (MkPair []) tms)) $ - -- transitive - -- (mapIntro - -- (\t, eq => - -- bindTermCong' - -- {v = isetoid (flip Elem _)} - -- {a = FreeAlgebra (isetoid (flip Elem _))} - -- (\_, Refl => Done' $ sym $ curryUncurry (curry f) _) $ - -- tmRelReflexive (\_ => MkReflexive reflexive) $ - -- eq) $ - -- equalImpliesPwEq Refl) $ - -- equalImpliesPwEq $ - -- mapUnwrap - -- (MkPair []) - -- (\ty => (renameFunc (reflexive ++ f)).func (snd ty)) - -- tms) - (\_, _ => Done' Refl) - (\t, f, tm, tms => + CalcWith (pwSetoid (FreeAlgebra (isetoid (flip Elem _))).setoid _) $ + |~ bindTerms {a = Free _} (\_ => Done . curry f) _ (unwrap (MkPair []) tms) + ~~ map (free (\_ => curry f)) (unwrap (MkPair []) tms) + .=.(bindTermsIsMap {a = Free _} _ _) + ~~ map (free (\_ => curry (reflexive {x = []} ++ f))) (unwrap (MkPair []) tms) + ..<(mapIntro' (\t => + freeCong' + {rel = \_ => Equal} + {u = isetoid (flip Elem _)} + (\_, Refl => curryUncurry (curry f) _) + _) $ + tmsRelRefl (\_ => MkReflexive reflexive) (unwrap (MkPair []) tms)) + ~~ unwrap (MkPair []) (map (\ty => free (\_ => curry (reflexive {x = fst ty} ++ f)) (snd ty)) tms) + .=.(mapUnwrap (MkPair []) tms) + , varNat = \_, _ => Done' Refl + , substNat = \t, f, tm, tms => bindUnique {a = FreeAlgebra (isetoid (flip Elem _))} (indexFunc _) - (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (indexFunc tms))) + (compHomo + (freeHomo (ifunc (\_ => curry f))) + (bindHomo (indexFunc tms))) (\i => tmRelReflexive (\_ => MkReflexive reflexive) $ sym $ indexMap tms i) - tm) - (\t, ctx, f, tm, tms => + tm + , substExnat = \t, ctx, f, tm, tms => bindUnique {a = FreeAlgebra (isetoid (flip Elem _))} (indexFunc _) - (compHomo (bindHomo (indexFunc tms)) (bindHomo (renameBodyFunc f))) + (compHomo + (bindHomo (indexFunc tms)) + (freeHomo (ifunc (\_ => curry f)))) (\i => tmRelReflexive (\_ => MkReflexive reflexive) $ sym $ indexShuffle f i) - tm) - (\t, ctx, tm, tms, tms' => + tm + , substComm = \t, ctx, tm, tms, tms' => bindUnique {a = FreeAlgebra (isetoid (flip Elem _))} (indexFunc _) - (compHomo (bindHomo (indexFunc tms')) (bindHomo (indexFunc tms))) + (compHomo + (bindHomo (indexFunc tms')) + (bindHomo (indexFunc tms))) (\i => tmRelReflexive (\_ => MkReflexive reflexive) $ sym $ indexMap tms i) - tm) - (\_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _) - (\t, ctx, tm => + tm + , substVarL = \_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _ + , substVarR = \t, ctx, tm => tmRelSym (\_ => MkSymmetric symmetric) $ bindUnique {a = FreeAlgebra (isetoid (flip Elem _))} @@ -241,108 +225,113 @@ InitialIsAlgebra sig = MkIsAlgebra tmRelReflexive (\_ => MkReflexive reflexive) $ sym $ indexTabulate Done i) - tm) - (\ctx, (MkOp (Op op)), tms, tms' => + tm + , substCompat = \ctx, (MkOp (Op op)), tms, tms' => Call' (MkOp op) $ - tmsRelTrans (\_ => MkTransitive transitive) - (tmsRelSym (\_ => MkSymmetric symmetric) $ - bindsUnique - {a = FreeAlgebra (isetoid (flip Elem _))} - (indexFunc tms') - (bindHomo (indexFunc _)) - (\i => - (tmRelTrans (\_ => MkTransitive transitive) - (tmRelReflexive (\_ => MkReflexive reflexive) $ - indexMap - {f = (\_ => bindTerm {a = Free _} (\_ => Done . curry (uncurry (curry reflexive))))} - tms' - i) $ - tmRelSym (\_ => MkSymmetric symmetric) $ - (bindUnique - {a = FreeAlgebra (isetoid (flip Elem _))} - (renameBodyFunc _) - idHomo - (\i => - Done' $ - sym $ - transitive (curryUncurry (curry reflexive) i) (curryUncurry id i)) - (index tms' i)))) - (unwrap (MkPair []) tms)) $ - tmsRelReflexive (\_ => MkReflexive reflexive) $ - mapUnwrap _ _) + CalcWith (pwSetoid (FreeAlgebra (isetoid (flip Elem _))).setoid _) $ + |~ bindTerms {a = Free _} (\_ => index tms') _ (unwrap (MkPair []) tms) + ~~ map (bindTerm {a = Free _} (\_ => index tms')) (unwrap (MkPair []) tms) + .=.(bindTermsIsMap {a = Free _} _ _) + ~~ map (\t => (Initial sig).extendSubst ctx tms' ([], t)) (unwrap (MkPair []) tms) + ..<(mapIntro' (\t => bindTermCong' + {rel = \_ => Equal} + {a = FreeAlgebra (isetoid (flip Elem _))} + (\t, Refl => CalcWith ((FreeAlgebra (isetoid (flip Elem _))).setoid.index _) $ + |~ index (map (free (\_ => curry ([] {ys = []} ++ reflexive))) tms') _ + ~~ free (\_ => curry ([] {ys = []} ++ reflexive)) _ (index tms' _) + .=.(indexMap tms' _) + ~~ index tms' _ + ..<(freeUnique + (ifunc (\_ => curry ([] {ys = []} ++ reflexive))) + idHomo + (\i => Done' $ sym $ trans (curryUncurry _ i) (curryUncurry id i)) + (index tms' _))) + _) $ + tmsRelRefl (\_ => MkReflexive reflexive) $ + unwrap (MkPair []) tms) + ~~ unwrap (MkPair []) (map ((Initial sig).extendSubst ctx tms') tms) + .=.(mapUnwrap (MkPair []) tms) + } public export InitialAlgebra : (0 sig : _) -> SecondOrder.Algebra.Algebra (lift sig) InitialAlgebra sig = MkAlgebra (Initial sig) _ (InitialIsAlgebra sig) public export -freeToInitialIsHomo : (0 sig : _) -> (ctx : List sig.T) - -> IsHomomorphism {sig = sig} - (FreeAlgebra (isetoid (flip Elem ctx))) - (projectAlgebra (InitialAlgebra sig) ctx) - (\_ => Basics.id) -freeToInitialIsHomo sig ctx = MkIsHomomorphism - (\_ => id) - (\(MkOp op), tms => - Call' (MkOp op) $ - tmsRelSym (\_ => MkSymmetric symmetric) $ - tmsRelReflexive (\_ => MkReflexive reflexive) $ - transitive (unwrapWrap _ _) (mapId tms)) - -public export -freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T) - -> Homomorphism {sig = sig} +ProjectInitialIsFree : (0 sig : _) -> (ctx : List sig.T) + -> Isomorphism {sig = sig} (FreeAlgebra (isetoid (flip Elem ctx))) (projectAlgebra (InitialAlgebra sig) ctx) -freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx) +ProjectInitialIsFree sig ctx = MkIsomorphism + { to = MkHomomorphism + { func = \_ => id + , homo = MkIsHomomorphism + { cong = \_ => id + , semHomo = \(MkOp op), ts => + Call' (MkOp op) $ + tmsRelReflexive (\_ => MkReflexive Refl) $ + sym $ + trans (unwrapWrap (extend (Initial sig).U ctx) _) (mapId ts) + } + } + , from = MkHomomorphism + { func = \_ => id + , homo = MkIsHomomorphism + { cong = \_ => id + , semHomo = \(MkOp op), ts => + Call' (MkOp op) $ + tmsRelReflexive (\_ => MkReflexive Refl) $ + trans (unwrapWrap (extend (Initial sig).U ctx) ts) (sym $ mapId ts) + } + } + , fromTo = \tm => tmRelRefl (\_ => MkReflexive Refl) tm + , toFrom = \tm => tmRelRefl (\_ => MkReflexive Refl) tm + } public export -fromInitial : (a : SecondOrder.Algebra.RawAlgebra (lift sig)) -> (t : sig.T) -> (ctx : List sig.T) - -> (Initial sig).U t ctx -> a.U t ctx -fromInitial a t ctx = bindTerm {a = project a ctx} (\_ => a.var) +fromInitial : (a : RawAlgebra (lift sig)) + -> (t : _) -> (ctx : _) -> (Initial sig).U t ctx -> a.U t ctx +fromInitial a t ctx = bindTerm {a = project a ctx} (\_ => a.var) t public export fromInitialIsHomo : (a : SecondOrder.Algebra.Algebra (lift sig)) -> IsHomomorphism (InitialAlgebra sig) a (fromInitial a.raw) fromInitialIsHomo a = MkIsHomomorphism - (\t , ctx => bindTermCong {a = projectAlgebra a ctx} (a.varFunc ctx)) - (\t, f => bindUnique' + { cong = \t, ctx => bindTermCong {a = projectAlgebra a ctx} (a.varFunc ctx) t + , renameHomo = \t, f => bindUnique' {v = isetoid (flip Elem _)} {a = projectAlgebra a _} - (compHomo (bindHomo (a.varFunc _)) (bindHomo (renameBodyFunc f))) + (compHomo (bindHomo (a.varFunc _)) (freeHomo (ifunc (\_ => curry f)))) (compHomo (a.renameHomo f) (bindHomo (a.varFunc _))) - (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i)) - (\ctx, (MkOp (Op op)), tms => + (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i) + , semHomo = \ctx, (MkOp (Op op)), tms => a.algebra.semCong ctx (MkOp (Op op)) $ - map (\_ => (a.algebra.equivalence _).equalImpliesEq) $ - equalImpliesPwEq $ - transitive - (cong (wrap _) $ bindTermsIsMap {a = project a.raw _} (\_ => a.raw.var) $ unwrap _ tms) $ - transitive - (sym $ mapWrap (MkPair []) {f = \_ => fromInitial a.raw _ _} $ unwrap _ tms) $ - cong (map _) $ - wrapUnwrap tms) - (\_ => (a.algebra.equivalence _).reflexive) - (\t, ctx, tm, tms => bindUnique' - {v = isetoid (flip Elem _)} - {a = projectAlgebra a _} - (compHomo (bindHomo (a.varFunc _)) (bindHomo (indexFunc tms))) - (compHomo (a.substHomo1 ctx _) (bindHomo (a.varFunc _))) - (\i => - (a.algebra.equivalence _).transitive - (bindUnique - {v = isetoid (flip Elem _)} - {a = projectAlgebra a _} - (a.varFunc _) - (bindHomo (a.varFunc _)) - (\i => (a.algebra.equivalence _).reflexive) - (index tms i)) $ - (a.algebra.equivalence _).symmetric $ - (a.algebra.equivalence _).transitive - (a.algebra.substVarL ctx i _) $ - (a.algebra.equivalence _).equalImpliesEq $ - indexMap {f = \t => bindTerm {a = project a.raw ctx} (\_ => a.raw.var)} tms i) - tm) + CalcWith (pwSetoid (a.setoid.reindex (\ty => (snd ty, fst ty ++ ctx))) _) $ + |~ wrap (MkPair []) (bindTerms {a = project a.raw ctx} (\_ => a.raw.var) _ (unwrap (MkPair []) tms)) + ~~ wrap (MkPair []) (map (\t => fromInitial a.raw t ctx) (unwrap (MkPair []) tms)) + .=.(cong (wrap _) $ bindTermsIsMap {a = project a.raw ctx} _ _) + ~~ wrap (MkPair []) (unwrap (MkPair []) (map (extendFunc (fromInitial a.raw) ctx) tms)) + .=.(cong (wrap _) $ mapUnwrap (MkPair []) tms) + ~~ map (extendFunc (fromInitial a.raw) ctx) tms + .=.(wrapUnwrap _) + , varHomo = \_ => (a.algebra.equivalence _).reflexive + , substHomo = \t, ctx, tm, tms => + bindUnique' + {v = isetoid (flip Elem _)} + {a = projectAlgebra a _} + (compHomo + (bindHomo (a.varFunc _)) + (bindHomo (indexFunc tms))) + (compHomo + (a.substHomo1 ctx _) (bindHomo (a.varFunc _))) + (\i => CalcWith (a.setoid.index _) $ + |~ bindTerm {a = project a.raw _} (\_ => a.raw.var) _ (index tms i) + ~~ index (map (bindTerm {a = project a.raw _} (\_ => a.raw.var)) tms) i + .=<(indexMap {f = bindTerm {a = project a.raw _} (\_ => a.raw.var)} tms i) + ~~ a.raw.subst _ ctx (a.raw.var i) (map (bindTerm {a = project a.raw _} (\_ => a.raw.var)) tms) + ..<(a.algebra.substVarL ctx i _)) + tm + } public export fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig)) @@ -358,5 +347,135 @@ fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique {v = isetoid (flip Elem _)} {a = projectAlgebra a ctx} (a.varFunc ctx) - (compHomo (projectHomo f ctx) (freeToInitialHomo sig ctx)) + (compHomo (projectHomo f ctx) (ProjectInitialIsFree sig ctx).to) f.homo.varHomo + +public export +FreeExtension : RawAlgebra sig -> RawAlgebra (lift sig) +FreeExtension a = MakeRawAlgebra + { U = \t, ctx => (FreeExtension a (flip Elem ctx)).U t + , rename = \t, f => extend (\_ => curry f) t + , sem = \ctx, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair []) + , var = Done . Right . Done + , subst = \t, ctx, tm, tms => + coproduct + {z = FreeExtension a (flip Elem _)} + (\_ => Done . Left) + (bindTerm {a = FreeExtension a (flip Elem _)} (\_ => index tms)) + t + tm + } + +public export +FreeExtensionAlgebra : Algebra sig -> Algebra (lift sig) +FreeExtensionAlgebra a = MkAlgebra + { raw = FreeExtension a.raw + , relation = \(t, ctx) => (FreeExtensionAlgebra a (isetoid (flip Elem ctx))).relation t + , algebra = MkIsAlgebra + { equivalence = \(t, ctx) => (FreeExtensionAlgebra a (isetoid (flip Elem ctx))).algebra.equivalence t + , renameCong = \t, f => extendCong (ifunc (\_ => curry f)) t + , semCong = \_ , (MkOp (Op op)) => Call (MkOp op) . unwrapIntro + , substCong = \t, ctx, eq, eqs => coproductCong' {z = FreeExtensionAlgebra a (isetoid (flip Elem ctx))} + (injectLHomo {y = FreeAlgebra (isetoid (flip Elem ctx))}) + (injectLHomo {y = FreeAlgebra (isetoid (flip Elem ctx))}) + (bindHomo (indexFunc _)) + (bindHomo (indexFunc _)) + (\_ => DoneL) + (bindTermCong' {a = FreeExtensionAlgebra a (isetoid (flip Elem _))} (\_, Refl => index eqs _)) + t + eq + , renameId = \t, ctx, tm => + (((FreeExtensionAlgebra a (isetoid (flip Elem _)))).algebra.equivalence _).symmetric $ + extendUnique + { v = isetoid (flip Elem _) + , u = isetoid (flip Elem _) + , f = ifunc ?f -- (\_ => curry reflexive) + , g = idHomo + , congL = ?congL + , congR = ?congR + , tm = ?tm + } + -- extendUnique (ifunc (\_ => curry reflexive)) idHomo ?congL ?congR tm + , renameComp = \t, f, g, tm => ?renameComp + , semNat = \f, (MkOp (Op op)), tms => Call (MkOp op) $ ?semNat + , varNat = \f, i => (((FreeExtensionAlgebra a (isetoid (flip Elem _)))).algebra.equivalence _).reflexive + , substNat = \t, f, tm, tms => ?substNat + , substExnat = \t, ctx, f, tm, tms => ?substExnat + , substComm = \t, ctx, tm, tms, tms' => ?substComm + , substVarL = \ctx, i, tms => ?substVarL + , substVarR = \t, ctx, tm => ?substVarR + , substCompat = \ctx, (MkOp (Op op)), tms, tms' => Call (MkOp op) $ ?substCompat + } + } + +public export +ProjectFreeExtensionIsOriginal : (a : FirstOrder.Algebra.Algebra sig) + -> Isomorphism (projectAlgebra (FreeExtensionAlgebra a) []) a + +public export +FreeExtensionIsFree : (a : Algebra sig) -> (b : Algebra (lift sig)) + -> Isomorphism (projectAlgebra b []) a + -> Homomorphism (FreeExtensionAlgebra a) b + +-- -- public export +-- -- FreeExtension : RawAlgebra sig -> RawAlgebra (lift sig) +-- -- FreeExtension a = MakeRawAlgebra +-- -- { U = \t, ctx => (Coproduct a (Free (flip Elem ctx))).U t +-- -- , rename = \t, f => coproduct +-- -- {z = Coproduct a (Free (flip Elem _))} +-- -- (\_ => Done . Left) +-- -- (\t => Done . Right . (Initial sig).rename t f) +-- -- t +-- -- , sem = \ctx, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair []) +-- -- , var = Done . Right . Done +-- -- , subst = \t, ctx, tm, tms => coproduct +-- -- {z = Coproduct a (Free (flip Elem _))} +-- -- (\_ => Done . Left) +-- -- (\_ => bindTerm {a = Coproduct a (Free (flip Elem ctx))} (\_ => index tms)) +-- -- t +-- -- tm +-- -- } + +-- -- public export 0 +-- -- FreeExtensionRelation : (algebra : FirstOrder.Algebra.IsAlgebra sig a rel) +-- -- -> IRel (uncurry (FreeExtension a).U) +-- -- FreeExtensionRelation algebra (t, ctx) = +-- -- (CoproductAlgebra (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem ctx)))).relation t + +-- -- public export +-- -- FreeExtensionIsAlgebra : {a : RawAlgebra sig} -> forall rel . (algebra : IsAlgebra sig a rel) +-- -- -> IsAlgebra (lift sig) (FreeExtension a) (FreeExtensionRelation algebra) +-- -- FreeExtensionIsAlgebra algebra = MkIsAlgebra +-- -- { equivalence = \(t, ctx) => ?equivalence +-- -- , renameCong = \t, f => coproductCong +-- -- (injectLHomo (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem _)))) +-- -- (compHomo (injectRHomo a ?y) ?g) +-- -- -- (compHomo +-- -- -- (injectRHomo (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem _)))) +-- -- -- ((InitialAlgebra sig).renameHomo f)) +-- -- t +-- -- , semCong = \ctx, (MkOp (Op op)) => Call (MkOp op) . unwrapIntro +-- -- , substCong = \t, ctx, eq, eqs => coproductCong' +-- -- (injectLHomo (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem _)))) +-- -- (injectLHomo (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem _)))) +-- -- (bindHomo (indexFunc _ _)) +-- -- (bindHomo (indexFunc _ _)) +-- -- (\_ => DoneL) +-- -- ?rhs -- (bindTermCong' (\_ => index ?eqseqs)) +-- -- _ +-- -- ?eq +-- -- , renameId = ?renameId +-- -- , renameComp = ?renameComp +-- -- , semNat = ?semNat +-- -- , varNat = ?varNat +-- -- , substNat = ?substNat +-- -- , substExnat = ?substExnat +-- -- , substComm = ?substComm +-- -- , substVarL = ?substVarL +-- -- , substVarR = ?substVarR +-- -- , substCompat = ?substCompat +-- -- } + +-- -- public export +-- -- FreeExtensionAlgebra : Algebra sig -> Algebra (lift sig) +-- -- FreeExtensionAlgebra a = MkAlgebra _ _ $ FreeExtensionIsAlgebra a.algebra |