summaryrefslogtreecommitdiff
path: root/src/Soat/FirstOrder
diff options
context:
space:
mode:
Diffstat (limited to 'src/Soat/FirstOrder')
-rw-r--r--src/Soat/FirstOrder/Algebra.idr48
-rw-r--r--src/Soat/FirstOrder/Term.idr119
2 files changed, 91 insertions, 76 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 245af6d..88191d6 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -1,12 +1,12 @@
module Soat.FirstOrder.Algebra
-import Data.Morphism.Indexed
import Data.Setoid.Indexed
import public Soat.Data.Product
import Soat.FirstOrder.Signature
+import Syntax.PreorderReasoning.Setoid
+
%default total
-%hide Control.Relation.Equivalence
public export
algebraOver : (sig : Signature) -> (U : sig.T -> Type) -> Type
@@ -30,25 +30,29 @@ public export
record RawAlgebraWithRelation (0 sig : Signature) where
constructor MkRawAlgebraWithRelation
raw : RawAlgebra sig
- 0 relation : IRel raw.U
+ 0 relation : (t : sig.T) -> Rel (raw.U t)
public export
-record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) where
+record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
constructor MkIsAlgebra
- equivalence : IEquivalence a.U rel
+ equivalence : IndexedEquivalence sig.T a.U
semCong : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
- -> Pointwise rel tms tms' -> rel t (a.sem op tms) (a.sem op tms')
+ -> Pointwise equivalence.relation tms tms'
+ -> equivalence.relation t (a.sem op tms) (a.sem op tms')
public export
record Algebra (0 sig : Signature) where
constructor MkAlgebra
raw : RawAlgebra sig
- 0 relation : IRel raw.U
- algebra : IsAlgebra sig raw relation
+ algebra : IsAlgebra sig raw
+
+public export 0
+(.relation) : (0 a : Algebra sig) -> (t : sig.T) -> Rel (a.raw.U t)
+(.relation) a = IndexedEquivalence.relation a.algebra.equivalence
public export
-(.setoid) : Algebra sig -> ISetoid sig.T
-(.setoid) a = MkISetoid a.raw.U a.relation a.algebra.equivalence
+(.setoid) : Algebra sig -> IndexedSetoid sig.T
+(.setoid) a = MkIndexedSetoid a.raw.U a.algebra.equivalence
public export
(.rawWithRelation) : Algebra sig -> RawAlgebraWithRelation sig
@@ -69,7 +73,7 @@ public export
record Homomorphism {0 sig : Signature} (a, b : Algebra sig)
where
constructor MkHomomorphism
- func : IFunc a.raw.U b.raw.U
+ func : (t : sig.T) -> a.raw.U t -> b.raw.U t
homo : IsHomomorphism a b func
public export
@@ -77,7 +81,7 @@ idIsHomo : {a : Algebra sig} -> IsHomomorphism a a (\_ => Basics.id)
idIsHomo = MkIsHomomorphism
(\_ => id)
(\op, tms =>
- (a.algebra.equivalence _).equalImpliesEq $
+ reflect (index a.setoid _) $
sym $
cong (a.raw.sem op) $
mapId tms)
@@ -87,19 +91,17 @@ idHomo : {a : Algebra sig} -> Homomorphism a a
idHomo = MkHomomorphism _ idIsHomo
public export
-compIsHomo : {a, b, c : Algebra sig} -> {f : IFunc b.raw.U c.raw.U} -> {g : IFunc a.raw.U b.raw.U}
+compIsHomo : {a, b, c : Algebra sig}
+ -> {f : (t : sig.T) -> b.raw.U t -> c.raw.U t} -> {g : (t : sig.T) -> a.raw.U t -> b.raw.U t}
-> IsHomomorphism b c f -> IsHomomorphism a b g -> IsHomomorphism a c (\i => f i . g i)
compIsHomo fHomo gHomo = MkIsHomomorphism
- (\t => fHomo.cong t . gHomo.cong t)
- (\op, tms =>
- (c.algebra.equivalence _).transitive
- (fHomo.cong _ $ gHomo.semHomo op tms) $
- (c.algebra.equivalence _).transitive
- (fHomo.semHomo op (map g tms)) $
- (c.algebra.equivalence _).equalImpliesEq $
- sym $
- cong (c.raw.sem op) $
- mapComp tms)
+ { cong = \t => fHomo.cong t . gHomo.cong t
+ , semHomo = \op, tms => CalcWith (index c.setoid _) $
+ |~ f _ (g _ (a.raw.sem op tms))
+ ~~ f _ (b.raw.sem op (map g tms)) ...(fHomo.cong _ $ gHomo.semHomo op tms)
+ ~~ c.raw.sem op (map f (map g tms)) ...(fHomo.semHomo op _)
+ ~~ c.raw.sem op (map (\i => f i . g i) tms) .=<(cong (c.raw.sem op) $ mapComp tms)
+ }
public export
compHomo : {a, b, c : Algebra sig} -> Homomorphism b c -> Homomorphism a b -> Homomorphism a c
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 4a51f94..806d192 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -1,6 +1,5 @@
module Soat.FirstOrder.Term
-import Data.Morphism.Indexed
import Data.Setoid.Indexed
import Soat.Data.Product
@@ -16,10 +15,12 @@ data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where
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
+bindTerm : {auto a : RawAlgebra sig} -> (f : (t : sig.T) -> v t -> a.U t)
+ -> {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
+bindTerms : {auto a : RawAlgebra sig} -> ((t : sig.T) -> v t -> a.U t)
+ -> {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)
@@ -29,7 +30,7 @@ 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)
+ -> (env : (t : sig.T) -> v t -> a.U t) -> {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)
@@ -37,13 +38,13 @@ bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env t)) (bindTermsIsMap env
-- FIXME: these names shouldn't be public. Indication of bad API design
namespace Rel
public export
- data (~=~) : forall v . (0 r : IRel v) -> IRel (Term sig v)
+ data (~=~) : forall v . (0 r : (t : _) -> Rel (v t)) -> (t : _) -> Rel (Term sig v t)
where
- Done' : {0 v : sig.T -> Type} -> {0 r : IRel v}
+ Done' : {0 v : sig.T -> Type} -> {0 r : (t : _) -> Rel (v t)}
-> {t : sig.T} -> {i, j : v t}
-> r t i j
-> (~=~) {sig} {v} r t (Done i) (Done j)
- Call' : {0 v : sig.T -> Type} -> {0 r : IRel v}
+ Call' : {0 v : sig.T -> Type} -> {0 r : (t : _) -> Rel (v t)}
-> {t : sig.T} -> (op : Op sig t) -> {tms, tms' : Term sig v ^ op.arity}
-> Pointwise ((~=~) {sig} {v} r) tms tms'
-> (~=~) {sig} {v} r t (Call op tms) (Call op tms')
@@ -61,36 +62,42 @@ namespace Rel
tmsRelEqualIsEqual (eq :: eqs) = cong2 (::) (tmRelEqualIsEqual eq) (tmsRelEqualIsEqual eqs)
public export
- tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
+ tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : (t : _) -> Rel (V t)}
+ -> ((t : sig.T) -> (x : V t) -> rel t x x)
-> {t : sig.T} -> (tm : Term sig V t) -> (~=~) rel t tm tm
public export
- tmsRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
+ tmsRelRefl : {0 V : sig.T -> Type} -> {0 rel : (t : _) -> Rel (V t)}
+ -> ((t : sig.T) -> (x : V t) -> rel t x x)
-> {ts : List sig.T} -> (tms : Term sig V ^ ts) -> Pointwise ((~=~) rel) tms tms
- tmRelRefl refl (Done i) = Done' reflexive
+ tmRelRefl refl (Done i) = Done' $ refl _ i
tmRelRefl refl (Call op ts) = Call' op (tmsRelRefl refl ts)
tmsRelRefl refl [] = []
tmsRelRefl refl (t :: ts) = tmRelRefl refl t :: tmsRelRefl refl ts
public export
- tmRelReflexive : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
+ tmRelReflexive : {0 V : sig.T -> Type} -> {0 rel : (t : _) -> Rel (V t)}
+ -> ((t : sig.T) -> (x : V t) -> rel t x x)
-> {t : sig.T} -> {tm, tm' : Term sig V t} -> tm = tm' -> (~=~) rel t tm tm'
tmRelReflexive refl Refl = tmRelRefl refl _
public export
- tmsRelReflexive : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
+ tmsRelReflexive : {0 V : sig.T -> Type} -> {0 rel : (t : _) -> Rel (V t)}
+ -> ((t : sig.T) -> (x : V t) -> rel t x x)
-> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts}
-> tms = tms' -> Pointwise ((~=~) rel) tms tms'
tmsRelReflexive refl Refl = tmsRelRefl refl _
public export
- tmRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
+ tmRelSym : {0 V : sig.T -> Type} -> {0 rel : (t : _) -> Rel (V t)}
+ -> ((t : sig.T) -> Symmetric (V t) (rel t))
-> {t : sig.T} -> {tm, tm' : Term sig V t} -> (~=~) rel t tm tm' -> (~=~) rel t tm' tm
public export
- tmsRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
+ tmsRelSym : {0 V : sig.T -> Type} -> {0 rel : (t : _) -> Rel (V t)}
+ -> ((t : sig.T) -> Symmetric (V t) (rel t))
-> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts}
-> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms
@@ -101,12 +108,14 @@ namespace Rel
tmsRelSym sym (t :: ts) = tmRelSym sym t :: tmsRelSym sym ts
public export
- tmRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
+ tmRelTrans : {0 V : sig.T -> Type} -> {0 rel : (t : _) -> Rel (V t)}
+ -> ((t : sig.T) -> Transitive (V t) (rel t))
-> {t : sig.T} -> {tm, tm', tm'' : Term sig V t}
-> (~=~) rel t tm tm' -> (~=~) rel t tm' tm'' -> (~=~) rel t tm tm''
public export
- tmsRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
+ tmsRelTrans : {0 V : sig.T -> Type} -> {0 rel : (t : _) -> Rel (V t)}
+ -> ((t : sig.T) -> Transitive (V t) (rel t))
-> {ts : List sig.T} -> {tms, tms', tms'' : Term sig V ^ ts}
-> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms''
-> Pointwise ((~=~) rel) tms tms''
@@ -117,34 +126,37 @@ namespace Rel
tmsRelTrans trans [] [] = []
tmsRelTrans trans (t :: ts) (t' :: ts') = tmRelTrans trans t t' :: tmsRelTrans trans ts ts'
- export
- tmRelEq : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IEquivalence V rel
- -> IEquivalence _ ((~=~) {sig = sig} {v = V} rel)
- tmRelEq eq t = MkEquivalence
- (MkReflexive $ tmRelRefl (\t => (eq t).refl) _)
- (MkSymmetric $ tmRelSym (\t => (eq t).sym))
- (MkTransitive $ tmRelTrans (\t => (eq t).trans))
+ public export
+ tmRelEq : IndexedEquivalence sig.T v -> IndexedEquivalence sig.T (Term sig v)
+ tmRelEq eq = MkIndexedEquivalence
+ { relation = (~=~) {sig, v} eq.relation
+ , reflexive = \t => tmRelRefl eq.reflexive
+ , symmetric = \t, _, _ => tmRelSym (\t => MkSymmetric $ eq.symmetric t _ _)
+ , transitive = \t, _, _, _ => tmRelTrans (\t => MkTransitive $ eq.transitive t _ _ _)
+ }
public export
Free : (0 V : sig.T -> Type) -> RawAlgebra sig
Free v = MakeRawAlgebra (Term sig v) Call
public export
-FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U) ((~=~) v.relation)
+FreeIsAlgebra : (v : IndexedSetoid sig.T) -> IsAlgebra sig (Free v.U)
FreeIsAlgebra v = MkIsAlgebra (tmRelEq v.equivalence) Call'
public export
-FreeAlgebra : ISetoid sig.T -> Algebra sig
-FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v)
+FreeAlgebra : IndexedSetoid sig.T -> Algebra sig
+FreeAlgebra v = MkAlgebra _ (FreeIsAlgebra v)
public export
-bindTermCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}
+bindTermCong' : {a : Algebra sig} -> {env, env' : (t : sig.T) -> v t -> a.raw.U t}
+ -> {0 rel : (t : _) -> Rel (v t)}
-> (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')
public export
-bindTermsCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}
+bindTermsCong' : {a : Algebra sig} -> {env, env' : (t : sig.T) -> v t -> a.raw.U t}
+ -> {0 rel : (t : _) -> Rel (v t)}
-> (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')
@@ -156,50 +168,51 @@ bindTermsCong' cong [] = []
bindTermsCong' cong (t :: ts) = bindTermCong' cong t :: bindTermsCong' cong ts
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')
-bindTermCong env = bindTermCong' env.cong
+bindTermCong : {a : Algebra sig} -> (env : v ~> a.setoid)
+ -> {t : sig.T} -> {tm, tm' : Term sig v.U t} -> (~=~) v.equivalence.relation t tm tm'
+ -> a.relation t (bindTerm {a = a.raw} env.H tm) (bindTerm {a = a.raw} env.H tm')
+bindTermCong env = bindTermCong' env.homomorphic
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'
+bindTermsCong : {a : Algebra sig} -> (env : v ~> a.setoid)
+ -> {ts : List sig.T} -> {tms, tms' : Term sig v.U ^ ts}
+ -> Pointwise ((~=~) v.equivalence.relation) tms tms'
-> Pointwise a.relation
- (bindTerms {a = a.raw} env.func tms)
- (bindTerms {a = a.raw} env.func tms')
-bindTermsCong env = bindTermsCong' env.cong
+ (bindTerms {a = a.raw} env.H tms)
+ (bindTerms {a = a.raw} env.H tms')
+bindTermsCong env = bindTermsCong' env.homomorphic
public export
-bindIsHomo : (a : Algebra sig) -> (env : IFunction v a.setoid)
- -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.func)
+bindIsHomo : (a : Algebra sig) -> (env : v ~> a.setoid)
+ -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.H)
bindIsHomo a env = MkIsHomomorphism
(\t, eq => bindTermCong env eq)
(\op, tms =>
a.algebra.semCong op $
- map (\t => (a.algebra.equivalence t).equalImpliesEq) $
+ map (\t => reflect $ index a.setoid t) $
equalImpliesPwEq $
- bindTermsIsMap {a = a.raw} env.func tms)
+ bindTermsIsMap {a = a.raw} env.H tms)
public export
-bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> Homomorphism (FreeAlgebra v) a
+bindHomo : {a : Algebra sig} -> (env : v ~> a.setoid) -> Homomorphism (FreeAlgebra v) a
bindHomo env = MkHomomorphism _ (bindIsHomo _ env)
public export
-bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
+bindUnique' : {v : IndexedSetoid 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' : {v : IndexedSetoid 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)
-> 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) = CalcWith (a.setoid.index _) $
+bindUnique' f g cong (Call op ts) = CalcWith (index a.setoid _) $
|~ 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 )
@@ -209,20 +222,20 @@ 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)
+bindUnique : {v : IndexedSetoid sig.T} -> {a : Algebra sig} -> (env : v ~> a.setoid)
-> (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))
+ -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.H 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.H tm)
bindUnique env f = bindUnique' f (bindHomo env)
public export
-bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
+bindsUnique : {v : IndexedSetoid sig.T} -> {a : Algebra sig} -> (env : v ~> a.setoid)
-> (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))
+ -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.H 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.H 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.H) ts ...( bindsUnique' f (bindHomo env) cong ts )
+ ~~ bindTerms {a = a.raw} env.H ts .=<( bindTermsIsMap {a = a.raw} env.H ts )
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 05:42:24 +0000