moving some lemmas.

Author: Gregory Malecha

theories/Data/LazyList.v

@@ -7,4 +7,13 @@ Section lazy_list.
   | lnil : llist
   | lcons : T -> (unit -> llist) -> llist.
 
-End lazy_list.
+  Fixpoint force (l : llist) : list T :=
+    match l with
+      | lnil => nil
+      | lcons a b => cons a (force (b tt))
+    end.
+
+End lazy_list.
+
+Arguments lnil {T}.
+Arguments lcons {T} _ _.

theories/Data/List.v

@@ -201,6 +201,22 @@ Global Instance Injective_nil_nil T : Injective (nil = @nil T) :=
 auto.
 Defined.
 
+Global Instance Injective_app_cons {T} (a : list T) b c d
+: Injective (a ++ b :: nil = (c ++ d :: nil)) :=
+  { result := a = c /\ b = d }.
+Proof. eapply app_inj_tail. Defined.
+
+Global Instance Injective_app_same_L {T} (a : list T) b c
+: Injective (b ++ a = b ++ c) :=
+  { result := a = c }.
+Proof. apply app_inv_head. Defined.
+
+Global Instance Injective_app_same_R {T} (a : list T) b c
+: Injective (a ++ b = c ++ b) :=
+{ result := a = c }.
+Proof. apply app_inv_tail. Defined.
+
+
 Lemma eq_list_eq
 : forall T (a b : T) (pf : a = b) (F : _ -> Type) val,
     match pf in _ = x return list (F x) with

theories/Data/Prop.v

@@ -77,11 +77,27 @@ Proof.
    intros. setoid_rewrite H. reflexivity.
 Qed.
 
+Lemma forall_impl : forall {T} (P Q : T -> Prop),
+                      (forall x, P x -> Q x) ->
+                      (forall x, P x) -> (forall x, Q x).
+Proof.
+  clear. intuition.
+Qed.
+
+
 (** Exists **)
 Lemma exists_iff : forall T P Q,
                      (forall x,
                         P x <-> Q x) ->
                      ((exists x : T, P x) <-> (exists x : T, Q x)).
 Proof.
    intros. setoid_rewrite H. reflexivity.
-Qed.
+Qed.
+
+Lemma exists_impl : forall {T} (P Q : T -> Prop),
+                      (forall x, P x -> Q x) ->
+                      (exists x, P x) -> (exists x, Q x).
+Proof.
+  clear. intuition.
+  destruct H0; eauto.
+Qed.