Begin big unification proof.

5 files changed, 128 insertions, 2 deletions

diff --git a/src/Data/Fin/Strong.idr b/src/Data/Fin/Strong.idr
index ebf3483..a0ed5df 100644
--- a/src/Data/Fin/Strong.idr
+++ b/src/Data/Fin/Strong.idr
@@ -1,6 +1,8 @@
 module Data.Fin.Strong
 
 import Data.Fin
+import Decidable.Equality.Core
+import Syntax.PreorderReasoning
 
 public export
 data SFin : Nat -> Type where
@@ -61,6 +63,14 @@ Injective (FS' {n}) where
   injective {x = FS x, y = FS y} prf = cong FS $ injective {f = FS'} $ injective prf
 
 export
+Injective (strongToFin {n}) where
+  injective {x, y} prf = Calc $
+    |~ x
+    ~~ finToStrong (strongToFin x) ..<(strongToFinToStrong x)
+    ~~ finToStrong (strongToFin y) ...(cong finToStrong prf)
+    ~~ y                           ...(strongToFinToStrong y)
+
+export
 Uninhabited (SFin 0) where uninhabited x impossible
 
 export
@@ -74,3 +84,9 @@ sucNonZero (FS x) prf = absurd prf
 export
 sucIsFS : (x : SFin (S n)) -> FS' x = FS x
 sucIsFS x = rewrite strongToFinToStrong x in Refl
+
+export
+DecEq (SFin n) where
+  decEq x y = viaEquivalence
+    (MkEquivalence (injective {f = strongToFin}) (\prf => cong strongToFin prf))
+    (decEq (strongToFin x) (strongToFin y))
diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 4b0ac3e..ebb7b00 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -30,6 +30,9 @@ export
 varIsVar : (x : SFin (S n)) -> Var' x = Var x
 varIsVar x = Refl
 
+export
+Uninhabited (Op op ts = Var x) where uninhabited prf impossible
+
 -- Substitution ----------------------------------------------------------------
 
 export
diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr
index d65d185..afec1a2 100644
--- a/src/Data/Term/Property.idr
+++ b/src/Data/Term/Property.idr
@@ -8,6 +8,8 @@ import Data.Vect.Quantifiers.Extra
 
 import Syntax.PreorderReasoning
 
+%prefix_record_projections off
+
 -- Definition ------------------------------------------------------------------
 
 public export
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)
diff --git a/src/Data/Term/Zipper.idr b/src/Data/Term/Zipper.idr
index 608e86c..ddc0797 100644
--- a/src/Data/Term/Zipper.idr
+++ b/src/Data/Term/Zipper.idr
@@ -115,6 +115,10 @@ actionHomo f (Op op i ts zip) t = cong (Op op) $ Calc $
   ~~ insertAt' i (f <$> zip + t) (map (f <$>) ts)           ...(mapInsertAt (f <$>) i (zip + t) ts)
   ~~ insertAt' i ((f <$> zip) + (f <$> t)) (map (f <$>) ts) ...(cong (\t => insertAt' i t (map (f <$>) ts)) $ actionHomo f zip t)
 
+export
+invertActionTop : (zip : Zipper sig k) -> (0 _ : f <$> zip = Top) -> zip = Top
+invertActionTop Top prf = Refl
+
 -- Cycles ----------------------------------------------------------------------
 
 pivotAt : sig.Operator k -> SFin k -> Vect k (Term sig n) -> Zipper sig n