Library LangAlg.tools

Toolbox of simple definitions, lemmas and tactics.

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

Notation " π{ x } " := (proj1_sig x).

Lifting of a binary function with arguments of type A and values of type B to a binary function with arguments of type option A and values of type option B.
Definition option_bimap (A B : Type) (f : A → A → B) x y :=
  match (x,y) with
  | (Some a,Some b) ⇒ Some (f a b)
  | _ ⇒ None
  end.

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).

Typeclass and notation for support functions
Class Support (T : Set → Set → Set) (X Y : Set) :=
  support : T X Y → list X.
Notation " ⌊ e ⌋ " := (support e).

Typeclass and notation for functions extracting sets of variables.
Class Alphabet (T : Set → Set) (X : Set) := variables : T X → list X.
Notation " ⌈ e ⌉ " := (variables e).

Typeclass and notation for size functions
Class Size X :=
  size : X → nat.
Notation " ⦃ e ⦄ " := (size e).

Typeclass and notation for semantic maps.
Class semantics (T : Set → Set) (D : Set → Type) (X : Set) (A : Set)
  := interprete : (X → D A) → T X → D A.
Notation " ⟦ e ⟧ σ " := (interprete σ e) (at level 75).

The following two definitions describe the standard way of relating two terms through their semantics.
Definition semantic_equality
       (T : Set → Set) (D : Set → Type) (X : Set)
       `{ ∀ A : Set, SemEquiv (D A) }
       `{ ∀ A : Set, semantics T D X A } : SemEquiv (T X) :=
  fun x y ⇒ ∀ A : Set,∀ σ : X → D A, ⟦x⟧σ ≃ ⟦y⟧σ.
Definition semantic_containment
       (T : Set → Set) (D : Set → Type) (X : Set)
       `{ ∀ A : Set, SemSmaller (D A) }
       `{ ∀ A : Set, semantics T D X A} : SemSmaller (T X) :=
  fun x y ⇒ ∀ A : Set,∀ σ : X → D A, ⟦x⟧σ ≲ ⟦y⟧σ.

Hint Unfold semantic_containment semantic_equality ssmaller sequiv: semantics.
Global Instance semantic_equality_Equivalence
       (T : Set → Set) (D : Set → Type) (X : Set)
       `{eqA: ∀ A : Set, SemEquiv (D A)}
       `{S : ∀ A, semantics T D X A}
       `{∀ A : Set, Equivalence (eqA A)} :
  Equivalence (@semantic_equality T D X eqA S).

Global Instance semantic_containment_PreOrder
       (T : Set → Set) (D : Set → Type) (X : Set)
       `{inclA: ∀ A : Set, SemSmaller (D A)}
       `{S : ∀ A, semantics T D X A}
       `{∀ A : Set, PreOrder (inclA A)} :
  PreOrder (@semantic_containment T D X inclA S).

Global Instance semantic_containment_PartialOrder
       (T : Set → Set) (D : Set → Type) (X : Set)
       `{eqA: ∀ A : Set, SemEquiv (D A)}
       `{inclA: ∀ A : Set, SemSmaller (D A)}
       `{S : ∀ A, semantics T D X A}
       `{equivA : ∀ A : Set, Equivalence (eqA A)}
       `{preordA : ∀ A : Set, PreOrder (inclA A)}
       `{partordA : ∀ A : Set, PartialOrder (eqA A) (inclA A)} :
  @PartialOrder
    _ _ (@semantic_equality_Equivalence T D X eqA S equivA)
    _ (@semantic_containment_PreOrder T D X inclA S preordA).

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)}.

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.

Whenever we have a decidable set, we can define the following replacement function.
  Definition replace a b := (fun n ⇒ if eqX n a then b else n).

End decidable.


Notation " {| a \ b |} " := (replace a b).

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.
Lemma dec_prod A B :
  decidable_set A → decidable_set B → decidable_set (A×B).

