PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.Tools.NatUtils

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global Imports

From Coq Require Import Setoid.
From Coq Require Import RelationPairs.
From Coq Require Import Lt.
From Coq Require Import Omega.
From Coq Require Import ArithRing.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require NArith.
From Coq Require Import Lia.

Local Imports

From Padec Require Import SetoidUtil.


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 m N (le_S _ _ h)) (exist _ m h :: l)
    end.

  Definition enum: list {m: nat | m < N} := enum_rec _ (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
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 K (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 k h l).

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

Section Sum.

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.

End Sum.

Section Mod.
  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.

End Mod.

Section Min.

look for 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.

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

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

look for min {x | f x=true /\ x < n}, return n if none found
  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)).

  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.

End Min.

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.

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.

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