proposition: Lemma optimize_Fix {A} : forall (body : forall x : ByteString, (forall y : ByteString, lt_B y x -> (fun _ : ByteString => CacheDecode -> option (A * ByteString * CacheDecode)) y) -> (fun _ : ByteString => CacheDecode -> option (A * ByteString * CacheDecode)) x) (body' : forall x : nat, (forall y : nat, (lt y x)%nat -> (fun m : nat => t (word 8) m -> CacheDecode -> option (A * {n : _ & Vector.t _ n} * CacheDecode)) y) -> t (word 8) x -> CacheDecode -> option (A * {n : _ & Vector.t _ n} * CacheDecode) ) n (b : Vector.t _ n) (cd : CacheDecode) (body_Proper : forall (x0 : ByteString) (f g : forall y : ByteString, lt_B y x0 -> CacheDecode -> option (A * ByteString * CacheDecode)), (forall (y : ByteString) (p : lt_B y x0), f y p = g y p) -> body x0 f = body x0 g) (body'_Proper : forall (x0 : nat) (f g : forall y : nat, (lt y x0)%nat -> t (word 8) y -> CacheDecode -> option (A * {n0 : nat & t Core.char n0} * CacheDecode)), (forall (y : nat) (p : (lt y x0)%nat), f y p = g y p) -> body' x0 f = body' x0 g) , (forall n (b : Vector.t (word 8) n) (rec : forall x : ByteString, lt_B x (build_aligned_ByteString b) -> CacheDecode -> option (A * ByteString * CacheDecode)) (rec' : forall x : nat, (lt x n)%nat -> t Core.char x -> CacheDecode -> option (A * {n : _ & Vector.t _ n} * CacheDecode)) cd, (forall m cd b a b' cd' b_lt b_lt' , rec' m b_lt' b cd = Some (a, b', cd') -> rec (build_aligned_ByteString b) b_lt cd = Some (a, build_aligned_ByteString (projT2 b'), cd')) -> (forall m cd b b_lt b_lt' , rec' m b_lt' b cd = None -> rec (build_aligned_ByteString b) b_lt cd = None) -> body (build_aligned_ByteString b) rec cd = match (body' n rec' b cd) with | Some (a, b', cd') => Some (a, build_aligned_ByteString (projT2 b'), cd') | None => None end) -> Fix well_founded_lt_b (fun _ : ByteString => CacheDecode -> option (A * ByteString * CacheDecode)) body (build_aligned_ByteString b) cd = match Fix Wf_nat.lt_wf (fun m : nat => Vector.t (word 8) m -> CacheDecode -> option (A * { n : _ & Vector.t _ n} * CacheDecode)) body' n b cd with | Some (a, b', cd') => Some (a, build_aligned_ByteString (projT2 b'), cd') | None => None end.
proof: Proof. intros. revert cd b; pattern n. eapply (well_founded_ind Wf_nat.lt_wf); intros. rewrite Init.Wf.Fix_eq, Init.Wf.Fix_eq. apply H; intros. erewrite H0, H1; eauto. rewrite H0, H1; eauto. eauto. eauto. 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