proposition: Lemma ByteAlign_Decode_w_Measure_lt {A} : forall (dec_a : nat -> ByteString -> CacheDecode -> option (A * ByteString * CacheDecode)) (n m : nat) (dec_a' : forall m n, Vector.t (word 8) (m + n) -> A) (cd : CacheDecode) (f : nat -> CacheDecode -> CacheDecode) (b : Vector.t (word 8) n) (m_OK : lt 0 m) decode_a_le (dec_fail : (lt n m)%nat -> forall b cd, dec_a m (build_aligned_ByteString (numBytes := n) b) cd = None), (forall n m b cd, dec_a m (build_aligned_ByteString b) cd = Some (dec_a' _ _ b, build_aligned_ByteString (snd (Vector_split m n b)), f m cd)) -> Decode_w_Measure_lt (dec_a m) (build_aligned_ByteString b) cd decode_a_le = match Compare_dec.lt_dec n m with | left _ => None | right n' => (Let a := dec_a' _ _ (Guarded_Vector_split m n b) in Some (a, lt_B_Guarded_Vector_split b m m_OK n' , f m cd)) end.
proof: Proof. intros. destruct (Compare_dec.lt_dec m n); destruct (Compare_dec.lt_dec n m); try omega. - assert (m + (n - m) = n) by omega. assert (forall b, Decode_w_Measure_lt (dec_a m) (build_aligned_ByteString b) cd decode_a_le = Decode_w_Measure_lt (dec_a m)(build_aligned_ByteString ( eq_rect _ _ (Guarded_Vector_split m n b) _ H0)) cd decode_a_le). { revert l; clear; intros. destruct (Decode_w_Measure_lt (dec_a m) (build_aligned_ByteString b) cd decode_a_le) as [ [ [? [? ?] ] ?] | ] eqn: ?. apply Decode_w_Measure_lt_eq' in Heqo. simpl in Heqo. destruct (Decode_w_Measure_lt (dec_a m) _ cd decode_a_le) as [ [ [? [? ?] ] ?] | ] eqn: ?. apply Decode_w_Measure_lt_eq' in Heqo0. unfold proj1_sig in Heqo0. rewrite <- build_aligned_ByteString_eq_split in Heqo0. rewrite Heqo0 in Heqo. injection Heqo; intros. rewrite H, H2; repeat f_equal. revert l1 l0. rewrite H1; intros; f_equal. f_equal; apply Core.le_uniqueness_proof. omega. apply ByteString_id. eapply Decode_w_Measure_lt_eq'' in Heqo0. rewrite <- build_aligned_ByteString_eq_split in Heqo0 by omega. rewrite Heqo0 in Heqo. discriminate. apply ByteString_id. erewrite (build_aligned_ByteString_eq_split m n) in Heqo by omega. rewrite Heqo; reflexivity. } rewrite H1. match goal with |- ?a = _ => destruct a as [ [ [? ?] ? ] | ] eqn: ? end. eapply Decode_w_Measure_lt_eq' in Heqo. assert (dec_a m (build_aligned_ByteString (Guarded_Vector_split m n b)) cd = Some (a, proj1_sig s, c)). { destruct s; simpl in *. rewrite <- Heqo. unfold build_aligned_ByteString; repeat f_equal; simpl. eapply ByteString_f_equal; simpl. instantiate (1 := eq_refl _); reflexivity. instantiate (1 := sym_eq H0). clear H1. destruct H0; reflexivity. } rewrite H in H2; injection H2; intros. rewrite H3, H5; unfold LetIn; simpl. repeat f_equal. destruct s; simpl in *. unfold lt_B_Guarded_Vector_split; simpl. clear H1; revert l0. rewrite <- H4; intros. f_equal. apply Core.le_uniqueness_proof. apply ByteString_id. apply Decode_w_Measure_lt_eq'' in Heqo. pose proof (H _ _ (Guarded_Vector_split m n b) cd). assert (Some (dec_a' _ _ (Guarded_Vector_split m n b), build_aligned_ByteString (snd (Vector_split m (n - m) (Guarded_Vector_split m n b))), f m cd) = None). { rewrite <- Heqo. rewrite <- H. repeat f_equal. eapply ByteString_f_equal; simpl. instantiate (1 := eq_refl _); reflexivity. instantiate (1 := sym_eq H0). clear H1. destruct H0; reflexivity. } discriminate. - eapply dec_fail in l; simpl. eapply Specs.Decode_w_Measure_lt_eq' in l. apply l. - assert (m = n) by omega; subst. assert (n + (n - n) = n) by omega. assert (forall b, Decode_w_Measure_lt (dec_a n) (build_aligned_ByteString b) cd decode_a_le = Decode_w_Measure_lt (dec_a n)(build_aligned_ByteString ( eq_rect _ _ (Guarded_Vector_split n n b) _ H0)) cd decode_a_le). { clear; intros. destruct (Decode_w_Measure_lt (dec_a n) (build_aligned_ByteString b) cd decode_a_le) as [ [ [? [? ?] ] ?] | ] eqn: ?. apply Decode_w_Measure_lt_eq' in Heqo. simpl in Heqo. destruct (Decode_w_Measure_lt (dec_a n) _ cd decode_a_le) as [ [ [? [? ?] ] ?] | ] eqn: ?. apply Decode_w_Measure_lt_eq' in Heqo0. unfold proj1_sig in Heqo0. rewrite <- build_aligned_ByteString_eq_split in Heqo0. rewrite Heqo0 in Heqo. injection Heqo; intros. rewrite H, H2; repeat f_equal. revert l l0. rewrite H1; intros; f_equal. f_equal; apply Core.le_uniqueness_proof. omega. apply ByteString_id. eapply Decode_w_Measure_lt_eq'' in Heqo0. rewrite <- build_aligned_ByteString_eq_split in Heqo0 by omega. rewrite Heqo0 in Heqo. discriminate. apply ByteString_id. erewrite (build_aligned_ByteString_eq_split n n) in Heqo by omega. rewrite Heqo; reflexivity. } rewrite H1. match goal with |- ?a = _ => destruct a as [ [ [? ?] ? ] | ] eqn: ? end. eapply Decode_w_Measure_lt_eq' in Heqo. assert (dec_a n (build_aligned_ByteString (Guarded_Vector_split n n b)) cd = Some (a, proj1_sig s, c)). { destruct s; simpl in *. rewrite <- Heqo. unfold build_aligned_ByteString; repeat f_equal; simpl. eapply ByteString_f_equal; simpl. instantiate (1 := eq_refl _); reflexivity. instantiate (1 := sym_eq H0). clear H1. destruct H0; reflexivity. } rewrite H in H2; injection H2; intros. rewrite H3, H5; unfold LetIn; simpl. repeat f_equal. destruct s; simpl in *. unfold lt_B_Guarded_Vector_split; simpl. clear H1; revert l. rewrite <- H4; intros. f_equal. apply Core.le_uniqueness_proof. apply ByteString_id. apply Decode_w_Measure_lt_eq'' in Heqo. pose proof (H _ _ (Guarded_Vector_split n n b) cd). assert (Some (dec_a' _ _ (Guarded_Vector_split n n b), build_aligned_ByteString (snd (Vector_split n (n - n) (Guarded_Vector_split n n b))), f n cd) = None). { rewrite <- Heqo. rewrite <- H. repeat f_equal. eapply ByteString_f_equal; simpl. instantiate (1 := eq_refl _); reflexivity. instantiate (1 := sym_eq H0). clear H1. destruct H0; reflexivity. } discriminate. 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