More silly lemmas

Libs/Lists_extended.v

@@ -9,6 +9,23 @@ Lemma nth_drop : forall A (n:nat) (l:list A) (d: A), n < length l -> drop n l =
 Proof. induction n ; destr_boum l. Qed.
 Arguments nth_drop [A] _ _ _ _.
 
+Lemma take_drop_length: forall A (n:nat) (l l':list A),
+  length l = length l' -> length (take n l ++ drop n l') = length l.
+Proof. intros A n l l' Hll'.
+assert(H: n < length l \/ length l <= n) by omega.
+destruct H ; rewrite app_length ; rewrite drop_length ; rewrite <- Hll' ; [rewrite take_length_le|rewrite take_length_ge] ; omega.
+Qed.
+Arguments take_drop_length [A] _ _ _.
+
+Lemma nth_take: forall A (n:nat) (l l':list A) d,
+  n <= length l -> nth n ((take n l) ++ l') d = nth 0 l' d.
+Proof. induction n ; destr_boum l. Qed.
+Arguments nth_take [A] _ _ _ _ _.
+
+Lemma nth_drop_2 : forall A (n:nat) (l:list A) (d:A), n <= length l -> nth n l d = nth 0 (drop n l) d.
+Proof. induction n ; destr_boum l. Qed.
+Arguments nth_drop [A] _ _ _.
+
 (*
 Lemma app_nill_r : forall (A:Type) (l:list A), l ++ nil = l.
 Proof. boum. Qed.

Makefile

@@ -84,7 +84,7 @@ FILES = \
  $(LISTSOP_FILES:%=ListsOp/%) \
  $(OP_FILES:%=Op/%) \
  $(CAR_FILES:%=Car/%) \
- $(SEL_FILES:%=Car/%) \
+ $(SEL_FILES:%=Sel/%) \
 
 ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
 -include $(addsuffix .d,$(FILES))

Sel/Sel25519.v

@@ -11,14 +11,18 @@ Definition list_cswap (b:Z) (p q : list Z) : list Z :=
 
 Lemma list_cswap_nth_true: forall i d p q,
   nth i (list_cswap 1 p q) d = nth i q d.
-Proof.
-  intros. go.
-Qed.
+Proof. go. Qed.
 
 Lemma list_cswap_nth_false: forall i d p q,
   nth i (list_cswap 0 p q) d = nth i p d.
-Proof.
-  intros. go.
-Qed.
+Proof. go. Qed.
+
+Lemma list_cswap_length_eq: forall b p q, length p = length q -> length p = length (list_cswap b p q).
+Proof. intros; unfold list_cswap; destruct (Z.eqb b 0); go. Qed.
+
+Lemma list_cswap_Zlength_eq: forall b p q, Zlength p = Zlength q -> Zlength p = Zlength (list_cswap b p q).
+Proof. intros; unfold list_cswap; destruct (Z.eqb b 0); go. Qed.
+
+
 
 Close Scope Z.
\ No newline at end of file