proposition: Theorem FixList_decode_correct : forall sz , CorrectDecoder monoid (fun ls => |ls| = sz /\ forall x, In x ls -> A_predicate x) (fun ls => |ls| = sz /\ forall x, In x ls -> A_predicate x) eq format_list (decode_list sz) A_cache_inv format_list.
proof: Proof. split. { intros env env' xenv l l' ext ? Eeq Ppred Penc. intuition; subst. revert H0. generalize dependent env. generalize dependent env'. generalize dependent xenv. generalize dependent l'. induction l. { intros. simpl in *; intuition; computes_to_inv; injections; simpl. rewrite mempty_left; eexists _, _; intuition eauto. simpl; computes_to_econstructor. } { intros; simpl in *. assert (A_predicate a) by eauto. unfold Bind2 in Penc; computes_to_inv; subst. destruct v; destruct v0; simpl in *. injections. destruct (proj1 A_decode_pf _ _ _ _ _ (mappend t0 ext) env_OK Eeq H Penc) as [ ? [? [? xenv_OK] ] ]. intuition; destruct_ex. setoid_rewrite <- mappend_assoc; setoid_rewrite H1; simpl; subst. destruct (IHl t0 xenv _ H6 c) as [? [? ?] ]; intuition eauto; subst. setoid_rewrite H5; simpl. eexists _, _; intuition. simpl; unfold Bind2; eauto. } } { induction sz; simpl; intros. - injections; simpl; repeat eexists; simpl; intuition eauto. symmetry; apply mempty_left. - destruct (A_decode t env') as [ [ [? ?] ?] | ] eqn: ? ; simpl in *; try discriminate. destruct (decode_list sz t0 c) as [ [ [? ?] ?] | ] eqn: ? ; simpl in *; try discriminate; injections. eapply (proj2 A_decode_pf) in Heqo; eauto; destruct Heqo; destruct_ex; intuition; subst; eapply IHsz in Heqo0; eauto; destruct Heqo0; destruct_ex; intuition; subst. simpl. eexists _, _; simpl; unfold id; intuition eauto. computes_to_econstructor; eauto. computes_to_econstructor; eauto. simpl. rewrite mappend_assoc; reflexivity. subst; eauto. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.Base.FixFormat Coq.Lists.List