Cleanup

wouter-swierstra · Jun 29, 2012 · cfd9e6c · cfd9e6c
1 parent 5040e2a
commit cfd9e6c
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 52 deletions.
diff --git a/src/ListLemmas.v b/src/ListLemmas.v
@@ -289,50 +289,4 @@ Proof.
   induction xs as [| x xs IHxs ].
   constructor.
   constructor.
-Admitted.
-
-(*
-let f := (fun s : stack a => s :: nil) in
-Permutation (flat_map g xs) (flat_map h ys) ->
-Permutation (maybe nil f ox ++ flat_map g xs)) (maybe nil f oy ++ flat_map h ys))
-
-maybe : forall a b, b -> (a -> b) -> option a -> b
-
-TODO: Find some interesting lemmas in this:
-
-
-  Permutation
-     (maybe nil (fun s0 : stack a => s0 :: nil)
-        (getStack (getWorkspace getCurrent)) ++
-      flat_map
-        (fun x : workspace nat l a =>
-         maybe nil (fun s0 : stack a => s0 :: nil) (getStack x))
-        (map (fun x : screen nat l a sd => getWorkspace x) getVisible ++
-         getHidden))
-     (maybe nil (fun s0 : stack a => s0 :: nil) (getStack (getWorkspace s)) ++
-      flat_map
-        (fun x : workspace nat l a =>
-         maybe nil (fun s0 : stack a => s0 :: nil) (getStack x))
-        (map (fun x : screen nat l a sd => getWorkspace x)
-           (deleteBy
-              (fun x y : screen nat l a sd =>
-               proj1_sig (beqsid (getScreen x) (getScreen y))) s getVisible) ++
-         getHidden))
-
-
-   Permutation
-     (maybe nil (fun s0 : stack a => s0 :: nil)
-        (getStack (getWorkspace (getCurrent st))) ++
-      flat_map
-        (fun x : workspace nat l a =>
-         maybe nil (fun s0 : stack a => s0 :: nil) (getStack x))
-        (map (fun x : screen nat l a sd => getWorkspace x) (getVisible st) ++
-         getHidden st))
-     (maybe nil (fun s0 : stack a => s0 :: nil)
-        (getStack (getWorkspace (getCurrent (focusMaster st)))) ++
-      flat_map
-        (fun x : workspace nat l a =>
-         maybe nil (fun s0 : stack a => s0 :: nil) (getStack x))
-        (map (fun x : screen nat l a sd => getWorkspace x)
-           (getVisible (focusMaster st)) ++ getHidden (focusMaster st)))
-*)
+Admitted.
diff --git a/src/Properties.v b/src/Properties.v
@@ -242,11 +242,10 @@ Theorem prop_greedyView_I (l a sd : Set) (n : nat) (s : StackSet.stackSet nat l
     case (find (fun x => proj1_sig 
                  (beqi eq_nat_dec n (getTag (getWorkspace x))))
                  (getVisible s)); auto.
-    destruct s; simpl; auto.
-    destruct s; simpl; auto.
-    destruct getVisible; simpl; auto.
-    unfold invariant; simpl; auto.
-    intros H.
+    destruct s. destruct s.
+    destruct getVisible.
+    unfold invariant.
+    simpl; intros H.
     apply (NoDupFlatMap _ _ _ _ _ H).
     apply Permutation_app_head.
   Admitted.