Prove mgu has a unique factor.

3 files changed, 213 insertions, 73 deletions

diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 385b864..973ff3d 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -93,6 +93,32 @@ subComp :
   f . pure r .=. f . r
 subComp f r i = Refl
 
+export
+compCong2 :
+  {0 f1, f2 : Fin k -> Term sig n} ->
+  {0 g1, g2 : Fin j -> Term sig k} ->
+  f1 .=. f2 ->
+  g1 .=. g2 ->
+  f1 . g1 .=. f2 . g2
+compCong2 prf1 prf2 i = Calc $
+  |~ f1 <$> g1 i
+  ~~ f1 <$> g2 i ...(cong (f1 <$>) $ prf2 i)
+  ~~ f2 <$> g2 i ...(subExtensional prf1 (g2 i))
+
+compCongL :
+  {0 f1, f2 : Fin k -> Term sig n} ->
+  f1 .=. f2 ->
+  (0 g : Fin j -> Term sig k) ->
+  f1 . g .=. f2 . g
+compCongL prf g = compCong2 prf (\_ => Refl)
+
+compCongR :
+  (0 f : Fin k -> Term sig n) ->
+  {0 g1, g2 : Fin j -> Term sig k} ->
+  g1 .=. g2 ->
+  f . g1 .=. f . g2
+compCongR f prf = compCong2 (\_ => Refl) prf
+
 -- Injectivity -----------------------------------------------------------------
 
 export
diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr
index 2de450f..62f4caa 100644
--- a/src/Data/Term/Property.idr
+++ b/src/Data/Term/Property.idr
@@ -16,7 +16,7 @@ public export
 record Property (sig : Signature) (k : Nat) where
   constructor MkProp
   0 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
+  cong : forall n. (f, g : Fin k -> Term sig n) -> f .=. g -> Prop f -> Prop g
 
 %name Property p, q
 
@@ -26,7 +26,7 @@ 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 $
+  , cong = \_, _, cong, prf => Calc $
     |~ _ <$> t
     ~~ _ <$> t ..<(subExtensional cong t)
     ~~ _ <$> u ...(prf)
@@ -35,7 +35,7 @@ Unifies t u = MkProp
 
 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))
+All ps = MkProp (\f => All (\p => p.Prop f) ps) (\f, g, cong => mapRel (\p => p.cong f g cong))
 
 public export
 UnifiesAll : Vect n (Term sig k) -> Vect n (Term sig k) -> Property sig k
@@ -111,7 +111,7 @@ 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 => subExtensional prf (f i))
+  , cong = \g, h, prf => p.cong (g . f) (h . f) (\i => subExtensional prf (f i))
   }
 
 -- Properties
@@ -128,8 +128,8 @@ extendCong2 :
   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)
