RIS.tools: Toolbox of simple definitions, lemmas and tactics.

Require Export Eqdep Setoid Morphisms Psatz List.
Require Import Bool.
Export ListNotations.
Set Implicit Arguments.
Infix " ∘ " := Basics.compose (at level 40).
Hint Unfold Basics.compose.
Notation " $ o " := (proj1_sig o) (at level 0).

Notations for equivalence relations and partial orders

Typeclass and notation for axiomatic equivalence relations.

Class Equiv (A : Set) := equiv : relation A.
Notation " e ≡ f " := (equiv e f) (at level 80).

Typeclass and notation for semantic equivalence relations.

Class SemEquiv (A : Type) := sequiv : relation A.
Notation " e ≃ f " := (sequiv e f) (at level 80).

Typeclass and notation for axiomatic preorder relations.

Class Smaller (A : Set) := smaller : relation A.
Notation " e ≤ f " := (smaller e f) (at level 80).

Typeclass and notation for semantic preorder relations.

Class SemSmaller (A : Type) := ssmaller : relation A.
Notation " e ≲ f " := (ssmaller e f) (at level 80).

Decidable sets

The class of decidable_set X contains a binary function associating to every pair of elements of type X a boolean and a proof that this function encodes faithfully equality over X.

Class decidable_set X :=
  { eqX : X → X → bool;
    eqX_eq : ∀ x y, reflect (x = y) (eqX x y)}.

Infix " =?= " := eqX (at level 20).

Section decidable.
  Context { X : Set }.
  Context { D : decidable_set X }.

This lemma is the preferred way of translating back and forth between boolean and propositional equality.

Lemma eqX_correct : ∀ x y : X, eqX x y = true ↔ x = y.

The next few lemmas are useful on occasion.

  Lemma eqX_false : ∀ x y, eqX x y = false ↔ x ≠ y.

  Lemma X_dec (x y : X) : {x = y } + {x ≠ y }.

  Lemma eqX_refl x : eqX x x = true.

End decidable.

The set of natural numbers is decidable.

Global Instance NatNum : decidable_set nat :=
Build_decidable_set PeanoNat.Nat.eqb_spec.

The set of natural booleans is decidable.

Global Instance Boolean : decidable_set bool.

If A and B are decidable, then so is their Cartesian product.

Global Instance dec_prod A B :
decidable_set A → decidable_set B → decidable_set (A ×B).

If A and B are decidable, then so is their sum.

Global Instance dec_sum A B :
decidable_set A → decidable_set B → decidable_set (A +B).

If A is decidable, then so is option A.

Global Instance dec_option (A : Set) :
decidable_set A → decidable_set (option A).

Binary relations

Section relations.
Context {A : Set}.

We define semantic (in)equality for binary relations in the usual way.

  Global Instance eqRel : SemEquiv (relation A) :=
    (fun r s ⇒ ∀ x y, r x y ↔ s x y).

  Global Instance infRel : SemSmaller (relation A) :=
    (fun r s ⇒ ∀ x y, r x y → s x y).

Semantic equality is an equivalence relation, inequality is a partial order.

  Global Instance eqRel_Equivalence : Equivalence (@sequiv _ eqRel).

  Global Instance infRel_PreOrder : PreOrder (@ssmaller _ infRel).

  Global Instance infRel_PartialOrder : PartialOrder sequiv (@ssmaller _ infRel).

The product of two relations is their sequential composition.

  Definition product (r s : relation A) : relation A :=
    fun x y ⇒ ∃ z, r x z ∧ s z y.

  Infix " ⨾ " := product (at level 40).

Δ is the identity relation, also called diagonal.

Definition Δ : relation A := fun x y ⇒ x = y.

≃ (reps. ≲) is a congruence (resp pre-congruence) with respect to ⨾.

Global Instance product_eqRel : Proper (sequiv ==>sequiv ==>sequiv) product.

Global Instance product_infRel : Proper (ssmaller ==>ssmaller ==>ssmaller) product.

Relations equipped with ⨾ and Δ form a monoid.

  Lemma product_assoc (r s t : relation A) : (r ⨾ s )⨾ t ≃ r ⨾ (s ⨾ t ).

  Lemma product_Δ (r : relation A) : r ⨾ Δ ≃ r.
  Lemma Δ_product (r : relation A) : Δ ⨾ r ≃ r.

Let X be a set.

Context {X : Set}.

Any map σ : X → relation A may be uniquely extended into a monoid homomorphism mapRel σ from list X to relation A.

  Definition mapRel (σ : X → relation A) (u : list X) :=
    fold_right (fun l r ⇒ σ l ⨾ r) Δ u.

  Lemma mapRel_nil σ : mapRel σ [] = Δ.

  Lemma mapRel_app σ (u v : list X) : mapRel σ (u ++v) ≃ mapRel σ u ⨾ mapRel σ v.

  Lemma mapRel_unique σ h :
    (∀ a, h [a ] ≃ σ a ) → (h [] ≃ Δ ) → (∀ u v, h (u ++v) = h u ⨾ h v ) →
    ∀ u, h u ≃ mapRel σ u.

  Remark mapRel_add σ u a : mapRel σ (u ++[a ]) ≃ mapRel σ u ⨾ σ a.

End relations.
Infix " ⨾ " := product (at level 40).

Lists

Notations

We associate the traditional containment symbol to list inclusion.

Infix " ⊆ " := incl (at level 80).

We use the following symbol to denote the membership predicate.

