Promote property equivalence to a record.

Improves inference for congruence.

1 files changed, 61 insertions, 32 deletions

diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr
index afec1a2..1fa53cd 100644
--- a/src/Data/Term/Property.idr
+++ b/src/Data/Term/Property.idr
@@ -39,15 +39,17 @@ All ps = MkProp (\f => All (\p => p.Prop f) ps) (\cong => mapRel (\p => p.cong c
 
 -- Equivalence -----------------------------------------------------------------
 
-public export 0
-(<=>) : Property sig k -> Property sig k -> Type
-p <=> q = forall n. (f : SFin k -> Term sig n) -> p.Prop f <=> q.Prop f
+public export
+record (<=>) (p, q : Property sig k) where
+  constructor MkEquivalence
+  leftToRight : forall n. (f : SFin k -> Term sig n) -> p.Prop f -> q.Prop f
+  rightToLeft : forall n. (f : SFin k -> Term sig n) -> q.Prop f -> p.Prop f
 
 -- Properties
 
 export
-unifiesSym : Unifies t u <=> Unifies u t
-unifiesSym f = MkEquivalence (\prf => sym prf) (\prf => sym prf)
+unifiesSym : (0 t, u : Term sig k) -> Unifies t u <=> Unifies u t
+unifiesSym t u = MkEquivalence (\_, prf => sym prf) (\_, prf => sym prf)
 
 export
 unifiesOp :
@@ -55,16 +57,17 @@ unifiesOp :
   {0 op : sig.Operator k} ->
   {0 ts, us : Vect k (Term sig j)} ->
   Unifies (Op op ts) (Op op us) <=> All (tabulate (\i => Unifies (index i ts) (index i us)))
-unifiesOp f = MkEquivalence
-  { leftToRight = \prf => tabulate (\i => Unifies (index i ts) (index i us)) (leftToRight prf)
-  , rightToLeft = \prf => irrelevantEq $ cong (Op op) $ rightToLeft prf
+unifiesOp = MkEquivalence
+  { leftToRight = \f, prf => tabulate (\i => Unifies (index i ts) (index i us)) (leftToRight f prf)
+  , rightToLeft = \f, prf => irrelevantEq $ cong (Op op) $ rightToLeft f prf
   }
   where
   leftToRight :
+    (f : SFin j -> Term sig n) ->
     (Unifies (Op op ts) (Op op us)).Prop f ->
     (i : _) ->
     f <$> index i ts = f <$> index i us
-  leftToRight prf i =
+  leftToRight f prf i =
     Calc $
       |~ f <$> index i ts
       ~~ index i (map (f <$>) ts) ...(sym $ indexNaturality i (f <$>) ts)
@@ -73,11 +76,12 @@ unifiesOp f = MkEquivalence
 
   rightToLeft :
     {k : Nat} ->
+    (f : SFin j -> Term sig n) ->
     {ts, us : Vect k (Term sig j)} ->
     (All (tabulate (\i => Unifies (index i ts) (index i us)))).Prop f ->
     map (f <$>) ts = map (f <$>) us
-  rightToLeft {ts = [], us = []} [] = Refl
-  rightToLeft {ts = t :: ts, us = u :: us} (prf :: prfs) = cong2 (::) prf (rightToLeft prfs)
+  rightToLeft f {ts = [], us = []} [] = Refl
+  rightToLeft f {ts = t :: ts, us = u :: us} (prf :: prfs) = cong2 (::) prf (rightToLeft f prfs)
 
 -- Nothing ---------------------------------------------------------------------
 
@@ -89,7 +93,7 @@ Nothing p = forall n. (f : SFin k -> Term sig n) -> Not (p.Prop f)
 
 export
 nothingEquiv : p <=> q -> Nothing p -> Nothing q
-nothingEquiv eq absurd f x = absurd f ((eq f).rightToLeft x)
+nothingEquiv eq absurd f x = absurd f (eq.rightToLeft f x)
 
 -- Extensions ------------------------------------------------------------------
 
@@ -107,8 +111,14 @@ nothingExtends : Nothing p -> Nothing (Extension p f)
 nothingExtends absurd g x = void $ absurd (g . f) x
 
 export
+extendCong : (f : _) -> p <=> q -> Extension p f <=> Extension q f
+extendCong f prf = MkEquivalence
+  (\g => prf.leftToRight (g . f))
+  (\g => prf.rightToLeft (g . f))
+
+export
 extendUnit : (p : Property sig k) -> p <=> Extension p Var'
-extendUnit p f = MkEquivalence id id
+extendUnit p = MkEquivalence (\_, x => x) (\_, x => x)
 
 export
 extendAssoc :
@@ -116,10 +126,10 @@ extendAssoc :
   (f : SFin j -> Term sig k) ->
   (g : SFin k -> Term sig m) ->
   Extension (Extension p f) g <=> Extension p (g . f)
-extendAssoc p f g h =
+extendAssoc p f g =
   MkEquivalence
-    (p.cong (\i => subAssoc h g (f i)))
-    (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 :
@@ -127,16 +137,16 @@ extendUnify :
   (f : SFin j -> Term sig k) ->
   (g : SFin k -> Term sig m) ->
   Extension (Unifies t u) (g . f) <=> Extension (Unifies (f <$> t) (f <$> u)) g
-extendUnify t u f g h =
+extendUnify t u f g =
   MkEquivalence
-    (\prf => Calc $
+    (\h, prf => Calc $
       |~ (h . g) <$> (f <$> t)
       ~~ ((h . g) . f) <$> t   ...(sym $ subAssoc (h . g) f t)
       ~~ (h . (g . f)) <$> t   ...(subCong (\i => subAssoc h g (f i)) t)
       ~~ (h . (g . f)) <$> u   ...(prf)
       ~~ ((h . g) . f) <$> u   ...(sym $ subCong (\i => subAssoc h g (f i)) u)
       ~~ (h . g) <$> (f <$> u) ...(subAssoc (h . g) f u))
-    (\prf => Calc $
+    (\h, prf => Calc $
       |~ (h . (g . f)) <$> t
       ~~ ((h . g) . f) <$> t   ...(sym $ subCong (\i => subAssoc h g (f i)) t)
       ~~ (h . g) <$> (f <$> t) ...(subAssoc (h . g) f t)
@@ -197,12 +207,12 @@ compLte prf h = MkLte
   }
 
 export
-lteExtend : 
+lteExtend :
   {p : Property sig k} ->
   {f : SFin k -> Term sig m} ->
   {g : SFin k -> Term sig n} ->
-  (prf : f <= g) -> 
-  p.Prop f -> 
+  (prf : f <= g) ->
+  p.Prop f ->
   (Extension p g).Prop prf.sub
 lteExtend prf x = p.cong prf.prf x
 
@@ -217,9 +227,9 @@ Max p = MkProp
 
 export
 maxCong : p <=> q -> Max p <=> Max q
-maxCong prf f = MkEquivalence
-  { leftToRight = \(x, max) => ((prf f).leftToRight x, \g, y => max g ((prf g).rightToLeft y))
-  , rightToLeft = \(x, max) => ((prf f).rightToLeft x, \g, y => max g ((prf g).leftToRight y))
+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))
   }
 
 -- Downward Closed -------------------------------------------------------------
@@ -236,6 +246,7 @@ DClosed p =
 
 -- Properties
 
+export
 unifiesDClosed : (t, u : Term sig k) -> DClosed (Unifies t u)
 unifiesDClosed t u f g prf1 prf2 = Calc $
   |~ f <$> t
@@ -245,21 +256,23 @@ unifiesDClosed t u f g prf1 prf2 = Calc $
   ~~ (prf1.sub . g) <$> u ..<(subAssoc prf1.sub g u)
   ~~ f <$> u              ..<(subCong prf1.prf u)
 
+export
 optimistLemma :
-  {q : Property sig j} ->
+  {ps : Vect _ (Property sig j)} ->
   {a : SFin j -> Term sig k} ->
   {f : SFin k -> Term sig m} ->
   {g : SFin m -> Term sig n} ->
   DClosed p ->
   (Max (Extension p a)).Prop f ->
-  (Max (Extension q (f . a))).Prop g ->
-  (Max (Extension (All [p, q]) a)).Prop (g . f)
+  (Max (Extension (All ps) (f . a))).Prop g ->
+  (Max (Extension (All (p :: ps)) a)).Prop (g . f)
 optimistLemma closed (x, max1) (y, max2) =
-  ([ closed ((g . f) . a) (f . a) (compLte (MkLte g (\i => Refl)) a) x
-  ,  q.cong (\i => sym $ subAssoc g f (a i)) y
-  ], \h, [x', y'] =>
+  ( ( 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'' = q.cong (\i => trans (subCong prf1.prf (a i)) (subAssoc prf1.sub f (a i))) y' in
+    let y'' = (All ps).cong (\i => trans (subCong prf1.prf (a i)) (subAssoc prf1.sub f (a i))) y' in
     let prf2 = max2 prf1.sub y'' in
     MkLte
       { sub = prf2.sub
@@ -270,3 +283,19 @@ optimistLemma closed (x, max1) (y, max2) =
         ~~ prf2.sub <$> (g <$> f i) ...(subAssoc prf2.sub g (f i))
       }
   )
+
+export
+failHead : Nothing (Extension p a) -> Nothing (Extension (All (p :: ps)) a)
+failHead absurd f (x :: xs) = absurd f x
+
+export
+failTail :
+  {ps : Vect _ (Property sig j)} ->
+  {a : SFin j -> Term sig k} ->
+  {f : SFin k -> Term sig m} ->
+  (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