proposition: Lemma monoid_get_encode_word' {T} {monoid : Monoid T} {monoid_opt : QueueMonoidOpt monoid bool} (sz : nat) : forall (w : word sz) (ext : T), monoid_get_word sz (mappend (encode_word' _ w mempty) ext) = Some w.
proof: Proof. induction sz; simpl; intros; try shatter_word w; simpl in *. - reflexivity. - destruct (shatter_word_S w) as (?, (?, ?)); subst; simpl. rewrite enqueue_opt_format_word. rewrite <- !mappend_assoc. destruct sz. + shatter_word x0; simpl. rewrite mempty_left. erewrite dequeue_mappend_opt; eauto using dequeue_head_opt. + rewrite dequeue_opt_Some'. pose proof (IHsz (WS x (word_split_tl x0)) ext). simpl in *. rewrite enqueue_opt_format_word in H. rewrite <- mappend_assoc in H. destruct (dequeue_opt (mappend (encode_word' sz (word_split_tl x0) mempty) (mappend (enqueue_opt x mempty) ext))) as [ [? ?] | ]; simpl in *; try discriminate. destruct (monoid_get_word sz t); try discriminate. injections. rewrite H0. simpl. rewrite <- (word_split_SW x0); auto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.BaseFormats