proposition: Lemma ByteString_dequeue_into_BitString : forall (l : BitString), ByteString_dequeue (queue_into_ByteString l) = match l with | b :: l' => Some (b, queue_into_ByteString l') | _ => None end.
proof: Proof. intro; destruct (queue_into_ByteString_eq_split_Vector_bool l); rewrite H. generalize (le_refl (length l)); remember (length l). setoid_rewrite Heqn at 1; clear Heqn; revert l x H; induction n. - intros; destruct l; simpl; intros. + reflexivity. + inversion H0. - intros l x H H0; destruct l as [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? ] ] ] ] ] ] ] ]. + simpl; reflexivity. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue; simpl; repeat f_equal; eapply le_uniqueness_proof. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue, ByteString_enqueue; simpl. repeat f_equal; eapply le_uniqueness_proof. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue, ByteString_enqueue; simpl. repeat f_equal; eapply le_uniqueness_proof. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue; simpl. unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. repeat f_equal; eapply le_uniqueness_proof. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue; simpl. unfold ByteString_enqueue at 4; simpl. unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl. unfold ByteString_enqueue at 1; simpl. repeat f_equal; eapply le_uniqueness_proof. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue; simpl. unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. repeat f_equal; eapply le_uniqueness_proof. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue; simpl. unfold ByteString_enqueue at 6; simpl; unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. repeat f_equal; eapply le_uniqueness_proof. + unfold queue_into_ByteString, ByteString_id; simpl. unfold ByteString_enqueue at 7; simpl; unfold ByteString_enqueue at 6; simpl; unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. simpl in *. destruct (split_Vector_bool l) eqn : ? ; simpl in *. simpl in H. destruct (queue_into_ByteString_eq_split_Vector_bool l). assert (length l <= n)%nat as l_OK by omega. pose proof (IHn l _ H1 l_OK). unfold queue_into_ByteString in H; simpl in H. unfold ByteString_enqueue at 7 in H; simpl in H; unfold ByteString_enqueue at 6 in H; simpl in H; unfold ByteString_enqueue at 5 in H; simpl in H; unfold ByteString_enqueue at 4 in H; simpl in H; unfold ByteString_enqueue at 3 in H; simpl in H; unfold ByteString_enqueue at 2 in H; simpl in H; unfold ByteString_enqueue at 1 in H; simpl in H. destruct (split_Vector_bool l); simpl in *. simpl in H2; revert H2; injection Heqp; clear. intros G G'. revert x x0; try rewrite G, G'; subst; intros. unfold ByteString_dequeue in *; repeat match goal with |- context [ByteString_enqueue_subproof0 ?z ?q ?m] => generalize (ByteString_enqueue_subproof0 z q m); intros; simpl in * | |- context [ByteString_enqueue_subproof ?z ?q ?m] => generalize (ByteString_enqueue_subproof z q m); intros; simpl in * end. destruct s as [[ | ?] ? ]; simpl in *. destruct s0 as [[ | ?] ? ]; simpl in *. * destruct (CharList_dequeue (Vector.cons _ (WS b (WS b6 (WS b5 (WS b4 (WS b3 (WS b2 (WS b1 (WS b0 WO)))))))) _ (ByteBuffer.nil))) as [ [? ?] ] eqn : ? ; try discriminate. destruct l; simpl in H2; try discriminate; injections. simpl. f_equal; f_equal; eapply byteString_f_equal; simpl; try (instantiate (1 := eq_refl); reflexivity). * destruct (word_dequeue w). destruct l; try discriminate; injections; simpl. match goal with |- context[fold_left _ _ ?q] => replace q with (queue_into_ByteString [b0; b1; b2; b3; b4; b5; b6; b8]); [ | unfold queue_into_ByteString; simpl; unfold ByteString_enqueue at 7; simpl; unfold ByteString_enqueue at 6; simpl; unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl ] end. rewrite <- queue_into_ByteString_app. f_equal; f_equal. rewrite <- ByteString_enqueue_ByteString_into_BitString. rewrite <- H. clear. unfold queue_into_ByteString at 1; simpl. unfold ByteString_enqueue at 7; simpl; unfold ByteString_enqueue at 6; simpl; unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. erewrite <- massage_queue_into_ByteString. eapply byteString_f_equal; simpl; instantiate (1 := eq_refl); try reflexivity. eapply byteString_f_equal; simpl; instantiate (1 := eq_refl); try reflexivity. * destruct s0 as [[ | ?] ? ]; simpl in *. destruct (CharList_dequeue t) as [ [? ?] ? ] eqn : ? . destruct l; try discriminate; injections; simpl. match goal with |- context[fold_left _ _ ?q] => replace q with (queue_into_ByteString [b0; b1; b2; b3; b4; b5; b6; b8]) by (unfold queue_into_ByteString; simpl; unfold ByteString_enqueue at 7; simpl; unfold ByteString_enqueue at 6; simpl; unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl; repeat f_equal; intros; apply le_uniqueness_proof) end. rewrite <- queue_into_ByteString_app. rewrite <- ByteString_enqueue_ByteString_into_BitString. rewrite <- H. clear. repeat f_equal. unfold queue_into_ByteString at 1; simpl. unfold ByteString_enqueue at 7; simpl; unfold ByteString_enqueue at 6; simpl; unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. erewrite <- massage_queue_into_ByteString; reflexivity. destruct l; try discriminate; injections; simpl. destruct (CharList_dequeue t) as [ [? ?] ? ] eqn : ? ; try discriminate; destruct (word_dequeue w). discriminate. destruct (CharList_dequeue t) as [ [? ?] ? ] eqn : ? ; try discriminate; destruct (word_dequeue w). match goal with |- context[fold_left _ _ ?q] => replace q with (queue_into_ByteString [b0; b1; b2; b3; b4; b5; b6; b8]); [ | unfold queue_into_ByteString; simpl; unfold ByteString_enqueue at 7; simpl; unfold ByteString_enqueue at 6; simpl; unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl ] end. rewrite <- queue_into_ByteString_app. rewrite <- ByteString_enqueue_ByteString_into_BitString. f_equal; f_equal. injection H2; intros. rewrite <- H. unfold queue_into_ByteString at 1; simpl. unfold ByteString_enqueue at 7; simpl; unfold ByteString_enqueue at 6; simpl; unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. erewrite <- massage_queue_into_ByteString; reflexivity. simpl. eapply byteString_f_equal; simpl; instantiate (1 := eq_refl); try reflexivity. simpl. injection H2; intros; subst. 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 Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Formats.ByteBuffer