PADEC - Coq Library

Library Padec.Tools.NatUtils

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global Imports

From Coq Require Import Setoid.
From Coq Require Import RelationPairs.
From Coq Require Import Lt.
From Coq Require Import Lia.
From Coq Require Import ArithRing.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import BinInt.
From Coq Require Import Nat.
From Coq Require Import Lia.

Local Imports

From Padec Require Import OptionUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import ListUtils.
From Padec Require FoldRight.

Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Natural numbers up to some value N

N is of type nat

Section Nat_lt_n.

Variable (N: nat).

Type of natural numbers from 0 to N-1

  Definition ltN := {n : nat | n < N }.

  Definition ltN_dec: Decider (equiv (A:=ltN)) :=
    fun x y => Peano_dec.eq_nat_dec (proj1_sig x) (proj1_sig y).

Enumeration of all numbers in ltN

  Program Fixpoint enum_rec (k: nat) (h: k <= N) l: list {m : nat | m < N } :=
    match k with
    | O => l
    | S m => enum_rec (le_S_n _ _ (le_S h)) (exist h :: l)
    end.

  Definition enum: list {m : nat | m < N } := enum_rec (PeanoNat.Nat.le_refl N) nil.

  Lemma enum_rec_InA:
    forall k (h: k <= N), forall x, forall l,
          InA equiv x l ->
          InA equiv x (enum_rec h l).

  Lemma enum_rec_enum: forall k (h: k <= N),
      forall x, forall l, proj1_sig x < k -> InA equiv x (enum_rec h l).

  Lemma ltN_in_enum: forall x: {m : nat | m < N }, InA equiv x enum.

End Nat_lt_n.

Additional Facts about ltN n defined as { p:nat | p < n }

n is of type (ltN (S n)), (it is the greatest number in (ltN (S n))

Program Definition ltSN_max (n: nat): ltN (S n) := n.

transform a number x (in ltN) into the same number in (ltN (S n))

Definition ltSN_inj: forall (n: nat), ltN n -> ltN (S n) :=
fun n x =>
@exist _ (fun x => x < S n) (proj1_sig x) (lt_S (proj2_sig x)).

no number from ltSN_inj can be equal to max

Lemma ltSN_inj_not_max:
forall (n: nat) (k: ltN n),
~ (ltSN_inj k ) == (ltSN_max n ).

being the max (n) or coming from inj is decidable

Definition ltSN_inj_max_dec:
  forall (n: nat) (k: ltN (S n)),
    { k': ltN n | k == (ltSN_inj k') }
    +
    { k == (ltSN_max n ) }.
Qed.

ltSN_inj is compatible

Global Instance ltSN_inj_compat:
forall (n: nat), Proper fequiv (@ltSN_inj n).
Qed.

Natural numbers up to some value K

K is of type N

Section N_lt_n.

  Import NArith.

  Open Scope N_scope.

  Variable (K: N).

Type of natural numbers from 0 to N-1

  Definition ltK := {n : N | n < K }.

  Definition ltK_dec: Decider (equiv (A:=ltK)) :=
    fun x y => N.eq_dec (proj1_sig x) (proj1_sig y).
  Import BinNat.N.

Enumeration of all numbers in ltN

  Program Definition Kenum_rec: forall n: N, n <= K -> list ltK -> list ltK :=
    peano_rect (fun k => k <=K -> list ltK -> list ltK) (fun h l => l)
               (fun m F h l => F _ (@exist _ (fun k => k < K) m _ :: l)).

  Definition Kenum:= Kenum_rec (le_refl K) nil.

  Lemma Kenum_rec_InA: forall k (h: k <= K), forall x, forall l,
          InA equiv x l -> InA equiv x (Kenum_rec h l).

  Lemma Kenum_rec_enum: forall k (h: k <= K), forall x, forall l,
          proj1_sig x < k -> InA equiv x (Kenum_rec h l).

  Lemma ltK_in_Kenum: forall x: {m : N | m < K }, InA equiv x Kenum.

  Definition ltK_inj (n:N): option ltK.
  Defined.

  Close Scope N_scope.

End N_lt_n.

Power Composition

Section Power_composition.

  Variable (A: Type).

  Fixpoint power (f: A -> A) (n: nat): A -> A :=
    match n with
    | 0%nat => (fun x => x)
    | S n => (fun x => f (power f n x))
    end.

  Lemma S_power: forall f n x, power f (S n) x = f (power f n x).

  Lemma power_S: forall f n x,
      power f (S n) x = (power f n (f x)).

  Lemma power_add: forall f n p x,
      power f (n +p) x = (power f n (power f p x)).

  Lemma power_mult: forall f n p x,
      power f (n *p) x = (power (power f p) n x ).

  Global Instance power_compat eqA:
    Proper ((eqA ==> eqA ) ==> eq ==> eqA ==> eqA) power.

End Power_composition.

Sum

Section Sum.
Open Scope nat_scope.

sum f x = sum{i = 1 .. x} f i

  Fixpoint sum (f: nat -> nat) (x: nat): nat :=
    match x with
    | O => O
    | S x' => (f x ) + (sum f x')
    end.

  Lemma sum_prod: forall x y, sum (fun _ => y) x = x * y.

  Close Scope nat_scope.

End Sum.

Modulo

Section Mod.
  Open Scope nat_scope.
  Lemma mod_plus_inv':
    forall (a b c: nat),
      a < c -> b < c ->
      exists x , x < c /\ (a + x ) mod c = b /\
                forall x', x' < c -> x' <> x ->
                           (a + x') mod c <> b.

  Lemma mod_plus_inv:
    forall (a b c: nat),
      a < c -> b < c ->
      (exists x , x < c /\ (a + x ) mod c = b )
      /\
      forall x1 x2, x1 < c -> x2 < c ->
                    (a + x1 ) mod c = b ->
                    (a + x2 ) mod c = b -> x1 = x2.

  Lemma arith_even:
    forall n, n > 0 -> exists k , n * (n - 1) = 2 * k.

  Close Scope nat_scope.

End Mod.

Minimum

Section Min.

  Definition is_minimum (f: nat -> bool) (m: nat): Prop :=
    f m = true /\ forall m', m' < m -> f m' = false.

  Lemma is_minimum_unique:
    forall f min1 min2, is_minimum f min1 -> is_minimum f min2 ->
                        min1 = min2.

  Lemma is_minimum_lt:
    forall f1 min1 f2 min2,
      (forall v1, f1 v1 = true -> exists v2 , f2 v2 = true /\ v2 < v1 )
      -> is_minimum f1 min1 -> is_minimum f2 min2 -> min2 < min1.

  Lemma is_minimum_le:
    forall f1 min1 f2 min2,
      (forall v1, f1 v1 = true -> exists v2 , f2 v2 = true /\ v2 <= v1 )
      -> is_minimum f1 min1 -> is_minimum f2 min2 -> min2 <= min1.

Pick min {x | f x=true /\ x < n}, return min_so_far if none found

  Fixpoint min_below_ (f: nat -> bool) (min_so_far n: nat): nat :=
    match n with
    | 0 => min_so_far
    | S n'=> if f n'
             then min_below_ f n' n'
             else min_below_ f min_so_far n'
    end.

  Lemma min_below__spec:
    forall f msf n,
      (min_below_ f msf n = msf /\ forall x, x < n -> f x = false ) \/
      (min_below_ f msf n < n /\ is_minimum f (min_below_ f msf n)).

  Definition min_below (f: nat -> bool) (n: nat): nat := min_below_ f n n.

  Lemma min_below_spec:
    forall f n,
      (min_below f n = n /\ forall x, x < n -> f x = false ) \/
      (min_below f n < n /\ is_minimum f (min_below f n)).

End Min.

Pick argmin:

i.e, pick an element a in a list such that a = argmin { f a, a in l }
where f: A -> nat and l: list A

Section Argmin.
  Variable (A: Type) (f: A -> nat).

  Context {SA: Setoid A}.
  Variable (f_compat: Proper pequiv f).
  Variable (DA: Decider (equiv (A := A))).

  Definition argmin_nat (x y: A): A :=
    if Compare_dec.le_gt_dec (f x) (f y) then x else y.

  Definition argmin (l: list A): option A :=
    match l with
    | nil => None
    | a :: l => Some (fold_right argmin_nat a l)
    end.

  Lemma argmin_nat_spec1:
    forall x y, f (argmin_nat x y) <= f x.

  Lemma argmin_nat_spec2:
    forall x y, f (argmin_nat x y) <= f y.

  Lemma argmin_nat_spec3:
    forall x y, {argmin_nat x y == x } + {argmin_nat x y == y }.

  Lemma argmin_nat_sym:
    forall x y, f x <> f y -> argmin_nat x y = argmin_nat y x.

  Lemma argmin_nat_assoc:
    forall x y z, argmin_nat x (argmin_nat y z) =
                  argmin_nat (argmin_nat x y) z.

  Instance argmin_nat_compat: Proper pequiv argmin_nat.

  Instance argmin_compat: Proper pequiv argmin.

  Definition is_minimum_list (l: list nat) (m: nat): Prop :=
    InA equiv m l /\ forall n, InA equiv n l -> m <= n.

  Instance is_minimum_list_compat: Proper pequiv is_minimum_list.

  Instance is_minimum_list_compat_equivlistA:
    Proper ((equivlistA (equiv (A := nat))) ==> pequiv) is_minimum_list.

  Definition inclA l l': Prop :=
    forall x, InA equiv x l -> InA equiv x l'.

  Lemma filter_inclA:
    forall (g: A -> bool) (l: list A), inclA (filter g l) l.

  Lemma argmin_min1:
    forall l a, argmin l == Some a -> InA equiv a l.

  Lemma fold_right_min0:
    forall a l, f (fold_right argmin_nat a l) <= f a.

  Lemma fold_right_min:
    forall x a l, InA equiv x l ->
                  f (fold_right argmin_nat a l) <= f x.
  Lemma argmin_nat_same:
    forall x y, f x = f y -> argmin_nat x y == x.

  Lemma argmin_nat_same':
    forall x, argmin_nat x x == x.

  Lemma fold_right_min':
    forall a l, ~ InA equiv a l ->
                fold_right argmin_nat a l == a ->
                forall x, InA equiv x l -> f a < f x.

  Lemma argmin_nat_l:
    forall a b, f a <= f b -> argmin_nat a b == a.

  Lemma fold_right_min'':
    forall a b l1 l2,
      ~ InA equiv a l1 ->
      fold_right argmin_nat b (l1 ++ a :: l2) == a ->
      forall n : A, InA equiv n l1 -> f a < f n.

  Lemma argmin_nat_r:
    forall a b, f b < f a -> argmin_nat a b == b.

  Lemma fold_right_min'_conv:
    forall a l, ~ InA equiv a l ->
                (forall x, InA equiv x l -> f a < f x ) ->
                fold_right argmin_nat a l == a.

  Lemma fold_right_min_other:
    forall a b l1 l2,
      f b <= f a ->
      (forall n, InA equiv n l1 -> f n > f b ) ->
      (forall n, InA equiv n l2 -> f b <= f n ) ->
      fold_right argmin_nat a (l1 ++ b :: l2) == b.

  Lemma argmin_None:
    forall l, argmin l = None <-> l = nil.

  Lemma argmin_Some:
    forall b l a,
      argmin (b :: l) == Some a <->
      (a == b /\ ~ InA equiv a l /\
       forall n, InA equiv n l -> f a < f n )
      \/
      (f a <= f b /\
       exists l1 l2 , l == l1 ++ a :: l2 /\ ~ InA equiv a l1 /\
                     (forall n, InA equiv n l1 -> f a < f n ) /\
                     (forall n, InA equiv n l2 -> f a <= f n )).

  Lemma argmin_min2:
    forall l a, argmin l == Some a ->
                forall n, InA equiv n l -> f a <= f n.

End Argmin.

Section Range.

List of consecutive values from 0 to n (n is excluded)

  Fixpoint range (n: nat): list nat :=
    match n with
      0 => nil
    | S m => m :: range m
    end.

Specification

Lemma In_range: forall n x, In x (range n) <-> x < n.

End Range.

Triangular numbers triangle n = sigma(i,i=0..n)

Section Triangular_Numbers.

  Open Scope nat_scope.

  Fixpoint triangle n :=
    match n with
      0 => 0
    | S n => S n + triangle n
    end.

  Lemma triangle_0 : triangle 0 = 0.

  Lemma triangle_S : forall n, triangle (S n) = S n + triangle n.

  Lemma triangle_half_rectangle:
    forall n, 2*triangle n = n *(n +1).

  Lemma triangle_half_rectangle_pn:
    forall n, 2*triangle (n -1) = n *(n -1).

  Lemma triangle_n : forall n, triangle n = n *(n +1)/2.

  Lemma triangle_pn: forall n, triangle (n -1) = n *(n -1)/2.

  Lemma triangle_le: forall n, n <= triangle n.

  Close Scope nat_scope.

End Triangular_Numbers.

Section ltk_inj.

  Variable k: nat.

  Lemma k_non_0: 0<=k -1.

ltk_inj turns a nat into a bounded integer if possible (else truncate sit to 0)

  Definition ltk_inj i : {i | i <= k -1} :=
    match Compare_dec.le_dec i (k -1) with
      left GT => @exist _ _ i GT
    | right _ => @exist _ _ 0 k_non_0
    end.

  Instance ltk_inj_compat:Proper fequiv ltk_inj.

  Lemma proj1_sig_ltk_inj: forall n, n <k -> proj1_sig (ltk_inj n) = n.

End ltk_inj.

Close Scope nat_scope.
Close Scope signature_scope.
Unset Implicit Arguments.