diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 15:15:40 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 15:15:40 +0000 |
| commit | dfed64700d3caae5749cc94cfcf8b97a4e27a435 (patch) | |
| tree | 938f8a29eb0edf301328713e6be1ff31c7c04177 /src/Soat/FirstOrder/Term.idr | |
| parent | d7fa1ccbbb6dcf78d16b8adfeab4e1a167a2f0b3 (diff) | |
Generalise bindUnique.
Diffstat (limited to 'src/Soat/FirstOrder/Term.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 41 |
1 files changed, 33 insertions, 8 deletions
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 |