Add PermutationMaybeNilFlatMap

wouter-swierstra · Jun 29, 2012 · 8144f36 · 8144f36
1 parent b11b14a
commit 8144f36
Showing 1 changed file with 10 additions and 3 deletions.
diff --git a/src/ListLemmas.v b/src/ListLemmas.v
@@ -216,8 +216,7 @@ Proof.
   simpl. apply Permutation_app_head. apply IHPermutation.
   simpl. do 2 rewrite -> app_assoc.
   apply Permutation_app_tail. apply Permutation_app_comm.
-  generalize IHPermutation2.
-  generalize IHPermutation1.
+  generalize IHPermutation1, IHPermutation2.
   apply Permutation_trans.
 Qed.
 
@@ -258,4 +257,12 @@ Qed.
 
 Lemma NotInApp : forall (a : Type) (x : a) (xs ys : list a),
   ~In x xs -> ~In x ys -> ~In x (xs ++ ys).
-Proof. Admitted.
+Proof. Admitted.Lemma PermutationMaybeNilFlatMap : forall (a b c : Type) (ox oy : option c) (g h : a -> list c) (f : c -> list c) (xs ys : list a),
+  Permutation (flat_map g xs) (flat_map h ys) ->
+  Permutation (maybe nil f ox ++ flat_map g xs) (maybe nil f ox ++ flat_map h ys).
+Proof. 
+  intros a b c ox oy g h f xs ys H.
+  destruct ox as [cx |].
+  simpl. apply Permutation_app_head. assumption.
+  simpl. assumption.
+Qed.