proposition: Lemma split1'_eq : forall sz sz' w, split1' sz sz' w = split2 sz' sz (eq_rect _ _ w _ (trans_plus_comm _ _)).
proof: Proof. induction sz; simpl; intros. - induction sz'; simpl. + shatter_word w; reflexivity. + destruct (shatter_word_S w) as (?, (w', H)); rewrite H in *; clear H. erewrite wtl_eq_rect_comm. eapply IHsz'. - intros; destruct (shatter_word_S w) as (?, (w', H)); rewrite H in *; clear H. simpl; rewrite IHsz; clear. generalize (eq_ind_r (fun n : nat => S n = sz' + S sz) (trans_S_comm sz' sz) (trans_plus_comm sz sz')). generalize (trans_plus_comm sz sz'). fold (plus sz sz'). revert x sz w'; induction sz'; simpl. + intros ? ?; rewrite <- (plus_n_O sz); simpl. intros. pattern e. apply K_dec_set; eauto; try decide equality. pattern e0. apply K_dec_set; eauto; try decide equality. unfold eq_rect; simpl. rewrite <- word_split_SW; reflexivity. + intros ? ?. rewrite <- !trans_S_comm. rewrite trans_plus_comm. intros; pattern e. apply K_dec_set; eauto; try decide equality; clear e. intros; destruct (shatter_word_S w') as (?, (w'', H)); rewrite H in *; clear H. rewrite (wtl_eq_rect_S _ _ _ e0 (trans_S_comm _ _)); simpl. assert (S (sz + sz') = sz' + S sz) by omega. replace (eq_rect (S (sz' + sz)) word (WS x0 w'') (sz' + S sz) (trans_S_comm sz' sz)) with (eq_rect (S (sz + sz')) word (WS x0 (eq_rect _ _ w'' _ (trans_plus_comm _ _))) (sz' + S sz) H). erewrite <- (IHsz' x0 sz _ (trans_plus_comm _ _)). repeat f_equal. { generalize (trans_plus_comm sz' sz); intros; clear. revert sz' x0 w'' e; induction sz; simpl. - intro; rewrite <- plus_n_O; intros. destruct e; reflexivity. - intro; rewrite <- (trans_S_comm sz' sz); intros. intros; destruct (shatter_word_S w'') as (?, (w', H)); rewrite H in *; clear H. simpl. rewrite (IHsz sz' x w' (trans_plus_comm _ _)); repeat f_equal. erewrite eq_rect_WS; eauto. } { eapply eq_rect_split_tl. } revert H; clear. revert w''; generalize (trans_S_comm sz' sz). rewrite (trans_plus_comm sz' sz); intros; simpl. destruct e; simpl. rewrite eq_rect_WS with (e' := eq_refl _); reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Logic.Eqdep_dec Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.Sequence Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.AlignedEncodeMonad Coq.Vectors.Vector Coq.ZArith.ZArith Bedrock.Word