PADEC - Coq Library

Library Padec.Tools.Count

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global Imports

Require Import Relations.
Require Import Setoid.
Require Import SetoidList.
Require Import SetoidClass.
Require Import Zcompare.
Require Import Basics.
Require Import Arith.
Require Import List.
Require Import RelationPairs.
Require Import Morphisms.
Require Import Coq.Numbers.Natural.Peano.NPeano.
Require Import Lia.

Local Imports

Require Import NatUtils.
Require Import OptionUtil.
Require Import SetoidUtil.

Unset Implicit Arguments.
Open Scope nat_scope.

Counting the number of elements in sets

Setoid injection

Definitions of tools to order setoids by Cardinality

setoids A/RA and B/RB are compared (A has less equivalence classes than B)
we define Injection as the existence of an injection relation inj_R between A/RA and B/RB that satisfies two properties:
- at_most_one_left: inj_R transports the relation pairs from B to A.
- at_least_one_right: inj_R relates every relation pair in A to at least one relation pair in B

Relation R transports pairs in RB to pairs in RA :

For any class b in B/RB there is at most one pair a in A/RA st R a b

Definition left_unique
           A `{SA:Setoid A}
           B `{SB:Setoid B}
           (R: A -> B -> Prop) :=
  forall (a1: A) (b1: B) (h1: R a1 b1)
         (a2: A) (b2: B) (h2: R a2 b2),
    (b1 == b2 -> a1 == a2).

Relation R relates each pair in RA to at least one pair in RB

Definition left_total
           A `{SA:Setoid A}
           B `{SB:Setoid B}
           (R: A -> B -> Prop) :=
  forall (a1 a2: A), a1 == a2 ->
                     exists (b1 b2: B ),
                       R a1 b1 /\ R a2 b2 /\ b1 == b2.

Inductive Inj
          A `{SA:Setoid A}
          B `{SB:Setoid B} : Prop:=
  mkInj:
    forall
      (inj_R: A -> B -> Prop)
      (inj_proper: Proper fequiv inj_R)
      (inj_left_unique: left_unique A B inj_R)
      (inj_left_total: left_total A B inj_R),
      Inj A B.

Inj facts

Inj is reflexive

Lemma Inj_refl:
  forall {A: Type} `{SA: Setoid A},
    Inj A A.

Lemma Inj_trans: forall
    {A: Type} `{SA: Setoid A}
    (B: Type) `{SB: Setoid B}
    {C: Type} `{SC: Setoid C},
    Inj A B ->
    Inj B C -> Inj A C.

Modelling Cardinality ordering

Card with parameter Smaller, Same or Larger (see Card_Prop) allows to express A/RA having as many, less or more classes then B/RB

Card_Prop : enumeration of the three basic

Inductive Card_Prop: Type := Smaller | Same | Larger.

symmetric values for Card_Prop

Definition sym_Card_Prop (prop: Card_Prop): Card_Prop :=
  match prop with
  | Smaller => Larger
  | Same => Same
  | Larger => Smaller
  end.

Definition Card (prop: Card_Prop)
           (A : Type) {SA: Setoid A}
           (B : Type) {SB: Setoid B} : Prop:=
  match prop with
    Smaller => Inj A B
  | Same => Inj A B /\ Inj B A
  | Larger => Inj B A
  end.

Card Same implies any relation

Lemma Card_weak: forall (prop: Card_Prop)
                        {A : Type} `{SA: Setoid A}
                        {B : Type} `{SB: Setoid B},
    Card Same A B -> Card prop A B.

Card is reflexive