+  (\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 :
@@ -152,8 +152,8 @@ extendAssoc :
   Extension (Extension p f) g <=> Extension p (g . f)
 extendAssoc p f g =
   MkEquivalence
-    (\h => p.cong (\i => subAssoc h g (f i)))
-    (\h => p.cong (\i => sym $ subAssoc h g (f i)))
+    (\h => p.cong _ _ (\i => subAssoc h g (f i)))
+    (\h => p.cong _ _ (\i => sym $ subAssoc h g (f i)))
 
 export
 extendUnify :
@@ -253,25 +253,78 @@ lteExtend :
   (prf : f <= g) ->
   p.Prop f ->
   (Extension p g).Prop prf.sub
-lteExtend prf x = p.cong prf.prf x
+lteExtend prf x = p.cong _ _ prf.prf x
 
 -- Most General ----------------------------------------------------------------
 
--- public export
--- record MostGeneral (p : Property sig k) where
+public export
+record MostGeneral (p : Property sig k) (f : Fin k -> Term sig n) where
+  constructor MkMostGeneral
+  valid : p.Prop f
+  universal : forall j. (g : Fin k -> Term sig j) -> p.Prop g -> Fin n -> Term sig j
+  factors :
+    forall j.
+    (g : Fin k -> Term sig j) ->
+    (v : p.Prop g) ->
+    g .=. universal g v . f
+  unique :
+    forall j.
+    (g : Fin k -> Term sig j) ->
+    (v : p.Prop g) ->
+    (h : Fin n -> Term sig j) ->
+    g .=. h . f ->
+    h .=. universal g v
+
+%name MostGeneral mg
+
+export
+varMostGeneral : p.Prop Var -> MostGeneral p Var
+varMostGeneral v =
+  MkMostGeneral
+    { valid = v
+    , universal = \g, _ => g
+    , factors = \g, _, x => Refl
+    , unique = \g, _, h, prf', x => sym $ prf' x
+    }
 
 public export
 Max : Property sig k -> Property sig k
 Max p = MkProp
-  { Prop = \f => (p.Prop f, forall n. (g : Fin k -> Term sig n) -> p.Prop g -> g <= f)
-  , cong = \cong, (x, max) => (p.cong cong x, \g, y => lteCong (\_ => Refl) cong (max g y))
+  { Prop = MostGeneral p
+  , cong = \f, g, prf, mg =>
+    MkMostGeneral
+      { valid = p.cong f g prf mg.valid
+      , universal = mg.universal
+      , factors = \h, v, x => Calc $
+        |~ h x
+        ~~ mg.universal h v <$> f x ...(mg.factors h v x)
+        ~~ mg.universal h v <$> g x ...(compCongR (mg.universal h v) prf x)
+      , unique = \h, v, i, prf' =>
+        mg.unique h v i $
+        \x => Calc $
+          |~ h x
+          ~~ i <$> g x ...(prf' x)
+          ~~ i <$> f x ...(compCongR i (\x => sym $ prf x) x)
+      }
   }
 
 export
 maxCong : p <=> q -> Max p <=> Max q
 maxCong prf = MkEquivalence
-  { leftToRight = \f, (x, max) => (prf.leftToRight f x, \g, y => max g (prf.rightToLeft g y))
-  , rightToLeft = \f, (x, max) => (prf.rightToLeft f x, \g, y => max g (prf.leftToRight g y))
+  { leftToRight = \f, mg =>
+    MkMostGeneral
+      { valid = prf.leftToRight f mg.valid
+      , universal = \g, v => mg.universal g (prf.rightToLeft g v)
+      , factors = \g, v => mg.factors g (prf.rightToLeft g v)
+      , unique = \g, v => mg.unique g (prf.rightToLeft g v)
+      }
+  , rightToLeft = \f, mg =>
+    MkMostGeneral
+      { valid = prf.rightToLeft f mg.valid
+      , universal = \g, v => mg.universal g (prf.leftToRight g v)
+      , factors = \g, v => mg.factors g (prf.leftToRight g v)
+      , unique = \g, v => mg.unique g (prf.leftToRight g v)
+      }
   }
 
 -- Downward Closed -------------------------------------------------------------
@@ -306,26 +359,66 @@ optimistLemma :
   {f : Fin k -> Term sig m} ->
   {g : Fin m -> Term sig n} ->
   DClosed p ->
-  (Max (Extension p a)).Prop f ->
-  (Max (Extension (All ps) (f . a))).Prop g ->
-  (Max (Extension (All (p :: ps)) a)).Prop (g . f)
-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') =>
-    let prf1 = max1 h x' in
-    let y'' = (All ps).cong (\i => trans (subExtensional prf1.prf (a i)) (subAssoc prf1.sub f (a i))) y' in
-    let prf2 = max2 prf1.sub y'' in
-    MkLte
-      { sub = prf2.sub
-      , prf = \i => Calc $
-        |~ h i
-        ~~ prf1.sub <$> f i         ...(prf1.prf i)
-        ~~ (prf2.sub . g) <$> f i   ...(subExtensional (prf2.prf) (f i))
-        ~~ prf2.sub <$> (g <$> f i) ...(subAssoc prf2.sub g (f i))
-      }
-  )
+  (MostGeneral (Extension p a)) f ->
+  (MostGeneral (Extension (All ps) (f . a))) g ->
+  (MostGeneral (Extension (All (p :: ps)) a)) (g . f)
+optimistLemma closed mg mg' =
+  MkMostGeneral
+    { valid =
+      closed.closed ((g . f) . a) (f . a) (compLte (MkLte g (\i => Refl)) a) mg.valid ::
+      (All ps).cong _ _ (\i => sym $ subAssoc g f (a i)) mg'.valid
+    , universal = universal
+    , factors = factors
+    , unique = unique
+    }
+  where
+  coerce :
+    forall i.
+    (h : Fin k -> Term sig i) ->
+    (v : (Extension p a).Prop h) ->
+    (Extension (All ps) a).Prop h ->
+    (Extension (All ps) (f . a)).Prop (mg.universal h v)
+  coerce h v =
+    (All ps).cong _ _
+        (\x => Calc $
+          |~ h <$> a x
+          ~~ mg.universal h v . f <$> a x   ...(subExtensional (mg.factors h v) (a x))
+          ~~ mg.universal h v <$> f <$> a x ...(subAssoc (mg.universal h v) f (a x)))
+  universal :
+    forall i.
+    (h : Fin k -> Term sig i) ->
+    (vs : (Extension (All (p :: ps)) a).Prop h) ->
+    Fin n -> Term sig i
+  universal h (v :: vs) =
+    mg'.universal (mg.universal h v) (coerce h v vs)
+
+  factors :
+    forall i.
+    (h : Fin k -> Term sig i) ->
+    (vs : (Extension (All (p :: ps)) a).Prop h) ->
+    h .=. universal h vs . (g . f)
+  factors h (v :: vs) x = Calc $
+    |~ h x
+    ~~ mg.universal h v <$> f x                                       ...(mg.factors h v x)
+    ~~ mg'.universal (mg.universal h v) (coerce h v vs) . g <$> f x   ...(subExtensional (mg'.factors (mg.universal h v) (coerce h v vs)) (f x))
+    ~~ mg'.universal (mg.universal h v) (coerce h v vs) <$> g <$> f x ...(subAssoc (mg'.universal (mg.universal h v) (coerce h v vs)) g (f x))
+
+  unique :
+    forall i.
+    (h : Fin k -> Term sig i) ->
+    (vs : (Extension (All (p :: ps)) a).Prop h) ->
+    (r : Fin n -> Term sig i) ->
+    h .=. r . (g . f) ->
+    r .=. universal h vs
+  unique h (v :: vs) r prf =
+    mg'.unique (mg.universal h v) (coerce h v vs) r $
+    \x => sym $
+      mg.unique h v (r . g)
+        (\x => Calc $
+          |~ h x
+          ~~ r <$> g <$> f x ...(prf x)
+          ~~ r . g <$> f x   ..<(subAssoc r g (f x)))
+        x
 
 export
 failHead : Nothing (Extension p a) -> Nothing (Extension (All (p :: ps)) a)
