Library hydras.Prelude.Sort_spec
Formal specification of list sorting functions
From Coq Require Export List RelationClasses Relations Sorting.Permutation
Sorting.Sorted.
From hydras Require Export DecPreOrder.
From hydras Require Import DecPreOrder_Instances.
Definition sort_fun_t := ∀ A, (A → A → bool) → list A → list A.
Section R_given.
Variables (A: Type)(R : relation A).
Lemma LocallySorted_cons:
∀ l a b, LocallySorted R (b::l) ∧ R a b ↔
LocallySorted R (a::b::l).
Definition sort_rel (l l': list A) :=
LocallySorted R l' ∧ Permutation l l'.
Definition sort_correct (f: list A → list A) : Prop :=
∀ l:list A, sort_rel l (f l).
already defined in DecPreOrder ?
Definition equiv (x y : A) := R x y ∧ R y x.
#[global] Instance equiv_equiv (P: PreOrder R): Equivalence equiv.
Abstract properties TODO: look into StdLib's Order whether some lemmas are already
proved
Lemma forall_weak (H: Transitive R):
∀ (l:list A) (a b:A), R a b →
List.Forall (R b) l →
List.Forall (R a) l.
To remove when it compiles again
Lemma LocallySorted_cons' (Htrans : Transitive R):
∀ l a, List.Forall (R a) l ∧ LocallySorted R l ↔
LocallySorted R (a::l).
Lemma LocallySorted_trans (Htrans : Transitive R):
∀ l a x, LocallySorted R (a::l) → R x a →
LocallySorted R (x::l).
Lemma LocallySorted_inv_In (Htrans : Transitive R):
∀ l x, LocallySorted R (x::l) → ∀ y, In y l → R x y.
End R_given.
Arguments LocallySorted {A} _ _.
#[global] Hint Constructors LocallySorted : lists.
A sort must work on any decidable total pre-order
Definition sort_spec (f : sort_fun_t) :=
∀ (A:Type) (le:relation A) (P:TotalPreOrder le) (dec:RelDecision le) (l:list A),
let l' := f A (fun x y ⇒ bool_decide (le x y)) l in Permutation l l' ∧ LocallySorted le l'.
A prototype for using TotalDecPreOrder type class
Definition sort (f:sort_fun_t)
{A} {le : relation A} {P: TotalPreOrder le} {dec:RelDecision le}
(l: list A) :=
f A (fun x y ⇒ bool_decide (le x y)) l.
stability
Inductive marked {A B : Type}(leA : relation A)(leB : relation B)
{pA : PreOrder leA}
{pB : PreOrder leB}:
list (A × B) → Prop :=
| marked0 : marked leA leB nil
| marked1 : ∀ a b l, marked leA leB l →
(∀ a' b', In (a',b') l →
leA a a' → lt b b') →
marked leA leB ((a,b)::l).
Definition stable (f : sort_fun_t) : Prop :=
∀ (A B : Type) leA leB
(PA : TotalPreOrder leA) (PB : TotalPreOrder leB)
(dec : RelDecision leA) (l : list (A × B)),
marked leA leB l →
marked leA leB (sort f (P:= Total_Inverse_fun
(f:= fst : A × B → A))
l).
for testing only
Fixpoint mark {A}(l:list A)(from:nat) : list (A × nat) :=
match l with
| nil ⇒ nil
| (a::l') ⇒ (a,from)::mark l' (S from)
end.
Definition stable_test (f : sort_fun_t)
{A} {le : relation A}{P: TotalPreOrder le} {dec:RelDecision le}
(l: list A) : list (A × nat) :=
let m := mark l 0 in
sort f (P:= @Total_Inverse_fun (A × nat) A fst le P) m.