Library Prelude

Require Import HahnBase.
Require Import List.
Require Import ListSet.
Require Import Permutation.
Require Import PermutationTactic.
Require Import Setoid.
Require Import ZArith.

Import ListNotations.

Set Implicit Arguments.

Domains

Module Type Domains.

Syntactic and semantic domains used in the formalisation:

  Parameter Act : Type.
  Parameter ProcVar : Type.
  Parameter Var : Type.
  Parameter Val : Type.

Operations and relations used in the formalisation:

Parameter val_op : Val -> Val -> Val.
Parameter val_unit : Val.

Decidable equality:

  Parameter procvar_eq_dec : forall x y: ProcVar, { x = y } + { x <> y }.
  Parameter val_eq_dec : forall x y: Val, { x = y } + { x <> y }.
  Parameter var_eq_dec : forall x y: Var, { x = y } + { x <> y }.

  Lemma procvars_eq_dec :
    forall xs ys: list ProcVar, { xs = ys } + { xs <> ys }.

  Lemma vals_eq_dec :
    forall x y: list Val, { x = y } + { x <> y }.

Infinite domains

Parameter val_inf : forall xs: list Val, exists v: Val, ~ In v xs.

End Domains.

Preliminaries

Lemma ex_iff :
  forall A p q (EQ: forall x : A, p x <-> q x),
  (exists x, p x) <-> (exists x, q x).

Lemma all_iff :
  forall A p q (EQ: forall x : A, p x <-> q x),
  (forall x, p x) <-> (forall x, q x).

Lemma option_not_none {T} :
  forall x : option T,
  ~ x = None <-> exists v, x = Some v.

Functions

The following section provides an update function for arbitrary functions f : A -> B for which members of A have decidable equality.

Section Update.
  Hypothesis A : Type.
  Hypothesis B : Type.
  Hypothesis eq_dec : forall x y: A, { x = y } + { x <> y }.

  Definition update (f : A -> B)(x : A)(v : B) : A -> B :=
    fun y: A => if eq_dec x y then v else f y.

  Lemma update_apply :
    forall f x v, update f x v x = v.

  Lemma update_eq_dep :
    forall f g x v,
    update f x v = update g x v ->
    forall y, x <> y -> f y = g y.

  Lemma update_idle :
    forall f x, f = update f x (f x).

  Lemma update_idle2 :
    forall f x v, f x = v -> update f x v = f.

  Lemma update_comm :
    forall f x1 v1 x2 v2,
    x1 <> x2 ->
    update (update f x1 v1) x2 v2 =
    update (update f x2 v2) x1 v1.

  Lemma update_redundant :
    forall f x v v',
    update (update f x v) x v' = (update f x v').

  Fixpoint updates (f : A -> B)(xs : list A)(vs : list B) : A -> B :=
    match xs, vs with
      | x :: xs', v :: vs' => update (updates f xs' vs') x v
      | _, _ => f
    end.

  Lemma updates_empty :
    forall f, updates f [] [] = f.
End Update.

Lists

Definition disjoint A (X Y : A -> Prop) :=
  forall x, X x -> Y x -> False.

Definition disjoint_list A (xl yl : list A) :=
  forall x (IN1 : In x xl) (IN2 : In x yl), False.

Definition pred_of_list A (l : list A) (x : A) := In x l.

Coercion pred_of_list : list >-> Funclass.

Lemma disjoint_conv :
  forall A (l1 l2 : list A),
  disjoint l1 l2 -> disjoint_list l1 l2.

Auxiliary results and lemmas on lists.

Fixpoint list_zip {A B} (xs : list A) (ys : list B) : list (A * B) :=
  match (xs, ys) with
    | (x::xs', y::ys') => (x, y) :: list_zip xs' ys'
    | _ => nil
  end.

