proposition: Theorem String_decode_with_term_char_correct {P : CacheDecode -> Prop} : forall term_char (P_OK : cache_inv_Property P (fun P => forall b cd, P cd -> P (addD cd b))), CorrectDecoder monoid (fun s => forall s1 s2, s <> s1 ++ String term_char s2)%string (fun s => forall s1 s2, s <> s1 ++ String term_char s2)%string eq (format_string_with_term_char term_char) (decode_string_with_term_char term_char) P (format_string_with_term_char term_char).
proof: Proof. split. { intros env env' xenv s s' ext ? Eeq Ppred Penc. subst. generalize dependent env. revert env' xenv s' env_OK. induction s. { unfold id in *; intros. unfold format_string_with_term_char in Penc. unfold decode_string_with_term_char. simpl in Penc; unfold Bind2 in *; computes_to_inv; subst; simpl in *. rewrite mempty_right in Penc''; inversion Penc''; subst. destruct v; simpl in *. eapply Ascii_decode_correct in Penc; eauto. unfold id in *. destruct_ex; split_and. eexists _, _; rewrite Init.Wf.Fix_eq. eapply Decode_w_Measure_lt_eq in H0; destruct_ex. rewrite H0; simpl. subst; destruct (ascii_dec x x); simpl; try congruence. intuition eauto. unfold format_string_with_term_char; simpl; unfold Bind2; repeat computes_to_econstructor; eauto. simpl;rewrite mempty_right; eauto. simpl. intros. repeat (apply functional_extensionality; intros; f_equal). rewrite H3. eauto. } { intros. unfold format_string_with_term_char in Penc; unfold decode_string_with_term_char. simpl in *. unfold Bind2 in *; computes_to_inv; subst. injection Penc''; intros; subst. destruct v; destruct v0. destruct (proj1 (Ascii_decode_correct P_OK) _ _ _ _ _ (mappend b0 ext) env_OK Eeq I Penc) as [? [? [? xenv_OK] ] ]. simpl. unfold format_string_with_term_char in IHs. simpl in Penc'; eapply IHs in Penc'. destruct Penc'; intuition. subst. destruct_ex; split_and. eexists _, _; rewrite Init.Wf.Fix_eq. eapply Decode_w_Measure_lt_eq in H; destruct_ex. rewrite <- mappend_assoc, H; simpl. destruct (ascii_dec x term_char); simpl. - exfalso. subst; eapply (Ppred "")%string; simpl; reflexivity. - intuition. unfold decode_string_with_term_char in H1. rewrite H1; simpl; subst; eauto. unfold format_string_with_term_char; simpl; unfold Bind2; computes_to_econstructor; eauto. subst; computes_to_econstructor; eauto. subst; eauto. eauto. - intros; repeat (apply functional_extensionality; intros; f_equal). rewrite H7; reflexivity. - unfold id in *; unfold not; intros; eapply (Ppred (String a s1) s2); simpl; congruence. - intuition eauto. - intuition eauto. } } { unfold decode_string_with_term_char, format_string_with_term_char; intros env env' xenv' data bin; revert env env' xenv' data. eapply (@well_founded_induction _ _ well_founded_lt_b) with (a := bin); intros. rewrite Coq.Init.Wf.Fix_eq in H2; auto; simpl. apply DecodeBindOpt2_inv in H2; destruct H2 as [? [? [? [? ?] ] ] ]; injections; subst. destruct (decode_ascii x env') as [ [ [? ?] ?] | ] eqn: ? . - destruct (Decode_w_Measure_lt_eq _ _ _ ascii_decode_lt Heqo). rewrite H4 in H2; injections. destruct (ascii_dec x0 term_char) eqn: ?; simpl in H3. + injections. eapply (proj2 (Ascii_decode_correct P_OK)) in Heqo; eauto; destruct Heqo as [? [? ?] ]; destruct_ex; intuition; subst. simpl. eexists _, _; intuition. computes_to_econstructor; eauto. computes_to_econstructor; eauto. simpl; rewrite mempty_right; eauto. destruct s1; simpl in *; discriminate. eauto. + eapply (proj2 (Ascii_decode_correct P_OK)) in Heqo; eauto; destruct Heqo as [? [? ?] ]; destruct_ex. symmetry in H3; apply DecodeBindOpt2_inv in H3; destruct H3 as [? [? [? [? ?] ] ] ]; injections; subst. eapply H in H3; intuition. destruct_ex; intuition; subst; eauto. eexists _, _; intuition. simpl. computes_to_econstructor; eauto. computes_to_econstructor; eauto. simpl; rewrite mappend_assoc; eauto. unfold id in *; destruct s1; simpl in *; injections; intros; congruence. simpl; eauto. simpl; eauto. - eapply Decode_w_Measure_lt_eq' in Heqo; rewrite Heqo in H2; discriminate. - intros; repeat (apply functional_extensionality; intros; f_equal). rewrite H3; reflexivity. } Qed.
imports: Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.AsciiOpt Bedrock.Word Coq.Strings.Ascii Coq.Strings.String