Prove more properties of (~=~)

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