proposition: Lemma optimize_Guarded_Decode {sz} {C} n : forall (a_opt : ByteString -> option C) (a_opt' : ByteString -> option C) v, (~ (n <= sz)%nat -> a_opt (build_aligned_ByteString v) = None) -> (le n sz -> a_opt (build_aligned_ByteString (Guarded_Vector_split n sz v)) = a_opt' (build_aligned_ByteString (Guarded_Vector_split n sz v))) -> a_opt (build_aligned_ByteString v) = If Coq.Init.Nat.leb n sz Then a_opt' (build_aligned_ByteString (Guarded_Vector_split n sz v)) Else None.
proof: Proof. intros; destruct (Coq.Init.Nat.leb n sz) eqn: ?. - apply Nat.leb_le in Heqb. rewrite <- H0. simpl; rewrite <- build_aligned_ByteString_eq_split'; eauto. eauto. - rewrite H; simpl; eauto. intro. rewrite <- Nat.leb_le in H1; congruence. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedString Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Formats.IPChecksum Fiat.Narcissus.Common.ComposeCheckSum Bedrock.Word