Begin big unification proof.

1 files changed, 103 insertions, 2 deletions

diff --git a/src/Data/Term/Unify.idr b/src/Data/Term/Unify.idr
index 7cb01d6..35cc048 100644
--- a/src/Data/Term/Unify.idr
+++ b/src/Data/Term/Unify.idr
@@ -5,6 +5,7 @@ import Data.Fin.Occurs
 import Data.Fin.Strong
 import Data.Maybe.Properties
 import Data.Term
+import Data.Term.Property
 import Data.Term.Zipper
 
 import Decidable.Equality
@@ -143,6 +144,13 @@ for : Term sig (pred k) -> SFin k -> SFin k -> Term sig (pred k)
 (t `for` x) y = maybe t Var' (thick x y)
 
 export
+forRefl :
+  (0 u : Term sig (pred k)) ->
+  (x : SFin k) ->
+  (u `for` x) x = u
+forRefl u x = cong (maybe u Var') $ extractIsNothing $ thickRefl x
+
+export
 forThin :
   (0 t : Term sig (pred k)) ->
   (x : SFin k) ->
@@ -161,7 +169,7 @@ forUnifies x t prf = Calc $
   ~~ (u `for` x) . thin x <$> u          ...(sym $ subAssoc (u `for` x) (pure (thin x)) u)
   ~~ Var' <$> u                          ...(subCong (forThin u x) u)
   ~~ u                                   ...(subUnit u)
-  ~~ (u `for` x) <$> Var' x              ...(sym $ cong (maybe u Var') $ extractIsNothing $ thickRefl x)
+  ~~ (u `for` x) <$> Var' x              ...(sym $ forRefl u x)
 
 -- Substitution List -----------------------------------------------------------
 
@@ -202,7 +210,7 @@ evalHomo sub2 (sub1 :< (t, x)) i = Calc $
 
 -- Unification -----------------------------------------------------------------
 
-flexFlex : (x : SFin (S n)) -> (y : SFin (S n)) -> Exists (AList sig (S n))
+flexFlex : SFin (S n) -> SFin (S n) -> Exists (AList sig (S n))
 flexFlex x y = case thick x y of
   Just z => Evidence _ [<(Var' z, x)]
   Nothing => Evidence _ [<]
@@ -246,3 +254,96 @@ amguAll (t :: ts) (u :: us) acc = do
 export
 mgu : DecEq (Exists sig.Operator) => (t, u : Term sig n) -> Maybe (Exists (AList sig n))
 mgu t u = amgu t u (Evidence _ [<])
+
+-- Properties
+
+export
+trivialUnify :
+  (0 f : SFin 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 :
+  (x : SFin (S n)) ->
+  (t : Term sig (S n)) ->
+  (0 _ : check x t = Just u) ->
+  (Max (Unifies (Var x) t)).Prop (u `for` x)
+varElim x t prf =
+  ( sym $ forUnifies x t prf
+  , \g, prf' => MkLte (g . thin x) (\i =>
+    case decEq x i of
+      Yes Refl =>
+       Calc $
+        |~ g x
+        ~~ g <$> t                        ...(prf')
+        ~~ g <$> pure (thin x) <$> u      ...(cong (g <$>) $ checkJust i t prf)
+        ~~ (g . thin x) <$> u             ...(sym $ subAssoc g (pure (thin x)) u)
+        ~~ (g . thin x) <$> (u `for` x) x ..<(cong ((g . thin x) <$>) $ forRefl u x)
+      No neq =>
+        let isJust = thickNeq x i neq in
+        let (y ** thickIsJustY) = extractIsJust isJust in
+        let thinXYIsI = thickJust x i thickIsJustY in
+        Calc $
+          |~ g i
+          ~~ g (thin x y)                            ..<(cong g thinXYIsI)
+          ~~ (g . thin x) <$> Var' y                 ...(Refl)
+          ~~ (g . thin x) <$> (u `for` x) (thin x y) ..<(cong ((g . thin x) <$>) $ forThin u x y)
+          ~~ (g . thin x) <$> (u `for` x) i          ...(cong (((g . thin x) <$>) . (u `for` x)) $ thinXYIsI))
+  )
+
+flexFlexUnifies :
+  (x, y : SFin (S n)) ->
+  (Max {sig} (Unifies (Var x) (Var y))).Prop (eval (flexFlex x y).snd)
+flexFlexUnifies x y with (thick x y) proof prf
+  _ | Just z =
+    (Max (Unifies (Var x) (Var y))).cong
+      (\i => sym $ subUnit ((Var' z `for` x) i))
+      (varElim x (Var y) (cong (map Var') prf))
+  _ | Nothing =
+    rewrite thickNothing x y (rewrite prf in ItIsNothing) in
+    trivialUnify Var' (Var y)
+
+flexRigidUnifies :
+  (x : SFin (S n)) ->
+  (t : Term sig (S n)) ->
+  (0 _ : flexRigid x t = Just sub) ->
+  (Max (Unifies (Var x) t)).Prop (eval sub.snd)
+flexRigidUnifies x t ok with (check x t) proof prf
+  flexRigidUnifies x t Refl | Just u =
+    (Max (Unifies (Var x) t)).cong
+      (\i => sym $ subUnit ((u `for` x) i))
+      (varElim x t prf)
+
+flexRigidFails :
+  (x : SFin (S k)) ->
+  (op : sig.Operator j) ->
+  (ts : Vect j (Term sig (S k))) ->
+  (0 _ : IsNothing (flexRigid x (Op op ts))) ->
+  Nothing (Unifies (Var x) (Op op ts))
+flexRigidFails x op ts isNothing f prf' with (check x (Op op ts)) proof prf
+  _ | Nothing =
+    let
+      (zip ** occurs) = checkNothing x (Op op ts) (rewrite prf in ItIsNothing)
+      cycle : (f x = (f <$> zip) + f x)
+      cycle = Calc $
+        |~ f x
+        ~~ f <$> Op op ts    ...(prf')
+        ~~ f <$> zip + Var x ...(cong (f <$>) occurs)
+        ~~ (f <$> zip) + f x ...(actionHomo f zip (Var x))
+      zipIsTop : (zip = Top)
+      zipIsTop = invertActionTop zip $ noCycles (f <$> zip) (f x) (sym cycle)
+      opIsVar : (Op op ts = Var x)
+      opIsVar = trans occurs (cong (+ Var x) zipIsTop)
+    in
+    absurd opIsVar
+
+stepEquiv :
+  (t, u : Term sig (S k)) ->
+  (sub : AList sig k j) ->
+  (v : Term sig k) ->
+  (x : SFin (S k)) ->
+  Extension (Unifies t u) (eval (sub :< (v, x))) <=>
+  Extension (Unifies ((v `for` x) <$> t) ((v `for` x) <$> u)) (eval sub)
+stepEquiv t u sub v x = extendUnify t u (v `for` x) (eval sub)