Module CommonPS

From Coq Require Import FSets.FMapPositive.
From Coq Require Import FSets.FMapFacts.
From Coq Require Import List.
Import ListNotations.
From Coq Require Import Sorting.Permutation.

From Coq Require Import Setoid.
From Coq Require Import Relations RelationPairs.
From Coq Require Import Morphisms.

From Coq Require MSets.MSets.
From Coq Require Export PArith.
From Coq Require Import Classes.EquivDec.

From Velus Require Import ClockDefs.
From Velus Require Import Common.CommonTactics.
From Velus Require Import Common.CommonList.

These modules are used to manipulate identifiers.

Module PS := Coq.MSets.MSetPositive.PositiveSet.
Module PSP := MSetProperties.WPropertiesOn Pos PS.
Module PSF := MSetFacts.Facts PS.
Module PSE := MSetEqProperties.WEqPropertiesOn Pos PS.
Module PSdec := Coq.MSets.MSetDecide.WDecide PS.

Definition ident_eq_dec := Pos.eq_dec.
Definition ident_eqb := Pos.eqb.

Instance: EqDec ident eq := { equiv_dec := ident_eq_dec }.

Implicit Type i j: ident.

Properties

Definition not_In_empty: forall x : ident, ~(PS.In x PS.empty) := PS.empty_spec.

Ltac not_In_empty :=
match goal with H:PS.In _ PS.empty |- _ => now apply not_In_empty in H end.

Lemma not_not_in:
forall x A, ~~PS.In x A <-> PS.In x A.

Proof.

Lemma PS_not_inter:
forall s t x,
~PS.In x (PS.inter s t) <-> ~PS.In x s \/ ~PS.In x t.

Proof.

Lemma PS_union_diff_same:
forall s t,
PS.Equal (PS.union (PS.diff s t) t) (PS.union s t).

Proof.

Lemma PS_not_union:
forall s t x,
~PS.In x (PS.union s t) <-> ~PS.In x s /\ ~PS.In x t.

Proof.

Lemma PS_not_diff:
forall s t x,
~PS.In x (PS.diff s t) <-> ~PS.In x s \/ PS.In x (PS.inter s t).

Proof.

Lemma PS_disjoint1:
  forall s1 s2,
    PS.Empty (PS.inter s1 s2) ->
    forall x, PS.In x s1 -> ~PS.In x s2.

Proof.

Lemma PS_disjoint2:
  forall s1 s2,
    PS.Empty (PS.inter s1 s2) ->
    forall x, PS.In x s2 -> ~PS.In x s1.

Proof.

Lemma PS_diff_inter_same:
  forall A B C,
    PS.Equal (PS.diff (PS.inter A C) (PS.inter B C))
             (PS.inter (PS.diff A B) C).

Proof.

Lemma PS_inter_union_dist:
  forall A B C D,
    PS.Equal (PS.inter (PS.union A B) (PS.union C D))
             (PS.union (PS.inter A C)
                       (PS.union (PS.inter A D)
                                 (PS.union (PS.inter B C)
                                           (PS.inter B D)))).

Proof.

Lemma PS_inter_inter_same:
  forall A B C,
    PS.Equal (PS.inter (PS.inter A C) (PS.inter B C))
             (PS.inter (PS.inter A B) C).

Proof.

Lemma PS_For_all_Forall:
forall P s,
PS.For_all P s <-> Forall P (PS.elements s).

Proof.

Lemma PS_not_in_diff:
  forall x s t,
    ~PS.In x t ->
    ~PS.In x (PS.diff s t) ->
    ~PS.In x s.

Proof.

Lemma PS_For_all_empty:
forall P,
PS.For_all P PS.empty.

Proof.

Lemma PS_In_Forall:
  forall P S,
    PS.For_all P S ->
    forall x, PS.In x S -> P x.

Proof.

Lemma PS_For_all_sub:
  forall P S T,
    PS.For_all P S ->
    (forall x, PS.In x T -> PS.In x S) ->
    PS.For_all P T.

Proof.

Lemma PS_For_all_diff:
  forall P S T,
    PS.For_all P S ->
    PS.For_all P (PS.diff S T).

Proof.

Lemma PS_For_all_inter:
  forall P S T,
    PS.For_all P S ->
    PS.For_all P (PS.inter S T).

Proof.

Lemma PS_For_all_union:
  forall P S T,
    PS.For_all P S ->
    PS.For_all P T ->
    PS.For_all P (PS.union S T).

Proof.

