PADEC - Coq Library

Library Padec.Tools.Relational_Stream

A Framework for Certified Self-Stabilization
PADEC Coq Library

Nov 2016

From Coq Require Import Setoid.
From Coq Require Import SetoidList.
From Coq Require Import Morphisms.
From Coq Require Import RelationClasses.
From Coq Require Import SetoidClass.
From Coq Require Import RelationPairs.

From Padec Require Import SetoidUtil.
From Padec Require Import Stream.

Open Scope signature_scope.
Set Implicit Arguments.

Section Relational_Stream.

  Context {A: Type} `{SA: PartialSetoid A}.

  Notation continue_R R :=
    (fun s => match s with | s_one _ => False
                      | s_cons a s => R (s_hd s) a end).
  Notation stop_P P :=
    (fun s => match s with | s_one a => P a | s_cons _ _ => False end).

  Definition Relational_Stream (R: relation A) (P: A -> Prop): Stream -> Prop :=
    WUntil (continue_R R) (stop_P P).

  Lemma Relational_Stream_inv_1:
    forall R P a s, Relational_Stream R P (s_cons a s) -> R (s_hd s) a.

  Lemma Relational_Stream_inv_2:
    forall R P a s, Relational_Stream R P (s_cons a s) -> Relational_Stream R P s.

  Lemma Relational_Stream_inv_0:
    forall R P a, Relational_Stream R P (s_one a) -> P a.

  Lemma Always_Relational_Stream:
    forall R P a, Relational_Stream R P a -> Always (fun s => Relational_Stream R P s) a.

The restriction of a relation on its right member to a property P

Definition Restriction (R: relation A) (P: A -> Prop) := (fun x y => R x y /\ P y).

The restriction of R to P is included in R

  Lemma subrelation_Restriction: forall R P, subrelation (Restriction R P) R.

  Global Instance Relational_Stream_compat:
    Proper (fequiv ==> fequiv ==> pequiv ==> impl) Relational_Stream.

  Global Instance Relational_Stream_compat_iff: Proper fequiv Relational_Stream.

If R preserves P and the first element of a stream respects P then it is the same thing to be a stream carrying information about R and be a stream carrying information about the restriction of R.

  Lemma Restriction_intro: forall (R: relation A)(Z P: A -> Prop),
      (forall x y, P x -> R y x -> P y ) ->
      forall e, P (s_hd e) ->
                Relational_Stream R Z e <->
                Relational_Stream (Restriction R P) Z e.

Eventually when the implication is conditionned on a third property P stable by R.

  Lemma Eventually_impl2: forall (R: relation A) (Z: A -> Prop) (P: A -> Prop) (B C: Stream -> Prop),
      (forall x y, P x -> R y x -> P y ) ->
      (forall e, P (s_hd e) -> B e -> C e ) ->
      forall e, P (s_hd e) ->
                Relational_Stream R Z e ->
                Eventually B e ->
                Eventually C e.

Let R be a relation and P,Q,Z three properties on A. if

P is preserved by R
for all stream e that are relational Streams, P x implies Eventually Q

then forall all stream carrying information about R such that the first element respects P eventually Q.

  Lemma Eventually_forall_always_enventually:
    forall (R:relation A) (Z P:A ->Prop) (Q:Stream ->Prop),
      (forall x y,P x -> R y x ->P y )->
      (forall e, P (s_hd e)-> Relational_Stream R Z e ->Eventually Q e )->
      forall e, Relational_Stream R Z e ->
                P (s_hd e) -> Always (Eventually Q ) e.

  Lemma Relational_Acc_Eventually:
    forall (R:relation A) (Z:A -> Prop) (Q:Stream ->Prop),
      (forall e, Z (s_hd e) -> Q e ) ->
      forall e, Relational_Stream R Z e -> Acc R (s_hd e) -> Eventually Q e.

  Section Weak_Prefix.

    Section Weak_Prefix_with_dep.
      Variable (Safe: Stream (A := A) -> Prop)
               (P: Stream (A := A) -> Prop).
      Hypothesis (P_dec: forall s, Safe s -> {P s }+{~P s }).

      CoFixpoint weak_prefix_until_P s (asa: Always Safe s) :=
        match s as ns return Always Safe ns -> Stream with
        | s_one a => fun _ => s_one a
        | s_cons a s' => fun asa' =>
                           if P_dec (Always_P_P asa) then s_one a
                           else s_cons a (weak_prefix_until_P
                                            (Always_inv_2 asa'))
        end asa.

      Lemma weak_prefix_until_P_decompose:
        forall s asa,
          weak_prefix_until_P asa =
          match s as ns return Always Safe ns -> Stream with
          | s_one a => fun _ => s_one a
          | s_cons a s' => fun asa' =>
                             if P_dec (Always_P_P asa) then s_one a
                             else s_cons a (weak_prefix_until_P
                                              (Always_inv_2 asa'))
          end asa.

      Lemma weak_prefix_until_P_hd: forall s (asa: Always Safe s),
          s_hd (weak_prefix_until_P asa) = (s_hd s ).

    End Weak_Prefix_with_dep.

    Lemma finite_weak_prefix:
      forall (P Safe: Stream -> Prop)
             (P_dec: forall s, Safe s -> {P s } + {~P s })
             (Q: A -> Prop) (incl: forall s, Q (s_hd s) -> P s)
             (s: Stream) (asa: Always Safe s),
        Always (fun e => match e with
                    s_one g => Q g | s_cons _ _ => True end) s ->
        finite (weak_prefix_until_P _ P_dec asa) ->
        Eventually (fun suf => P suf) s.

  End Weak_Prefix.

Finite Relational Stream:

definitions with Acc and well_founded

  Section Finite_Relational_Stream.

    Variable (R: relation A) (P: A -> Prop).
    Notation RP := (fun a b => ~P b /\ R a b).

    Lemma Acc_finite_rel_stream:
      forall init,
        Acc RP init ->
        (forall s, init = s_hd s ->
                   Always (fun s => match s with
                                      s_one a => P a
                                    | s_cons a s => RP (s_hd s) a end) s
                   -> finite s ).

    Lemma wf_finite_rel_stream:
      well_founded RP ->
      (forall s,
          Always (fun s => match s with
                             s_one a => P a
                           | s_cons a s => RP (s_hd s) a end) s
          -> finite s ).

  End Finite_Relational_Stream.

  Lemma rel_stream_preserved:
    forall R P s,
      Relational_Stream R P s ->
      forall Safe Q Q_dec (asa: Always Safe s),
        Relational_Stream (fun a b => ~Q b /\ R a b)
                          (fun a => P a \/ Q a)
                          (weak_prefix_until_P (fun s => Q (s_hd s)) Q_dec asa).

End Relational_Stream.

Unset Implicit Arguments.
Close Scope signature_scope.