diff options
Diffstat (limited to 'theories/Lists/SetoidList.v')
-rw-r--r-- | theories/Lists/SetoidList.v | 189 |
1 files changed, 170 insertions, 19 deletions
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 0fd1693e..b57c3f04 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -11,7 +11,7 @@ Require Export Sorted. Require Export Setoid Basics Morphisms. Set Implicit Arguments. Unset Strict Implicit. - +(* Set Universe Polymorphism. *) (** * Logical relations over lists with respect to a setoid equality or ordering. *) @@ -34,7 +34,7 @@ Hint Constructors InA. of the previous one. Having [InA = Exists eqA] raises too many compatibility issues. For now, we only state the equivalence: *) -Lemma InA_altdef : forall x l, InA x l <-> Exists (eqA x) l. +Lemma InA_altdef : forall x l, InA x l <-> Exists (eqA x) l. Proof. split; induction 1; auto. Qed. Lemma InA_cons : forall x y l, InA x (y::l) <-> eqA x y \/ InA x l. @@ -101,10 +101,12 @@ Proof. split; induction 1; auto. Qed. (** Results concerning lists modulo [eqA] *) Hypothesis eqA_equiv : Equivalence eqA. - -Hint Resolve (@Equivalence_Reflexive _ _ eqA_equiv). -Hint Resolve (@Equivalence_Transitive _ _ eqA_equiv). -Hint Immediate (@Equivalence_Symmetric _ _ eqA_equiv). +Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv). +Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv). +Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv). + +Hint Resolve eqarefl eqatrans. +Hint Immediate eqasym. Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA. @@ -123,7 +125,6 @@ Proof. intros x y z H; revert z; induction H; auto. inversion 1; subst; auto. invlist eqlistA; eauto with *. Qed. - (** Moreover, [eqlistA] implies [equivlistA]. A reverse result will be proved later for sorted list without duplicates. *) @@ -149,7 +150,7 @@ Qed. Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l. Proof. - intros l x y H H'. rewrite <- H; auto. + intros l x y H H'. rewrite <- H. auto. Qed. Hint Immediate InA_eqA. @@ -496,7 +497,7 @@ Proof. apply Hrec; auto. inv; auto. eapply NoDupA_split; eauto. - invlist ForallOrdPairs; auto. + invlist ForallOrdPairs; auto. eapply equivlistA_NoDupA_split; eauto. transitivity (f y (fold_right f i (s1++s2))). apply Comp; auto. reflexivity. @@ -545,6 +546,155 @@ Qed. End Fold. + +Section Fold2. + +Variable B:Type. +Variable eqB:B->B->Prop. +Variable st:Equivalence eqB. +Variable f:A->B->B. +Variable Comp:Proper (eqA==>eqB==>eqB) f. + + +Lemma fold_right_eqlistA2 : + forall s s' (i j:B) (heqij: eqB i j) (heqss': eqlistA s s'), + eqB (fold_right f i s) (fold_right f j s'). +Proof. + intros s. + induction s;intros. + - inversion heqss'. + subst. + simpl. + assumption. + - inversion heqss'. + subst. + simpl. + apply Comp. + + assumption. + + apply IHs;assumption. +Qed. + +Section Fold2_With_Restriction. + +Variable R : A -> A -> Prop. +Hypothesis R_sym : Symmetric R. +Hypothesis R_compat : Proper (eqA==>eqA==>iff) R. + +(** Two-argument functions that allow to reorder their arguments. *) +Definition transpose2 (f : A -> B -> B) := + forall (x y : A) (z z': B), eqB z z' -> eqB (f x (f y z)) (f y (f x z')). + +(** A version of transpose with restriction on where it should hold *) +Definition transpose_restr2 (R : A -> A -> Prop)(f : A -> B -> B) := + forall (x y : A) (z z': B), R x y -> eqB z z' -> eqB (f x (f y z)) (f y (f x z')). + +Variable TraR :transpose_restr2 R f. + +Lemma fold_right_commutes_restr2 : + forall s1 s2 x (i j:B) (heqij: eqB i j), ForallOrdPairs R (s1++x::s2) -> + eqB (fold_right f i (s1++x::s2)) (f x (fold_right f j (s1++s2))). +Proof. +induction s1; simpl; auto; intros. +- apply Comp. + + destruct eqA_equiv. apply Equivalence_Reflexive. + + eapply fold_right_eqlistA2. + * assumption. + * reflexivity. +- transitivity (f a (f x (fold_right f j (s1++s2)))). + apply Comp; auto. + eapply IHs1. + assumption. + invlist ForallOrdPairs; auto. + apply TraR. + invlist ForallOrdPairs; auto. + rewrite Forall_forall in H0; apply H0. + apply in_or_app; simpl; auto. + reflexivity. +Qed. + +Lemma fold_right_equivlistA_restr2 : + forall s s' (i j:B) (heqij: eqB i j), + NoDupA s -> NoDupA s' -> ForallOrdPairs R s -> + eqB i j -> + equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s'). +Proof. + simple induction s. + destruct s'; simpl. + intros. assumption. + unfold equivlistA; intros. + destruct (H3 a). + assert (InA a nil) by auto; inv. + intros x l Hrec s' i j heqij N N' F eqij E; simpl in *. + assert (InA x s') by (rewrite <- (E x); auto). + destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))). + subst s'. + transitivity (f x (fold_right f j (s1++s2))). + - apply Comp; auto. + apply Hrec; auto. + inv; auto. + eapply NoDupA_split; eauto. + invlist ForallOrdPairs; auto. + eapply equivlistA_NoDupA_split; eauto. + - transitivity (f y (fold_right f i (s1++s2))). + + apply Comp; auto. + symmetry. + apply fold_right_eqlistA2. + * assumption. + * reflexivity. + + symmetry. + apply fold_right_commutes_restr2. + symmetry. + assumption. + apply ForallOrdPairs_inclA with (x::l); auto. + red; intros; rewrite E; auto. +Qed. + + +Lemma fold_right_add_restr2 : + forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ForallOrdPairs R s' -> ~ InA x s -> + equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)). +Proof. + intros; apply (@fold_right_equivlistA_restr2 s' (x::s) i j); auto. +Qed. + +End Fold2_With_Restriction. + +Variable Tra :transpose2 f. + +Lemma fold_right_commutes2 : forall s1 s2 i x x', + eqA x x' -> + eqB (fold_right f i (s1++x::s2)) (f x' (fold_right f i (s1++s2))). +Proof. + induction s1;simpl;intros. +- apply Comp;auto. + reflexivity. +- transitivity (f a (f x' (fold_right f i (s1++s2)))); auto. + + apply Comp;auto. + + apply Tra. + reflexivity. +Qed. + +Lemma fold_right_equivlistA2 : + forall s s' i j, NoDupA s -> NoDupA s' -> eqB i j -> + equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s'). +Proof. +red in Tra. +intros; apply fold_right_equivlistA_restr2 with (R:=fun _ _ => True); +repeat red; auto. +apply ForallPairs_ForallOrdPairs; try red; auto. +Qed. + +Lemma fold_right_add2 : + forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ~ InA x s -> + equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)). +Proof. + intros. + replace (f x (fold_right f j s)) with (fold_right f j (x::s)) by auto. + eapply fold_right_equivlistA2;auto. +Qed. + +End Fold2. + Section Remove. Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}. @@ -582,14 +732,14 @@ split. intro; inv. destruct 1; inv. intros. -destruct (eqA_dec x a); simpl; auto. +destruct (eqA_dec x a) as [Heq|Hnot]; simpl; auto. rewrite IHl; split; destruct 1; split; auto. inv; auto. destruct H0; transitivity a; auto. split. intro; inv. split; auto. -contradict n. +contradict Hnot. transitivity y; auto. rewrite (IHl x y) in H0; destruct H0; auto. destruct 1; inv; auto. @@ -633,7 +783,9 @@ Variable ltA : A -> A -> Prop. Hypothesis ltA_strorder : StrictOrder ltA. Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA. -Hint Resolve (@StrictOrder_Transitive _ _ ltA_strorder). +Let sotrans := (@StrictOrder_Transitive _ _ ltA_strorder). + +Hint Resolve sotrans. Notation InfA:=(lelistA ltA). Notation SortA:=(sort ltA). @@ -647,7 +799,7 @@ Proof. Qed. Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA. -Proof. +Proof using eqA_equiv ltA_compat. (* and not ltA_strorder *) intros x x' Hxx' l l' Hll'. inversion_clear Hll'. intuition. @@ -658,7 +810,7 @@ Qed. (** For compatibility, can be deduced from [InfA_compat] *) Lemma InfA_eqA l x y : eqA x y -> InfA y l -> InfA x l. -Proof. +Proof using eqA_equiv ltA_compat. intros H; now rewrite H. Qed. Hint Immediate InfA_ltA InfA_eqA. @@ -759,7 +911,7 @@ Qed. Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A). Proof. repeat red. intros. -rewrite (app_nil_end (rev x)), (app_nil_end (rev y)). +rewrite <- (app_nil_r (rev x)), <- (app_nil_r (rev y)). apply eqlistA_rev_app; auto. Qed. @@ -815,13 +967,12 @@ intros. rewrite filter_In in H; destruct H. eapply SortA_InfA_InA; eauto. Qed. - 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. Proof. -clear ltA ltA_compat ltA_strorder. +clear sotrans ltA ltA_strorder ltA_compat. intros; do 2 rewrite InA_alt; intuition. destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition. destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition. @@ -888,9 +1039,9 @@ split; intros. invlist InA. compute in H2; destruct H2. subst b'. destruct (eqA_dec a a'); intuition. -destruct (eqA_dec a a'); simpl. +destruct (eqA_dec a a') as [HeqA|]; simpl. contradict H0. -revert e H2; clear - eqA_equiv. +revert HeqA H2; clear - eqA_equiv. induction l. intros; invlist InA. intros; invlist InA; auto. |