Library DeltaList: lists of natural numbers with constrained differences


Require Import Arith Omega Wf_nat List.
Import ListNotations.
Set Implicit Arguments.

Increasing lists

Delta p l means that consecutives values in the list l have differences of at least p.

Inductive Delta (p:nat) : list nat → Prop :=
  | Dnil : Delta p []
  | Done n : Delta p [n]
  | Dcons n m l : m+p ≤ n → Delta p (n::l) → Delta p (m::n::l).
Hint Constructors Delta.

In particular:
  • Delta 0 l means that l is increasing
  • Delta 1 l means that l is stricly increasing
  • Delta 2 l implies in addition that no consecutive numbers can occur in l.

Lemma Delta_alt p x l :
 Delta p (x::l) ↔ Delta p l ∧ (∀ y, In y l → x+p ≤ y).

Lemma Delta_inv p x l : Delta p (x::l) → Delta p l.

Lemma Delta_more l p p´ : p ≤ p´ → Delta p´ l → Delta p l.

Lemma Delta_21 l : Delta 2 l → Delta 1 l.

Lemma Delta_nz p k l : 0<k → Delta p (k::l) → ¬In 0 (k::l).
Hint Resolve Delta_21 Delta_inv Delta_nz.

Lemma Delta_low_hd p k k´ l :
 k´≤k → Delta p (k::l) → Delta p (k´::l).

Lemma Delta_21_S x l : Delta 2 (x::l) → Delta 1 (S x::l).
Hint Resolve Delta_21_S.

Lemma Delta_map p p´ f l :
  (∀ x y, x+p ≤ y → f x + p´ ≤ f y) →
  Delta p l → Delta p´ (map f l).

Lemma Delta_pred p l :
 ¬In 0 l → Delta p l → Delta p (map pred l).


Lemma Delta_seq n k : Delta 1 (seq n k).

Lemma Delta_app p x l l´ :
  Delta p l → Delta p (x::l´) →
  (∀ y, In y l → y ≤ x) → Delta p (l++l´).

Lemma Delta_app_inv p l l´ :
 Delta p (l++l´) →
 Delta p l ∧ Delta p l´ ∧
 ∀ x x´, In x l → In x´ l´ → x+p ≤ x´.

Decreasing lists

DeltaRev p l is Delta p (rev l) : it considers differences in the reversed order, leading to decreasing lists

Inductive DeltaRev (p:nat) : list nat → Prop :=
  | DRnil : DeltaRev p []
  | DRone n : DeltaRev p [n]
  | DRcons n m l : n+p ≤ m → DeltaRev p (n::l) → DeltaRev p (m::n::l).
Hint Constructors DeltaRev.

Lemma DeltaRev_alt p x l :
 DeltaRev p (x::l) ↔ DeltaRev p l ∧ (∀ y, In y l → y+p ≤ x).

Lemma DeltaRev_app p x l l´ :
  DeltaRev p l → DeltaRev p (x::l´) →
  (∀ y, In y l → x ≤ y) → DeltaRev p (l++l´).

Lemma DeltaRev_app_inv p l l´ :
 DeltaRev p (l++l´) →
 DeltaRev p l ∧ DeltaRev p l´ ∧
 ∀ x x´, In x l → In x´ l´ → x´+p ≤ x.

Lemma Delta_rev p l : Delta p (rev l) ↔ DeltaRev p l.

Lemma DeltaRev_rev p l : DeltaRev p (rev l) ↔ Delta p l.