PADEC - Coq Library

Library Padec.Tools.WellfoundedUtil

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global Imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Wellfounded.
From Coq Require Import RelationPairs.
From Coq Require Import Arith.
From Coq Require Import Morphisms_Prop.
From Coq Require Import Bool.
From Coq Require Import Lia.

Local Imports

From CoLoR Require RelUtil.

From Padec Require Import SetoidUtil.
From Padec Require Import ListUtils.
From Padec Require Import ZUtils.
From Padec Require Import RelationA.

Open Scope signature_scope.
Set Implicit Arguments.

Tools for proving well-foundedness on transformed relations

Global Instance Acc_per_morphism {A: Type} `{SA: PartialSetoid A}
         (R: A -> A -> Prop) `(pR: Proper _ fequiv R)
         `(closure: forall x y, R y x -> Proper pequiv x -> Proper pequiv y):
  Proper fequiv (Acc R).

Lemma Acc_per_impl {A: Type} `{SA: PartialSetoid A}
      (R1 R2: A -> A -> Prop) `(pR: R1 =~= R2)
      `(closure: forall x y, R1 y x -> Proper pequiv x -> Proper pequiv y):
  (pequiv ==> impl ) (Acc R2 ) (Acc R1 ).

Lemma Acc_per_morphism' {A: Type} `{SA: PartialSetoid A}
      (R1 R2: A -> A -> Prop) `(pR: R1 =~= R2)
      `(closure_R1: forall x y, R1 y x -> Proper pequiv x -> Proper pequiv y)
      `(closure_R2: forall x y, R2 y x -> Proper pequiv x -> Proper pequiv y):
  (pequiv ==> iff ) (Acc R1 ) (Acc R2 ).

Section Well_Founded.

Two equivalent relations are equivalently well founded.

  Lemma wf_rel_equiv:
    forall (A: Type) (R1: relation A) (R2: relation A),
      (forall a b, R1 a b <-> R2 a b ) -> (well_founded R1 <-> well_founded R2 ).

Any well-founded relation cannot be reflexive!

  Lemma acc_rel_is_non_reflexive:
    forall (A: Type) (R: relation A) (x: A), Acc R x -> ~R x x.

  Lemma wf_rel_is_non_reflexive:
    forall (A: Type) (R: relation A),
      well_founded R -> forall x, ~R x x.

Equivalence between two different definitions of the transitive of a relation.

  Lemma equiv_clos_trans_transitive_closure:
    forall (A: Type) (R: relation A) (x y: A),
      Relation_Operators.clos_trans R x y <-> transitive_closure R x y.

  Lemma equiv_wf_clos_trans_wf_transitive_closure:
    forall (A: Type) (R: relation A),
      well_founded (Relation_Operators.clos_trans R) <->
      well_founded (transitive_closure R).

A well-founded relation has a well-founded transitive closure.

  Lemma wf_rel_has_wf_transitive_closure:
    forall (A: Type) (R: relation A),
      well_founded R -> well_founded (transitive_closure R).

A well-founded has a non reflexive transitive closure.

  Lemma wf_rel_has_non_reflexive_transitive_closure:
    forall (A: Type) (R: relation A),
      well_founded R -> forall x, ~(transitive_closure R) x x.

With Setoid

Two equivalent relations are equivalently well-founded.

  Lemma well_founded_equiv_equiv {A: Type} `{SA: Setoid A}:
    forall (R1 R2: A -> A -> Prop),
      R1 =~= R2 -> (well_founded R1 <-> well_founded R2 ).

The flips (transpositions) of two equivalent relations are equivalent.

  Lemma flip_equiv_equiv {A: Type} `{SA: Setoid A}:
    forall (R1 R2: A -> A -> Prop),
      R1 =~= R2 -> (equiv ==> equiv ==> iff ) (flip R1 ) (flip R2 ).

The flip of two equivalent relations are equivalently well-founded.

  Lemma well_founded_flip_equiv_equiv {A: Type} `{SA: Setoid A}:
    forall (R1 R2: A -> A -> Prop),
      R1 =~= R2 -> (well_founded (flip R1) <-> well_founded (flip R2)).

