summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--soat.ipkg8
-rw-r--r--src/Data/Morphism/Indexed.idr13
-rw-r--r--src/Data/Setoid.idr55
-rw-r--r--src/Data/Setoid/Indexed.idr44
-rw-r--r--src/Soat/Data/Product.idr54
-rw-r--r--src/Soat/FirstOrder/Algebra.idr48
-rw-r--r--src/Soat/FirstOrder/Term.idr119
-rw-r--r--src/Soat/SecondOrder/Algebra.idr99
-rw-r--r--src/Soat/SecondOrder/Algebra/Lift.idr658
-rw-r--r--src/Syntax/PreorderReasoning/Setoid.idr55
10 files changed, 563 insertions, 590 deletions
diff --git a/soat.ipkg b/soat.ipkg
index d5cdcd9..d0eaffc 100644
--- a/soat.ipkg
+++ b/soat.ipkg
@@ -2,10 +2,9 @@ package soat
authors = "Greg Brown"
sourcedir = "src"
-modules = Data.Morphism.Indexed
- , Data.Setoid
- , Data.Setoid.Either
- , Data.Setoid.Indexed
+depends = setoid
+
+modules = Data.Setoid.Either
, Soat.Data.Product
, Soat.Data.Sublist
, Soat.FirstOrder.Algebra
@@ -16,4 +15,3 @@ modules = Data.Morphism.Indexed
, Soat.SecondOrder.Algebra.Lift
, Soat.SecondOrder.Signature
, Soat.SecondOrder.Signature.Lift
- , Syntax.PreorderReasoning.Setoid
diff --git a/src/Data/Morphism/Indexed.idr b/src/Data/Morphism/Indexed.idr
deleted file mode 100644
index c271c90..0000000
--- a/src/Data/Morphism/Indexed.idr
+++ /dev/null
@@ -1,13 +0,0 @@
-module Data.Morphism.Indexed
-
-import Data.Setoid.Indexed
-
-public export
-IFunc : {a : Type} -> (x, y : a -> Type) -> Type
-IFunc {a} x y = (i : a) -> x i -> y i
-
-public export
-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)
diff --git a/src/Data/Setoid.idr b/src/Data/Setoid.idr
deleted file mode 100644
index 8014bac..0000000
--- a/src/Data/Setoid.idr
+++ /dev/null
@@ -1,55 +0,0 @@
-module Data.Setoid
-
-import public Control.Relation
-
-%default total
-
-public export
-record Equivalence a (rel : Rel a) where
- constructor MkEquivalence
- refl : Reflexive a rel
- sym : Symmetric a rel
- trans : Transitive a rel
-
-public export
-record Setoid where
- constructor MkSetoid
- 0 U : Type
- 0 relation : Rel U
- equivalence : Data.Setoid.Equivalence U relation
-
-public export
-equiv : Control.Relation.Equivalence a rel => Data.Setoid.Equivalence a rel
-equiv = MkEquivalence (MkReflexive reflexive) (MkSymmetric symmetric) (MkTransitive transitive)
-
-public export
-[refl'] (eq : Data.Setoid.Equivalence a rel) => Reflexive a rel where
- reflexive = reflexive @{eq.refl}
-
-public export
-[sym'] (eq : Data.Setoid.Equivalence a rel) => Symmetric a rel where
- symmetric = symmetric @{eq.sym}
-
-public export
-[trans'] (eq : Data.Setoid.Equivalence a rel) => Transitive a rel where
- transitive = transitive @{eq.trans}
-
-public export
-[equiv'] Data.Setoid.Equivalence a rel => Control.Relation.Equivalence a rel
- using refl' sym' trans' where
-
-public export
-(.reflexive) : Data.Setoid.Equivalence a rel -> {x : a} -> rel x x
-(.reflexive) eq = reflexive @{eq.refl}
-
-public export
-(.symmetric) : Data.Setoid.Equivalence a rel -> {x, y : a} -> rel x y -> rel y x
-(.symmetric) eq = symmetric @{eq.sym}
-
-public export
-(.transitive) : Data.Setoid.Equivalence a rel -> {x, y, z : a} -> rel x y -> rel y z -> rel x z
-(.transitive) eq = transitive @{eq.trans}
-
-public export
-(.equalImpliesEq) : Data.Setoid.Equivalence a rel -> {x, y : a} -> x = y -> rel x y
-(.equalImpliesEq) eq Refl = eq.reflexive
diff --git a/src/Data/Setoid/Indexed.idr b/src/Data/Setoid/Indexed.idr
deleted file mode 100644
index 7277932..0000000
--- a/src/Data/Setoid/Indexed.idr
+++ /dev/null
@@ -1,44 +0,0 @@
-module Data.Setoid.Indexed
-
-import public Data.Setoid
-
-%default total
-
-public export
-IRel : {a : Type} -> (a -> Type) -> Type
-IRel {a = a} x = (i : a) -> x i -> x i -> Type
-
-public export
-IReflexive : {a : Type} -> (x : a -> Type) -> IRel x -> Type
-IReflexive x rel = (i : a) -> Reflexive (x i) (rel i)
-
-public export
-ISymmetric : {a : Type} -> (x : a -> Type) -> IRel x -> Type
-ISymmetric x rel = (i : a) -> Symmetric (x i) (rel i)
-
-public export
-ITransitive : {a : Type} -> (x : a -> Type) -> IRel x -> Type
-ITransitive x rel = (i : a) -> Transitive (x i) (rel i)
-
-public export
-IEquivalence : {a : Type} -> (x : a -> Type) -> IRel x -> Type
-IEquivalence x rel = (i : a) -> Setoid.Equivalence (x i) (rel i)
-
-public export
-record ISetoid (a : Type) where
- constructor MkISetoid
- 0 U : a -> Type
- 0 relation : IRel U
- equivalence : IEquivalence U relation
-
-public export
-fromIndexed : (a -> Setoid) -> ISetoid a
-fromIndexed x = MkISetoid (\i => (x i).U) (\i => (x i).relation) (\i => (x i).equivalence)
-
-public export
-(.index) : ISetoid a -> a -> Setoid
-(.index) x i = MkSetoid (x.U i) (x.relation i) (x.equivalence i)
-
-public export
-isetoid : (a -> Type) -> ISetoid a
-isetoid u = MkISetoid u (\_ => Equal) (\_ => equiv)
diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
index 0cb5dda..3a5d96c 100644
--- a/src/Soat/Data/Product.idr
+++ b/src/Soat/Data/Product.idr
@@ -1,8 +1,7 @@
module Soat.Data.Product
import Data.List.Elem
-import Data.Morphism.Indexed
-import Data.Setoid.Indexed
+import Data.Setoid.Indexed.Definition
%default total
@@ -68,7 +67,7 @@ map f [] = []
map f (x :: xs) = f _ x :: map f xs
public export
-indexMap : {0 f : IFunc x y} -> (xs : x ^ is) -> (elem : Elem i is)
+indexMap : forall x, y . {0 f : (i : a) -> x i -> y i} -> (xs : x ^ is) -> (elem : Elem i is)
-> index (map f xs) elem = f i (index xs elem)
indexMap (x :: xs) Here = Refl
indexMap (x :: xs) (There elem) = indexMap xs elem
@@ -79,8 +78,8 @@ mapId [] = Refl
mapId (x :: xs) = cong ((::) x) $ mapId xs
public export
-mapComp : {0 f : IFunc y z} -> {0 g : IFunc x y} -> (xs : x ^ is)
- -> map (\i => f i . g i) xs = map f (map g xs)
+mapComp : forall x, y, z . {0 f : (i : a) -> y i -> z i} -> {0 g : (i : a) -> x i -> y i}
+ -> (xs : x ^ is) -> map (\i => f i . g i) xs = map f (map g xs)
mapComp [] = Refl
mapComp (x :: xs) = cong ((::) (f _ (g _ x))) $ mapComp xs
@@ -95,7 +94,7 @@ wrap f [] = []
wrap f (x :: xs) = x :: wrap f xs
public export
-mapWrap : {0 f : IFunc x y} -> (0 g : a -> b) -> (xs : (x . g) ^ is)
+mapWrap : forall x, y . {0 f : (i : b) -> x i -> y i} -> (0 g : a -> b) -> (xs : (x . g) ^ is)
-> map f (wrap g xs) = wrap g (map (\i => f (g i)) xs)
mapWrap g [] = Refl
mapWrap g (x :: xs) = cong ((::) (f (g _) x)) $ mapWrap g xs
@@ -106,7 +105,8 @@ unwrap f {is = []} [] = []
unwrap f {is = (i :: is)} (x :: xs) = x :: unwrap f xs
public export
-mapUnwrap : {0 f : IFunc x y} -> (0 g : a -> b) -> {is : _} -> (xs : x ^ map g is)
+mapUnwrap : forall x, y . {0 f : (i : b) -> x i -> y i} -> (0 g : a -> b)
+ -> {is : _} -> (xs : x ^ map g is)
-> map (\i => f (g i)) {is} (unwrap g xs) = unwrap g {is} (map f xs)
mapUnwrap g {is = []} [] = Refl
mapUnwrap g {is = (i :: is)} (x :: xs) = cong (Product.(::) (f (g i) x)) $ mapUnwrap g xs
@@ -166,16 +166,16 @@ namespace Pointwise
public export
pwRefl : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-> ((i : a) -> Reflexive (x i) (rel i))
- -> {is : List a} -> {xs : x ^ is} -> Pointwise rel xs xs
- pwRefl f {xs = []} = []
- pwRefl f {xs = (x :: xs)} = reflexive :: pwRefl f
+ -> {is : List a} -> (xs : x ^ is) -> Pointwise rel xs xs
+ pwRefl f [] = []
+ pwRefl f (x :: xs) = reflexive :: pwRefl f xs
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
+ pwReflexive refl Refl = pwRefl refl _
public export
pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
@@ -193,44 +193,50 @@ namespace Pointwise
pwTrans f (r :: rs) (s :: ss) = transitive r s :: pwTrans f rs ss
public export
- pwEquivalence : IEquivalence x rel -> {is : _} -> Setoid.Equivalence (x ^ is) (Pointwise rel)
+ pwEquivalence : IndexedEquivalence a x -> {is : _} -> Equivalence (x ^ is)
pwEquivalence eq = MkEquivalence
- (MkReflexive $ pwRefl (\i => (eq i).refl))
- (MkSymmetric $ pwSym (\i => (eq i).sym))
- (MkTransitive $ pwTrans (\i => (eq i).trans))
+ { relation = Pointwise eq.relation
+ , reflexive = pwRefl (\i => MkReflexive $ eq.reflexive i _)
+ , symmetric = \_, _ => pwSym (\i => MkSymmetric $ eq.symmetric i _ _)
+ , transitive = \_, _, _ => pwTrans (\i => MkTransitive $ eq.transitive i _ _ _)
+ }
public export
- pwSetoid : ISetoid a -> List a -> Setoid
- pwSetoid x is = MkSetoid (x.U ^ is) _ (pwEquivalence x.equivalence)
+ pwSetoid : IndexedSetoid a -> List a -> Setoid
+ pwSetoid x is = MkSetoid (x.U ^ is) (pwEquivalence x.equivalence)
-- Introductors and Eliminators
public export
- mapIntro'' : forall x, y . {0 rel : IRel x} -> {0 rel' : IRel y} -> {0 f, g : IFunc x y}
+ mapIntro'' : forall x, y . {0 rel : (i : a) -> Rel (x i)} -> {0 rel' : (i : a) -> Rel (y i)}
+ -> {0 f, g : (i : a) -> x i -> y i}
-> (cong : (i : a) -> (u, v : x i) -> rel i u v -> rel' i (f i u) (g i v))
-> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys)
mapIntro'' cong [] = []
mapIntro'' cong (r :: rs) = cong _ _ _ r :: mapIntro'' cong rs
public export
- mapIntro' : forall x, y . {0 rel : IRel x} -> {0 rel' : IRel y} -> {0 f, g : IFunc x y}
+ mapIntro' : forall x, y . {0 rel : (i : a) -> Rel (x i)} -> {0 rel' : (i : a) -> Rel (y i)}
+ -> {0 f, g : (i : a) -> x i -> y i}
-> (cong : (i : a) -> {u, v : x i} -> rel i u v -> rel' i (f i u) (g i v))
-> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys)
mapIntro' cong = mapIntro'' (\t, _, _ => cong t)
public export
- mapIntro : (f : IFunction x y) -> {is : _} -> {xs, ys : x.U ^ is}
- -> Pointwise x.relation xs ys -> Pointwise y.relation (map f.func xs) (map f.func ys)
- mapIntro f = mapIntro' f.cong
+ mapIntro : (f : x ~> y) -> {is : _} -> {xs, ys : x.U ^ is}
+ -> Pointwise x.equivalence.relation xs ys
+ -> Pointwise y.equivalence.relation (map f.H xs) (map f.H ys)
+ mapIntro f = mapIntro' f.homomorphic
public export
- wrapIntro : forall f . {0 rel : IRel x} -> {0 xs, ys : (x . f) ^ is}
+ wrapIntro : forall f . {0 rel : (i : a) -> Rel (x i)} -> {0 xs, ys : (x . f) ^ is}
-> Pointwise (\i => rel (f i)) xs ys -> Pointwise rel (wrap f xs) (wrap f ys)
wrapIntro [] = []
wrapIntro (r :: rs) = r :: wrapIntro rs
public export
- unwrapIntro : {0 f : a -> b} -> {0 rel : IRel x} -> {is : List a} -> {0 xs, ys : x ^ map f is}
+ unwrapIntro : {0 f : a -> b} -> {0 rel : (i : b) -> Rel (x i)} -> {is : List a}
+ -> {0 xs, ys : x ^ map f is}
-> Pointwise rel xs ys -> Pointwise (\i => rel (f i)) {is = is} (unwrap f xs) (unwrap f ys)
unwrapIntro {is = []} [] = []
unwrapIntro {is = (i :: is)} (r :: rs) = r :: unwrapIntro rs
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 )
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index c506c85..5dd53c5 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -1,6 +1,5 @@
module Soat.SecondOrder.Algebra
-import Data.Morphism.Indexed
import Data.Setoid.Indexed
import Data.List.Elem
@@ -13,11 +12,17 @@ extend : (U : a -> List a -> Type) -> (ctx : List a) -> Pair (List a) a -> Type
extend x ctx ty = x (snd ty) (fst ty ++ ctx)
public export
-extendRel : {U : a -> List a -> Type} -> (rel : IRel (uncurry U))
- -> (ctx : List a) -> IRel (extend U ctx)
+extendRel : {0 U : a -> List a -> Type} -> (rel : (ty : _) -> Rel (uncurry U ty))
+ -> (ctx : List a) -> (ty : _) -> Rel (extend U ctx ty)
extendRel rel ctx ty = rel (snd ty, fst ty ++ ctx)
public export
+extendFunc : {0 U, V : a -> List a -> Type}
+ -> (f : (t : a) -> (ctx : List a) -> U t ctx -> V t ctx)
+ -> (ctx : List a) -> (ty : Pair (List a) a) -> extend U ctx ty -> extend V ctx ty
+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
@@ -30,100 +35,108 @@ record RawAlgebra (0 sig : Signature) where
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
+ -> forall ctx' . (tm : U t ctx') -> (tms : (\t => U t ctx) ^ ctx') -> U t ctx
+
+public export
+(.extendSubst) : (a : RawAlgebra sig) -> (ctx : _) -> {ctx' : _}
+ -> (tms : (\t => a.U t ctx) ^ ctx') -> (ty : _) -> extend a.U ctx' ty -> extend a.U ctx ty
+a .extendSubst ctx tms ty tm = a.subst
+ (snd ty)
+ (fst ty ++ ctx)
+ tm
+ (tabulate {is = fst ty} (a.var . elemJoinL {ys = ctx}) ++
+ map (\t => a.rename t ([] {ys = fst ty} ++ reflexive {x = ctx})) tms)
public export
-record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncurry a.U)) where
+record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
constructor MkIsAlgebra
- equivalence : IEquivalence (uncurry a.U) rel
+ equivalence : IndexedEquivalence (Pair sig.T (List sig.T)) (uncurry a.U)
-- Congruences
renameCong : (t : sig.T) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx')
- -> {tm, tm' : a.U t ctx} -> rel (t, ctx) tm tm'
- -> rel (t, ctx') (a.rename t f tm) (a.rename t f tm')
+ -> {tm, tm' : a.U t ctx} -> equivalence.relation (t, ctx) tm tm'
+ -> equivalence.relation (t, ctx') (a.rename t f tm) (a.rename t f tm')
semCong : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
-> {tms, tms' : extend a.U ctx ^ op.arity}
- -> Pointwise (extendRel {U = a.U} rel ctx) tms tms'
- -> rel (t, ctx) (a.sem ctx op tms) (a.sem ctx op tms')
+ -> Pointwise (extendRel {U = a.U} equivalence.relation ctx) tms tms'
+ -> equivalence.relation (t, ctx) (a.sem ctx op tms) (a.sem ctx op tms')
substCong : (t : sig.T) -> (ctx : List sig.T)
- -> {ctx' : _} -> {tm, tm' : a.U t ctx'} -> rel (t, ctx') tm tm'
- -> {tms, tms' : (\t => a.U t ctx) ^ ctx'} -> Pointwise (\t => rel (t, ctx)) tms tms'
- -> rel (t, ctx) (a.subst t ctx tm tms) (a.subst t ctx tm' tms')
+ -> {ctx' : _} -> {tm, tm' : a.U t ctx'} -> equivalence.relation (t, ctx') tm tm'
+ -> {tms, tms' : (\t => a.U t ctx) ^ ctx'}
+ -> Pointwise (\t => equivalence.relation (t, ctx)) tms tms'
+ -> equivalence.relation (t, ctx) (a.subst t ctx tm tms) (a.subst t ctx tm' tms')
-- rename is functorial
renameId : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
- -> rel (t, ctx) (a.rename t {ctx = ctx} Relation.reflexive tm) tm
+ -> equivalence.relation (t, ctx) (a.rename t {ctx = ctx} Relation.reflexive tm) tm
renameComp : (t : sig.T) -> {ctx, ctx', ctx'' : _}
-> (f : ctx' `Sublist` ctx'') -> (g : ctx `Sublist` ctx')
-> (tm : a.U t ctx)
- -> rel (t, ctx'') (a.rename t (transitive g f) tm) (a.rename t f $ a.rename t g tm)
+ -> equivalence.relation (t, ctx'')
+ (a.rename t (transitive g f) tm)
+ (a.rename t f $ a.rename t g tm)
-- sem are natural transformation
semNat : {ctx, ctx' : _} -> (f : ctx `Sublist` ctx') -> {t : sig.T} -> (op : Op sig t)
-> (tms : extend a.U ctx ^ op.arity)
- -> rel (t, ctx')
+ -> equivalence.relation (t, ctx')
(a.rename t f $ a.sem ctx op tms)
(a.sem ctx' op $
map (\ty => a.rename (snd ty) (Relation.reflexive {x = fst ty} ++ f)) $
tms)
-- var is natural transformation
varNat : {t : _} -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx') -> (i : Elem t ctx)
- -> rel (t, ctx') (a.rename t f $ a.var i) (a.var $ curry f i)
+ -> equivalence.relation (t, ctx') (a.rename t f $ a.var i) (a.var $ curry f i)
-- subst is natural transformation
substNat : (t : sig.T) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx')
-> {ctx'' : _} -> (tm : a.U t ctx'') -> (tms : (\t => a.U t ctx) ^ ctx'')
- -> rel (t, ctx')
+ -> equivalence.relation (t, ctx')
(a.rename t f $ a.subst t ctx tm tms)
(a.subst t ctx' tm $ map (\t => a.rename t f) tms)
-- subst is extranatural transformation
substExnat : (t : sig.T) -> (ctx : List sig.T)
-> {ctx', ctx'' : _} -> (f : ctx' `Sublist` ctx'')
-> (tm : a.U t ctx') -> (tms : (\t => a.U t ctx) ^ ctx'')
- -> rel (t, ctx) (a.subst t ctx (a.rename t f tm) tms) (a.subst t ctx tm (shuffle f tms))
+ -> equivalence.relation (t, ctx)
+ (a.subst t ctx (a.rename t f tm) tms)
+ (a.subst t ctx tm (shuffle f tms))
-- var, subst is a monoid
substComm : (t : sig.T) -> (ctx : List sig.T)
-> {ctx', ctx'' : _} -> (tm : a.U t ctx'')
-> (tms : (\t => a.U t ctx') ^ ctx'') -> (tms' : (\t => a.U t ctx) ^ ctx')
- -> rel (t, ctx)
+ -> equivalence.relation (t, ctx)
(a.subst t ctx (a.subst t ctx' tm tms) tms')
(a.subst t ctx tm $ map (\t, tm => a.subst t ctx tm tms') tms)
substVarL : {t : _} -> (ctx : List sig.T) -> {ctx' : _} -> (i : Elem t ctx')
-> (tms : (\t => a.U t ctx) ^ ctx')
- -> rel (t, ctx) (a.subst t ctx (a.var i) tms) (index tms i)
+ -> equivalence.relation (t, ctx) (a.subst t ctx (a.var i) tms) (index tms i)
substVarR : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
- -> rel (t, ctx) (a.subst t ctx {ctx' = ctx} tm $ tabulate a.var) tm
+ -> equivalence.relation (t, ctx) (a.subst t ctx {ctx' = ctx} tm $ tabulate a.var) tm
-- sem, var and subst are compatible
substCompat : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
-> {ctx' : _} -> (tms : extend a.U ctx' ^ op.arity) -> (tms' : (\t => a.U t ctx) ^ ctx')
- -> rel (t, ctx)
+ -> equivalence.relation (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
constructor MkAlgebra
raw : RawAlgebra sig
- 0 relation : IRel (uncurry raw.U)
- algebra : IsAlgebra sig raw relation
+ algebra : IsAlgebra sig raw
+
+public export 0
+(.relation) : (0 a : Algebra sig) -> (ty : _) -> Rel (uncurry a.raw.U ty)
+(.relation) a = a.algebra.equivalence.relation
public export
-(.setoid) : Algebra sig -> ISetoid (Pair sig.T (List sig.T))
-(.setoid) a = MkISetoid (uncurry a.raw.U) a.relation a.algebra.equivalence
+(.setoid) : Algebra sig -> IndexedSetoid (Pair sig.T (List sig.T))
+(.setoid) a = MkIndexedSetoid (uncurry a.raw.U) a.algebra.equivalence
public export
-(.setoidAt) : Algebra sig -> (ctx : List sig.T) -> ISetoid sig.T
-(.setoidAt) a ctx = MkISetoid
- (flip a.raw.U ctx)
- (\t => a.relation (t, ctx))
- (\_ => a.algebra.equivalence _)
+(.setoidAt) : Algebra sig -> (ctx : List sig.T) -> IndexedSetoid sig.T
+(.setoidAt) a ctx = reindex (flip MkPair ctx) a.setoid
public export
-(.varFunc) : (a : Algebra sig) -> (ctx : _) -> IFunction (isetoid (flip Elem ctx)) (a.setoidAt ctx)
-(.varFunc) a ctx = MkIFunction
- (\_ => a.raw.var)
- (\_ => (a.algebra.equivalence _).equalImpliesEq . cong a.raw.var)
+(.varFunc) : (a : Algebra sig) -> (ctx : _) -> cast (flip Elem ctx) ~> a.setoidAt ctx
+(.varFunc) a ctx = mate (\_ => a.raw.var)
public export
record IsHomomorphism
@@ -139,7 +152,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..e981593 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -1,7 +1,6 @@
module Soat.SecondOrder.Algebra.Lift
import Data.List.Elem
-import Data.Morphism.Indexed
import Data.Setoid.Indexed
import Soat.Data.Product
@@ -11,6 +10,9 @@ import Soat.FirstOrder.Term
import Soat.SecondOrder.Algebra
import Soat.SecondOrder.Signature.Lift
+import Syntax.PreorderReasoning.Setoid
+
+%ambiguity_depth 4
%default total
public export
@@ -21,31 +23,30 @@ project a ctx = MakeRawAlgebra
(\op => a.sem ctx (MkOp (Op op.op)) . wrap (MkPair []))
public export
-projectIsAlgebra : {a : _} -> forall rel . SecondOrder.Algebra.IsAlgebra (lift sig) a rel
- -> (ctx : List sig.T)
- -> FirstOrder.Algebra.IsAlgebra sig (project a ctx) (\t => rel (t, ctx))
-projectIsAlgebra a ctx = MkIsAlgebra
- (\t => a.equivalence (t, ctx))
- (\op => a.semCong ctx _ . wrapIntro)
-
-public export
projectAlgebra : SecondOrder.Algebra.Algebra (lift sig) -> (ctx : List sig.T)
-> FirstOrder.Algebra.Algebra sig
-projectAlgebra a ctx = MkAlgebra _ _ (projectIsAlgebra a.algebra ctx)
+projectAlgebra a ctx = MkAlgebra
+ { raw = project a.raw ctx
+ , algebra = MkIsAlgebra
+ { equivalence = (a.setoidAt ctx).equivalence
+ , semCong = \op => a.algebra.semCong ctx _ . wrapIntro
+ }
+ }
+
public export
projectIsHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> {f : _} -> IsHomomorphism a b f
-> (ctx : _)
-> 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 (index b.setoid _) $
+ |~ f _ _ (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,85 +58,79 @@ 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 (index a.setoid _) $
+ |~ 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 (reindex (\ty => (snd ty, fst ty ++ _)) a.setoid) _) $
+ |~ 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')))
+ { func = \t, tm => a.raw.subst t ctx tm tms
+ , homo = MkIsHomomorphism
+ { cong = \t, eq =>
+ a.algebra.substCong t ctx eq $
+ (pwSetoid (a.setoidAt _) _).equivalence.reflexive _
+ , semHomo = \op, tms' => CalcWith (index a.setoid _) $
+ |~ 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 (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid) _) $
+ |~ 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)) $
+ (pwSetoid (a.setoidAt _) _).equivalence.reflexive _))
+ }
+ }
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))
+ -> cast (flip Elem ctx) ~> (FreeAlgebra {sig = sig} (irrelevantCast (flip Elem ctx'))).setoid
+renameBodyFunc f = mate (\_ => Done . curry f)
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 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))
+ -> cast (flip Elem ts) ~> (FreeAlgebra {sig = sig} (irrelevantCast (flip Elem ctx))).setoid
+indexFunc tms = mate (\_ => 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 => bindTerm {a = Free _} (renameBodyFunc f).H)
(\_, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair []))
Done
(\_, _, t, ts => bindTerm {a = Free _} (\_ => index ts) t)
@@ -145,218 +140,331 @@ InitialIsAlgebra : (0 sig : _)
-> SecondOrder.Algebra.IsAlgebra
(lift 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'
- {a = FreeAlgebra (isetoid (flip Elem _))}
+ { equivalence = (bundle $ \(t, ctx) => index (FreeAlgebra (irrelevantCast (flip Elem ctx))).setoid t).equivalence
+ , renameCong = \t, f => bindTermCong ?renameCongEnv t
+ , semCong = \_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro
+ , substCong = \_, _, eq, eqs => bindTermCong'
+ {rel = \_ => Equal}
+ {a = FreeAlgebra (irrelevantCast (flip Elem _))}
(\t, Refl => index eqs _)
- eq)
- (\t, ctx, tm =>
- tmRelSym (\_ => MkSymmetric symmetric) $
- bindUnique (renameBodyFunc reflexive) idHomo (\i => Done' $ sym $ curryUncurry id i) $
- tm)
- (\t, f, g, tm =>
+ eq
+ , renameId = \t, ctx, tm =>
+ (FreeAlgebra (irrelevantCast (flip Elem _))).setoid.equivalence.symmetric _ _ _ $
+ bindUnique ?renameIdEnv 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)))
+ ?renameCompEnv
+ -- (ifunc (\_ => curry (transitive g f)))
+ (compHomo (bindHomo ?renameCompFunc) (bindHomo ?renameCompFunc'))
(\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 (irrelevantCast (flip Elem _))).setoid _) $
+ |~ bindTerms {a = Free _} (\_ => Done . curry f) (unwrap (MkPair []) tms)
+ ~~ map (\_ => bindTerm {a = Free _} (\_ => Done . curry f)) (unwrap (MkPair []) tms)
+ .=.(bindTermsIsMap {a = Free _} _ _)
+ ~~ map (\_ => bindTerm {a = Free _} (\_ => Done . curry (reflexive {x = []} ++ f))) (unwrap (MkPair []) tms)
+ ..<(mapIntro' (\t =>
+ bindTermCong'
+ {rel = \_ => Equal}
+ {a = FreeAlgebra (irrelevantCast (flip Elem _))}
+ (\_, Refl => Done' $ curryUncurry (curry f) _)) $
+ (pwSetoid (FreeAlgebra (irrelevantCast (flip Elem _))).setoid _).equivalence.reflexive _)
+ ~~ unwrap (MkPair []) (map (\ty => bindTerm {a = Free _} (\_ => Done . curry (reflexive {x = fst ty} ++ f))) tms)
+ .=.(mapUnwrap (MkPair []) tms)
+ , varNat = \_, _ => Done' Refl
+ , substNat = \t, f, tm, tms =>
bindUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
+ {a = FreeAlgebra (irrelevantCast (flip Elem _))}
(indexFunc _)
- (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (indexFunc tms)))
- (\i =>
- tmRelReflexive (\_ => MkReflexive reflexive) $
- sym $
- indexMap tms i)
- tm)
- (\t, ctx, f, tm, tms =>
+ (compHomo
+ (bindHomo ?substNatFunc)
+ (bindHomo (indexFunc tms)))
+ ?substNatCong
+ -- (\i =>
+ -- tmRelReflexive (\_ => MkReflexive reflexive) $
+ -- sym $
+ -- indexMap tms i)
+ tm
+ , substExnat = \t, ctx, f, tm, tms =>
bindUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
+ {a = FreeAlgebra (irrelevantCast (flip Elem _))}
(indexFunc _)
- (compHomo (bindHomo (indexFunc tms)) (bindHomo (renameBodyFunc f)))
- (\i =>
- tmRelReflexive (\_ => MkReflexive reflexive) $
- sym $
- indexShuffle f i)
- tm)
- (\t, ctx, tm, tms, tms' =>
+ (compHomo
+ (bindHomo (indexFunc tms))
+ (bindHomo ?substExnatFunc))
+ ?substExnatCong
+ -- (\i =>
+ -- tmRelReflexive (\_ => MkReflexive reflexive) $
+ -- sym $
+ -- indexShuffle f i)
+ tm
+ , substComm = \t, ctx, tm, tms, tms' =>
bindUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
+ {a = FreeAlgebra (irrelevantCast (flip Elem _))}
(indexFunc _)
- (compHomo (bindHomo (indexFunc tms')) (bindHomo (indexFunc tms)))
- (\i =>
- tmRelReflexive (\_ => MkReflexive reflexive) $
- sym $
- indexMap tms i)
- tm)
- (\_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _)
- (\t, ctx, tm =>
- tmRelSym (\_ => MkSymmetric symmetric) $
+ (compHomo
+ (bindHomo (indexFunc tms'))
+ (bindHomo (indexFunc tms)))
+ ?substCommCong
+ -- (\i =>
+ -- tmRelReflexive (\_ => MkReflexive reflexive) $
+ -- sym $
+ -- indexMap tms i)
+ tm
+ , substVarL = ?substVarL -- \_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _
+ , substVarR = \t, ctx, tm =>
+ (FreeAlgebra (irrelevantCast (flip Elem _))).setoid.equivalence.symmetric _ _ _ $
bindUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
+ {a = FreeAlgebra (irrelevantCast (flip Elem _))}
(indexFunc _)
idHomo
- (\i =>
- tmRelReflexive (\_ => MkReflexive reflexive) $
- sym $
- indexTabulate Done i)
- tm)
- (\ctx, (MkOp (Op op)), tms, tms' =>
+ ?substVarRCong
+ -- (\i =>
+ -- tmRelReflexive (\_ => MkReflexive reflexive) $
+ -- sym $
+ -- indexTabulate Done i)
+ 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 (irrelevantCast (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 (irrelevantCast (flip Elem _))}
+ (\t, Refl => CalcWith (index (FreeAlgebra (irrelevantCast (flip Elem _))).setoid _) $
+ |~ index (map (\_ => bindTerm {a = Free _} (\_ => Done . curry ([] {ys = []} ++ reflexive))) tms') _
+ ~~ bindTerm {a = Free _} (\_ => Done . curry ([] {ys = []} ++ reflexive)) (index tms' _)
+ .=.(indexMap tms' _)
+ ~~ index tms' _
+ ..<(bindUnique
+ ?substCompatEnv
+ idHomo
+ (\i => Done' $ sym $ trans (curryUncurry _ i) (curryUncurry id i))
+ (index tms' _)))) $
+ (pwSetoid (FreeAlgebra (irrelevantCast (flip Elem _))).setoid _).equivalence.reflexive $
+ unwrap (MkPair []) tms)
+ ~~ unwrap (MkPair []) (map ((Initial sig).extendSubst ctx tms') tms)
+ .=.(mapUnwrap (MkPair []) tms)
+ }
+-- InitialIsAlgebra sig = MkIsAlgebra
+-- (\(t, ctx) => tmRelEq (\_ => equiv) t)
+-- (\t, f => bindTermCong {a = FreeAlgebra (irrelevantCast (flip Elem _))} (renameBodyFunc f))
+-- (\_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro)
+-- (\_, _, eq, eqs => bindTermCong'
+-- {a = FreeAlgebra (irrelevantCast (flip Elem _))}
+-- (\t, Refl => index eqs _)
+-- eq)
+-- (\t, ctx, tm =>
+-- tmRelSym (\_ => MkSymmetric symmetric) $
+-- bindUnique (renameBodyFunc reflexive) idHomo (\i => Done' $ sym $ curryUncurry id i) $
+-- tm)
+-- (\t, f, g, tm =>
+-- tmRelSym (\_ => MkSymmetric symmetric) $
+-- bindUnique
+-- {a = FreeAlgebra (irrelevantCast (flip Elem _))}
+-- (renameBodyFunc (transitive g f))
+-- (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (renameBodyFunc g)))
+-- (\i => Done' $ sym $ curryUncurry (curry f . curry g) i) $
+-- tm)
+-- (\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 (irrelevantCast (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 = irrelevantCast (flip Elem _)}
+-- -- {a = FreeAlgebra (irrelevantCast (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 =>
+-- bindUnique
+-- {a = FreeAlgebra (irrelevantCast (flip Elem _))}
+-- (indexFunc _)
+-- (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (indexFunc tms)))
+-- (\i =>
+-- tmRelReflexive (\_ => MkReflexive reflexive) $
+-- sym $
+-- indexMap tms i)
+-- tm)
+-- (\t, ctx, f, tm, tms =>
+-- bindUnique
+-- {a = FreeAlgebra (irrelevantCast (flip Elem _))}
+-- (indexFunc _)
+-- (compHomo (bindHomo (indexFunc tms)) (bindHomo (renameBodyFunc f)))
+-- (\i =>
+-- tmRelReflexive (\_ => MkReflexive reflexive) $
+-- sym $
+-- indexShuffle f i)
+-- tm)
+-- (\t, ctx, tm, tms, tms' =>
+-- bindUnique
+-- {a = FreeAlgebra (irrelevantCast (flip Elem _))}
+-- (indexFunc _)
+-- (compHomo (bindHomo (indexFunc tms')) (bindHomo (indexFunc tms)))
+-- (\i =>
+-- tmRelReflexive (\_ => MkReflexive reflexive) $
+-- sym $
+-- indexMap tms i)
+-- tm)
+-- (\_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _)
+-- (\t, ctx, tm =>
+-- tmRelSym (\_ => MkSymmetric symmetric) $
+-- bindUnique
+-- {a = FreeAlgebra (irrelevantCast (flip Elem _))}
+-- (indexFunc _)
+-- idHomo
+-- (\i =>
+-- tmRelReflexive (\_ => MkReflexive reflexive) $
+-- sym $
+-- indexTabulate Done i)
+-- tm)
+-- (\ctx, (MkOp (Op op)), tms, tms' =>
+-- Call' (MkOp op) $
+-- tmsRelTrans (\_ => MkTransitive transitive)
+-- (tmsRelSym (\_ => MkSymmetric symmetric) $
+-- bindsUnique
+-- {a = FreeAlgebra (irrelevantCast (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 (irrelevantCast (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 _ _)
-public export
-InitialAlgebra : (0 sig : _) -> SecondOrder.Algebra.Algebra (lift sig)
-InitialAlgebra sig = MkAlgebra (Initial sig) _ (InitialIsAlgebra sig)
+-- 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
+-- freeToInitialIsHomo : (0 sig : _) -> (ctx : List sig.T)
+-- -> IsHomomorphism {sig = sig}
+-- (FreeAlgebra (irrelevantCast (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}
- (FreeAlgebra (isetoid (flip Elem ctx)))
- (projectAlgebra (InitialAlgebra sig) ctx)
-freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx)
+-- public export
+-- freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T)
+-- -> Homomorphism {sig = sig}
+-- (FreeAlgebra (irrelevantCast (flip Elem ctx)))
+-- (projectAlgebra (InitialAlgebra sig) ctx)
+-- freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx)
-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)
+-- 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)
-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'
- {v = isetoid (flip Elem _)}
- {a = projectAlgebra a _}
- (compHomo (bindHomo (a.varFunc _)) (bindHomo (renameBodyFunc f)))
- (compHomo (a.renameHomo f) (bindHomo (a.varFunc _)))
- (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i))
- (\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)
+-- 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'
+-- {v = irrelevantCast (flip Elem _)}
+-- {a = projectAlgebra a _}
+-- (compHomo (bindHomo (a.varFunc _)) (bindHomo (renameBodyFunc f)))
+-- (compHomo (a.renameHomo f) (bindHomo (a.varFunc _)))
+-- (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i))
+-- (\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 = irrelevantCast (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 = irrelevantCast (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)
-public export
-fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
- -> Homomorphism (InitialAlgebra sig) a
-fromInitialHomo a = MkHomomorphism (fromInitial a.raw) (fromInitialIsHomo a)
+-- public export
+-- fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
+-- -> Homomorphism (InitialAlgebra sig) a
+-- fromInitialHomo a = MkHomomorphism (fromInitial a.raw) (fromInitialIsHomo a)
-public export
-fromInitialUnique : {a : SecondOrder.Algebra.Algebra (lift sig)}
- -> (f : Homomorphism (InitialAlgebra sig) a)
- -> (t : sig.T) -> (ctx : List sig.T) -> (tm : Term sig (flip Elem ctx) t)
- -> a.relation (t, ctx) (f.func t ctx tm) (fromInitial a.raw t ctx tm)
-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))
- f.homo.varHomo
+-- public export
+-- fromInitialUnique : {a : SecondOrder.Algebra.Algebra (lift sig)}
+-- -> (f : Homomorphism (InitialAlgebra sig) a)
+-- -> (t : sig.T) -> (ctx : List sig.T) -> (tm : Term sig (flip Elem ctx) t)
+-- -> a.relation (t, ctx) (f.func t ctx tm) (fromInitial a.raw t ctx tm)
+-- fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique
+-- {v = irrelevantCast (flip Elem _)}
+-- {a = projectAlgebra a ctx}
+-- (a.varFunc ctx)
+-- (compHomo (projectHomo f ctx) (freeToInitialHomo sig ctx))
+-- f.homo.varHomo
diff --git a/src/Syntax/PreorderReasoning/Setoid.idr b/src/Syntax/PreorderReasoning/Setoid.idr
deleted file mode 100644
index f0480b2..0000000
--- a/src/Syntax/PreorderReasoning/Setoid.idr
+++ /dev/null
@@ -1,55 +0,0 @@
-{- Taken from https://github.com/ohad/idris-setoid -}
-
-||| Like Syntax.PreorderReasoning.Generic, but optimised for setoids
-module Syntax.PreorderReasoning.Setoid
-
-import public Data.Setoid
-
-infixl 0 ~~
-prefix 1 |~
-infix 1 ...,..<,..>,.=.,.=<,.=>
-
-public export
-data Step : (a : Setoid) -> (lhs,rhs : U a) -> Type where
- (...) : {0 a : Setoid} -> (0 y : U a) -> {0 x : U a} ->
- a.relation x y -> Step a x y
-
-public export
-data FastDerivation : (a : Setoid) -> (x, y : U a) -> Type where
- (|~) : {0 a : Setoid} -> (x : U a) -> FastDerivation a x x
- (~~) : {0 a : Setoid} -> {x, y : U a}
- -> FastDerivation a x y -> {z : U a} -> (step : Step a y z)
- -> FastDerivation a x z
-
-public export
-CalcWith : (a : Setoid) -> {0 x : U a} -> {0 y : U a} -> FastDerivation a x y ->
- a.relation x y
-CalcWith a (|~ x) = a.equivalence.reflexive
-CalcWith a ((~~) der (z ... step)) = a.equivalence.transitive
- (CalcWith a der) step
-
--- Smart constructors
-public export
-(..<) : {a : Setoid} -> (y : U a) -> {x : U a} ->
- a.relation y x -> Step a x y
-(y ..<(prf)) {x} = (y ...(a.equivalence.symmetric prf))
-
-public export
-(..>) : {0 a : Setoid} -> (0 y : U a) -> {0 x : U a} ->
- a.relation x y -> Step a x y
-(..>) = (...)
-
-public export
-(.=.) : {a : Setoid} -> (y : U a) -> {x : U a} ->
- x === y -> Step a x y
-(y .=.(Refl)) = (y ...(a.equivalence.reflexive))
-
-public export
-(.=>) : {a : Setoid} -> (y : U a) -> {x : U a} ->
- x === y -> Step a x y
-(.=>) = (.=.)
-
-public export
-(.=<) : {a : Setoid} -> (y : U a) -> {x : U a} ->
- y === x -> Step a x y
-(y .=<(Refl)) = (y ...(a.equivalence.reflexive))
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 21:14:53 +0000