From fd658831ab53f07969524fee0257d086d6f79f5a Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 12 Jul 2023 14:02:42 +0100
Subject: Prove unification correct.

---
 src/Data/Term/Property.idr | 116 ++++++++++++++++++++++++++++++---------------
 1 file changed, 78 insertions(+), 38 deletions(-)

(limited to 'src/Data/Term/Property.idr')

diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr
index 1fa53cd..bed4e49 100644
--- a/src/Data/Term/Property.idr
+++ b/src/Data/Term/Property.idr
@@ -2,8 +2,8 @@ module Data.Term.Property
 
 import Data.Term
 
+import public Data.Vect.Quantifiers
 import Data.Vect.Properties.Index
-import Data.Vect.Quantifiers
 import Data.Vect.Quantifiers.Extra
 
 import Syntax.PreorderReasoning
@@ -37,6 +37,10 @@ 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))
 
+public export
+UnifiesAll : Vect n (Term sig k) -> Vect n (Term sig k) -> Property sig k
+UnifiesAll ts us = All (zipWith Unifies ts us)
+
 -- Equivalence -----------------------------------------------------------------
 
 public export
@@ -47,41 +51,47 @@ record (<=>) (p, q : Property sig k) where
 
 -- Properties
 
+export
+Reflexive (Property sig k) (<=>) where
+  reflexive = MkEquivalence (\_ => id) (\_ => id)
+
+export
+Symmetric (Property sig k) (<=>) where
+  symmetric prf = MkEquivalence prf.rightToLeft prf.leftToRight
+
 export
 unifiesSym : (0 t, u : Term sig k) -> Unifies t u <=> Unifies u t
 unifiesSym t u = 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 = MkEquivalence
-  { leftToRight = \f, prf => tabulate (\i => Unifies (index i ts) (index i us)) (leftToRight f prf)
-  , rightToLeft = \f, prf => irrelevantEq $ cong (Op op) $ rightToLeft f prf
+  {0 k : Nat} ->
+  (0 op : sig.Operator k) ->
+  (ts, us : Vect k (Term sig j)) ->
+  Unifies (Op op ts) (Op op us) <=> UnifiesAll ts us
+unifiesOp op ts us = MkEquivalence
+  { leftToRight = \f, prf => leftToRight ts us f (opInjectiveTs' prf)
+  , rightToLeft = \f, prf => cong (Op op) $ rightToLeft ts us f prf
   }
   where
   leftToRight :
-    (f : SFin j -> Term sig n) ->
-    (Unifies (Op op ts) (Op op us)).Prop f ->
-    (i : _) ->
-    f <$> index i ts = f <$> index i us
-  leftToRight f 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)
+    forall k.
+    (ts, us : Vect k (Term sig j)) ->
+    (0 f : (SFin j -> Term sig n)) ->
+    map (f <$>) ts = map (f <$>) us ->
+    (UnifiesAll ts us).Prop f
+  leftToRight [] [] f prf = []
+  leftToRight (t :: ts) (u :: us) f prf =
+    fst (biinj (::) prf) :: leftToRight ts us f (snd $ biinj (::) prf)
 
   rightToLeft :
-    {k : Nat} ->
-    (f : SFin j -> Term sig n) ->
-    {ts, us : Vect k (Term sig j)} ->
-    (All (tabulate (\i => Unifies (index i ts) (index i us)))).Prop f ->
+    forall k.
+    (ts, us : Vect k (Term sig j)) ->
+    (0 f : (SFin j -> Term sig n)) ->
+    (UnifiesAll ts us).Prop f ->
     map (f <$>) ts = map (f <$>) us
-  rightToLeft f {ts = [], us = []} [] = Refl
-  rightToLeft f {ts = t :: ts, us = u :: us} (prf :: prfs) = cong2 (::) prf (rightToLeft f prfs)
+  rightToLeft [] [] f [] = Refl
+  rightToLeft (t :: ts) (u :: us) f (prf :: prfs) = cong2 (::) prf (rightToLeft ts us f prfs)
 
 -- Nothing ---------------------------------------------------------------------
 
@@ -111,7 +121,21 @@ nothingExtends : Nothing p -> Nothing (Extension p f)
 nothingExtends absurd g x = void $ absurd (g . f) x
 
 export
-extendCong : (f : _) -> p <=> q -> Extension p f <=> Extension q f
+extendCong2 :
+  {f, g : SFin n -> Term sig k} ->
+  {p, q : Property sig n} ->
+  f .=. g ->
+  p <=> q ->
+  Extension p f <=> Extension q g
+extendCong2 prf1 prf2 = MkEquivalence
+  (\h, x => prf2.leftToRight (h . g) $ p.cong (\i => cong (h <$>) $ prf1 i) x)
+  (\h, x => prf2.rightToLeft (h . f) $ q.cong (\i => sym $ cong (h <$>) $ prf1 i) x)
+
+export
+extendCong :
+  (f : SFin n -> Term sig k) ->
+  p <=> q ->
+  Extension p f <=> Extension q f
 extendCong f prf = MkEquivalence
   (\g => prf.leftToRight (g . f))
   (\g => prf.rightToLeft (g . f))
@@ -154,6 +178,21 @@ extendUnify t u f g =
       ~~ ((h . g) . f) <$> u   ...(sym $ subAssoc (h . g) f u)
       ~~ (h . (g . f)) <$> u   ...(subCong (\i => subAssoc h g (f i)) u))
 
