\import Logic.Accessible
\import Logic.Rewriting.ARS.AbstractReductionSystem
\import Logic
\import Logic.Meta
\import Relation.Truncated
\import Set

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

\truncated \data HasNormalForm {A : SimpleARS} (a : A) : \Prop
  | normal-form (b : A) (isNormalForm b) (a ~>_* b)

\func isNormalizing (A : SimpleARS) : \Prop => \Pi (a : A) -> HasNormalForm a

\func Acc-Trans {A : \Set} (R : Rel A) (a : A) : \Prop
  => Acc (TransClosure R) a

\lemma Acc=>AccTrans {A : \Set} {R : Rel A} {a : A} (acc : Acc R a) : Acc (TransClosure R) a \elim acc
  | acc r => acc \case \elim __ \with {
    | tc-direct b<a => Acc=>AccTrans (r b<a)
    | tc-connect b<*c c<a => \case Acc=>AccTrans (r c<a) \with {
      | acc h => h b<*c
    }
  }

\func isTerminating (A : SimpleARS) : \Prop => \Pi (a : A) -> Acc (\lam x y => y ~> x) a

\lemma Termination=>Normalization {A : SimpleARS} (dec : \Pi (a : A) -> Dec (∃ (a' : A) (a ~> a')))
                                  (a : A)
                                  (term : Acc (\lam x y => y ~> x) a) : HasNormalForm a =>
  well-founded-induction-transitive
      HasNormalForm
      (\lam z step => \case dec z \with {
        | yes (inP (x, z~>x)) => \case (step x (tc-direct z~>x)) \with {
          | normal-form e nfe x~>*e => normal-form e nfe (~>*-concat (trc-unary z~>x) x~>*e)
        }
        | no n => normal-form z (\lam {b} z~>b => n (inP (b, z~>b))) trc-direct'
      })
      a
      (Acc=>AccTrans term)

\func well-founded-induction
  {A : \Set} {R : Rel A} (C : A -> \Type)
  (induction : \Pi (a : A) (\Pi (b : A) (R b a) -> C b) -> C a)
  (a : A) (a-is-accessible : Acc R a) : C a
\elim a-is-accessible
  | acc successors => induction a (\lam b a~>b => well-founded-induction C induction b (successors a~>b))

\func well-founded-induction-transitive {A : \Set} {R : Rel A} (C : A -> \Type)
                                        (induction : \Pi (a : A) (\Pi (b : A) (TransClosure R b a) -> C b) -> C a)
                                        (a : A) (a-is-accessible : Acc-Trans R a) : C a \elim a-is-accessible
  | acc successors => induction a (\lam b a~>b => well-founded-induction C induction b (successors a~>b))


\func one-step-reduction {A : SimpleARS} (a : A) : \Set => \Sigma (b : A) (a ~> b)

\data ReductionPath {A : SimpleARS} (a : A)
  | branch (b : A) (ReductionPath b) (a ~> b)
  | leaf (isNormalForm a)