@@ -339,6 +432,11 @@ failTail :
   (Max (Extension p a)).Prop f ->
   Nothing (Extension (All ps) (f . a)) ->
   Nothing (Extension (All (p :: ps)) a)
-failTail (x, max) absurd g (y :: ys) =
-  let prf = max g y in
-  absurd prf.sub $ (All ps).cong (compLte prf a).prf ys
+failTail mg absurd g (v :: vs) =
+  absurd (mg.universal g v) $
+    (All ps).cong _ _
+      (\x => Calc $
+        |~ g <$> a x
+        ~~ mg.universal g v . f <$> a x   ...(subExtensional (mg.factors g v) (a x))
+        ~~ mg.universal g v <$> f <$> a x ...(subAssoc (mg.universal g v) f (a x)))
+      vs
diff --git a/src/Data/Term/Unify.idr b/src/Data/Term/Unify.idr
index b4f7ebd..9f806fa 100644
--- a/src/Data/Term/Unify.idr
+++ b/src/Data/Term/Unify.idr
@@ -4,6 +4,7 @@ import Data.Fin.Occurs
 import Data.Term
 import Data.Term.Property
 import Data.Term.Zipper
+import Data.Vect.Quantifiers.Extra
 
 import Decidable.Equality
 
@@ -97,6 +98,45 @@ forUnifies x t = Calc $
   ~~ t                                   ...(subUnit t)
   ~~ (t `for` x) <$> Var x               ...(sym $ forRefl t x)
 
