Remove SFin.

Delete unused modules.

Restructure some proofs to reduce the number of lemmas.

1 files changed, 49 insertions, 46 deletions

diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr
index bed4e49..2de450f 100644
--- a/src/Data/Term/Property.idr
+++ b/src/Data/Term/Property.idr
@@ -15,8 +15,8 @@ import Syntax.PreorderReasoning
 public export
 record Property (sig : Signature) (k : Nat) where
   constructor MkProp
-  0 Prop : forall n. (SFin k -> Term sig n) -> Type
-  cong : forall n. {f, g : SFin k -> Term sig n} -> f .=. g -> Prop f -> Prop g
+  0 Prop : forall n. (Fin k -> Term sig n) -> Type
+  cong : forall n. {f, g : Fin k -> Term sig n} -> f .=. g -> Prop f -> Prop g
 
 %name Property p, q
 
@@ -28,9 +28,9 @@ Unifies t u = MkProp
   { Prop = \f => f <$> t = f <$> u
   , cong = \cong, prf => Calc $
     |~ _ <$> t
-    ~~ _ <$> t ..<(subCong cong t)
+    ~~ _ <$> t ..<(subExtensional cong t)
     ~~ _ <$> u ...(prf)
-    ~~ _ <$> u ...(subCong cong u)
+    ~~ _ <$> u ...(subExtensional cong u)
   }
 
 public export
@@ -46,8 +46,8 @@ UnifiesAll ts us = All (zipWith Unifies ts us)
 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
+  leftToRight : forall n. (f : Fin k -> Term sig n) -> p.Prop f -> q.Prop f
+  rightToLeft : forall n. (f : Fin k -> Term sig n) -> q.Prop f -> p.Prop f
 
 -- Properties
 
@@ -77,7 +77,7 @@ unifiesOp op ts us = MkEquivalence
   leftToRight :
     forall k.
     (ts, us : Vect k (Term sig j)) ->
-    (0 f : (SFin j -> Term sig n)) ->
+    (0 f : (Fin j -> Term sig n)) ->
     map (f <$>) ts = map (f <$>) us ->
     (UnifiesAll ts us).Prop f
   leftToRight [] [] f prf = []
@@ -87,7 +87,7 @@ unifiesOp op ts us = MkEquivalence
   rightToLeft :
     forall k.
     (ts, us : Vect k (Term sig j)) ->
-    (0 f : (SFin j -> Term sig n)) ->
+    (0 f : (Fin j -> Term sig n)) ->
     (UnifiesAll ts us).Prop f ->
     map (f <$>) ts = map (f <$>) us
   rightToLeft [] [] f [] = Refl
@@ -97,7 +97,7 @@ unifiesOp op ts us = MkEquivalence
 
 public export 0
 Nothing : Property sig k -> Type
-Nothing p = forall n. (f : SFin k -> Term sig n) -> Not (p.Prop f)
+Nothing p = forall n. (f : Fin k -> Term sig n) -> Not (p.Prop f)
 
 -- Properties
 
@@ -108,10 +108,10 @@ nothingEquiv eq absurd f x = absurd f (eq.rightToLeft f x)
 -- Extensions ------------------------------------------------------------------
 
 public export
-Extension : Property sig k -> (SFin k -> Term sig n) -> Property sig n
+Extension : Property sig k -> (Fin k -> Term sig n) -> Property sig n
 Extension p f = MkProp
   { Prop = \g => p.Prop (g . f)
-  , cong = \prf => p.cong (\i => subCong prf (f i))
+  , cong = \prf => p.cong (\i => subExtensional prf (f i))
   }
 
 -- Properties
@@ -122,7 +122,7 @@ nothingExtends absurd g x = void $ absurd (g . f) x
 
 export
 extendCong2 :
-  {f, g : SFin n -> Term sig k} ->
+  {f, g : Fin n -> Term sig k} ->
   {p, q : Property sig n} ->
   f .=. g ->
   p <=> q ->
@@ -133,7 +133,7 @@ extendCong2 prf1 prf2 = MkEquivalence
 
 export
 extendCong :
-  (f : SFin n -> Term sig k) ->
+  (f : Fin n -> Term sig k) ->
   p <=> q ->
   Extension p f <=> Extension q f
 extendCong f prf = MkEquivalence
@@ -141,14 +141,14 @@ extendCong f prf = MkEquivalence
   (\g => prf.rightToLeft (g . f))
 
 export