If A is decidable, then so is option A.
Lemma dec_option (A : Set) :
  decidable_set A → decidable_set (option A).

Lists

General lemmas

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) :
  filter f (l++m) = filter f l ++ filter f m.

Filtering reduces the length of the list.
Lemma filter_length {A} (f : A → bool) l :
  length (filter f l) ≤ length l.

The following lemma give a more precise description.
Lemma filter_length_eq {A} (f : A → bool) l :
  length (filter f l) + length (filter (fun x ⇒ negb (f x)) l) = length l.

filter and map commute.
Lemma filter_map {A B} (f : A → bool) (g : B → A) l :
  filter f (map g l) = map g (filter (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, In x l → f x = g x) → filter f l = filter g l.

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

Filtering with the predicate true does not modify the list.
Lemma filter_true {A} (l : list A) :
  filter (fun _ ⇒ true) l = l.

Filtering preserves the property NoDup (absence of duplicates).
Lemma filter_NoDup {A} (f : A → bool) l :
  NoDup l → NoDup (filter f l).

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) :
  length l1 = length m1 → l1++l2 = m1++m2 → l1 = m1 ∧ l2 = m2.

Lists as finite sets

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 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 following simple facts about inclusion 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.

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.

Lists over a decidable set

Section dec_list.
  Context { A : Set }.
  Context { 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 }.

If i is in l, then l can be decomposed as m++i::n, where n doesn't contain i.
  Lemma in_split_strict (i : A) l :
   i ∈ l → ∃ m n, l = m++(i::n) ∧ ¬ i ∈ n.

Removing an element from a list.
  Definition rm (x : A) := filter (fun y ⇒ negb (eqX x y)).
  Hint Unfold rm.

  Lemma in_rm x y l : x ∈ (rm y l) ↔ x ≠ y ∧ x ∈ l .

Removing from m an element that was not in m in the first place does not modify m.
  Lemma rm_notin a m : ¬ a ∈ m → rm a m = m.

rm a commutes with concatenation.
  Lemma rm_app a l m : rm a (l++m) = rm a l ++ rm a m.

rm reduces the length.
  Lemma rm_length x l :
    length (rm x l) ≤ length l.

If x is in l, then rm x l is strictly smaller than l.
  Lemma rm_length_in x l :
    x ∈ l → length (rm x l) < length l.

rm a preserves both ⊆ and ≈.
  Global Instance rm_incl_Proper a :
    Proper (@incl A ==> @incl A) (rm a).
  Global Instance rm_equivalent_Proper a :
    Proper (@equivalent A ==> @equivalent A) (rm a).

Removing an element from a lists reduces its length.
  Lemma length_rm_not_in a (l : list A) :
    a ∈ l → length (rm a l) < length l.


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 → length l ≤ length m.

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.

φ1 ⧼l⧽ φ2 is a function that combines φ1 and φ2 as illustrated by the following pair of lemmas.
  Definition seq_morph {B} (φ1 φ2 : A → B) l :=
    fun x ⇒ if inb x l then φ1 x else φ2 x.

  Notation " f ⧼ l ⧽ g " := (seq_morph f g l) (at level 60).

If x is in the list l, then its image by seq_morph φ1 φ2 l is equal to its image by φ1.
  Lemma seq_morph_in {B} (φ1 φ2 : A → B) l x :
    x ∈ l → (φ1 ⧼l⧽ φ2) x = φ1 x.
Otherwise, φ1 ⧼l⧽ φ2 sends x to φ2 x.
  Lemma seq_morph_not_in {B} (φ1 φ2 : A → B) l x :
    ¬ x ∈ l → (φ1 ⧼l⧽ φ2) x = φ2 x.

seq_morph uses its argument list as a set, so replacing a list with an equivalent list doesn't change the function.
  Lemma seq_morph_equivalent {B} l m
        (f g : A → B) x :
    l ≈ m → (f ⧼l⧽ g) x = (f ⧼m⧽ g) x.

