diff options
| -rw-r--r-- | src/Soat/Data/Product.idr | 7 | ||||
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 41 |
2 files changed, 40 insertions, 8 deletions
diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr index cd69098..f92c23c 100644 --- a/src/Soat/Data/Product.idr +++ b/src/Soat/Data/Product.idr @@ -109,6 +109,13 @@ namespace Pointwise pwRefl f {xs = []} = [] pwRefl f {xs = (x :: xs)} = reflexive :: pwRefl f + + public export + pwReflexive : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)} + -> ((i : a) -> Reflexive (x i) (rel i)) + -> {is : List a} -> {xs, ys : x ^ is} -> xs = ys -> Pointwise rel xs ys + pwReflexive refl Refl = pwRefl refl + public export pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)} -> ((i : a) -> Symmetric (x i) (rel i)) diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index 8f1b71a..701d3d6 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -153,11 +153,38 @@ 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} + -> (f, g : Homomorphism (FreeAlgebra v) a) + -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (g.f t (Done i))) + -> {t : sig.T} -> (tm : Term sig v.U t) + -> a.rel t (f.f t tm) (g.f t tm) + +public export +bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig} + -> (f, g : Homomorphism (FreeAlgebra v) a) + -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (g.f t (Done i))) + -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts) + -> Pointwise a.rel (map f.f tms) (map g.f tms) + +bindUnique' f g cong (Done i) = cong i +bindUnique' f g cong (Call op ts) = + (a.algebra.equivalence _).transitive (f.homo.semHomo op ts) $ + (a.algebra.equivalence _).symmetric $ + (a.algebra.equivalence _).transitive (g.homo.semHomo op ts) $ + (a.algebra.equivalence _).symmetric $ + a.algebra.semCong op $ + bindsUnique' f g cong ts + +bindsUnique' f g cong [] = [] +bindsUnique' f g cong (t :: ts) = bindUnique' f g cong t :: bindsUnique' f g cong ts + +public export bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid) -> (f : Homomorphism (FreeAlgebra v) a) -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.func t i)) -> {t : sig.T} -> (tm : Term sig v.U t) -> a.rel t (f.f t tm) (bindTerm {a = a.raw} env.func tm) +bindUnique env f = bindUnique' f (bindHomo env) public export bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid) @@ -165,11 +192,9 @@ bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.s -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.func t i)) -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts) -> Pointwise a.rel (map f.f tms) (bindTerms {a = a.raw} env.func tms) - -bindUnique env f fDone (Done i) = fDone i -bindUnique env f fDone (Call op ts) = (a.algebra.equivalence _).transitive - (f.homo.semHomo op ts) - (a.algebra.semCong op $ bindsUnique env f fDone ts) - -bindsUnique env f fDone [] = [] -bindsUnique env f fDone (t :: ts) = bindUnique env f fDone t :: bindsUnique env f fDone ts +bindsUnique env f cong ts = + pwTrans (\i => (a.algebra.equivalence i).trans) + (bindsUnique' f (bindHomo env) cong ts) $ + pwReflexive (\i => (a.algebra.equivalence i).refl) $ + sym $ + bindTermsIsMap {a = a.raw} env.func ts
\ No newline at end of file |