From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Sat, 26 Mar 2011 07:01:32 +0000 (-0700)
Subject: change fst_zip/snd_zip to axioms
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=f60f9ed58ad2ea12fd293dfbcc015c3ffb827a20;hp=8cb97991a95d5761a28ca94767b8fe637d1411d9

change fst_zip/snd_zip to axioms
---

diff --git a/src/General.v b/src/General.v
index 6cb18be..25856d1 100644
--- a/src/General.v
+++ b/src/General.v
@@ -906,14 +906,9 @@ Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 ->
   reflexivity.
   Qed.
 
-Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
-  admit.
-  Defined.
-
-Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
-  admit.
-  Defined.
-
+(* gee I wish I knew how to get Coq to accept these... *)
+Axiom fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
+Axiom snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
 
 Fixpoint mapM {M}{mon:Monad M}{T}(ml:list (M T)) : M (list T) :=
   match ml with