Permalink
Browse files

Merge pull request #2 from norm2782/master

s/PermApp/PermAppL, add PermAppR, remove NoDupAppConsR', cleanup NoDupAppL, remove NoDupAppApp
  • Loading branch information...
2 parents 24a8cfa + cfce5fd commit 38b9e75c5e4999136dbe336b8b30feaaade8f852 @wouter-swierstra committed Jul 3, 2012
Showing with 15 additions and 31 deletions.
  1. +15 −31 src/ListLemmas.v
View
46 src/ListLemmas.v
@@ -110,7 +110,7 @@ Proof.
apply IHPermutation2,IHPermutation1; auto.
Qed.
-Lemma PermApp : forall (a : Type) (xs ys zs : list a),
+Lemma PermAppL : forall (a : Type) (xs ys zs : list a),
Permutation ys zs -> Permutation (xs ++ ys) (xs ++ zs).
Proof.
intros a xs ys zs H1.
@@ -119,6 +119,16 @@ Proof.
induction xs; [auto | simpl; auto].
Qed.
+Lemma PermAppR : forall (a : Type) (xs ys zs : list a),
+ Permutation ys zs -> Permutation (ys ++ xs) (zs ++ xs).
+Proof.
+ intros a xs ys zs H.
+ induction xs as [| x xs IHxs].
+ do 2 rewrite -> app_nil_r; apply H.
+ apply Permutation_add_inside. apply H.
+ apply Permutation_refl.
+Qed.
+
Lemma NoDupConsSwap : forall (a : Type) (xs : list a) (x y : a),
NoDup (x :: y :: xs) -> NoDup (y :: x :: xs).
Proof.
@@ -138,15 +148,6 @@ Proof.
apply H1.
Qed.
-Lemma NoDupAppConsR' : forall (a : Type) (xs ys : list a) (x y : a),
- NoDup (x :: xs ++ y :: ys) -> NoDup (x :: xs ++ ys).
-Proof.
- intros a xs ys x y H.
- rewrite -> app_comm_cons.
- apply (NoDupAppConsR _ (x :: xs) ys y).
- apply H.
-Qed.
-
Lemma NoDupAppR : forall (a : Type) (xs ys : list a),
NoDup (xs ++ ys) -> NoDup ys.
Proof.
@@ -167,14 +168,8 @@ Lemma NoDupAppL : forall (a : Type) (xs ys : list a),
NoDup (xs ++ ys) -> NoDup xs.
Proof.
intros a xs ys H.
- generalize dependent xs.
- induction ys as [| y ys IHys].
- destruct xs as [| x xs].
- intros H; apply H.
- intros H; rewrite -> app_nil_r in H; apply H.
- intros xs H.
- apply IHys.
- apply (NoDupAppConsR _ xs ys y).
+ apply NoDupAppAss in H.
+ apply (NoDupAppR _ ys xs).
apply H.
Qed.
@@ -187,23 +182,12 @@ Proof.
rewrite -> app_ass. reflexivity.
Qed.
-Lemma NoDupAppApp : forall (a : Type) (xs ys zs : list a),
- NoDup (xs ++ ys ++ zs) -> NoDup (ys ++ zs).
-Proof.
- intros a xs ys zs H.
- generalize dependent ys.
- generalize dependent zs.
- induction xs as [| x xs IHxs]. simpl; intros; assumption.
- intros zs ys H. apply IHxs.
- apply (NoDupCons _ (xs ++ ys ++ zs) x). assumption.
-Qed.
-
Lemma NoDupFlatMapCons : forall (a b : Type) (x : a) (xs : list a) (f : a -> list b),
NoDup (flat_map f (x :: xs)) -> NoDup (flat_map f xs).
Proof.
intros a b x xs f H.
destruct xs as [| y ys ]. constructor.
- apply (NoDupAppApp _ (f x) (f y) (flat_map f ys)).
+ apply (NoDupAppR _ (f x) (f y ++ flat_map f ys)).
assumption.
Qed.
@@ -297,4 +281,4 @@ Proof.
intros F; induction xs.
exfalso; apply F; reflexivity.
reflexivity.
- Qed.
+ Qed.

0 comments on commit 38b9e75

Please sign in to comment.