Fixpoint list_zipped {A B} (xs : list A) (ys : list B) (zs : list (A * B)) : Prop :=
  match (xs, ys, zs) with
    | (x::xs', y::ys', (z1, z2)::zs') => x = z1 /\ y = z2 /\ list_zipped xs' ys' zs'
    | (nil, nil, nil) => True
    | _ => False
  end.

Fixpoint list_disj {A} (xs ys : list A) : Prop :=
  match xs with
    | nil => True
    | x::xs' => ~ In x ys /\ list_disj xs' ys
  end.

Lemma in_app {T} :
  forall (xs ys : list T)(x : T),
  In x xs -> In x (xs ++ ys).

Lemma list_member_not_split {T} :
  forall (x : T)(xs1 xs2 : list T),
  ~ In x (xs1 ++ xs2) ->
  ~ In x xs1 /\ ~ In x xs2.

Lemma remove_In_neq {T} (eq_dec : forall x y : T, { x = y } + { x <> y }) :
  forall xs x y,
  x <> y ->
  In x xs <-> In x (remove eq_dec y xs).

Lemma map_eq_In {T U} :
  forall (xs : list T)(x : T)(f1 f2 : T -> U),
  In x xs ->
  map f1 xs = map f2 xs ->
  f1 x = f2 x.

List partitioning

Properties of the partition operation that are not in the standard library.

Lemma partition_permut {T} :
  forall (xs ys1 ys2 : list T)(f : T -> bool),
  partition f xs = (ys1, ys2) ->
  Permutation xs (ys1 ++ ys2).

Lemma partition_f_left {T} :
  forall (xs ys1 ys2 : list T)(f : T -> bool),
  partition f xs = (ys1, ys2) ->
  forall x : T, In x ys1 -> f x = true.

Lemma partition_f_right {T} :
  forall (xs ys1 ys2 : list T)(f : T -> bool),
  partition f xs = (ys1, ys2) ->
  forall x : T, In x ys2 -> f x = false.

Lemma partition_exists {T} :
  forall (xs : list T)(f : T -> bool),
  exists ys, partition f xs = ys.

Lemma partition_res {T} :
  forall (xs : list T)(f : T -> bool),
  partition f xs = (fst (partition f xs), snd (partition f xs)).

Lists of natural numbers

Open Scope nat_scope.

Fixpoint list_nat_max (xs : list nat) : nat :=
  match xs with
    | nil => 0
    | x :: xs' => max x (list_nat_max xs')
  end.

Lemma list_nat_max_app :
  forall xs x,
  list_nat_max (x :: xs) = max x (list_nat_max xs).

Lemma list_nat_max_tail :
  forall xs x,
  list_nat_max xs <= list_nat_max (x :: xs).

Lemma list_nat_max_le_app :
  forall xs x,
  x <= list_nat_max (x :: xs).

Lemma list_nat_max_In :
  forall xs x,
  In x xs -> x <= list_nat_max xs.

Lemma list_nat_max_In_neg :
  forall xs,
  ~ In ((list_nat_max xs) + 1) xs.

Given any list of natural numbers, one can always find a natural number that is not in this list.

Lemma list_nat_max_notin :
forall xs : list nat,
exists x : nat, ~ In x xs.

Close Scope nat_scope.

Lists of integers

Open Scope Z_scope.

Fixpoint list_Z_max (xs : list Z) : Z :=
  match xs with
    | nil => 0
    | x :: xs' => Z.max x (list_Z_max xs')
  end.

Lemma list_Z_max_app :
  forall xs x,
  list_Z_max (x :: xs) = Z.max x (list_Z_max xs).

Lemma list_Z_max_tail :
  forall xs x,
  list_Z_max xs <= list_Z_max (x :: xs).

Lemma list_Z_max_le_app :
  forall xs x,
  x <= list_Z_max (x :: xs).

Lemma list_Z_max_In :
  forall xs x,
  In x xs -> x <= list_Z_max xs.

Lemma list_Z_max_In_neg :
  forall xs,
  ~ In ((list_Z_max xs) + 1) xs.

Given any (finite) list of integers, one can always find an integer that is not in this list.

Lemma list_Z_max_notin :
forall xs : list Z,
exists x : Z, ~ In x xs.

Close Scope Z_scope.

List removal

The removeFirst operation removes only the first occurrence of a given element x in a given list xs.

Section ListRemoval.

Variable T : Type.
Hypothesis eq_dec : forall x y : T, { x = y } + { x <> y }.

Fixpoint removeFirst (x : T)(xs : list T) : list T :=
  match xs with
    | [] => []
    | y :: xs' => if eq_dec x y then xs' else y :: removeFirst x xs'
  end.

Lemma Permutation_moveleft :
  forall (xs : list T)(x : T),
  In x xs -> Permutation xs (x :: removeFirst x xs).

End ListRemoval.

Permutations

Different results on permutations on certain substructures and operations on lists.

Lemma map_permut {T U} :
  forall (xs ys : list T)(f : T -> U),
  Permutation xs ys ->
  Permutation (map f xs) (map f ys).

Add Parametric Morphism {T U} : (@map T U)
  with signature eq ==> @Permutation T ==> @Permutation U
    as map_permut_mor.

Finite sets

Auxiliary results

Some results that are not present in the ListSet library.

Lemma set_In_permutation {T}:
  forall (xs ys : set T)(e : T),
  Permutation xs ys -> set_In e xs -> set_In e ys.

Add Parametric Morphism {T} : (@set_In T)
  with signature eq ==> (@Permutation T) ==> iff
    as set_In_permut_mor.

Lemma set_remove_permutation {T} (eq_dec : forall x y : T, { x = y } + { x <> y }) :
  forall (xs ys : set T)(e : T),
  Permutation xs ys ->
  Permutation (set_remove eq_dec e xs) (set_remove eq_dec e ys).

Hint Resolve set_remove_permutation : core.

Add Parametric Morphism {T} : (@set_remove T)
  with signature eq ==> eq ==> (@Permutation T) ==> (@Permutation T)
    as set_remove_permut_mor.

Lemma set_In_remove {T} (eq_dec : forall x y : T, { x = y } + { x <> y }) :
  forall xs x y,
  x <> y -> set_In x (set_remove eq_dec y xs) <-> set_In x xs.

