Fix invalid statementHEADmaster

3 files changed, 147 insertions, 43 deletions

diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 973ff3d..bfeb360 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -2,7 +2,10 @@ module Data.Term
 
 import public Data.DPair
 import public Data.Vect
+
+import Data.Fin.Extra
 import Data.Vect.Properties.Map
+
 import Syntax.PreorderReasoning
 
 %prefix_record_projections off
@@ -88,12 +91,20 @@ subAssoc f g (Op op ts) = cong (Op op) $ Calc $
 
 export
 subComp :
-  (f : Fin k -> Term sig n) ->
-  (r : Fin j -> Fin k) ->
+  (0 f : Fin k -> Term sig n) ->
+  (0 r : Fin j -> Fin k) ->
   f . pure r .=. f . r
 subComp f r i = Refl
 
 export
+subAssoc' :
+  (f : Fin k -> Term sig n) ->
+  (g : Fin j -> Fin k) ->
+  (t : Term sig j) ->
+  (f . g) <$> t = f <$> pure g <$> t
+subAssoc' f g = subAssoc f (Var . g)
+
+export
 compCong2 :
   {0 f1, f2 : Fin k -> Term sig n} ->
   {0 g1, g2 : Fin j -> Term sig k} ->
@@ -119,6 +130,53 @@ compCongR :
   f . g1 .=. f . g2
 compCongR f prf = compCong2 (\_ => Refl) prf
 
+-- Substitution is a Semigroupoid ----------------------------------------------
+
+export
+(++) :
+  {j : Nat} ->
+  (Fin j -> Term sig n) ->
+  (Fin k -> Term sig n) ->
+  Fin (j + k) -> Term sig n
+f ++ g = either f g . splitSum
+
+export
+appendWeakenN :
+  {j : Nat} ->
+  (0 f : Fin j -> Term sig n) ->
+  (0 g : Fin k -> Term sig n) ->
+  (f ++ g) . weakenN k .=. f
+appendWeakenN f g i = cong (either f g) $ splitSumOfWeakenN i
+
+export
+appendShift :
+  {j : Nat} ->
+  (0 f : Fin j -> Term sig n) ->
+  (0 g : Fin k -> Term sig n) ->
+  (f ++ g) . shift j .=. g
+appendShift f g i = cong (either f g) $ splitSumOfShift i
+
+export
+appendCong2 :
+  {j : Nat} ->
+  {0 f : Fin j -> Term sig n} ->
+  {0 g : Fin k -> Term sig n} ->
+  {0 h : Fin (j + k) -> Term sig n} ->
+  h . weakenN k .=. f ->
+  h . shift j .=. g ->
+  h .=. f ++ g
+appendCong2 prf1 prf2 x with (splitSum x) proof prf
+  _ | Left i = Calc $
+    |~ h x
+    ~~ h (indexSum (splitSum x)) ..<(cong h (indexOfSplitSumInverse x))
+    ~~ h (weakenN k i)           ...(cong (h . indexSum) prf)
+    ~~ f i                       ...(prf1 i)
+  _ | Right i = Calc $
+    |~ h x
+    ~~ h (indexSum (splitSum x)) ..<(cong h (indexOfSplitSumInverse x))
+    ~~ h (shift j i)             ...(cong (h . indexSum) prf)
+    ~~ g i                       ...(prf2 i)
+
 -- Injectivity -----------------------------------------------------------------
 
 export
diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr
index 62f4caa..958c1c2 100644
--- a/src/Data/Term/Property.idr
+++ b/src/Data/Term/Property.idr
@@ -232,8 +232,8 @@ transitive prf1 prf2 = MkLte
   }
 
 export
-varMax : (f : Fin k -> Term sig m) -> f <= Var
-varMax f = MkLte f (\i => Refl)
+varUniqueMax : (f : Fin k -> Term sig m) -> f <= Var
+varUniqueMax f = MkLte f (\i => Refl)
 
 export
 compLte : f <= g -> (h : Fin k -> Term sig m) -> f . h <= g . h
@@ -255,6 +255,34 @@ lteExtend :
   (Extension p g).Prop prf.sub
 lteExtend prf x = p.cong _ _ prf.prf x
 
+-- Maximal ---------------------------------------------------------------------
+
+public export
+record Maximal (p : Property sig k) (f : Fin k -> Term sig n) where
+  constructor MkMaximal
+  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
+
+public export
+Max : Property sig k -> Property sig k
+Max p = MkProp
+  { Prop = Maximal p
+  , cong = \f, g, prf, mg =>
+    MkMaximal
+      { 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)
+      }
+  }
+
 -- Most General ----------------------------------------------------------------
 
 public export
@@ -278,6 +306,10 @@ record MostGeneral (p : Property sig k) (f : Fin k -> Term sig n) where
 %name MostGeneral mg
 
 export
