Define properties of substitutions.

1 files changed, 143 insertions, 0 deletions

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))