Library MSetFoldWithAbort
- --
Fold with abort for sets
- - --Require Export MSetInterface.
-Require Import ssreflect.
-Require Import MSetWithDups.
-Require Import Int.
-Require Import MSetGenTree MSetAVL MSetRBT.
-Require Import MSetList MSetWeakList.
- -
-
Fold With Abort Operations
- - -- -
-Definition foldWithAbortSpecPred {elt t : Type}
- (In : elt -> t -> Prop)
- (fold : forall {A : Type}, (elt -> A -> A) -> t -> A -> A)
- (foldWithAbort : forall {A : Type}, foldWithAbortType elt t A) : Prop :=
-
- forall
- (A : Type)
-
-
-
- In e1 s -> f_abort e1 st = true ->
- (forall st´ e2, P st st´ ->
- In e2 s -> e2 <> e1 ->
- P st (f e2 st´))) ->
-
-
- -
-Definition foldWithAbortGtSpecPred {elt t : Type}
- (lt : elt -> elt -> Prop)
- (In : elt -> t -> Prop)
- (fold : forall {A : Type}, (elt -> A -> A) -> t -> A -> A)
- (foldWithAbortGt : forall {A : Type}, foldWithAbortType elt t A) : Prop :=
-
- forall
- (A : Type)
-
-
-
-
- In e1 s -> f_gt e1 st = true ->
- (forall st´ e2, P st st´ ->
- In e2 s -> lt e1 e2 ->
- P st (f e2 st´))) ->
-
-
- -
-Definition foldWithAbortGtLtSpecPred {elt t : Type}
- (lt : elt -> elt -> Prop)
- (In : elt -> t -> Prop)
- (fold : forall {A : Type}, (elt -> A -> A) -> t -> A -> A)
- (foldWithAbortGtLt : forall {A : Type}, foldWithAbortGtLtType elt t A) : Prop :=
-
- forall
- (A : Type)
-
-
-
-
- In e1 s -> f_lt e1 st = true ->
- (forall st´ e2, P st st´ ->
- In e2 s -> lt e2 e1 ->
- P st (f e2 st´))) ->
-
-
- In e1 s -> f_gt e1 st = true ->
- (forall st´ e2, P st st´ ->
- In e2 s -> lt e1 e2 ->
- P st (f e2 st´))) ->
-
-
- (lt : elt -> elt -> Prop)
- (In : elt -> t -> Prop)
- (fold : forall {A : Type}, (elt -> A -> A) -> t -> A -> A)
- (foldWithAbortPrecompute : forall {A B : Type}, foldWithAbortPrecomputeType elt t A B) : Prop :=
-
- forall
- (A B : Type)
-
-
-
-
-
-
- In e1 s -> f_lt e1 (f_precompute e1) st = true ->
- (forall st´ e2, P st st´ ->
- In e2 s -> lt e2 e1 ->
- P st (f e2 (f_precompute e2) st´))) ->
-
-
- In e1 s -> f_gt e1 (f_precompute e1) st = true ->
- (forall st´ e2, P st st´ ->
- In e2 s -> lt e1 e2 ->
- P st (f e2 (f_precompute e2) st´))) ->
-
-
Module Types
- --Module Type HasFoldWithAbort (E : OrderedType) (Import C : WSetsOnWithDups E).
- -
- Parameter foldWithAbortPrecompute : forall {A B : Type},
- foldWithAbortPrecomputeType elt t A B.
- -
- Parameter foldWithAbortPrecomputeSpec :
- foldWithAbortPrecomputeSpecPred E.lt In (@fold) (@foldWithAbortPrecompute).
- -
-End HasFoldWithAbort.
- -
-
Derived operations
- - --Module HasFoldWithAbortOps (E : OrderedType) (C : WSetsOnWithDups E)
- (FT : HasFoldWithAbort E C).
- -
- Import FT.
- Import C.
- -
-
- Definition foldWithAbortGtLt {A} f_lt (f : (elt -> A -> A)) f_gt :=
- foldWithAbortPrecompute (fun _ => tt) (fun e _ st => f_lt e st)
- (fun e _ st => f e st) (fun e _ st => f_gt e st).
- -
- Lemma foldWithAbortGtLtSpec :
- foldWithAbortGtLtSpecPred E.lt In (@fold) (@foldWithAbortGtLt).
- -
- Definition foldWithAbortGt {A} (f : (elt -> A -> A)) f_gt :=
- foldWithAbortPrecompute (fun _ => tt) (fun _ _ _ => false)
- (fun e _ st => f e st) (fun e _ st => f_gt e st).
- -
- Lemma foldWithAbortGtSpec :
- foldWithAbortGtSpecPred E.lt In (@fold) (@foldWithAbortGt).
- -
- Definition foldWithAbort {A} (f : (elt -> A -> A)) f_abort :=
- foldWithAbortPrecompute (fun _ => tt) (fun e _ st => f_abort e st)
- (fun e _ st => f e st) (fun e _ st => f_abort e st).
- -
- Lemma foldWithAbortSpec :
- foldWithAbortSpecPred In (@fold) (@foldWithAbort).
- -
-
Specialisations for equality
- -- (f : elt -> B -> A -> A) (f´ : elt -> A -> A) (f_lt f_gt : elt -> B -> A -> bool) (s : t),
-
- (forall e st, In e s -> (f e (f_pre e) st = f´ e st)) ->
-
-
- (forall e1 st,
- In e1 s -> f_lt e1 (f_pre e1) st = true ->
- (forall e2, In e2 s -> E.lt e2 e1 ->
- (f e2 (f_pre e2) st = st))) ->
-
-
- (forall e1 st,
- In e1 s -> f_gt e1 (f_pre e1) st = true ->
- (forall e2, In e2 s -> E.lt e1 e2 ->
- (f e2 (f_pre e2) st = st))) ->
-
- (foldWithAbortPrecompute f_pre f_lt f f_gt s i) = (fold f´ s i).
- Lemma foldWithAbortGtLtSpec_Equal : forall (A : Type) (i : A)
- (f : elt -> A -> A) (f´ : elt -> A -> A) (f_lt f_gt : elt -> A -> bool) (s : t),
-
- (forall e st, In e s -> (f e st = f´ e st)) ->
-
-
- (forall e1 st,
- In e1 s -> f_lt e1 st = true ->
- (forall e2, In e2 s -> E.lt e2 e1 ->
- (f e2 st = st))) ->
-
-
- (forall e1 st,
- In e1 s -> f_gt e1 st = true ->
- (forall e2, In e2 s -> E.lt e1 e2 ->
- (f e2 st = st))) ->
-
- (foldWithAbortGtLt f_lt f f_gt s i) = (fold f´ s i).
- Lemma foldWithAbortGtSpec_Equal : forall (A : Type) (i : A)
- (f : elt -> A -> A) (f´ : elt -> A -> A) (f_gt : elt -> A -> bool) (s : t),
-
- (forall e st, In e s -> (f e st = f´ e st)) ->
-
-
- (forall e1 st,
- In e1 s -> f_gt e1 st = true ->
- (forall e2, In e2 s -> E.lt e1 e2 ->
- (f e2 st = st))) ->
-
- (foldWithAbortGt f f_gt s i) = (fold f´ s i).
- Lemma foldWithAbortSpec_Equal : forall (A : Type) (i : A)
- (f : elt -> A -> A) (f´ : elt -> A -> A) (f_abort : elt -> A -> bool) (s : t),
-
- (forall e st, In e s -> (f e st = f´ e st)) ->
-
-
- (forall e1 st,
- In e1 s -> f_abort e1 st = true ->
- (forall e2, In e2 s -> e1 <> e2 ->
- (f e2 st = st))) ->
-
- (foldWithAbort f f_abort s i) = (fold f´ s i).
-
FoldWithAbortSpecArgs
- -- -
-
- (s : t) (P : elt -> bool) (fwasa : @FoldWithAbortSpecArg A) :=
-
-
- In e1 s -> fwasa_f_lt fwasa e1 (fwasa_f_pre fwasa e1) = true ->
- (forall e2, In e2 s -> E.lt e2 e1 -> (P e2 = false))) /\
-
-
- In e1 s -> fwasa_f_gt fwasa e1 (fwasa_f_pre fwasa e1) = true ->
- (forall e2, In e2 s -> E.lt e1 e2 -> (P e2 = false))).
- -
- -
-
- @foldWithAbortPrecompute t B (fwasa_f_pre fwasa) (fun e p _ => fwasa_f_lt fwasa e p)
- (fun e e_pre s => if fwasa_P´ fwasa e e_pre then add e s else s)
- (fun e p _ => fwasa_f_gt fwasa e p) s empty.
- -
- Lemma filter_with_abort_spec {B} : forall fwasa P s,
- @foldWithAbortSpecArgsForPred B s P fwasa ->
- Proper (E.eq ==> Logic.eq) P ->
- Equal (filter_with_abort fwasa s)
- (filter P s).
-
- foldWithAbortPrecompute (fwasa_f_pre fwasa)
- (fun e p st => match st with None => (fwasa_f_lt fwasa e p) | _ => true end)
- (fun e e_pre st => match st with None =>
- if (fwasa_P´ fwasa e e_pre) then Some e else None | _ => st end)
-
- (fun e p st => match st with None => (fwasa_f_gt fwasa e p) | _ => true end)
- s None.
- -
- Lemma choose_with_abort_spec {B} : forall fwasa P s,
- @foldWithAbortSpecArgsForPred B s P fwasa ->
- Proper (E.eq ==> Logic.eq) P ->
- (match (choose_with_abort fwasa s) with
- | None => (forall e, In e s -> P e = false)
- | Some e => In e s /\ (P e = true)
- end).
-
- match choose_with_abort fwasa s with
- | None => false
- | Some _ => true
- end.
- -
- Lemma exists_with_abort_spec {B} : forall fwasa P s,
- @foldWithAbortSpecArgsForPred B s P fwasa ->
- Proper (E.eq ==> Logic.eq) P ->
- (exists_with_abort fwasa s =
- exists_ P s).
-
- negb (@exists_with_abort B fwasa s).
- -
- Lemma forall_with_abort_spec {B} : forall fwasa s P,
- @foldWithAbortSpecArgsForPred B s P fwasa ->
- Proper (E.eq ==> Logic.eq) P ->
- (forall_with_abort fwasa s =
- for_all (fun e => negb (P e)) s).
- End HasFoldWithAbortOps.
- -
-
- Declare Module E : OrderedType.
- Include WSetsOnWithDups E.
- Include HasFoldWithAbort E.
- Include HasFoldWithAbortOps E.
-End WSetsWithDupsFoldA.
- -
-Module Type WSetsWithFoldA <: WSets.
- Declare Module E : OrderedType.
- Include WSetsOn E.
- Include HasFoldWithAbort E.
- Include HasFoldWithAbortOps E.
-End WSetsWithFoldA.
- -
-Module Type SetsWithFoldA <: Sets.
- Declare Module E : OrderedType.
- Include SetsOn E.
- Include HasFoldWithAbort E.
- Include HasFoldWithAbortOps E.
-End SetsWithFoldA.
- -
-
Implementations
- -GenTree implementation
- - Finally, provide such a fold with abort operation for generic trees. -- (Import Raw:Ops E I)
- (M : MSetGenTree.Props E I Raw).
- -
- Fixpoint foldWithAbort_Raw {A B: Type} (f_pre : E.t -> B) f_lt (f: E.t -> B -> A -> A) f_gt t (base: A) : A :=
- match t with
- | Raw.Leaf => base
- | Raw.Node _ l x r =>
- let x_pre := f_pre x in
- let st0 := if f_lt x x_pre base then base else foldWithAbort_Raw f_pre f_lt f f_gt l base in
- let st1 := f x x_pre st0 in
- let st2 := if f_gt x x_pre st1 then st1 else foldWithAbort_Raw f_pre f_lt f f_gt r st1 in
- st2
- end.
- -
- Lemma foldWithAbort_RawSpec : forall (A B : Type) (i i´ : A) (f_pre : E.t -> B)
- (f : E.t -> B -> A -> A) (f´ : E.t -> A -> A) (f_lt f_gt : E.t -> B -> A -> bool) (s : Raw.tree)
- (P : A -> A -> Prop),
-
- (M.bst s) ->
- Equivalence P ->
- (forall st st´ e, M.In e s -> P st st´ -> P (f e (f_pre e) st) (f e (f_pre e) st´)) ->
- (forall e st, M.In e s -> P (f e (f_pre e) st) (f´ e st)) ->
-
-
- (forall e1 st,
- M.In e1 s -> f_lt e1 (f_pre e1) st = true ->
- (forall st´ e2, P st st´ ->
- M.In e2 s -> E.lt e2 e1 ->
- P st (f e2 (f_pre e2) st´))) ->
-
-
- (forall e1 st,
- M.In e1 s -> f_gt e1 (f_pre e1) st = true ->
- (forall st´ e2, P st st´ ->
- M.In e2 s -> E.lt e1 e2 ->
- P st (f e2 (f_pre e2) st´))) ->
-
- P i i´ ->
- P (foldWithAbort_Raw f_pre f_lt f f_gt s i) (fold f´ s i´).
-End MakeGenTreeFoldA.
- -
-
-Module MakeAVLSetsWithFoldA (X : OrderedType) <: SetsWithFoldA with Module E := X.
- Include MSetAVL.Make X.
- Include MakeGenTreeFoldA X Z_as_Int Raw Raw.
- -
- Definition foldWithAbortPrecompute {A B: Type} f_pre f_lt (f: elt -> B -> A -> A) f_gt t (base: A) : A :=
- foldWithAbort_Raw f_pre f_lt f f_gt (t.(this)) base.
- -
- Lemma foldWithAbortPrecomputeSpec : foldWithAbortPrecomputeSpecPred X.lt In fold (@foldWithAbortPrecompute).
- -
- Include HasFoldWithAbortOps X.
- -
-End MakeAVLSetsWithFoldA.
- -
-
- Include MSetRBT.Make X.
- Include MakeGenTreeFoldA X Color Raw Raw.
- -
- Definition foldWithAbortPrecompute {A B: Type} f_pre f_lt (f: elt -> B -> A -> A) f_gt t (base: A) : A :=
- foldWithAbort_Raw f_pre f_lt f f_gt (t.(this)) base.
- -
- Lemma foldWithAbortPrecomputeSpec : foldWithAbortPrecomputeSpecPred X.lt In fold (@foldWithAbortPrecompute).
- -
- Include HasFoldWithAbortOps X.
- -
-End MakeRBTSetsWithFoldA.
- -
-
- Include MSetList.Make X.
- -
- Fixpoint foldWithAbortRaw {A B: Type} (f_pre : X.t -> B) (f_lt : X.t -> B -> A -> bool)
- (f: X.t -> B -> A -> A) (f_gt : X.t -> B -> A -> bool) (t : list X.t) (acc : A) : A :=
- match t with
- | nil => acc
- | x :: xs => (
- let pre_x := f_pre x in
- let acc := f x (pre_x) acc in
- if (f_gt x pre_x acc) then
- acc
- else
- foldWithAbortRaw f_pre f_lt f f_gt xs acc
- )
- end.
- -
- Definition foldWithAbortPrecompute {A B: Type} f_pre f_lt f f_gt t acc :=
- @foldWithAbortRaw A B f_pre f_lt f f_gt t.(this) acc.
- -
- Lemma foldWithAbortPrecomputeSpec : foldWithAbortPrecomputeSpecPred X.lt In fold (@foldWithAbortPrecompute).
- Include HasFoldWithAbortOps X.
- -
-End MakeListSetsWithFoldA.
- -
-
- Module Raw := MSetWeakList.MakeRaw X.
- Module E := X.
- Include WRaw2SetsOn E Raw.
- -
- Fixpoint foldWithAbortRaw {A B: Type} (f_pre : X.t -> B) (f_lt : X.t -> B -> A -> bool)
- (f: X.t -> B -> A -> A) (f_gt : X.t -> B -> A -> bool) (t : list X.t) (acc : A) : A :=
- match t with
- | nil => acc
- | x :: xs => (
- let pre_x := f_pre x in
- let acc := f x (pre_x) acc in
- if (f_gt x pre_x acc) && (f_lt x pre_x acc) then
- acc
- else
- foldWithAbortRaw f_pre f_lt f f_gt xs acc
- )
- end.
- -
- Definition foldWithAbortPrecompute {A B: Type} f_pre f_lt f f_gt t acc :=
- @foldWithAbortRaw A B f_pre f_lt f f_gt t.(this) acc.
- -
- Lemma foldWithAbortPrecomputeSpec : foldWithAbortPrecomputeSpecPred X.lt In fold (@foldWithAbortPrecompute).
- Include HasFoldWithAbortOps X.
- -
-End MakeWeakListSetsWithFoldA.
- -
-