Library ATBR.MyFSetProperties
This module is an handler through wich we access the standard
library about FSets.
TODO: Coq standard library has evolved in v8.3, so that (parts of) this file might no longer be useful.
We include the most used modules, Facts and OrdProps, but unfortunately, we cannot import neither Props neither EqProps.
In order to acces a lemma in Props, use Module.Props.lemma In order to acces a lemma in EqProps, use Module.EqProps.lemma
We use the abreviation setdec for fsetdec.
We provide a mem_propview tactic, see BoolView.v for more informations about this.
We also provide (new) induction principles about finite sets, which actually coincides with the ones defined in FSetMaps. One slogan here is to use them for reasonning about fold instead of the dependent ones provided by S. Lescuyer in the standard library, and to rewrite lemmas that describe the computational behavior of fold.
Typically, if one want to go through a fold from top (ie, to rewrite fold f acc ((x -> y) :: m) into f x y (fold f acc m)), one will use set_induction_above and rewrite the lemma fold_add_above, while if one want to go through the fold bottom-up (ie, to rewrite fold f acc ((x -> y) :: m) into fold f (f x y acc) m), one will use set_induction_below and rewrite the lemma fold_add_below
TODO: Coq standard library has evolved in v8.3, so that (parts of) this file might no longer be useful.
We include the most used modules, Facts and OrdProps, but unfortunately, we cannot import neither Props neither EqProps.
In order to acces a lemma in Props, use Module.Props.lemma In order to acces a lemma in EqProps, use Module.EqProps.lemma
We use the abreviation setdec for fsetdec.
We provide a mem_propview tactic, see BoolView.v for more informations about this.
We also provide (new) induction principles about finite sets, which actually coincides with the ones defined in FSetMaps. One slogan here is to use them for reasonning about fold instead of the dependent ones provided by S. Lescuyer in the standard library, and to rewrite lemmas that describe the computational behavior of fold.
Typically, if one want to go through a fold from top (ie, to rewrite fold f acc ((x -> y) :: m) into f x y (fold f acc m)), one will use set_induction_above and rewrite the lemma fold_add_above, while if one want to go through the fold bottom-up (ie, to rewrite fold f acc ((x -> y) :: m) into fold f (f x y acc) m), one will use set_induction_below and rewrite the lemma fold_add_below
Require Import FSets.
Require Import Common.
Require Import BoolView.
Module MySetProps (X : FSetInterface.S).
Module EqProps := FSetEqProperties.EqProperties X.
Module Props := EqProps.MP.
Module Facts := Props.FM.
Module OrdProps := FSetProperties.OrdProperties X.
Module Dec := Props.Dec.
Include Facts.
Include OrdProps.
Import X.
Ltac setdec := Dec.fsetdec.
Lemma mem_add : forall x s, mem x (add x s) = true.
Lemma mem_spec : forall x s, reflect (In x s) (mem x s).
Instance mem_type_view : Type_View mem := { type_view := mem_spec }.
Ltac mem_analyse := repeat type_view mem.
Lemma mem_false_not_in: forall x s, mem x s = false <-> ~ In x s.
Hint Rewrite mem_false_not_in : mem_prop.
Hint Rewrite <- mem_iff : mem_prop.
Ltac mem_prop := autorewrite with mem_prop in *.
Hint Rewrite singleton_b union_b add_b mem_add : bool_simpl.
set_induction_below
Section ListViewBelow.
Inductive lvb : t -> Type :=
| lnil : forall s, Equal s empty -> lvb s
| lcons : forall x p, lvb p -> ~In x p -> Below x p -> forall s, Equal s (add x p) -> lvb s.
Program Definition lvb_iter
(P : t -> Type)
(a : forall s, Equal s empty -> P s)
(f : forall p x, P p -> ~In x p -> Below x p -> forall s, Equal s (add x p) -> P s)
:=
fix iter p (q : lvb p) : P p :=
match q in lvb p return P p with
| lnil s hs => a s hs
| lcons x p lvp _ _ _ _ => f p x (iter _ lvp) _ _ _ _
end.
Program Fixpoint lVB s {measure (cardinal s)}: lvb s :=
match min_elt s with
| None => @lnil _ _
| Some x => @lcons x _ (lVB (remove x s)) _ _ _ _
end.
Definition set_induction_below
(P:t->Type)
(a:forall s, Equal s empty ->P s)
(f:forall p x, P p -> ~ In x p -> Below x p -> forall s, Equal s (add x p) -> P s)
(s: t): P s :=
lvb_iter P a f s (lVB s).
End ListViewBelow.
Inductive lvb : t -> Type :=
| lnil : forall s, Equal s empty -> lvb s
| lcons : forall x p, lvb p -> ~In x p -> Below x p -> forall s, Equal s (add x p) -> lvb s.
Program Definition lvb_iter
(P : t -> Type)
(a : forall s, Equal s empty -> P s)
(f : forall p x, P p -> ~In x p -> Below x p -> forall s, Equal s (add x p) -> P s)
:=
fix iter p (q : lvb p) : P p :=
match q in lvb p return P p with
| lnil s hs => a s hs
| lcons x p lvp _ _ _ _ => f p x (iter _ lvp) _ _ _ _
end.
Program Fixpoint lVB s {measure (cardinal s)}: lvb s :=
match min_elt s with
| None => @lnil _ _
| Some x => @lcons x _ (lVB (remove x s)) _ _ _ _
end.
Definition set_induction_below
(P:t->Type)
(a:forall s, Equal s empty ->P s)
(f:forall p x, P p -> ~ In x p -> Below x p -> forall s, Equal s (add x p) -> P s)
(s: t): P s :=
lvb_iter P a f s (lVB s).
End ListViewBelow.
set_induction_above
Section ListViewAbove.
Inductive lva : t -> Type :=
| lnila : forall s, Equal s empty -> lva s
| lconsa : forall x p, lva p -> ~In x p -> Above x p -> forall s, Equal s (add x p) -> lva s.
Section i.
Variable P : t -> Type.
Hypothesis a : forall s, Equal s empty -> P s.
Hypothesis f : forall p x, P p -> ~In x p -> Above x p -> forall s, Equal s (add x p) -> P s.
Lemma lva_iter: forall p, lva p -> P p.
End i.
Program Fixpoint lVA s {measure (cardinal s)}: lva s :=
match max_elt s with
| None => @lnila _ _
| Some x => @lconsa x _ (lVA (remove x s)) _ _ _ _
end.
Definition set_induction_above
(P:t->Type)
(a:forall s, Equal s empty ->P s)
(f:forall p x, P p -> ~ In x p -> Above x p -> forall s, Equal s(add x p) -> P s)
(s: t): P s :=
lva_iter P a f s (lVA s).
End ListViewAbove.
Section MyFold.
Variable A : Type.
Variable eqA : A -> A -> Prop.
Hypothesis equivalence_eqA : Equivalence eqA.
Variable f : E.t -> A -> A.
Variable Hcompat : compat_op E.eq eqA f.
Lemma fold_empty : forall s (i: A), Equal s empty -> eqA (fold f s i) i.
Lemma fold_add_below x p i :
~In x p -> Below x p -> eqA (fold f (add x p) i) (fold f p (f x i)).
Lemma fold_add_above x p i:
~In x p -> Above x p -> eqA (fold f (add x p) i) (f x (fold f p i)).
Inductive lva : t -> Type :=
| lnila : forall s, Equal s empty -> lva s
| lconsa : forall x p, lva p -> ~In x p -> Above x p -> forall s, Equal s (add x p) -> lva s.
Section i.
Variable P : t -> Type.
Hypothesis a : forall s, Equal s empty -> P s.
Hypothesis f : forall p x, P p -> ~In x p -> Above x p -> forall s, Equal s (add x p) -> P s.
Lemma lva_iter: forall p, lva p -> P p.
End i.
Program Fixpoint lVA s {measure (cardinal s)}: lva s :=
match max_elt s with
| None => @lnila _ _
| Some x => @lconsa x _ (lVA (remove x s)) _ _ _ _
end.
Definition set_induction_above
(P:t->Type)
(a:forall s, Equal s empty ->P s)
(f:forall p x, P p -> ~ In x p -> Above x p -> forall s, Equal s(add x p) -> P s)
(s: t): P s :=
lva_iter P a f s (lVA s).
End ListViewAbove.
Section MyFold.
Variable A : Type.
Variable eqA : A -> A -> Prop.
Hypothesis equivalence_eqA : Equivalence eqA.
Variable f : E.t -> A -> A.
Variable Hcompat : compat_op E.eq eqA f.
Lemma fold_empty : forall s (i: A), Equal s empty -> eqA (fold f s i) i.
Lemma fold_add_below x p i :
~In x p -> Below x p -> eqA (fold f (add x p) i) (fold f p (f x i)).
Lemma fold_add_above x p i:
~In x p -> Above x p -> eqA (fold f (add x p) i) (f x (fold f p i)).
Here, we prove the usual dependent induction principles about finite sets
Section fold_rec_bis.
Variable P : t -> A -> Type.
Theorem fold_rec_bis' :
forall (i:A)(s:t),
(forall s s' a a', s[=]s' -> eqA a a' -> P s a -> P s' a') ->
(P empty i ) ->
(forall x a s', In x s -> ~In x s' -> P s' a -> P (add x s') (f x a)) ->
P s (fold f s i).
End fold_rec_bis.
End MyFold.
Variable P : t -> A -> Type.
Theorem fold_rec_bis' :
forall (i:A)(s:t),
(forall s s' a a', s[=]s' -> eqA a a' -> P s a -> P s' a') ->
(P empty i ) ->
(forall x a s', In x s -> ~In x s' -> P s' a -> P (add x s') (f x a)) ->
P s (fold f s i).
End fold_rec_bis.
End MyFold.
Lemmas about elements
Section elements.
Lemma fold_left_id : forall A (s y : list A), List.fold_left (fun acc x => acc ++x::nil) s y = y ++ s.
Lemma elements_fold : forall s, elements s = fold (fun x acc => acc++x::nil) s nil.
End elements.
Lemma fold_left_id : forall A (s y : list A), List.fold_left (fun acc x => acc ++x::nil) s y = y ++ s.
Lemma elements_fold : forall s, elements s = fold (fun x acc => acc++x::nil) s nil.
End elements.
Lemmas about exists_, mainly compat issues, or describing its computationnal behavior
Section exists_.
Variable f : E.t -> bool.
Hypothesis Hcompat : compat_bool (E.eq) f.
Lemma exists_compat : forall x y, Equal x y -> exists_ f x = exists_ f y.
Lemma exists_add : forall x s, ~ In x s ->
exists_ f (add x s) = exists_ f s || f x.
Lemma exists_empty : exists_ f empty = false.
Lemma exists_fold' :
forall x init init',
init = init' ->
exists_ f x || init = fold (fun k acc => f k || acc) x init'.
Lemma exists_fold x:
exists_ f x = fold (fun k acc => f k || acc) x false.
End exists_.
Lemma fold_compat
(f : E.t -> bool -> bool)
(g : E.t -> bool -> bool) x x' init init' :
compat_op E.eq Logic.eq f ->
compat_op E.eq Logic.eq g ->
Equal x x' ->
init = init' ->
(forall e acc, In e x -> f e acc = g e acc) ->
fold f x init = fold g x' init'.
End MySetProps.
Variable f : E.t -> bool.
Hypothesis Hcompat : compat_bool (E.eq) f.
Lemma exists_compat : forall x y, Equal x y -> exists_ f x = exists_ f y.
Lemma exists_add : forall x s, ~ In x s ->
exists_ f (add x s) = exists_ f s || f x.
Lemma exists_empty : exists_ f empty = false.
Lemma exists_fold' :
forall x init init',
init = init' ->
exists_ f x || init = fold (fun k acc => f k || acc) x init'.
Lemma exists_fold x:
exists_ f x = fold (fun k acc => f k || acc) x false.
End exists_.
Lemma fold_compat
(f : E.t -> bool -> bool)
(g : E.t -> bool -> bool) x x' init init' :
compat_op E.eq Logic.eq f ->
compat_op E.eq Logic.eq g ->
Equal x x' ->
init = init' ->
(forall e acc, In e x -> f e acc = g e acc) ->
fold f x init = fold g x' init'.
End MySetProps.