Library Padec.Model.Composition_Steps

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

From Padec Require Import WellfoundedUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Stream.
From Padec Require Import Simulation.
From Padec Require Import Stream_Length.
From Padec Require Import Exec.
From Padec Require Import ListUtils.
From Padec Require Import BoolSet.
From Padec Require Import Self_Stabilization.
From Padec Require Import Composition.
From Padec Require Import Fairness.
From Padec Require Import Steps.
From Padec Require Import NatUtils.

Open Scope nat_scope.
Open Scope signature_scope.

Section Tools_For_Composition_Steps_0.

  Lemma Always_True: forall A (s: @Stream A), Always (fun _ => True) s.

  Lemma length_P_equiv:
    forall A (P Q: @Stream A -> Prop) s n,
      WUntil (fun s => P s <-> Q s) (fun s => P s /\ Q s) s ->
      
      length_until_P P s n <-> length_until_P Q s n.

  Lemma Always_conj:
    forall A (P Q: @Stream A -> Prop) s,
      Always P s -> Always Q s -> Always (fun s => P s /\ Q s) s.

  Lemma Forever_P_P:
    forall (A: Type) P (s: @Stream A), Forever P s -> P s.

  Lemma Forever_forall:
    forall (A: Type) P, (forall (s: @Stream A), P s) -> forall s, Forever P s.

End Tools_For_Composition_Steps_0.

