Define properties of substitutions.

4 files changed, 170 insertions, 0 deletions

diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 2afc774..3b16f38 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -38,6 +38,13 @@ public export
 0 (.=.) : Rel (Fin k -> Term sig n)
 f .=. g = (i : Fin k) -> f i = g i
 
+export
+subCong : {f, g : Fin k -> Term sig n} -> f .=. g -> (t : Term sig k) -> f <$> t = g <$> t
+subCong prf (Var i) = prf i
+subCong prf (Op op ts) =
+  cong (Op op) $
+  mapExtensional (f <$>) (g <$>) (\t => subCong prf (assert_smaller ts t)) ts
+
 -- Substitution is Monadic -----------------------------------------------------
 
 export
@@ -80,6 +87,10 @@ opInjectiveLen : (prf : Op {k} op ts = Op {k = n} op' us) -> k = n
 opInjectiveLen Refl = Refl
 
 export
+opInjectiveTs' : {0 ts, us : Vect k (Term sig n)} -> (prf : Op op ts = Op op us) -> ts = us
+opInjectiveTs' Refl = Refl
+
+export
 opInjectiveTs :
   {0 ts : Vect k (Term sig n)} ->
   {0 us : Vect j (Term sig n)} ->
diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr
new file mode 100644
index 0000000..41fb906
--- /dev/null
+++ b/src/Data/Term/Property.idr
@@ -0,0 +1,143 @@
+module Data.Term.Property
+
+import Data.Term
+
+import Data.Vect.Properties.Index
+import Data.Vect.Quantifiers
+import Data.Vect.Quantifiers.Extra
+
+import Syntax.PreorderReasoning
+
+-- Definition ------------------------------------------------------------------
+
+public export
+record Property (sig : Signature) (k : Nat) where
+  constructor MkProp
+  Prop : forall n. (Fin k -> Term sig n) -> Type
+  cong : forall n. {f, g : Fin k -> Term sig n} -> f .=. g -> Prop f -> Prop g
+
+%name Property p, q
+
+-- Instances -------------------------------------------------------------------
+
+public export
+Unifies : Term sig k -> Term sig k -> Property sig k
+Unifies t u = MkProp
+  { Prop = \f => f <$> t = f <$> u
+  , cong = \cong, prf => Calc $
+    |~ _ <$> t
+    ~~ _ <$> t ..<(subCong cong t)
+    ~~ _ <$> u ...(prf)
+    ~~ _ <$> u ...(subCong cong u)
+  }
+
+public export
+All : Vect n (Property sig k) -> Property sig k
+All ps = MkProp (\f => All (\p => p.Prop f) ps) (\cong => mapRel (\p => p.cong cong))
+
+-- Equivalence -----------------------------------------------------------------
+
+public export 0
+(<=>) : Property sig k -> Property sig k -> Type
+p <=> q = forall n. (f : Fin k -> Term sig n) -> p.Prop f <=> q.Prop f
+
+-- Properties
+
+export
+unifiesSym : Unifies t u <=> Unifies u t
+unifiesSym f = MkEquivalence (\prf => sym prf) (\prf => sym prf)
+
+export
+unifiesOp :
+  {k : Nat} ->
+  {0 op : sig.Operator k} ->
+  {0 ts, us : Vect k (Term sig j)} ->
+  Unifies (Op op ts) (Op op us) <=> All (tabulate (\i => Unifies (index i ts) (index i us)))
+unifiesOp f = MkEquivalence
+  { leftToRight = \prf => tabulate (\i => Unifies (index i ts) (index i us)) (leftToRight prf)
+  , rightToLeft = \prf => irrelevantEq $ cong (Op op) $ rightToLeft prf
+  }
+  where
+  leftToRight :
+    (Unifies (Op op ts) (Op op us)).Prop f ->
+    (i : _) ->
+    f <$> index i ts = f <$> index i us
+  leftToRight prf i =
+    Calc $
+      |~ f <$> index i ts
+      ~~ index i (map (f <$>) ts) ...(sym $ indexNaturality i (f <$>) ts)
+      ~~ index i (map (f <$>) us) ...(cong (index i) $ opInjectiveTs' prf)
+      ~~ f <$> index i us         ...(indexNaturality i (f <$>) us)
+
+  rightToLeft :
+    {k : Nat} ->
+    {ts, us : Vect k (Term sig j)} ->
+    (All (tabulate (\i => Unifies (index i ts) (index i us)))).Prop f ->
+    map (f <$>) ts = map (f <$>) us
+  rightToLeft {ts = [], us = []} [] = Refl
+  rightToLeft {ts = t :: ts, us = u :: us} (prf :: prfs) = cong2 (::) prf (rightToLeft prfs)
+
+-- Nothing ---------------------------------------------------------------------
+
+public export 0
+Nothing : Property sig k -> Type
+Nothing p = forall n. (f : Fin k -> Term sig n) -> Not (p.Prop f)
+
+-- Properties
+
+export
+nothingEquiv : p <=> q -> Nothing p -> Nothing q
+nothingEquiv eq absurd f x = absurd f ((eq f).rightToLeft x)
+
+-- Extensions ------------------------------------------------------------------
+
+public export
+Extension : Property sig k -> (Fin k -> Term sig n) -> Property sig n
+Extension p f = MkProp
+  { Prop = \g => p.Prop (g . f)
+  , cong = \prf => p.cong (\i => subCong prf (f i))
+  }
+
+-- Properties
+
+export
+nothingExtends : Nothing p -> Nothing (Extension p f)
+nothingExtends absurd g x = void $ absurd (g . f) x
+
+export
+extendUnit : (p : Property sig k) -> p <=> Extension p Var
+extendUnit p f = MkEquivalence id id
+
+export
+extendAssoc :
+  (p : Property sig j) ->
+  (f : Fin j -> Term sig k) ->
+  (g : Fin k -> Term sig m) ->
+  Extension (Extension p f) g <=> Extension p (g . f)
+extendAssoc p f g h =
+  MkEquivalence
+    (p.cong (\i => subAssoc h g (f i)))
+    (p.cong (\i => sym $ subAssoc h g (f i)))
+
+export
+extendUnify :
+  (t, u : Term sig j) ->
+  (f : Fin j -> Term sig k) ->
+  (g : Fin k -> Term sig m) ->
+  Extension (Unifies t u) (g . f) <=> Extension (Unifies (f <$> t) (f <$> u)) g
+extendUnify t u f g h =
+  MkEquivalence
+    (\prf => Calc $
+      |~ (h . g) <$> (f <$> t)
+      ~~ ((h . g) . f) <$> t   ...(sym $ subAssoc (h . g) f t)
+      ~~ (h . (g . f)) <$> t   ...(subCong (\i => subAssoc h g (f i)) t)
+      ~~ (h . (g . f)) <$> u   ...(prf)
+      ~~ ((h . g) . f) <$> u   ...(sym $ subCong (\i => subAssoc h g (f i)) u)
+      ~~ (h . g) <$> (f <$> u) ...(subAssoc (h . g) f u))
+    (\prf => Calc $
+      |~ (h . (g . f)) <$> t
+      ~~ ((h . g) . f) <$> t   ...(sym $ subCong (\i => subAssoc h g (f i)) t)
+      ~~ (h . g) <$> (f <$> t) ...(subAssoc (h . g) f t)
+      ~~ (h . g) <$> (f <$> u) ...(prf)
+      ~~ ((h . g) . f) <$> u   ...(sym $ subAssoc (h . g) f u)
+      ~~ (h . (g . f)) <$> u   ...(subCong (\i => subAssoc h g (f i)) u))
diff --git a/src/Data/Vect/Quantifiers/Extra.idr b/src/Data/Vect/Quantifiers/Extra.idr
new file mode 100644
index 0000000..dc5a224
--- /dev/null
+++ b/src/Data/Vect/Quantifiers/Extra.idr
@@ -0,0 +1,14 @@
+module Data.Vect.Quantifiers.Extra
+
+import Data.Vect
+import Data.Vect.Quantifiers
+
+export
+mapRel : ((x : a) -> p x -> q x) -> {xs : Vect n a} -> All p xs -> All q xs
+mapRel f [] = []
+mapRel f (px :: pxs) = f _ px :: mapRel f pxs
+
+export
+tabulate : {n : Nat} -> (0 f : Fin n -> a) -> ((i : Fin n) -> p (f i)) -> All p (tabulate f)
+tabulate {n = 0} f pf = []
+tabulate {n = S k} f pf = pf FZ :: tabulate (f . FS) (\i => pf $ FS i)
diff --git a/unify.ipkg b/unify.ipkg
index 060368f..44ee037 100644
--- a/unify.ipkg
+++ b/unify.ipkg
@@ -10,5 +10,7 @@ modules
   = Data.Fin.Occurs
   , Data.Maybe.Properties
   , Data.Term
+  , Data.Term.Property
   , Data.Term.Zipper
   , Data.Vect.Properties.Insert
+  , Data.Vect.Quantifiers.Extra