Lemma PS_For_all_impl_In:
  forall (P Q : PS.elt -> Prop) S,
    PS.For_all P S ->
    (forall x, PS.In x S -> P x -> Q x) ->
    PS.For_all Q S.

Proof.

Instance PS_For_all_Equals_Proper:
Proper (pointwise_relation positive iff ==> PS.Equal ==> iff) PS.For_all.

Proof.

Lemma PS_For_all_add:
forall P a S,
PS.For_all P (PS.add a S) <-> (P a /\ PS.For_all P S).

Proof.

Lemma In_PS_elements:
forall x s,
In x (PS.elements s) <-> PS.In x s.

Proof.

Lemma Permutation_elements_add:
  forall xs x s,
    Permutation (PS.elements s) xs ->
    ~PS.In x s ->
    Permutation (PS.elements (PS.add x s)) (x::xs).

Proof.

Add Morphism PS.elements
with signature PS.Equal ==> @Permutation positive
as PS_elements_Equal.

Proof.

Lemma Permutation_PS_elements_of_list:
  forall xs,
    NoDup xs ->
    Permutation (PS.elements (PSP.of_list xs)) xs.

Proof.

Lemma PS_elements_NoDup: forall s,
NoDup (PS.elements s).

Proof.

Definition ps_adds (xs: list positive) (s: PS.t) :=
  fold_left (fun s x => PS.add x s) xs s.

Definition ps_from_list (l: list positive) : PS.t :=
  ps_adds l PS.empty.

Lemma ps_adds_spec:
  forall s xs y,
    PS.In y (ps_adds xs s) <-> In y xs \/ PS.In y s.

Proof.

Instance eq_equiv : Equivalence PS.eq.

Proof.

Instance ps_adds_Proper (xs: list ident) :
Proper (PS.eq ==> PS.eq) (ps_adds xs).

Proof.

Lemma add_ps_from_list_cons:
  forall xs x,
    PS.eq (PS.add x (ps_from_list xs))
          (ps_from_list (x :: xs)).

Proof.

Lemma ps_add_eq : forall x1 x2 s,
PS.eq (PS.add x1 (PS.add x2 s)) (PS.add x2 (PS.add x1 s)).

Proof.

Lemma ps_add_adds_eq : forall xs x s,
PS.eq (PS.add x (ps_adds xs s)) (ps_adds xs (PS.add x s)).

Proof.

Lemma ps_adds_app: forall xs1 xs2 s,
PS.eq (ps_adds (xs1 ++ xs2) s)
(ps_adds xs1 (ps_adds xs2 s)).

Proof.

Lemma ps_from_list_In:
forall xs x,
PS.In x (ps_from_list xs) <-> In x xs.

Proof.

Instance ps_from_list_Permutation:
Proper (@Permutation.Permutation ident ==> fun xs xs' => forall x, PS.In x xs -> PS.In x xs')
ps_from_list.

Proof.

Instance ps_from_list_Proper:
Proper (@Permutation ident ==> PS.Equal) ps_from_list.

Proof.

Lemma ps_adds_In:
  forall x xs s,
    PS.In x (ps_adds xs s) ->
    ~PS.In x s ->
    In x xs.

Proof.

Lemma Permutation_PS_elements_ps_adds:
  forall xs S,
    NoDup xs ->
    Forall (fun x => ~PS.In x S) xs ->
    Permutation (PS.elements (ps_adds xs S)) (xs ++ PS.elements S).

Proof.

Lemma Permutation_PS_elements_ps_adds':
  forall xs S,
    NoDup (xs ++ PS.elements S) ->
    Permutation (PS.elements (ps_adds xs S)) (xs ++ PS.elements S).

Proof.