+mostGeneralIsMaximal : MostGeneral p f -> Maximal p f
+mostGeneralIsMaximal mg = MkMaximal mg.valid mg.universal mg.factors
+
+export
 varMostGeneral : p.Prop Var -> MostGeneral p Var
 varMostGeneral v =
   MkMostGeneral
@@ -288,8 +320,8 @@ varMostGeneral v =
     }
 
 public export
-Max : Property sig k -> Property sig k
-Max p = MkProp
+UniqueMax : Property sig k -> Property sig k
+UniqueMax p = MkProp
   { Prop = MostGeneral p
   , cong = \f, g, prf, mg =>
     MkMostGeneral
@@ -309,7 +341,7 @@ Max p = MkProp
   }
 
 export
-maxCong : p <=> q -> Max p <=> Max q
+maxCong : p <=> q -> UniqueMax p <=> UniqueMax q
 maxCong prf = MkEquivalence
   { leftToRight = \f, mg =>
     MkMostGeneral
@@ -429,7 +461,7 @@ failTail :
   {ps : Vect _ (Property sig j)} ->
   {a : Fin j -> Term sig k} ->
   {f : Fin k -> Term sig m} ->
-  (Max (Extension p a)).Prop f ->
+  (UniqueMax (Extension p a)).Prop f ->
   Nothing (Extension (All ps) (f . a)) ->
   Nothing (Extension (All (p :: ps)) a)
 failTail mg absurd g (v :: vs) =
diff --git a/src/Data/Term/Unify.idr b/src/Data/Term/Unify.idr
index 9f806fa..113514a 100644
--- a/src/Data/Term/Unify.idr
+++ b/src/Data/Term/Unify.idr
@@ -148,8 +148,8 @@ data AList : Signature -> Nat -> Nat -> Type where
 
 namespace Exists
   public export
-  (:<) : Exists (AList sig n) -> (Term sig n, Fin (S n)) -> Exists (AList sig (S n))
-  Evidence _ sub :< tx = Evidence _ (sub :< tx)
+  (:<) : (k ** AList sig n k) -> (Term sig n, Fin (S n)) -> (k ** AList sig (S n) k)
+  (_ ** sub) :< tx = (_ ** sub :< tx)
 
 export
 eval : {k : Nat} -> AList sig k n -> Fin k -> Term sig n
@@ -198,29 +198,29 @@ flexFlex {n = S n} x y = case thick x y of
   Just z => (_ **[<(Var z, x)])
   Nothing => (_ ** [<])
 
-flexRigid : {n : Nat} -> Fin n -> Term sig n -> Maybe (Exists (AList sig n))
+flexRigid : {n : Nat} -> Fin n -> Term sig n -> Maybe (k ** AList sig n k)
 flexRigid {n = S n} x t = case check x t of
-  Just u => Just (Evidence _ [<(u, x)])
+  Just u => Just (_ ** [<(u, x)])
   Nothing => Nothing
 
 export
 amgu :
   DecOp sig =>
-  {n : Nat} ->
+  {k, n : Nat} ->
   (t, u : Term sig n) ->
   AList sig n k ->
-  Maybe (Exists (AList sig n))
+  Maybe (k ** AList sig n k)
 amguAll :
   DecOp sig =>
-  {n : Nat} ->
+  {k, n : Nat} ->
   (ts, us : Vect j (Term sig n)) ->
   AList sig n k ->
-  Maybe (Exists (AList sig n))
+  Maybe (k ** AList sig n k)
 
 amgu (Op op ts) (Op op' us) acc with (decOp (Evidence _ op) (Evidence _ op'))
   amgu (Op op ts) (Op op us) acc | Yes Refl = amguAll ts us acc
   _ | No neq = Nothing
-amgu (Var x) (Var y) [<] = Just (Evidence _ (flexFlex x y).snd)
+amgu (Var x) (Var y) [<] = Just (flexFlex x y)
 amgu (Var x) (Op op' us) [<] = flexRigid x (Op op' us)
 amgu (Op op ts) (Var y) [<] = flexRigid y (Op op ts)
 amgu t@(Var _) u@(Var _) (sub :< (v, z)) =
@@ -230,13 +230,13 @@ amgu t@(Var _) u@(Op _ _) (sub :< (v, z)) =
 amgu t@(Op _ _) u@(Var _) (sub :< (v, z)) =
   (:< (v, z)) <$> amgu ((v `for` z) <$> t) ((v `for` z) <$> u) sub
 
-amguAll [] [] acc = Just (Evidence _ acc)
+amguAll [] [] acc = Just (_ ** acc)
 amguAll (t :: ts) (u :: us) acc = do
   acc <- amgu t u acc
   amguAll ts us acc.snd
 
 export
