proposition: Lemma format_SW_word {n} : forall b (w : word n) ce, refine (format_word (SW_word b w) ce) (`(bs, ce') <- format_word w (addE ce 1); ret (mappend (enqueue_opt b mempty) bs, ce')).
proof: Proof. induction n; simpl; intros. - shatter_word w; simpl. unfold format_word; simpl. autorewrite with monad laws. simpl; rewrite addE_addE_plus; rewrite mempty_right; reflexivity. - pose proof (shatter_word_S w); destruct_ex; subst. simpl. unfold format_word; simpl. autorewrite with monad laws; simpl. assert (computes_to (`(bs, ce') <- ret (encode_word' n x0 mempty, addE (addE ce 1) n); ret (mappend (enqueue_opt b mempty) bs, ce')) (mappend (enqueue_opt b mempty) (encode_word' n x0 mempty), addE (addE ce 1) n)) by repeat computes_to_econstructor. pose proof (IHn b x0 ce _ H). unfold format_word in H0. computes_to_inv; inversion H0; subst. rewrite H2. rewrite enqueue_mappend_opt. rewrite addE_addE_plus. 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