Library Coq.Lists.SetoidList
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.
Inductive InA (x : A) : list A -> Prop :=
| InA_cons_hd : forall y l, eqA x y -> InA x (y :: l)
| InA_cons_tl : forall y l, InA x l -> InA x (y :: l).
Hint Constructors InA.
Lemma InA_cons : forall x y l, InA x (y::l) <-> eqA x y \/ InA x l.
Lemma InA_nil : forall x, InA x nil <-> False.
An alternative definition of InA.
A list without redundancy modulo the equality over A.
Inductive NoDupA : list A -> Prop :=
| NoDupA_nil : NoDupA nil
| NoDupA_cons : forall x l, ~ InA x l -> NoDupA l -> NoDupA (x::l).
Hint Constructors NoDupA.
lists with same elements modulo eqA
lists with same elements modulo eqA at the same place
Inductive eqlistA : list A -> list A -> Prop :=
| eqlistA_nil : eqlistA nil nil
| eqlistA_cons : forall x x' l l',
eqA x x' -> eqlistA l l' -> eqlistA (x::l) (x'::l').
Hint Constructors eqlistA.
Compatibility of a boolean function with respect to an equality.
Compatibility of a function upon natural numbers.
Compatibility of a predicate with respect to an equality.
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
Section EqlistA.
Lemma eqlistA_length : forall l l', eqlistA l l' -> length l = length l'.
Lemma eqlistA_app : forall l1 l1' l2 l2',
eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2').
Lemma eqlistA_rev_app : forall l1 l1',
eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' ->
eqlistA ((rev l1)++l2) ((rev l1')++l2').
Lemma eqlistA_rev : forall l1 l1',
eqlistA l1 l1' -> eqlistA (rev l1) (rev l1').
Lemma SortA_equivlistA_eqlistA : forall l l',
SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'.
End EqlistA.
A few things about filter
Section Filter.
Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l).
Lemma filter_InA : forall f, (compat_bool f) ->
forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
Lemma filter_split :
forall f, (forall x y, f x = true -> f y = false -> ltA x y) ->
forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l.
End Filter.
Section Fold.
Variable B:Type.
Variable eqB:B->B->Prop.
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').
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)).
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
Definition transpose_restr (R : A -> A -> Prop)(f : A -> B -> B) :=
forall (x y : A) (z : B), R x y -> eqB (f x (f y z)) (f y (f x z)).
Variable st:Equivalence eqB.
Variable f:A->B->B.
Variable i:B.
Variable Comp:compat_op f.
Lemma fold_right_eqlistA :
forall s s', eqlistA s s' ->
eqB (fold_right f i s) (fold_right f i s').
Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y ->
NoDupA (x::l) -> NoDupA (l1++y::l2) ->
equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
forall (x y : A) (z : B), R x y -> eqB (f x (f y z)) (f y (f x z)).
Variable st:Equivalence eqB.
Variable f:A->B->B.
Variable i:B.
Variable Comp:compat_op f.
Lemma fold_right_eqlistA :
forall s s', eqlistA s s' ->
eqB (fold_right f i s) (fold_right f i s').
Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y ->
NoDupA (x::l) -> NoDupA (l1++y::l2) ->
equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
ForallList2 : specifies that a certain binary predicate should
always hold when inspecting two different elements of the list.
Inductive ForallList2 (R : A -> A -> Prop) : list A -> Prop :=
| ForallNil : ForallList2 R nil
| ForallCons : forall a l,
(forall b, In b l -> R a b) ->
ForallList2 R l -> ForallList2 R (a::l).
Hint Constructors ForallList2.
NoDupA can be written in terms of ForallList2
Lemma ForallList2_NoDupA : forall l,
ForallList2 (fun a b => ~eqA a b) l <-> NoDupA l.
Lemma ForallList2_impl : forall (R R':A->A->Prop),
(forall a b, R a b -> R' a b) ->
forall l, ForallList2 R l -> ForallList2 R' l.
The following definition is easier to use than ForallList2.
Definition ForallList2_alt (R:A->A->Prop) l :=
forall a b, InA a l -> InA b l -> ~eqA a b -> R a b.
Section Restriction.
Variable R : A -> A -> Prop.
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.
Hypothesis R_sym : forall a b, R a b -> R b a.
Hypothesis R_compat : forall a, compat_P (R a).
Lemma ForallList2_equiv2 : forall l,
ForallList2 R l -> ForallList2_alt R l.
Lemma ForallList2_equiv : forall l, NoDupA l ->
(ForallList2 R l <-> ForallList2_alt R l).
Lemma ForallList2_equivlistA : forall l l', NoDupA l' ->
equivlistA l l' -> ForallList2 R l -> ForallList2 R l'.
Variable TraR :transpose_restr R f.
Lemma fold_right_commutes_restr :
forall s1 s2 x, ForallList2 R (s1++x::s2) ->
eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
Lemma fold_right_equivlistA_restr :
forall s s', NoDupA s -> NoDupA s' -> ForallList2 R s ->
equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
Lemma fold_right_add_restr :
forall s' s x, NoDupA s -> NoDupA s' -> ForallList2 R s' -> ~ InA x s ->
equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
End Restriction.
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.