Section Tools_For_Composition_Steps.

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

  Definition Has_Moved1 (e: Exec): bool :=
    (existsb (fun n => ACT_b n e) all_nodes).

  Instance Has_Moved1_compat: Proper fequiv Has_Moved1.

  Definition Term := (fun e: Exec => terminal (s_hd e)).

  Lemma Has_Moved1_not_terminal:
    forall e1, is_exec e1 ->
               Has_Moved1 e1 = true -> Term e1 -> False.

  Lemma Has_Moved1_progress:
    forall e1, Proper pequiv e1 -> Has_Moved1 e1 = true ->
               exists g1 e1', e1 =~= s_cons g1 e1' /\ ~ (s_hd e1') =~= g1.

  Lemma Has_Moved1_progress':
    forall g1 e1, Proper pequiv (s_cons g1 e1) -> Has_Moved1 (s_cons g1 e1) = true ->
                  ~ s_hd e1 =~= g1.

  Lemma Has_not_Moved1_same1:
    forall g e, Step (s_hd e) g -> Proper pequiv (s_cons g e) ->
                Has_Moved1 (s_cons g e) = false -> g =~= s_hd e.

  Lemma is_exec_Has_Moved1:
    forall g e, is_exec (s_cons g e) ->
                Has_Moved1 (s_cons g e) = true.

  Lemma Term_wd: Weak_Dec pequiv Term.

  Lemma Term_compat: Proper pequiv Term.

  Definition endS := (fun s:Exec => match s with | s_one _ => True
                                            | s_cons _ _ => False end).
  Definition finiteT := (Finally endS).
  Lemma finite_finiteT:
    forall e: Exec, finiteT e -> finite e.

  Lemma finiteT_finite:
    forall e: Exec, Proper pequiv e -> finite e -> finiteT e.

  Lemma is_exec_finite:
    forall e (ise: is_exec e), Finally Term e -> finiteT e.

  Lemma is_exec_finite':
    forall e (ise: is_exec e), finiteT e -> Finally Term e.

  Lemma is_constant_dec_finite:
    forall (e: Exec) (a: Env),
      Proper pequiv e -> Proper pequiv a ->
      finiteT e -> {is_constant a e} + {~is_constant a e}.

  Lemma finiteT_non_constant_Acc_RSkip:
    forall (e: Exec) (a: Env),
      Proper pequiv e -> finiteT e ->
      ~ is_constant a e -> Acc (Rskip a) e.

  Lemma collapsible_finite:
    forall e: Exec, Proper pequiv e -> finiteT e -> Squeezable e.

  Definition Move :=
    (fun e: Exec => match e with
                    | s_one _ => false
                    | s_cons g e =>
                      if Env_dec (s_hd e) g then false
                      else true
                    end).
  Lemma Move_compat: Proper fequiv Move.

  Lemma Nb_Steps_rewrite:
    forall (e: Exec) (fe: finiteT e) P Q,
      Always (fun e => P e = Q e) e -> Nb_Steps P fe = Nb_Steps Q fe.

  Lemma star_Move:
    forall (e: Exec) (pe: Proper pequiv e) (fe: finiteT e) a
           s (ps: Proper pequiv s) (fs: finiteT s),
      is_cons_star a s e ->
            (~s_hd e =~= s_hd s -> S (Nb_Steps Move fs) =
                                   Nb_Steps Move fe) /\
            (s_hd e =~= s_hd s -> Nb_Steps Move fs =
                                  Nb_Steps Move fe).

  Lemma step_progress:
    forall (g g': Env), Step g g' -> ~ g =~= g'.

  Lemma is_cons_star_finiteT:
    forall (e: Exec) (pe: Proper pequiv e) a
           s (ps: Proper pequiv s),
      finiteT e -> is_cons_star a s e -> finiteT s.

  Lemma same_steps_simulation:
    forall (e: Exec) s (sim: Simulation s e)
           (fe: finiteT e) (fs: finiteT s),
      Proper pequiv e -> is_exec s -> Nb_Steps Move fs == Nb_Steps Move fe.

  Inductive Nb_Steps_eq (P: Exec -> bool) (T: Exec -> Prop):
            nat -> Exec -> Prop :=
  | at_T_eq: forall e, T e -> Nb_Steps_eq P T 0 e
  | add_step1: forall n g e, ~ T (s_cons g e) -> Nb_Steps_eq P T n e ->
                             P (s_cons g e) = true -> Nb_Steps_eq P T (S n) (s_cons g e)
  | add_step2: forall n g e, ~ T (s_cons g e) -> Nb_Steps_eq P T n e ->
                             P (s_cons g e) = false -> Nb_Steps_eq P T n (s_cons g e).

  Instance Nb_Steps_eq_compat: Proper fequiv Nb_Steps_eq.

  Lemma Nb_Steps_equiv':
    forall P T n e (fe: Finally T e), Nb_Steps_eq P T n e <-> Nb_Steps P fe = n.

  Lemma Nb_Steps_eq_Finally:
    forall P T e n, Forever (fun s : Stream => {T s} + {~ T s}) e ->
                    Proper pequiv e -> Nb_Steps_eq P T n e ->
                    Finally T e.

  Lemma Nb_Steps_eq_le:
    forall P T n e (pe: Proper pequiv e)
           (fdec: Forever (fun s : Stream => {T s} + {~ T s}) e),
      Nb_Steps_le P T n e <->
      exists k, k <= n /\ Nb_Steps_eq P T k e.

  Lemma Nb_Steps_exist:
    forall P T e, Finally T e -> exists n, Nb_Steps_eq P T n e .

  Lemma Nb_Steps_eq_unique:
    forall P T e n1 n2, Nb_Steps_eq P T n1 e -> Nb_Steps_eq P T n2 e -> n1 = n2.

End Tools_For_Composition_Steps.

Section Composition_Steps.

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

  Context (Algo1: Algorithm).

  Notation run1 := (@run Algo1).
  Notation S1 := (@State Algo1).
  Notation Env1 := (@Env Chans Net Algo1).
  Notation Exec1 := (@Exec Chans Net Algo1).

  Variable Assumption1: Stable_Assumption (Algo := Algo1).
  Existing Instance Assumption1.

  Notation RO1 := (ROType (Stable_Assumption := Assumption1)).
  Notation RO1_part := (getRO (Stable_Assumption := Assumption1)).

  Context (Algo2 : Algorithm).

  Notation run2 := (@run Algo2).
  Notation S2 := (@State Algo2).
  Notation Env2 := (@Env Chans Net Algo2).
  Notation Exec2 := (@Exec Chans Net Algo2).

  Variable Assumption2: Stable_Assumption (Algo := Algo2).
  Existing Instance Assumption2.

  Notation RO2 := (ROType (Stable_Assumption := Assumption2)).
  Notation RO2_part := (getRO (Stable_Assumption := Assumption2)).

  Context {CS: Composition_State Algo1 Assumption2}.
  Definition Algo3 := (Collateral_composition (Assumption2 := Assumption2)).
  Notation run3 := (@run Algo3).

  Existing Instance Algo3.

  Notation S3 := (S3 (Assumption2 := Assumption2)).
  Notation Env3 := (@Env Chans Net Algo3).
  Notation Exec3 := (@Exec Chans Net Algo3).

  Notation read1 := (read1 (Assumption2 := Assumption2)).
  Notation write1 := (write1 (Assumption2 := Assumption2)).
  Notation read2 := (read2 (Assumption2 := Assumption2)).
  Notation write2 := (write2 (Assumption2 := Assumption2)).

  Existing Instance read1_compat.
  Existing Instance write1_compat.
  Existing Instance read2_compat.
  Existing Instance write2_compat.

  Notation envread1 := (envread1 (Assumption2 := Assumption2)).
  Notation envread2 := (envread2 (Assumption2 := Assumption2)).
  Notation execread1 := (execread1 (Assumption2 := Assumption2)).
  Notation execread2 := (execread2 (Assumption2 := Assumption2)).

  Notation Assume1 := (Assume (Stable_Assumption := Assumption1)).
  Notation Assume2 := (Assume (Stable_Assumption := Assumption2)).

  Instance Assumption3: Stable_Assumption (Algo := Algo3) :=
    Assumption3 Assumption1 (Assumption2 := Assumption2).

  Notation Assume3 := (Assume (Stable_Assumption := Assumption3)).

  Context (N1: nat).

  Hypothesis steps1:
    Steps_complexity (Algo := Algo1) N1 Term
                     (fun e1 => Assume1 (s_hd e1) /\ is_exec e1).

  Context (N2: nat).

  Hypothesis steps2:
    Steps_complexity (Algo := Algo2) N2 Term is_exec.


  Hypothesis Terminal1_Assume2 :
    forall g3, Proper fequiv g3 -> Assume1 (envread1 g3) ->
               terminal (envread1 g3) -> (Assume2 (envread2 g3)).

  Lemma Assume_31: forall g3, Assume3 g3 = Assume1 (envread1 g3).


  Lemma Has_not_Moved1_same:
    forall g e, is_exec (s_cons g e) ->
                Has_Moved1 (execread1 (s_cons g e)) = false ->
                  envread1 g =~= envread1 (s_hd e).

  Lemma s_hd_read2: forall e3,
      envread2 (s_hd e3) = s_hd (execread2 e3).

  Lemma At_N_steps_3_2:
    forall n e3,
      Assume3 (s_hd e3) -> is_exec e3 ->
      terminal (envread1 (s_hd e3)) ->
      At_N_steps n Term (execread2 e3) -> At_N_steps n Term e3.

  Notation term1 := (fun e3 => terminal (envread1 (s_hd e3))).
  Notation hasmoved1 := (fun e3 => Has_Moved1 (execread1 e3)).
  Notation Nb_steps1 := (@Nb_Steps _ _ _ hasmoved1 term1).
  Notation Nb_steps1_le := (@Nb_Steps_le _ _ _ hasmoved1 term1).

  Lemma term1_wd: Weak_Dec pequiv term1.

  Lemma term1_compat: Proper pequiv term1.

  Lemma Always_term1:
    forall e (ise: is_exec e),
      Always
        (fun ee =>
           match ee with
           | s_one _ => True
           | s_cons g e1 =>
             hasmoved1 (s_cons g e1) = false -> term1 e1 -> term1 (s_cons g e1)
           end) e.

  Lemma Nb_steps1_cons:
    forall n g e, is_exec (s_cons g e) ->
                  Nb_steps1_le n (s_cons g e) -> Nb_steps1_le n e.

  Lemma finally_term:
    forall e3: Exec3, Assume3 (s_hd e3) -> is_exec e3 -> Finally Term e3.

  Lemma finally_term1:
    forall e3, Assume3 (s_hd e3) -> is_exec e3 -> Finally term1 e3.

  CoFixpoint build_proj2_sync (e3: Exec3): Exec2 :=
    match e3 with
    | s_one g3 => s_one (envread2 g3)
    | s_cons g3 e3' =>
      if Has_Moved1 (execread1 e3) then sync_exec (envread2 g3)
      else s_cons (envread2 g3) (build_proj2_sync e3')
    end.

  Lemma build_proj2_sync_unfold:
    forall e3, build_proj2_sync e3 =
               match e3 with
               | s_one g3 => s_one (envread2 g3)
               | s_cons g3 e3' =>
                 if Has_Moved1 (execread1 e3) then
                   sync_exec (envread2 g3)
                 else s_cons (envread2 g3) (build_proj2_sync e3')
              end.

  Instance build_proj2_sync_compat:
    Proper fequiv build_proj2_sync.

  Lemma build_proj2_sync_hd:
    forall e3, s_hd (build_proj2_sync e3) = envread2 (s_hd e3).

  Lemma build_proj2_sync_is_exec:
    forall e3, is_exec e3 -> is_exec (build_proj2_sync e3).

  Lemma enabled_31:
    forall g3 n,
      Proper pequiv g3 ->
      terminal (envread2 g3) ->
      enabled_b g3 n = true ->
      enabled_b (envread1 g3) n = true.

  Lemma has_moved_31:
    forall g3' g3 n,
      Step g3' g3 ->
      terminal (envread2 g3) ->
      has_moved_b g3' g3 n = true ->
      has_moved_b (envread1 g3') (envread1 g3) n = true.

  Lemma Step_1_2:
    forall g e , Proper pequiv (s_cons g e) ->
                 Step (s_hd e) g -> terminal (envread2 g) ->
                 hasmoved1 (s_cons g e) = true.


  Lemma proj2_sync_steps:
    forall e3 n,
      is_exec e3 -> ~ term1 e3 ->
      At_N_steps n Term (build_proj2_sync e3) ->
      exists n', n' <= n /\
                 At_N_steps
                   n'
                   (fun ee3 => Has_Moved1 (execread1 ee3) = true)
                   e3.

  Lemma constant_term1:
    forall e3 g1,
      Assume3 (s_hd e3) -> is_exec e3 ->
      is_constant g1 (execread1 e3) -> terminal g1.

  Lemma execread1_finite:
    forall e, finiteT e -> finiteT (execread1 e).

  Lemma At_N_steps_0:
    forall P (e: Exec1), At_N_steps 0 P e -> P e.

  Lemma At_SN_steps_one:
    forall P n (g: Env1), At_N_steps (S n) P (s_one g) -> False.

  Lemma At_SN_steps_cons:
    forall P n (g: Env1) e, At_N_steps (S n) P (s_cons g e) ->
                            At_N_steps n P e.

  Lemma At_N_steps_Finally:
    forall N P (e: Exec1), At_N_steps N P e -> Finally P e.

  Lemma bounded_step1:
    forall e, Assume3 (s_hd e) -> is_exec e -> Nb_steps1_le N1 e.

  Lemma big_step:
    forall k e3, Assume3 (s_hd e3) -> is_exec e3 ->
                 Nb_steps1_le (S k) e3 ->
                 exists n, n <= S N2 /\
                           At_N_steps n (Nb_steps1_le k) e3.

  Theorem Collateral_step_complexity:
    Steps_complexity (Algo := Algo3) (N1 * (S N2) + N2)
                     Term (fun e3 => Assume3 (s_hd e3) /\ is_exec e3).


End Composition_Steps.

Close Scope signature_scope.
Close Scope nat_scope.