Library hydras.rpo.dickson

by Evelyne Contejean

Dickson Lemma: the multiset extension of a well-founded ordering is well-founded.

Set Implicit Arguments.

From Coq Require Import Relations List Setoid Multiset.
From hydras Require Import closure more_list list_permut.

Module Make (DS1 : decidable_set.S).

Module DS := DS1.
Module LP := list_permut.Make (DS1).
Import LP.

Definition of the multiset extension of a relation.

Inductive multiset_extension_step (R : relation elt) : list elt → list elt → Prop :=
  | rmv_case :
     ∀ l1 l2 l la a, (∀ b, In b la → R b a ) →
      list_permut l1 (la ++ l) → list_permut l2 (a :: l) →
      multiset_extension_step R l1 l2.

If n << {a} U m , then either, there exists n' such that n = {a} U n' and n' << m, or, there exists k, such that n = k U m, and k << {a}.

Lemma two_cases :
∀ R a m n,
multiset_extension_step R n (a :: m) →
(∃ n', list_permut n (a :: n') ∧
multiset_extension_step R n' m ) ∨
(∃ k , (∀ b, In b k → R b a ) ∧
list_permut n (k ++ m)).

multiset_extension_step is compatible with permutation.

Lemma list_permut_multiset_extension_step_1 :
  ∀ R l1 l2 l, list_permut l1 l2 →
  multiset_extension_step R l1 l → multiset_extension_step R l2 l.

Lemma list_permut_multiset_extension_step_2 :
  ∀ R l1 l2 l, list_permut l1 l2 →
  multiset_extension_step R l l1 → multiset_extension_step R l l2.

Lemma context_multiset_extension_step_app1 :
  ∀ R l1 l2 l, multiset_extension_step R l1 l2 →
                         multiset_extension_step R (l ++ l1) (l ++ l2).

Lemma context_trans_clos_multiset_extension_step_app1 :
  ∀ R l1 l2 l, trans_clos (multiset_extension_step R) l1 l2 →
                         trans_clos (multiset_extension_step R) (l ++ l1) (l ++ l2).

Lemma context_multiset_extension_step_app2 :
  ∀ R l1 l2 l, multiset_extension_step R l1 l2 →
                         multiset_extension_step R (l1 ++ l) (l2 ++ l).

Add Parametric Morphism R : (@multiset_extension_step R) with signature (list_permut ==> list_permut ==> iff) as mult_morph.

Accessibility lemmata.

Lemma list_permut_acc :
  ∀ R l1 l2, list_permut l2 l1 →
  Acc (multiset_extension_step R) l1 → Acc (multiset_extension_step R) l2.

Add Parametric Morphism R : (Acc (multiset_extension_step R)) with signature (list_permut ==> iff) as acc_morph.

Lemma dickson_aux1 :
∀ (R : relation elt) a,
(∀ b, R b a →
  ∀ m, Acc (multiset_extension_step R) m →
            Acc (multiset_extension_step R) (b :: m)) →
∀ m, Acc (multiset_extension_step R) m →
(∀ m', (multiset_extension_step R) m' m →
             Acc (multiset_extension_step R) (a :: m')) →
Acc (multiset_extension_step R) (a :: m).

Lemma dickson_aux2 :
∀ R m,
  Acc (multiset_extension_step R) m →
  ∀ a, (∀ b, R b a →
             ∀ m, Acc (multiset_extension_step R) m →
                       Acc (multiset_extension_step R) (b :: m)) →
   Acc (multiset_extension_step R) (a :: m).

Lemma dickson_aux3 :
∀ R a, Acc R a → ∀ m, Acc (multiset_extension_step R) m →
Acc (multiset_extension_step R) (a :: m).

Main lemma.

Lemma dickson :
  ∀ R, well_founded R → well_founded (multiset_extension_step R).

Lemma multiset_closure :
  ∀ R p q, transitive _ R →
  closure.trans_clos (multiset_extension_step R) p q →
        ∃ p', ∃ q', ∃ pq ,
        list_permut p (p' ++ pq) ∧
        list_permut q (q' ++ pq) ∧
        q' ≠ nil ∧
        (∀ a, In a p' → ∃ b , In b q' ∧ R a b ).

End Make.