Library Padec.Model.Composition_Round_inductive_def

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Bool.
From Coq Require Import PeanoNat.
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 Exec.
From Padec Require Import ZUtils.
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 Rounds_inductive_def.
From Padec Require Import Rounds_Slices.


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

Section Composition_Round.

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

  Context (Algo1: Algorithm).

  Notation run1 := (@run Algo1).
  Notation S1 := (@State Algo1).
  Notation Env1 := (@Env 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).

  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 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)).

  Context (N1: nat).


  Hypothesis Algo1_round_complexity:
    Round_complexity (Algo:=Algo1)
                     (fun e => Assume1 (s_hd e) /\
                               is_exec e /\
                               weakly_fair e) (fun e =>terminal (s_hd e)) N1.

  Context (N2: nat).

  Hypothesis Algo2_round_complexity:
    Round_complexity (Algo:=Algo2)
                     (fun e => Assume2 (s_hd e) /\
                               is_exec e /\
                               weakly_fair e) (fun e =>terminal (s_hd e)) N2.

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

  Lemma rounds_proj_algo1:
    forall e (ise: is_exec e),
      let P1 := fun e => terminal (envread1 (s_hd e)) in
      let P1' := fun e => terminal (s_hd e) in
      forall N (hN: At_N_rounds N P1' (execread1 e)),
      exists N', N' <= N /\ At_N_rounds N' P1 e.


  Lemma rounds_proj_algo2:
    forall e (pe : Proper pequiv e),
      terminal (envread1 (s_hd e)) ->
      is_exec e ->
      let P2 := fun e => terminal (Algo:=Algo3) (s_hd e) in
      let P2' := fun e => terminal (Algo:=Algo2) (s_hd e) in
      forall N (hN:At_N_rounds N P2' (execread2 e)),
        At_N_rounds N P2 e.

Lemma sim_progress_P_1:
  forall (P: Exec (Algo:= Algo1) -> Prop),
    Simulation_monotonic P ->
    Simulation_monotonic (progress_P P).

Axiom sim_progress_P_2:
  forall Algo_ (P: Exec (Algo:= Algo_) -> Prop),
    Simulation_monotonic P ->
    Simulation_comonotonic (progress_P P).


  Theorem Collateral_round_complexity:
    Round_complexity (Algo:=Algo3)
                     (fun e => Assume1 (envread1 (s_hd e)) /\
                               is_exec e /\
                               weakly_fair e) (fun e =>terminal (s_hd e)) (N1+N2).

End Composition_Round.

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