diff options
| -rw-r--r-- | doc/changelog/10-standard-library/13671-Vector_to_list.rst | 4 | ||||
| -rw-r--r-- | theories/Vectors/VectorSpec.v | 157 |
2 files changed, 150 insertions, 11 deletions
diff --git a/doc/changelog/10-standard-library/13671-Vector_to_list.rst b/doc/changelog/10-standard-library/13671-Vector_to_list.rst new file mode 100644 index 0000000000..e8404f0c93 --- /dev/null +++ b/doc/changelog/10-standard-library/13671-Vector_to_list.rst @@ -0,0 +1,4 @@ +- **Added:** + Lemmas about vectors related with ``to_list``: ``length_to_list``, ``of_list_to_list_opp``, ``to_list_nil``, ``to_list_cons``, ``to_list_hd``, ``to_list_last``, ``to_list_const``, ``to_list_nth_order``, ``to_list_tl``, ``to_list_append``, ``to_list_rev_append_tail``, ``to_list_rev_append``, ``to_list_rev``, ``to_list_map``, ``to_list_fold_left``, ``to_list_fold_right``, ``to_list_Forall``, ``to_list_Exists``, ``to_list_In``, ``to_list_Forall2`` + (`#13671 <https://github.com/coq/coq/pull/13671>`_, + by Olivier Laurent). diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 10545332bb..227ac00e79 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -14,9 +14,9 @@ Institution: PPS, INRIA 12/2010 *) -Require Fin. +Require Fin List. Require Import VectorDef PeanoNat Eqdep_dec. -Import VectorNotations. +Import VectorNotations EqNotations. Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n} (eq : a1 :: v1 = a2 :: v2) : a1 = a2 /\ v1 = v2 := @@ -233,15 +233,6 @@ assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h). + simpl. intros; now rewrite<- (IHv). Qed. -(** ** Properties of [to_list] *) - -Lemma to_list_of_list_opp {A} (l: list A): to_list (of_list l) = l. -Proof. -induction l. -- reflexivity. -- unfold to_list; simpl. now f_equal. -Qed. - (** ** Properties of [take] *) Lemma take_O : forall {A} {n} le (v:t A n), take 0 le v = []. @@ -387,3 +378,147 @@ intros P n v1 v2; split; induction n as [|n IHn]. (proj1 (Nat.succ_lt_mono _ _) Hi2). now rewrite <- (nth_order_tl _ _ _ _ Hi1), <- (nth_order_tl _ _ _ _ Hi2) in HP. Qed. + +(** ** Properties of [to_list] *) + +Lemma to_list_of_list_opp {A} (l: list A): to_list (of_list l) = l. +Proof. +induction l. +- reflexivity. +- unfold to_list; simpl. now f_equal. +Qed. + +Lemma length_to_list A n (v : t A n): length (to_list v) = n. +Proof. induction v; cbn; auto. Qed. + +Lemma of_list_to_list_opp A n (v: t A n): + rew length_to_list _ _ _ in of_list (to_list v) = v. +Proof. +induction v as [ | h n v IHv ]. +- now apply case0 with (P := fun v => v = nil A). +- replace (length_to_list _ _ (cons _ h _ v)) with (f_equal S (length_to_list _ _ v)) + by apply (UIP_dec Nat.eq_dec). + cbn; rewrite map_subst_map. + f_equal. + now etransitivity; [ | apply IHv]. +Qed. + +Lemma to_list_nil A : to_list (nil A) = List.nil. +Proof. reflexivity. Qed. + +Lemma to_list_cons A h n (v : t A n): + to_list (cons A h n v) = List.cons h (to_list v). +Proof. reflexivity. Qed. + +Lemma to_list_hd A n (v : t A (S n)) d: + hd v = List.hd d (to_list v). +Proof. now rewrite (eta v). Qed. + +Lemma to_list_last A n (v : t A (S n)) d: + last v = List.last (to_list v) d. +Proof. +apply rectS with (v:=v); trivial. +intros a k u IH. +rewrite to_list_cons. +simpl List.last. +now rewrite <- IH, (eta u). +Qed. + +Lemma to_list_const A (a : A) n: + to_list (const a n) = List.repeat a n. +Proof. +induction n as [ | n IHn ]; trivial. +now cbn; rewrite <- IHn. +Qed. + +Lemma to_list_nth_order A n (v : t A n) p (H : p < n) d: + nth_order v H = List.nth p (to_list v) d. +Proof. +revert n v H; induction p as [ | p IHp ]; intros n v H; + (destruct n; [ inversion H | rewrite (eta v) ]); trivial. +now rewrite <- nth_order_tl with (H:=Lt.lt_S_n _ _ H), IHp. +Qed. + +Lemma to_list_tl A n (v : t A (S n)): + to_list (tl v) = List.tl (to_list v). +Proof. now rewrite (eta v). Qed. + +Lemma to_list_append A n m (v1 : t A n) (v2 : t A m): + to_list (append v1 v2) = List.app (to_list v1) (to_list v2). +Proof. +induction v1; simpl; trivial. +now rewrite to_list_cons; f_equal. +Qed. + +Lemma to_list_rev_append_tail A n m (v1 : t A n) (v2 : t A m): + to_list (rev_append_tail v1 v2) = List.rev_append (to_list v1) (to_list v2). +Proof. now revert m v2; induction v1 as [ | ? ? ? IHv1 ]; intros; [ | simpl; rewrite IHv1 ]. Qed. + +Lemma to_list_rev_append A n m (v1 : t A n) (v2 : t A m): + to_list (rev_append v1 v2) = List.rev_append (to_list v1) (to_list v2). +Proof. unfold rev_append; rewrite (Plus.plus_tail_plus n m); apply to_list_rev_append_tail. Qed. + +Lemma to_list_rev A n (v : t A n): + to_list (rev v) = List.rev (to_list v). +Proof. +unfold rev; rewrite (plus_n_O n); unfold eq_rect_r; simpl. +now rewrite to_list_rev_append, List.rev_alt. +Qed. + +Lemma to_list_map A B (f : A -> B) n (v : t A n) : + to_list (map f v) = List.map f (to_list v). +Proof. +induction v; cbn; trivial. +now cbn; f_equal. +Qed. + +Lemma to_list_fold_left A B f (b : B) n (v : t A n): + fold_left f b v = List.fold_left f (to_list v) b. +Proof. now revert b; induction v; cbn. Qed. + +Lemma to_list_fold_right A B f (b : B) n (v : t A n): + fold_right f v b = List.fold_right f b (to_list v). +Proof. now revert b; induction v; cbn; intros; f_equal. Qed. + +Lemma to_list_Forall A P n (v : t A n): + Forall P v <-> List.Forall P (to_list v). +Proof. +split; intros HF. +- induction HF; now constructor. +- remember (to_list v) as l. + revert n v Heql; induction HF; intros n v Heql; + destruct v; inversion Heql; subst; constructor; auto. +Qed. + +Lemma to_list_Exists A P n (v : t A n): + Exists P v <-> List.Exists P (to_list v). +Proof. +split; intros HF. +- induction HF; now constructor. +- remember (to_list v) as l. + revert n v Heql; induction HF; intros n v Heql; + destruct v; inversion Heql; subst; now constructor; auto. +Qed. + +Lemma to_list_In A a n (v : t A n): + In a v <-> List.In a (to_list v). +Proof. +split. +- intros HIn; induction HIn; now constructor. +- induction v; intros HIn; inversion HIn; subst; constructor; auto. +Qed. + +Lemma to_list_Forall2 A B P n (v1 : t A n) (v2 : t B n) : + Forall2 P v1 v2 <-> List.Forall2 P (to_list v1) (to_list v2). +Proof. +split; intros HF. +- induction HF; now constructor. +- remember (to_list v1) as l1. + remember (to_list v2) as l2. + revert n v1 v2 Heql1 Heql2; induction HF; intros n v1 v2 Heql1 Heql2. + + destruct v1; [ | inversion Heql1 ]. + apply case0 with (P0 := fun x => Forall2 P (nil A) x); constructor. + + destruct v1; inversion Heql1; subst. + rewrite (eta v2) in Heql2; inversion Heql2; subst. + rewrite (eta v2); constructor; auto. +Qed. |