Library Padec.MessagePassing.Fair_convergence

From Coq Require Import Arith.
From Coq Require Import List.
From Coq Require Import Relations.
From Coq Require Import Wellfounded.
From Coq Require Import Setoid.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Basics.
From Coq Require Import RelationPairs.
From Coq Require Import Lia.

From Padec Require Import SetoidUtil.
From Padec Require Import ListUtils.
From Padec Require Import WellfoundedUtil.
From Coq Require Import Streams.

Open Scope signature_scope.
Set Implicit Arguments.

  CoInductive eqStreamA A (eqA:relation A) (s1 s2: Stream A):Prop :=
    eqCons:
      eqA (hd s1) (hd s2) ->
      eqStreamA eqA (tl s1) (tl s2) ->
      eqStreamA eqA s1 s2.

  Global Instance eqStreamA_refl: forall A (eqA:relation A),
      Reflexive eqA -> Reflexive (eqStreamA eqA).

  Global Instance eqStreamA_sym: forall A (eqA:relation A),
      Symmetric eqA -> Symmetric (eqStreamA eqA).

  Global Instance eqStreamA_trans: forall A (eqA:relation A),
      Transitive eqA -> Transitive (eqStreamA eqA).

  Global Instance hd_compat A (eqA:relation A): Proper (eqStreamA eqA ==> eqA) (hd (A:=A)).

  Global Instance tl_compat A (eqA:relation A):
    Proper (eqStreamA eqA ==> eqStreamA eqA) (tl (A:=A)).

  Global Instance eqStreamA_per A (eqA:relation A) (eqA_per: PER eqA):
      PER (eqStreamA eqA).

  Global Instance eqStreamA_equiv A (eqA:relation A) (eqA_equiv: Equivalence eqA):
      Equivalence (eqStreamA eqA).

  Global Instance Stream_Setoid A (SA:Setoid A): Setoid (Stream A) :=
    {| equiv := eqStreamA equiv |}.

  Global Instance Stream_PartialSetoid A (PSA:PartialSetoid A): PartialSetoid (Stream A) :=
    {| pequiv := eqStreamA pequiv |}.

  Global Instance ForAll_compat A (eqA:relation A) :
    Proper ((eqStreamA eqA ==> iff) ==> (eqStreamA eqA ==> iff)) (ForAll (A:=A)).

  Global Instance Exists_compat A (eqA:relation A) :
    Proper ((eqStreamA eqA ==> iff) ==> (eqStreamA eqA ==> iff)) (Exists (A:=A)).

  Section Fair_convergence.

  Variables (A B:Type).
  Variable (PSA: PartialSetoid A) (SB:Setoid B).
  Variable (ltB:relation B).
  Hypothesis ltB_compat: Proper fequiv ltB.
  Hypothesis wf_ltB: well_founded ltB.
  Variable pot:A -> B.
  Hypothesis pot_compat: Proper fequiv pot.

  Definition R_step R (s:Stream A) :Prop := R (hd s) (hd (tl s)).
  Global Instance R_step_compat: Proper fequiv R_step.

  Definition pot_decreases (sa:Stream A) :=
    ForAll (fun s => R_step (flip ltB @@ pot) s \/ R_step (equiv @@ pot) s) sa.

  Definition pot_fairly_decreases_until P (sa:Stream A) :=
    ForAll (fun s => P s \/ Exists (R_step (flip ltB @@ pot)) s) sa.

  Definition is_suffix (sa ssa:Stream A) := Exists (pequiv ssa) sa.

  Lemma is_suffix_tl: forall sa ssa, is_suffix sa ssa -> is_suffix sa (tl ssa).

  Lemma is_suffix_ForAll: forall P sa ssa, Proper pequiv P ->
      is_suffix sa ssa -> ForAll P sa -> ForAll P ssa.

  Theorem fair_convergence:
    forall P (P_compat:Proper fequiv P) sa, Proper pequiv sa -> pot_decreases sa ->
                 pot_fairly_decreases_until P sa -> Exists P sa.

End Fair_convergence.