-mgu : DecOp sig => {n : Nat} -> (t, u : Term sig n) -> Maybe (Exists (AList sig n))
+mgu : DecOp sig => {n : Nat} -> (t, u : Term sig n) -> Maybe (k ** AList sig n k)
 mgu t u = amgu t u [<]
 
 -- Properties
@@ -258,17 +258,17 @@ flexFlexUnifies {n = S n} x y with (thickProof x y)
     trivialUnify Var (Var x)
   flexFlexUnifies {n = S n} x _ | Thinned y prf =
     rewrite prf in
-    (Max (Unifies (Var x) (Var _))).cong _ _
+    (UniqueMax (Unifies (Var x) (Var _))).cong _ _
       (\i => sym $ subUnit ((Var y `for` x) i))
       (varElim x (Var y))
 
-data FlexRigidProof : Fin n -> Term sig n -> Maybe (Exists (AList sig n)) -> Type where
+data FlexRigidProof : Fin n -> Term sig n -> Maybe (k ** AList sig n k) -> Type where
   NoUnifier : Nothing (Unifies (Var x) t) -> res = Nothing -> FlexRigidProof x t res
   ElimVar :
     {n : Nat} ->
     (sub : AList sig k n) ->
     (mgu : MostGeneral (Unifies (Var x) t) (eval sub)) ->
-    res = Just (Evidence _ sub) ->
+    res = Just (_ ** sub) ->
     FlexRigidProof x t res
 
 flexRigidProof :
@@ -301,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 _ _
+      ((UniqueMax (Unifies (Var x) (Op op _))).cong _ _
         (\i => sym $ subUnit ((Op op us `for` x) i))
         (varElim x (Op op us)))
       Refl
@@ -322,7 +322,7 @@ parameters {auto _ : DecOp sig}
     Term sig k ->
     Term sig k ->
     AList sig k n ->
-    Maybe (Exists (AList sig k)) ->
+    Maybe (n ** AList sig k n) ->
     Type
     where
     Failure :
