\import Logic.Rewriting.ARS.AbstractReductionSystem
\import Logic
\import Paths
\import Paths.Meta
\import Relation.Truncated
\import Logic.Rewriting.ARS.Termination

\truncated \data StrongJoin {A : SimpleARS} (b c : A) : \Prop
  | strong-join (d : A) (b ~>_= d) (c ~>_* d)

\func isStronglyConfluent (A : SimpleARS) : \Prop =>
  \Pi {a b c : A} (p : a ~> b) (q : a ~> c) -> StrongJoin b c

\func isChurchRosser (A : SimpleARS) : \Prop =>
  \Pi {a b : A} (a <~>* b) -> Join a b

\func isConfluent (A : SimpleARS) : \Prop =>
  \Pi {a b c : A} (a ~>_* b) (a ~>_* c) -> Join b c

\func isLocallyConfluent (A : SimpleARS) : \Prop =>
  \Pi {a b c : A} (a ~> b) (a ~> c) -> Join b c

\func hasUniqueNormalFormsWrtReduction (A : SimpleARS) : \Prop =>
  \Pi {a b c : A} (a ~>_* b) (a ~>_* c) (isNormalForm b) (isNormalForm c) -> b = c

\func hasUniqueNormalForms (A : SimpleARS) : \Prop =>
  \Pi {a b : A} (a <~>* b) (isNormalForm a) (isNormalForm b) -> a = b

\func hasNormalFormProperty (A : SimpleARS) : \Prop =>
  \Pi {a b : A} (a <~>* b) (isNormalForm b) -> a ~>_* b

\lemma ChurchRosser=>Confluence {A : SimpleARS} (cr : isChurchRosser A) : isConfluent A =>
  \lam {a} {b} {c} a~>*b a~>*c => cr {b} {c} (<~>*-compose a (<~>*-reverse (~>*=><~>* a~>*b)) (~>*=><~>* a~>*c))

\lemma Confluence=>ChurchRosser {A : SimpleARS} (conf : isConfluent A) : isChurchRosser A =>
  \lam {a} {b} a<~>*b => conf=>rc-helper a b a<~>*b
  \where {
    \lemma conf=>rc-helper (a b : A) (a<~>*b : a <~>* b) : Join a b \elim a<~>*b
      | trc-direct p => join a trc-direct' (trc-direct (inv p))
      | trc-connect c a<~>c c<~>*b => \let join-c-b : Join c b => conf=>rc-helper c b c<~>*b \in \case join-c-b, a<~>c \with {
        | join c' c~>*c' b~>*c', sc-left a~>c => join c' (trc-connect c a~>c c~>*c') b~>*c'
        | join c' c~>*c' b~>*c', sc-right c~>a => \let join-a-c' : Join a c' => conf {c} {a} {c'} (trc-unary c~>a) c~>*c'
                                                  \in Join.append-right b~>*c' join-a-c'
      }
  }

\lemma ChurchRosser=Confluence {A : SimpleARS} : isChurchRosser A = isConfluent A =>
  propExt ChurchRosser=>Confluence Confluence=>ChurchRosser

\lemma StrongConfluence=>Confluence {A : SimpleARS} (sconf : isStronglyConfluent A) : isConfluent A =>
  strong-join=>Confluence
  \where {
    \lemma SCR=>strong-join {a b c : A} (a~>*b : a ~>_* b) (a~>c : a ~> c) : StrongJoin b c \elim a~>*b
      | trc-direct p => strong-join c (rc-rel (rewriteI p a~>c)) trc-direct'
      | trc-connect c' a~>c' c'~>*b => \let strong-join-c-c' => sconf a~>c' a~>c \in \case strong-join-c-c' \with {
        | strong-join d c~>_=d c~>*d => \case \elim c~>_=d \with {
          | rc-id c'=d => strong-join b (rc-id idp) (~>*-concat c~>*d (transport (__ ~>_* b) c'=d c'~>*b))
          | rc-rel c'~>d => \let sjoin-b-d => SCR=>strong-join c'~>*b c'~>d
                            \in \case sjoin-b-d \with {
              | strong-join d' b~>_=d d~>*d' => strong-join d' b~>_=d (~>*-concat c~>*d d~>*d')
            }
        }
      }

    \lemma strong-join=>Confluence {x y z : A} (x~>*y : x ~>_* y) (x~>*z : x ~>_* z) : Join y z \elim x~>*z
      | trc-direct p => join y trc-direct' (rewriteI p x~>*y)
      | trc-connect c x~>c c~>*z => \let partial => SCR=>strong-join x~>*y x~>c \in \case partial \with {
        | strong-join d y~>_=d c~>*d => \let inner-join => strong-join=>Confluence c~>*d c~>*z
                                        \in \case inner-join \with {
            | join c1 d~>c1 z~>c1 => join c1 (~>_=-append y~>_=d d~>c1) z~>c1
          }
      }
  }