+export
+extendUnifyAll :
+  (ts, us : Vect n (Term sig j)) ->
+  (f : SFin j -> Term sig k) ->
+  (g : SFin k -> Term sig m) ->
+  Extension (UnifiesAll ts us) (g . f) <=>
+  Extension (UnifiesAll (map (f <$>) ts) (map (f <$>) us)) g
+extendUnifyAll [] [] f g = MkEquivalence (\h, [] => []) (\h, [] => [])
+extendUnifyAll (t :: ts) (u :: us) f g =
+  let head = extendUnify t u f g in
+  let tail = extendUnifyAll ts us f g in
+  MkEquivalence
+    (\h, (x :: xs) => head.leftToRight h x :: tail.leftToRight h xs)
+    (\h, (x :: xs) => head.rightToLeft h x :: tail.rightToLeft h xs)
+
 -- Ordering --------------------------------------------------------------------
 
 public export
@@ -234,27 +273,28 @@ maxCong prf = MkEquivalence
 
 -- Downward Closed -------------------------------------------------------------
 
-public export 0
-DClosed : Property sig k -> Type
-DClosed p =
-  forall m, n.
-  (f : SFin k -> Term sig m) ->
-  (g : SFin k -> Term sig n) ->
-  f <= g ->
-  p.Prop g ->
-  p.Prop f
+public export
+record DClosed (p : Property sig k) where
+  constructor MkDClosed
+  closed :
+    forall m, n.
+    (f : SFin k -> Term sig m) ->
+    (g : SFin k -> Term sig n) ->
+    f <= g ->
+    p.Prop g ->
+    p.Prop f
 
 -- Properties
 
 export
 unifiesDClosed : (t, u : Term sig k) -> DClosed (Unifies t u)
-unifiesDClosed t u f g prf1 prf2 = Calc $
+unifiesDClosed t u = MkDClosed (\f, g, prf1, prf2 => Calc $
   |~ f <$> t
   ~~ (prf1.sub . g) <$> t ...(subCong prf1.prf t)
   ~~ prf1.sub <$> g <$> t ...(subAssoc prf1.sub g t)
   ~~ prf1.sub <$> g <$> u ...(cong (prf1.sub <$>) prf2)
   ~~ (prf1.sub . g) <$> u ..<(subAssoc prf1.sub g u)
-  ~~ f <$> u              ..<(subCong prf1.prf u)
+  ~~ f <$> u              ..<(subCong prf1.prf u))
 
 export
 optimistLemma :
@@ -266,8 +306,8 @@ optimistLemma :
   (Max (Extension p a)).Prop f ->
   (Max (Extension (All ps) (f . a))).Prop g ->
   (Max (Extension (All (p :: ps)) a)).Prop (g . f)
-optimistLemma closed (x, max1) (y, max2) =
-  ( ( closed ((g . f) . a) (f . a) (compLte (MkLte g (\i => Refl)) a) x
+optimistLemma prf (x, max1) (y, max2) =
+  ( ( prf.closed ((g . f) . a) (f . a) (compLte (MkLte g (\i => Refl)) a) x
     :: (All ps).cong (\i => sym $ subAssoc g f (a i)) y
     )
   , \h, (x' :: y') =>
-- 
cgit v1.2.3