-extendUnit : (p : Property sig k) -> p <=> Extension p Var'
+extendUnit : (p : Property sig k) -> p <=> Extension p Var
 extendUnit p = MkEquivalence (\_, x => x) (\_, x => x)
 
 export
 extendAssoc :
   (p : Property sig j) ->
-  (f : SFin j -> Term sig k) ->
-  (g : SFin k -> Term sig m) ->
+  (f : Fin j -> Term sig k) ->
+  (g : Fin k -> Term sig m) ->
   Extension (Extension p f) g <=> Extension p (g . f)
 extendAssoc p f g =
   MkEquivalence
@@ -158,31 +158,31 @@ extendAssoc p f g =
 export
 extendUnify :
   (t, u : Term sig j) ->
-  (f : SFin j -> Term sig k) ->
-  (g : SFin k -> Term sig m) ->
+  (f : Fin j -> Term sig k) ->
+  (g : Fin k -> Term sig m) ->
   Extension (Unifies t u) (g . f) <=> Extension (Unifies (f <$> t) (f <$> u)) g
 extendUnify t u f g =
   MkEquivalence
     (\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)) <$> t   ...(subExtensional (\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   ...(sym $ subExtensional (\i => subAssoc h g (f i)) u)
       ~~ (h . g) <$> (f <$> u) ...(subAssoc (h . g) f u))
     (\h, prf => Calc $
       |~ (h . (g . f)) <$> t
-      ~~ ((h . g) . f) <$> t   ...(sym $ subCong (\i => subAssoc h g (f i)) t)
+      ~~ ((h . g) . f) <$> t   ...(sym $ subExtensional (\i => subAssoc h g (f i)) t)
       ~~ (h . g) <$> (f <$> t) ...(subAssoc (h . g) f t)
       ~~ (h . g) <$> (f <$> u) ...(prf)
       ~~ ((h . g) . f) <$> u   ...(sym $ subAssoc (h . g) f u)
-      ~~ (h . (g . f)) <$> u   ...(subCong (\i => subAssoc h g (f i)) u))
+      ~~ (h . (g . f)) <$> u   ...(subExtensional (\i => subAssoc h g (f i)) u))
 
 export
 extendUnifyAll :
   (ts, us : Vect n (Term sig j)) ->
-  (f : SFin j -> Term sig k) ->
-  (g : SFin k -> Term sig m) ->
+  (f : Fin j -> Term sig k) ->
+  (g : Fin k -> Term sig m) ->
   Extension (UnifiesAll ts us) (g . f) <=>
   Extension (UnifiesAll (map (f <$>) ts) (map (f <$>) us)) g
 extendUnifyAll [] [] f g = MkEquivalence (\h, [] => []) (\h, [] => [])
@@ -196,9 +196,9 @@ extendUnifyAll (t :: ts) (u :: us) f g =
 -- Ordering --------------------------------------------------------------------
 
 public export
-record (<=) (f : SFin k -> Term sig m) (g : SFin k -> Term sig n) where
+record (<=) (f : Fin k -> Term sig m) (g : Fin k -> Term sig n) where
   constructor MkLte
-  sub : SFin n -> Term sig m
+  sub : Fin n -> Term sig m
   prf : f .=. sub . g
 
 %name Property.(<=) prf
@@ -217,8 +217,8 @@ lteCong prf1 prf2 prf3 = MkLte
   }
 
 export
-Reflexive (SFin k -> Term sig m) (<=) where
-  reflexive = MkLte Var' (\i => sym $ subUnit _)
+Reflexive (Fin k -> Term sig m) (<=) where
+  reflexive = MkLte Var (\i => sym $ subUnit _)
 
 export
 transitive : f <= g -> g <= h -> f <= h
@@ -232,35 +232,38 @@ transitive prf1 prf2 = MkLte
   }
 
 export
-varMax : (f : SFin k -> Term sig m) -> f <= Var'
+varMax : (f : Fin k -> Term sig m) -> f <= Var
 varMax f = MkLte f (\i => Refl)
 
 export
-compLte : f <= g -> (h : SFin k -> Term sig m) -> f . h <= g . h
+compLte : f <= g -> (h : Fin k -> Term sig m) -> f . h <= g . h
 compLte prf h = MkLte
   { sub = prf.sub
   , prf = \i => Calc $
     |~ f <$> h i
-    ~~ (prf.sub . g) <$> h i ...(subCong prf.prf (h i))
+    ~~ (prf.sub . g) <$> h i ...(subExtensional prf.prf (h i))
     ~~ prf.sub <$> g <$> h i ...(subAssoc prf.sub g (h i))
   }
 
 export
 lteExtend :
   {p : Property sig k} ->