Lemma set_remove_swap {T} (eq_dec : forall x y : T, { x = y } + { x <> y }):
  forall xs x y,
  set_remove eq_dec x (set_remove eq_dec y xs) =
  set_remove eq_dec y (set_remove eq_dec x xs).

Lemma set_remove_cons {T} (eq_dec : forall x y : T, { x = y } + { x <> y }) :
  forall (xs : set T)(x y : T),
  x <> y -> y :: set_remove eq_dec x xs = set_remove eq_dec x (y :: xs).

Subset

Definition subset {T} (X Y : set T) : Prop :=
  forall e : T, set_In e X -> set_In e Y.

Global Instance subset_refl {T} :
  Reflexive (@subset T).

Hint Resolve subset_refl : core.

Global Instance subset_trans {T} :
  Transitive (@subset T).

Section Subset.

Variable T : Type.
Hypothesis eq_dec : forall x y : T, { x = y } + { x <> y }.

Lemma subset_add :
  forall (e : T)(X : set T),
  subset [e] (set_add eq_dec e X).

Lemma subset_add_mono :
  forall (e : T)(X : set T),
  subset X (set_add eq_dec e X).

Lemma subset_union_mono_l :
  forall (X Y : set T),
  subset X (set_union eq_dec X Y).

Lemma subset_union_mono_r :
  forall (X Y : set T),
  subset X (set_union eq_dec Y X).

Lemma subset_union_l :
  forall (X1 X2 Y : set T),
  subset X1 X2 -> subset (set_union eq_dec X1 Y) (set_union eq_dec X2 Y).

Lemma subset_union_r :
  forall (X Y1 Y2 : set T),
  subset Y1 Y2 -> subset (set_union eq_dec X Y1) (set_union eq_dec X Y2).

End Subset.

Add Parametric Morphism {T} (eq_dec : forall x y : T, { x = y } + { x <> y }) : (set_union eq_dec)
  with signature (@subset T) ==> (@subset T) ==> (@subset T)
    as set_union_subset_mor.

Sublists

A slightly different definition than subset; here elements are allowed to occur multiple times in the specified lists.

TODO: prove antisymmetry.

Section Sublist.

Variable T : Type.
Hypothesis eq_dec : forall x y : T, { x = y } + { x <> y }.

Fixpoint sublist (xs ys : set T) : Prop :=
  match xs with
    | nil => True
    | x :: xs' => set_In x ys /\ sublist xs' (set_remove eq_dec x ys)
  end.

Lemma sublist_In :
  forall (xs ys : set T)(x : T),
  sublist xs ys -> set_In x xs -> set_In x ys.

Lemma sublist_cons :
  forall (xs ys : set T)(x : T),
  sublist xs (x :: ys) <-> sublist (set_remove eq_dec x xs) ys.

Lemma sublist_nil :
  forall xs : set T,
  sublist xs nil -> xs = nil.

Lemma sublist_remove_In :
  forall (ys xs : set T)(x : T),
  set_In x ys ->
  sublist xs (set_remove eq_dec x ys) <-> sublist (x :: xs) ys.

Lemma sublist_remove :
  forall (xs ys : set T)(x : T),
  sublist xs ys -> sublist (set_remove eq_dec x xs) (set_remove eq_dec x ys).

Global Instance sublist_refl :
  Reflexive sublist.

Hint Resolve sublist_refl : core.

Global Instance sublist_trans :
  Transitive sublist.

Lemma sublist_permutation_r :
  forall xs ys1 ys2 : set T,
  Permutation ys1 ys2 -> sublist xs ys1 -> sublist xs ys2.

Lemma sublist_permutation_l :
  forall xs1 xs2 : set T,
  Permutation xs1 xs2 ->
  forall ys, sublist xs1 ys -> sublist xs2 ys.

Add Parametric Morphism : sublist
  with signature (@Permutation T) ==> (@Permutation T) ==> iff
    as sublist_permut_mor.

Lemma sublist_permutation :
  forall xs ys,
  Permutation xs ys -> sublist xs ys.

Hint Resolve sublist_permutation : core.

End Sublist.

Finite maps

A list of pairs is a finite map if there are no duplicates among the left elements

Definition fmap_dom {T U} (xs : list (T * U)) : list T :=
  fst (split xs).

Definition fmap {T U} (xs : list (T * U)) : Prop :=
  NoDup (fmap_dom xs).

Lemma fmap_dom_cons {T U} :
  forall (xs : list (T * U))(x : T * U),
  fmap_dom (x :: xs) = fst x :: fmap_dom xs.

Lemma fmap_dom_In {T U} :
  forall (xs : list (T * U))(x : T * U),
  In x xs -> In (fst x) (fmap_dom xs).

The following definition determines whether a list of pairs is projected onto a given mapping.

Definition projected {T U} (xs : list (T * U))(f : T -> U) : Prop :=
forall x : T * U, In x xs -> f (fst x) = snd x.