proposition: Lemma ByteString_mappend_BitString_into : forall l l', ByteString_append (BitString_into_ByteString l) (BitString_into_ByteString l') = BitString_into_ByteString (app l l').
proof: Proof. induction l; simpl. - unfold ByteString_append; simpl; eauto. - intro; rewrite <- IHl; clear IHl. unfold ByteString_append. destruct (BitString_into_ByteString l); simpl. unfold ByteString_push; simpl. destruct (eq_nat_dec padding0 7); subst. + unfold front at 1; unfold byteString at 1. unfold ByteString_push_word at 1; unfold padding at 1. unfold eq_rec_r, eq_rec, eq_rect, Logic.eq_sym. simpl fold_right. destruct (eq_nat_dec (padding (ByteString_push_word front0 (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0))) 7). * rewrite ByteString_push_char_WS. assert (0 = padding (ByteString_push a ((ByteString_push_word front0) (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0)))). { induction (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0). unfold ByteString_push. destruct (eq_nat_dec (padding (ByteString_push_word front0 {| padding := padding0; front := front1; paddingOK := paddingOK1; byteString := byteString1 |})) 7). simpl; reflexivity. exfalso; apply n. apply e. } apply ByteString_mappend_f_equal with (p_eq := H). apply le_uniqueness_proof. destruct (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0). unfold front at 3; unfold padding at 2. destruct (ByteString_push_word front0 {| padding := padding0; front := front1; paddingOK := paddingOK1; byteString := byteString1 |}). revert H; unfold ByteString_push; simpl in *. destruct (eq_nat_dec padding1 7); simpl; intros. apply eq_rect_eq_dec; eauto using eq_nat_dec. congruence. destruct (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0). unfold byteString at 2. unfold ByteString_push at 1. destruct (ByteString_push_word front0 {| padding := padding0; front := front1; paddingOK := paddingOK1; byteString := byteString1 |}). simpl padding. destruct (eq_nat_dec padding1 7). simpl. repeat f_equal. unfold eq_rec_r, eq_rec_r, eq_rec. unfold Logic.eq_sym. unfold eq_rect. assert (e0 = e) by (apply eq_proofs_unicity; intros; omega). rewrite H0; eauto. simpl in e; congruence. * rewrite ByteString_push_char_WS. assert (S (padding (ByteString_push_word front0 (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0))) = padding (ByteString_push a ((ByteString_push_word front0) (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0)))). { destruct (ByteString_push_word front0 (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0)). simpl in *. unfold ByteString_push. destruct (eq_nat_dec (padding {| padding := padding0; front := front1; paddingOK := paddingOK1; byteString := byteString1 |}) 7). simpl in *|-; congruence. reflexivity. } apply ByteString_mappend_f_equal with (p_eq := H). apply le_uniqueness_proof. unfold front at 3; unfold padding at 2. destruct (ByteString_push_word front0 (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0)). simpl. revert H; unfold ByteString_push; simpl in *. destruct (eq_nat_dec padding0 7). simpl; intros. congruence. simpl; intros. apply eq_rect_eq_dec; eauto using eq_nat_dec. destruct (ByteString_push_word front0 (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0)). simpl. revert H; unfold ByteString_push; simpl in *. destruct (eq_nat_dec padding0 7). simpl; intros. congruence. simpl; intros. reflexivity. + unfold front at 1; unfold byteString at 1. destruct (eq_nat_dec (padding (ByteString_push_word front0 (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0))) 7). setoid_rewrite ByteString_push_word_WS. assert (0 = padding (ByteString_push a ((ByteString_push_word front0) (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0)))). { induction (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0). unfold ByteString_push. destruct (eq_nat_dec (padding (ByteString_push_word front0 {| padding := padding1; front := front1; paddingOK := paddingOK1; byteString := byteString1 |})) 7). simpl; reflexivity. congruence. } apply ByteString_mappend_f_equal with (p_eq := H). apply le_uniqueness_proof. destruct (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0). unfold front at 3; unfold padding at 2. destruct (ByteString_push_word front0 {| padding := padding1; front := front1; paddingOK := paddingOK1; byteString := byteString1 |}). revert H; unfold ByteString_push; simpl in *. destruct (eq_nat_dec padding2 7); simpl; intros. apply eq_rect_eq_dec; eauto using eq_nat_dec. congruence. destruct (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0). unfold byteString at 2. unfold ByteString_push at 1. destruct (ByteString_push_word front0 {| padding := padding1; front := front1; paddingOK := paddingOK1; byteString := byteString1 |}). simpl padding. destruct (eq_nat_dec padding2 7). simpl. repeat f_equal. apply eq_proofs_unicity; intros; omega. simpl in e; congruence. setoid_rewrite ByteString_push_word_WS. assert (S (padding (ByteString_push_word front0 (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0))) = padding (ByteString_push a ((ByteString_push_word front0) (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0)))). { destruct (ByteString_push_word front0 (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0)). simpl in *. unfold ByteString_push. destruct (eq_nat_dec (padding {| padding := padding1; front := front1; paddingOK := paddingOK1; byteString := byteString1 |}) 7). simpl in *|-; congruence. reflexivity. } apply ByteString_mappend_f_equal with (p_eq := H). apply le_uniqueness_proof. unfold front at 3; unfold padding at 2. destruct (ByteString_push_word front0 (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0)). simpl. revert H; unfold ByteString_push; simpl in *. destruct (eq_nat_dec padding1 7). simpl; intros. congruence. simpl; intros. apply eq_rect_eq_dec; eauto using eq_nat_dec. destruct (ByteString_push_word front0 (fold_right ByteString_push_char (BitString_into_ByteString l') byteString0)). simpl. revert H; unfold ByteString_push; simpl in *. destruct (eq_nat_dec padding1 7). simpl; intros. congruence. simpl; intros. reflexivity. 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