Prove mgu has a unique factor.

1 files changed, 51 insertions, 35 deletions

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 :