Lemma Card_refl:
forall (prop: Card_Prop) {A : Type} `{SA: Setoid A},
Card prop A A.

Card is symmetric when using opposite property

Lemma Card_sym:
  forall (prop: Card_Prop)
         {A : Type} `{SA: Setoid A}
         {B : Type} `{SB: Setoid B},
    Card (sym_Card_Prop prop) A B -> Card prop B A.

Idem but with iff

Lemma Card_sym_iff:
  forall (prop: Card_Prop)
         {A : Type} `{SA: Setoid A}
         {B : Type} `{SB: Setoid B},
    Card (sym_Card_Prop prop) B A <-> Card prop A B.

Card is transitive

Lemma Card_trans:
  forall (prop: Card_Prop)
         {A : Type} `{SA: Setoid A}
         (B : Type) `{SB: Setoid B}
         {C : Type} `{SC: Setoid C},
    Card prop A B ->
    Card prop B C -> Card prop A C.

Larger and Smaller (using the same counting relation) implies Same

Lemma Card_antisym:
  forall {A : Type} `{SA: Setoid A}
         {B : Type} `{SB: Setoid B},
    Card Smaller A B -> Card Larger A B ->
    Card Same A B.

Same implies Larger and Smaller

Lemma Card_antisym_converse:
  forall {A : Type} `{SA: Setoid A}
         {B : Type} `{SB: Setoid B},
    Card Same A B -> Card Smaller A B /\ Card Larger A B.

Same implies symmetric

Lemma Card_Same_sym:
  forall {A : Type} `{SA: Setoid A}
         {B : Type} `{SB: Setoid B},
    Card Same A B -> Card Same B A.

Counting fundamental lemma using ltN

(Inj captures finite Cardinality ordering)

Lemma Inj_le_iff:
forall (m n: nat), Inj (ltN m) (ltN n) <-> m <= n.

Correspondence between ltN size and Card ordering

Lemma Card_smaller_le_iff:
  forall (m n: nat), Card Smaller (ltN m) (ltN n) <-> m <= n.

Lemma Card_larger_ge_iff:
  forall (m n: nat), Card Larger (ltN m) (ltN n) <-> m >= n.

Lemma Card_same_eq_iff:
  forall (m n: nat), Card Same (ltN m) (ltN n) <-> m = n.

For instance, (Num_Card RA Same n) means that RA contains exactly n elements.

Definition Num_Card prop (A:Type) {SA:Setoid A} n := Card prop A (ltN n).

Cartesian Products

Cartesian product is monotonic w.r.t. Cardinality

Lemma Inj_prod:
  forall {A1 : Type} `{SA1: Setoid A1}
         {A2 : Type} `{SA2: Setoid A2}
         {B1 : Type} `{SB1: Setoid B1}
         {B2 : Type} `{SB2: Setoid B2},
    Inj A1 A2 -> Inj B1 B2 -> Inj (A1 *B1) (A2 *B2).

Counting elements in product sets

Lemma Card_prod:
  forall prop
         {A1 : Type} `{SA1: Setoid A1}
         {A2 : Type} `{SA2: Setoid A2}
         {B1 : Type} `{SB1: Setoid B1}
         {B2 : Type} `{SB2: Setoid B2},
    Card prop A1 A2 -> Card prop B1 B2 ->
    Card prop (A1 *B1) (A2 *B2).

Encoding from (ltN m * ltN n) to (ltN (m * n))

Unique and compatible.

Program Definition encode (m n: nat) (ab: ltN m * ltN n): ltN (m * n)
  := let (a, b) := ab in m * b + a.
Obligation 1.

Lemma encode_compat:
  forall (m n: nat),
    Proper fequiv (encode m n).

encode is injective

