proposition: Lemma decode_string_peek_distinct : forall n xenv xenv' b b' l, decode_string n b xenv = Some (l, b', xenv') -> peekD xenv' = peekD (addD xenv (n * 8)).
proof: Proof. induction n; simpl; intros. - injections; eauto. - apply DecodeBindOpt2_inv in H; destruct H as [? [? [? [? ?] ] ] ]; injections; subst. destruct (decode_string n x0 x1) eqn: ?; simpl in *; try discriminate. destruct p; destruct p; injections. unfold decode_ascii in H. apply DecodeBindOpt2_inv in H; destruct H as [? [? [? [? ?] ] ] ]; injections; subst. eapply decode_word_peek_distinct in H; eauto. eapply IHn in Heqo; eauto; rewrite Heqo. destruct (peekD xenv) eqn: peekD_eq. + destruct (Compare_dec.lt_dec (1 + n + pointerT2Nat p) (pow2 14)). * destruct (addPeekSome _ 1 _ peekD_eq) as [p' [? ?] ]; try omega. simpl in H0; rewrite H0 in H. destruct (addPeekSome _ n _ H) as [p'' [? ?] ]; try omega. destruct (addPeekSome _ (S n) _ peekD_eq) as [p''' [? ?] ]; try omega. simpl in H4; rewrite H4. rewrite H1 in H3. simpl in H2; rewrite H2. f_equal. rewrite <- Nat2pointerT_pointerT2Nat, H5. rewrite <- (Nat2pointerT_pointerT2Nat p''), H3. f_equal. omega. * destruct (Compare_dec.lt_dec (1 + pointerT2Nat p) (pow2 14)). { destruct (addPeekSome _ 1 _ peekD_eq) as [p' [? ?] ]; try omega. pose proof (addPeekNone' xenv (S n)) as H'; simpl in H'; erewrite H'; eauto; clear H'. simpl in H0; rewrite H0 in H; eauto. eapply addPeekNone'; eauto. rewrite H1. simpl; omega. } { rewrite addPeekNone; auto. pose proof (addPeekNone' xenv (S n)) as H'; simpl in H'; erewrite H'; eauto; clear H'. rewrite H. eapply (addPeekNone' _ 1); eauto. } + rewrite !addPeekNone; auto. rewrite H. apply addPeekNone; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Computation.Core Fiat.Computation.FixComp Fiat.Computation.Notations Fiat.Computation.Refinements.General Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.AsciiOpt