path: root/src/Data/Term/Property.idr

module Data.Term.Property

import Data.Term

import public Data.Vect.Quantifiers
import Data.Vect.Properties.Index
import Data.Vect.Quantifiers.Extra

import Syntax.PreorderReasoning

%prefix_record_projections off

-- Definition ------------------------------------------------------------------

public export
record Property (sig : Signature) (k : Nat) where
  constructor MkProp
  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

-- Instances -------------------------------------------------------------------

public export
Unifies : Term sig k -> Term sig k -> Property sig k
Unifies t u = MkProp
  { Prop = \f => f <$> t = f <$> u
  , cong = \_, _, cong, prf => Calc $
    |~ _ <$> t
    ~~ _ <$> t ..<(subExtensional cong t)
    ~~ _ <$> u ...(prf)
    ~~ _ <$> u ...(subExtensional cong u)
  }

public export
All : Vect n (Property sig k) -> Property sig k
All ps = MkProp (\f => All (\p => p.Prop f) ps) (\f, g, cong => mapRel (\p => p.cong f g cong))

public export
UnifiesAll : Vect n (Term sig k) -> Vect n (Term sig k) -> Property sig k
UnifiesAll ts us = All (zipWith Unifies ts us)

-- Equivalence -----------------------------------------------------------------

public export
record (<=>) (p, q : Property sig k) where
  constructor MkEquivalence
  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

export
Reflexive (Property sig k) (<=>) where
  reflexive = MkEquivalence (\_ => id) (\_ => id)

export
Symmetric (Property sig k) (<=>) where
  symmetric prf = MkEquivalence prf.rightToLeft prf.leftToRight

export
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 :
  {0 k : Nat} ->
  (0 op : sig.Operator k) ->
  (ts, us : Vect k (Term sig j)) ->
  Unifies (Op op ts) (Op op us) <=> UnifiesAll ts us
