diff options
Diffstat (limited to 'theories/Lists/SetoidList.v')
| -rw-r--r-- | theories/Lists/SetoidList.v | 101 |
1 files changed, 85 insertions, 16 deletions
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index ec31f37d..0fd1693e 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -6,10 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: SetoidList.v 12919 2010-04-10 16:30:44Z herbelin $ *) - Require Export List. -Require Export Sorting. +Require Export Sorted. Require Export Setoid Basics Morphisms. Set Implicit Arguments. Unset Strict Implicit. @@ -82,6 +80,10 @@ Qed. Definition inclA l l' := forall x, InA x l -> InA x l'. Definition equivlistA l l' := forall x, InA x l <-> InA x l'. +Lemma incl_nil l : inclA nil l. +Proof. intro. intros. inversion H. Qed. +Hint Resolve incl_nil : list. + (** lists with same elements modulo [eqA] at the same place *) Inductive eqlistA : list A -> list A -> Prop := @@ -159,8 +161,7 @@ Qed. 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. + exists l1 y l2, eqA x y /\ l = l1++y::l2. Proof. induction l; intros; inv. exists (@nil A); exists a; exists l; auto. @@ -198,7 +199,29 @@ Proof. rewrite <- In_rev; auto. Qed. +(** Some more facts about InA *) + +Lemma InA_singleton x y : InA x (y::nil) <-> eqA x y. +Proof. + rewrite InA_cons, InA_nil; tauto. +Qed. + +Lemma InA_double_head x y l : + InA x (y :: y :: l) <-> InA x (y :: l). +Proof. + rewrite !InA_cons; tauto. +Qed. + +Lemma InA_permute_heads x y z l : + InA x (y :: z :: l) <-> InA x (z :: y :: l). +Proof. + rewrite !InA_cons; tauto. +Qed. +Lemma InA_app_idem x l : InA x (l ++ l) <-> InA x l. +Proof. + rewrite InA_app_iff; tauto. +Qed. Section NoDupA. @@ -269,7 +292,56 @@ Proof. eapply NoDupA_split; eauto. Qed. -Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y -> +Lemma NoDupA_singleton x : NoDupA (x::nil). +Proof. + repeat constructor. inversion 1. +Qed. + +End NoDupA. + +Section EquivlistA. + +Global Instance equivlistA_cons_proper: + Proper (eqA ==> equivlistA ==> equivlistA) (@cons A). +Proof. + intros ? ? E1 ? ? E2 ?; now rewrite !InA_cons, E1, E2. +Qed. + +Global Instance equivlistA_app_proper: + Proper (equivlistA ==> equivlistA ==> equivlistA) (@app A). +Proof. + intros ? ? E1 ? ? E2 ?. now rewrite !InA_app_iff, E1, E2. +Qed. + +Lemma equivlistA_cons_nil x l : ~ equivlistA (x :: l) nil. +Proof. + intros E. now eapply InA_nil, E, InA_cons_hd. +Qed. + +Lemma equivlistA_nil_eq l : equivlistA l nil -> l = nil. +Proof. + destruct l. + - trivial. + - intros H. now apply equivlistA_cons_nil in H. +Qed. + +Lemma equivlistA_double_head x l : equivlistA (x :: x :: l) (x :: l). +Proof. + intro. apply InA_double_head. +Qed. + +Lemma equivlistA_permute_heads x y l : + equivlistA (x :: y :: l) (y :: x :: l). +Proof. + intro. apply InA_permute_heads. +Qed. + +Lemma equivlistA_app_idem l : equivlistA (l ++ l) l. +Proof. + intro. apply InA_app_idem. +Qed. + +Lemma equivlistA_NoDupA_split 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). Proof. @@ -289,9 +361,7 @@ Proof. rewrite <-H,<-EQN; auto. Qed. -End NoDupA. - - +End EquivlistA. Section Fold. @@ -587,10 +657,9 @@ Proof. Qed. (** For compatibility, can be deduced from [InfA_compat] *) -Lemma InfA_eqA : - forall l x y, eqA x y -> InfA y l -> InfA x l. +Lemma InfA_eqA l x y : eqA x y -> InfA y l -> InfA x l. Proof. - intros l x y H; rewrite H; auto. + intros H; now rewrite H. Qed. Hint Immediate InfA_ltA InfA_eqA. @@ -747,7 +816,7 @@ rewrite filter_In in H; destruct H. eapply SortA_InfA_InA; eauto. Qed. -Implicit Arguments eq [ [A] ]. +Arguments eq {A} x _. Lemma filter_InA : forall f, Proper (eqA==>eq) f -> forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true. @@ -784,9 +853,11 @@ Qed. End Filter. End Type_with_equality. - Hint Constructors InA eqlistA NoDupA sort lelistA. +Arguments equivlistA_cons_nil {A} eqA {eqA_equiv} x l _. +Arguments equivlistA_nil_eq {A} eqA {eqA_equiv} l _. + Section Find. Variable A B : Type. @@ -837,7 +908,6 @@ Qed. End Find. - (** Compatibility aliases. [Proper] is rather to be used directly now.*) Definition compat_bool {A} (eqA:A->A->Prop)(f:A->bool) := @@ -851,4 +921,3 @@ Definition compat_P {A} (eqA:A->A->Prop)(P:A->Prop) := Definition compat_op {A B} (eqA:A->A->Prop)(eqB:B->B->Prop)(f:A->B->B) := Proper (eqA==>eqB==>eqB) f. - |