From accc9fa1f5689d1bf57d3024c4ad293fd10f3617 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 22 Jun 2016 11:47:16 -0700 Subject: Make Coq 8.5 the default target for Fiat-Crypto Instructions for 8.4 build in the README --- coqprime-8.4/Coqprime/ListAux.v | 271 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 271 insertions(+) create mode 100644 coqprime-8.4/Coqprime/ListAux.v (limited to 'coqprime-8.4/Coqprime/ListAux.v') diff --git a/coqprime-8.4/Coqprime/ListAux.v b/coqprime-8.4/Coqprime/ListAux.v new file mode 100644 index 000000000..4ed154685 --- /dev/null +++ b/coqprime-8.4/Coqprime/ListAux.v @@ -0,0 +1,271 @@ + +(*************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(*************************************************************) +(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) +(*************************************************************) + +(********************************************************************** + Aux.v + + Auxillary functions & Theorems + **********************************************************************) +Require Export Coq.Lists.List. +Require Export Coq.Arith.Arith. +Require Export Coqprime.Tactic. +Require Import Coq.Wellfounded.Inverse_Image. +Require Import Coq.Arith.Wf_nat. + +(************************************** + Some properties on list operators: app, map,... +**************************************) + +Section List. +Variables (A : Set) (B : Set) (C : Set). +Variable f : A -> B. + +(************************************** + An induction theorem for list based on length +**************************************) + +Theorem list_length_ind: + forall (P : list A -> Prop), + (forall (l1 : list A), + (forall (l2 : list A), length l2 < length l1 -> P l2) -> P l1) -> + forall (l : list A), P l. +intros P H l; + apply well_founded_ind with ( R := fun (x y : list A) => length x < length y ); + auto. +apply wf_inverse_image with ( R := lt ); auto. +apply lt_wf. +Qed. + +Definition list_length_induction: + forall (P : list A -> Set), + (forall (l1 : list A), + (forall (l2 : list A), length l2 < length l1 -> P l2) -> P l1) -> + forall (l : list A), P l. +intros P H l; + apply well_founded_induction + with ( R := fun (x y : list A) => length x < length y ); auto. +apply wf_inverse_image with ( R := lt ); auto. +apply lt_wf. +Qed. + +Theorem in_ex_app: + forall (a : A) (l : list A), + In a l -> (exists l1 : list A , exists l2 : list A , l = l1 ++ (a :: l2) ). +intros a l; elim l; clear l; simpl; auto. +intros H; case H. +intros a1 l H [H1|H1]; auto. +exists (nil (A:=A)); exists l; simpl; auto. +rewrite H1; auto. +case H; auto; intros l1 [l2 Hl2]; exists (a1 :: l1); exists l2; simpl; auto. +rewrite Hl2; auto. +Qed. + +(************************************** + Properties on app +**************************************) + +Theorem length_app: + forall (l1 l2 : list A), length (l1 ++ l2) = length l1 + length l2. +intros l1; elim l1; simpl; auto. +Qed. + +Theorem app_inv_head: + forall (l1 l2 l3 : list A), l1 ++ l2 = l1 ++ l3 -> l2 = l3. +intros l1; elim l1; simpl; auto. +intros a l H l2 l3 H0; apply H; injection H0; auto. +Qed. + +Theorem app_inv_tail: + forall (l1 l2 l3 : list A), l2 ++ l1 = l3 ++ l1 -> l2 = l3. +intros l1 l2; generalize l1; elim l2; clear l1 l2; simpl; auto. +intros l1 l3; case l3; auto. +intros b l H; absurd (length ((b :: l) ++ l1) <= length l1). +simpl; rewrite length_app; auto with arith. +rewrite <- H; auto with arith. +intros a l H l1 l3; case l3. +simpl; intros H1; absurd (length (a :: (l ++ l1)) <= length l1). +simpl; rewrite length_app; auto with arith. +rewrite H1; auto with arith. +simpl; intros b l0 H0; injection H0. +intros H1 H2; rewrite H2, (H _ _ H1); auto. +Qed. + +Theorem app_inv_app: + forall l1 l2 l3 l4 a, + l1 ++ l2 = l3 ++ (a :: l4) -> + (exists l5 : list A , l1 = l3 ++ (a :: l5) ) \/ + (exists l5 , l2 = l5 ++ (a :: l4) ). +intros l1; elim l1; simpl; auto. +intros l2 l3 l4 a H; right; exists l3; auto. +intros a l H l2 l3 l4 a0; case l3; simpl. +intros H0; left; exists l; injection H0; intros; subst; auto. +intros b l0 H0; case (H l2 l0 l4 a0); auto. +injection H0; auto. +intros [l5 H1]. +left; exists l5; injection H0; intros; subst; auto. +Qed. + +Theorem app_inv_app2: + forall l1 l2 l3 l4 a b, + l1 ++ l2 = l3 ++ (a :: (b :: l4)) -> + (exists l5 : list A , l1 = l3 ++ (a :: (b :: l5)) ) \/ + ((exists l5 , l2 = l5 ++ (a :: (b :: l4)) ) \/ + l1 = l3 ++ (a :: nil) /\ l2 = b :: l4). +intros l1; elim l1; simpl; auto. +intros l2 l3 l4 a b H; right; left; exists l3; auto. +intros a l H l2 l3 l4 a0 b; case l3; simpl. +case l; simpl. +intros H0; right; right; injection H0; split; auto. +rewrite H2; auto. +intros b0 l0 H0; left; exists l0; injection H0; intros; subst; auto. +intros b0 l0 H0; case (H l2 l0 l4 a0 b); auto. +injection H0; auto. +intros [l5 HH1]; left; exists l5; injection H0; intros; subst; auto. +intros [H1|[H1 H2]]; auto. +right; right; split; auto; injection H0; intros; subst; auto. +Qed. + +Theorem same_length_ex: + forall (a : A) l1 l2 l3, + length (l1 ++ (a :: l2)) = length l3 -> + (exists l4 , + exists l5 , + exists b : B , + length l1 = length l4 /\ (length l2 = length l5 /\ l3 = l4 ++ (b :: l5)) ). +intros a l1; elim l1; simpl; auto. +intros l2 l3; case l3; simpl; (try (intros; discriminate)). +intros b l H; exists (nil (A:=B)); exists l; exists b; (repeat (split; auto)). +intros a0 l H l2 l3; case l3; simpl; (try (intros; discriminate)). +intros b l0 H0. +case (H l2 l0); auto. +intros l4 [l5 [b1 [HH1 [HH2 HH3]]]]. +exists (b :: l4); exists l5; exists b1; (repeat (simpl; split; auto)). +rewrite HH3; auto. +Qed. + +(************************************** + Properties on map +**************************************) + +Theorem in_map_inv: + forall (b : B) (l : list A), + In b (map f l) -> (exists a : A , In a l /\ b = f a ). +intros b l; elim l; simpl; auto. +intros tmp; case tmp. +intros a0 l0 H [H1|H1]; auto. +exists a0; auto. +case (H H1); intros a1 [H2 H3]; exists a1; auto. +Qed. + +Theorem in_map_fst_inv: + forall a (l : list (B * C)), + In a (map (fst (B:=_)) l) -> (exists c , In (a, c) l ). +intros a l; elim l; simpl; auto. +intros H; case H. +intros a0 l0 H [H0|H0]; auto. +exists (snd a0); left; rewrite <- H0; case a0; simpl; auto. +case H; auto; intros l1 Hl1; exists l1; auto. +Qed. + +Theorem length_map: forall l, length (map f l) = length l. +intros l; elim l; simpl; auto. +Qed. + +Theorem map_app: forall l1 l2, map f (l1 ++ l2) = map f l1 ++ map f l2. +intros l; elim l; simpl; auto. +intros a l0 H l2; rewrite H; auto. +Qed. + +Theorem map_length_decompose: + forall l1 l2 l3 l4, + length l1 = length l2 -> + map f (app l1 l3) = app l2 l4 -> map f l1 = l2 /\ map f l3 = l4. +intros l1; elim l1; simpl; auto; clear l1. +intros l2; case l2; simpl; auto. +intros; discriminate. +intros a l1 Rec l2; case l2; simpl; clear l2; auto. +intros; discriminate. +intros b l2 l3 l4 H1 H2. +injection H2; clear H2; intros H2 H3. +case (Rec l2 l3 l4); auto. +intros H4 H5; split; auto. +subst; auto. +Qed. + +(************************************** + Properties of flat_map +**************************************) + +Theorem in_flat_map: + forall (l : list B) (f : B -> list C) a b, + In a (f b) -> In b l -> In a (flat_map f l). +intros l g; elim l; simpl; auto. +intros a l0 H a0 b H0 [H1|H1]; apply in_or_app; auto. +left; rewrite H1; auto. +right; apply H with ( b := b ); auto. +Qed. + +Theorem in_flat_map_ex: + forall (l : list B) (f : B -> list C) a, + In a (flat_map f l) -> (exists b , In b l /\ In a (f b) ). +intros l g; elim l; simpl; auto. +intros a H; case H. +intros a l0 H a0 H0; case in_app_or with ( 1 := H0 ); simpl; auto. +intros H1; exists a; auto. +intros H1; case H with ( 1 := H1 ). +intros b [H2 H3]; exists b; simpl; auto. +Qed. + +(************************************** + Properties of fold_left +**************************************) + +Theorem fold_left_invol: + forall (f: A -> B -> A) (P: A -> Prop) l a, + P a -> (forall x y, P x -> P (f x y)) -> P (fold_left f l a). +intros f1 P l; elim l; simpl; auto. +Qed. + +Theorem fold_left_invol_in: + forall (f: A -> B -> A) (P: A -> Prop) l a b, + In b l -> (forall x, P (f x b)) -> (forall x y, P x -> P (f x y)) -> + P (fold_left f l a). +intros f1 P l; elim l; simpl; auto. +intros a1 b HH; case HH. +intros a1 l1 Rec a2 b [V|V] V1 V2; subst; auto. +apply fold_left_invol; auto. +apply Rec with (b := b); auto. +Qed. + +End List. + + +(************************************** + Propertie of list_prod +**************************************) + +Theorem length_list_prod: + forall (A : Set) (l1 l2 : list A), + length (list_prod l1 l2) = length l1 * length l2. +intros A l1 l2; elim l1; simpl; auto. +intros a l H; rewrite length_app; rewrite length_map; rewrite H; auto. +Qed. + +Theorem in_list_prod_inv: + forall (A B : Set) a l1 l2, + In a (list_prod l1 l2) -> + (exists b : A , exists c : B , a = (b, c) /\ (In b l1 /\ In c l2) ). +intros A B a l1 l2; elim l1; simpl; auto; clear l1. +intros H; case H. +intros a1 l1 H1 H2. +case in_app_or with ( 1 := H2 ); intros H3; auto. +case in_map_inv with ( 1 := H3 ); intros b1 [Hb1 Hb2]; auto. +exists a1; exists b1; split; auto. +case H1; auto; intros b1 [c1 [Hb1 [Hb2 Hb3]]]. +exists b1; exists c1; split; auto. +Qed. -- cgit v1.2.3