Prove the optimist's lemma.

1 files changed, 128 insertions, 1 deletions

diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr
index 41fb906..2435c98 100644
--- a/src/Data/Term/Property.idr
+++ b/src/Data/Term/Property.idr
@@ -13,7 +13,7 @@ import Syntax.PreorderReasoning
 public export
 record Property (sig : Signature) (k : Nat) where
   constructor MkProp
-  Prop : forall n. (Fin k -> Term sig n) -> Type
+  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
@@ -141,3 +141,130 @@ extendUnify t u f g h =
       ~~ (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))
+
+-- Ordering --------------------------------------------------------------------
+
+public export
+record (<=) (f : Fin k -> Term sig m) (g : Fin k -> Term sig n) where
+  constructor MkLte
+  sub : Fin n -> Term sig m
+  prf : f .=. sub . g
+
+%name Property.(<=) prf
+
+-- Properties
+
+export
+lteCong : f .=. f' -> g .=. g' -> f <= g -> f' <= g'
+lteCong prf1 prf2 prf3 = MkLte
+  { sub = prf3.sub
+  , prf = \i => Calc $
+    |~ f' i
+    ~~ f i               ...(sym $ prf1 i)
+    ~~ prf3.sub <$> g i  ...(prf3.prf i)
+    ~~ prf3.sub <$> g' i ...(cong (prf3.sub <$>) $ prf2 i)
+  }
+
+export
+Reflexive (Fin k -> Term sig m) (<=) where
+  reflexive = MkLte Var (\i => sym $ subUnit _)
+
+export
+transitive : f <= g -> g <= h -> f <= h
+transitive prf1 prf2 = MkLte
+  { sub = prf1.sub . prf2.sub
+  , prf = \i => Calc $
+    |~ f i
+    ~~ prf1.sub <$> g i              ...(prf1.prf i)
+    ~~ prf1.sub <$> prf2.sub <$> h i ...(cong (prf1.sub <$>) $ prf2.prf i)
+    ~~ (prf1.sub . prf2.sub) <$> h i ...(sym $ subAssoc prf1.sub prf2.sub (h i))
+  }
+
+export
+varMax : (f : Fin k -> Term sig m) -> f <= Var
+varMax f = MkLte f (\i => Refl)
+
+export
+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 ...(subAssoc prf.sub g (h i))
+  }
+
+export
+lteExtend : 
+  {p : Property sig k} ->
+  {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 ---------------------------------------------------------------------
+
+public export
+Max : Property sig k -> Property sig k
+Max p = MkProp
+  { 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))
+  }
+
+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))
+  }
+
+-- Downward Closed -------------------------------------------------------------
+
+public export 0
+DClosed : Property sig k -> Type
+DClosed p =
+  forall m, n.
+  (f : Fin k -> Term sig m) ->
+  (g : Fin k -> Term sig n) ->
+  f <= g ->
+  p.Prop g ->
+  p.Prop f
+
+-- Properties
+
+unifiesDClosed : (t, u : Term sig k) -> DClosed (Unifies t u)
+unifiesDClosed t u f g prf1 prf2 = Calc $
+  |~ f <$> t
+  ~~ (prf1.sub . g) <$> t ...(subCong 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)
+
+optimistLemma :
+  {q : Property sig j} ->
+  {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 q (f . a))).Prop g ->
+  (Max (Extension (All [p, q]) 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'] =>
+    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 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) ...(subAssoc prf2.sub g (f i))
+      }
+  )