diff options
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index be6ab86..2013876 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -47,6 +47,16 @@ namespace Rel -> Pointwise ((~=~) {sig} {v} r) tms tms' -> (~=~) {sig} {v} r t (Call op tms) (Call op tms') + tmRelEqualIsEqual : (~=~) (\_ => Equal) t tm tm' -> tm = tm' + + tmsRelEqualIsEqual : Pointwise ((~=~) (\_ => Equal)) tms tms' -> tms = tms' + + tmRelEqualIsEqual (Done' eq) = cong Done eq + tmRelEqualIsEqual (Call' op eqs) = cong (Call op) $ tmsRelEqualIsEqual eqs + + tmsRelEqualIsEqual [] = Refl + tmsRelEqualIsEqual (eq :: eqs) = cong2 (::) (tmRelEqualIsEqual eq) (tmsRelEqualIsEqual eqs) + tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel -> {t : sig.T} -> (tm : Term sig V t) -> (~=~) rel t tm tm @@ -59,6 +69,15 @@ namespace Rel tmsRelRefl refl [] = [] tmsRelRefl refl (t :: ts) = tmRelRefl refl t :: tmsRelRefl refl ts + tmRelReflexive : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel + -> {t : sig.T} -> {tm, tm' : Term sig V t} -> tm = tm' -> (~=~) rel t tm tm' + tmRelReflexive refl Refl = tmRelRefl refl _ + + tmsRelReflexive : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel + -> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts} + -> tms = tms' -> Pointwise ((~=~) rel) tms tms' + tmsRelReflexive refl Refl = tmsRelRefl refl _ + tmRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel) -> {t : sig.T} -> {tm, tm' : Term sig V t} -> (~=~) rel t tm tm' -> (~=~) rel t tm' tm |