+export
+varElim :
+  {n : Nat} ->
+  (x : Fin (S n)) ->
+  (t : Term sig n) ->
+  MostGeneral (Unifies (Var x) (pure (thin x) <$> t)) (t `for` x)
+varElim x t =
+  MkMostGeneral
+    { valid = sym $ forUnifies x t
+    , universal = \g, prf => g . thin x
+    , factors = factors
+    , unique = unique
+    }
+  where
+  factors :
+    forall k.
+    (g : Fin (S n) -> Term sig k) ->
+    (Unifies (Var x) (pure (thin x) <$> t)).Prop g ->
+    g .=. (g . thin x) . (t `for` x)
+  factors g prf i with (thickProof x i)
+    factors g prf _ | Equal prf' = Calc $
+      |~ g x
+      ~~ g <$> pure (thin x) <$> t    ...(prf)
+      ~~ g . thin x <$> t             ..<(subAssoc g (pure (thin x)) t)
+      ~~ g . thin x <$> (t `for` x) x ..<(cong ((g . thin x <$>) . maybe t Var) prf')
+    factors g prf _ | Thinned i prf' = sym $ cong (g . thin x <$>) (forThin t x i)
+
+  unique :
+    forall k.
+    (g : Fin (S n) -> Term sig k) ->
+    (Unifies (Var x) (pure (thin x) <$> t)).Prop g ->
+    (h : Fin n -> Term sig k) ->
+    g .=. h . (t `for` x) ->
+    h .=. g . thin x
+  unique g prf h prf' i = Calc $
+    |~ h i
+    ~~ h <$> (t `for` x) (thin x i) ..<(cong (h <$>) $ forThin t x i)
+    ~~ g (thin x i)                 ..<(prf' (thin x i))
+
 -- Substitution List -----------------------------------------------------------
 
 public export
@@ -205,44 +245,20 @@ export
 trivialUnify :
   (0 f : Fin n -> Term sig k) ->
   (t : Term sig n) ->
-  (Max (Extension (Unifies t t) f)).Prop Var
-trivialUnify f t = (Refl , \g, prf => varMax g)
-
-export
-varElim :
-  {n : Nat} ->
-  (x : Fin (S n)) ->
-  (t : Term sig n) ->
-  (Max (Unifies (Var x) (pure (thin x) <$> t))).Prop (t `for` x)
-varElim x t =
-  ( sym $ forUnifies x t
-  , \g, prf' => MkLte (g . thin x) (lteProof g prf')
-  )
-  where
-  lteProof :
-    forall k.
-    (g : Fin (S n) -> Term sig k) ->
-    (Unifies (Var x) (pure (thin x) <$> t)).Prop g ->
-    g .=. (g . thin x) . (t `for` x)
-  lteProof g prf i with (thickProof x i)
-    lteProof g prf _ | Equal prf' = Calc $
-      |~ g x
-      ~~ g <$> pure (thin x) <$> t    ...(prf)
-      ~~ g . thin x <$> t             ..<(subAssoc g (pure (thin x)) t)
-      ~~ g . thin x <$> (t `for` x) x ..<(cong ((g . thin x <$>) . maybe t Var) prf')
-    lteProof g prf _ | Thinned i prf' = sym $ cong (g . thin x <$>) (forThin t x i)
+  MostGeneral (Extension (Unifies t t) f) Var
+trivialUnify f t = varMostGeneral Refl
 
 flexFlexUnifies :
   {n : Nat} ->
   (x, y : Fin n) ->
-  (Max {sig} (Unifies (Var x) (Var y))).Prop (eval (flexFlex x y).snd)
+  MostGeneral {sig} (Unifies (Var x) (Var y)) (eval (flexFlex x y).snd)
 flexFlexUnifies {n = S n} x y with (thickProof x y)
   flexFlexUnifies {n = S n} x _ | Equal prf =
     rewrite prf in
     trivialUnify Var (Var x)
   flexFlexUnifies {n = S n} x _ | Thinned y prf =
     rewrite prf in
-    (Max (Unifies (Var x) (Var _))).cong
+    (Max (Unifies (Var x) (Var _))).cong _ _
       (\i => sym $ subUnit ((Var y `for` x) i))
       (varElim x (Var y))
 
@@ -251,7 +267,7 @@ data FlexRigidProof : Fin n -> Term sig n -> Maybe (Exists (AList sig n)) -> Typ
   ElimVar :
     {n : Nat} ->
     (sub : AList sig k n) ->
-    (mgu : (Max (Unifies (Var x) t)).Prop (eval sub)) ->
+    (mgu : MostGeneral (Unifies (Var x) t) (eval sub)) ->
     res = Just (Evidence _ sub) ->
     FlexRigidProof x t res
 
@@ -285,7 +301,7 @@ flexRigidProof {n = S n} x op ts with (checkProof x (Op op ts))
     rewrite prf in
     ElimVar
       [<(Op op us, x)]
-      ((Max (Unifies (Var x) (Op op _))).cong
+      ((Max (Unifies (Var x) (Op op _))).cong _ _
         (\i => sym $ subUnit ((Op op us `for` x) i))
         (varElim x (Op op us)))
       Refl
@@ -317,7 +333,7 @@ parameters {auto _ : DecOp sig}
       {j : Nat} ->
       {0 sub : AList sig k n} ->
       (sub' : AList sig n j) ->
-      (Max (Extension (Unifies t u) (eval sub))).Prop (eval sub') ->
+      MostGeneral (Extension (Unifies t u) (eval sub)) (eval sub') ->
       res = Just (Evidence _ (sub' ++ sub)) ->
       AmguProof t u sub res
 
@@ -337,7 +353,7 @@ parameters {auto _ : DecOp sig}
       {j : Nat} ->
       {0 sub : AList sig k n} ->
       (sub' : AList sig n j) ->
-      (Max (Extension (UnifiesAll ts us) (eval sub))).Prop (eval sub') ->
+      MostGeneral (Extension (UnifiesAll ts us) (eval sub)) (eval sub') ->
       res = Just (Evidence _ (sub' ++ sub)) ->
       AmguAllProof ts us sub res
 
@@ -453,7 +469,7 @@ amguProof (Op op ts) (Var y) (sub :< (v, z))
 
 amguAllProof [] [] sub =
   SuccessAll [<]
-    ([], \g, x => varMax g)
+    (varMostGeneral [])
     (sym $ cong (\sub => Just (Evidence _ sub)) $ appendUnitLeft sub)
 amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
   _ | Success sub' val prf with (amguAllProof ts us (sub' ++ sub))
@@ -467,7 +483,7 @@ amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
           cong'.leftToRight (eval sub'') val'
       in
       SuccessAll (sub'' ++ sub')
-        ((Max (Extension (UnifiesAll (t :: ts) (u :: us)) (eval sub))).cong
+        ((Max (Extension (UnifiesAll (t :: ts) (u :: us)) (eval sub))).cong _ _
           (\i => sym $ evalHomo sub'' sub' i)
           opt)
         (rewrite prf in rewrite prf' in
@@ -491,7 +507,7 @@ parameters {auto _ : DecOp sig}
     data MguProof : (t, u : Term sig k) -> Maybe (Exists (AList sig k)) -> Type where
       Success :
         (sub : AList sig k n) ->
-        (Max (Unifies t u)).Prop (eval sub) ->
+        MostGeneral (Unifies t u) (eval sub) ->
         res = Just (Evidence _ sub) ->
         MguProof t u res
       Failure :