@@ -334,7 +334,7 @@ parameters {auto _ : DecOp sig}
       {0 sub : AList sig k n} ->
       (sub' : AList sig n j) ->
       MostGeneral (Extension (Unifies t u) (eval sub)) (eval sub') ->
-      res = Just (Evidence _ (sub' ++ sub)) ->
+      res = Just (_ ** sub' ++ sub) ->
       AmguProof t u sub res
 
   public export
@@ -342,7 +342,7 @@ parameters {auto _ : DecOp sig}
     Vect j (Term sig k) ->
     Vect j (Term sig k) ->
     AList sig k n ->
-    Maybe (Exists (AList sig k)) ->
+    Maybe (n ** AList sig k n) ->
     Type
     where
     FailureAll :
@@ -354,7 +354,7 @@ parameters {auto _ : DecOp sig}
       {0 sub : AList sig k n} ->
       (sub' : AList sig n j) ->
       MostGeneral (Extension (UnifiesAll ts us) (eval sub)) (eval sub') ->
-      res = Just (Evidence _ (sub' ++ sub)) ->
+      res = Just (_ ** sub' ++ sub) ->
       AmguAllProof ts us sub res
 
 export
@@ -378,8 +378,8 @@ amguProof (Op op ts) (Op op' us) sub with (decOp (Evidence _ op) (Evidence _ op'
     _ | SuccessAll sub' val prf' =
       let
         cong :
-          Max (Extension (Unifies (Op op ts) (Op op us)) (eval sub)) <=>
-          Max (Extension (UnifiesAll ts us) (eval sub))
+          UniqueMax (Extension (Unifies (Op op ts) (Op op us)) (eval sub)) <=>
+          UniqueMax (Extension (UnifiesAll ts us) (eval sub))
         cong = maxCong $ extendCong (eval sub) $ unifiesOp op ts us
       in
       Success sub'
@@ -397,7 +397,10 @@ amguProof (Var x) (Var y) [<] =
   Success
     (flexFlex x y).snd
     (flexFlexUnifies x y)
-    Refl
+    (cong Just $ ext _ (flexFlex x y))
+  where
+  ext : (0 b : a -> Type) -> (v : (x : a ** b x)) -> v = (v.fst ** v.snd)
+  ext b (fst ** snd) = Refl
 amguProof (Var x) (Op op' us) [<] with (flexRigidProof x op' us)
   _ | NoUnifier absurd prf = Failure absurd prf
   _ | ElimVar sub val prf = Success sub val prf
@@ -413,8 +416,8 @@ amguProof (Op op ts) (Var y) [<] with (flexRigidProof y op ts)
   _ | ElimVar sub val prf =
     let
       cong :
-        Max (Extension (Unifies (Var y) (Op op ts)) Var) <=>
-        Max (Extension (Unifies (Op op ts) (Var y)) Var)
+        UniqueMax (Extension (Unifies (Var y) (Op op ts)) Var) <=>
+        UniqueMax (Extension (Unifies (Op op ts) (Var y)) Var)
       cong = maxCong $ extendCong Var $ unifiesSym (Var y) (Op op ts)
     in
     Success sub (cong.leftToRight _ val) prf
@@ -423,8 +426,8 @@ amguProof (Var x) (Var y) (sub :< (v, z))
   _ | Success sub' val prf =
     let
       cong' :
-        Max (Extension (Unifies (Var x) (Var y)) (eval sub . (v `for` z))) <=>
-        Max (Extension (Unifies ((v `for` z) x) ((v `for` z) y)) (eval sub))
+        UniqueMax (Extension (Unifies (Var x) (Var y)) (eval sub . (v `for` z))) <=>
+        UniqueMax (Extension (Unifies ((v `for` z) x) ((v `for` z) y)) (eval sub))
       cong' = maxCong $ stepEquiv (Var x) (Var y) sub v z
     in
     Success sub'
@@ -439,8 +442,8 @@ amguProof (Var x) (Op op' us) (sub :< (v, z))
   _ | Success sub' val prf =
     let
       cong' :
-        Max (Extension (Unifies (Var x) (Op op' us)) (eval sub . (v `for` z))) <=>
-        Max (Extension (Unifies ((v `for` z) x) ((v `for` z) <$> Op op' us)) (eval sub))
+        UniqueMax (Extension (Unifies (Var x) (Op op' us)) (eval sub . (v `for` z))) <=>
+        UniqueMax (Extension (Unifies ((v `for` z) x) ((v `for` z) <$> Op op' us)) (eval sub))
       cong' = maxCong $ stepEquiv (Var x) (Op op' us) sub v z
     in
     Success sub'
@@ -455,8 +458,8 @@ amguProof (Op op ts) (Var y) (sub :< (v, z))
   _ | Success sub' val prf =
     let
       cong' :
-        Max (Extension (Unifies (Op op ts) (Var y)) (eval sub . (v `for` z))) <=>
-        Max (Extension (Unifies ((v `for` z) <$> Op op ts) ((v `for` z) y)) (eval sub))
+        UniqueMax (Extension (Unifies (Op op ts) (Var y)) (eval sub . (v `for` z))) <=>
+        UniqueMax (Extension (Unifies ((v `for` z) <$> Op op ts) ((v `for` z) y)) (eval sub))
       cong' = maxCong $ stepEquiv (Op op ts) (Var y) sub v z
     in
     Success sub'
@@ -470,7 +473,7 @@ amguProof (Op op ts) (Var y) (sub :< (v, z))
 amguAllProof [] [] sub =
   SuccessAll [<]
     (varMostGeneral [])
-    (sym $ cong (\sub => Just (Evidence _ sub)) $ appendUnitLeft sub)
+    (sym $ cong (\sub => Just (_ ** sub)) $ appendUnitLeft sub)
 amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
   _ | Success sub' val prf with (amguAllProof ts us (sub' ++ sub))
     _ | SuccessAll sub'' val' prf' =
@@ -483,11 +486,11 @@ 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 _ _
+        ((UniqueMax (Extension (UnifiesAll (t :: ts) (u :: us)) (eval sub))).cong _ _
           (\i => sym $ evalHomo sub'' sub' i)
           opt)
         (rewrite prf in rewrite prf' in
-          cong (\sub => Just (Evidence _ sub)) $
+          cong (\sub => Just (_ ** sub)) $
           appendAssoc sub'' sub' sub)
     _ | FailureAll absurd prf' =
       let
@@ -504,11 +507,12 @@ amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
 parameters {auto _ : DecOp sig}
   namespace MguProof
     public export
-    data MguProof : (t, u : Term sig k) -> Maybe (Exists (AList sig k)) -> Type where
+    data MguProof : (t, u : Term sig k) -> Maybe (n ** AList sig k n) -> Type where
       Success :
+        {n : Nat} ->
         (sub : AList sig k n) ->
         MostGeneral (Unifies t u) (eval sub) ->
-        res = Just (Evidence _ sub) ->
+        res = Just (_ ** sub) ->
         MguProof t u res
       Failure :
         Nothing (Unifies t u) ->
@@ -520,3 +524,13 @@ mguProof : DecOp sig => {k : Nat} -> (t, u : Term sig k) -> MguProof t u (mgu t
 mguProof t u with (amguProof t u [<])
   _ | Success sub val prf = Success sub val prf
   _ | Failure absurd prf = Failure absurd prf
+
+export
+invertMgu :
+  DecOp sig =>
+  {0 t, u : Term sig k} ->
+  MguProof t u res ->
+  res = Just (_ ** sub) ->
+  MostGeneral (Unifies t u) (eval sub)
+invertMgu (Success sub mg Refl) Refl = mg
+invertMgu (Failure _ prf) Refl = absurd prf