End dec_list.

Bimap

bimap f l m computes the list containing every element of the shape f x y, with x in l and y in m. For instance, if we take f to be the pairing function that associate to x and y the pair (x,y), then bimap f l m is the Cartesian product of the lists l and m.
Definition bimap A B C (f : A → B → C) l m :=
  flat_map (fun a ⇒ map (f a) m) l.

Lemma in_bimap A B C (f : A → B → C) l m x :
  x ∈ (bimap f l m) ↔ ∃ a b, f a b = x ∧ a ∈ l ∧ b ∈ m.

We can absorb a map inside a bimap.
Lemma map_bimap A B C D (g : C → D) (f : A → B → C) l m :
  map g (bimap f l m) = bimap (fun x y ⇒ g (f x y)) l m.

bimap f is monotone.
Global Instance bimap_equiv {A B C} (f : A → B → C) :
  Proper ((@equivalent A) ==> (@equivalent B)==> (@equivalent C)) (bimap f).

Invertible functions

ψ is the inverse on φ in the list A if ψ∘φ is the identity on the elements of A.
Definition inverse {X Y: Set} (φ : X → Y) ψ A :=
  ∀ x, x ∈ A → ψ (φ x) = x.

φ is injective on A if it admits an inverse on A.
Definition injective {X Y: Set} (φ : X → Y) A :=
  ∃ ψ, inverse φ ψ A.

For we can compute an inverse of a composite function by composing the inverses of its parts in reverse order.
Lemma inverse_composition {X Y Z : Set}
      (f : X → Y) f' (g : Y → Z) g' A :
  inverse f f' A → inverse g g' (List.map f A) →
  inverse (g∘f) (f'∘g') A.
Lemma injective_compose {X Y Z : Set}
      (f : X → Y) (g : Y → Z) A :
  injective f A → injective g (List.map f A) → injective (g∘f) A.

The function {|b\a|} is the inverse of {|a\b|} on any list that does not contain the element b.
Lemma inverse_replace {X : Set} `{decidable_set X} (a b : X) A :
  ¬ b ∈ A → inverse {| a \ b |} {| b \ a |} A.

Lemma injective_replace {X : Set} `{decidable_set X} (a b : X) A :
  ¬ b ∈ A → injective {| a \ b |} A.

The following trivial lemmas are used in many places in the proof.
Definition incr a b := a + b.
Notation " ⨥ " := incr.
Definition decr a b := b - a.
Notation " ⨪ " := decr.
Hint Transparent incr decr.
Hint Unfold decr incr.

Lemma inverse_add_left n A :
  inverse (⨥ n) (⨪ n) A.
Lemma injective_add_left n A : injective (⨥ n) A.

Lists over a duplicated set

In several parts of the proofs, we'll need to duplicate our alphabet. This section provides the way to do that, as well as some key observations about this new alphabet.
Section primed.
  Context {X : Set } {D : decidable_set X}.

We encode the duplicated alphabet as the Cartesian product of the original alphabet with the booleans. We will call the pair (a,true) a positive occurrence of a, and the pair (a,false) a negative occurrence of a.
  Definition X' : Set := X × bool.

A list A is said to be balanced if a letter appear positively if and only if it appears negatively.
  Definition is_balanced A := ∀ a : X, (a,true) ∈ A ↔ (a,false) ∈ A.

Concatenation preserves balance.
  Lemma is_balanced_app A B :
    is_balanced A → is_balanced B → is_balanced (A++B).

The empty list is balanced.
  Lemma balanced_nil : is_balanced (@nil (X×bool)).

If the original alphabet is decidable, so is its duplicate.
  Definition eqX' (a b : X') :=
    eqX (fst a) (fst b) && eqb (snd a) (snd b).
  Lemma eqX'_spec a b : reflect (a = b) (eqX' a b).
  Global Instance dec_X' : decidable_set X' :=
    Build_decidable_set eqX'_spec.

End primed.