add more proofs

Op/M_low_level.v

@@ -536,6 +536,11 @@ repeat (rewrite update_M2_0 ; simpl).
 reflexivity. *)
 Qed.
 
+Theorem M2_fix_eq_M2Z : forall (a:list Z),
+  Zlength a = 31 ->
+  M2_fix 15 a = mult_2 a.
+Proof. convert_length_to_Zlength M2_fix_eq_M2. Qed.
+
 
 Function M3_fix (i : Z) (from : list Z) (to : list Z) {measure Z.to_nat i} : list Z :=
   if (i <=? 0) then to else 
@@ -569,6 +574,14 @@ Proof.
   rewrite Z2Nat.inj_add ; try replace (Z.to_nat 1) with 1%nat by reflexivity ; omega.
 Qed.
 
+Lemma M3_fix_0 : forall (f t:list Z),
+    M3_fix 0 f t = t.
+Proof.
+  intros f t.
+  rewrite M3_fix_equation.
+  destruct (0 <=? 0) eqn:H ; [| compute in H]; go.
+Qed.
+
 Lemma M3_fix_step : forall (i:Z) (f t:list Z),
   0 <= i < 16 -> 
   length t = 16%nat -> 
@@ -595,6 +608,13 @@ assert(forall n, 16 <= (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S n))))))))
 omega.
 Qed.
 
+Lemma M3_fix_stepZ : forall (i:Z) (f t:list Z),
+  0 <= i < 16 -> 
+  Zlength t = 16 -> 
+  Zlength f = 31 ->
+    M3_fix (i + 1) f t = ((take (Z.to_nat i) (M3_fix i f t)) ++ [nth (Z.to_nat i) f 0]) ++ drop (Z.to_nat i + 1) (M3_fix i f t).
+Proof. convert_length_to_Zlength M3_fix_step. Qed.
+
 Theorem M3_fix_eq_M3 : forall (from to:list Z)  ,
   (length from = 31)%nat ->
   (length to = 16)%nat ->
@@ -608,4 +628,18 @@ Proof.
   reflexivity.
 Qed.
 
+Theorem M3_fix_eq_M3Z : forall (from to:list Z)  ,
+  Zlength from = 31 ->
+  Zlength to = 16 ->
+  M3_fix 16 from to = mult_3 from.
+Proof. convert_length_to_Zlength M3_fix_eq_M3. Qed.
+
+Lemma M3_fix_length: forall (i: Z) (f t: list Z),
+  length t = length (M3_fix i f t).
+Proof. intros ; gen i f ; induction t ; intros ; rewrite M3_fix_equation; flatten; go. Qed.
+
+Lemma M3_fix_Zlength: forall (i: Z) (f t: list Z),
+  Zlength t = Zlength (M3_fix i f t).
+Proof. intros; repeat rewrite Zlength_correct; rewrite <- M3_fix_length ; reflexivity. Qed.
+
 Close Scope Z.

makefile

@@ -40,6 +40,7 @@ ifeq ("$(filter $(COQVERSION),$(COQV))","")
 endif
 
 define clean_files
+	$($(1):%.v=$(2)/%.vio) \
 	$($(1):%.v=$(2)/%.vo) \
 	$($(1):%.v=$(2)/.%.aux) \
 	$($(1):%.v=$(2)/.%.vo.aux) \
@@ -81,7 +82,18 @@ else
 	@$(COQC) $(COQFLAGS) $*.v
 endif
 
+%.vio: %.v
+	@echo COQC $*.v
+ifeq ($(TIMINGS), true)
+#	bash -c "wc $*.v >>timings; date +'%s.%N before' >> timings; $(COQC) $(COQFLAGS) $*.v; date +'%s.%N after' >>timings" 2>>timings
+	@bash -c "/bin/time --output=TIMINGS -a -f '%e real, %U user, %S sys, '\"$(shell wc $*.v)\" $(COQC) $(COQFLAGS) $*.v"
+#	echo -n $*.v " " >>TIMINGS; bash -c "/usr/bin/time -o TIMINGS -a $(COQC) $(COQFLAGS) $*.v"
+else
+	@$(COQC) -quick $(COQFLAGS) $*.v
+endif
+
 all: .loadpath $(FILES:.v=.vo)
+quick: .loadpath $(FILES:.v=.vio)
 
 Libs: 		.loadpath $(LIBS_FILES:%.v=Libs/%.vo)
 ListsOp:	.loadpath $(LISTSOP_FILES:%.v=ListsOp/%.vo)
@@ -110,9 +122,27 @@ depend:
 clean:
 	rm -f $(CLEANFILES) .loadpath .depend .nia.cache .lia.cache
 
+# check: quick
+# 	coqtop -schedule-vio2vo
+
+vio2vo: quick
+	$(COQC) $(COQFLAGS) -schedule-vio2vo $(J) $(FILES:%.v=%.vio)
+
+checkproofs:
+	$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(FILES:%.v=%.vio)
+
 count:
 	wc $(FILES)
 
+printenv:
+	@"$(COQTOP)" -config
+	@echo 'CAMLC =	$(CAMLC)'
+	@echo 'CAMLOPTC =	$(CAMLOPTC)'
+	@echo 'PP =	$(PP)'
+	@echo 'COQFLAGS =	$(COQFLAGS)'
+	@echo 'COQLIBINSTALL =	$(COQLIBINSTALL)'
+	@echo 'COQDOCINSTALL =	$(COQDOCINSTALL)'
+
 # The .depend file is divided into two parts, .depend and .depend-concur,
 # in order to work around a limitation in Cygwin about how long one
 # command line can be.  (Or at least, it seems to be a solution to some