Lemma encode_unique:
  forall m n ab ab',
    (encode m n ab ) == (encode m n ab') ->
    ab == ab'.

Decoding from (ltN (m * n)) to (ltN m * ltN n)

Unique and compatible.

Program Definition decode (m n: nat) (Hm: m > 0)
        (ab: ltN (m * n)): (ltN m * ltN n) :=
  (modulo (proj1_sig ab) m , div (proj1_sig ab) m ).
Obligation 1.

Obligation 2.

Lemma decode_compat:
  forall (m n: nat) (Hm: m > 0),
    Proper fequiv (decode m n Hm).

decode o encode is identity

Lemma decode_encode:
forall (m n: nat) (Hm: m > 0) (a: ltN m) (b: ltN n),
(decode _ _ Hm (encode _ _ (a ,b ))) == (a , b ).

encode o decode is identity

Lemma encode_decode:
forall (m n: nat) (Hm: m > 0) (ab: ltN (m * n)),
(encode _ _ (decode _ _ Hm ab)) == ab.

Count elements in (ltN (m * n)) and in (ltN n * ltN m)

Lemma Inj_prod_left:
  forall m n , Inj (ltN m * ltN n) (ltN (m * n)).

Lemma Inj_prod_right_non_zero:
  forall m n , m > 0 ->
               Inj (ltN (m * n)) (ltN m * ltN n).

Lemma Inj_prod_right_zero:
  forall n, Inj (ltN (0 * n)) (ltN 0 * ltN n).

Lemma Card_as_many_prod:
  forall m n ,
    Card Same (ltN n * ltN m) (ltN (n * m)).

Lemma Num_Card_prod:
  forall {A : Type} `{SA: Setoid A}
         {B : Type} `{SB: Setoid B},
  forall prop n m,
    Num_Card prop A n -> Num_Card prop B m -> Num_Card prop (A *B) (n * m).

Disjoint sum of relations

Definition coprod_rel (A B: Type) (RA: relation A) (RB: relation B):
  relation (A + B) :=
  fun s1 s2 => match s1,s2 with
                 inl a1,inl a2 => RA a1 a2
               | inr b1,inr b2 => RB b1 b2
               | _ ,_ => False
               end.

Arguments coprod_rel [A B].

Infix "+" := coprod_rel: signature_scope.

Global Instance coprod_rel_equiv:
  forall A B (RA: relation A) (RB: relation B),
    Equivalence RA -> Equivalence RB -> Equivalence (RA + RB).

Global Instance coproduct_setoid
         {A : Type} `{SA: Setoid A}
         {B : Type} `{SB: Setoid B} : Setoid (A +B) :=
  {|equiv:=coprod_rel equiv equiv|}.

Lemma Inj_coprod:
  forall {A1 : Type} `{SA1: Setoid A1}
         {A2 : Type} `{SA2: Setoid A2}
         {B1 : Type} `{SB1: Setoid B1}
         {B2 : Type} `{SB2: Setoid B2},
    Inj A1 A2 -> Inj B1 B2 -> Inj (A1 +B1) (A2 +B2).

Lemma Card_coprod:
  forall prop
         {A1 : Type} `{SA1: Setoid A1}
         {A2 : Type} `{SA2: Setoid A2}
         {B1 : Type} `{SB1: Setoid B1}
         {B2 : Type} `{SB2: Setoid B2},
    Card prop A1 A2 -> Card prop B1 B2 ->
    Card prop (A1 + B1) (A2 + B2).

Encoding / Decoding from (ltN m + ltN n) to ltN (m + n)

Program Definition coprod_encode (m n: nat) (x: ltN m + ltN n): ltN (m + n) :=
  match x with inl (@exist _ _ m' h) => m'+ n | inr (@exist _ _ n' h) => n' end.

Program Definition coprod_decode (m n: nat) (x: ltN (m +n)): ltN m + ltN n :=
  let (k,hk):= x in
  match le_gt_dec n k return ltN m + ltN n with
    left h => inl (k -n) | right h => inr k end.

Global Instance coprod_encode_compat (m n: nat):
  Proper fequiv (coprod_encode m n).

Global Instance coprod_decode_compat (m n: nat):
  Proper fequiv (coprod_decode m n).

Lemma coprod_encode_unique:
  forall n m x x',
    (coprod_encode m n x ) == (coprod_encode m n x') ->
    x == x'.

Lemma coprod_decode_encode:
  forall m n x,
    (coprod_decode m n (coprod_encode m n x)) == x.

Lemma coprod_encode_decode:
  forall m n x,
    (coprod_encode m n (coprod_decode m n x)) == x.

Count elements in (ltN (m + n)) and in (ltN n + ltN m)

Lemma Inj_coprod_left:
  forall (m n: nat),Inj (ltN m + ltN n) (ltN (m + n)).

Lemma Inj_coprod_right:
  forall (m n: nat), Inj (ltN (m + n)) (ltN m + ltN n).

Lemma Card_as_many_coprod:
  forall (m n: nat),Card Same (ltN m + ltN n) (ltN (m + n)).

Lemma Num_Card_prop_coprod:
  forall {A : Type} `{SA: Setoid A}
         {B : Type} `{SB: Setoid B},
  forall prop n m,
    Num_Card prop A n -> Num_Card prop B m -> Num_Card prop (A + B) (n + m).

Infix "+" := coprod_rel: signature_scope.

Lemma Inj_unit_l: Inj unit (ltN 1).

Lemma Inj_unit_r: Inj (ltN 1) unit.

Lemma Num_Card_prop_unit:
  forall prop, Num_Card prop unit 1.

Lemma Inj_empty_l: Inj Empty_set (ltN 0).

Lemma Inj_empty_r: Inj (ltN 0) Empty_set.

Lemma Num_Card_prop_empty:
  forall prop, Num_Card prop Empty_set 0.

Subsets

Section Subsets.

Context {A} `{SA:Setoid A}.

A subset has Smaller Cardinality

Lemma Subset_Num_Card: forall P:A -> Prop, Proper fequiv P ->
Card Smaller (sig P) A.

The set itself is one of its subset, but of same Cardinality

Lemma Trivial_subset_Num_Card: Card Same (sig (fun _:A => True)) A.

The trivially empty subset contains 0 element...

  Lemma Empty_subset_Num_Card:
    Num_Card Same (sig (fun _:A => False)) 0.

  Variables (PA1: A -> Prop) (PA1_compat: Proper fequiv PA1).
  Variables (PA2: A -> Prop) (PA2_compat: Proper fequiv PA2).

SA1 stands for: { x | PA1 x }

Notation SA1 := (sig PA1).

SA2 stands for: { x | PA2 x }

Notation SA2 := (sig PA2).

relation RA restricted between SA1 and SA2

Notation RRA := (fun (a1: SA1) (a2: SA2) =>
(proj1_sig a1 ) == (proj1_sig a2 )).

If for all RA-related elements, x, y, we have (PA1 x) implies (PA2 y), then the subset built from PA1 (RSA1) is smaller than the one from PA2 (RSA2).

Lemma Inj_impl: (equiv ==> impl)%signature PA1 PA2 -> Card Smaller SA1 SA2.

same with Larger

Lemma Inj_impl2: (equiv ==> flip impl)%signature PA1 PA2 -> Card Larger SA1 SA2.

If for all RA-related elements, x, y, we have (PA1 x) <-> (PA2 y), then the subset built from PA1 (RSA1) has same Num_Card than the one from PA2 (RSA2).

  Lemma Inj_iff: PA1 =~= PA2 -> Card Same SA1 SA2.

  Lemma Inj_iff2: PA1 =~= PA2 ->
                  forall n, Num_Card Same SA1 n -> Num_Card Same SA2 n.

n1 and n2 are Num_Card of RSA1 and RSA2

Variable (n1: nat) (hn1: Num_Card Same SA1 n1).
Variable (n2: nat) (hn2: Num_Card Same SA2 n2).

If PA1 implies PA2 through RA-related elements, then n1 is smaller than or equal n2

Lemma Subset_Num_Card_impl_le: (equiv ==> impl)%signature PA1 PA2 -> n1 <= n2.

same for greater

Lemma Subset_Num_Card_flipimpl_ge:
(equiv ==> flip impl)%signature PA1 PA2 -> n1 >= n2.

same for equality

Lemma Subset_Num_Card_iff_eq: PA1 =~= PA2 -> n1 = n2.

A non-empty setoid contains at least 1 element...

Lemma Nonempty_Num_Card: forall a, Proper equiv a -> Num_Card Larger A 1.

A singleton contains exactly one element.

Lemma Singleton_Num_Card:
forall a1, PA1 a1 -> (forall a2, PA1 a2 -> a1 == a2 ) -> Num_Card Same SA1 1.

A singleton contains exactly one element (converse).

Lemma Singleton_Num_Card_unique:
Num_Card Smaller SA1 1 -> forall a1 a2, PA1 a1 -> PA1 a2 -> a1 == a2.

Union of disjoints sets

  Section Disjoint.

    Hypothesis Disjoint: forall x, PA1 x -> PA2 x -> False.

    Notation PA12 := (fun x => PA1 x \/ PA2 x).
    Notation SA12 := {x : A | PA12 x }.

    Global Instance Union_compat: Proper fequiv PA12.

    Lemma Disjoint_union_as_many_coproduct: Card Same SA12 (SA1 + SA2)%type.

    Lemma Disjoint_union_Num_Card: Num_Card Same SA12 (n1 + n2).

  End Disjoint.

End Subsets.

Section Classical_subsets.

  Context {A} `{SA:Setoid A}.

  Variable A_classical: forall a1 a2:A, a1 == a2 \/ ~ a1 == a2.

  Lemma InA_classical : forall a l, InA equiv a l \/ ~InA equiv a l.

Predicate P defines the subset

  Section With_P.

    Variable (P: A -> Prop)
             (P_compat: Proper fequiv P)
             (P_classical: forall (a: A), P a \/ ~P a).

    Notation PL := (fun l a => P a /\ InA equiv a l).

relation RA restricted to SA1

    Notation LSA l := (sig (PL l)).

    Instance PL_compat: Proper (equivlistA equiv ==> fequiv) PL.

    Lemma listP_Num_Card: forall l:list A, exists n , Num_Card Same (LSA l) n.

The set itself is one of its subset, but of same Cardinality

    Lemma Classical_subset_Num_Card:
      forall lA: list A, (forall a:A, P a -> InA equiv a lA ) ->
                         exists cardP , Num_Card Same (sig P) cardP.

  End With_P.

  Lemma Classical_set_Num_Card:
    forall lA: list A, (forall a:A, InA equiv a lA ) ->
                       exists cardL , Num_Card Same A cardL.

End Classical_subsets.

Section Decidable_subsets.

  Context {A} `{SA:Setoid A}.

  Variable (DA: forall a b, {a == b } + {~a == b }).

Predicate P defines the subset

  Section With_P.

    Variable (P: A -> Prop)
             (P_compat: Proper fequiv P)
             (P_dec: forall (a: A), {P a } + {~P a }).

    Notation PL := (fun l a => P a /\ InA equiv a l).

relation RA restricted to SA1

    Notation LSA l := (sig (PL l)).

    Instance PL_dec_compat: Proper (equivlistA equiv ==> fequiv) PL.

    Lemma listP_Num_CardT:
      forall l:list A, { n | Num_Card Same (LSA l) n }.

The set itself is one of its subset, but of same Cardinality

    Lemma Classical_subset_Num_CardT:
      forall lA: list A, (forall a:A, P a -> InA equiv a lA ) ->
                         { cardP | Num_Card Same (sig P) cardP }.

  End With_P.

  Lemma Classical_set_Num_CardT:
    forall lA: list A, (forall a:A, InA equiv a lA ) ->
                       { cardL | Num_Card Same A cardL }.

End Decidable_subsets.

Require Import setoid_ring.Ring.

Section Triangles_and_Trapezoids.

  Variable a b:nat.

  Hypothesis ab_interval: a <=b.

  Notation trapezoid a b cpl :=
    (a<= fst cpl /\ fst cpl <b /\ snd cpl < fst cpl).
  Definition Trapezoid:= {cpl | trapezoid a b cpl }.

  Let count:=((b -a )*(a +(b -1))/2).

  Lemma count_Trapezoid: Num_Card Same Trapezoid count.

End Triangles_and_Trapezoids.

Unset Implicit Arguments.
Close Scope nat_scope.