Lemma Subset_ps_adds:
  forall xs S S',
    PS.Subset S S' ->
    PS.Subset (ps_adds xs S) (ps_adds xs S').

Proof.

Definition ps_removes (xs: list positive) (s: PS.t)
:= fold_left (fun s x => PS.remove x s) xs s.

Lemma ps_removes_spec: forall s xs y,
PS.In y (ps_removes xs s) <-> ~In y xs /\ PS.In y s.

Proof.

Lemma ps_removes_app : forall xs1 xs2 s,
ps_removes (xs1 ++ xs2) s = ps_removes xs2 (ps_removes xs1 s).

Proof.

Lemma PS_For_all_ps_adds:
forall P xs S,
PS.For_all P (ps_adds xs S) <-> (Forall P xs /\ PS.For_all P S).

Proof.

Corollary PS_For_all_Forall': forall P xs,
PS.For_all P (ps_from_list xs) <-> (Forall P xs).

Proof.

Lemma ps_adds_of_list:
forall xs,
PS.Equal (ps_adds xs PS.empty) (PSP.of_list xs).

Proof.

Corollary ps_from_list_ps_of_list : forall xs,
PS.eq (ps_from_list xs) (PSP.of_list xs).

Proof.

Corollary ps_of_list_In : forall xs x,
PS.In x (PSP.of_list xs) <-> In x xs.

Proof.

Lemma ps_of_list_ps_to_list : forall id xs,
In id (PSP.to_list (PSP.of_list xs)) <-> In id xs.

Proof.

Lemma ps_of_list_ps_to_list_Perm : forall xs,
NoDup xs ->
Permutation (PSP.to_list (PSP.of_list xs)) xs.

Proof.

Inductive DisjointSetList : list PS.t -> Prop :=
| DJSnil: DisjointSetList []
| DJScons: forall s ss,
    DisjointSetList ss ->
    Forall (fun t => PS.Empty (PS.inter s t)) ss ->
    DisjointSetList (s :: ss).

Instance DisjointSetList_Proper:
  Proper (@Permutation.Permutation PS.t ==> iff) DisjointSetList.

Proof.

Definition PSUnion (xs : list PS.t) : PS.t :=
  List.fold_left PS.union xs PS.empty.

Instance fold_left_PS_Proper:
  Proper ((PS.Equal ==> PS.Equal ==> PS.Equal) ==> eq ==> PS.Equal ==> PS.Equal)
         (@fold_left PS.t PS.t).

Proof.

Instance PSUnion_Proper:
Proper (@Permutation.Permutation PS.t ==> PS.Equal) PSUnion.

Proof.

Instance PSUnion_eqlistA_Proper:
Proper (SetoidList.eqlistA PS.Equal ==> PS.Equal) PSUnion.

Proof.

Lemma PSUnion_cons:
forall T TS, (PSUnion (T :: TS)) === (PS.union T (PSUnion TS)).

Proof.

Lemma Subset_PSUnion_cons:
forall T TS, PS.Subset T (PSUnion (T :: TS)).

Proof.

Lemma In_PSUnion:
  forall T TS,
    In T TS ->
    PS.Subset T (PSUnion TS).

Proof.

Lemma PS_union_empty1:
forall s, PS.union PS.empty s === s.

Proof.

Lemma PS_union_empty2:
forall s, PS.union s PS.empty === s.

Proof.

Lemma PSUnion_cons_empty:
forall xs, PSUnion (PS.empty :: xs) === PSUnion xs.

Proof.

Lemma PSUnion_nil:
PSUnion nil = PS.empty.

Proof.

Lemma PSUnion_app:
forall xs ys,
PSUnion (PSUnion xs :: ys) === PSUnion (xs ++ ys).

Proof.

Lemma PSUnion_In_app:
forall x xs ys,
PS.In x (PSUnion (xs ++ ys)) <-> PS.In x (PSUnion xs) \/ PS.In x (PSUnion ys).

Proof.

Lemma In_In_PSUnion:
  forall x s ss,
    PS.In x s ->
    In s ss ->
    PS.In x (PSUnion ss).

Proof.

Lemma PSUnion_In_In:
  forall x ss,
    PS.In x (PSUnion ss) ->
    exists s, In s ss /\ PS.In x s.

Proof.

Definition In_ps (xs : list positive) (v : PS.t) :=
Forall (fun x => PS.In x v) xs.

Lemma In_ps_nil:
forall v, In_ps [] v.

Proof.

Lemma In_ps_singleton:
forall x v,
PS.In x v <-> In_ps [x] v.

Proof.

Lemma PS_In_In_mem_mem:
forall x m n,
PS.In x m <-> PS.In x n <-> PS.mem x m = PS.mem x n.

Proof.

Sets and maps of identifiers as efficient list lookups

Section Ps_From_Fo_List.

  Context {A : Type} (f: A -> option ident).

  Definition ps_from_fo_list' (xs: list A) (s: PS.t) : PS.t :=
    fold_left (fun s x=> match f x with
                      | None => s
                      | Some i => PS.add i s
                      end) xs s.

  Definition ps_from_fo_list (xs: list A) : PS.t :=
    ps_from_fo_list' xs PS.empty.

  Lemma In_ps_from_fo_list':
    forall x xs s,
      PS.In x (ps_from_fo_list' xs s) ->
      PS.In x s \/ In (Some x) (map f xs).

Proof.

End Ps_From_Fo_List.