unifiesOp op ts us = MkEquivalence
  { leftToRight = \f, prf => leftToRight ts us f (opInjectiveTs' prf)
  , rightToLeft = \f, prf => cong (Op op) $ rightToLeft ts us f prf
  }
  where
  leftToRight :
    forall k.
    (ts, us : Vect k (Term sig j)) ->
    (0 f : (Fin j -> Term sig n)) ->
    map (f <$>) ts = map (f <$>) us ->
    (UnifiesAll ts us).Prop f
  leftToRight [] [] f prf = []
  leftToRight (t :: ts) (u :: us) f prf =
    fst (biinj (::) prf) :: leftToRight ts us f (snd $ biinj (::) prf)

  rightToLeft :
    forall k.
    (ts, us : Vect k (Term sig j)) ->
    (0 f : (Fin j -> Term sig n)) ->
    (UnifiesAll ts us).Prop f ->
    map (f <$>) ts = map (f <$>) us
  rightToLeft [] [] f [] = Refl
  rightToLeft (t :: ts) (u :: us) f (prf :: prfs) = cong2 (::) prf (rightToLeft ts us f prfs)

-- Nothing ---------------------------------------------------------------------

public export 0
Nothing : Property sig k -> Type
Nothing p = forall n. (f : Fin k -> Term sig n) -> Not (p.Prop f)

-- Properties

export
nothingEquiv : p <=> q -> Nothing p -> Nothing q
nothingEquiv eq absurd f x = absurd f (eq.rightToLeft f x)

-- Extensions ------------------------------------------------------------------

public export
Extension : Property sig k -> (Fin k -> Term sig n) -> Property sig n
Extension p f = MkProp
  { Prop = \g => p.Prop (g . f)
  , cong = \g, h, prf => p.cong (g . f) (h . f) (\i => subExtensional prf (f i))
  }

-- Properties

export
nothingExtends : Nothing p -> Nothing (Extension p f)
nothingExtends absurd g x = void $ absurd (g . f) x

export
extendCong2 :
  {f, g : Fin n -> Term sig k} ->
  {p, q : Property sig n} ->
  f .=. g ->
  p <=> q ->
  Extension p f <=> Extension q g
extendCong2 prf1 prf2 = MkEquivalence
  (\h, x => prf2.leftToRight (h . g) $ p.cong _ _ (\i => cong (h <$>) $ prf1 i) x)
  (\h, x => prf2.rightToLeft (h . f) $ q.cong _ _ (\i => sym $ cong (h <$>) $ prf1 i) x)

export
extendCong :
  (f : Fin n -> Term sig k) ->
  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 = MkEquivalence (\_, x => x) (\_, x => x)

export
extendAssoc :
  (p : Property sig j) ->
  (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
    (\h => p.cong _ _ (\i => subAssoc h g (f i)))
    (\h => p.cong _ _ (\i => sym $ subAssoc h g (f i)))

export
extendUnify :
  (t, u : Term sig j) ->
  (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   ...(subExtensional (\i => subAssoc h g (f i)) t)
      ~~ (h . (g . f)) <$> u   ...(prf)
      ~~ ((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 $ 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   ...(subExtensional (\i => subAssoc h g (f i)) u))

export
extendUnifyAll :
  (ts, us : Vect n (Term sig j)) ->
  (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, [] => [])
extendUnifyAll (t :: ts) (u :: us) f g =
  let head = extendUnify t u f g in
  let tail = extendUnifyAll ts us f g in
  MkEquivalence
    (\h, (x :: xs) => head.leftToRight h x :: tail.leftToRight h xs)
    (\h, (x :: xs) => head.rightToLeft h x :: tail.rightToLeft h xs)

-- 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 ...(subExtensional 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

-- Most General ----------------------------------------------------------------

public export
record MostGeneral (p : Property sig k) (f : Fin k -> Term sig n) where
  constructor MkMostGeneral
  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
  unique :
    forall j.
    (g : Fin k -> Term sig j) ->
    (v : p.Prop g) ->
    (h : Fin n -> Term sig j) ->
    g .=. h . f ->
    h .=. universal g v

%name MostGeneral mg

export
varMostGeneral : p.Prop Var -> MostGeneral p Var
varMostGeneral v =
  MkMostGeneral
    { valid = v
    , universal = \g, _ => g
    , factors = \g, _, x => Refl
    , unique = \g, _, h, prf', x => sym $ prf' x
    }

public export
Max : Property sig k -> Property sig k
Max p = MkProp
  { Prop = MostGeneral p
  , cong = \f, g, prf, mg =>
    MkMostGeneral
      { 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)
      , unique = \h, v, i, prf' =>
        mg.unique h v i $
        \x => Calc $
          |~ h x
          ~~ i <$> g x ...(prf' x)
          ~~ i <$> f x ...(compCongR i (\x => sym $ prf x) x)
      }
  }

export
maxCong : p <=> q -> Max p <=> Max q
maxCong prf = MkEquivalence
  { leftToRight = \f, mg =>
    MkMostGeneral
      { valid = prf.leftToRight f mg.valid
      , universal = \g, v => mg.universal g (prf.rightToLeft g v)
      , factors = \g, v => mg.factors g (prf.rightToLeft g v)
      , unique = \g, v => mg.unique g (prf.rightToLeft g v)
      }
  , rightToLeft = \f, mg =>
    MkMostGeneral
      { valid = prf.rightToLeft f mg.valid
      , universal = \g, v => mg.universal g (prf.leftToRight g v)
      , factors = \g, v => mg.factors g (prf.leftToRight g v)
      , unique = \g, v => mg.unique g (prf.leftToRight g v)
      }
  }

-- Downward Closed -------------------------------------------------------------

public export
record DClosed (p : Property sig k) where
  constructor MkDClosed
  closed :
    forall m, n.
    (f : Fin k -> Term sig m) ->
    (g : Fin k -> Term sig n) ->
    f <= g ->
    p.Prop g ->
    p.Prop f

-- Properties

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 ...(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              ..<(subExtensional prf1.prf u))

export
optimistLemma :
  {ps : Vect _ (Property sig j)} ->
  {a : Fin j -> Term sig k} ->
  {f : Fin k -> Term sig m} ->
  {g : Fin m -> Term sig n} ->
  DClosed p ->
  (MostGeneral (Extension p a)) f ->
  (MostGeneral (Extension (All ps) (f . a))) g ->
  (MostGeneral (Extension (All (p :: ps)) a)) (g . f)
optimistLemma closed mg mg' =
  MkMostGeneral
    { valid =
      closed.closed ((g . f) . a) (f . a) (compLte (MkLte g (\i => Refl)) a) mg.valid ::
      (All ps).cong _ _ (\i => sym $ subAssoc g f (a i)) mg'.valid
    , universal = universal
    , factors = factors
    , unique = unique
    }
  where
  coerce :
    forall i.
    (h : Fin k -> Term sig i) ->
    (v : (Extension p a).Prop h) ->
    (Extension (All ps) a).Prop h ->
    (Extension (All ps) (f . a)).Prop (mg.universal h v)
  coerce h v =
    (All ps).cong _ _
        (\x => Calc $
          |~ h <$> a x
          ~~ mg.universal h v . f <$> a x   ...(subExtensional (mg.factors h v) (a x))
          ~~ mg.universal h v <$> f <$> a x ...(subAssoc (mg.universal h v) f (a x)))
  universal :
    forall i.
    (h : Fin k -> Term sig i) ->
    (vs : (Extension (All (p :: ps)) a).Prop h) ->
    Fin n -> Term sig i
  universal h (v :: vs) =
    mg'.universal (mg.universal h v) (coerce h v vs)

  factors :
    forall i.
    (h : Fin k -> Term sig i) ->
    (vs : (Extension (All (p :: ps)) a).Prop h) ->
    h .=. universal h vs . (g . f)
  factors h (v :: vs) x = Calc $
    |~ h x
    ~~ mg.universal h v <$> f x                                       ...(mg.factors h v x)
    ~~ mg'.universal (mg.universal h v) (coerce h v vs) . g <$> f x   ...(subExtensional (mg'.factors (mg.universal h v) (coerce h v vs)) (f x))
    ~~ mg'.universal (mg.universal h v) (coerce h v vs) <$> g <$> f x ...(subAssoc (mg'.universal (mg.universal h v) (coerce h v vs)) g (f x))

  unique :
    forall i.
    (h : Fin k -> Term sig i) ->
    (vs : (Extension (All (p :: ps)) a).Prop h) ->
    (r : Fin n -> Term sig i) ->
    h .=. r . (g . f) ->
    r .=. universal h vs
  unique h (v :: vs) r prf =
    mg'.unique (mg.universal h v) (coerce h v vs) r $
    \x => sym $
      mg.unique h v (r . g)
        (\x => Calc $
          |~ h x
          ~~ r <$> g <$> f x ...(prf x)
          ~~ r . g <$> f x   ..<(subAssoc r g (f x)))
        x

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 : 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)
failTail mg absurd g (v :: vs) =
  absurd (mg.universal g v) $
    (All ps).cong _ _
      (\x => Calc $
        |~ g <$> a x
        ~~ mg.universal g v . f <$> a x   ...(subExtensional (mg.factors g v) (a x))
        ~~ mg.universal g v <$> f <$> a x ...(subAssoc (mg.universal g v) f (a x)))
      vs