proposition: Theorem String_decode_correct {P : CacheDecode -> Prop} (P_OK : forall b cd, P cd -> P (addD cd b)) : forall sz, CorrectDecoder monoid (fun ls => length ls = sz) (fun ls => length ls = sz) eq format_string (decode_string sz) P format_string.
proof: Proof. split. { intros env env' xenv l l' ext ? Eeq Ppred Penc. subst. generalize dependent env. revert env' xenv l' env_OK. induction l. { intros. inversion Penc; subst; clear Penc. rewrite mempty_left; eexists _, _; intuition eauto. simpl; eauto. apply add_correct; eauto. } { intros. 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. rewrite <- mappend_assoc, H; simpl; split_and; subst. destruct (IHl _ _ _ H4 _ H1 Penc') as [? [? ?] ]. split_and; subst. setoid_rewrite H3; simpl; eexists _, _; intuition eauto. simpl; unfold Bind2; eauto. } } { induction sz; simpl; intros. { split; eauto; injections; repeat eexists; simpl; eauto using mempty_left. apply add_correct; eauto. } { destruct (decode_ascii t env') as [ [ [? ?] ?] | ] eqn: ? ; simpl in *; try discriminate. destruct (decode_string sz b c) as [ [ [? ?] ?] | ] eqn: ? ; simpl in *; try discriminate; injections. eapply (proj2 (Ascii_decode_correct P_OK)) in Heqo; eauto; destruct Heqo; destruct_ex; intuition; subst; eapply IHsz in Heqo0; eauto; destruct Heqo0; destruct_ex; intuition; subst. simpl. eexists _, _; intuition eauto. computes_to_econstructor; eauto. computes_to_econstructor; eauto. rewrite mappend_assoc; reflexivity. } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.AsciiOpt Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String