From f60f9ed58ad2ea12fd293dfbcc015c3ffb827a20 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 26 Mar 2011 00:01:32 -0700 Subject: [PATCH] change fst_zip/snd_zip to axioms --- src/General.v | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) 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 -- 1.7.10.4