diff options
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 23 |
1 files changed, 10 insertions, 13 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index 99f7e32..4a51f94 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -6,6 +6,7 @@ import Data.Setoid.Indexed import Soat.Data.Product import Soat.FirstOrder.Algebra import Soat.FirstOrder.Signature +import Syntax.PreorderReasoning.Setoid %default total @@ -198,13 +199,11 @@ bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig} -> Pointwise a.relation (map f.func tms) (map g.func 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 +bindUnique' f g cong (Call op ts) = CalcWith (a.setoid.index _) $ + |~ f.func _ (Call op ts) + ~~ a.raw.sem op (map f.func ts) ...( f.homo.semHomo op ts ) + ~~ a.raw.sem op (map g.func ts) ...( a.algebra.semCong op $ bindsUnique' f g cong ts ) + ~~ g.func _ (Call op ts) ..<( g.homo.semHomo op ts ) bindsUnique' f g cong [] = [] bindsUnique' f g cong (t :: ts) = bindUnique' f g cong t :: bindsUnique' f g cong ts @@ -223,9 +222,7 @@ bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.s -> (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) -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 +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 ) |