Infix " ∈ " := In (at level 60).

We'll write P :> l for the list l where we've removed elements that do not satisfy the boolean predicate P.

Infix " :> " := filter (at level 50).

The length of the list l is denoted by ⎢l⎥.

Notation "⎢ l ⎥" := (length l).

Induction principles

Induction principle for lists in the reverse order.

Lemma rev_induction {A} (P : list A → Prop) :
P [] → (∀ a l, P l → P (l ++[a ])) → ∀ l, P l.

Strong induction on the length of a list.

Lemma len_induction {A} (P : list A → Prop) :
P [] → (∀ a l, (∀ m, ⎢m ⎥ ≤ ⎢l ⎥ → P m ) → P (a ::l)) → ∀ l, P l.

Strong induction on the length of a list, taken in the reverse order.

Lemma len_rev_induction {A} (P : list A → Prop) :
P [] → (∀ a l, (∀ m, ⎢m ⎥ ≤ ⎢l ⎥ → P m ) → P (l ++[a ])) → ∀ l, P l.

General lemmas

A list is not empty if and only if it has a last element.

Lemma not_nil_add {A} (v : list A) : v ≠ [] ↔ ∃ u l, v = u ++[l ].

A list is either empty or can be decomposed with its last element apparent.

Lemma nil_or_last {A} (v : list A) : {v = []} + {∃ a v', v = v'++[a ]}.

If the list l++a::l' is duplicate free, so are l and l'.

