Library Interval.Integral.Priority

This file is part of the Coq.Interval library for proving bounds of real-valued expressions in Coq: https://coqinterval.gitlabpages.inria.fr/
Copyright (C) 2007-2019, Inria
This library is governed by the CeCILL-C license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the library under the terms of the CeCILL-C license as circulated by CEA, CNRS and Inria at the following URL: http://www.cecill.info/
As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only with a limited warranty and the library's author, the holder of the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details.

From Coq Require Import List Arith ZArith Psatz.
From mathcomp.ssreflect Require Import ssrfun ssrbool fintype.

Section Permut.

Context {T : Type}.

Fixpoint onth n (l : list T) :=
  match l, n with
  | nil, _None
  | v :: _, OSome v
  | _ :: l, S nonth n l
  end.

Lemma onth_nth :
   n p d,
  n < length p
  onth n p = Some (nth n p d).

Lemma onth_rev :
   n p,
  n < length p
  onth n (rev p) = onth (length p - S n) p.

Lemma onth_app_l :
   n p q,
  n < length p
  onth n (p ++ q) = onth n p.

Lemma onth_app_r :
   n p q,
  length p n
  onth n (p ++ q) = onth (n - length p) q.

Lemma onth_insert :
   n v p,
  onth n p = Some v
   q r, p = q ++ v :: r.

Fixpoint all P (l : list T) :=
  match l with
  | nilTrue
  | h :: tP h all P t
  end.

Inductive permut (p q : list T) : Prop :=
  | Permut (Hl : length p = length q)
     (f : ordinal (length p) ordinal (length p))
     (Hf : injective f)
     (Hpq : n : ordinal _, onth n p = onth (f n) q).

Lemma permut_refl :
   p, permut p p.

Lemma permut_sym :
   p q, permut p q permut q p.

Lemma permut_trans :
   q p r,
  permut p q permut q r permut p r.

Lemma permut_rev :
   p, permut (rev p) p.

Lemma injective_split :
   n n1 n2 n3 n4 (H1 : n = n1 + n2) (H2 : n3 + n4 = n) f,
  injective f
  injective (fun k : ordinal ncast_ord H2 (unsplit (f (split (cast_ord H1 k))))).

Lemma permut_app_l :
   p q r,
  permut q r
  permut (p ++ q) (p ++ r).

Lemma permut_app :
   p q,
  permut (p ++ q) (q ++ p).

Lemma permut_app_r :
   p q r,
  permut p r
  permut (p ++ q) (r ++ q).

Lemma permut_cons :
   h p q,
  permut p q
  permut (h :: p) (h :: q).

Lemma permut_cons_rev :
   h p q,
  permut (h :: p) (h :: q)
  permut p q.

Lemma permut_insert :
   v p q,
  permut (v :: p ++ q) (p ++ v :: q).

Lemma permut_remove :
   v p q,
  permut (v :: p) q
   s, t,
  q = s ++ v :: t permut p (s ++ t).

Lemma all_permut :
   P p q,
  all P p
  permut p q
  all P q.

Lemma fold_right_permut :
   {A} f (acc : A) p q,
  ( u v w, f u (f v w) = f v (f u w))
  permut p q
  fold_right f acc p = fold_right f acc q.

Lemma fold_left_permut :
   {A} f (acc : A) p q,
  ( u v w, f (f u v) w = f (f u w) v)
  permut p q
  fold_left f p acc = fold_left f q acc.

End Permut.

Section Pairing.

Context {T : Type}.

Inductive ptree := PTsome (v : T) (l : list ptree).
Inductive pheap := PHnone | PHsome (t : ptree).

Theorem ptree_ind' :
   P : ptree Prop,
  ( v l, Forall P l P (PTsome v l))
   t, P t.

Fixpoint ptree_to_list (p : ptree) : list T :=
  match p with
  | PTsome v lv :: flat_map ptree_to_list l
  end.

Fixpoint pheap_to_list (p : pheap) : list T :=
  match p with
  | PHnonenil
  | PHsome pptree_to_list p
  end.

Variable le : T T bool.

Definition ptree_meld (p1 p2 : ptree) : ptree :=
  match p1, p2 with
  | PTsome v1 l1, PTsome v2 l2
    if le v1 v2 then PTsome v1 (p2 :: l1)
    else PTsome v2 (p1 :: l2)
  end.

Theorem ptree_meld_correct :
   p1 p2,
  permut (ptree_to_list (ptree_meld p1 p2)) (ptree_to_list p1 ++ ptree_to_list p2).

Definition ptree_insert (p : ptree) (v : T) :=
  ptree_meld p (PTsome v nil).

Theorem ptree_insert_correct :
   p v,
  permut (ptree_to_list (ptree_insert p v)) (v :: ptree_to_list p).

Definition pheap_insert (p : pheap) (v : T) : ptree :=
  match p with
  | PHnonePTsome v nil
  | PHsome pptree_insert p v
  end.

Theorem pheap_insert_correct :
   p v,
  permut (ptree_to_list (pheap_insert p v)) (v :: pheap_to_list p).

Fixpoint ptree_merge_pairs (p1 : ptree) (l : list ptree) : ptree :=
  match l with
  | nilp1
  | p2 :: nilptree_meld p1 p2
  | p2 :: p3 :: l'ptree_meld (ptree_meld p1 p2) (ptree_merge_pairs p3 l')
  end.

Lemma list_ind2 :
   A (P : list A Prop),
  P nil
  ( v, P (v :: nil))
  ( v w l, P l P (v :: w :: l))
   l, P l.

Theorem ptree_merge_pairs_correct :
   p l,
  permut (ptree_to_list (ptree_merge_pairs p l)) (ptree_to_list p ++ flat_map ptree_to_list l).

Definition ptree_pop (p : ptree) : T × pheap :=
  match p with
  | PTsome v l(v,
    match l with
    | nilPHnone
    | lh :: ltPHsome (ptree_merge_pairs lh lt)
    end)
  end.

Theorem ptree_pop_correct :
   p,
  match ptree_pop p with
  | (v, q)permut (v :: pheap_to_list q) (ptree_to_list p)
  end.

Fixpoint ptree_fold {A} (f : A T A) (p : ptree) (acc : A) : A :=
  match p with
  | PTsome v lfold_left (fun acc qptree_fold f q acc) l (f acc v)
  end.

Theorem ptree_fold_correct :
   A (f : A T A) acc p,
  ptree_fold f p acc = fold_left f (ptree_to_list p) acc.

End Pairing.

Arguments ptree : clear implicits.
Arguments pheap : clear implicits.