proposition: Lemma CorrectAlignedEncoderForFormatNChar' (addE_addE_plus : forall ce n m, addE (addE ce n) m = addE ce (n + m)) {sz} : forall encoder, (CorrectAlignedEncoder (format_word (monoidUnit := ByteString_QueueMonoidOpt)) (fun sz => encoder sz)) -> CorrectAlignedEncoder (format_word (monoidUnit := ByteString_QueueMonoidOpt)) (fun sz' => AppendAlignedEncodeM (fun v idx w => @SetCurrentByte _ _ sz' v idx (split1' 8 sz w)) (fun v idx w => encoder sz' v idx (split2' 8 sz w))).
proof: Proof. intros; pose proof (format_words addE_addE_plus (n := 8) (m := sz)) as H'; eapply refine_CorrectAlignedEncoder. split. - unfold flip, pointwise_relation; eapply H'. - intros; intro. eapply H. unfold compose, format_word; computes_to_econstructor; eauto. unfold compose, format_word; computes_to_econstructor; eauto. - eapply refine_CorrectAlignedEncoder. split; intros. rewrite <- split2'_eq, <- split1'_eq. 3: eapply CorrectAlignedEncoderForThenC. instantiate (1 := Projection_Format format_word (split2' 8 sz)). rewrite refine_sequence_Format. instantiate (1 := Projection_Format format_word (split1' 8 sz)). unfold compose, Bind2; rewrite refine_Projection_Format; f_equiv. intro; rewrite refine_Projection_Format; f_equiv. 2: eapply CorrectAlignedEncoderForProjection_Format; eauto. + intro. eapply H. rewrite <- split2'_eq, <- split1'_eq in H0. unfold sequence_Format. unfold compose, Bind2 in *; computes_to_inv; computes_to_econstructor. apply refine_Projection_Format; eauto. computes_to_econstructor. apply refine_Projection_Format; eauto. subst; eauto. + intros. instantiate (1 := (@CorrectAlignedEncoderForFormatChar_f (word (8 + sz)) (split1' 8 sz))). destruct (projT1 (CorrectAlignedEncoderForFormatChar_f (split1' 8 sz)) s env) eqn: ?. * eexists _, _; split; eauto. apply refine_Projection_Format; eauto. unfold format_word; eauto. * generalize (proj2 (proj1 (projT2 (CorrectAlignedEncoderForFormatChar_f (split1' 8 sz))) s env)); intro. eapply H1 in Heqo. eapply Heqo in H; intuition eauto. Defined.
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 Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedDecodeMonad