PADEC - Coq Library

Library Padec.Tools.Simulation

A Framework for Certified Self-Stabilization
PADEC Coq Library

Nov 2016

Global Imports

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 Coq Require Import Arith.

Local Imports

From Padec Require Import OptionUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import WellfoundedUtil.
From Padec Require Import RelationA.
From Padec Require Import Stream.

Open Scope signature_scope.
Set Implicit Arguments.

Simulation and Squeezing

Squeezing is an operator on streams that removes any consecutive duplicated elements. It may remove finite numbers of duplicates. It also removes an infinite number of duplicates provided that they are at the end of the stream.

Squeezable establishes a condition under which Squeezing is actually computable.

Simulation defines an order on streams: X <= Y when X contains less consecutive duplicates thatn Y.

For a stream X, (Squeeze X) is the minimum stream among the streams Y such that Y <= X.

Section Simulation_Squeezing.

Simulation and Squeeze are defined assuming a partial setoid A Equality relation on A is assumed to be weakly decidable

Context {A: Type} `{SA: PartialSetoid A}.
Context `{pequiv_dec: Weak_Dec_relation pequiv (A:=A)}.

Squeezable: defines a condition under which a stream can be squeezed

Nb: this condition should be in Type, to achieve constructive arguments that can be used to actually build the operator Squeeze as a CoFixpoint.

Rskip

Relation on stream: (Rskip a s1 s2) means

either the two streams are reduced to one element and equal; or
add element a to s1 to obtain s2

  Definition Rskip (a: A): relation Stream :=
    (fun s1 s2 => Proper pequiv s2 ->
                  s_cons a s1 =~= s2 \/
                  s1 =~= s_one a /\ s_one a =~= s2).

  Global Instance Rskip_compat: Proper fequiv Rskip.

  Global Instance Rskip_compat_right: forall a s, Proper fequiv (Rskip a s).

  Lemma Rskip_hd :
    forall a s1 s2, Rskip a s1 s2 -> Proper pequiv s2 -> a =~= s_hd s2.

  Lemma Rskip_cons :
    forall a b x y,
      a =~= b -> x =~=y -> Rskip a x (s_cons b y).

  Lemma Rskip_left_unique:
    forall a s1 s2 s, Proper pequiv s -> Rskip a s1 s -> Rskip a s2 s ->
                      s1 =~= s2.

  Lemma Rskip_cons_4_Skip (a: A) (pa: Proper pequiv a) (x: A)
        (ss: Stream)
        (EQ: Proper pequiv a -> Proper pequiv x -> pequiv a x):
    Rskip a ss (s_cons x ss).

Skippable

Type on Stream: Skippable a s means that it can be decided is

whether s in constantly made of the element a, or
s begins with a finite number of elements, followed then by an element which is different from a.

  Definition Skippable (a: A) (s: Stream): Type :=
    {is_constant a s }+{Acc (Rskip a) s }.

  Lemma Acc_Rskip_if_not_a:
    forall a s, Proper pequiv s -> ~ (a =~= s_hd s ) -> Acc (Rskip a) s.

  Lemma Skippable_if_not_a:
    forall a s, Proper pequiv s -> ~ (a =~= s_hd s ) -> Skippable a s.

  Lemma is_constant_not_Acc:
    forall s a, is_constant a s -> ~Acc (Rskip a) s.

  Lemma Acc_not_is_constant:
    forall s a, Acc (Rskip a) s -> ~is_constant a s.

  Lemma Acc_Rskip_cons:
    forall a s, Acc (Rskip a) (s_cons a s) -> Acc (Rskip a) s.

  Instance Acc_Rskip_compat: Proper fequiv (fun a => Acc (Rskip a)).

  Lemma Skippable_if_move:
    forall a s s0, ~ (a =~= s_hd s0 ) -> s_cons a s0 =~= s ->
                   Skippable a s.

  Lemma Skippable_if_move':
    forall a (pa: Proper pequiv a)
           s (ps: Proper pequiv s),
      ~ (a =~= s_hd s ) -> Skippable a (s_cons a s).

  Lemma Skippable_compat:
    forall a b (eab: a =~= b)
           x y (exy: x =~= y),
      Skippable a x -> Skippable b y.

Squeezable

Type on Stream: Squeezable s means that the stream is forever skippable, namely all along the stream, it is skippable using its head element.

  Definition Squeezable (s: Stream): Type :=
    Forever (fun s => Skippable (s_hd s) s) s.

  Lemma Squeezable_inv (s: Stream) (w: Squeezable s): Skippable (s_hd s) s.

  Lemma Squeezable_inv_cons (a: A) (s: Stream) (w: Squeezable (s_cons a s)):
    Squeezable s.

  Lemma Squeezable_one (a: A): Proper pequiv a -> Squeezable (s_one a).

  Lemma Squeezable_compat:
    forall x y (exy: x =~= y), Squeezable x -> Squeezable y.

  Lemma Squeezable_cons:
    forall (a : A) (s : Stream)
           (pa:Proper pequiv a) (ps:Proper pequiv s),
      Squeezable s -> Squeezable (s_cons a s).

  Lemma is_constant_Squeezable:
    forall a s, is_constant a s -> Squeezable s.

Skip

Operator that removes a finite prefix of a stream: Skip a s returns the suffix of the stream s from which every element a has been removed at the beginning. It requires Acc (Rskip a) s to be able to perform induction.

  Fixpoint Skip (a: A) (pa: Proper pequiv a)
           (s: Stream) (W: Acc (Rskip a) s): Stream :=
    match s as es return Acc (Rskip a) es -> Stream with
    | s_one x => fun _ => s_one x
    | s_cons x ss =>
      fun w =>
        match (pequiv_dec a x) with
        | left EQ => Skip pa (Acc_inv w _ (Rskip_cons_4_Skip a pa EQ ))
        | right _ => s_cons x ss
        end end W.

  Global Instance Skip_compat:
    forall a (pa: Proper pequiv a)
           (s: Stream) (ps: Proper pequiv s)
           (W: Acc (Rskip a) s),
      Proper pequiv (Skip pa W).

  Lemma Skip_compat':
    forall (a: A) (pa: Proper pequiv a)
           (b: A) (pb: Proper pequiv b)
           (x y: Stream)
           (Wax: Acc (Rskip a) x) (Wby: Acc (Rskip b) y),
      a =~= b -> x =~= y -> Skip pa Wax =~= Skip pb Wby.

  Lemma Skip_hd:
    forall a (pa: Proper pequiv a) s (W: Acc (Rskip a) s),
      ~ (a =~= s_hd (Skip pa W)).

  Lemma Skip_suffix:
    forall (a: A) (pa: Proper pequiv a)
           (s: Stream) (ps: Proper pequiv s)
           (W: Acc (Rskip a) s),
      is_suffix s (Skip pa W).

  Lemma Skip_cons:
    forall (a: A) (pa: Proper pequiv a) (s: Stream)
           (W: Acc (Rskip a) (s_cons a s)) (W': Acc (Rskip a) s),
      Proper pequiv s -> Skip pa W =~= Skip pa W'.

A squeezable stream from which has been removed its finite prefix of duplicates (Skip) is still squeezable

  Lemma Squeezable_Skip:
    forall a (pa:Proper pequiv a)
           (s: Stream)
           (SQ: Squeezable s)
           (W : Acc (Rskip a) s),
      Squeezable (Skip pa W).

Squeeze

Operator that removes every consecutive duplicates from the stream, included at its (potentially infinite) suffix. It requires the stream to be squeezable.

Precisely, (Skip (s_hd s) s) if it exists implies that s can be written as s = a^+.s' with a = (s_hd s) and s' a non-empty stream. Then, (Skip (s_hd s) s) returns s'.

If (is_constant s), (Squeeze s) returns (s_one (s_hd s))
Otherwise: + s is not (s_one _) and s can be written as a^+.s' with s' a non-empty stream and ~(pequiv a (s_hd s')) + (Squeeze a^+.s') returns a.(Squeeze s')

Precisely, (Skip a a^+.s') returns s' and (Squeeze a^+.s') returns a.(Squeeze (Skip a a^+.s'))

Note that (Skip a a^+.s') is itself Squeezable from Lemma Squeezable_Skip.

  CoFixpoint Squeeze (s: Stream) (p: Proper pequiv s) (CC: Squeezable s):
    Stream :=
    match s as op return Proper pequiv op -> Squeezable op -> Stream with
    | s_one x => fun _ _ => s_one x
    | s_cons x ss => fun ps cc =>
                       match Squeezable_inv cc with
                       | left _ =>
                         s_one x
                       | right hW =>
                         s_cons x (Squeeze
                                     (Skip_compat (hd_compat ps) ps hW)
                                     (Squeezable_Skip (hd_compat ps) cc hW))
                       end end p CC.

  Lemma Squeeze_unfold:
    forall s p (CC: Squeezable s),
      Squeeze p CC =
      match s as op return Proper pequiv op -> Squeezable op -> Stream with
      | s_one x => fun _ _ => s_one x
      | s_cons x ss => fun ps cc =>
                         match Squeezable_inv cc with
                         | left _ =>
                           s_one x
                         | right hW =>
                           s_cons x (Squeeze
                                       (Skip_compat (hd_compat ps) ps hW)
                                       (Squeezable_Skip (hd_compat ps) cc hW))
                         end end p CC.

  Lemma Squeeze_compat:
    forall x (px: Proper pequiv x) (cx: Squeezable x)
           y (py: Proper pequiv y) (cy: Squeezable y),
      x =~= y -> Squeeze px cx =~= Squeeze py cy.

  Lemma Squeeze_hd: forall (s: Stream) (p: Proper pequiv s) (CC: Squeezable s),
      s_hd (Squeeze p CC) = s_hd s.

  Lemma Squeeze_one: forall (a: A) (s: Stream)
                            (p: Proper pequiv s) (CC: Squeezable s),
      s_one a =~= Squeeze p CC -> is_constant a s.

cons_plus

Predicate, (cons_plus a s) means that s = a^+.s', namely s begins with a finite positive number of a.

  Inductive cons_plus (a: A): Stream -> Stream -> Prop :=
  | cons_plus_one: forall b s1 s2, a =~= b -> s1 =~= s2 ->
                                   cons_plus a s1 (s_cons b s2)
  | cons_plus_add: forall b s1 s2, a =~= b -> cons_plus a s1 s2 ->
                                   cons_plus a s1 (s_cons b s2).

  Lemma cons_plus_hd: forall a s1 s2, cons_plus a s1 s2 -> a =~= s_hd s2.

  Lemma cons_plus_Proper_1:
    forall a s1 s2, cons_plus a s1 s2 -> Proper pequiv a.

  Lemma cons_plus_Proper_2:
    forall a s1 s2, cons_plus a s1 s2 -> Proper pequiv s1.

  Lemma cons_plus_Proper_3:
    forall a s1 s2, cons_plus a s1 s2 -> Proper pequiv s2.

Simulation

Relation on streams, Simulation X Y means that X contains less consecutive duplicates than Y. The number of duplicates removed between X and Y may be infinite provided that there were at the end of Y (Y has an infinite suffix of duplicates). It is finite in any other case.

Simulation has 2 constructors:

Simulation (s_one a) s is obtained when s is constantly made of a
Simulation (s_cons a s1) s3 is obtained when + s1 is itself smaller than a stream s2 such that + s3 is equal to s2 at the beginning of which a finite number of a has been added.

We also provide an alternative definition which is less difficult to read (one more constructor) but easier to use.

  CoInductive Simulation_alt: Stream -> Stream -> Prop :=
  | simalt_constant: forall a b s, a =~= b ->
                                   is_constant b s ->
                                   Simulation_alt (s_one a) s
  | simalt_cons: forall a b s1 s2 s3, a =~= b ->
                                      Simulation_alt s1 s2 ->
                                      cons_plus b s2 s3 ->
                                      Simulation_alt (s_cons a s1) s3.

is_cons_star

Predicate, (is_cons_star a s) means that s = a^*.s', namely s begins with a finite number (may be 0) of a.

  Inductive is_cons_star (a: A): Stream -> Stream -> Prop :=
  | cons_star_no: forall s1 s2, s1 =~= s2 -> is_cons_star a s1 s2
  | cons_star_add: forall b s1 s2, a =~= b -> is_cons_star a s1 s2 ->
                                   is_cons_star a s1 (s_cons b s2).

  Global Instance is_cons_star_compat: Proper fequiv is_cons_star.

  Lemma is_cons_star_Proper_r: forall a x y,
      is_cons_star a x y -> Proper pequiv y.

  Lemma is_cons_star_Proper_l: forall a x y,
      is_cons_star a x y -> Proper pequiv x.

  Lemma is_cons_star_Skip:
    forall (a: A) (pa: Proper pequiv a) (s: Stream) (W: Acc (Rskip a) s),
      Proper pequiv s -> is_cons_star a (Skip pa W) s.

  Lemma Skip_is_cons_star:
    forall a pa s ss ws,
      is_cons_star a ss s -> ~ a =~= s_hd ss ->
      Skip (a:=a) pa (s:=s) ws =~= ss.
    Arguments Skip : clear implicits.
    Arguments Skip: default implicits.

  Lemma is_cons_star_suffix:
    forall a s1 s2, is_cons_star a s1 s2 -> is_suffix s2 s1.

  Lemma cons_star_suffix_bis:
    forall a s suf, Proper pequiv a -> Proper pequiv s ->
                    is_suffix s suf -> is_cons_star a suf s ->
                    is_suffix (s_cons a s) (s_cons a suf).

  Lemma is_cons_star_cons: forall a x sx,
      is_cons_star a (s_cons a sx) x -> is_cons_star a sx x.

  Lemma is_cons_star_trans:
    forall a, Proper pequiv a ->
              forall x y z, is_cons_star a x y ->
                            is_cons_star a y z ->
                            is_cons_star a x z.

  Lemma cons_star_plus:
    forall a b s1 s2, a =~= b ->
                      (is_cons_star a s1 s2 <-> cons_plus a s1 (s_cons b s2)).

  Lemma is_cons_star_epsilon:
    forall x s s',
      is_cons_star x s s' -> ~(x =~= s_hd s') -> s =~= s'.

  Lemma star_constant:
    forall b s, is_cons_star b (s_one b) s -> is_constant b s.

  Lemma is_cons_star_is_constant:
    forall a x y,
      is_constant a x -> is_cons_star a x y -> is_constant a y.

  Lemma is_cons_star_is_constant':
    forall a x y,
      is_constant a x -> is_cons_star a y x -> is_constant a y.

Simulation: alternative definition (the one used in the proof)

  CoInductive Simulation: Stream -> Stream -> Prop :=
  | sim_one_one: forall a b, a =~= b ->
                             Simulation (s_one a) (s_one b)
  | sim_one_cons: forall a b s, a =~= b -> is_constant a s ->
                                Simulation (s_one a) (s_cons b s)
  | sim_cons: forall a b s1 s2 s3, a =~= b ->
                                   Simulation s1 s2 ->
                                   is_cons_star a s2 s3 ->
                                   Simulation (s_cons a s1) (s_cons b s3).

  Lemma Simulation_hd: forall x y, Simulation x y -> s_hd x =~= s_hd y.

  Global Instance Simulation_Proper_l:
    forall x y, Simulation x y -> Proper pequiv x.

  Global Instance Simulation_Proper_r:
    forall x y, Simulation x y -> Proper pequiv y.

  Global Instance Simulation_compat: Proper fequiv Simulation.

Both definition of Simulation are indeed equivalent

  Lemma Simulation_alt_equiv:
    forall s1 s2, Simulation s1 s2 <-> Simulation_alt s1 s2.

  Lemma Simulation_inv_one:
    forall a x, Simulation (s_one a) x -> is_constant a x.

  Lemma Simulation_inv_cons_one:
    forall a x b, ~ Simulation (s_cons a x) (s_one b).

  Lemma Simulation_inv_cons: forall a x b y,
      Simulation (s_cons a x) (s_cons b y) ->
      Simulation x y \/Simulation (s_cons a x) y.
  Lemma Simulation_inv_cons_star: forall a x b y,
      Simulation (s_cons a x) (s_cons b y) ->
      exists _y , Simulation x _y /\ is_cons_star a _y y.

  Lemma is_constant_Simulation:
    forall a y, is_constant a y -> Simulation (s_one a) y.

  Lemma Simulation_remove_hd:
    forall x y a,
      a =~= s_hd x -> Simulation (s_cons a x) y -> Simulation x y.

  Lemma Simulation_add_hd:
    forall x y a, s_hd x =~= a ->
                  Simulation x y -> Simulation x (s_cons a y).

  Lemma Simulation_is_constant:
    forall a x y, is_constant a x -> Simulation x y -> is_constant a y.

  Lemma Simulation_is_constant':
    forall a x y, is_constant a y -> Simulation x y -> is_constant a x.

Simulation is an order, i.e. a reflexive, transitive and

antisymmetric relation. Nb: Reflexivity is obtained only for compatible streams.

  Lemma Simulation_refl: forall x, Proper pequiv x -> Simulation x x.

  Lemma Simulation_antisym:
    forall x y, Simulation x y -> Simulation y x -> x =~= y.

  Lemma Simulation_trans:
    forall x y z,
      Simulation x y -> Simulation y z -> Simulation x z.

Monotony / Comonotony

Monotony and comonotony is a tool to define preservation of some property which is preserved between a stream and a smaller (greater) one wrt Simulation.

  Definition Simulation_monotonic (P: Stream -> Prop) :=
    forall X Y, Simulation X Y -> P Y -> P X.

  Definition Simulation_comonotonic (P: Stream -> Prop) :=
    forall X Y, Simulation X Y -> P X -> P Y.

Instant: for a property that applies on the first element of the

stream only

  Definition Instant (P: Stream -> Prop) :=
    forall x y, (s_hd x ) =~= (s_hd y ) -> P x <-> P y.

  Lemma Instant_Proper:
    forall P, Instant P -> Proper fequiv P.

  Theorem Instant_Simulation_monotonic:
    forall P, Instant P -> Simulation_monotonic P.

  Theorem Instant_Simulation_comonotonic:
    forall P, Instant P -> Simulation_comonotonic P.

Stepwise: for a property that applies

on the single element of the stream or
on the two first elements, in which case, they should be different

  Definition Stepwise (P: Stream -> Prop): Prop :=
    (forall a b, a =~= b -> P (s_one a) <-> P (s_one b)) /\
    (forall a x, P (s_cons a x) -> ~ (a =~= s_hd x )) /\
    (forall a b x y, a =~=b -> s_hd x =~= s_hd y ->
                     P (s_cons a x) <-> P (s_cons b y)).
  Lemma Stepwise_Proper:
    forall P, Stepwise P -> Proper fequiv P.

  Theorem Stepwise_Simulation_monotonic:
    forall P, Stepwise P -> Simulation_monotonic P.

  Lemma Stepwise_moves: Stepwise moves.

  Lemma Stepwise_strict_moves: Stepwise strict_moves.

  Theorem Stepwise_Always_Simulation_monotonic:
    forall P, Stepwise P -> (forall a, Proper pequiv a -> P (s_one a)) ->
              Simulation_monotonic (Always (fun e => moves e -> P e)).

Simulation preserves moves

  Definition two_fst_eq (s s': Stream): Prop :=
    match s with
      s_one _ => False
    | s_cons a ss =>
      match s' with s_one _ => False
               | s_cons a' ss' =>
                 a =~= a' /\ s_hd ss =~= s_hd ss' end end.

  Lemma Simulation_preserves_move:
    forall s suf,
      is_suffix s suf -> strict_moves suf ->
      forall sim, Simulation sim s ->
                  exists suf_sim , is_suffix sim suf_sim /\
                                  two_fst_eq suf suf_sim.

(Squeeze s) is smallest than s

  Lemma Simulation_Squeeze:
    forall (s: Stream) (p: Proper pequiv s) (w: Squeezable s),
      Simulation (Squeeze p w) s.

  Lemma Simulation_Skip :
    forall a x b y
           (pa:Proper pequiv a) (pb:Proper pequiv b)
           (haccx: Acc (Rskip a) x) (haccy: Acc (Rskip b) y),
      Simulation (s_cons a x) (s_cons b y) ->
      Simulation (Skip pa haccx) (Skip pb haccy).
    Arguments Skip : clear implicits.
    Arguments Skip: default implicits.

(Squeeze s) is the minimum stream among the ones smaller than s

  Lemma Simulation_Squeeze_min:
    forall (s: Stream) (p:Proper pequiv s) (c: Squeezable s) x,
      Simulation x s -> Simulation (Squeeze p c) x.

(Squeeze s) contains no duplicate

  Lemma Squeeze_no_repeat:
    forall (s: Stream) (p: Proper pequiv s) (w: Squeezable s),
      Always moves (Squeeze p w).

End Simulation_Squeezing.

Unset Implicit Arguments.
Close Scope signature_scope.