From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Lia.

From Padec Require Import ZUtils.
From Padec Require Import NatUtils.
From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Stream.
From Padec Require Import Stream_Length.
From Padec Require Import Exec.
From Padec Require Import BoolSet.
From Padec Require Import Self_Stabilization.

Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Section At_Steps.

  Context {Chans: Channels} {Net: Network} {Algo: Algorithm}.

  Definition At_N_steps N: (Exec -> Prop) -> (Exec -> Prop) :=
    fun P e => length_until_P (A := Env) P e N.

  Instance At_N_steps_compat: Proper fequiv At_N_steps.

  Lemma After_SN_steps_notP:
    forall N P (e: Exec), At_N_steps (S N) P e -> ~P e.

  Lemma At_N_steps_Eventually:
    forall N P e, At_N_steps N P e -> Eventually P e.

  Lemma Reachable_Steps:
    forall (P: Exec -> Prop),
      (forall e, (Proper pequiv e -> P e) \/ ~ P e) ->
      forall e, Proper pequiv e -> Eventually P e ->
                exists N, At_N_steps N P e.

  Lemma At_N_steps_unique:
    forall e P N1 N2,
      Proper pequiv e ->
      At_N_steps N1 P e -> At_N_steps N2 P e -> N1 = N2.

  Fixpoint count_steps_aux (P: Exec -> Prop) (e: Exec)
           (F: Finally P e): nat :=
    match F in Finally _ _ return nat with
    | finally_now _ _ _ => 0
    | finally_not_yet _ _ F' => S (count_steps_aux F')
    end.

  Instance count_steps_aux_compat:
    Proper (respectful_dep_param
              (equiv (A:=nat))
              ((Exec -> Prop)::Exec::nil)
              (fequiv,(pequiv,tt))
              (inr Finally::nil)) (@count_steps_aux).

  Definition count_steps (P: Exec -> Prop) (e: Exec)
             (P_dec: Weak_Dec pequiv P) (pe: Proper pequiv e)
             (he: Eventually P e): nat :=
    count_steps_aux (Eventually_Dec_Finally' P_dec pe he).

  Instance count_steps_compat:
    Proper (respectful_dep_param
              (equiv (A:=nat))
              ((Exec -> Prop)::Exec::nil)
              (fequiv,(pequiv,tt))
              (inr (fun P e => Weak_Dec pequiv P)
                   ::inl (fun P e => Proper pequiv e)
                   ::inl Eventually :: nil)) (@count_steps).

  Theorem steps_equivalence:
    forall (P: Exec -> Prop) (P_dec: Weak_Dec pequiv P),
    forall e (pe: Proper pequiv e) (he: Eventually P e) N,
      count_steps P_dec pe he = N <-> At_N_steps N P e.

  Lemma Finite_exec_Steps:
    forall e (ise: is_exec e),
      finite_exec e <->
      exists N, At_N_steps N (fun e => terminal (s_hd e)) e.

  Lemma at_steps_concat:
    forall (P Q: Exec -> Prop) e,
      Always (fun e => Q e -> P e) e ->
      forall np, At_N_steps np P e ->
                 forall nq,
                   (forall w: Finally P e, At_N_steps nq Q (When w)) ->
                   At_N_steps (np + nq) Q e.

  Lemma steps_induction:
    forall (Q: Exec -> Prop) (Pot: nat -> Exec -> Prop)
           (Q_means_Always: forall e, Q e -> Always Q e)
           (m: nat -> nat),
      (forall e, Q e -> Pot 0 e -> forall n, Pot n e) ->
      (forall e k, Q e -> Pot (S k) e ->
                   At_N_steps (m (S k)) (Pot k) e) ->
      forall n e, Q e -> Pot n e ->
                  At_N_steps (sum m n) (Pot 0) e.

  Lemma steps_induction_le:
    forall (Q: Exec -> Prop) (Pot: nat -> Exec -> Prop)
           
           (Pot_wd: forall n e, Q e -> {Pot n e} + { ~Pot n e})
           (Pot_compat: Proper fequiv Pot)
           
           (Q_means_Always: forall e, Q e -> Always Q e)
           (Q_means_compat: forall e, Q e -> Proper pequiv e)
           (m: nat -> nat),
      (forall e, Q e -> Pot 0 e -> forall n, Pot n e) ->
      (forall e k, Q e -> Pot (S k) e ->
                   exists n, n <= m (S k) /\
                             At_N_steps n (Pot k) e) ->
      forall N e, Q e -> Pot N e ->
                  exists n, n <= sum m N /\
                            At_N_steps n (Pot 0) e.

  Definition Steps_complexity N (P Q: Exec -> Prop) :=
    forall exec, Q exec -> exists n, n <= N /\
                                     At_N_steps n P exec.

  Lemma Steps_complexity_compat:
    forall n1 n2 (en: n1 == n2)
           P1 P2 (eP: fequiv P1 P2)
           (Q1 Q2: Exec -> Prop) (eQ: fequiv Q1 Q2)
           (hp1: forall e, Q1 e -> Proper pequiv e)
           (hp2: forall e, Q2 e -> Proper pequiv e),
      Steps_complexity n1 P1 Q1 == Steps_complexity n2 P2 Q2.

  Lemma Steps_complexity_reach:
    forall N P Q, Steps_complexity N P Q ->
                  forall e, Q e -> Eventually P e.

  Lemma At_N_steps_monotonic:
    forall (Q P P': Exec -> Prop)
           (inclP: forall e, Always Q e -> P e -> P' e)
           n e,
      Always Q e -> Always (fun e => P' e \/ ~P' e) e ->
      At_N_steps n P e ->
      exists n', n' <= n /\ At_N_steps n' P' e.

  Lemma Steps_complexity_monotonic:
    forall
      (Q Q': Exec -> Prop) (inclQ: forall e, Q' e -> Q e)
      (Q_means_Always: forall e, Q e -> Always Q e)
      (P P': Exec -> Prop) (inclP: forall e, Q e -> P e -> P' e)
      (clas: forall e, Q e -> P' e \/ ~P' e)
      N,
      Steps_complexity N P Q -> Steps_complexity N P' Q'.

  Lemma Steps_complexity_Acc:
    forall N (P Q: Env -> Prop),
      (forall g g', Q g -> Step g' g -> Q g') ->
      Steps_complexity N (fun e => P (s_hd e))
                       (fun e => Q (s_hd e) /\ is_exec e) ->
      forall g, Q g -> Acc (fun g' g => ~P g /\ Step g' g) g.

  Lemma Steps_complexity_Acc_term:
    forall N (Q: Env -> Prop),
      (forall g g', Q g -> Step g' g -> Q g') ->
      Steps_complexity N (fun e => terminal (s_hd e))
                       (fun e => Q (s_hd e) /\ is_exec e) ->
      forall g, Q g -> Acc (fun g' g => Step g' g) g.

  Lemma Steps_complexity_induction:
    forall (Q: Exec -> Prop) (Pot: nat -> Exec -> Prop)
           
           (Pot_wd: forall n e, Q e -> {Pot n e} + { ~Pot n e})
           (Pot_compat: Proper fequiv Pot)
           
           (Q_means_Always: forall e, Q e -> Always Q e)
           (Q_means_compat: forall e, Q e -> Proper pequiv e)
           (m: nat -> nat),
      (forall e, Q e -> Pot 0 e -> forall n, Pot n e) ->
      (forall k, Steps_complexity (m (S k)) (Pot k)
                                  (fun e => Q e /\ Pot (S k) e)) ->
      forall n, Steps_complexity (sum m n) (Pot 0)
                                 (fun e => Q e /\ Pot n e).

  Lemma Steps_complexity_add:
    forall (Q P1 P2: Exec -> Prop)
           (P1_wd: forall e, Q e -> {P1 e} + { ~P1 e})
           (P2_wd: forall e, Q e -> {P2 e} + { ~P2 e})
           (P1_compat: Proper fequiv P1)
           (P2_compat: Proper fequiv P2)
           (Q_means_Always: forall e, Q e -> Always Q e)
           (Q_means_compat: forall e, Q e -> Proper pequiv e)
           n1 n2,
      (forall e, Q e -> P2 e -> P1 e) ->
      Steps_complexity n1 P1 Q ->
      Steps_complexity n2 P2 (fun e => Q e /\ P1 e) ->
      Steps_complexity (n1 + n2) P2 Q.

  Lemma exec_bounded_length:
    forall (Q: Exec -> Prop) (Q_preserved: forall g e, Q (s_cons g e) ->
                                                       Q e)
           (P: Exec -> Prop) (P_clas: forall e, Q e -> P e \/ ~ P e)
           (P_Q: forall g, Q (s_one g) -> P (s_one g)),
    forall (cost: Exec -> nat)
           (cost_decreases: forall g e,
               Q (s_cons g e) -> ~ P (s_cons g e) ->
               cost e < cost (s_cons g e))
           (cost_0: forall e, Q e -> cost e = 0 -> P e),
    forall e, Q e -> exists ne, At_N_steps ne P e /\ ne <= cost e.

  Theorem Steps_complexity_Bound_Cost:
    forall (Q: Exec -> Prop)
           (Q_preserved: forall g e, Q (s_cons g e) -> Q e)
           (P: Exec -> Prop)
           (P_clas: forall e, Q e -> P e \/ ~ P e)
           (P_Q: forall g, Q (s_one g) -> P (s_one g)),
    forall (cost: Exec -> nat)
           (cost_decreases: forall g e,
               Q (s_cons g e) -> ~ P (s_cons g e) ->
               cost e < cost (s_cons g e))
           (cost_0: forall e, Q e -> cost e = 0 -> P e),
    forall (N: nat)
           (cost_bound: forall e, Q e -> cost e <= N),
      Steps_complexity N P Q.

  Theorem Non_Leg_Steps_min_bound :
    forall exec N (P Q: Exec -> Prop),
      Proper pequiv exec ->
      Q exec ->
      At_N_steps N P exec ->
      forall n, n<N -> ~ Steps_complexity n P Q.

End At_Steps.

Section Before_Steps.
  Context {Chans: Channels} {Net: Network} {Algo: Algorithm}.

  Inductive Before_N_steps: nat -> (Exec -> Prop) -> (Exec -> Prop) :=
  | at_P: forall (P: Exec -> Prop) e n, P e -> Before_N_steps n P e
  | add_step: forall (P: Exec -> Prop) g e n,
      Before_N_steps n P e -> Before_N_steps (S n) P (s_cons g e).

  Lemma Before_N_steps_equiv:
    forall P e,
      Always (fun e => P e \/ ~P e) e ->
      forall n, Before_N_steps n P e <->
                exists n', n' <= n /\ At_N_steps n' P e.

End Before_Steps.

Section Nb_Steps.

  Context {Chans: Channels} {Net: Network} {Algo: Algorithm}.

  Fixpoint Nb_Steps (P: Exec -> bool) (T: Exec -> Prop)
           (e: Exec) (f: Finally T e): nat :=
    match f in Finally _ _ return nat with
    | finally_now _ _ _ => 0
    | @finally_not_yet _ _ g' e' _ F' =>
      if P (s_cons g' e') then S (Nb_Steps P F')
      else Nb_Steps P F'
    end.

  Instance Nb_Steps_compat:
    Proper (respectful_dep_param
              (equiv (A:=nat))
              ((Exec -> bool)::(Exec -> Prop)::Exec::nil)
              (fequiv,(fequiv,(pequiv,tt)))
              (inr (fun P T e => Finally T e)::nil)) Nb_Steps.

  Inductive Nb_Steps_le (P: Exec -> bool) (T: Exec -> Prop):
    nat -> Exec -> Prop :=
  | at_T: forall k e, T e -> Nb_Steps_le P T k e
  | add_stepP: forall k g e, Nb_Steps_le P T k e ->
                             P (s_cons g e) = true ->
                             Nb_Steps_le P T (S k) (s_cons g e)
  | add_stepNP: forall k g e, Nb_Steps_le P T k e ->
                              P (s_cons g e) = false ->
                              Nb_Steps_le P T k (s_cons g e).

  Instance Nb_Steps_le_compat: Proper fequiv Nb_Steps_le.

  Lemma Nb_Steps_Finally:
    forall P T e n, Weak_Dec pequiv T ->
                    Proper pequiv e -> Nb_Steps_le P T n e ->
                    Finally T e.

  Lemma Nb_Steps_equiv:
    forall P T e (f: Finally T e),
    forall n, Nb_Steps_le P T n e <-> Nb_Steps P f <= n.

  Lemma Nb_Steps_0:
    forall P T e, Weak_Dec pequiv T ->
                   Proper pequiv e ->
                   Always ( fun e => match e with
                                     | s_one _ => True
                                     | s_cons g e =>
                                       P (s_cons g e) = false -> T e -> T (s_cons g e) end) e ->
                   Nb_Steps_le P T 0 e ->
                   T e.

  Lemma Nb_Steps_more:
    forall P T n e, Weak_Dec pequiv T -> Proper pequiv e ->
                    Nb_Steps_le P T n e -> forall n', n' >= n -> Nb_Steps_le P T n' e.

  Lemma Nb_Steps_le_wd:
    forall P T e, Finally T e ->
                  forall n, {Nb_Steps_le P T n e} +
                            {~Nb_Steps_le P T n e}.

End Nb_Steps.

Close Scope nat_scope.
Close Scope signature_scope.
Unset Implicit Arguments.