proposition: Lemma queue_into_ByteString_eq_split_BitString : forall l, exists paddingOK', queue_into_ByteString l = {| front := projT2 (snd (split_BitString l)); paddingOK := paddingOK'; byteString := fst (split_BitString l) |}.
proof: Proof. intro; generalize (le_refl (length l)); remember (length l). unfold queue_into_ByteString. replace (fst (split_BitString l)) with ((byteString ByteString_id) ++ (fst (split_BitString l))) by reflexivity. assert (padding ByteString_id = 0) as H' by reflexivity; revert H'. generalize ByteString_id. setoid_rewrite Heqn at 1; clear Heqn; revert l; induction n. - intros; destruct l; simpl; intros. + setoid_rewrite app_nil_r; eexists (lt_0_Sn _). eauto using empty_padding_ByteString_eq_byteString. + match goal with | [ H : (_ <= 0)%nat |- _ ] => inversion H end. - intros l b H0 H; destruct l as [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? ] ] ] ] ] ] ] ]; try match goal with |- exists _ : lt ?z 8, _ => let H := fresh in try (assert (lt z 8) as H by (simpl; omega); exists H; simpl in H); solve [unfold queue_into_ByteString, ByteString_id; simpl; destruct b; simpl in *; subst; erewrite ByteString_enqueue_simpl by (simpl; omega); shatter_word front0; repeat f_equal; eauto using app_nil_r, le_uniqueness_proof] end. + unfold queue_into_ByteString, ByteString_id; simpl; unfold ByteString_enqueue; simpl; repeat f_equal; rewrite app_nil_r; eauto using empty_padding_ByteString_eq_byteString. + destruct (split_BitString l) eqn : ?. destruct b. destruct (IHn l {| front := WO; paddingOK := lt_0_Sn _; byteString := byteString0 ++ [ WS b7 (WS b6 (WS b5 (WS b4 (WS b3 (WS b2 (WS b1 (WS b0 WO)))))))] |}). simpl in *; omega. simpl in *; omega. simpl split_BitString. revert x H0 H1; rewrite Heqp; intros; clear Heqp. exists x. simpl byteString. unfold fst. rewrite (app_cons_assoc _ _ l0). match goal with H : _ = ?a |- _ = ?a' => replace a' with a by reflexivity; rewrite <- H end. clear H1 H x s IHn. simpl in H0. revert front0 paddingOK0; rewrite H0. intros; shatter_word front0. erewrite <- fold_left_enqueue_simpl. apply f_equal. apply f_equal. reflexivity. Unshelve. simpl; omega. simpl; omega. simpl; omega. simpl; omega. simpl; omega. simpl; omega. simpl; omega. omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs