proposition: Lemma Vector_split_merge {A} : forall sz m n (v : Vector.t A _), snd (Vector_split m _ (snd (Vector_split n (m + sz) v))) = snd (Vector_split (n + m) _ (eq_rect _ _ v _ (plus_assoc _ _ _))).
proof: Proof. induction m; intros; simpl. - induction n; simpl. + simpl in *. apply Eqdep_dec.eq_rect_eq_dec; auto with arith. + simpl in v. assert (forall A n b, exists a b', b = Vector.cons A a n b') by (clear; intros; pattern n, b; apply caseS; eauto). pose proof (H _ _ v); destruct_ex; subst. simpl. pose proof (IHn x0). destruct (Vector_split n sz x0) eqn: ?. simpl in *. rewrite H0. erewrite eq_rect_Vector_cons with (H' := (plus_assoc n 0 sz)); eauto; simpl. destruct (Vector_split (n + 0) sz (eq_rect (n + sz) (Vector.t A) x0 (n + 0 + sz) (plus_assoc n 0 sz))); reflexivity. - assert (n + (S m + sz) = S n + (m + sz)) by omega. fold plus in *; unfold Core.char in *. replace (Vector.tl (snd (Vector_split n (S (m + sz)) v))) with ((snd (Vector_split n (m + sz) (Vector.tl (eq_rect _ _ v _ H))))). + pose proof (IHm n ((Vector.tl (eq_rect (n + (S m + sz)) (t A) v (S n + (m + sz)) H)))). destruct (Vector_split m sz (snd (Vector_split n (m + sz) (Vector.tl (eq_rect (n + (S m + sz)) (t A) v (S n + (m + sz)) H))))) eqn: ?; simpl in *. fold plus in *; rewrite Heqp. simpl; rewrite H0. clear. assert ( S (n + (m + sz)) = S (n + m + sz)) by omega. rewrite <- eq_rect_Vector_tl with (H1 := H0). rewrite <- Equality.transport_pp; simpl; clear. generalize (eq_trans H H0); generalize (NPeano.Nat.add_assoc n (S m) sz); clear H H0. revert sz m v; induction n; simpl. * intros. rewrite <- !Eqdep_dec.eq_rect_eq_dec; auto with arith. destruct (Vector_split m sz (Vector.tl v)) eqn: ?. simpl in *; fold plus in *; rewrite Heqp; reflexivity. * intros. assert (n + S (m + sz) = S (n + m + sz)) by omega. assert (n + S (m + sz) = n + S m + sz) by omega. erewrite eq_rect_Vector_tl with (H' := H0). erewrite eq_rect_Vector_tl with (H' := H). pose proof (IHn _ _ (Vector.tl v) H0 H). destruct ((Vector_split (n + m) sz (Vector.tl (eq_rect (n + S (m + sz)) (t A) (Vector.tl v) (S (n + m + sz)) H)))) eqn: ?. simpl in *; fold plus in *; rewrite Heqp, H1; simpl. destruct (Vector_split (n + S m) sz (eq_rect (n + S (m + sz)) (Vector.t A) (Vector.tl v) (n + S m + sz) H0)) eqn: ?. replace (plus_assoc n (S m) sz) with H0; simpl; eauto. eapply Eqdep_dec.eq_proofs_unicity; intros; omega. + clear. revert H v. assert (forall q (v : t A (n + (S q))) H, snd (Vector_split n q (Vector.tl (eq_rect (n + (S q)) (t A) v (S n + (q)) H))) = Vector.tl (snd (Vector_split n (S (q)) v))). { induction n; simpl; intros. rewrite <- Eqdep_dec.eq_rect_eq_dec; auto with arith. assert (n + S q = S (n + q)) by omega. rewrite eq_rect_Vector_tl with (H' := H0). pose proof (IHn q (Vector.tl v) H0). destruct ((Vector_split n q (Vector.tl (eq_rect (n + S q) (t A) (Vector.tl v) (S n + q) H0)))) eqn: ?. fold plus in *; simpl in *; rewrite Heqp; simpl. rewrite H1. destruct (Vector_split n (S q) (Vector.tl v)); reflexivity. } intros; rewrite H; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedString Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Formats.IPChecksum Fiat.Narcissus.Common.ComposeCheckSum Bedrock.Word