-  {f : SFin k -> Term sig m} ->
-  {g : SFin k -> Term sig n} ->
+  {f : Fin k -> Term sig m} ->
+  {g : Fin k -> Term sig n} ->
   (prf : f <= g) ->
   p.Prop f ->
   (Extension p g).Prop prf.sub
 lteExtend prf x = p.cong prf.prf x
 
--- Maximal ---------------------------------------------------------------------
+-- Most General ----------------------------------------------------------------
+
+-- public export
+-- record MostGeneral (p : Property sig k) where
 
 public export
 Max : Property sig k -> Property sig k
 Max p = MkProp
-  { Prop = \f => (p.Prop f, forall n. (g : SFin k -> Term sig n) -> p.Prop g -> g <= f)
+  { Prop = \f => (p.Prop f, forall n. (g : Fin k -> Term sig n) -> p.Prop g -> g <= f)
   , cong = \cong, (x, max) => (p.cong cong x, \g, y => lteCong (\_ => Refl) cong (max g y))
   }
 
@@ -278,8 +281,8 @@ record DClosed (p : Property sig k) where
   constructor MkDClosed
   closed :
     forall m, n.
-    (f : SFin k -> Term sig m) ->
-    (g : SFin k -> Term sig n) ->
+    (f : Fin k -> Term sig m) ->
+    (g : Fin k -> Term sig n) ->
     f <= g ->
     p.Prop g ->
     p.Prop f
@@ -290,18 +293,18 @@ export
 unifiesDClosed : (t, u : Term sig k) -> DClosed (Unifies t u)
 unifiesDClosed t u = MkDClosed (\f, g, prf1, prf2 => Calc $
   |~ f <$> t
-  ~~ (prf1.sub . g) <$> t ...(subCong prf1.prf t)
+  ~~ (prf1.sub . g) <$> t ...(subExtensional prf1.prf t)
   ~~ prf1.sub <$> g <$> t ...(subAssoc prf1.sub g t)
   ~~ prf1.sub <$> g <$> u ...(cong (prf1.sub <$>) prf2)
   ~~ (prf1.sub . g) <$> u ..<(subAssoc prf1.sub g u)
-  ~~ f <$> u              ..<(subCong prf1.prf u))
+  ~~ f <$> u              ..<(subExtensional prf1.prf u))
 
 export
 optimistLemma :
   {ps : Vect _ (Property sig j)} ->
-  {a : SFin j -> Term sig k} ->
-  {f : SFin k -> Term sig m} ->
-  {g : SFin m -> Term sig n} ->
+  {a : Fin j -> Term sig k} ->
+  {f : Fin k -> Term sig m} ->
+  {g : Fin m -> Term sig n} ->
   DClosed p ->
   (Max (Extension p a)).Prop f ->
   (Max (Extension (All ps) (f . a))).Prop g ->
@@ -312,14 +315,14 @@ optimistLemma prf (x, max1) (y, max2) =
     )
   , \h, (x' :: y') =>
     let prf1 = max1 h x' in
-    let y'' = (All ps).cong (\i => trans (subCong prf1.prf (a i)) (subAssoc prf1.sub f (a i))) y' in
+    let y'' = (All ps).cong (\i => trans (subExtensional prf1.prf (a i)) (subAssoc prf1.sub f (a i))) y' in
     let prf2 = max2 prf1.sub y'' in
     MkLte
       { sub = prf2.sub
       , prf = \i => Calc $
         |~ h i
         ~~ prf1.sub <$> f i         ...(prf1.prf i)
-        ~~ (prf2.sub . g) <$> f i   ...(subCong (prf2.prf) (f i))
+        ~~ (prf2.sub . g) <$> f i   ...(subExtensional (prf2.prf) (f i))
         ~~ prf2.sub <$> (g <$> f i) ...(subAssoc prf2.sub g (f i))
       }
   )
@@ -331,8 +334,8 @@ 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} ->
+  {a : Fin j -> Term sig k} ->
+  {f : Fin k -> Term sig m} ->
   (Max (Extension p a)).Prop f ->
   Nothing (Extension (All ps) (f . a)) ->
   Nothing (Extension (All (p :: ps)) a)