LAProof.C.distinct
Require Import VST.floyd.functional_base.
From Stdlib Require Import Relations.Relations Classes.RelationClasses.
Import ListNotations.
Inductive sorted {A} (le: relation A): list A → Prop :=
| sorted_nil:
sorted le nil
| sorted_1: ∀ x,
sorted le (x::nil)
| sorted_cons: ∀ x y l,
le x y → sorted le (y::l) → sorted le (x::y::l).
Lemma sorted_e: ∀ {A} `{d: Inhabitant A} {le: A → A → Prop}
{TR: Transitive le}
(al: list A),
sorted le al → ∀ i j, 0 ≤ i < j → j < Zlength al →
(le (Znth i al) (Znth j al)).
Lemma sorted_i: ∀ {A} `{d: Inhabitant A} (le: A → A → Prop) {TR: Transitive le}
(al: list A),
(∀ i j, 0 ≤ i < j → j < Zlength al → le (Znth i al) (Znth j al)) →
sorted le al.
Lemma le1_sorted: ∀ {A} {le: A → A → Prop}
{TR: Transitive le}
(a b: A) (al: list A),
(le a b) → sorted le (b::al) → sorted le (a::al).
Lemma sorted_app:
∀ {A} {le: A→A→Prop} {TRANS: Transitive le}
pivot al bl,
sorted le al → sorted le bl →
Forall (fun x ⇒ le x pivot) al →
Forall (le pivot) bl →
sorted le (al++bl).
Lemma sorted_app_e3:
∀ {A} {le: relation A} {TRANS: Transitive le}
pivot al bl,
sorted le (al++[pivot]++bl) →
sorted le al ∧ sorted le bl ∧
Forall (fun x ⇒ le x pivot) al ∧
Forall (le pivot) bl.
Lemma sorted_e1: ∀ {t} {Inh: Inhabitant t} {le: relation t} (al: list t), sorted le al →
∀ i,
0 ≤ i < Zlength al-1 → le (Znth i al) (Znth (i+1) al).
Lemma sorted_sublist:
∀ (i j: Z) {A} {InhA: Inhabitant A} le (al: list A),
0 ≤ i ≤ j → j ≤ Zlength al → sorted le al → sorted le (sublist i j al).
Class BoolOrder {A: Type} (R: relation A): Type := {
test : A → A → bool;
test_spec: ∀ x y, reflect (R x y) (test x y)
}.
Arguments test {A} R {BoolOrder}.
Module BPO.
Local Lemma mkteststrictspec {A} {R: relation A} {B: BoolOrder R}{P: PreOrder R}:
let strict x y := R x y ∧ ¬R y x in
let teststrict x y := andb (test R x y) (negb (test R y x)) in
∀ x y : A, reflect (strict x y) (teststrict x y).
Local Lemma StrictOrderstrict {A}{R: relation A}{P: PreOrder R}:
let strict x y := R x y ∧ ¬ R y x in
StrictOrder strict.
Local Lemma mktesteqvspec {A} {R: relation A}{BO: BoolOrder R}:
let eqv x y := R x y ∧ R y x in
let testeqv x y := andb (test R x y) (test R y x) in
∀ x y : A, reflect (eqv x y) (testeqv x y).
Local Lemma mkEqv {A}{R: relation A}{PO: PreOrder R}:
let eqv x y := R x y ∧ R y x in
Equivalence eqv.
Class BoolPreOrder {A: Type} (R: relation A) : Type := {
#[export] BO :: BoolOrder R ;
#[export] PO :: PreOrder R ;
lt : relation A := fun x y ⇒ R x y ∧ ¬R y x;
ltb: A → A → bool := fun x y ⇒ andb (test R x y) (negb (test R y x));
ltb_spec: ∀ x y, reflect (lt x y) (ltb x y) :=
mkteststrictspec;
#[export] Strict :: StrictOrder lt := StrictOrderstrict;
eqv: relation A := fun x y ⇒ R x y ∧ R y x;
eqvb: A → A → bool := fun x y ⇒ andb (test R x y) (test R y x);
eqvbspec: ∀ x y, reflect (eqv x y) (eqvb x y) :=
mktesteqvspec;
Eqv :: Equivalence eqv := mkEqv
}.
Arguments lt [A] [R] {_}.
Arguments ltb [A] [R] {_}.
Arguments eqv [A] [R] {_}.
Arguments eqvb [A] [R] {_}.
End BPO.
Import BPO.
Section SBO.
Context {A: Type} {le: relation A} {SBO: BoolPreOrder le}.
Context {InhA: Inhabitant A}.
Definition count_distinct_aux u v :=
let '(k,x) := u in (if ltb x v then k+1 else k, v).
Definition count_distinct (al: list A) : Z :=
match al with
| nil ⇒ 0
| a::rest ⇒ fst (fold_left count_distinct_aux rest (1,a))
end.
Lemma count_distinct_bound: ∀ el: list A,
0 ≤ count_distinct el ≤ Zlength el.
Lemma count_distinct_bound': ∀ el,
0 < Zlength el →
0 < @count_distinct el.
Lemma count_distinct_mono:
∀ (bl: list A) i,
count_distinct (sublist 0 i bl) ≤ count_distinct bl.
Lemma count_distinct_incr:
∀ (bl: list A) i,
lt (Znth (i-1) bl) (Znth i bl) →
0 < i < Zlength bl →
count_distinct (sublist 0 i bl) + 1 = count_distinct (sublist 0 (i+1) bl).
Lemma count_distinct_incr':
∀ (bl: list A) i,
lt (Znth (i - 1) bl) (Znth i bl) →
0 ≤ i - 1 < Zlength bl - 1 →
count_distinct (sublist 0 i bl) < count_distinct bl.
Lemma count_distinct_noincr:
∀ (al: list A) i,
0 < i < Zlength al →
¬lt (Znth (i-1) al) (Znth i al) →
count_distinct (sublist 0 i al) = count_distinct (sublist 0 (i+1) al).
Lemma count_distinct_aux_mono:
∀ al y u,
fst (fold_left count_distinct_aux al (u, y)) ≥ u.
Lemma eqv_cda: ∀ a x u al,
eqv x a →
fst (fold_left count_distinct_aux al (u, x)) =
fst (fold_left count_distinct_aux al (u, a)).
Lemma count_distinct_aux_lemma:
∀ al y (SOR: sorted le (y::al)) u,
fst (fold_left count_distinct_aux al (u, y)) ≤ u →
Forall (Basics.compose not (lt y)) al.
Lemma count_distinct_1:
∀ al
(SOR: sorted le al),
count_distinct al = 1 →
∀ x y, In x al → In y al → eqv x y.
Lemma count_distinct_range_same:
∀ al g h,
sorted le al → 0 ≤ g < h-1 → h ≤ Zlength al →
BPO.eqv (Znth g al) (Znth (h-1) al) ↔
count_distinct (sublist 0 (g+1) al) = count_distinct (sublist 0 h al).
End SBO.
From Stdlib Require Import Relations.Relations Classes.RelationClasses.
Import ListNotations.
Inductive sorted {A} (le: relation A): list A → Prop :=
| sorted_nil:
sorted le nil
| sorted_1: ∀ x,
sorted le (x::nil)
| sorted_cons: ∀ x y l,
le x y → sorted le (y::l) → sorted le (x::y::l).
Lemma sorted_e: ∀ {A} `{d: Inhabitant A} {le: A → A → Prop}
{TR: Transitive le}
(al: list A),
sorted le al → ∀ i j, 0 ≤ i < j → j < Zlength al →
(le (Znth i al) (Znth j al)).
Lemma sorted_i: ∀ {A} `{d: Inhabitant A} (le: A → A → Prop) {TR: Transitive le}
(al: list A),
(∀ i j, 0 ≤ i < j → j < Zlength al → le (Znth i al) (Znth j al)) →
sorted le al.
Lemma le1_sorted: ∀ {A} {le: A → A → Prop}
{TR: Transitive le}
(a b: A) (al: list A),
(le a b) → sorted le (b::al) → sorted le (a::al).
Lemma sorted_app:
∀ {A} {le: A→A→Prop} {TRANS: Transitive le}
pivot al bl,
sorted le al → sorted le bl →
Forall (fun x ⇒ le x pivot) al →
Forall (le pivot) bl →
sorted le (al++bl).
Lemma sorted_app_e3:
∀ {A} {le: relation A} {TRANS: Transitive le}
pivot al bl,
sorted le (al++[pivot]++bl) →
sorted le al ∧ sorted le bl ∧
Forall (fun x ⇒ le x pivot) al ∧
Forall (le pivot) bl.
Lemma sorted_e1: ∀ {t} {Inh: Inhabitant t} {le: relation t} (al: list t), sorted le al →
∀ i,
0 ≤ i < Zlength al-1 → le (Znth i al) (Znth (i+1) al).
Lemma sorted_sublist:
∀ (i j: Z) {A} {InhA: Inhabitant A} le (al: list A),
0 ≤ i ≤ j → j ≤ Zlength al → sorted le al → sorted le (sublist i j al).
Class BoolOrder {A: Type} (R: relation A): Type := {
test : A → A → bool;
test_spec: ∀ x y, reflect (R x y) (test x y)
}.
Arguments test {A} R {BoolOrder}.
Module BPO.
Local Lemma mkteststrictspec {A} {R: relation A} {B: BoolOrder R}{P: PreOrder R}:
let strict x y := R x y ∧ ¬R y x in
let teststrict x y := andb (test R x y) (negb (test R y x)) in
∀ x y : A, reflect (strict x y) (teststrict x y).
Local Lemma StrictOrderstrict {A}{R: relation A}{P: PreOrder R}:
let strict x y := R x y ∧ ¬ R y x in
StrictOrder strict.
Local Lemma mktesteqvspec {A} {R: relation A}{BO: BoolOrder R}:
let eqv x y := R x y ∧ R y x in
let testeqv x y := andb (test R x y) (test R y x) in
∀ x y : A, reflect (eqv x y) (testeqv x y).
Local Lemma mkEqv {A}{R: relation A}{PO: PreOrder R}:
let eqv x y := R x y ∧ R y x in
Equivalence eqv.
Class BoolPreOrder {A: Type} (R: relation A) : Type := {
#[export] BO :: BoolOrder R ;
#[export] PO :: PreOrder R ;
lt : relation A := fun x y ⇒ R x y ∧ ¬R y x;
ltb: A → A → bool := fun x y ⇒ andb (test R x y) (negb (test R y x));
ltb_spec: ∀ x y, reflect (lt x y) (ltb x y) :=
mkteststrictspec;
#[export] Strict :: StrictOrder lt := StrictOrderstrict;
eqv: relation A := fun x y ⇒ R x y ∧ R y x;
eqvb: A → A → bool := fun x y ⇒ andb (test R x y) (test R y x);
eqvbspec: ∀ x y, reflect (eqv x y) (eqvb x y) :=
mktesteqvspec;
Eqv :: Equivalence eqv := mkEqv
}.
Arguments lt [A] [R] {_}.
Arguments ltb [A] [R] {_}.
Arguments eqv [A] [R] {_}.
Arguments eqvb [A] [R] {_}.
End BPO.
Import BPO.
Section SBO.
Context {A: Type} {le: relation A} {SBO: BoolPreOrder le}.
Context {InhA: Inhabitant A}.
Definition count_distinct_aux u v :=
let '(k,x) := u in (if ltb x v then k+1 else k, v).
Definition count_distinct (al: list A) : Z :=
match al with
| nil ⇒ 0
| a::rest ⇒ fst (fold_left count_distinct_aux rest (1,a))
end.
Lemma count_distinct_bound: ∀ el: list A,
0 ≤ count_distinct el ≤ Zlength el.
Lemma count_distinct_bound': ∀ el,
0 < Zlength el →
0 < @count_distinct el.
Lemma count_distinct_mono:
∀ (bl: list A) i,
count_distinct (sublist 0 i bl) ≤ count_distinct bl.
Lemma count_distinct_incr:
∀ (bl: list A) i,
lt (Znth (i-1) bl) (Znth i bl) →
0 < i < Zlength bl →
count_distinct (sublist 0 i bl) + 1 = count_distinct (sublist 0 (i+1) bl).
Lemma count_distinct_incr':
∀ (bl: list A) i,
lt (Znth (i - 1) bl) (Znth i bl) →
0 ≤ i - 1 < Zlength bl - 1 →
count_distinct (sublist 0 i bl) < count_distinct bl.
Lemma count_distinct_noincr:
∀ (al: list A) i,
0 < i < Zlength al →
¬lt (Znth (i-1) al) (Znth i al) →
count_distinct (sublist 0 i al) = count_distinct (sublist 0 (i+1) al).
Lemma count_distinct_aux_mono:
∀ al y u,
fst (fold_left count_distinct_aux al (u, y)) ≥ u.
Lemma eqv_cda: ∀ a x u al,
eqv x a →
fst (fold_left count_distinct_aux al (u, x)) =
fst (fold_left count_distinct_aux al (u, a)).
Lemma count_distinct_aux_lemma:
∀ al y (SOR: sorted le (y::al)) u,
fst (fold_left count_distinct_aux al (u, y)) ≤ u →
Forall (Basics.compose not (lt y)) al.
Lemma count_distinct_1:
∀ al
(SOR: sorted le al),
count_distinct al = 1 →
∀ x y, In x al → In y al → eqv x y.
Lemma count_distinct_range_same:
∀ al g h,
sorted le al → 0 ≤ g < h-1 → h ≤ Zlength al →
BPO.eqv (Znth g al) (Znth (h-1) al) ↔
count_distinct (sublist 0 (g+1) al) = count_distinct (sublist 0 h al).
End SBO.