\lemma Confluence=>LocalConfluence {A : SimpleARS} (conf : isConfluent A) : isLocallyConfluent A =>
  \lam {a} {b} {c} a~>b a~>c => conf (trc-unary a~>b) (trc-unary a~>c)

\lemma Confluence=>NormalFormProperty {A : SimpleARS} (conf : isConfluent A) : hasNormalFormProperty A =>
  \lam {a} {b} a<~>*b bnf => conf=>nfp-helper a b a<~>*b bnf
  \where {
    \lemma conf=>nfp-helper (a b : A) (a<~>*b : a <~>* b) (bnf : isNormalForm b) : a ~>_* b \elim a<~>*b
      | trc-direct a=b => trc-direct a=b
      | trc-connect c a<~>c c<~>*b => \let c~>*b => conf=>nfp-helper c b c<~>*b bnf \in \case \elim a<~>c \with {
        | sc-left a~>c => trc-connect c a~>c c~>*b
        | sc-right c~>a => \let join-a-b => conf (trc-unary c~>a) c~>*b \in \case \elim join-a-b \with {
          | join c' a~>*c' b~>*c' => \case \elim b~>*c' \with {
            | trc-direct c'=b => rewrite c'=b a~>*c'
            | trc-connect c1 b~>c1 _ => absurd (bnf b~>c1)
          }
        }
      }
  }

\lemma NormalFormProperty=>UniqueNormalForms {A : SimpleARS} (nfp : hasNormalFormProperty A) : hasUniqueNormalForms A =>
  \lam {a} {b} a<~>*b anf bnf => \case (nfp a<~>*b bnf) \with {
    | trc-direct a=b => a=b
    | trc-connect c r t => absurd (anf r)
  }

\lemma UniqueNormalForms=>UniqueNormalFormsWrtReduction {A : SimpleARS} (unf : hasUniqueNormalForms A) : hasUniqueNormalFormsWrtReduction A =>
  \lam {a} {b} {c} a~>*b a~>*c bnf cnf => unf (<~>*-compose a (<~>*-reverse (~>*=><~>* a~>*b)) (~>*=><~>* a~>*c)) bnf cnf

\lemma Normalization+UniqueNormalForms=>Confluence {A : SimpleARS} (norm : isNormalizing A) (unf : hasUniqueNormalForms A) : isConfluent A =>
  \lam {a} {b} {c} a~>*b a~>*c => \case (norm b), (norm c) \with {
    | normal-form b' b'nf b~>*b', normal-form c' c'nf c~>*c' =>
      \let b'=c' => UniqueNormalForms=>UniqueNormalFormsWrtReduction unf (~>*-concat a~>*b b~>*b') (~>*-concat a~>*c c~>*c') b'nf c'nf
      \in join b' b~>*b' (rewrite b'=c' c~>*c')
  }

\lemma Termination+LocalConfluence=>Confluence {A : SimpleARS} (term : isTerminating A) (lconf : isLocallyConfluent A): isConfluent A =>
  \lam {a} => well-founded-induction-transitive
      (\lam a => \Pi {b c : A} (p1 : a ~>_* b) (p2 : a ~>_* c) -> Join b c) -- we want to prove confluence for each element
      (\lam x step {b'} {c'} x~>*b' x~>*c' => \case x~>*b', x~>*c' \with {
        | trc-direct x=b', _ => join c' (rewriteI x=b' x~>*c') trc-direct'
        | _, trc-direct x=c' => join b' trc-direct' (rewriteI x=c' x~>*b')
        | trc-connect e x~>e e~>*b', trc-connect d x~>d d~>*c' => \case (lconf x~>e x~>d) \with {
          | join u e~>*u d~>*u => \let | join-b'-u => step e (tc-direct x~>e) {b'} {u} e~>*b' e~>*u
                                  \in \case \elim join-b'-u \with {
              | join v b'~>*v u~>*v => \let join-v-c' => step d (tc-direct x~>d) {v} {c'} (~>*-concat d~>*u u~>*v) d~>*c'
                                       \in Join.append-left b'~>*v join-v-c'
            }
        }
      })
      a
      (Acc=>AccTrans a (term a))

\lemma Termination=>[LocalConfluence=Confluence] \alias Newman {A : SimpleARS} (term : isTerminating A) :
  isLocallyConfluent A = isConfluent A =>
  propExt (Termination+LocalConfluence=>Confluence term __) Confluence=>LocalConfluence