A well-founded relation cannot be reflexive (using equality on elements and assuming compatibility of the elements.

  Lemma wf_rel_for_non_equiv_elements {A: Type} `{SA: Setoid A}:
    forall (R: relation A) (R_compat: Proper fequiv R),
      well_founded R -> forall x y, R x y -> ~x == y.

For any compatible relation, flip (transposition) is also compatible.

  Lemma flip_proper_rel {A: Type} `{SA: Setoid A}:
    forall (R: relation A) (R_compat: Proper fequiv R),
      Proper fequiv (flip R).

For any well-founded relation, for any point x and z, x is not z and there exists a path from x to z is equivalent to x has a neighbor y and there exists a path from y to z

  Lemma well_founded_strict {A: Type} `{SA: Setoid A}:
    forall (R: relation A) (R_compat: Proper fequiv R),
      well_founded R ->
      forall x z,
        (exists y , R x y /\ reflexive_transitive_closure R y z )
        <->
        (~x == z /\ reflexive_transitive_closure R x z ).

Well_founded / Finite elements

The goal of the section is to show that a relation on a finite set of elements is a well-founded order

iff

the transitive closure of the relation is not reflexive, i.e., there is no cycle in the relation.

We deduce that in case of finite elements, a relation is well-founded iff its inverse is well-founded

Lemma wf_rel_has_non_reflexive_transitive_closure (well_founded R -> forall x, ~(transitive_closure R) x x) provides one implication, with no requirement on the set of elements.

We prove here the inverse implication, i.e. (see above)

Lemma finite_acyclic_wf: forall (lA: list A) (all: forall a, InA eqA a lA) (R: relation A) (R_dec: forall a1 a2, {R a1 a2}+{~R a1 a2}) (R_compat: Proper (eqA ==> eqA ==> iff) R), (forall x: A, ~ transitive_closure R x x) -> well_founded R.

  Section Wf_flip_finite.

    Context {A: Type} `{SA: Setoid A}
            {A_dec: Decider (equiv (A:=A))}.

TCR and properties

The proof of the result uses a subrelation of the transitive closure, i.e., the transitive closure between elements of a given list only

    Inductive TCR (l: list A) (R: relation A): relation A :=
    | TCR_step: forall x y, R x y -> TCR l R x y
    | TCR_transitivity: forall x y z, InA equiv y l ->
                                      TCR l R x y -> TCR l R y z -> TCR l R x z.

    Lemma TCR_gen:
      forall (l: list A) (R: relation A) (x y: A),
        TCR l R x y -> transitive_closure R x y.

    Lemma TCR_all:
      forall (lA: list A) (all: forall a, InA equiv a lA)
             (R: relation A) (x y: A),
        transitive_closure R x y -> TCR lA R x y.

    Lemma TCR_all_equiv:
      forall (lA: list A) (all: forall a, InA equiv a lA)
             (R: relation A) (x y: A),
        transitive_closure R x y <-> TCR lA R x y.

    Instance TCR_compat:
      Proper (equivlistA equiv ==> fequiv ==> equiv ==> equiv ==> iff) TCR.

    Lemma TCR_incl:
      forall (R: relation A) (l l': list A),
        inclA equiv l l' -> forall a1 a2, TCR l R a1 a2 -> TCR l' R a1 a2.

    Inductive TCR_left (l: list A) (R: relation A): relation A :=
    | TCR_left_step: forall x y, R x y -> TCR_left l R x y
    | TCR_left_transitivity:
        forall x y z, InA equiv y l -> R x y ->
                      TCR_left l R y z -> TCR_left l R x z.

    Lemma TCR_left_TCR_equiv:
      forall (R: relation A) (l: list A) (x y: A),
        TCR l R x y <-> TCR_left l R x y.

    Inductive TCR_right (l: list A) (R: relation A): relation A :=
    | TCR_right_step: forall x y, R x y -> TCR_right l R x y
    | TCR_right_transitivity:
        forall x y z, InA equiv y l -> R y z ->
                      TCR_right l R x y -> TCR_right l R x z.

    Lemma TCR_right_TCR_equiv:
      forall (R: relation A) (l: list A) (x y: A),
        TCR l R x y <-> TCR_right l R x y.

TCR does not require that the first and last elements of the chain be in the list. Hence the relation is preserved when removing one the them from the list.

    Lemma TCR_remove_1:
      forall (R: relation A) (R_compat: Proper fequiv R) (l: list A) (a1 a2: A),
        TCR l R a1 a2 -> TCR (removeA A_dec a1 l) R a1 a2.

    Lemma TCR_remove_2:
      forall (R: relation A) (R_compat: Proper fequiv R) (l: list A) (a1 a2: A),
        TCR l R a1 a2 -> TCR (removeA A_dec a2 l) R a1 a2.

    Lemma remove_incl:
      forall (l: list A) (a: A), inclA equiv (removeA A_dec a l) l.

    Lemma TCR_remove_1_iff:
      forall (R: relation A) (R_compat: Proper fequiv R) (l: list A) (a1 a2: A),
        TCR l R a1 a2 <-> TCR (removeA A_dec a1 l) R a1 a2.

    Lemma TCR_remove_2_iff:
      forall (R: relation A) (R_compat: Proper fequiv R) (l: list A) (a1 a2: A),
        TCR l R a1 a2 <-> TCR (removeA A_dec a2 l) R a1 a2.

Checking if there exists an element with some property in a list is decidable, provided that the property itself is decidable.

    Lemma finite_dec:
      forall (l: list A) (P: A -> Prop) (P_compat: Proper fequiv P)
             (P_dec: forall a, { P a } + { ~ P a }),
        { (exists a , InA equiv a l /\ P a ) } +
        { ~(exists a , InA equiv a l /\ P a ) }.

    Lemma finite_dec':
      forall (lA: list A) (all: forall a, InA equiv a lA)
             (P: A -> Prop) (P_compat: Proper fequiv P)
             (P_dec: forall a, { P a } + { ~ P a }),
        { (exists a , P a ) } + { ~(exists a , P a ) }.

length of a list when an element is removed

    Lemma removeA_length_leq:
      forall (l: list A) (a: A), (length (removeA A_dec a l)) <= length l.

    Lemma removeA_length_le:
      forall (l: list A) (a: A),
        InA equiv a l -> (length (removeA A_dec a l)) < length l.

Decidability of transitive closure over finite sets

If the set is finite, checking that a pair of elements are related with transitive closure is decidable (provided that the relation itself is decidable).

The proof shows the result for TCR and for any list of any length as intermediate goal: this proof is done using induction on the lenght of the list.

    Lemma finite_transitive_closure_dec:
      forall (lA: list A) (all: forall a, InA equiv a lA)
             (R: relation A) (R_dec: forall a1 a2, {R a1 a2 }+{~R a1 a2 })
             (R_compat: Proper fequiv R),
      forall (a1 a2: A), {transitive_closure R a1 a2 } +
                         {~transitive_closure R a1 a2 }.

Pointwise strict order on list

    Inductive PW_lt (X: Type) (ltX eqX: relation X): relation (list X) :=
    | PWcons1: forall a a' l l',
        ltX a a' -> PW_lt ltX eqX l l' -> PW_lt ltX eqX (a ::l) (a'::l')
    | PWcons2: forall a a' l l',
        ltX a a' -> eqlistA eqX l l' -> PW_lt ltX eqX (a ::l) (a'::l')
    | PWcons3: forall a a' l l',
        eqX a a' -> PW_lt ltX eqX l l' -> PW_lt ltX eqX (a ::l) (a'::l').

    Lemma PW_length:
      forall (X: Type) (ltX eqX: relation X),
      forall (l1 l2: list X), PW_lt ltX eqX l1 l2 -> length l1 = length l2.

    Definition PW_lt_n (X: Type) (ltX eqX: relation X) (n: nat)
               (l1 l2: list X): Prop :=
      (length l1 = n /\ length l2 = n ) /\ PW_lt ltX eqX l1 l2.

    Lemma PW_lt_n_length_l:
      forall (X: Type) (ltX eqX: relation X) (l1 l2: list X),
        PW_lt eqX ltX l1 l2 -> PW_lt_n eqX ltX (length l1) l1 l2.

    Lemma PW_lt_n_length_r:
      forall (X: Type) (ltX eqX: relation X) (l1 l2: list X),
        PW_lt eqX ltX l1 l2 -> PW_lt_n eqX ltX (length l2) l1 l2.

    Lemma Acc_PW_lt_n:
      forall (X: Type) (ltX eqX: relation X) (n: nat) (lx: list X),
        length lx = n -> Acc (PW_lt_n ltX eqX n) lx -> Acc (PW_lt ltX eqX) lx.

    Lemma PW_lt_n_wf:
      forall (X: Type) (ltX eqX: relation X) (eqX_equiv: Equivalence eqX)
             (px: Proper (eqX ==> eqX ==> iff) ltX) (wfX: well_founded ltX),
      forall (n: nat), well_founded (PW_lt_n ltX eqX n).

The point strict order on list is well-founded when the strict order on elements is well-founded.

    Lemma PW_lt_wf:
      forall (X: Type) (ltX eqX: relation X) (eqX_equiv: Equivalence eqX)
             (px: Proper (eqX ==> eqX ==> iff) ltX) (wfX: well_founded ltX),
        well_founded (PW_lt ltX eqX).

A relation with non-reflexive transitive closure over finite sets

is well-founded.

For the proof, we build for any element a list of nat as follows:

R_trans_dec := (finite_transitive_closure_dec all R_dec R_compat) left_cone_charac := fun a0 a : A => if R_trans_dec a a0 then 1%nat else 0%nat measure := fun a0 : A => map (left_cone_charac a0) lA

And we show that for any a1, a2 such that R a1 a2 we have:

PW_lt lt eq (measure a1) (measure a2)

Inclusion of well-founded order and Lemma PW_lt_wf lead to the conclusion.

    Lemma finite_acyclic_wf:
      forall (lA: list A) (all: forall a, InA equiv a lA)
             (R: relation A) (R_compat: Proper fequiv R)
             (R_dec: forall a1 a2, {R a1 a2 } + {~R a1 a2 }),
        (forall x: A, ~ transitive_closure R x x ) -> well_founded R.
      Import Lia.

Consequences on inverse relation

    Lemma transitive_closure_flip:
      forall (R: relation A) (x y: A),
        transitive_closure R x y <-> transitive_closure (flip R) y x.

    Lemma tc_equiv:
      forall (R1: relation A) (R2: relation A) (equiv: R1 =~= R2),
      forall (x y: A),
        transitive_closure R1 x y <-> transitive_closure R2 x y.

    Lemma flip_flip:
      forall (R: relation A) (R_compat: Proper fequiv R),
        (flip (flip R)) =~= R.

    Lemma finite_acyclic_wf_flip:
      forall (lA: list A) (all: forall a, InA equiv a lA)
             (R: relation A) (R_compat: Proper fequiv R)
             (R_dec: forall a1 a2, {R a1 a2 }+{~R a1 a2 }),
        (forall x, ~ transitive_closure R x x ) -> well_founded (flip R).

    Lemma wf_flip_finite:
      forall (lA: list A) (all: forall a, InA equiv a lA)
             (R: relation A) (R_compat: Proper fequiv R)
             (R_dec: forall a1 a2, {R a1 a2 }+{~R a1 a2 }),
        well_founded R <-> well_founded (flip R).

  End Wf_flip_finite.

End Well_Founded.

Lemma not_not_dec:
  forall (A: Type) (R: relation A)
         (R_dec: forall a b: A, { R a b } + { ~R a b }),
  forall a b, R a b <-> ~ ~ R a b.

Lemma not_exists_forall:
  forall (A: Type) (R: relation A),
  forall (y: A), ~(exists x , R x y ) <-> (forall x, ~R x y ).

Lemma existsb_sig {A: Type} `{SA: Setoid A}:
  forall (f: A -> bool) (f_compat: Proper fequiv f) (l: list A),
    existsb f l = true -> {x : A | InA equiv x l /\ f x = true }.

Section Wf_finite.

  Lemma exists_forall_finite_dec {A: Type} `{SA: Setoid A}:
    forall (lA: list A) (all: forall a, InA equiv a lA),
    forall (R: relation A) (R_dec: forall a b, { R a b } + { ~R a b })
           (R_compat: Proper fequiv R),
    forall y, { x | R x y } + { forall x, ~R x y }.

  Lemma wf_finite_path {A: Type} `{SA: Setoid A}:
    forall (lA: list A) (all: forall a, InA equiv a lA),
    forall (R: relation A)
           (R_dec: forall a b, { R a b } + { ~R a b })
           (R_compat: Proper fequiv R),
      well_founded R ->
      forall x, exists (p: list A) y , chain R y p x /\ forall x, ~R x y.

End Wf_finite.

Lexicographic ordering on pairs Well founded property

Section Lexico_pairs.

  Context {A B: Type}.
  Variable (eqA ltA: relation A) (ltB: relation B).

  Inductive lexico_pairs: relation (A * B) :=
  | lpA: forall a a' b b', ltA a a' -> lexico_pairs (a , b ) (a', b')
  | lpB: forall a a' b b', eqA a a' -> ltB b b' -> lexico_pairs (a , b ) (a', b').

  Lemma lexico_pairs_inv:
    forall a a' b b', lexico_pairs (a , b ) (a', b') ->
                      ltA a a' \/ eqA a a' /\ ltB b b'.

  Lemma lexico_pairs_intro:
    forall a a' b b', ltA a a' \/ eqA a a' /\ ltB b b' ->
                      lexico_pairs (a , b ) (a', b').

  Lemma lexico_pairs_Acc:
    Transitive eqA ->
    inclusion (RelUtil.compose ltA eqA) ltA ->
    well_founded ltB -> forall a, Acc ltA a ->
                                  forall b, Acc lexico_pairs (a , b ).

  Lemma lexico_pairs_wf:
    Transitive eqA ->
    inclusion (RelUtil.compose ltA eqA) ltA ->
    well_founded ltA -> well_founded ltB -> well_founded lexico_pairs.

End Lexico_pairs.

Close Scope signature_scope.
Unset Implicit Arguments.