Library Coq.Lists.SetoidList
Logical relations over lists with respect to a setoid equality
or ordering.
This can be seen as a complement of predicate lelistA and sort
found in Sorting.
Being in a list modulo an equality relation over type A.
An alternative definition of InA.
Lemma InA_alt :
forall x l,
InA x l <->
exists y,
eqA x y /\
In y l.
A list without redundancy modulo the equality over A.
lists with same elements modulo eqA
lists with same elements modulo eqA at the same place
Compatibility of a boolean function with respect to an equality.
Definition compat_bool (
f :
A->bool) :=
forall x y,
eqA x y ->
f x =
f y.
Compatibility of a function upon natural numbers.
Definition compat_nat (
f :
A->nat) :=
forall x y,
eqA x y ->
f x =
f y.
Compatibility of a predicate with respect to an equality.
Definition compat_P (
P :
A->Prop) :=
forall x y,
eqA x y ->
P x ->
P y.
Results concerning lists modulo eqA
Hypothesis eqA_refl :
forall x,
eqA x x.
Hypothesis eqA_sym :
forall x y,
eqA x y ->
eqA y x.
Hypothesis eqA_trans :
forall x y z,
eqA x y ->
eqA y z ->
eqA x z.
Hint Resolve eqA_refl eqA_trans.
Hint Immediate eqA_sym.
Lemma InA_eqA :
forall l x y,
eqA x y ->
InA x l ->
InA y l.
Hint Immediate InA_eqA.
Lemma In_InA :
forall l x,
In x l ->
InA x l.
Hint Resolve In_InA.
Lemma InA_split :
forall l x,
InA x l ->
exists l1,
exists y,
exists l2,
eqA x y /\
l =
l1++y::l2.
Lemma InA_app :
forall l1 l2 x,
InA x (
l1 ++
l2) ->
InA x l1 \/
InA x l2.
Lemma InA_app_iff :
forall l1 l2 x,
InA x (
l1 ++
l2) <->
InA x l1 \/
InA x l2.
Lemma InA_rev :
forall p m,
InA p (
rev m) <->
InA p m.
Results concerning lists modulo eqA and ltA
Variable ltA :
A ->
A ->
Prop.
Hypothesis ltA_trans :
forall x y z,
ltA x y ->
ltA y z ->
ltA x z.
Hypothesis ltA_not_eqA :
forall x y,
ltA x y -> ~
eqA x y.
Hypothesis ltA_eqA :
forall x y z,
ltA x y ->
eqA y z ->
ltA x z.
Hypothesis eqA_ltA :
forall x y z,
eqA x y ->
ltA y z ->
ltA x z.
Hint Resolve ltA_trans.
Hint Immediate ltA_eqA eqA_ltA.
Notation InfA:=(lelistA
ltA).
Notation SortA:=(sort
ltA).
Hint Constructors lelistA sort.
Lemma InfA_ltA :
forall l x y,
ltA x y ->
InfA y l ->
InfA x l.
Lemma InfA_eqA :
forall l x y,
eqA x y ->
InfA y l ->
InfA x l.
Hint Immediate InfA_ltA InfA_eqA.
Lemma SortA_InfA_InA :
forall l x a,
SortA l ->
InfA a l ->
InA x l ->
ltA a x.
Lemma In_InfA :
forall l x, (
forall y,
In y l ->
ltA x y) ->
InfA x l.
Lemma InA_InfA :
forall l x, (
forall y,
InA y l ->
ltA x y) ->
InfA x l.
Lemma InfA_alt :
forall l x,
SortA l -> (
InfA x l <-> (
forall y,
InA y l ->
ltA x y)).
Lemma InfA_app :
forall l1 l2 a,
InfA a l1 ->
InfA a l2 ->
InfA a (
l1++l2).
Lemma SortA_app :
forall l1 l2,
SortA l1 ->
SortA l2 ->
(
forall x y,
InA x l1 ->
InA y l2 ->
ltA x y) ->
SortA (
l1 ++
l2).
Section NoDupA.
Lemma SortA_NoDupA :
forall l,
SortA l ->
NoDupA l.
Lemma NoDupA_app :
forall l l',
NoDupA l ->
NoDupA l' ->
(
forall x,
InA x l ->
InA x l' ->
False) ->
NoDupA (
l++l').
Lemma NoDupA_rev :
forall l,
NoDupA l ->
NoDupA (
rev l).
Lemma NoDupA_split :
forall l l' x,
NoDupA (
l++x::l') ->
NoDupA (
l++l').
Lemma NoDupA_swap :
forall l l' x,
NoDupA (
l++x::l') ->
NoDupA (
x::l++l').
End NoDupA.
Some results about eqlistA
A few things about filter
Compatibility of a two-argument function with respect to two equalities.
Definition compat_op (
f :
A ->
B ->
B) :=
forall (
x x' :
A) (
y y' :
B),
eqA x x' ->
eqB y y' ->
eqB (
f x y) (
f x' y').
Two-argument functions that allow to reorder their arguments.
Definition transpose (
f :
A ->
B ->
B) :=
forall (
x y :
A) (
z :
B),
eqB (
f x (
f y z)) (
f y (
f x z)).
A version of transpose with restriction on where it should hold
ForallList2 : specifies that a certain binary predicate should
always hold when inspecting two different elements of the list.
NoDupA can be written in terms of ForallList2
The following definition is easier to use than ForallList2.
ForallList2 and ForallList2_alt are related, but no completely
equivalent. For proving one implication, we need to know that the
list has no duplicated elements...
... and for proving the other implication, we need to be able
to reverse and adapt relation R modulo eqA.
we know state similar results, but without restriction on transpose.
Variable Tra :transpose
f.
Lemma fold_right_commutes :
forall s1 s2 x,
eqB (
fold_right f i (
s1++x::s2)) (
f x (
fold_right f i (
s1++s2))).
Lemma fold_right_equivlistA :
forall s s',
NoDupA s ->
NoDupA s' ->
equivlistA s s' ->
eqB (
fold_right f i s) (
fold_right f i s').
Lemma fold_right_add :
forall s' s x,
NoDupA s ->
NoDupA s' -> ~
InA x s ->
equivlistA s' (
x::s) ->
eqB (
fold_right f i s') (
f x (
fold_right f i s)).
Section Remove.
Hypothesis eqA_dec :
forall x y :
A, {
eqA x y}+{~(eqA
x y)}.
Lemma InA_dec :
forall x l, {
InA x l } + { ~
InA x l }.
Fixpoint removeA (
x :
A) (
l :
list A){
struct l} :
list A :=
match l with
|
nil =>
nil
|
y::tl =>
if (
eqA_dec x y)
then removeA x tl else y::(removeA
x tl)
end.
Lemma removeA_filter :
forall x l,
removeA x l =
filter (
fun y =>
if eqA_dec x y then false else true)
l.
Lemma removeA_InA :
forall l x y,
InA y (
removeA x l) <->
InA y l /\ ~eqA
x y.
Lemma removeA_NoDupA :
forall s x,
NoDupA s ->
NoDupA (
removeA x s).
Lemma removeA_equivlistA :
forall l l' x,
~InA
x l ->
equivlistA (
x ::
l)
l' ->
equivlistA l (
removeA x l').
End Remove.
End Fold.
End Type_with_equality.
Hint Unfold compat_bool compat_nat compat_P.
Hint Constructors InA NoDupA sort lelistA eqlistA.
Section Find.
Variable A B :
Type.
Variable eqA :
A ->
A ->
Prop.
Hypothesis eqA_sym :
forall x y,
eqA x y ->
eqA y x.
Hypothesis eqA_trans :
forall x y z,
eqA x y ->
eqA y z ->
eqA x z.
Hypothesis eqA_dec :
forall x y :
A, {
eqA x y}+{~(eqA
x y)}.
Fixpoint findA (
f :
A ->
bool) (
l:list (
A*B)) :
option B :=
match l with
|
nil =>
None
| (
a,b)::l =>
if f a then Some b else findA f l
end.
Lemma findA_NoDupA :
forall l a b,
NoDupA (
fun p p' =>
eqA (
fst p) (
fst p'))
l ->
(
InA (
fun p p' =>
eqA (
fst p) (
fst p') /\
snd p =
snd p') (
a,b)
l <->
findA (
fun a' =>
if eqA_dec a a' then true else false)
l =
Some b).
End Find.