Lemma NoDup_remove_3 {A} (l l' : list A) (a : A) :
NoDup (l ++ a :: l') → NoDup l ∧ NoDup l'.

Filtering a concatenation is the same as concatenating filters.

Lemma filter_app {A} (f : A → bool) (l m : list A) :
f :> (l ++m ) = f :> l ++ f :> m.

Filtering reduces the length of the list.

Lemma filter_length {A} (f : A → bool) l :
⎢f :> l ⎥ ≤ ⎢l ⎥ .

The following lemma give a more precise description.

Lemma filter_length_eq {A} (f : A → bool) l :
⎢f :> l ⎥ + ⎢(fun x ⇒ negb (f x)) :> l ⎥ = ⎢l ⎥ .

filter and map commute.

Lemma filter_map {A B} (f : A → bool) (g : B → A) l :
f :> (map g l ) = map g ((f ∘g ) :> l).

filter only depends on the values of the filtering function, not its implementation.

Lemma filter_ext_In {A} (f g : A → bool) l :
(∀ x, x ∈ l → f x = g x ) → f :> l = g :> l.

Lemma filter_ext {A} (f g : A → bool) l :
(∀ x, f x = g x ) → f :> l = g :> l.

Filtering with the predicate true does not modify the list.

Lemma filter_true {A} (l : list A) :
(fun _ ⇒ true ) :> l = l.

Filtering preserves the property NoDup (absence of duplicates).

Lemma filter_NoDup {A} (f : A → bool) l :
NoDup l → NoDup (f :> l).

A filtered list P :> l is empty if and only if P x is false for every element x∈l.

Lemma filter_nil {A} (P : A → bool) l :
P :>l = [] ↔ ∀ a, a ∈ l → P a = false.

If two concatenations are equal, and if the two initial factors have the same length, then the factors are equal.

Lemma length_app {A} (l1 l2 m1 m2 : list A) :
⎢l1 ⎥ = ⎢m1 ⎥ → l1 ++l2 = m1 ++m2 → l1 = m1 ∧ l2 = m2.

If two concatenations are equal, and if the two final factors have the same length, then the factors are equal.

Lemma length_app_tail {A} (l1 l2 m1 m2 : list A) :
⎢l2 ⎥ = ⎢m2 ⎥ → l1 ++l2 = m1 ++m2 → l1 = m1 ∧ l2 = m2.

If two concatenations are equal, and the first initial factor is smaller than the second one, we can find a unifying factor w.

Lemma app_eq_app_length {A : Set} (u1 u2 v1 v2 : list A) :
u1 ++u2 = v1 ++ v2 → ⎢u1 ⎥ ≤ ⎢v1 ⎥ → ∃ w, v1 = u1 ++w ∧ u2 = w ++v2.

If two concatenations are equal, we can always find a unifying factor.

Lemma Levi {A:Set} (u1 u2 v1 v2 : list A) :
u1 ++u2 = v1 ++v2 → ∃ w, (u1 =v1 ++w ∧ v2 =w ++u2 ) ∨ (v1 =u1 ++w ∧ u2 =w ++v2 ).

This next lemma makes the unifying factor unambiguous.

Lemma Levi_strict {A:Set} (u1 u2 v1 v2 : list A) :
u1 ++u2 = v1 ++v2 → (u1 = v1 ∧ u2 = v2 )
∨ ∃ a w, (u1 =v1 ++a ::w ∧ v2 =a ::w ++u2 ) ∨ (v1 =u1 ++a ::w ∧ u2 =a ::w ++v2 ).

If the concatenation of two lists is duplication free, then so are they.

Lemma NoDup_app_inv {X:Set} : ∀ (l m : list X),
NoDup (l ++m) → NoDup l ∧ NoDup m.

If l and m don't share any element, then if both of them don't have duplication their concatenation won't either.

Lemma NoDup_app {X : Set} l m:
(∀ a : X, a ∈ l → ¬ a ∈ m ) → NoDup l → NoDup m → NoDup (l ++m).

If the boolean predicate forallb f l is false, then me may extract a counter-example, that is an element in the list l where the predicate f is false.

Lemma forallb_false_exists {A} f (l:list A) :
forallb f l = false ↔ ∃ a, a ∈ l ∧ f a = false.

l appears in the list concat m exactly when there is a list L in m such that l appears in L.

Lemma in_concat {A : Set} l (m : list (list A)) :
l ∈ concat m ↔ ∃ L, L ∈ m ∧ l ∈ L.

If map f m can be split into l1++l2, then we may split l into m1++m2 accordingly.

Lemma map_app_inverse {A B} (f : A → B) m l1 l2 :
map f m = l1 ++ l2 → ∃ m1 m2, l1 = map f m1 ∧ l2 = map f m2 ∧ m = m1 ++ m2.

lift_prod f is the pointwise extension of the binary operation f over A into a binary operation over list A.

Definition lift_prod {A: Set} (f : A → A → A) : list A → list A → list A :=
fun l m ⇒ flat_map (fun a ⇒ map (f a) m) l.

Lemma lift_prod_spec {A:Set} f (l m : list A) :
∀ c, c ∈ lift_prod f l m ↔ ∃ a b, a ∈ l ∧ b ∈ m ∧ c = f a b.

Lemma incl_map {A B:Set} (f : A → B) l m : l ⊆ map f m → ∃ n, l = map f n ∧ n ⊆ m.

Lists of pairs

We introduce some notations for lists of pairs: prj1 l is the list obtained by applying pointwise to l the function fun (x,y) ⇒ x.

Notation prj1 := (map fst).

Similarly, prj2 l is the list obtained by applying pointwise to l the function fun (x,y) ⇒ y.

Notation prj2 := (map snd).

If the a projection of l is equal to a projection of m, then they have the same length.

Lemma proj_length {A B C} (l : list (A ×B)) (m:list (B ×C)) : prj2 l = prj1 m → ⎢l ⎥=⎢m ⎥.

Combine

Section combine.
  Context {A B : Set}.
  Context {l1 l3 : list A} {l2 l4: list B} {l: list (A ×B)}.
  Hypothesis same_length : ⎢l1 ⎥ = ⎢l2 ⎥.

The combine function can be described by the following recursive definition :

[]⊗l = l⊗[] = [];
(a::l)⊗(b::m)=(a,b)::(l⊗m).

In the following, we will only use l⊗m when l and m have the same length.

Infix "⊗" := combine (at level 50).

The first projection of l1 ⊗ l2 is l1.

Lemma combine_fst : prj1 (l1 ⊗ l2) = l1.

The second projection of l1 ⊗ l2 is l2.

Lemma combine_snd : prj2 (l1 ⊗ l2) = l2.

A combination of concatenations is the concatenation of combinations (assuming the first arguments of both concatenations have the same length).

Lemma combine_app : (l1 ++l3 ) ⊗ (l2 ++l4 ) = l1 ⊗ l2 ++ l3 ⊗ l4.

Every list of pairs can be expressed as the combination of its first and second components.

Lemma combine_split : l = (prj1 l ) ⊗ (prj2 l ).

End combine.
Infix "⊗" := combine (at level 50).

Mix

Section mix.
Context {A B : Set} {s1 s2 s3 s4 : list (A ×B)}.
Hypothesis same_length : ⎢s1 ⎥ = ⎢s2 ⎥.

Given two lists of pairs s1 and s2, the mix of s1 and s2 is the combination of the first projection of s1 with the second projection of s2. We will only use this construct when s1 and s2 have the same length.

  Definition mix (s1 s2 : list (A ×B)) := (prj1 s1 ) ⊗ (prj2 s2 ).
  Infix "⋈" := mix (at level 50).

  Lemma mix_fst : prj1 (s1 ⋈ s2) = prj1 s1.

  Lemma mix_snd : prj2 (s1 ⋈ s2) = prj2 s2.

  Lemma mix_app : (s1 ++s3 ) ⋈ (s2 ++s4 ) = s1 ⋈ s2 ++ s3 ⋈ s4.
End mix.
Infix "⋈" := mix (at level 50).

Flip

Section flip.
Context {A B : Set} {l m : list (A ×B)}.

Flipping a list of pairs amounts to applying pointwise to the list the function fun (x,y) ⇒ (y,x), that is exchanging the order of every pair in the list.

Definition flip {A B} : list (A ×B) → list (B ×A) := map (fun x ⇒ (snd x ,fst x )).
Notation " l ` " := (flip l) (at level 20).

Flip is an involution.

Lemma flip_involutive : l `` = l.

Flip distributes over concatenations.

Lemma flip_app : (l ++m )`=l `++m `.

Flip swaps first and second projections.

Lemma flip_proj1 : prj1 (l `) = prj2 l.

Lemma flip_proj2 : prj2 (l `) = prj1 l.

The pair (a,b) is in l if and only if (b,a) is in l`.

Lemma In_flip a b : (a ,b ) ∈ l ` ↔ (b ,a ) ∈ l.

End flip.
Notation " l ` " := (flip l) (at level 30).

Lists as finite sets

We say that two lists are equivalent if they contain the same elements.

Definition equivalent A l m := ∀ x : A , x ∈ l ↔ x ∈ m.
Infix " ≈ " := equivalent (at level 80).

We now establish that ≈ is a congruence, and that ⊆ is a partial order.

Global Instance equivalent_Equivalence T : Equivalence (@equivalent T).
Global Instance incl_PreOrder T : PreOrder (@incl T).
Global Instance incl_PartialOrder T :
PartialOrder (@equivalent T) (@incl T).

Concatenation preserves both relations.

Global Instance incl_app_Proper T :
  Proper ((@incl T ) ==> (@incl T ) ==> (@incl T )) (@app T).
Global Instance equivalent_app_Proper T :
  Proper ((@equivalent T ) ==> (@equivalent T ) ==> (@equivalent T ))
         (@app T).

The operation of adding an element to a list preserves both relations.

Global Instance incl_cons_Proper T a :
Proper ((@incl T ) ==> (@incl T )) (cons a).
Global Instance equivalent_cons_Proper T a :
Proper ((@equivalent T ) ==> (@equivalent T )) (cons a).

For any function f, the list morphism map f preserves both relations.

Global Instance map_incl_Proper {A B} (f : A → B) :
Proper (@incl A ==> @incl B) (map f).
Global Instance map_equivalent_Proper {A B} (f : A → B) :
Proper (@equivalent A ==> @equivalent B) (map f).

For any boolean predicate f, the filtering map filter f preserves both relations.

Global Instance filter_incl_Proper {A} (f : A → bool) :
Proper (@incl A ==> @incl A) (filter f).
Global Instance filter_equivalent_Proper {A} (f : A → bool) :
Proper (@equivalent A ==> @equivalent A) (filter f).

The lemmas In_incl_Proper and In_equivalent_Proper are completely tautological, but turn out to be useful for technical reasons.

Global Instance In_incl_Proper {A} (x : A): Proper ((@incl A ) ==> Basics.impl) (In x).
Global Instance In_equivalent_Proper {A} (x : A): Proper ((@equivalent A ) ==> iff) (In x).

The operation of reversing a list preserves both relations.

Lemma rev_equivalent {A} (l : list A) : l ≈ rev l.
Global Instance incl_rev_Proper T : Proper ((@incl T ) ==> (@incl T )) (@rev T).
Global Instance equivalent_rev_Proper T : Proper ((@equivalent T ) ==> (@equivalent T )) (@rev T).

The flat_map function preserves both relations.

Global Instance incl_flat_map_Proper A B (f : A → list B) :
Proper ((@incl A ) ==> (@incl B )) (flat_map f).
Global Instance equivalent_flat_map_Proper A B (f : A → list B) :
Proper ((@equivalent A ) ==> (@equivalent B )) (flat_map f).

The lift_prod f function preserves both relations.

Global Instance incl_lift_prod_Proper {A:Set} (f : A → A → A) :
Proper ((@incl _) ==> (@incl _) ==> (@incl _)) (lift_prod f).
Global Instance equivalent_lift_prod_Proper {A:Set} (f : A → A → A) :
Proper ((@equivalent _) ==> (@equivalent _) ==> (@equivalent _)) (lift_prod f).

The following simple facts about inclusion and equivalence are convenient to have in our toolbox.

Lemma incl_nil T (A : list T) : [] ⊆ A.
Lemma incl_app_or T (A B C : list T) : A ⊆ B ∨ A ⊆ C → A ⊆B ++C.
Lemma incl_app_split {A} (l m p : list A) : l ++m ⊆ p ↔ l ⊆ p ∧ m ⊆ p.
Hint Resolve incl_appl incl_appr incl_nil app_assoc : eq_list.
Lemma app_idem {A} (l : list A) : l ++ l ≈ l.
Lemma app_comm {A} (l m : list A) : l ++ m ≈ m ++ l.
Lemma incl_split {A} (l m n : list A) :
l ⊆ m ++ n → ∃ l1 l2, l ≈ l1 ++l2 ∧ l1 ⊆ m ∧ l2 ⊆ n.

More general lemmas

If a boolean predicate f fails to be true for every element of a list l, then there must exists a witnessing element y falsifying f. This is an instance of a classical principle holding constructively when restricted to decidable properties over finite domains.

Lemma forall_existsb {A} (f : A → bool) l :
¬ (∀ x, x ∈ l → f x = true ) → ∃ y, y ∈ l ∧ f y = false.

In forallb f l we may replace f with a function g outputting the same values on the elements of l.

Lemma forallb_ext_In {A} (f g : A → bool) l : (∀ a, a ∈ l → f a = g a ) → forallb f l = forallb g l.

In forallb f l we may replace f with a function g outputting the same values.

Lemma forallb_ext {A} (f g : A → bool) l : (∀ a, f a = g a ) → forallb f l = forallb g l.

For every list l and every function f, l is a fixpoint of map f if and only if every element of l is a fixpoint of f.

Lemma map_eq_id {A} (l : list A) (f : A → A) :
map f l = l ↔ (∀ x, x ∈ l → f x = x ).

fun f ⇒ map f l is bijective, using extensional equality of functions.

Lemma map_bij {A B} (f g : A → B) l : map f l = map g l → ∀ a, a ∈ l → f a = g a.

Lemma map_ext_in_iff (A B : Type) (f g : A → B) (l : list A) :
(∀ a : A, a ∈ l → f a = g a ) ↔ map f l = map g l.

Lemma map_eq_equivalent (A B : Set) (f g : A → B) l m :
l ≈ m → map f m = map g m ↔ map f l = map g l.

We may lift a decomposition of the second (respectively first) component of a list of pairs into a decomposition of the original list.

Lemma split_snd {A B} a (t : list (A × B)) t1 t2 :
prj2 t = t1 ++ a :: t2 → ¬ a ∈ t1 → ∃ k s1 s2, t = s1 ++(k ,a )::s2 ∧ t1 = prj2 s1 ∧ t2 = prj2 s2.

Lemma split_fst {A B} a (t : list (A × B)) t1 t2 :
prj1 t = t1 ++ a :: t2 → ¬ a ∈ t1 → ∃ k s1 s2, t = s1 ++(a ,k )::s2 ∧ t1 = prj1 s1 ∧ t2 = prj1 s2.

If n is smaller than the length of u, then u can be split into a prefix of size n, followed by a non-empty list.

Lemma split_word {A} n (u : list A) : n < ⎢u ⎥ → ∃ x u1 u2, u = u1 ++x ::u2 ∧ ⎢u1 ⎥ = n.

Subsets of a list

Fixpoint subsets {A : Set} (l : list A) :=
  match l with
  | [] ⇒ [[]]
| a::l ⇒ map (cons a) (subsets l)++subsets l
  end.

Lemma subsets_In {A : Set}(l : list A) :
  ∀ m, m ∈ subsets l → m ⊆ l.

Lemma incl_cons_disj {A : Set} (a : A) m l :
  m ⊆ a :: l → m ⊆ l ∨ ∃ m', m ≈ a ::m' ∧ m' ⊆ l.

Lemma subsets_spec {A : Set} (l : list A) :
  ∀ m, m ⊆ l ↔ ∃ m', m' ∈ subsets l ∧ m ≈ m'.

Lemma subsets_NoDup {A : Set} (k l : list A) :
  NoDup l → k ∈ subsets l → NoDup k.

Pairs

Definition pairs {A B : Set} l r : list (A × B) :=
fold_right (fun a acc ⇒ (map (fun b ⇒ (a ,b )) r )++acc) [] l.

Lemma pairs_spec {A B : Set} l r (a : A) (b : B) : (a ,b ) ∈ pairs l r ↔ a ∈ l ∧ b ∈ r.

Enumerate lists of a certain length

Fixpoint lists_of_length {A} (elts:list A) n :=
  match n with
  | 0 ⇒ [[]]
| S n ⇒ flat_map (fun l ⇒ map (fun e ⇒ e ::l) elts) (lists_of_length elts n)
  end.

Lemma lists_of_length_spec {A} (elts : list A) n l :
  l ∈ lists_of_length elts n ↔ ⎢l ⎥ = n ∧ l ⊆ elts.

Pad a list with an element

Definition pad {A} (e : A) (l : list A) := e ::flat_map (fun a ⇒ [a ;e ]) l.

Lemma pad_contents {A} (e : A) l : pad e l ≈ e ::l.

Lists over a decidable set

Section dec_list.
Context { A : Set } { dec_A : decidable_set A }.

Boolean equality for lists

  Fixpoint equal_list l m :=
    match (l ,m ) with
    | ([],[]) ⇒ true
    | (a::l,b::m) ⇒ eqX a b && equal_list l m
    | _ ⇒ false
    end.

  Lemma equal_list_spec l m : reflect (l = m) (equal_list l m).

The set of lists of As is decidable.

Global Instance dec_list : decidable_set (list A).

Boolean predicate testing whether an element belongs to a list.

  Definition inb (n : A) l := existsb (eqX n) l.

  Lemma inb_spec n l : inb n l = true ↔ n ∈ l.

  Lemma inb_false n l : inb n l = false ↔ ¬ n ∈ l.

This boolean predicate allows us to use the excluded middle with the predicate In.

Lemma inb_dec n l : { inb n l = true ∧ n ∈ l } + { inb n l = false ∧ ¬ n ∈ l }.

Lemma In_dec (n : A) l : { n ∈ l } + { ¬ n ∈ l }.

Boolean function implementing containment test.

  Definition inclb (a b : list A) :=
    forallb (fun x ⇒ inb x b) a.

  Lemma inclb_correct a b : inclb a b = true ↔ a ⊆ b.

Boolean function testing for equivalence of lists.

Definition equivalentb l1 l2 := inclb l1 l2 && inclb l2 l1.

Lemma equivalentb_spec l1 l2 : equivalentb l1 l2 = true ↔ l1 ≈ l2.

If u=u1++a::u2, we call the triple (u1,u2) an a-decomposition of u if a does not appear in u1.

If a is in l, then there exists an a-decomposition of l.

Lemma decomposition (a : A) l :
a ∈ l ↔ ∃ l1 l2, l = l1 ++ a :: l2 ∧ ¬ a ∈ l1.

Decompositions are unique.

  Lemma decomp_unique (a:A) u1 u2 v1 v2 :
    u1 ++(a ::u2 ) = v1 ++a ::v2 → ¬ In a v1 → ¬ In a u1 → u1 = v1 ∧ u2 = v2.

  Lemma decomp_unambiguous (u1 u2 v1 v2 : list A) a b :
    u1 ++a ::u2 = v1 ++b ::v2 → ¬ In a v1 → ¬ In b u1 → u1 = v1 ∧ a =b ∧ u2 = v2.

{{l}} is a list containing the same elements as l, but without duplication.

  Definition undup l :=
    fold_right (fun a acc ⇒
                  if inb a acc
                  then acc
                  else a ::acc)
               nil
               l.

  Notation " {{ l }} " := (undup l) (at level 0).

{{l}} is shorter than l.

Lemma undup_length l : ⎢{{l }}⎥ ≤ ⎢l ⎥ .

{{l}} contains the same elements as l.

Lemma In_undup a l: a ∈ {{l }} ↔ a ∈ l.

Put differently, {{l}} is equivalent to l.

Lemma undup_equivalent l : {{l }} ≈ l.

The {{}} operator always produces a duplication free list.

Lemma NoDup_undup l : NoDup {{l }}.

The {{}} operator doesn't change duplication free lists.

Lemma NoDup_undup_eq l : NoDup l → l = {{l }}.

A list is without duplication if and only if its mirror is duplication free.

Lemma NoDup_rev {X:Set} (l : list X) : NoDup l ↔ NoDup (rev l).

{{}} preserves both ⊆ and ≈.

Global Instance undup_incl_Proper : Proper (@incl A ==> @incl A) undup.
Global Instance undup_equivalent_Proper : Proper (@equivalent A ==> @equivalent A) undup.

If l is contained in m and doesn't contain duplicates, then it must be shorter than m.

Lemma NoDup_length (l m : list A) :
l ⊆ m → NoDup l → ⎢l ⎥ ≤ ⎢m ⎥ .

l is a fixpoint of map f if and only if {{l}} is a fixpoint of the same list homomorphism map f.

Lemma map_undup_id (l : list A) (f : A → A) :
map f l = l ↔ map f {{l }} = {{l }}.

If f is injective, map f and {{}} commute.

Lemma map_undup_inj (l : list A) (f : A → A) :
(∀ x y, f x = f y → x = y ) → map f {{l }} = {{map f l }}.

NoDup is a decidable property.

Definition NoDupb l := l =?= {{l }}.

Lemma NoDupb_NoDup l : NoDupb l = true ↔ NoDup l.

Remove an element from a list.

  Definition rm (a : A) l := (fun x ⇒ negb (a =?=x)) :> l.
  Notation " l ∖ a " := (rm a l) (at level 50).

  Lemma rm_In b a l : b ∈ l ∖ a ↔ b ∈ l ∧ a ≠b.

  Lemma rm_equiv a l : a ∈ l → l ≈ a ::(l ∖ a ).

  Global Instance rm_equivalent_Proper a : Proper ((@equivalent A )==> (@equivalent A )) (rm a).

  Global Instance rm_incl_Proper a : Proper ((@incl A )==> (@incl A )) (rm a).

  Lemma rm_notin a l : ¬ a ∈ l → l ∖ a = l.

Remove the first occurrence of an element from a list.

  Fixpoint rmfst (a : A) l :=
  match l with
  | [] ⇒ []
  | b::l ⇒ if a =?=b then l else b::(rmfst a l )
  end.
  Notation " l ⊖ a " := (rmfst a l) (at level 50).

  Lemma rmfst_notin a l : ¬ a ∈ l → l ⊖ a = l.

  Lemma rmfst_in a l1 l2 : ¬ a ∈ l1 → (l1 ++ a :: l2 ) ⊖ a = l1 ++l2.

l ⊖ a is contained in the list l.

Lemma rmfst_decr a l : l ⊖ a ⊆ l.

The operation rmfst commutes with itself.

Lemma rmfst_comm (l : list A) a b : (l ⊖ a ) ⊖ b = (l ⊖ b ) ⊖ a.

If we try to remove a from l++m, one of three things may happen:

a appears in l, so we obtain (l⊖ a)++m;
a appears in m but not in l, so we obtain l++(m⊖ a);
a does not appear in l or m, so we obtain l++m.

  Lemma rmfst_app_dec (l m:list A) a :
    (∃ l1 l2, l = l1 ++a ::l2 ∧ ¬ a ∈ l1 ∧ (l ++m ) ⊖ a = l1 ++l2 ++m )
    ∨ (∃ m1 m2, m = m1 ++a ::m2 ∧ ¬ a ∈ (l ++m1 ) ∧ (l ++m ) ⊖ a = l ++m1 ++m2 )
    ∨ (¬ a ∈ (l ++m ) ∧ (l ++m ) ⊖ a = l ++m ).

This lemma highlights the existence of a list l1-l2: the list m shown to exist here is such that it contains no elements from l1, but concatenating l1 and m yields a list equivalent to l1++l2. Furthermore, we produce m without inserting any duplicates.

Lemma split_app_unambiguous (l1 l2 : list A) :
∃ m, l1 ++l2 ≈ l1 ++m ∧ NoDup m ∧ (∀ a, a ∈ m → ¬ a ∈ l1 ).

Sometimes we will need to count the number of occurrences of a particular element in a given list.

Notation nb a l := ⎢eqX a :> l⎥.

An equivalent (but slightly less convenient) function was defined in the standard library.

Lemma nb_count_occ (a : A) l : nb a l = count_occ X_dec l a.

For convenience, we translate all the lemmas regarding count_occ in terms of nb.

  Lemma nb_nil (x : A) : nb x [] = 0.

  Lemma nb_In l (x : A) : x ∈ l ↔ nb x l > 0.

  Lemma nb_not_In (l : list A) (x : A): ¬ x ∈ l ↔ nb x l = 0.

  Lemma NoDup_nb (l : list A) : NoDup l ↔ (∀ x : A, nb x l ≤ 1).

  Lemma nb_inv_nil (l : list A) : (∀ x : A, nb x l = 0) ↔ l = [].

  Lemma nb_cons_neq (l : list A) (x y : A) : x ≠ y → nb y (x :: l) = nb y l.

  Lemma nb_cons_eq (l : list A) (x y : A) : x = y → nb y (x :: l) = S (nb y l).

  Lemma NoDup_nb' (l : list A) : NoDup l ↔ (∀ x : A, x ∈ l → nb x l = 1).

End dec_list.
Notation " l ∖ a " := (rm a l) (at level 50).
Notation " l ⊖ a " := (rmfst a l) (at level 50).
Notation nb a l := ⎢eqX a :> l⎥.
Notation " {{ l }} " := (undup l) (at level 0).

Lemma nb_map {A B :Set} `{decidable_set A,decidable_set B} (f : A → B) :
  (∀ x1 x2 : A, f x1 = f x2 → x1 = x2 ) →
  ∀ (x : A) (l : list A), nb x l = nb (f x) (map f l).

Lemma rmfst_flip {A B : Set} `{decidable_set A,decidable_set B} (s : list (A ×B)) a b :
  s ` ⊖ (a ,b ) = (s ⊖ (b ,a ))`.

Sum function

If a1,...,an are elements in A and f is a function from A to nat, then sum f [a1;...;an] is the natural number f a1+...+f an.

Definition sum {A} f (l : list A) := fold_right (fun a acc ⇒ f a + acc) 0 l.

sum f distributes over concatenations.

Lemma sum_app {A} f (l m : list A) : sum f (l ++m) = sum f l + sum f m.

If l is contained in m and has no duplicates, then summing f on l yields a smaller value than summing f on m.

Lemma sum_incl_ND {A} f (l m : list A) :
l ⊆ m → NoDup l → sum f l ≤ sum f m.

If two duplicate-free list are equivalent, then summing f on any of them yields the same result.

Lemma sum_eq_ND {A} f (l m : list A) :
l ≈ m → NoDup l → NoDup m → sum f l = sum f m.

If f is pointwise smaller than g, then the sum sum f l is smaller than sum g l.

Lemma sum_incr {A} f g (l : list A) : (∀ x, f x ≤ g x ) → sum f l ≤ sum g l.

sum f l only depends on the values of f, not its implementation.

Lemma sum_ext {A} f g (l : list A) : (∀ x, f x = g x ) → sum f l = sum g l.

Lemma sum_ext_In {A} f g (l : list A) : (∀ x, x ∈ l → f x = g x ) → sum f l = sum g l.

If h is the pointwise sum of f and g, then sum h l is the sum of sum f l and sum g l.

Lemma sum_add {A} f g h (l : list A) : (∀ x, h x = f x + g x ) → sum h l = sum f l + sum g l.

Lemma sum_add_distr {A} f g (l : list A) : sum f l + sum g l = sum (fun x ⇒ f x + g x) l.

If f is uniformly 0 on the elements of the list l, then sum f l is 0.

Lemma sum_zero_in {A} f (l : list A) : (∀ x, x ∈ l → f x = 0) → sum f l = 0.

If l is contained in m and if m has no duplicates, then the length of l can be obtained by summing over m the function that maps a to the number of occurrences of a in l.

Lemma length_sum_filter {A:Set} {d:decidable_set A} l m:
  l ⊆ m → NoDup m → ⎢l ⎥ = sum (fun a ⇒ nb a l) m.

Lemma sum_le {A} f g (l : list A) :
  (∀ a, a ∈ l → f a ≤ g a ) → sum f l ≤ sum g l.

Lemma sum_lt {A} f g (l : list A) :
  (∀ a, a ∈ l → f a ≤ g a ) → (∃ b, b ∈ l ∧ f b < g b ) → sum f l < sum g l.

Lemma sum_incr_0_left {A : Set} `{decidable_set A} f (l m : list A) :
  (∀ x, ¬ x ∈ l → f x = 0) → sum f {{l }} = sum f {{m ++l }}.

Lemma sum_incr_0_right {A : Set} `{decidable_set A} f (l m : list A) :
  (∀ x, ¬ x ∈ l → f x = 0) → sum f {{l }} = sum f {{l ++m }}.

Lemma sum_filter {A : Set} (P : A → bool) f l : sum f (P :>l) ≤ sum f l.

Function predicates

Class injective {A B} (f : A → B) :=
  {is_injective : ∀ x y, f x = f y → x = y}.
Class surjective {A B} (f : A → B) :=
  {is_surjective : ∀ y, ∃ x, f x = y}.
Class has_support {A} (f : A → A) l :=
  {is_support : ∀ x, f x ≠ x ↔ In x l}.
Class supported {A} (f : A → A) :=
  {is_supported : ∃ l, has_support f l}.
Lemma has_support_supported {A} f l `{has_support A f l} : supported f.
Hint Resolve has_support_supported.

Global Instance extensional_equality {A B} : SemEquiv (A →B) :=
  { sequiv := fun f g ⇒ ∀ x, f x = g x }.
Global Instance ext_eq_Equiv {A B} : Equivalence (@sequiv (A →B) extensional_equality).
Global Instance extensional_equality2 {A B C} : SemEquiv (A →B →C) :=
  { sequiv := fun f g ⇒ ∀ x y, f x y = g x y }.
Global Instance ext_eq2_Equiv {A B C} : Equivalence (@sequiv (A →B →C) extensional_equality2).

Lemma NoDup_map_injective {A B} {f : A →B} l : injective f → NoDup l → NoDup (map f l).

Lemma injective_support_closed {A} f l {x : A} :
  injective f → has_support f l → x ∈ l → f x ∈ l.

Global Instance ext_eq_map {A B} : Proper (sequiv ==> sequiv) (@map A B).
Global Instance ext_eq_sum {A} : Proper (sequiv ==> sequiv) (@sum A).
Global Instance ext_eq_filter {A} : Proper (sequiv ==> sequiv) (@filter A).
Global Instance ext_eq_fold_left {A B} : Proper (sequiv ==> sequiv) (@fold_left A B).
Global Instance ext_eq_fold_right {A B} : Proper (sequiv ==> sequiv) (@fold_right A B).
Global Instance injective_ext_eq {A B} : Proper (@sequiv (A →B) _ ==> iff) injective.
Global Instance surjective_ext_eq {A B} : Proper (@sequiv (A →B) _ ==> iff) surjective.
Global Instance has_support_ext_eq {A} :
  Proper (@sequiv (A →A) _ ==> (@equivalent A ) ==> iff) has_support.
Global Instance supported_ext_eq {A} :
  Proper (@sequiv (A →A) _ ==> iff) supported.

Lemma map_injective_injective {A B: Set} (f : A → B) :
  injective f → ∀ l m, map f l = map f m → l = m.

Enumerate permutations of a list

Section shuffle.
Context {A : Set}.

insert a l generates the list of all possibles lists l1::a++l2 such that l=l1++l2.

  Fixpoint insert (a : A) l :=
    match l with
    | [] ⇒ [[a ]]
| b::l ⇒ (a ::b::l )::(map (cons b) (insert a l))
    end.

shuffles l generates the list of all lists obtained by reordering the elements of l. For instance shuffles [a;b]=[[a;b];[b;a]].

  Fixpoint shuffles l :=
    match l with
    | [] ⇒ [[]]
| a::l ⇒ flat_map (insert a) (shuffles l)
    end.

  Lemma insert_spec a l m :
    m ∈ insert a l ↔ ∃ l1 l2, l = l1 ++l2 ∧ m = l1 ++a ::l2.

A list m appears in shuffles l exactly when for every a:A there are as may occurrences of a in l as in m.

Lemma shuffles_spec `{decidable_set A} m l : m ∈ shuffles l ↔ ∀ a, nb a l = nb a m.

Shuffles of l contain the same elements.

Lemma shuffles_equiv l m : m ∈ shuffles l → l ≈ m.

If l has no duplicates and m is a shuffle of l, then m has no duplicates either.

Lemma shuffles_nodup l m : NoDup l → m ∈ shuffles l → NoDup m.

Shuffles of l have the same length as l.

Lemma shuffles_length l m : m ∈ shuffles l → ⎢l ⎥ = ⎢m ⎥.

If l has no duplicates, then shuffles l contain exactly the lists that are equivalent to l without having any duplicates.

Lemma In_shuffles l m :
NoDup l → m ∈ shuffles l ↔ l ≈ m ∧ NoDup m.

If l1 is a shuffle of l2, then being a shuffle of l1 is equivalent to being a shuffle of l2.

Lemma eq_shuffles l1 l2 : l1 ∈ shuffles l2 → shuffles l1 ≈ shuffles l2.

If l has no duplicates, neither does shuffles l.

Lemma NoDup_shuffles (l : list A) : NoDup l → NoDup (shuffles l).

End shuffle.

insert commutes with map.

Lemma insert_map {A B : Set} `{decidable_set A,decidable_set B} :
∀ (f : A → B) l a, insert (f a) (map f l) = map (map f) (insert a l).

shuffles commutes with map.

Lemma shuffles_map {A B : Set} `{decidable_set A,decidable_set B} :
  ∀ (f : A → B) l, shuffles (map f l) = map (map f) (shuffles l).

Lemma incl_cons_disj' {A : Set} (a : A) m l :
  NoDup m → m ⊆ a :: l → m ⊆ l ∨ ∃ m', m ≈ a ::m' ∧ m' ⊆ l ∧ NoDup m'.

Lemma all_subsets_nodup {A : Set} (l : list A) :
  NoDup l → ∀ m, m ∈ (flat_map shuffles (subsets l)) ↔ NoDup m ∧ m ⊆ l.

Section group_by_fst.
  Context {A B : Set} `{decidable_set A}.
  Definition group_by_fst : list (A ×B) → list (list B) :=
    fun l ⇒ map (fun a ⇒ map snd ((fun p ⇒ fst p =?= a ):> l)) {{map fst l }}.

  Lemma group_by_fst_length l : ⎢l ⎥ = sum (@length B) (group_by_fst l).

  Lemma group_by_fst_In l b1 b2 :
    (∃ c, c ∈ group_by_fst l ∧ b1 ∈ c ∧ b2 ∈ c ) ↔ ∃ a, (a ,b1 ) ∈ l ∧ (a ,b2 ) ∈ l.

  Lemma group_by_fst_map_supp l f x :
    x ∈ l ↔ (∃ c, c ∈ group_by_fst (map (fun x ⇒ (f x ,x )) l) ∧ x ∈ c ).

  Lemma group_by_fst_map_In l f x1 x2 :
    (∃ c, c ∈ group_by_fst (map (fun x ⇒ (f x ,x )) l) ∧ x1 ∈ c ∧ x2 ∈ c ) ↔
    (x1 ∈ l ∧ x2 ∈ l ∧ f x1 = f x2 ).

End group_by_fst.